From 62651f13e08304d8fa6395fde7352984f48adb46 Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Wed, 5 Nov 2025 09:09:53 +0100 Subject: evaluate deBruijn terms in environment --- lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) (limited to 'lambda-calcul/haskell/src') diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs b/lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs index 290839e..8b24f8b 100644 --- a/lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs +++ b/lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs @@ -1,8 +1,9 @@ {-# LANGUAGE LambdaCase #-} + module Minilang.Lambda.DeBruijn where import Data.List (elemIndex) -import Data.Text (Text, unpack, pack) +import Data.Text (Text) import Minilang.Lambda.Eval (Term) import qualified Minilang.Lambda.Eval as Eval @@ -13,6 +14,12 @@ data DeBruijn ann | App (DeBruijn ann) (DeBruijn ann) deriving (Show, Read, Eq) +type Env ann = [(Text, DeBruijn ann)] + +newEnv :: Env ann +newEnv = [] + + fromDeBruijn :: DeBruijn Text -> Term fromDeBruijn = \case FV x -> Eval.Var x @@ -40,6 +47,16 @@ eval (App f a) = f' -> App f' a eval term = term +eval' :: 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 +eval' _ term = term + substitute :: Int -> DeBruijn ann -> DeBruijn ann -> DeBruijn ann substitute n arg term = case term of FV x -> FV x -- cgit v1.3.1