draft env-based normaliser

1 files changed, 44 insertions, 4 deletions

diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs b/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs
index 7f7aad7..9d56c49 100644
--- a/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs
+++ b/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE LambdaCase #-}
 
 module Minilang.Lambda.Eval where
 
@@ -12,14 +13,53 @@ data Term
   | App Term Term
   deriving (Show, Read, Eq, Generic, ToJSON, FromJSON)
 
+data Value = Clos EnvValue Text Term | VNeut Neutral
+  deriving (Show, Read, Eq)
+
+data Neutral = NVar Text | NApp Neutral Value
+  deriving (Show, Read, Eq)
+
 type Env = [(Text, Term)]
 
+type EnvValue = [(Text, Value)]
+
 newEnv :: Env
 newEnv = []
 
 -- call-by-value evaluator
-eval :: Term -> Env -> Term
-eval = undefined
+-- from https://davidchristiansen.dk/tutorials/nbe/#%28part._untyped-eval%29
+eval :: EnvValue -> Term -> Value
+eval env = \case
+  Var x -> case lookup x env of
+    Just term -> term
+    Nothing -> error $ "Unbound variable: " ++ show x
+  Lam x body -> Clos env x body
+  App f a -> apply (eval env f) (eval env a)
+
+apply :: Value -> Value -> Value
+apply f a =
+  case f of
+    Clos closureEnv x body ->
+      let env' = (x, a) : closureEnv
+       in eval env' body
+    VNeut f' -> VNeut (NApp f' a)
+
+readBack :: Value -> Term
+readBack = go []
+  where
+    go names = \case
+      Clos env x body ->
+        let name = freshName x names
+            names' = name : names
+            val' = eval ((x, VNeut (NVar name)) : env) body
+         in Lam name (go names' val')
+      VNeut (NVar n) -> Var n
+      VNeut (NApp f a) -> App (go names (VNeut f)) (go names a)
+
+normalise :: Term -> Term
+normalise term = readBack (eval [] term)
 
-evalNeed :: Term -> Env -> Term
-evalNeed = undefined
+freshName :: Text -> [Text] -> Text
+freshName x names
+  | x `elem` names = freshName (x <> "'") names
+  | otherwise = x