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.