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:=
   fun_par : list ident ;
   fun_body : Fterm

Record fprog :Set:=
    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

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

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

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 ( (@fst ident funct) (fprog_def p)) /\
 ~In (Psucc xH) ( (@fst ident funct) (fprog_def p)) /\
 list_norepet ( (@fst ident funct) (fprog_def p)) /\
 feval_term (fprog_def p) (@PTree.empty fval) (fprog_main p) v.