1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
|
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE LambdaCase #-}
module Minilang.Lambda.Eval where
import Data.Aeson (FromJSON, ToJSON)
import Data.String (IsString (..))
import Data.Text (Text, pack)
import GHC.Generics (Generic)
data Term
= Var Text
| Lam Text Term
| App Term Term
deriving (Show, Read, Eq, Generic, ToJSON, FromJSON)
instance IsString Term where
fromString = Var . pack
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 = []
normalise :: Term -> Term
normalise term = readBack (eval [] term)
-- call-by-value evaluator
-- 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 -> VNeut (NVar x)
Lam x body -> Clos env x body
App f a ->
let f' = eval env f
a' = eval env a
in f' `seq` a' `seq` apply f' 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)
freshName :: Text -> [Text] -> Text
freshName x names
| x `elem` names = freshName (x <> "'") names
| otherwise = x
|
