lambda/test.icl

   1 module test
   2
   3 import Control.Applicative
   4 import Control.Monad
   5 import Data.Func
   6 import Data.Functor
   7 import Data.Either
   8 import Data.Maybe
   9 import StdEnv
  10
  11 :: In a b = In infixl 0 a b
  12 class lambda v
  13 where
  14         (@) infixr 1 :: (v ((v a) -> v b)) (v a) -> v b
  15         \| :: ((v a) -> v b) -> v ((v a) -> v b) | TC a & TC b & TC (v b)
  16
  17 class expr v
  18 where
  19         lit :: a -> v a | toString a
  20         (+.) infixl 6 :: (v a) (v a) -> v a | + a
  21         (-.) infixl 6 :: (v a) (v a) -> v a | - a
  22         (*.) infixl 6 :: (v a) (v a) -> v a | * a
  23         (/.) infixl 6 :: (v a) (v a) -> v a | / a
  24         (==.) infix 4 :: (v a) (v a) -> v Bool | == a
  25         If :: (v Bool) (v a) (v a) -> v a
  26
  27 class let v
  28 where
  29         lett :: ((v a) -> In (v a) (v b)) -> v b | TC a
  30
  31 :: St a = St (Env -> Either String (a, Env))
  32 :: Env :== [(Int, Dynamic)]
  33 instance Functor St where fmap f m = m >>= pure o f
  34 instance pure St where pure x = St \s->Right (x, s)
  35 instance <*> St where (<*>) mfa ma = mfa >>= \fa->ma >>= \a->pure (fa a)
  36 instance Monad St where bind ma a2mb = St $ either Left (\(a,s)->evalSt (a2mb a) s) o evalSt ma
  37
  38 get    = St \s->Right (s, s)
  39 put s  = St \_->Right ((), s)
  40 fail e = St \_->Left e
  41 evalSt (St m) = m
  42 eval m = either Left (Right o fst) (evalSt m [])
  43
  44 instance expr St
  45 where
  46         lit a = pure a
  47         (+.) l r = (+) <$> l <*> r
  48         (-.) l r = (-) <$> l <*> r
  49         (*.) l r = (*) <$> l <*> r
  50         (/.) l r = (/) <$> l <*> r
  51         (==.) l r = (==) <$> l <*> r
  52         If i t e = i >>= \b->if b t e
  53
  54 instance lambda St
  55 where
  56         (@) l r = l >>= \l->l r
  57         \| def = pure \x->fresh >>= \l->putVar l x >>| def (getVar l)
  58
  59 instance let St
  60 where
  61         lett def = fresh >>= \l->
  62                 let (x In y) = def (getVar l)
  63                 in  putVar l x >>| y
  64
  65 fresh = length <$> get
  66 putVar l x = get >>= \s->put [(l, dynamic x):s]
  67 getVar l = get >>= \s->hd [a\\(x, a :: St a^)<-s | x == l]
  68
  69 :: Print a = Print (Int [String] -> [String])
  70 unPrint (Print f) = f
  71 print :: (Print a) -> [String]
  72 print f = unPrint f 0 []
  73 var d i _ c = [d,toString i:c]
  74 instance expr Print
  75 where
  76         lit a = Print \i c->[toString a:c]
  77         (+.) l r = Print \i c->["(":unPrint l i ["+":unPrint r i [")":c]]]
  78         (-.) l r = Print \i c->["(":unPrint l i ["-":unPrint r i [")":c]]]
  79         (*.) l r = Print \i c->["(":unPrint l i ["*":unPrint r i [")":c]]]
  80         (/.) l r = Print \i c->["(":unPrint l i ["/":unPrint r i [")":c]]]
  81         (==.) l r = Print \i c->["(":unPrint l i ["==":unPrint r i [")":c]]]
  82         If p t e = Print \i c->["if ":unPrint p i [" ":unPrint t i [" ":unPrint e i c]]]
  83 instance lambda Print
  84 where
  85         (@) l r = Print \i c->["(":unPrint l i [" ":unPrint r i [")":c]]]
  86         \| def = Print \i c->["(\\":var "x" i i ["->":unPrint (def (Print (var "x" i))) (inc i) [")":c]]]
  87 instance let Print
  88 where
  89         lett def = Print \i c->let (x In y) = def (Print (var "f" i))
  90                 in ["(let ":var "f" i i ["=":unPrint x i ["\nin ":unPrint y (inc i) [")":c]]]]
  91
  92 meval :: (?a) -> ?a
  93 meval a = a
  94 instance expr (?)
  95 where
  96         lit a = pure a
  97         (+.) l r = (+) <$> l <*> r
  98         (-.) l r = (-) <$> l <*> r
  99         (*.) l r = (*) <$> l <*> r
 100         (/.) l r = (/) <$> l <*> r
 101         (==.) l r = (==) <$> l <*> r
 102         If p t e = p >>= \b->if b t e
 103 instance lambda (?)
 104 where
 105         (@) l r = l >>= \l->l r
 106         \| def = pure def
 107 instance let (?)
 108 where
 109         lett def = let (x In y) = def x in y
 110
 111 :: Identity a =: Identity a
 112 runIdentity (Identity a) = a
 113 instance Functor Identity where fmap f a = Identity (f $ runIdentity a)
 114 instance pure Identity where pure a = Identity a
 115 instance <*> Identity where (<*>) mfa a = Identity (runIdentity mfa $ runIdentity a)
 116 instance Monad Identity where bind ma a2mb = a2mb $ runIdentity ma
 117 instance expr Identity
 118 where
 119         lit a = pure a
 120         (+.) l r = (+) <$> l <*> r
 121         (-.) l r = (-) <$> l <*> r
 122         (*.) l r = (*) <$> l <*> r
 123         (/.) l r = (/) <$> l <*> r
 124         (==.) l r = (==) <$> l <*> r
 125         If p t e = p >>= \b->if b t e
 126 instance lambda Identity
 127 where
 128         (@) l r = l >>= \l->l r
 129         \| def = pure def
 130 instance let Identity
 131 where
 132         lett def = let (x In y) = def x in y
 133
 134 Start =
 135         ( "--eval t1: ", eval t1
 136         , "\n--meval t1: ", meval t1
 137         , "\n--ieval t1: ", runIdentity t1
 138         , "\n--print t1:\n", print t1
 139         , "--eval t2: ", eval t2
 140         , "\n--meval t2: ", meval t2
 141         , "\n--ieval t2: ", runIdentity t2
 142         , "\n--print t2:\n", print t2
 143         )
 144
 145 t1 :: (v Int) | let, lambda, expr v & TC (v Int)
 146 t1 =
 147            lett \id     = (\| \x->x)
 148         In lett \fac    = (\| \n->If (n ==. lit 0) (lit 1) (n *. (fac @ n -. lit 1)))
 149         In fac @ id @ lit 10
 150
 151 //Dit wil je niet zelf moeten typen......
 152 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)))
 153 t2 =
 154            lett \id     = (\| \x->x)
 155         In lett \fix    = (\| \f->lett \x=f @ x In x)
 156         In lett \fac    = (\| \n->If (n ==. lit 0) (lit 1) (n *. (fac @ n -. lit 1)))
 157         In lett \facfix = (\| \n->(fix @ \| \fac-> \| \n->If (n ==. lit 0) (lit 1) (n *. (fac @ n -. lit 1))) @ n)
 158         In facfix @ id @ lit 10