diff --git a/sample-programs/lambda_calculus-2.crf b/sample-programs/lambda_calculus-2.crf new file mode 100644 index 0000000..acf7885 --- /dev/null +++ b/sample-programs/lambda_calculus-2.crf @@ -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 +