diff options
| author | Arnaud Bailly <arnaud@pankzsoft.com> | 2025-11-05 09:09:53 +0100 |
|---|---|---|
| committer | Arnaud Bailly <arnaud@pankzsoft.com> | 2025-11-05 09:09:53 +0100 |
| commit | 62651f13e08304d8fa6395fde7352984f48adb46 (patch) | |
| tree | c6b4045e154bef30170c4ce5a7be430e453a1bf4 /lambda-calcul/haskell/src | |
| parent | 246d370bd903edeb5570b6f016556528b8ca57fc (diff) | |
| download | lambda-nantes-62651f13e08304d8fa6395fde7352984f48adb46.tar.gz | |
evaluate deBruijn terms in environment
Diffstat (limited to 'lambda-calcul/haskell/src')
| -rw-r--r-- | lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs | 19 |
1 files changed, 18 insertions, 1 deletions
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 |
