wip: use de Bruijn indices representation

provide sample complex terms to evaluate

4 files changed, 86 insertions, 15 deletions

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