+module test
+
+import Control.Applicative
+import Control.Monad
+import Data.Func
+import Data.Functor
+import Data.Either
+import Data.Maybe
+import StdEnv
+
+:: In a b = In infixl 0 a b
+class lambda v
+where
+ (@) infixr 1 :: (v ((v a) -> v b)) (v a) -> v b
+ \| :: ((v a) -> v b) -> v ((v a) -> v b) | TC a & TC b & TC (v b)
+
+class expr v
+where
+ lit :: a -> v a | toString a
+ (+.) infixl 6 :: (v a) (v a) -> v a | + a
+ (-.) infixl 6 :: (v a) (v a) -> v a | - a
+ (*.) infixl 6 :: (v a) (v a) -> v a | * a
+ (/.) infixl 6 :: (v a) (v a) -> v a | / a
+ (==.) infix 4 :: (v a) (v a) -> v Bool | == a
+ If :: (v Bool) (v a) (v a) -> v a
+
+class let v
+where
+ lett :: ((v a) -> In (v a) (v b)) -> v b | TC a
+
+:: St a = St (Env -> Either String (a, Env))
+:: Env :== [(Int, Dynamic)]
+instance Functor St where fmap f m = m >>= pure o f
+instance pure St where pure x = St \s->Right (x, s)
+instance <*> St where (<*>) mfa ma = mfa >>= \fa->ma >>= \a->pure (fa a)
+instance Monad St where bind ma a2mb = St $ either Left (\(a,s)->evalSt (a2mb a) s) o evalSt ma
+
+get = St \s->Right (s, s)
+put s = St \_->Right ((), s)
+fail e = St \_->Left e
+evalSt (St m) = m
+eval m = either Left (Right o fst) (evalSt m [])
+
+instance expr St
+where
+ lit a = pure a
+ (+.) l r = (+) <$> l <*> r
+ (-.) l r = (-) <$> l <*> r
+ (*.) l r = (*) <$> l <*> r
+ (/.) l r = (/) <$> l <*> r
+ (==.) l r = (==) <$> l <*> r
+ If i t e = i >>= \b->if b t e
+
+instance lambda St
+where
+ (@) l r = l >>= \l->l r
+ \| def = pure \x->fresh >>= \l->putVar l x >>| def (getVar l)
+
+instance let St
+where
+ lett def = fresh >>= \l->
+ let (x In y) = def (getVar l)
+ in putVar l x >>| y
+
+fresh = length <$> get
+putVar l x = get >>= \s->put [(l, dynamic x):s]
+getVar l = get >>= \s->hd [a\\(x, a :: St a^)<-s | x == l]
+
+:: Print a = Print (Int [String] -> [String])
+unPrint (Print f) = f
+print :: (Print a) -> [String]
+print f = unPrint f 0 []
+var d i _ c = [d,toString i:c]
+instance expr Print
+where
+ lit a = Print \i c->[toString a:c]
+ (+.) l r = Print \i c->["(":unPrint l i ["+":unPrint r i [")":c]]]
+ (-.) l r = Print \i c->["(":unPrint l i ["-":unPrint r i [")":c]]]
+ (*.) l r = Print \i c->["(":unPrint l i ["*":unPrint r i [")":c]]]
+ (/.) l r = Print \i c->["(":unPrint l i ["/":unPrint r i [")":c]]]
+ (==.) l r = Print \i c->["(":unPrint l i ["==":unPrint r i [")":c]]]
+ If p t e = Print \i c->["if ":unPrint p i [" ":unPrint t i [" ":unPrint e i c]]]
+instance lambda Print
+where
+ (@) l r = Print \i c->["(":unPrint l i [" ":unPrint r i [")":c]]]
+ \| def = Print \i c->["(\\":var "x" i i ["->":unPrint (def (Print (var "x" i))) (inc i) [")":c]]]
+instance let Print
+where
+ lett def = Print \i c->let (x In y) = def (Print (var "f" i))
+ in ["(let ":var "f" i i ["=":unPrint x i ["\nin ":unPrint y (inc i) [")":c]]]]
+
+meval :: (?a) -> ?a
+meval a = a
+instance expr (?)
+where
+ lit a = pure a
+ (+.) l r = (+) <$> l <*> r
+ (-.) l r = (-) <$> l <*> r
+ (*.) l r = (*) <$> l <*> r
+ (/.) l r = (/) <$> l <*> r
+ (==.) l r = (==) <$> l <*> r
+ If p t e = p >>= \b->if b t e
+instance lambda (?)
+where
+ (@) l r = l >>= \l->l r
+ \| def = pure def
+instance let (?)
+where
+ lett def = let (x In y) = def x in y
+
+:: Identity a =: Identity a
+runIdentity (Identity a) = a
+instance Functor Identity where fmap f a = Identity (f $ runIdentity a)
+instance pure Identity where pure a = Identity a
+instance <*> Identity where (<*>) mfa a = Identity (runIdentity mfa $ runIdentity a)
+instance Monad Identity where bind ma a2mb = a2mb $ runIdentity ma
+instance expr Identity
+where
+ lit a = pure a
+ (+.) l r = (+) <$> l <*> r
+ (-.) l r = (-) <$> l <*> r
+ (*.) l r = (*) <$> l <*> r
+ (/.) l r = (/) <$> l <*> r
+ (==.) l r = (==) <$> l <*> r
+ If p t e = p >>= \b->if b t e
+instance lambda Identity
+where
+ (@) l r = l >>= \l->l r
+ \| def = pure def
+instance let Identity
+where
+ lett def = let (x In y) = def x in y
+
+Start =
+ ( "--eval t1: ", eval t1
+ , "\n--meval t1: ", meval t1
+ , "\n--ieval t1: ", runIdentity t1
+ , "\n--print t1:\n", print t1
+ , "--eval t2: ", eval t2
+ , "\n--meval t2: ", meval t2
+ , "\n--ieval t2: ", runIdentity t2
+ , "\n--print t2:\n", print t2
+ )
+
+t1 :: (v Int) | let, lambda, expr v & TC (v Int)
+t1 =
+ lett \id = (\| \x->x)
+ In lett \fac = (\| \n->If (n ==. lit 0) (lit 1) (n *. (fac @ n -. lit 1)))
+ In fac @ id @ lit 10
+
+//Dit wil je niet zelf moeten typen......
+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)))
+t2 =
+ lett \id = (\| \x->x)
+ In lett \fix = (\| \f->lett \x=f @ x In x)
+ In lett \fac = (\| \n->If (n ==. lit 0) (lit 1) (n *. (fac @ n -. lit 1)))
+ In lett \facfix = (\| \n->(fix @ \| \fac-> \| \n->If (n ==. lit 0) (lit 1) (n *. (fac @ n -. lit 1))) @ n)
+ In facfix @ id @ lit 10