Library c2pp

Semantics preservation of the constructor numbering

author : Zaynah Dargaye <dargaye@ensiie.fr>

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)

    end.




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)  

      end.

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 (List.map (@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.