diff options
Diffstat (limited to 'lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs')
| -rw-r--r-- | lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs | 22 |
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 |
