.

[clean-tests.git] / lambda / test2.icl

diff --git a/lambda/test2.icl b/lambda/test2.icl
new file mode 100644 (file)
index 0000000..e0d64bb
--- /dev/null
+++ b/lambda/test2.icl
@@ -0,0 +1,130 @@
+module test2
+
+import Control.Applicative
+import Control.Monad
+import Data.Functor
+import Data.Either
+import Data.Maybe
+import StdEnv
+
+:: In a b = In infixl 0 a b
+class lambda v w
+where
+       \| :: ((v a) -> w) -> ((v a) -> w)
+
+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 | /, zero, == a
+       (==.) infix 4 :: (v a) (v a) -> v Bool | == a
+       If :: (v Bool) (v a) (v a) -> v a
+
+class let v w
+where
+       lett :: (w -> In w (v b)) -> v b
+
+:: 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 (Print a)
+where
+       \| :: ((Print a) -> Print b) -> ((Print a) -> Print b)
+       \| def = \arg->Print \i c->["(\\":var "x" i i ["->":unPrint (def (Print (var "x" i))) (inc i) [") ":unPrint arg i c]]]
+//NB: Dit moet ook te doen zijn vrees ik maar het lukt mij zo gauw niet
+//instance lambda Print ((Print a) -> b) | lambda Print (Print b)
+//where
+//     \| def = \arg arg0->Print \i c->["(\\":var "x" i i ["->":unPrint ((\| def (Print (var "x" i))) arg0) (inc i) [") ":unPrint arg i c]]]
+instance lambda Print ((Print a) -> Print b)
+where
+       \| :: ((Print a) (Print b) -> Print c) -> ((Print a) (Print b) -> Print c)
+       \| 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]]]]
+instance lambda Print ((Print a) (Print b) -> Print c)
+where
+       \| :: ((Print a) (Print b) (Print c) -> Print d) -> ((Print a) (Print b) (Print c) -> Print d)
+       \| 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]]]]]
+instance let Print (Print a)
+where
+       lett def = Print \i c->let (x In y) = def (Print (var "v" i))
+               in ["(let ":var "v" i i ["=":unPrint x i ["\nin ":unPrint y (inc i) [")":c]]]]
+//NB: dit dan misschien ook wel
+//instance let Print ((Print a) -> b) | let Print b
+//where
+//     lett def = 
+instance let Print ((Print a) -> Print b)
+where
+       lett def = Print \i c->let (x In y) = def (\a->Print \_ c->["(":var "v" i i [" ":unPrint a i [")":c]]])
+               in ["(let ":var "v" i i ["=":unPrint (x (Print \_ c->c)) i ["\nin ":unPrint y (inc i) [")":c]]]]
+instance let Print ((Print a) (Print b) -> Print c)
+where
+       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]]]])
+               in ["(let ":var "v" i i ["=":unPrint (x (Print \_ c->c) (Print \_ c->c)) 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 >>= \l->r >>= \r->if (r == zero) ?None (pure (l/r))
+       (==.) l r = (==) <$> l <*> r
+       If p t e = p >>= \b->if b t e
+instance lambda (?) a
+where
+       \| def = def
+instance let (?) a
+where
+       lett def = let (x In y) = def x in y
+
+Start =
+//     ( "--eval t1: ", eval t1
+       ( "\n--meval t0: ", meval t0
+       , "\n--print t0:\n", print t0
+       , "\n--meval t1: ", meval t1
+       , "\n--print t1:\n", print t1
+       , "\n--meval t2: ", meval t2
+       , "\n--print t2:\n", print t2
+       , "\n--meval t3: ", meval t3
+       , "\n--print t3:\n", print t3
+       )
+//     , "--eval t2: ", eval t2
+//     , "\n--meval t2: ", meval t2
+//     , "\n--ieval t2: ", runIdentity t2
+//     , "\n--print t2:\n", print t2
+//     )
+//t0 :: v Int | let v ((v Int) -> v Int) & lambda v (v Int) & expr v
+t0 = lett \id = (\| \x->x)
+       In id (lit 42)
+//t1 :: v Int | let v ((v Int) -> v Int) & lambda v (v Int) & expr v
+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))
+//t2 :: v Int | let v ((v Int) (v Int) -> v Int) & lambda v (v Int) & lambda v ((v Int) -> v Int) & expr v
+t2 = (\| \x-> (\| \y->x +. y)) (lit 11) (lit 31)
+
+t3 = (\| \x-> (\| \y-> (\| \z->x +. y +. z))) (lit 11) (lit 15) (lit 16)
+//
+////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))