wip: use de Bruijn indices representation

provide sample complex terms to evaluate

8 files changed, 155 insertions, 15 deletions

diff --git a/lambda-calcul/haskell/bool.lisp b/lambda-calcul/haskell/bool.lisp
new file mode 100644
index 0000000..250c38a
--- /dev/null
+++ b/lambda-calcul/haskell/bool.lisp
@@ -0,0 +1,10 @@
+(let ((False (lam (f t) f))
+      (True (lam (f t) t))
+      (If (lam (b x y) (b x y)))
+      (Zero (lam (z s) z))
+      (Succ (lam (n z s) (s n)))
+      (One (Succ Zero))
+      (Two (Succ One))
+      (Three (Succ Two))
+      (IsZero (lam (n) (n True (lam (m) False)))))
+  (IsZero Two))
diff --git a/lambda-calcul/haskell/fac.lisp b/lambda-calcul/haskell/fac.lisp
new file mode 100644
index 0000000..549334b
--- /dev/null
+++ b/lambda-calcul/haskell/fac.lisp
@@ -0,0 +1,39 @@
+(let ((False (lam (f t) f))
+      (True (lam (f t) t))
+      (If (lam (b x y) (b x y)))
+      (Zero (lam (z s) z))
+      (Succ (lam (n z s) (s n)))
+      (One (Succ Zero))
+      (Two (Succ One))
+      (Three (Succ Two))
+      (IsZero (lam (n) (n True (lam (m) False))))
+      (const (lam (x y) x))
+      (Pair (lam (a b p) (p a b)))
+      (fst (lam (pair) (pair (lam (a b) a))))
+      (snd (lam (pair) (pair (lam (a b) b))))
+      (fix (lam (f)
+             ((lam (x) (f (x x)))
+              (lam (x) (f (x x))))))
+      (add (fix (lam (radd x y)
+                     (x y (lam (n) (Succ (radd n y)))))))
+      (mul (fix (lam (rmul x y)
+                     (x Zero (lam (n) (add y (rmul n y)))))))
+      (fac (fix (lam (rfac x)
+                 (x
+                     One
+                     (lam (n) (mul x (rfac n)))))))
+      (eqnat (fix (lam (reqnat x y)
+                       (x (y True (const False))
+                          (lam (x1) (y False (lam (y1) (reqnat x1 y1))))))))
+      (sumto (fix (lam (rsumto n)
+                     (n Zero
+                        (lam (m) (add n (rsumto m)))))))
+      (n5 (add Two Three))
+      (n6 (mul Two Three))
+      (n17 (add n6 (add n6 n5)))
+      (n37 (Succ (mul n6 n6)))
+      (n703 (sumto n37))
+      (n704 (Succ (sumto n37)))
+      (n720 (fac n6))
+      )
+  (eqnat n720 (add n704 n17)))
diff --git a/lambda-calcul/haskell/minilang.cabal b/lambda-calcul/haskell/minilang.cabal
index a39c466..a2bb355 100644
--- a/lambda-calcul/haskell/minilang.cabal
+++ b/lambda-calcul/haskell/minilang.cabal
@@ -27,6 +27,7 @@ library
   exposed-modules:
       Minilang.IO
       Minilang.Lambda.Unify
+      Minilang.Lambda.DeBruijn
       Minilang.Lambda.Eval
       Minilang.Lambda.Infer
       Minilang.Lambda.Parser
@@ -65,6 +66,7 @@ test-suite minilang-test
   other-modules:
       Minilang.IOSpec
       Minilang.Lambda.InferSpec
+      Minilang.Lambda.DeBruijnSpec
       Minilang.Lambda.EvalSpec
       Minilang.Lambda.ParserSpec
   hs-source-dirs:
diff --git a/lambda-calcul/haskell/src/Minilang/IO.hs b/lambda-calcul/haskell/src/Minilang/IO.hs
index 28b6f01..a045647 100644
--- a/lambda-calcul/haskell/src/Minilang/IO.hs
+++ b/lambda-calcul/haskell/src/Minilang/IO.hs
@@ -7,9 +7,9 @@ import Data.Text.Encoding
     encodeUtf8,
   )
 import Data.Text.Encoding.Error (lenientDecode)
-import Minilang.Lambda.Eval (eval)
+import Minilang.Lambda.DeBruijn (eval, toDeBruijn)
+import Minilang.Lambda.Parser (desugar, parse, pretty)
 import System.IO (Handle)
-import Minilang.Lambda.Parser (parse, desugar)
 
 -- | Read a "program" from @hin@ handle, evaluate it and dump the result
 -- on @hout@.
@@ -17,13 +17,11 @@ runEval :: Handle -> Handle -> IO ()
 runEval hin hout = do
   programText <- decodeUtf8With lenientDecode <$> BS.hGetContents hin
   let parsed = parse programText
-      result = case parsed of
-         Left err -> show err
-         Right ast ->
-           let term = desugar ast
-               env = mempty
-           in show $ eval term env
-
-  BS.hPut
-    hout
-    (encodeUtf8 (Text.pack result <> "\n"))
+  case parsed of
+    Left err -> print err
+    Right ast -> do
+      putStrLn $ Text.unpack $ "Evaluating " <> pretty ast
+      let termy = desugar ast
+      putStrLn $ "Desugared to " <> show termy
+      let term = toDeBruijn termy
+      print $ eval term
diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs b/lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs
new file mode 100644
index 0000000..6b5b7a2
--- /dev/null
+++ b/lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs
@@ -0,0 +1,42 @@
+module Minilang.Lambda.DeBruijn where
+
+import Data.List (elemIndex)
+import Data.Text (Text)
+import Minilang.Lambda.Eval (Term)
+import qualified Minilang.Lambda.Eval as Eval
+
+data DeBruijn
+  = FV Text
+  | Var Int
+  | Lam DeBruijn
+  | App DeBruijn DeBruijn
+  deriving (Show, Read, Eq)
+
+-- Convert a term with named variables to De Bruijn indices
+toDeBruijn :: Term -> DeBruijn
+toDeBruijn term = go term []
+  where
+    go (Eval.Var x) env =
+      case elemIndex x env of
+        Just idx -> Var idx
+        Nothing -> FV x
+    go (Eval.Lam x body) env =
+      Lam (go body (x : env))
+    go (Eval.App f a) env =
+      App (go f env) (go a env)
+
+eval :: DeBruijn -> DeBruijn
+eval (App f a) =
+  case eval f of
+    Lam body -> eval (substitute 0 a body)
+    f' -> App f' a
+eval term = term
+
+substitute :: Int -> DeBruijn -> DeBruijn -> DeBruijn
+substitute n arg term = case term of
+  FV x -> FV x
+  Var x
+    | x == n -> arg
+    | otherwise -> Var x
+  Lam body -> Lam (substitute (n + 1) arg body)
+  App f a -> App (substitute n arg f) (substitute n arg a)
diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs b/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs
index cbbdc51..35f9460 100644
--- a/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs
+++ b/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs
@@ -42,3 +42,32 @@ evalNeed (App f a) env =
    in case evalNeed f env of
         Abs x body env' -> evalNeed body ((x, a') : env')
         f' -> Ap f' a'
+
+x =
+  App
+    ( App
+        ( App
+            ( App
+                ( App
+                    ( App
+                        ( App
+                            ( App
+                                ( App
+                                    (Lam "False" (Lam "True" (Lam "If" (Lam "Zero" (Lam "Succ" (Lam "One" (Lam "Two" (Lam "Three" (Lam "IsZero" (App (Var "IsZero") (Var "Two")))))))))))
+                                    (Lam "f" (Lam "t" (Var "f")))
+                                )
+                                (Lam "f" (Lam "t" (Var "t")))
+                            )
+                            (Lam "b" (Lam "x" (Lam "y" (App (App (Var "b") (Var "x")) (Var "y")))))
+                        )
+                        (Lam "z" (Lam "s" (Var "z")))
+                    )
+                    (Lam "n" (Lam "z" (Lam "s" (App (Var "s") (Var "n")))))
+                )
+                (App (Var "Succ") (Var "Zero"))
+            )
+            (App (Var "Succ") (Var "One"))
+        )
+        (App (Var "Succ") (Var "Two"))
+    )
+    (Lam "n" (App (App (Var "n") (Var "True")) (Lam "m" (Var "False"))))
diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/Parser.hs b/lambda-calcul/haskell/src/Minilang/Lambda/Parser.hs
index 9ed4626..e52c981 100644
--- a/lambda-calcul/haskell/src/Minilang/Lambda/Parser.hs
+++ b/lambda-calcul/haskell/src/Minilang/Lambda/Parser.hs
@@ -75,16 +75,18 @@ letExpr =
     rpar
     ( do
         void $ lexeme "let"
-        (bind : binds) <-
+        bindings <-
           between
             lpar
             rpar
             (some binding)
         body <- ast
-        let fun = Abs (fst <$> (bind : binds)) body
-        return $ App fun (snd bind) (snd <$> binds)
+        return $ foldr mkLet body bindings
     )
 
+mkLet :: (Text, AST) -> AST -> AST
+mkLet (var, bound) body = App (Abs [var] body) bound []
+
 binding :: Parser (Text, AST)
 binding =
   between
diff --git a/lambda-calcul/haskell/test/Minilang/Lambda/DeBruijnSpec.hs b/lambda-calcul/haskell/test/Minilang/Lambda/DeBruijnSpec.hs
new file mode 100644
index 0000000..ef8903c
--- /dev/null
+++ b/lambda-calcul/haskell/test/Minilang/Lambda/DeBruijnSpec.hs
@@ -0,0 +1,18 @@
+module Minilang.Lambda.DeBruijnSpec where
+
+import Minilang.Lambda.DeBruijn (DeBruijn (..), eval, toDeBruijn)
+import qualified Minilang.Lambda.Eval as Eval
+import Test.Hspec (Spec, it, shouldBe)
+
+spec :: Spec
+spec = do
+  it "convert term to deBruijn representation" $ do
+    let term = Eval.Lam "x" (Eval.Lam "y" (Eval.Var "x"))
+        deBruijn = toDeBruijn term
+
+    deBruijn `shouldBe` Lam (Lam (Var 1))
+
+  it "evaluates deBruijn term" $ do
+    let term = App (App (Lam (Lam (Var 1))) (Var 12)) (Var 34)
+
+    eval term `shouldBe` Var 12