lambda/test.icl

   1 module test
   2
   3 import StdEnv
   4 import Data.Functor
   5 import Data.Func
   6 import Data.Maybe
   7 import Control.Applicative
   8 import Control.Monad
   9
  10 :: In a b = In infixl 0 a b
  11 class lambda v
  12 where
  13         (@) infixr 1 :: (v (a -> b)) (v a) -> v b
  14         \| :: ((v a) -> v b) -> v (a -> b) | TC a & TC b
  15
  16 class expr v
  17 where
  18         lit :: a -> v a | toString, TC 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 | * a
  22         (/.) infixl 6 :: (v a) (v a) -> v a | / a
  23         (==.) infix 4 :: (v a) (v a) -> v Bool | == a
  24         If :: (v Bool) (v a) (v a) -> v a
  25
  26 class let v
  27 where
  28         lett :: ((v a) -> In (v a) (v b)) -> v b | TC a
  29
  30 :: Printer a = P ([String] [String] -> [String])
  31 unP (P a) = a
  32 print :: (Printer a) -> [String]
  33 print (P a) = a ["v" +++ toString i\\i<-[0..]] []
  34 instance lambda Printer
  35 where
  36         (@) (P l) (P r) = P \i c->l i [" ":r i c]
  37         \| def = P \[i:is] c->["(\\", i, "->":unP (def (P \_ c->[i:c])) is [")":c]]
  38
  39 instance expr Printer
  40 where
  41         lit a = P \i c->[toString a:c]
  42         (+.) (P l) (P r) = P \i c->["(":l i ["+":r i [")":c]]]
  43         (-.) (P l) (P r) = P \i c->["(":l i ["-":r i [")":c]]]
  44         (*.) (P l) (P r) = P \i c->["(":l i ["*":r i [")":c]]]
  45         (/.) (P l) (P r) = P \i c->["(":l i ["/":r i [")":c]]]
  46         (==.) (P l) (P r) = P \i c->["(":l i ["==":r i [")":c]]]
  47         If (P p) (P t) (P e) = P \i c->["if ":p i [" then ":t i [" else ":e i [" fi":c]]]]
  48
  49 instance let Printer
  50 where
  51         lett def = P \[i:is] c->
  52                 let (x In y) = def $ P \_ c->[i:c]
  53                 in  ["let ",i,"=":(unP x) [i:is] [" in ":(unP y) is c]]
  54
  55 eval :: (Maybe a) -> Maybe a
  56 eval a = a
  57
  58 instance lambda Maybe
  59 where
  60         (@) l r = ($) <$> l <*> r
  61         \| def = Just $ fromJust o def o Just
  62
  63 instance expr Maybe
  64 where
  65         lit a = pure a
  66         (+.) l r = (+) <$> l <*> r
  67         (-.) l r = (-) <$> l <*> r
  68         (*.) l r = (*) <$> l <*> r
  69         (/.) l r = (/) <$> l <*> r
  70         (==.) l r = (==) <$> l <*> r
  71         If i t e = if` <$> i <*> t <*> e
  72
  73 instance let m
  74 where
  75         lett def = let (x In y) = def x in y
  76
  77 :: St a = St (State -> (a, State))
  78 :: State :== [(Int, Dynamic)]
  79 instance Functor St where fmap f m = St $ (\(a, b)->(f a, b)) o evalSt m
  80 instance pure St where pure x = St \s->(x, s)
  81 instance <*> St where (<*>) mfa ma = ap mfa ma
  82 instance Monad St
  83 where
  84         bind ma a2mb = St \s
  85                 # (a, s) = evalSt ma s
  86                 = evalSt (a2mb a) s
  87
  88 get   = St \s->(s, s)
  89 put s = St \_->((), s)
  90 evalSt (St m) = m
  91
  92 instance expr St
  93 where
  94         lit a = pure a
  95         (+.) l r = (+) <$> l <*> r
  96         (-.) l r = (-) <$> l <*> r
  97         (*.) l r = (*) <$> l <*> r
  98         (/.) l r = (/) <$> l <*> r
  99         (==.) l r = (==) <$> l <*> r
 100         If i t e = if` <$> i <*> t <*> e
 101
 102 instance lambda St
 103 where
 104         (@) l r = ($) <$> l <*> r
 105         \| def = get >>= \s->pure \a->fst $ evalSt (def $ pure a) s
 106
 107 instance let St
 108 where
 109         lett def = length <$> get >>= \l->
 110                 let (x In y) = def $ get >>= \s->hd [d\\(x, d :: St a^)<-s | l == x]
 111                 in  get >>= \s->put [(l, dynamic x):s] >>| y
 112
 113 //Start = (print t, "\n", eval t, semSt t)
 114 Start = (print t, "\n", fst $ evalSt t [])
 115 where
 116         t :: (v Int) | expr, lambda, let v
 117         t  = lett \id =(\| \x->x)
 118           In lett \fix =(\| \f->lett \x=f @ x In x)
 119           In lett \fac=(\| \n->If (n ==. lit 0) (lit 1) (n *. (fac @ n -. lit 1)))
 120           In lett \facfix=(\| \n->(fix @ \| \fac-> \| \n->If (n ==. lit 0) (lit 1) (n *. (fac @ n -. lit 1))) @ n)
 121           In facfix @ id @ lit 10