Library compilation
Require Import List.
Require Omega.
Syntax and big-step semantics with de Bruijn indices,
closures, and environments.
Parameter const: Set.
Inductive term: Set :=
| Var: nat -> term
| Const: const -> term
| Fun: term -> term
| App: term -> term -> term.
Inductive value: Set :=
| Int: const -> value
| Clos: term -> list value -> value.
Definition env := list value.
Inductive eval: env -> term -> value -> Prop :=
| eval_Var: forall e n v,
nth_error e n = Some v ->
eval e (Var n) v
| eval_Const: forall e i,
eval e (Const i) (Int i)
| eval_Fun: forall e a,
eval e (Fun a) (Clos a e)
| eval_App: forall e a b ca ea vb v,
eval e a (Clos ca ea) ->
eval e b vb ->
eval (vb :: ea) ca v ->
eval e (App a b) v.
CoInductive evalinf: env -> term -> Prop :=
| evalinf_App_l: forall e a b,
evalinf e a ->
evalinf e (App a b)
| evalinf_App_r: forall e a b v,
eval e a v ->
evalinf e b ->
evalinf e (App a b)
| evalinf_App_f: forall e a b ca ea vb,
eval e a (Clos ca ea) ->
eval e b vb ->
evalinf (vb :: ea) ca ->
evalinf e (App a b).
CoInductive coeval: env -> term -> value -> Prop :=
| coeval_Var: forall e n v,
nth_error e n = Some v ->
coeval e (Var n) v
| coeval_Const: forall e i,
coeval e (Const i) (Int i)
| coeval_Fun: forall e a,
coeval e (Fun a) (Clos a e)
| coeval_App: forall e a b ca ea vb v,
coeval e a (Clos ca ea) ->
coeval e b vb ->
coeval (vb :: ea) ca v ->
coeval e (App a b) v.
Abstract machine and compilation scheme
Inductive instr: Set :=
| INop: instr
| IVar: nat -> instr
| IConst: const -> instr
| IClosure: list instr -> instr
| IApp: instr
| IReturn: instr.
Definition code := list instr.
Fixpoint compile (a: term) (k: code) {struct a} : code :=
match a with
| Var n => IVar n :: k
| Const i => IConst i :: k
| Fun b => IClosure (compile b (IReturn :: nil)) :: k
| App b c => compile b (compile c (IApp :: k))
end.
Inductive mvalue: Set :=
| MInt: const -> mvalue
| MClos: code -> list mvalue -> mvalue.
Definition menv := list mvalue.
Inductive slot : Set :=
| Slot_value: mvalue -> slot
| Slot_return: code -> menv -> slot.
Definition stack := list slot.
Inductive transition: code -> menv -> stack ->
code -> menv -> stack -> Prop :=
| trans_INop: forall k e s,
transition (INop :: k) e s
k e s
| trans_IVar: forall n k e s v,
nth_error e n = Some v ->
transition (IVar n :: k) e s
k e (Slot_value v :: s)
| trans_IConst: forall n k e s,
transition (IConst n :: k) e s
k e (Slot_value (MInt n) :: s)
| trans_IClosure: forall c k e s,
transition (IClosure c :: k) e s
k e (Slot_value (MClos c e) :: s)
| trans_IApp: forall k e v k' e' s,
transition (IApp :: k) e (Slot_value v :: Slot_value (MClos k' e') :: s)
k' (v :: e') (Slot_return k e :: s)
| trans_IReturn: forall k e v k' e' s,
transition (IReturn :: k) e (Slot_value v :: Slot_return k' e' :: s)
k' e' (Slot_value v :: s).
Inductive trans: code -> menv -> stack ->
code -> menv -> stack -> Prop :=
| trans_refl: forall k1 e1 s1,
trans k1 e1 s1 k1 e1 s1
| trans_step: forall k1 e1 s1 k2 e2 s2 k3 e3 s3,
transition k1 e1 s1 k2 e2 s2 ->
trans k2 e2 s2 k3 e3 s3 ->
trans k1 e1 s1 k3 e3 s3.
Inductive transplus: code -> menv -> stack ->
code -> menv -> stack -> Prop :=
| transplus_base: forall k1 e1 s1 k2 e2 s2,
transition k1 e1 s1 k2 e2 s2 ->
transplus k1 e1 s1 k2 e2 s2
| transplus_step: forall k1 e1 s1 k2 e2 s2 k3 e3 s3,
transition k1 e1 s1 k2 e2 s2 ->
transplus k2 e2 s2 k3 e3 s3 ->
transplus k1 e1 s1 k3 e3 s3.
Lemma transplus_transitive:
forall k1 e1 s1 k2 e2 s2 k3 e3 s3,
transplus k1 e1 s1 k2 e2 s2 ->
transplus k2 e2 s2 k3 e3 s3 ->
transplus k1 e1 s1 k3 e3 s3.
Proof.
induction 1; intros; eapply transplus_step; eauto.
Qed.
Lemma transplus_trans:
forall k1 e1 s1 k2 e2 s2,
transplus k1 e1 s1 k2 e2 s2 ->
trans k1 e1 s1 k2 e2 s2.
Proof.
induction 1; eapply trans_step; eauto. apply trans_refl.
Qed.
CoInductive transinf: code -> menv -> stack -> Prop :=
| transinf_intro: forall k1 e1 s1 k2 e2 s2,
transition k1 e1 s1 k2 e2 s2 ->
transinf k2 e2 s2 ->
transinf k1 e1 s1.
CoInductive transinfN: nat -> code -> menv -> stack -> Prop :=
| transinfN_stutter: forall n k e s,
transinfN n k e s ->
transinfN (S n) k e s
| transinfN_perform: forall n1 k1 e1 s1 n2 k2 e2 s2,
transplus k1 e1 s1 k2 e2 s2 ->
transinfN n2 k2 e2 s2 ->
transinfN n1 k1 e1 s1.
Lemma decompose_transinfN:
forall n k e s,
transinfN n k e s ->
exists n', exists k', exists e', exists s',
transition k e s k' e' s' /\ transinfN n' k' e' s'.
Proof.
intros until s.
assert (
forall m n, m > n ->
transinfN n k e s ->
exists n', exists k', exists e', exists s',
transition k e s k' e' s' /\ transinfN n' k' e' s').
induction m; intros.
cut False; [contradiction | omega].
inversion H0.
eapply IHm; eauto. omega.
inversion H1.
exists n2; exists k2; exists e2; exists s2.
split. assumption. assumption.
exists 0; exists k3; exists e3; exists s3.
split. assumption. eapply transinfN_perform; eauto.
intros; eauto.
Qed.
Lemma transinfN_transinf:
forall n k e s,
transinfN n k e s -> transinf k e s.
Proof.
cofix COINDHYP; intros.
generalize (decompose_transinfN _ _ _ _ H).
intros [n' [k' [e' [s' [T TINF]]]]].
apply transinf_intro with k' e' s'. assumption.
apply COINDHYP with n'; assumption.
Qed.
CoInductive cotrans: code -> menv -> stack ->
code -> menv -> stack -> Prop :=
| cotrans_refl: forall k e s,
cotrans k e s k e s
| cotrans_step: forall k1 e1 s1 k2 e2 s2 k3 e3 s3,
transition k1 e1 s1 k2 e2 s2 ->
cotrans k2 e2 s2 k3 e3 s3 ->
cotrans k1 e1 s1 k3 e3 s3.
CoInductive cotransN: nat -> code -> menv -> stack ->
code -> menv -> stack -> Prop :=
| cotransN_perform: forall n k1 e1 s1 k2 e2 s2,
transition k1 e1 s1 k2 e2 s2 ->
cotransN n k1 e1 s1 k2 e2 s2
| cotransN_trans: forall n n' k1 e1 s1 k2 e2 s2 k3 e3 s3,
cotransN n k1 e1 s1 k2 e2 s2 ->
cotransN n' k2 e2 s2 k3 e3 s3 ->
cotransN (S n) k1 e1 s1 k3 e3 s3.
Lemma decompose_cotransN:
forall n k1 e1 s1 k3 e3 s3,
cotransN n k1 e1 s1 k3 e3 s3 ->
transition k1 e1 s1 k3 e3 s3 \/
exists k2, exists e2, exists s2, exists n2,
transition k1 e1 s1 k2 e2 s2 /\ cotransN n2 k2 e2 s2 k3 e3 s3.
Proof.
induction n; intros.
inversion H. left. auto.
inversion H. left. auto.
right.
elim (IHn _ _ _ _ _ _ H1).
intros. exists k2; exists e2; exists s2; exists n'. split. auto. auto.
intros [k' [e' [s' [n'' [A B]]]]].
exists k'; exists e'; exists s'; exists (S n''). split. auto.
eapply cotransN_trans; eauto.
Qed.
Lemma cotransN_cotrans:
forall n k1 e1 s1 k2 e2 s2,
cotransN n k1 e1 s1 k2 e2 s2 ->
cotrans k1 e1 s1 k2 e2 s2.
Proof.
cofix COINDHYP.
intros. elim (decompose_cotransN _ _ _ _ _ _ _ H).
intro. eapply cotrans_step. eauto. apply cotrans_refl.
intros [k' [e' [s' [n' [A B]]]]].
apply cotrans_step with k' e' s'. assumption.
apply COINDHYP with n'. assumption.
Qed.
Compiler correctness, terminating programs
Fixpoint compile_value (v: value) : mvalue :=
match v with
| Int n => MInt n
| Clos a e =>
let fix compenv (e: env) : menv :=
match e with
| nil => nil
| v :: e' => compile_value v :: compenv e'
end in
MClos (compile a (IReturn :: nil)) (compenv e)
end.
Fixpoint compile_env (e: env) : menv :=
match e with
| nil => nil
| v :: e' => compile_value v :: compile_env e'
end.
Lemma find_var_match:
forall e n v,
nth_error e n = Some v ->
nth_error (compile_env e) n = Some (compile_value v).
Proof.
induction e; destruct n; simpl; intros.
discriminate.
discriminate.
unfold Specif.value in *; congruence.
auto.
Qed.
Lemma compile_eval:
forall e a v,
eval e a v ->
forall k s,
transplus (compile a k) (compile_env e) s
k (compile_env e) (Slot_value (compile_value v) :: s).
Proof.
induction 1; simpl; intros.
apply transplus_base. constructor. apply find_var_match; auto.
apply transplus_base. constructor.
apply transplus_base. constructor.
eapply transplus_transitive; eauto.
eapply transplus_transitive; eauto.
eapply transplus_step.
change (compile_value (Clos ca ea))
with (MClos (compile ca (IReturn :: nil)) (compile_env ea)).
constructor.
eapply transplus_transitive; eauto.
apply transplus_base. constructor.
Qed.
Compiler correctness, non-terminating programs
Fixpoint left_app_height (a: term) : nat :=
match a with
| App b c => S(left_app_height b)
| _ => 0
end.
Lemma compile_evalinf_aux:
forall e a k s,
evalinf e a ->
transinfN (left_app_height a) (compile a k) (compile_env e) s.
Proof.
cofix COINDHYP. intros.
inversion H; simpl.
apply transinfN_stutter.
apply COINDHYP. auto.
apply transinfN_perform with (left_app_height b)
(compile b (IApp :: k))
(compile_env e)
(Slot_value (compile_value v) :: s).
apply compile_eval; auto.
apply COINDHYP; auto.
apply transinfN_perform with (left_app_height ca)
(compile ca (IReturn :: nil))
(compile_env (vb :: ea))
(Slot_return k (compile_env e) :: s).
apply transplus_transitive with
(compile b (IApp :: k)) (compile_env e)
(Slot_value (compile_value (Clos ca ea)) :: s).
apply compile_eval; auto.
apply transplus_transitive with
(IApp :: k) (compile_env e)
(Slot_value (compile_value vb) :: Slot_value (compile_value (Clos ca ea)) :: s).
apply compile_eval; auto.
apply transplus_base. simpl. fold compile_env. constructor.
apply COINDHYP; auto.
Qed.
Lemma compile_evalinf:
forall e a k s,
evalinf e a ->
transinf (compile a k) (compile_env e) s.
Proof.
intros. apply transinfN_transinf with (left_app_height a).
apply compile_evalinf_aux. auto.
Qed.
Compiler correctness, using
coeval and cotrans
Lemma compile_coeval_aux:
forall e a v,
coeval e a v ->
forall k s,
cotransN (left_app_height a)
(compile a k) (compile_env e) s
k (compile_env e) (Slot_value (compile_value v) :: s).
Proof.
cofix COINDHYP. intros.
inversion H; simpl.
apply cotransN_perform. constructor. apply find_var_match; auto.
apply cotransN_perform. constructor.
apply cotransN_perform. constructor.
apply cotransN_trans with
(S (left_app_height b))
(compile b (IApp :: k)) (compile_env e)
(Slot_value (compile_value (Clos ca ea)) :: s).
apply COINDHYP. assumption.
apply cotransN_trans with
(S 0)
(IApp :: k) (compile_env e)
(Slot_value (compile_value vb) ::
Slot_value (compile_value (Clos ca ea)) :: s).
apply COINDHYP. assumption.
apply cotransN_trans with
(S (left_app_height ca))
(compile ca (IReturn :: nil)) (compile_env (vb :: ea))
(Slot_return k (compile_env e) :: s).
apply cotransN_perform.
change (compile_value (Clos ca ea))
with (MClos (compile ca (IReturn :: nil)) (compile_env ea)).
simpl compile_env. constructor.
apply cotransN_trans with
0
(IReturn :: nil)
(compile_env (vb :: ea))
(Slot_value (compile_value v) :: Slot_return k (compile_env e) :: s).
apply COINDHYP. assumption.
apply cotransN_perform.
constructor.
Qed.
Lemma compile_coeval:
forall e a v k s,
coeval e a v ->
cotrans (compile a k) (compile_env e) s
k (compile_env e) (Slot_value (compile_value v) :: s).
Proof.
intros. apply cotransN_cotrans with (left_app_height a).
apply compile_coeval_aux. assumption.
Qed.