Library Fminor
Fminor : 7th and last intermediate language of MLCompCert
Author : Zaynah Dargaye
Created: 29th April 2009
Programs are organised in global functions. Variables are named. Fminor is in intermediate monadic form with a materialisation of the set of roots
Require Import List.
Require Import Coqlib.
Require Import Coqlib2.
Require Import Integers.
Require Import AST.
Require Import Globalenvs.
Require Import Maps.
Require Import Mml.
Require Import FSets.
Require Import FSetAVL.
Require Import Ordered.
Require Import Compare_dec.
Require Import Mml_pre.
I. Syntax
Inductive Param:Set:= | VR :ident->Param | SL :nat->Param.
Inductive catom:Set:=
| Cvar: ident->catom
| Cfield: nat->catom->catom
| Cslot : nat->catom.
Inductive Cterm : Set:=
| Catom : catom->Cterm
| Capp: option ident-> catom -> list catom ->nat->Cterm
| Cclos: ident->list catom ->nat->Cterm
| Ccon : nat->list catom->nat->Cterm
| Clet : ident ->Cterm->Cterm->Cterm
| Cpush : nat ->Cterm->Cterm->Cterm
| Cmatch: catom -> list cpat ->Cterm
with cpat :Set:=
|CPatc : list Param -> Cterm->cpat.
Record cfunction :Set:=
mkCfun { cn_params: list ident ; cn_stackspace : nat ;
cn_vars: list ident; cn_body : Cterm }.
Record cprogram : Set := mkCprogram {
cprog_funct: list (ident * cfunction);
cprog_main: cfunction
}.
II. Big-step semantics CBV with 2 environments
Fixpoint recup_cfunct (id:ident) (s:list (ident*cfunction)) {struct s}:option cfunction:=
match s with
|nil => None
|(id1,d1)::l => if (peq id id1) then Some d1 else recup_cfunct id l
end.
Inductive cval:Set:=
|cclos : ident->list cval -> cval
|cconstr: nat->list cval -> cval .
Definition env:= PTree.t cval.
Definition spenv := nat-> option cval.
Definition sp_empty := fun n:nat =>(@None cval).
Definition sp_get (n:nat) (sp:spenv):= sp n.
Definition sp_set (n:nat) (cv:cval) (sp:spenv):=
(fun m=> if nat_eq n m then Some cv else sp m).
Lemma sp_gss:
forall n cv sp, sp_get n (sp_set n cv sp) =Some cv.
Lemma sp_gso:
forall n n0 cv sp, n<>n0 ->
sp_get n0 (sp_set n cv sp) = sp_get n0 sp.
Fixpoint set_local_pat (xl:list Param) (vl:list cval)
(e:env) (s:spenv){struct xl}: option (env*spenv):=
match xl,vl with
| nil, nil => Some (e,s)
| VR a::xm , va::vm =>
(set_local_pat xm vm (PTree.set a va e) s)
| SL k::xm , va::vm =>
(set_local_pat xm vm e (sp_set k va s))
| _,_ => None
end.
Fixpoint set_loc_par (xl:list ident) (vl:list cval) (e:env) {struct xl}:=
match xl,vl with
| nil,nil => Some e
| x::xm,v::vm => (set_loc_par xm vm (PTree.set x v e))
| _ , _ =>None
end.
Definition varp_test_prop (x:Param) :=
forall id , x = VR id -> var_test_prop id.
Definition varpl_test_prop (xl:list Param) :=
forall x, In x xl -> varp_test_prop x.
Section Csem.
Variable cf: list (ident*cfunction).
Inductive ceval_atom: env->spenv->catom->cval->Prop:=
| cvar: forall e s id v , var_test_prop id ->
PTree.get id e =Some v -> ceval_atom e s (Cvar id) v
| cfield: forall e s t fid vl n v,
ceval_atom e s t (cclos fid vl) ->
nth_error vl n=Some v->
ceval_atom e s (Cfield (S n) t) v
| cslot: forall e s n v,
sp_get n s = Some v -> ceval_atom e s (Cslot n ) v.
Inductive ceval_atlist: env->spenv->list catom->list cval->Prop:=
| cnil: forall e s, ceval_atlist e s nil nil
| ccons : forall e s chd vhd ctl vtl,
ceval_atom e s chd vhd->ceval_atlist e s ctl vtl->
ceval_atlist e s (chd::ctl) (vhd::vtl).
Inductive ceval_term : env->spenv ->Cterm->env->spenv->cval->Prop:=
| cat: forall e1 s1 a va , ceval_atom e1 s1 a va ->
ceval_term e1 s1 (Catom a) e1 s1 va
| ccl : forall z e1 s1 fid d tl vl ,
recup_cfunct fid cf = Some d ->
ceval_atlist (@PTree.empty cval) s1 tl vl ->
Zlt (8+(Z_of_nat z)*4+4) Int.max_signed ->
Zlt ( (Z_of_nat(S(length tl)))*4+4) Int.max_signed ->
ceval_term e1 s1 (Cclos fid tl z) (@PTree.empty cval) s1 (cclos fid vl)
| ccn : forall z e1 n s1 tl vl ,
ceval_atlist (@PTree.empty cval) s1 tl vl ->
Zlt (8+(Z_of_nat z)*4+4) Int.max_signed ->
Zlt ((Z_of_nat (S (length tl)))*4+4) Int.max_signed ->
ceval_term e1 s1 (Ccon n tl z) (@PTree.empty cval) s1 (cconstr n vl)
| clet: forall id e s t1 v1 e1 s1 t2 v2 e2 s2,
ceval_term e s t1 e1 s1 v1 -> var_test_prop id ->
ceval_term (PTree.set id v1 e1) s1 t2 e2 s2 v2 ->
ceval_term e s (Clet id t1 t2) e2 s2 v2
|cpush : forall n t1 v1 t2 e s e1 s1 e2 s2 v2,
ceval_term e s t1 e1 s1 v1 ->
ceval_term e1 (sp_set n v1 s1) t2 e2 s2 v2 ->
ceval_term e s (Cpush n t1 t2) e2 s2 v2
|capp: forall z info t1 targs fid vl d vargs e s e1 e2 s2 v,
ceval_atom e s t1 (cclos fid vl) ->
recup_cfunct fid cf = Some d->
Zlt (8+(Z_of_nat z)*4+4) Int.max_signed ->
ceval_atlist e s targs vargs-> list_norepet (cn_params d) ->
varl_test_prop (cn_params d) ->
list_disjoint (Roots::cn_params d) (cn_vars d) ->
set_loc_par (cn_params d) ( (cclos fid vl)::vargs)
(@PTree.empty cval) =Some e1->
Zlt (8+Z_of_nat (cn_stackspace d)*4+4) Int.max_signed ->
ceval_term e1 sp_empty (cn_body d) e2 s2 v ->
(info = None \/ info = Some fid) ->
ceval_term e s (Capp info t1 targs z) (@PTree.empty cval) s v
| cmatch : forall e s a n vl pl xl p e1 s1 e2 s2 v,
Zlt (Z_of_nat (length pl)) Int.max_signed ->
ceval_atom e s a (cconstr n vl) ->
nth_error pl n = Some (CPatc xl p) -> list_norepet xl->
varpl_test_prop xl ->
set_local_pat xl vl e s = Some (e1,s1) ->
ceval_term e1 s1 p e2 s2 v->
ceval_term e s (Cmatch a pl) e2 s2 v.
End Csem.
Definition ceval_prog (p:cprogram) (v:cval) :Prop:=
list_norepet (List.map (@fst ident cfunction) (cprog_funct p)) /\
~In (Psucc xH) (List.map (@fst ident cfunction) (cprog_funct p)) /\
~In xH (List.map (@fst ident cfunction) (cprog_funct p)) /\
exists ef, exists spf,
(cn_params (cprog_main p)) = nil /\
(8 + Z_of_nat (cn_stackspace (cprog_main p)) * 4 + 4 < Int.max_signed)%Z /\
ceval_term (cprog_funct p)
(@PTree.empty cval) sp_empty (cn_body (cprog_main p)) ef spf v.