From 99e2ce71faa82e7b99574895e0fe24183ba9f6c3 Mon Sep 17 00:00:00 2001
From: Arnaud Bailly <arnaud@pankzsoft.com>
Date: Wed, 5 Nov 2025 12:02:23 +0100
Subject: can parse whole programs and load them

---
 .../haskell/src/Minilang/Lambda/DeBruijn.hs        | 22 ++++++++++++----------
 1 file changed, 12 insertions(+), 10 deletions(-)

(limited to 'lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs')

diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs b/lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs
index 8b24f8b..de179ad 100644
--- a/lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs
+++ b/lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs
@@ -6,6 +6,7 @@ import Data.List (elemIndex)
 import Data.Text (Text)
 import Minilang.Lambda.Eval (Term)
 import qualified Minilang.Lambda.Eval as Eval
+import Debug.Trace (trace)
 
 data DeBruijn ann
   = FV Text
@@ -19,7 +20,6 @@ type Env ann = [(Text, DeBruijn ann)]
 newEnv :: Env ann
 newEnv = []
 
-
 fromDeBruijn :: DeBruijn Text -> Term
 fromDeBruijn = \case
   FV x -> Eval.Var x
@@ -43,28 +43,30 @@ toDeBruijn term = go term []
 eval :: DeBruijn ann -> DeBruijn ann
 eval (App f a) =
   case eval f of
-    Lam _ body -> eval (substitute 0 a body)
+    Lam _ body -> eval (substitute [] 0 a body)
     f' -> App f' a
 eval term = term
 
-eval' :: Env ann -> DeBruijn ann -> DeBruijn ann
+eval' :: Show ann => Env ann -> DeBruijn ann -> DeBruijn ann
 eval' env (FV v) = case lookup v env of
   Just term -> term
   Nothing -> FV v
 eval' env (App f a) =
   case eval' env f of
-    Lam _ body -> eval' env (substitute 0 a body)
-    f' -> App f' a
+    Lam _ body -> eval' env (substitute env 0 a body)
+    f' -> eval' env $ App f' a
 eval' _ term = term
 
-substitute :: Int -> DeBruijn ann -> DeBruijn ann -> DeBruijn ann
-substitute n arg term = case term of
-  FV x -> FV x
+substitute :: Env ann -> Int -> DeBruijn ann -> DeBruijn ann -> DeBruijn ann
+substitute env n arg term = case term of
+  FV x -> case lookup x env of
+    Just term -> term
+    Nothing -> FV x
   Var t x
     | x == n -> arg
     | otherwise -> Var t x
-  Lam x body -> Lam x (substitute (n + 1) arg body)
-  App f a -> App (substitute n arg f) (substitute n arg a)
+  Lam x body -> Lam x (substitute env (n + 1) arg body)
+  App f a -> App (substitute env n arg f) (substitute env n arg a)
 
 pretty :: DeBruijn Text -> Text
 pretty = \case
-- 
cgit v1.3.1