Module compilation

From Coq Require Import List Lia.


Parameter const: Type.

Inductive term: Type :=
  | Var: nat -> term
  | Const: const -> term
  | Fun: term -> term
  | App: term -> term -> term.

Inductive value: Type :=
  | 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.


Inductive instr: Type :=
  | 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: Type :=
  | MInt: const -> mvalue
  | MClos: code -> list mvalue -> mvalue.

Definition menv := list mvalue.

Inductive slot : Type :=
  | 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.

Lemma transplus_trans:
  forall k1 e1 s1 k2 e2 s2,
  transplus k1 e1 s1 k2 e2 s2 ->
  trans k1 e1 s1 k2 e2 s2.

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'.

Lemma transinfN_transinf:
  forall n k e s,
  transinfN n k e s -> transinf k e s.


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.

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.


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).

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).


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.

Lemma compile_evalinf:
  forall e a k s,
  evalinf e a ->
  transinf (compile a k) (compile_env e) s.


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).

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).