From 04ab328e138b21090401ae2fa32737f59439317f Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Wed, 25 Nov 2020 16:28:42 +0100 Subject: [PATCH] . --- lambda/bug.icl | 138 ++++++++++++++++++++++++----------------- lambda/test.icl | 158 +++++++++++++++++++++++++++++++++++++++++++++++ lambda/test2.icl | 130 ++++++++++++++++++++++++++++++++++++++ 3 files changed, 368 insertions(+), 58 deletions(-) create mode 100644 lambda/test.icl create mode 100644 lambda/test2.icl 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] -[line:65];38;90 [module: bug] -[line:39];27;103 [module: bug] -evalSt [module: bug] -[line:39];23;11 [module: bug] -evalSt [module: bug] -[line:39];23;11 [module: bug] -evalSt [module: bug] -evalSt [module: bug] -[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] -[line:65];38;101 [module: bug] -[line:39];27;135 [module: bug] -evalSt [module: bug] -[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)) -- 2.20.1