Add call-by-name lambda calculus example

This commit is contained in:
Martin Fredin 2023-05-15 00:32:53 +02:00
parent 36df452db5
commit 0659386ae7

View file

@ -0,0 +1,53 @@
data List a where
Nil : List a
Cons : a -> List a -> List a
data Pair a b where
Pair : a -> b -> Pair a b
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
-- FIXME segmentation fault när man löser f istället för 1000
VClosure delta x f => eval delta (EInt 1000)
-- 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' (EInt 40)) (EInt 20)
main : Int
main = case eval Nil exp of
VInt i => i