churf/sample-programs/lambda_calculus-2.crf
2023-05-15 13:45:50 +02:00

50 lines
1.4 KiB
Text

-- data List a where
-- Nil : List a
-- Cons : a -> List a -> List a
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 f
-- 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