churf/sample-programs/working/lambda_calculus-2.crf
Martin Fredin 06259e8abf Move file
2023-05-15 17:28:42 +02:00

44 lines
1.3 KiB
Text

data Exp where
EVar : Char -> Exp
EAbs : Char -> Exp -> Exp
EApp : Exp -> Exp -> Exp
EInt : Int -> Exp
EAdd : Exp -> Exp -> Exp
data Val where
VInt : Int -> Val
VClosure : List (Pair Char Val) -> Char -> Exp -> Val
lookup : Char -> List (Pair Char Val) -> Val
lookup x cxt = case cxt of
Cons p ps => case p of
Pair y v => case (asciiCode x) == (asciiCode y) of
True => v
False => lookup x ps
insert : Char -> Val -> List (Pair Char Val) -> List (Pair Char Val)
insert x v cxt = Cons (Pair x v) cxt
eval : List (Pair Char Val) -> Exp -> Val
eval cxt exp = case exp of
EVar x => case lookup x cxt of
VInt i => VInt i
VClosure delta x e => eval delta e
EAbs x e => VClosure cxt x e
EApp e1 e2 => case eval cxt e1 of
VClosure delta x f =>
let v = VClosure cxt x e2 in
eval (insert x v delta) f
EInt i => VInt i
EAdd e1 e2 =>
let i1 = case eval cxt e1 of { VInt i => i } in
let i2 = case eval cxt e2 of { VInt i => i } in
VInt (i1 + i2)
exp = EApp (EAbs 'x' (EVar 'x')) (EApp (EAbs 'x' (EAdd (EVar 'x') (EInt 100))) (EInt 200))
-- (λ x . x) (λ x . x + 100) 200
main : Int
main = case eval Nil exp of
VInt i => i