Library c2pp

Semantics preservation of the constructor numbering

author : Zaynah Dargaye <>

created : 29th April 2009

Require Import List.
Require Import Coqlib.
Require Import Coqlib2.
Require Import AST.
Require Import Epsml.
Require Import Pml.
Require Import Compare_dec.
Require Import EqNat.
Require Import c2p.
Require Import c2pp_pre.

Section Eps2PP.

Variable gam:gamma.
Variable g: GMenv.

Fixpoint c2pl (lc : list Epsterm) :option (list PMterm):=
    match lc with
    | nil => Some nil
    | c::l => do p<- c2p gam c ;
                 do lp<- c2pl l ;
                 Some (p::lp)

Fixpoint c2p_cpat_list (cpl : list cpat) {struct cpl}: option (list (nat*pat)) :=
      match cpl with
      | nil => Some nil
      | c::l => do p <- c2p_cpat gam c ; do pl <- c2p_cpat_list l ;
                   Some (p::pl)

I. Correspondance between environments

Inductive match_val : Epsval -> PMval -> Prop :=
| match_clos : forall ce c pe p ,
                       match_env ce pe -> c2p gam c = Some p ->
                       match_val (EpsClos ce c) (PMClos pe p)
| match_closr : forall ce c pe p ,
                       match_env ce pe -> c2p gam c = Some p ->
                       match_val (EpsClos_rec ce c) (PMClos_rec pe p)
| match_constr : forall n C cvl pvl ,
                       get_num gam C=Some n->
                       match_env cvl pvl ->
                       match_val (Epsconstr C cvl) (PMConstr n pvl)
with match_env : list Epsval -> list PMval -> Prop:=
| match_nil : match_env nil nil
| match_cons : forall hdc hdp tlc tlp,
                        match_val hdc hdp -> match_env tlc tlp ->
                        match_env (hdc::tlc) (hdp::tlp) .

Hypothesis match_global :
 forall l C,
   In l g -> In C l ->
   exists n , nth_error l n = Some C /\
                  get_num gam C = Some n.

Hypothesis NOREPET : forall l , In l g -> list_norepet l.

Lemma insert_length :
 forall l n p l2 , insert n p l = Some l2 -> length l2 = S(length l).

Lemma sort_length :
 forall l1 l2 , sort l1 = Some l2 -> length l2 = length l1.

Lemma c2p_cpat_list_length :
 forall l l2 , c2p_cpat_list l = Some l2 -> length l2 = length l.

Lemma extract_constr_match_length :
 forall l , length (extract_constr_match l) = length l.

Lemma match_env_length :
forall c p , match_env c p -> length c = length p.

Lemma match_env_nth:
 forall ce pe n cv ,
 nth_error ce n = Some cv ->
 match_env ce pe ->
 exists pv, nth_error pe n = Some pv /\ match_val cv pv .

Lemma match_env_append :
 forall c1 c2 p1 p2,
   match_env c1 p1 -> match_env c2 p2 ->
   match_env (c1++c2) (p1++p2).

Lemma match_env_rev :
 forall c p ,
    match_env c p -> match_env (rev c) (rev p).

II Pattern-matching evaluation properties
Lemma in_c2p_cpatlist :
forall pl l m tn C n ,
 In (Epsatc C m tn) pl -> get_num gam C = Some n ->
 c2p_cpat_list pl = Some l ->
 exists ptn, In (n, Patc m ptn) l /\ c2p gam tn = Some ptn.

Lemma c2p_list_get_num :
 forall pl l ,
 c2p_cpat_list pl = Some l ->
 get_numC_list gam (extract_constr_match pl) =
                    Some ( (@fst nat pat) l).

Lemma in_case_in_constr:
 forall pl C m tn ,
       In (Epsatc C m tn) pl ->
       In C (extract_constr_match pl).

Lemma wf_match_ok :
 forall l1 l3 l2 ,
     In (l3++l1++l2) g ->
     get_numC_list gam l1 =
     Some (enum_list (length l1) (length l3)).

Lemma wf_match_inv :
 forall pl , wf_match pl g ->
  exists l,
     get_numC_list gam(extract_constr_match pl) = Some l /\
      list_permut_norepet nat l (enum_list (length pl) O).

III Simulation scheme
Definition c2p_prop (ce:list Epsval) (c:Epsterm) (cv:Epsval) :Prop:=
forall pe p
   (MENV:match_env ce pe)
   (TRANSL : c2p gam c = Some p),
   exists pv , Peval pe p pv /\
                    match_val cv pv.

Definition c2pl_prop (ce:list Epsval) (cl: list Epsterm) (cvl : list Epsval):Prop:=
forall pe pl
   (MENV:match_env ce pe)
   (TRANSL : c2pl cl = Some pl),
      exists pvl , Peval_list pe pl pvl /\
                    match_env cvl pvl.

Lemma c2p_var :
forall (n : nat) (e : list Epsval) (v : Epsval),
        nth_error e n = Some v -> c2p_prop e (EpsVar n) v.

Lemma c2p_fun :
forall (e : list Epsval) (t : Epsterm), c2p_prop e (EpsFun t) (EpsClos e t).

Lemma c2p_let:
forall (e : list Epsval) (t1 t2 : Epsterm) (v1 v : Epsval),
 Epseval g e t1 v1 ->
 c2p_prop e t1 v1 ->
 Epseval g (v1 :: e) t2 v ->
 c2p_prop (v1 :: e) t2 v -> c2p_prop e (EpsLet t1 t2) v.

Lemma c2p_letrec:
forall (e : list Epsval) (t1 t2 : Epsterm) (v : Epsval),
 Epseval g (EpsClos_rec e t1 :: e) t2 v ->
 c2p_prop (EpsClos_rec e t1 :: e) t2 v ->
 c2p_prop e (EpsLetrec t1 t2) v.

Lemma c2p_app:
forall (e e' : list Epsval) (t t1 t2 : Epsterm) (v v2 : Epsval),
  Epseval g e t1 (EpsClos e' t) ->
  c2p_prop e t1 (EpsClos e' t) ->
  Epseval g e t2 v2 ->
  c2p_prop e t2 v2 ->
  Epseval g (v2 :: e') t v ->
  c2p_prop (v2 :: e') t v -> c2p_prop e (EpsApply t1 t2) v.

Lemma c2p_appr :
forall (e e' : list Epsval) (t t1 t2 : Epsterm) (v v2 : Epsval),
 Epseval g e t1 (EpsClos_rec e' t) ->
 c2p_prop e t1 (EpsClos_rec e' t) ->
 Epseval g e t2 v2 ->
 c2p_prop e t2 v2 ->
 Epseval g (v2 :: EpsClos_rec e' t :: e') t v ->
 c2p_prop (v2 :: EpsClos_rec e' t :: e') t v ->
 c2p_prop e (EpsApply t1 t2) v.

Lemma c2p_constr:
forall (e : list Epsval) (tl : list Epsterm) (vl : list Epsval) (n : ident),
 exists_constr n g ->
 Epseval_list g e tl vl ->
 c2pl_prop e tl vl -> c2p_prop e (EpsConstr n tl) (Cconstr n vl).

Lemma c2p_match:
forall (e : list Epsval) (t : Epsterm) (c : ident) (pl : list cpat)
 (vl : list Epsval) (m : nat) (tn : Epsterm) (v : Epsval),
 Epseval g e t (Epsconstr c vl) ->
 c2p_prop e t (Epsconstr c vl) ->
 wf_match pl g ->
 In (Epsatc c m tn) pl ->
 length vl = m ->
 Epseval g (rev vl ++ e) tn v ->
 c2p_prop (rev vl ++ e) tn v -> c2p_prop e (EpsMatch t pl) v.

Lemma c2p_nil:
forall e : list Epsval, c2pl_prop e nil nil.

Lemma c2p_cons:
forall (e : list Epsval) (t : Epsterm) (lt : list Epsterm) (v : Epsval)
 (lv : list Epsval),
 Epseval g e t v ->
 c2p_prop e t v ->
 Epseval_list g e lt lv ->
 c2pl_prop e lt lv -> c2pl_prop e (t :: lt) (v :: lv).

Theorem c2p_correct:
 forall (l : list Epsval) (c : Epsterm) (c0 : Epsval),
       Epseval g l c c0 -> c2p_prop l c c0.

End Eps2PP.

IV Semantics preservation of a program transformation

Lemma get_num_num_tl :
forall l a C n m,
get_num (num_list m l) C = Some n -> a <> C ->
 get_num (num_list m (a::l))C = Some (S n).

Lemma num_list_correct:
forall l C,
 In C l -> list_norepet l ->
 exists n : nat,
  nth_error l n = Some C /\ get_num (num_list 0 l ) C = Some n.

Lemma get_num_app_hd:
forall l C lp n m,
 In C l -> list_norepet l ->
 get_num (num_list m l) C= Some n->
 get_num (num_list m l ++ list_flat lp) C = Some n .

Lemma get_num_not :
 forall l a m,
 ~In a l -> get_num (num_list m l) a =None.

Lemma get_num_snd:
 forall l1 l2 C n,
  get_num l2 C = Some n ->
  get_num l1 C = None ->
  get_num (l1 ++ l2) C = Some n.

Lemma get_num_app_tl :
forall lp a C n ,
  get_num (list_flat lp) C = Some n ->
 ~In C a ->
 get_num (list_flat (a :: lp)) C = Some n.

Lemma match_global_make:
forall lp,
 list_norepet lp ->
 (forall l, In l lp -> list_norepet l) ->
 (forall l1 l2, l1<>l2 -> In l1 lp ->
         In l2 lp -> list_disjoint l1 l2) ->
 forall (l : list ident) (C : ident),
  In l lp ->
  In C l ->
  exists n : nat,
    nth_error l n = Some C /\ get_num (list_flat lp) C = Some n.

Theorem trad_prg_correct:
 forall p v t, eval_prog p v ->
                 trad_prg p = Some t ->
  exists pv, Peval nil t pv /\ match_val (list_flat p.(prog_type)) v pv.