summaryrefslogtreecommitdiff
path: root/lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs
diff options
context:
space:
mode:
authorArnaud Bailly <arnaud@pankzsoft.com>2025-11-05 12:02:23 +0100
committerArnaud Bailly <arnaud@pankzsoft.com>2025-11-05 12:02:23 +0100
commit99e2ce71faa82e7b99574895e0fe24183ba9f6c3 (patch)
tree10538bb91d187a3c1d281a87a3974a6036f2ad2f /lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs
parent438e3f8c5dcdfeead15a6a9a1760f7c254fc54b2 (diff)
downloadlambda-nantes-99e2ce71faa82e7b99574895e0fe24183ba9f6c3.tar.gz
can parse whole programs and load them
Diffstat (limited to 'lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs')
-rw-r--r--lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs22
1 files changed, 12 insertions, 10 deletions
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