Library Nml

Nml : second intermediaite language of MLCompCert



author : Zaynah Dargaye <dargaye@ensiie.fr>

created : 29th April 2009

EpsilonML with naries abstractions and applications

Require Import List.
Require Import Coqlib.
Require Import AST.
I. Syntax
Inductive Nterm:Set :=
  | NVar : nat -> Nterm
  | NLet : Nterm -> Nterm -> Nterm
  | NFun : nat->Nterm -> Nterm
  | NLetrec : nat -> Nterm -> Nterm -> Nterm
  | NApply : Nterm -> list Nterm -> Nterm
  | NConstr : nat -> list Nterm -> Nterm
  | NMatch : Nterm -> list npat -> Nterm
with npat :Set :=
  | NPatc : nat -> Nterm -> npat.
II. Big-step semantics CBV with environment


Inductive Nval :Set:=
  | NClos : nat->list Nval ->Nterm ->Nval
  | NClos_rec: nat->list Nval ->Nterm ->Nval
  | Nconstr : nat -> list Nval ->Nval
.

Inductive Neval: list Nval ->Nterm->Nval->Prop:=
  | Neval_V : forall n e v,
          nth_error e n = (Some v)-> Neval e (NVar n) v
  | Neval_Fun : forall e n t , Neval e (NFun n t) (NClos n e t)
  | Neval_let : forall e t1 t2 v1 v ,
          Neval e t1 v1 ->
          Neval (v1::e) t2 v ->
          Neval e (NLet t1 t2) v
  | Neval_letrec : forall e n t1 t2 v,
          Neval ((NClos_rec n e t1)::e) t2 v ->
          Neval e (NLetrec n t1 t2) v
  | Neval_app : forall e n e' t t1 tl v vl,
          Neval e t1 (NClos n e' t) ->
          Neval_list e tl vl ->
          List.length tl = S n ->
          Neval ((List.rev vl)++e') t v ->
          Neval e (NApply t1 tl) v
  | Neval_appr : forall e n e' t t1 tl v vl,
          Neval e t1 (NClos_rec n e' t) ->
          Neval_list e tl vl ->
          List.length tl = S n ->
          Neval ((List.rev vl)++(NClos_rec n e' t)::e') t v ->
          Neval e (NApply t1 tl) v
  | Neval_constr : forall e tl vl n ,
          Neval_list e tl vl ->
          Neval e (NConstr n tl) (Nconstr n vl)
  | Neval_match : forall e t n pl vl m tn v,
          Neval e t (Nconstr n vl) ->
          nth_error pl n = Some (NPatc m tn) ->
          length vl = m ->
          Neval ((rev vl)++e) tn v ->
          Neval e (NMatch t pl) v
with
Neval_list : list Nval->list Nterm-> list Nval ->Prop:=
   | Neval_nil : forall e , Neval_list e nil nil
   | Neval_cons : forall e t lt v lv ,
          Neval e t v ->
          Neval_list e lt lv ->
          Neval_list e (t::lt) (v::lv)
.

Scheme neval_term_ind6 := Minimality for Neval Sort Prop
 with neval_terml_ind6 := Minimality for Neval_list Sort Prop.
III. Determinism of Nml evaluation

Definition Neval_det_prop (ne: list Nval) (n: Nterm) (nv: Nval):Prop:=
 forall v , Neval ne n v -> v =nv.

Definition Neval_list_det_prop (ne: list Nval) (n: list Nterm) (nv: list Nval):Prop:=
 forall v , Neval_list ne n v -> v =nv.

Lemma det_var:
forall (n : nat) (e : list Nval) (v : Nval),
        nth_error e n = Some v -> Neval_det_prop e (NVar n) v .

Lemma det_fun:
forall (e : list Nval) (n : nat) (t : Nterm),
        Neval_det_prop e (NFun n t) (NClos n e t).

Lemma det_let:
forall (e : list Nval) (t1 t2 : Nterm) (v1 v : Nval),
 Neval e t1 v1 ->
 Neval_det_prop e t1 v1 ->
 Neval (v1 :: e) t2 v ->
 Neval_det_prop (v1 :: e) t2 v -> Neval_det_prop e (NLet t1 t2) v.

Lemma det_letrec:
forall (e : list Nval) (n : nat) (t1 t2 : Nterm) (v : Nval),
 Neval (NClos_rec n e t1 :: e) t2 v ->
 Neval_det_prop (NClos_rec n e t1 :: e) t2 v ->
 Neval_det_prop e (NLetrec n t1 t2) v.

Lemma det_app:
forall (e : list Nval) (n : nat) (e' : list Nval) (t t1 : Nterm)
 (tl : list Nterm) (v : Nval) (vl : list Nval),
 Neval e t1 (NClos n e' t) ->
 Neval_det_prop e t1 (NClos n e' t) ->
 Neval_list e tl vl ->
 Neval_list_det_prop e tl vl ->
 length tl = S n ->
 Neval (rev vl ++ e') t v ->
 Neval_det_prop (rev vl ++ e') t v ->
 Neval_det_prop e (NApply t1 tl) v.

Lemma det_appr:
forall (e : list Nval) (n : nat) (e' : list Nval) (t t1 : Nterm)
 (tl : list Nterm) (v : Nval) (vl : list Nval),
 Neval e t1 (NClos_rec n e' t) ->
 Neval_det_prop e t1 (NClos_rec n e' t) ->
 Neval_list e tl vl ->
 Neval_list_det_prop e tl vl ->
 length tl = S n ->
 Neval (rev vl ++ NClos_rec n e' t :: e') t v ->
 Neval_det_prop (rev vl ++ NClos_rec n e' t :: e') t v ->
 Neval_det_prop e (NApply t1 tl) v.

Lemma det_nil:
forall e : list Nval, Neval_list_det_prop e nil nil.

Lemma det_cons:
forall (e : list Nval) (t : Nterm) (lt : list Nterm) (v : Nval)
(lv : list Nval),
  Neval e t v ->
  Neval_det_prop e t v ->
  Neval_list e lt lv ->
  Neval_list_det_prop e lt lv ->
  Neval_list_det_prop e (t :: lt) (v :: lv).

Lemma det_constr :
 forall (e : list Nval) (tl : list Nterm) (vl : list Nval) (n : nat),
  Neval_list e tl vl ->
  Neval_list_det_prop e tl vl ->
  Neval_det_prop e (NConstr n tl) (Nconstr n vl).

Lemma det_match:
forall (e : list Nval) (t : Nterm) (n : nat) (pl : list npat)
    (vl : list Nval) (m : nat) (tn : Nterm) (v : Nval),
  Neval e t (Nconstr n vl) ->
  Neval_det_prop e t (Nconstr n vl) ->
  nth_error pl n = Some (NPatc m tn) ->
  length vl = m ->
  Neval (rev vl ++ e) tn v ->
  Neval_det_prop (rev vl ++ e) tn v -> Neval_det_prop e (NMatch t pl) v.

Lemma det_Neval:
forall (l : list Nval) (n : Nterm) (n0 : Nval),
       Neval l n n0 -> Neval_det_prop l n n0 .

Theorem Neval_det :
 forall ne n v nv,
 Neval ne n nv -> Neval ne n v -> v = nv.

Theorem Neval_list_det:
 forall nl ne nvl vl,
 Neval_list ne nl nvl -> Neval_list ne nl vl -> nvl = vl.