Skip to content

Instantly share code, notes, and snippets.

@ikr7 ikr7/tlc.v
Last active Nov 30, 2018

Embed
What would you like to do?
Typed Lambda Calculus (sort of)
Require Import List.
Inductive Error : Set :=
| NotImplemented : Error
| NotDeclared : Error
| NotApplicable : Error
| NotExpectedType : Error
| SomethingWrong : Error
.
Inductive LType : Set :=
| ErrorType : Error -> LType
| BaseType : nat -> LType
| FuncType : LType -> LType -> LType
.
Inductive Var : Set :=
| VarOf : nat -> Var
.
Inductive Decl : Set :=
| DeclOf : Var -> LType -> Decl
.
Inductive Term : Set :=
| VarTerm : Var -> Term
| ApplyTerm : Term -> Term -> Term
| AbstTerm : Decl -> Term -> Term
.
Definition EqualVar (x y: Var) : bool :=
match (x, y) with
| (VarOf n, VarOf m) => Nat.eqb n m
end
.
Fixpoint EqualType (x y: LType) : bool :=
match (x, y) with
| (BaseType n, BaseType m) => Nat.eqb n m
| (FuncType F X, FuncType G Y) => andb (EqualType F G) (EqualType X Y)
| (_, _) => false
end
.
Fixpoint lookup (env: list Decl) (v: Var) : LType :=
match env with
| head :: tail => (
match head with
| DeclOf u T => (
if (EqualVar u v)
then T
else (lookup tail v)
)
end
)
| nil => ErrorType NotDeclared
end
.
Fixpoint LCheck (env: list Decl) (t: Term) : LType :=
match t with
| VarTerm v => lookup env v
| ApplyTerm f a => (
match (LCheck env f) with
| ErrorType e => ErrorType e
| BaseType _ => ErrorType NotApplicable
| FuncType X Y => (
match X with
| ErrorType e => ErrorType e
| _ => (
if (EqualType X (LCheck env a))
then Y
else ErrorType NotExpectedType
)
end
)
end
)
| AbstTerm (DeclOf dv dt) a => (
FuncType dt (LCheck ((DeclOf dv dt) :: env) a)
)
end
.
(*
Test Data
Variables:
x <-> VarOf 1
y <-> VarOf 2
z <-> VarOf 3
Base Types:
T <-> BaseType 1
S <-> BaseType 2
Test 1:
Term:
\x:T.\y:T->S.yx
Environment:
[]
Correct Answer:
T->(T->S)->S
Test 2:
Term:
(\x:T.\y:T->S.yx)z
Environment:
[z:T]
Correct Answer:
(T->S)->S
*)
Definition testenv1 : (list Decl) := nil.
Definition testterm1 : Term :=
(AbstTerm
(DeclOf
(VarOf 1)
(BaseType 1)
)
(AbstTerm
(DeclOf
(VarOf 2)
(FuncType
(BaseType 1)
(BaseType 2)
)
)
(ApplyTerm
(VarTerm (VarOf 2))
(VarTerm (VarOf 1))
)
)
)
.
Eval compute in LCheck testenv1 testterm1.
Definition testenv2 : (list Decl) :=
(DeclOf (VarOf 3) (BaseType 1)) ::
nil
.
Definition testterm2 : Term :=
(ApplyTerm
testterm1
(VarTerm (VarOf 3))
)
.
Eval compute in LCheck testenv2 testterm2.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.