Library LambdaExceptions
Calculation of a compiler for the call-by-value lambda calculus +
arithmetic + exceptions.
Inductive Expr : Set :=
| Val : nat → Expr
| Add : Expr → Expr → Expr
| Throw : Expr
| Catch : Expr → Expr → Expr
| Var : nat → Expr
| Abs : Expr → Expr
| App : Expr → Expr → Expr.
Inductive Value : Set :=
| Num : nat → Value
| Clo : Expr → list Value → Value.
Definition Env := list Value.
Reserved Notation "x ⇓[ e ] y" (at level 80, no associativity).
Inductive eval : Expr → Env → option Value → Prop :=
| eval_val e n : Val n ⇓[e] Some (Num n)
| eval_add e x y m n : x ⇓[e] m → y ⇓[e] n
→ Add x y ⇓[e] (match m, n with
| Some (Num m'), Some (Num n') ⇒ Some (Num (m' + n'))
| _,_ ⇒ None
end )
| eval_throw e : Throw ⇓[e] None
| eval_catch e x y m n : x ⇓[e] m → y ⇓[e] n
→ Catch x y ⇓[e] (match m with
| None ⇒ n
| _ ⇒ m
end )
| eval_var e i : Var i ⇓[e] nth e i
| eval_abs e x : Abs x ⇓[e] Some (Clo x e)
| eval_app e x x'' y x' e' y' : x ⇓[e] Some (Clo x' e') → y ⇓[e] Some y' → x' ⇓[y' :: e'] x''
→ App x y ⇓[e] x''
| eval_app_fail x x' y y' e : x ⇓[e] x' → y ⇓[e] y' →
(x' = None ∨ ∃ n, x' = Some (Num n) ∨ y' = None) →
App x y ⇓[e] None
where "x ⇓[ e ] y" := (eval x e y).
Inductive Code : Set :=
| PUSH : nat → Code → Code
| ADD : Code → Code
| LOOKUP : nat → Code → Code
| RET : Code
| APP : Code → Code
| ABS : Code → Code → Code
| ASSERT_NUM : Code → Code
| ASSERT_CLO : Code → Code
| UNMARK : Code → Code
| MARK : Code → Code → Code
| FAIL : Code
| HALT : Code.
Fixpoint comp' (e : Expr) (c : Code) : Code :=
match e with
| Val n ⇒ PUSH n c
| Add x y ⇒ comp' x (ASSERT_NUM (comp' y (ADD c)))
| Var i ⇒ LOOKUP i c
| App x y ⇒ comp' x (ASSERT_CLO (comp' y (APP c)))
| Abs x ⇒ ABS (comp' x RET) c
| Throw ⇒ FAIL
| Catch x y ⇒ MARK (comp' y c) (comp' x (UNMARK c))
end.
Definition comp (e : Expr) : Code := comp' e HALT.
Inductive Value' : Set :=
| Num' : nat → Value'
| Exc' : Value'
| Clo' : Code → list Value' → Value'.
Definition Env' := list Value'.
Inductive Elem : Set :=
| VAL : Value' → Elem
| HAN : Code → Elem
| CLO : Code → Env' → Elem
.
Definition Stack : Set := list Elem.
Inductive Conf : Set :=
| conf : Code → Stack → Env' → Conf
| fail : Stack → Env' → Conf.
Notation "⟨ x , y , e ⟩" := (conf x y e).
Notation "⟪ x , e ⟫" := (fail x e ).
Reserved Notation "x ==> y" (at level 80, no associativity).
Inductive VM : Conf → Conf → Prop :=
| vm_push n c s e : ⟨PUSH n c, s, e⟩ ==> ⟨c, VAL (Num' n) :: s, e⟩
| vm_add c m n s e : ⟨ADD c, VAL (Num' n) :: VAL (Num' m) :: s, e⟩
==> ⟨c, VAL (Num'(m + n)) :: s, e⟩
| vm_lookup e i c v s : nth e i = Some v → ⟨LOOKUP i c, s, e ⟩ ==> ⟨c, VAL v :: s, e ⟩
| vm_lookup_fail e i c s : nth e i = None → ⟨LOOKUP i c, s, e ⟩ ==> ⟪s, e ⟫
| vm_env v c e e' s : ⟨RET, VAL v :: CLO c e :: s, e'⟩ ==> ⟨c, VAL v :: s, e⟩
| vm_fail_env c e e' s : ⟪CLO c e :: s, e'⟫ ==> ⟪s, e⟫
| vm_app c c' e e' v s : ⟨APP c, VAL v :: VAL (Clo' c' e') :: s, e⟩
==> ⟨c', CLO c e :: s, v :: e'⟩
| vm_abs c c' s e : ⟨ABS c' c, s, e ⟩ ==> ⟨c, VAL (Clo' c' e) :: s, e ⟩
| vm_fail_val s e v : ⟪ VAL v :: s, e ⟫ ==> ⟪ s, e ⟫
| vm_fail_han c s e : ⟪HAN c :: s, e ⟫ ==> ⟨c, s, e⟩
| vm_fail s e : ⟨ FAIL, s, e ⟩ ==> ⟪ s, e ⟫
| vm_add_fail s c c' e e' m : ⟨ADD c, VAL (Clo' c' e') :: VAL (Num' m) :: s, e⟩ ==> ⟪s, e⟫
| vm_unmark c n h s e : ⟨UNMARK c, VAL n :: HAN h :: s, e⟩ ==> ⟨c, VAL n :: s, e⟩
| vm_mark c h s e : ⟨MARK h c, s, e⟩ ==> ⟨c, HAN h :: s, e⟩
| vm_assert_num s c e n : ⟨ASSERT_NUM c, VAL (Num' n) :: s, e⟩ ==> ⟨c, VAL (Num' n) :: s, e⟩
| vm_assert_num_fail s c e c' e' : ⟨ASSERT_NUM c, VAL (Clo' c' e') :: s, e⟩ ==> ⟪s, e⟫
| vm_assert_clo s c e c' e' : ⟨ASSERT_CLO c, VAL (Clo' c' e') :: s, e⟩ ==> ⟨c, VAL (Clo' c' e') :: s, e⟩
| vm_assert_clo_fail s c e n : ⟨ASSERT_CLO c, VAL (Num' n) :: s, e⟩ ==> ⟪s, e⟫
where "x ==> y" := (VM x y).
Conversion functions from semantics to VM
Fixpoint conv (v : Value) : Value' :=
match v with
| Num n ⇒ Num' n
| Clo x e ⇒ Clo' (comp' x RET) (map conv e)
end.
Definition convE : Env → Env' := map conv.
Module VM <: Preorder.
Definition Conf := Conf.
Definition VM := VM.
End VM.
Module VMCalc := Calculation VM.
Import VMCalc.
Specification of the compiler
Theorem spec p e r c s : p ⇓[e] r → ⟨comp' p c, s, convE e⟩
=>> match r with
| Some r' ⇒ ⟨c , VAL (conv r') :: s, convE e⟩
| None ⇒ ⟪s, convE e⟫
end.
Setup the induction proof
Proof.
intros.
generalize dependent c.
generalize dependent s.
induction H;intros.
begin
match m, n with
| Some (Num m'), Some (Num n') ⇒ ⟨c, VAL (Num' (m' + n')) :: s, convE e ⟩
| _ , _ ⇒ ⟪ s , convE e ⟫
end.
<<= {apply vm_add}
match m, n with
| Some (Num m'), Some (Num n') ⇒ ⟨ADD c, VAL (Num' n') :: VAL (Num' m') :: s, convE e ⟩
| _ , _ ⇒ ⟪ s , convE e ⟫
end.
= {auto}
match m with
| Some (Num m') ⇒ match n with
| Some v ⇒ match v with
| Num n' ⇒ ⟨ADD c, VAL (Num' n') :: VAL (Num' m') :: s, convE e ⟩
| _ ⇒ ⟪s, convE e ⟫
end
| None ⇒ ⟪ s , convE e ⟫
end
| _ ⇒ ⟪ s , convE e ⟫
end.
<<= {apply vm_add_fail}
match m with
| Some (Num m') ⇒ match n with
| Some v ⇒ ⟨ADD c, VAL (conv v) :: VAL (Num' m') :: s, convE e ⟩
| None ⇒ ⟪ s , convE e ⟫
end
| _ ⇒ ⟪ s , convE e ⟫
end.
<<= {apply vm_fail_val}
match m with
| Some (Num m') ⇒ match n with
| Some v ⇒ ⟨ADD c, VAL (conv v) :: VAL (Num' m') :: s, convE e ⟩
| None ⇒ ⟪ VAL (Num' m') :: s , convE e ⟫
end
| _ ⇒ ⟪ s , convE e ⟫
end.
<<= { apply IHeval2 }
match m with
| Some (Num m') ⇒ ⟨comp' y (ADD c), VAL (Num' m') :: s, convE e ⟩
| _ ⇒ ⟪ s , convE e ⟫
end.
= { auto }
match m with
| Some v ⇒ match v with
| Num m' ⇒ ⟨comp' y (ADD c), VAL (Num' m') :: s, convE e ⟩
| _ ⇒ ⟪ s , convE e ⟫
end
| _ ⇒ ⟪ s , convE e ⟫
end.
<<= { first [apply vm_assert_num| apply vm_assert_num_fail] }
(match m with
| Some v ⇒ ⟨ASSERT_NUM (comp' y (ADD c)), VAL (conv v) :: s, convE e ⟩
| _ ⇒ ⟪ s , convE e ⟫
end).
<<= { apply IHeval1 }
⟨comp' x (ASSERT_NUM (comp' y (ADD c))), s, convE e⟩.
[].
begin
match m with
| Some r ⇒ ⟨c, VAL (conv r) :: s, convE e ⟩
| None ⇒ match n with
| Some r ⇒ ⟨c, VAL (conv r) :: s, convE e ⟩
| None ⇒ ⟪s, convE e ⟫
end
end.
<<= {apply IHeval2}
match m with
| Some r ⇒ ⟨c, VAL (conv r) :: s, convE e ⟩
| None ⇒ ⟨comp' y c, s, convE e ⟩
end.
<<= {apply vm_fail_han}
match m with
| Some r ⇒ ⟨c, VAL (conv r) :: s, convE e ⟩
| None ⇒ ⟪ HAN (comp' y c) :: s, convE e ⟫
end.
<<= {apply vm_unmark}
match m with
| Some r ⇒ ⟨UNMARK c, VAL (conv r) :: HAN (comp' y c) :: s, convE e ⟩
| None ⇒ ⟪ HAN (comp' y c) :: s, convE e ⟫
end.
<<= {apply IHeval1}
⟨comp' x (UNMARK c),HAN (comp' y c) :: s, convE e ⟩.
<<= {apply vm_mark}
⟨MARK (comp' y c) (comp' x (UNMARK c)),s, convE e ⟩.
[].
match m with
| Some r ⇒ ⟨c, VAL (conv r) :: s, convE e ⟩
| None ⇒ match n with
| Some r ⇒ ⟨c, VAL (conv r) :: s, convE e ⟩
| None ⇒ ⟪s, convE e ⟫
end
end.
<<= {apply IHeval2}
match m with
| Some r ⇒ ⟨c, VAL (conv r) :: s, convE e ⟩
| None ⇒ ⟨comp' y c, s, convE e ⟩
end.
<<= {apply vm_fail_han}
match m with
| Some r ⇒ ⟨c, VAL (conv r) :: s, convE e ⟩
| None ⇒ ⟪ HAN (comp' y c) :: s, convE e ⟫
end.
<<= {apply vm_unmark}
match m with
| Some r ⇒ ⟨UNMARK c, VAL (conv r) :: HAN (comp' y c) :: s, convE e ⟩
| None ⇒ ⟪ HAN (comp' y c) :: s, convE e ⟫
end.
<<= {apply IHeval1}
⟨comp' x (UNMARK c),HAN (comp' y c) :: s, convE e ⟩.
<<= {apply vm_mark}
⟨MARK (comp' y c) (comp' x (UNMARK c)),s, convE e ⟩.
[].
begin
match nth e i with
| Some r' ⇒ ⟨c, VAL (conv r') :: s, convE e ⟩
| None ⇒ ⟪s, convE e ⟫
end.
<== {first[apply vm_lookup|apply vm_lookup_fail]; unfold convE; rewrite nth_map}
⟨LOOKUP i c, s, convE e ⟩.
[].
begin
⟨c, VAL (Clo' (comp' x RET) (convE e)) :: s, convE e ⟩.
<== { apply vm_abs }
⟨ABS (comp' x RET) c, s, convE e ⟩.
[].
begin
match x'' with
| Some r' ⇒ ⟨c, VAL (conv r') :: s, convE e ⟩
| None ⇒ ⟪s, convE e ⟫
end.
<== { first[apply vm_env|apply vm_fail_env] }
match x'' with
| Some r' ⇒ ⟨RET, VAL (conv r') :: CLO c (convE e) :: s, convE (y' :: e') ⟩
| None ⇒ ⟪CLO c (convE e) :: s, convE (y' :: e') ⟫
end.
<<= { apply IHeval3 }
⟨comp' x' RET, CLO c (convE e) :: s, convE (y' :: e') ⟩.
= {reflexivity}
⟨comp' x' RET, CLO c (convE e) :: s, conv y' :: convE e' ⟩.
<== { apply vm_app }
⟨APP c, VAL (conv y') :: VAL (Clo' (comp' x' RET) (convE e')) :: s, convE e ⟩.
<<= { apply IHeval2 }
⟨comp' y (APP c), VAL (Clo' (comp' x' RET) (convE e')) :: s, convE e ⟩.
= {reflexivity}
⟨comp' y (APP c), VAL (conv (Clo x' e')) :: s, convE e ⟩.
<== {apply vm_assert_clo}
⟨ASSERT_CLO (comp' y (APP c)), VAL (conv (Clo x' e')) :: s, convE e ⟩.
<<= { apply IHeval1 }
⟨comp' x (ASSERT_CLO (comp' y (APP c))), s, convE e ⟩.
[].
begin
⟪s, convE e ⟫.
= {reflexivity}
match x' with
| Some (Clo x'' e') ⇒ match y' with
| Some r ⇒ ⟨ APP c, VAL (conv r) :: VAL (conv (Clo x'' e')) :: s, convE e ⟩
| None ⇒ ⟪s, convE e ⟫
end
| _ ⇒ ⟪s, convE e ⟫
end.
<<= {apply vm_fail_val}
match x' with
| Some (Clo x'' e') ⇒ match y' with
| Some r ⇒ ⟨ APP c, VAL (conv r) :: VAL (conv (Clo x'' e')) :: s, convE e ⟩
| None ⇒ ⟪VAL (conv (Clo x'' e')) :: s, convE e ⟫
end
| _ ⇒ ⟪s, convE e ⟫
end.
<<= {apply IHeval2}
match x' with
| Some (Clo x'' e') ⇒ ⟨comp' y (APP c), VAL (conv (Clo x'' e')) :: s, convE e ⟩
| _ ⇒ ⟪s, convE e ⟫
end.
= {reflexivity}
match x' with
| Some v ⇒ match v with
| Clo x'' e' ⇒ ⟨comp' y (APP c), VAL (conv v) :: s, convE e ⟩
| Num n ⇒ ⟪s, convE e ⟫
end
| _ ⇒ ⟪s, convE e ⟫
end.
<<= {first [apply vm_assert_clo_fail| apply vm_assert_clo]}
match x' with
| Some v ⇒ ⟨ASSERT_CLO (comp' y (APP c)), VAL (conv v) :: s, convE e ⟩
| _ ⇒ ⟪s, convE e ⟫
end.
<<= {apply IHeval1}
⟨comp' x (ASSERT_CLO (comp' y (APP c))), s, convE e ⟩.
[].
Qed.
match x'' with
| Some r' ⇒ ⟨c, VAL (conv r') :: s, convE e ⟩
| None ⇒ ⟪s, convE e ⟫
end.
<== { first[apply vm_env|apply vm_fail_env] }
match x'' with
| Some r' ⇒ ⟨RET, VAL (conv r') :: CLO c (convE e) :: s, convE (y' :: e') ⟩
| None ⇒ ⟪CLO c (convE e) :: s, convE (y' :: e') ⟫
end.
<<= { apply IHeval3 }
⟨comp' x' RET, CLO c (convE e) :: s, convE (y' :: e') ⟩.
= {reflexivity}
⟨comp' x' RET, CLO c (convE e) :: s, conv y' :: convE e' ⟩.
<== { apply vm_app }
⟨APP c, VAL (conv y') :: VAL (Clo' (comp' x' RET) (convE e')) :: s, convE e ⟩.
<<= { apply IHeval2 }
⟨comp' y (APP c), VAL (Clo' (comp' x' RET) (convE e')) :: s, convE e ⟩.
= {reflexivity}
⟨comp' y (APP c), VAL (conv (Clo x' e')) :: s, convE e ⟩.
<== {apply vm_assert_clo}
⟨ASSERT_CLO (comp' y (APP c)), VAL (conv (Clo x' e')) :: s, convE e ⟩.
<<= { apply IHeval1 }
⟨comp' x (ASSERT_CLO (comp' y (APP c))), s, convE e ⟩.
[].
begin
⟪s, convE e ⟫.
= {reflexivity}
match x' with
| Some (Clo x'' e') ⇒ match y' with
| Some r ⇒ ⟨ APP c, VAL (conv r) :: VAL (conv (Clo x'' e')) :: s, convE e ⟩
| None ⇒ ⟪s, convE e ⟫
end
| _ ⇒ ⟪s, convE e ⟫
end.
<<= {apply vm_fail_val}
match x' with
| Some (Clo x'' e') ⇒ match y' with
| Some r ⇒ ⟨ APP c, VAL (conv r) :: VAL (conv (Clo x'' e')) :: s, convE e ⟩
| None ⇒ ⟪VAL (conv (Clo x'' e')) :: s, convE e ⟫
end
| _ ⇒ ⟪s, convE e ⟫
end.
<<= {apply IHeval2}
match x' with
| Some (Clo x'' e') ⇒ ⟨comp' y (APP c), VAL (conv (Clo x'' e')) :: s, convE e ⟩
| _ ⇒ ⟪s, convE e ⟫
end.
= {reflexivity}
match x' with
| Some v ⇒ match v with
| Clo x'' e' ⇒ ⟨comp' y (APP c), VAL (conv v) :: s, convE e ⟩
| Num n ⇒ ⟪s, convE e ⟫
end
| _ ⇒ ⟪s, convE e ⟫
end.
<<= {first [apply vm_assert_clo_fail| apply vm_assert_clo]}
match x' with
| Some v ⇒ ⟨ASSERT_CLO (comp' y (APP c)), VAL (conv v) :: s, convE e ⟩
| _ ⇒ ⟪s, convE e ⟫
end.
<<= {apply IHeval1}
⟨comp' x (ASSERT_CLO (comp' y (APP c))), s, convE e ⟩.
[].
Qed.
Lemma determ_vm : determ VM.
intros C C1 C2 V. induction V; intro V'; inversion V'; subst; first [reflexivity|congruence].
Qed.
Definition terminates (p : Expr) : Prop := ∃ r, p ⇓[nil] r.
Theorem sound p C : terminates p → ⟨comp p, nil, nil⟩ =>>! C →
(∃ r, C = ⟨HALT , VAL (conv r) :: nil, nil⟩ ∧ p ⇓[nil] Some r)
∨ (C = ⟪ nil, nil⟫ ∧ p ⇓[nil] None).
Proof.
unfold terminates. intros. destruct H as [r T].
pose (spec p nil r HALT nil) as H'.
pose (determ_trc determ_vm) as D. unfold determ in D.
destruct r.
- left. eexists. split. eapply D. eassumption. split. auto. intro. destruct H.
inversion H. assumption.
- right. split. eapply D. eassumption. split. auto. intro. destruct H. inversion H. assumption.
Qed.