wip: use de Bruijn indices representation

provide sample complex terms to evaluate

1 files changed, 42 insertions, 0 deletions

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)