Library Pml

EpsilonML with numbered constructors



author: Zaynah Dargaye <dargaye@ensiie.fr>

Created: 29th April 2009.

EpsilonML with numbered constructors is the first intermediate language of MLCompCert.

Require Import List.
Require Import Coqlib.
I. Syntax
Inductive PMterm:Set :=
  | TVar : nat -> PMterm
  | TLet : PMterm -> PMterm -> PMterm
  | TFun : PMterm -> PMterm
  | TLetrec : PMterm -> PMterm -> PMterm
  | TApply : PMterm -> PMterm -> PMterm
  | TConstr : nat -> list PMterm -> PMterm
  | TMatch : PMterm -> list pat -> PMterm
with pat :Set :=
  | Patc : nat -> PMterm -> pat.



Inductive PMval :Set:=
  | PMClos : list PMval ->PMterm ->PMval
  | PMClos_rec: list PMval ->PMterm ->PMval
  | PMConstr: nat -> list PMval -> PMval
.

Inductive Peval: list PMval ->PMterm->PMval->Prop:=
  | Peval_V : forall n e v,
         nth_error e n = (Some v)-> Peval e (TVar n) v
 | Peval_Fun : forall e t , Peval e (TFun t) (PMClos e t)
 | Peval_let : forall e t1 t2 v1 v ,
          Peval e t1 v1 ->
          Peval (v1::e) t2 v ->
          Peval e (TLet t1 t2) v
  | Peval_letrec : forall e t1 t2 v,
          Peval ((PMClos_rec e t1)::e) t2 v ->
          Peval e (TLetrec t1 t2) v
  | Peval_app : forall e e' t t1 t2 v v2,
          Peval e t1 (PMClos e' t) ->
          Peval e t2 v2 ->
          Peval (v2::e') t v ->
          Peval e (TApply t1 t2) v
  | Peval_appr : forall e e' t t1 t2 v v2,
          Peval e t1 (PMClos_rec e' t) ->
          Peval e t2 v2 ->
          Peval (v2::(PMClos_rec e' t)::e') t v ->
          Peval e (TApply t1 t2) v
  | Peval_constr : forall e tl vl n ,
          Peval_list e tl vl ->
          Peval e (TConstr n tl) (PMConstr n vl)
  | Peval_match : forall e t n pl vl m tn v,
          Peval e t (PMConstr n vl) ->
          nth_error pl n = Some (Patc m tn) ->
          length vl = m ->
          Peval ((rev vl)++e) tn v ->
          Peval e (TMatch t pl) v
with
Peval_list : list PMval->list PMterm-> list PMval ->Prop:=
   | Peval_nil : forall e , Peval_list e nil nil
   | Peval_cons : forall e t lt v lv ,
          Peval e t v ->
          Peval_list e lt lv ->
          Peval_list e (t::lt) (v::lv)
.

Scheme peval_term_ind6 := Minimality for Peval Sort Prop
 with peval_terml_ind6 := Minimality for Peval_list Sort Prop.
II. Evaluation determinism

Definition Peval_det_prop (e:list PMval) (t:PMterm) (v:PMval) :Prop:=
 forall v' (E: Peval e t v'), v=v'.

Definition Peval_list_det_prop (e:list PMval) (t:list PMterm) (v:list PMval) :Prop:=
 forall v' (E: Peval_list e t v'), v=v'.

Lemma Peval_var_det:
forall (n : nat) (e : list PMval) (v : PMval),
 nth_error e n = Some v -> Peval_det_prop e (TVar n) v.

Lemma Peval_fun_det:
forall (e : list PMval) (t : PMterm),
 Peval_det_prop e (TFun t) (PMClos e t).

Lemma Peval_let_det:
forall (e : list PMval) (t1 t2 : PMterm) (v1 v : PMval),
 Peval e t1 v1 ->
 Peval_det_prop e t1 v1 ->
 Peval (v1 :: e) t2 v ->
 Peval_det_prop (v1 :: e) t2 v ->
 Peval_det_prop e (TLet t1 t2) v.

Lemma Peval_letrec_det:
forall (e : list PMval) (t1 t2 : PMterm) (v : PMval),
Peval (PMClos_rec e t1 :: e) t2 v ->
Peval_det_prop (PMClos_rec e t1 :: e) t2 v ->
Peval_det_prop e (TLetrec t1 t2) v.

Lemma Peval_app_det:
forall (e e' : list PMval) (t t1 t2 : PMterm) (v v2 : PMval),
 Peval e t1 (PMClos e' t) ->
 Peval_det_prop e t1 (PMClos e' t) ->
 Peval e t2 v2 ->
 Peval_det_prop e t2 v2 ->
 Peval (v2 :: e') t v ->
 Peval_det_prop (v2 :: e') t v ->
 Peval_det_prop e (TApply t1 t2) v.

Lemma Peval_appr_det:
forall (e e' : list PMval) (t t1 t2 : PMterm) (v v2 : PMval),
  Peval e t1 (PMClos_rec e' t) ->
  Peval_det_prop e t1 (PMClos_rec e' t) ->
  Peval e t2 v2 ->
  Peval_det_prop e t2 v2 ->
  Peval (v2 :: PMClos_rec e' t :: e') t v ->
  Peval_det_prop (v2 :: PMClos_rec e' t :: e') t v ->
  Peval_det_prop e (TApply t1 t2) v.

Lemma Peval_nil_det:
 forall e : list PMval, Peval_list_det_prop e nil nil.

Lemma Peval_cons_det:
 forall (e : list PMval) (t : PMterm) (lt : list PMterm) (v : PMval)
  (lv : list PMval),
  Peval e t v ->
  Peval_det_prop e t v ->
  Peval_list e lt lv ->
  Peval_list_det_prop e lt lv ->
  Peval_list_det_prop e (t :: lt) (v :: lv).

Lemma Peval_constr_det :
forall (e : list PMval) (tl : list PMterm) (vl : list PMval) (n : nat),
  Peval_list e tl vl ->
  Peval_list_det_prop e tl vl ->
  Peval_det_prop e (TConstr n tl) (PMConstr n vl).

Lemma Peval_match_det :
forall (e : list PMval) (t : PMterm) (n : nat) (pl : list pat)
    (vl : list PMval) (m : nat) (tn : PMterm) (v : PMval),
  Peval e t (PMConstr n vl) ->
  Peval_det_prop e t (PMConstr n vl) ->
  nth_error pl n = Some (Patc m tn) ->
  length vl = m ->
  Peval (rev vl ++ e) tn v ->
  Peval_det_prop (rev vl ++ e) tn v -> Peval_det_prop e (TMatch t pl) v.

Lemma Peval_determinism:
forall (l : list PMval) (p : PMterm) (p0 : PMval),
 Peval l p p0 -> Peval_det_prop l p p0 .

Theorem Peval_det:
 forall e t v v1,
   Peval e t v -> Peval e t v1 -> v=v1.

Theorem Peval_list_det:
 forall e tl lv lv1,
  Peval_list e tl lv -> Peval_list e tl lv1 -> lv = lv1.