lambda/test2.icl

   1 module test2
   2
   3 import Control.Applicative
   4 import Control.Monad
   5 import Data.Functor
   6 import Data.Either
   7 import Data.Maybe
   8 import StdEnv
   9
  10 :: In a b = In infixl 0 a b
  11 class lambda v w
  12 where
  13         \| :: ((v a) -> w) -> ((v a) -> w)
  14
  15 class expr v
  16 where
  17         lit :: a -> v a | toString a
  18         (+.) infixl 6 :: (v a) (v a) -> v a | + a
  19         (-.) infixl 6 :: (v a) (v a) -> v a | - a
  20         (*.) infixl 6 :: (v a) (v a) -> v a | * a
  21         (/.) infixl 6 :: (v a) (v a) -> v a | /, zero, == a
  22         (==.) infix 4 :: (v a) (v a) -> v Bool | == a
  23         If :: (v Bool) (v a) (v a) -> v a
  24
  25 class let v w
  26 where
  27         lett :: (w -> In w (v b)) -> v b
  28
  29 :: Print a = Print (Int [String] -> [String])
  30 unPrint (Print f) = f
  31 print :: (Print a) -> [String]
  32 print f = unPrint f 0 []
  33 var d i _ c = [d,toString i:c]
  34 instance expr Print
  35 where
  36         lit a = Print \i c->[toString a:c]
  37         (+.) l r = Print \i c->["(":unPrint l i ["+":unPrint r i [")":c]]]
  38         (-.) l r = Print \i c->["(":unPrint l i ["-":unPrint r i [")":c]]]
  39         (*.) l r = Print \i c->["(":unPrint l i ["*":unPrint r i [")":c]]]
  40         (/.) l r = Print \i c->["(":unPrint l i ["/":unPrint r i [")":c]]]
  41         (==.) l r = Print \i c->["(":unPrint l i ["==":unPrint r i [")":c]]]
  42         If p t e = Print \i c->["if ":unPrint p i [" ":unPrint t i [" ":unPrint e i c]]]
  43 instance lambda Print (Print a)
  44 where
  45         \| :: ((Print a) -> Print b) -> ((Print a) -> Print b)
  46         \| def = \arg->Print \i c->["(\\":var "x" i i ["->":unPrint (def (Print (var "x" i))) (inc i) [") ":unPrint arg i c]]]
  47 //NB: Dit moet ook te doen zijn vrees ik maar het lukt mij zo gauw niet
  48 //instance lambda Print ((Print a) -> b) | lambda Print (Print b)
  49 //where
  50 //      \| def = \arg arg0->Print \i c->["(\\":var "x" i i ["->":unPrint ((\| def (Print (var "x" i))) arg0) (inc i) [") ":unPrint arg i c]]]
  51 instance lambda Print ((Print a) -> Print b)
  52 where
  53         \| :: ((Print a) (Print b) -> Print c) -> ((Print a) (Print b) -> Print c)
  54         \| def = \arg0 arg1->Print \i c->["(\\":var "x" i i ["->":unPrint (def (Print (var "x" i)) (Print \_ c->c)) (inc i) [") ":unPrint arg0 i [" ":unPrint arg1 i c]]]]
  55 instance lambda Print ((Print a) (Print b) -> Print c)
  56 where
  57         \| :: ((Print a) (Print b) (Print c) -> Print d) -> ((Print a) (Print b) (Print c) -> Print d)
  58         \| def = \arg0 arg1 arg2->Print \i c->["(\\":var "x" i i ["->":unPrint (def (Print (var "x" i)) (Print \_ c->c) (Print \_ c->c)) (inc i) [") ":unPrint arg0 i [" ":unPrint arg1 i [" ":unPrint arg2 i c]]]]]
  59 instance let Print (Print a)
  60 where
  61         lett def = Print \i c->let (x In y) = def (Print (var "v" i))
  62                 in ["(let ":var "v" i i ["=":unPrint x i ["\nin ":unPrint y (inc i) [")":c]]]]
  63 //NB: dit dan misschien ook wel
  64 //instance let Print ((Print a) -> b) | let Print b
  65 //where
  66 //      lett def =
  67 instance let Print ((Print a) -> Print b)
  68 where
  69         lett def = Print \i c->let (x In y) = def (\a->Print \_ c->["(":var "v" i i [" ":unPrint a i [")":c]]])
  70                 in ["(let ":var "v" i i ["=":unPrint (x (Print \_ c->c)) i ["\nin ":unPrint y (inc i) [")":c]]]]
  71 instance let Print ((Print a) (Print b) -> Print c)
  72 where
  73         lett def = Print \i c->let (x In y) = def (\a0 a1->Print \_ c->["(":var "v" i i [" ":unPrint a0 i [" ":unPrint a1 i [")":c]]]])
  74                 in ["(let ":var "v" i i ["=":unPrint (x (Print \_ c->c) (Print \_ c->c)) i ["\nin ":unPrint y (inc i) [")":c]]]]
  75
  76 meval :: (?a) -> ?a
  77 meval a = a
  78 instance expr (?)
  79 where
  80         lit a = pure a
  81         (+.) l r = (+) <$> l <*> r
  82         (-.) l r = (-) <$> l <*> r
  83         (*.) l r = (*) <$> l <*> r
  84         (/.) l r = l >>= \l->r >>= \r->if (r == zero) ?None (pure (l/r))
  85         (==.) l r = (==) <$> l <*> r
  86         If p t e = p >>= \b->if b t e
  87 instance lambda (?) a
  88 where
  89         \| def = def
  90 instance let (?) a
  91 where
  92         lett def = let (x In y) = def x in y
  93
  94 Start =
  95 //      ( "--eval t1: ", eval t1
  96         ( "\n--meval t0: ", meval t0
  97         , "\n--print t0:\n", print t0
  98         , "\n--meval t1: ", meval t1
  99         , "\n--print t1:\n", print t1
 100         , "\n--meval t2: ", meval t2
 101         , "\n--print t2:\n", print t2
 102         , "\n--meval t3: ", meval t3
 103         , "\n--print t3:\n", print t3
 104         )
 105 //      , "--eval t2: ", eval t2
 106 //      , "\n--meval t2: ", meval t2
 107 //      , "\n--ieval t2: ", runIdentity t2
 108 //      , "\n--print t2:\n", print t2
 109 //      )
 110 //t0 :: v Int | let v ((v Int) -> v Int) & lambda v (v Int) & expr v
 111 t0 = lett \id = (\| \x->x)
 112         In id (lit 42)
 113 //t1 :: v Int | let v ((v Int) -> v Int) & lambda v (v Int) & expr v
 114 t1 =
 115            lett \id     = (\| \x->x)
 116         In lett \fac    = (\| \n->If (n ==. lit 0) (lit 1) (n *. (fac (n -. lit 1))))
 117         In fac (id (lit 10))
 118 //t2 :: v Int | let v ((v Int) (v Int) -> v Int) & lambda v (v Int) & lambda v ((v Int) -> v Int) & expr v
 119 t2 = (\| \x-> (\| \y->x +. y)) (lit 11) (lit 31)
 120
 121 t3 = (\| \x-> (\| \y-> (\| \z->x +. y +. z))) (lit 11) (lit 15) (lit 16)
 122 //
 123 ////Dit wil je niet zelf moeten typen......
 124 //t2 :: v Int | let, lambda, expr v & TC (v Int) & TC (v ((v Int) -> v Int)) & TC (v ((v ((v Int) -> v Int)) -> v ((v Int) -> v Int)))
 125 //t2 =
 126 //         lett \id     = (\| \x->x)
 127 //      In lett \fix    = (\| \f->lett \x=f x In x)
 128 //      In lett \fac    = (\| \n->If (n ==. lit 0) (lit 1) (n *. (fac (n -. lit 1))))
 129 //      In lett \facfix = (\| \n->(fix ( \| \fac-> \| \n->If (n ==. lit 0) (lit 1) (n *. (fac (n -. lit 1))))) n)
 130 //      In facfix (id (lit 10))