churf/sample-programs/lambda_calculus.crf

53 lines
1.5 KiB
Text

data Exp where
EVar : Char -> Exp
EInt : Int -> Exp
EAbs : Char -> Exp -> Exp
EApp : Exp -> Exp -> Exp
EAdd : Exp -> Exp -> Exp
data Env where
Env : List (Pair Char Context) -> Env
data Context where
VInt : Int -> Context
VClos : Env -> Char -> Exp -> Context
lookupVar : Char -> Env -> Context
lookupVar ident1 env = case env of
Env list => case list of
Cons a as => case a of
Pair ident2 val => case (asciiCode ident1) == (asciiCode ident2) of
True => val
False => lookupVar ident1 (Env as)
insert : Char -> Context -> Env -> Env
insert ident v env = case env of
Env list => Env (Cons (Pair ident v) list)
interp : Env -> Exp -> Context
interp env exp = case exp of
EInt i => VInt i
EAdd e1 e2 => case interp env e1 of
VInt i => case interp env e2 of
VInt j => VInt (i + j)
EAbs ident expr => VClos env ident expr
EApp e1 e2 => case interp env e1 of
VClos closEnv ident exp => case interp env e2 of
v => interp (insert ident v closEnv) exp
EVar v => lookupVar v env
eval : Context -> Int
eval v = case v of
VInt i => i
_ => const (0 - 1) (printStr "Fail: final value is not an integer\n")
expression : Exp
expression = EApp (EAbs 'x' (EVar 'x')) (EApp (EAbs 'x' (EAdd (EVar 'x') (EInt 100))) (EInt 200))
-- (λ x . x) (λ x . x + 100) 200
context : Env
context = Env Nil
main : Int
main = eval (interp context expression)