From: Mart Lubbers <mart@martlubbers.net>
Date: Wed, 25 Nov 2020 15:28:42 +0000 (+0100)
Subject: .
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=04ab328e138b21090401ae2fa32737f59439317f;p=clean-tests.git

.
---

diff --git a/lambda/bug.icl b/lambda/bug.icl
index 91cbeb9..cfa46ec 100644
--- a/lambda/bug.icl
+++ b/lambda/bug.icl
@@ -1,11 +1,26 @@
-module bug
+module test
 
 import StdEnv
-import Data.Functor
-import Data.Func
-import Data.Maybe
-import Control.Applicative
-import Control.Monad
+
+:: Either l r = Left l | Right r
+either f _ (Left x) = f x
+either _ f (Right x) = f x
+class Functor m
+where
+	fmap :: (a -> b) (m a) -> m b
+	(<$>) infixl 4 :: (a -> b) (m a) -> m b
+	(<$>) a b = fmap a b
+class Applicative m
+where
+	pure :: a -> m a
+	(<*>) infixl 4 :: (m (a -> b)) (m a) -> m b
+class Monad m
+where
+	bind :: (m a) (a -> m b) -> m b
+	(>>=) infixl 1 :: (m a) (a -> m b) -> m b
+	(>>=) a b = bind a b
+	(>>|) infixl 1 :: (m a) (m b) -> m b
+	(>>|) a b = bind a \_->b
 
 :: In a b = In infixl 0 a b
 class lambda v
@@ -15,7 +30,7 @@ where
 
 class expr v
 where
-	lit :: a -> v a | toString, TC a
+	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
@@ -27,13 +42,13 @@ class let v
 where
 	lett :: ((v a) -> In (v a) (v b)) -> v b | TC a
 
-import Data.Either
-import Data.Tuple
 :: St a = St (Env -> Either String (a, Env))
-:: Env :== [(Int, Dynamic)]
-instance Functor St where fmap f m = St $ fmap (appFst f) o evalSt m
-instance pure St where pure x = St \s->Right (x, s)
-instance <*> St where (<*>) mfa ma = ap mfa ma
+:: Env :== [Dynamic]
+instance Functor St where fmap f m = m >>= \a->pure (f a)
+instance Applicative St
+where
+	pure x = St \s->Right (x, s)
+	(<*>) mfa ma = mfa >>= \fa->ma >>= \a->pure (fa a)
 instance Monad St
 where
 	bind ma a2mb = St \s->case evalSt ma s of
@@ -42,7 +57,9 @@ where
 
 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
@@ -52,58 +69,63 @@ where
 	(*.) l r = (*) <$> l <*> r
 	(/.) l r = (/) <$> l <*> r
 	(==.) l r = (==) <$> l <*> r
-	If i t e = if` <$> i <*> t <*> e
+	If i t e = i >>= \b->if b t e
 
 instance lambda St
 where
 	(@) l r = l >>= \l->r >>= \r->l r
-	\| def = pure $ def o pure
+	\| def = pure (def o pure)
 
 instance let St
 where
 	lett def = length <$> get >>= \l->
-		let (x In y) = def $ get >>= \s->hd [d\\(x, d :: St a^)<-s | l == x]
-		in  get >>= \s->put [(l, dynamic x):s] >>| y
+		let (x In y) = def (get >>= deref o flip (!!) l)
+		in  get >>= \s->put (s ++ [dynamic x]) >>| y
+
+deref a = abort (toString (typeCodeOfDynamic a))
+deref (a :: a^) = a
+deref _ = fail "Variable not known???"
 
-Start = evalSt t2 []
+:: 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
-// Geeft:
-/*
-initial_unification_environment [module: _SystemDynamic]
-_initial_unification_environment [module: _SystemDynamic]
-_f111;111 [module: bug]
-<lambda>[line:65];38;90 [module: bug]
-<case>[line:39];27;103 [module: bug]
-evalSt [module: bug]
-<lambda>[line:39];23;11 [module: bug]
-evalSt [module: bug]
-<lambda>[line:39];23;11 [module: bug]
-evalSt [module: bug]
-evalSt [module: bug]
-<lambda>[line:39];23;11 [module: bug]
-*/
-	t1  = 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 fac @ id @ lit 10
-// Geeft:
-/*
-unify_ [module: _SystemDynamic]
-unify_ [module: _SystemDynamic]
-unify_ [module: _SystemDynamic]
-unify_types [module: _SystemDynamic]
-_unify [module: _SystemDynamic]
-_f143;143 [module: bug]
-<lambda>[line:65];38;101 [module: bug]
-<case>[line:39];27;135 [module: bug]
-evalSt [module: bug]
-<lambda>[line:39];23;22 [module: bug]
-evalSt [module: bug]
-evalSt [module: bug]
-*/
-	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
+	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]]]]
+
+Start =
+	( "--eval t1: ", eval t1
+	, "\n--print t1:\n", print t1
+	, "--eval t2: ", eval t2
+	, "\n--pritn 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
+
+t2 :: (v Int) | let, lambda, expr v & TC (v Int) & TC (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
diff --git a/lambda/test.icl b/lambda/test.icl
new file mode 100644
index 0000000..0b05327
--- /dev/null
+++ b/lambda/test.icl
@@ -0,0 +1,158 @@
+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
diff --git a/lambda/test2.icl b/lambda/test2.icl
new file mode 100644
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))