Library Mml
The Intermediate Monadic Form (Mon) : 6th intermediate language of MLCompCert
Author : Zaynah Dargaye
Created: 29th April 2009
Programs are aorganised into global functions and variable are named. The intermediate monadic form is a weak form of A-normal form.
Require Import List.
Require Import Coqlib.
Require Import Coqlib2.
Require Import AST.
Require Import Globalenvs.
Require Import Maps.
I. Syntax
Inductive atom:Set:=
| Fvar: ident->atom
| Ffield: nat->atom->atom.
Inductive Fterm:Set:=
| Atom : atom->Fterm
| Fapp: option ident-> atom -> list atom ->Fterm
| Fclos: ident->list atom ->Fterm
| Fcon : nat->list atom->Fterm
| Flet :ident->Fterm->Fterm->Fterm
| Fmatch: atom -> list fpat ->Fterm
with fpat :Set:=
|FPatc : list ident -> Fterm->fpat .
Record funct :Set:=
mkfunct{
fun_par : list ident ;
fun_body : Fterm
}.
Record fprog :Set:=
mkfprog{
fprog_main : Fterm ;
fprog_def : list (ident * funct)
} .
II. Big-step semantic CBV with environment and a global state (list of global functions)
Fixpoint recup_funct (id:ident) (s:list (ident*funct)) {struct s}:option funct:=
match s with
|nil => None
|(id1,d1)::l => if (peq id id1) then Some d1 else recup_funct id l
end.
Inductive fval:Set:=
|fclos : ident->list fval -> fval
|fconstr: nat->list fval -> fval .
Definition env:= PTree.t fval.
Fixpoint set_local_par (xl:list ident) (vl:list fval)
(e:env){struct xl}: option env:=
match xl,vl with
| nil, nil => Some e
| a::xm , va::vm =>
(set_local_par xm vm (PTree.set a va e))
| _,_ => None
end.
Definition res:= (xO xH).
Definition alloc_block := (xO xH).
Definition Roots:= xH.
Definition tmp_st:= (xI xH).
Definition var_test (p:positive) :=
if (peq p Roots) then false else
if (peq p tmp_st) then false else
if (peq p res) then false else true.
Definition var_test_prop (id:ident) :Prop:=
id<>Roots /\ id <>tmp_st /\ id <>res.
Definition varl_test_prop (lid : list ident) :Prop:=
forall x, In x lid ->var_test_prop x.
Fixpoint varl_test (pl: list ident) :=
match pl with
| nil => true | a::m => if (var_test a) then varl_test m else false
end.
Section Fsem.
Variable s: list (ident*funct).
Inductive feval_atom:env->atom->fval->Prop:=
|fvar: forall e id v , var_test_prop id ->
PTree.get id e =Some v -> feval_atom e (Fvar id) v
|ffield : forall e n fid t vl v,
feval_atom e t (fclos fid vl) ->
nth_error vl n=Some v->
feval_atom e (Ffield (S n) t) v.
Inductive feval_atlist: env->list atom->list fval->Prop:=
|fanil: forall e, feval_atlist e nil nil
|facons: forall e a v al vl, feval_atom e a v->feval_atlist e al vl->
feval_atlist e (a::al) (v::vl).
Inductive feval_term:env->Fterm->fval->Prop:=
|fAtom : forall e a v,
feval_atom e a v ->
feval_term e (Atom a) v
| fClos: forall e fid tl vl d,
recup_funct fid s = Some d ->
feval_atlist e tl vl ->
feval_term e (Fclos fid tl) (fclos fid vl)
|fcon: forall e n tl vl,
feval_atlist e tl vl ->
feval_term e (Fcon n tl) (fconstr n vl)
|flet: forall e id t1 v1 t2 v2,
feval_term e t1 v1-> var_test_prop id ->
feval_term (PTree.set id v1 e) t2 v2 ->
feval_term e (Flet id t1 t2) v2
|fapp:forall e t1 fid vl targs vargs d e1 v info,
feval_atom e t1 (fclos fid vl) ->
recup_funct fid s = Some d-> varl_test_prop (fun_par d) ->
list_norepet (fun_par d) ->
feval_atlist e targs vargs->
set_local_par (fun_par d) ( (fclos fid vl)::vargs)
(@PTree.empty fval) =Some e1->
feval_term e1 (fun_body d) v ->
(info = None \/ info = Some fid) ->
feval_term e (Fapp info t1 targs) v
|fmatch : forall e a pl n vl xl p e1 v,
feval_atom e a (fconstr n vl) ->
nth_error pl n = Some (FPatc xl p) ->
varl_test_prop xl ->
list_norepet xl ->
set_local_par xl vl e = Some e1->
feval_term e1 p v ->
feval_term e (Fmatch a pl) v.
Inductive feval_list:env->list Fterm->list fval->Prop:=
|fnil: forall e, feval_list e nil nil
|fcons: forall e hd vhd tl vtl,
feval_term e hd vhd ->feval_list e tl vtl->
feval_list e (hd::tl) (vhd::vtl).
End Fsem.
Definition eval_prog (p:fprog) (v:fval):Prop:=
~In xH (List.map (@fst ident funct) (fprog_def p)) /\
~In (Psucc xH) (List.map (@fst ident funct) (fprog_def p)) /\
list_norepet (List.map (@fst ident funct) (fprog_def p)) /\
feval_term (fprog_def p) (@PTree.empty fval) (fprog_main p) v.