From: Mart Lubbers <mart@martlubbers.net>
Date: Mon, 8 Jun 2020 06:09:50 +0000 (+0200)
Subject: lambda
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=ae0e2cb316d4d51cef959a29220040784406c120;p=clean-tests.git

lambda
---

diff --git a/lambda/test.icl b/lambda/test.icl
index 2dfb06f..0841159 100644
--- a/lambda/test.icl
+++ b/lambda/test.icl
@@ -11,11 +11,11 @@ import Control.Monad
 class lambda v
 where
 	(@) infixr 1 :: (v (a -> b)) (v a) -> v b
-	\| :: ((v a) -> v b) -> v (a -> b)
+	\| :: ((v a) -> v b) -> v (a -> b) | TC a & TC b
 
 class expr v
 where
-	lit :: a -> v a | toString a
+	lit :: a -> v a | toString, TC 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
@@ -25,7 +25,7 @@ where
 
 class let v
 where
-	lett :: ((v a) -> In (v a) (v b)) -> v b
+	lett :: ((v a) -> In (v a) (v b)) -> v b | TC a
 
 :: Printer a = P ([String] [String] -> [String])
 unP (P a) = a
@@ -58,7 +58,7 @@ eval a = a
 instance lambda Maybe
 where
 	(@) l r = ($) <$> l <*> r
-	\| def = Just (\a->fromJust (def (Just a)))
+	\| def = Just $ fromJust o def o Just
 
 instance expr Maybe
 where
@@ -70,13 +70,52 @@ where
 	(==.) l r = (==) <$> l <*> r
 	If i t e = if` <$> i <*> t <*> e
 
-instance let Maybe
+instance let m
 where
 	lett def = let (x In y) = def x in y
 
-Start = (print t, "\n", eval t)
+:: St a = St (State -> (a, State))
+:: State :== [(Int, Dynamic)]
+instance Functor St where fmap f m = St $ (\(a, b)->(f a, b)) o evalSt m
+instance pure St where pure x = St \s->(x, s)
+instance <*> St where (<*>) mfa ma = ap mfa ma
+instance Monad St
+where
+	bind ma a2mb = St \s
+		# (a, s) = evalSt ma s
+		= evalSt (a2mb a) s
+
+get   = St \s->(s, s)
+put s = St \_->((), s)
+evalSt (St m) = 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 = if` <$> i <*> t <*> e
+
+instance lambda St
+where
+	(@) l r = ($) <$> l <*> r
+	\| def = get >>= \s->pure \a->fst $ evalSt (def $ pure a) s
+
+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
+
+//Start = (print t, "\n", eval t, semSt t)
+Start = (print t, "\n", fst $ evalSt t [])
 where
 	t :: (v Int) | expr, lambda, let v
 	t  = 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 fac @ lit 10
+	  In lett \facfix=(\| \n->(fix @ \| \fac-> \| \n->If (n ==. lit 0) (lit 1) (n *. (fac @ n -. lit 1))) @ n)
+	  In facfix @ id @ lit 10