Library Dml

Fml the 5th intermediate language of MLCompCert

Author : Zaynah Dargaye

Created: 29th April 2009

miniML organised into global functions and within explicit minimal closures in terms; variables are named.

Require Import Coqlib.
Require Import Coqlib2.
Require Import AST.
Require Import Globalenvs.
Require Import Maps.

Open Scope nat_scope.


Inductive Dterm:Set:=
|Dvar : ident -> Dterm
|Dfield : nat->Dterm ->Dterm
|Clos : ident-> list Dterm-> Dterm
|Dapp : option ident -> Dterm-> list Dterm->Dterm
|Dcon : nat->list Dterm->Dterm
|Dlet : ident -> Dterm->Dterm->Dterm
|Dmatch: Dterm-> list dpat ->Dterm
with dpat:Set:=
|DPatc : list ident -> Dterm->dpat.

Record def :Set:=
   funct_par : list ident ;
   funct_body : Dterm

Record prog :Set:=
    prog_main : Dterm ;
    prog_def : list (ident * def)
 } .

II. Big-step semantics CBV with environment and a global state (the program list of global functions)

Fixpoint recup_fun (id:ident) (s:list (ident*def)) {struct s}:option def:=
 match s with
 |nil => None
 |(id1,d1)::l => if (peq id id1) then Some d1 else recup_fun id l

Inductive dval:Set:=
 |dclos : ident->list dval -> dval
 |dconstr: nat->list dval -> dval .

Definition env:= PTree.t dval.

Fixpoint set_local_par (xl:list ident) (vl:list dval)
    (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

Section Dsem.

Variable s: list (ident*def).

Inductive deval_term:env->Dterm->dval->Prop:=
|dvar: forall e id v , id <> xH ->
   PTree.get id e =Some v -> deval_term e (Dvar id) v
|dfield : forall e n fid t vl v,
     deval_term e t (dclos fid vl) ->
    nth_error vl n=Some v->
    deval_term e (Dfield (S n) t) v
| dClos: forall e fid tl vl d,
       recup_fun fid s = Some d ->
       deval_list e tl vl ->
       deval_term e (Clos fid tl) (dclos fid vl)
|dcon: forall e n tl vl,
       deval_list e tl vl -> deval_term e (Dcon n tl) (dconstr n vl)
|dlet: forall e id t1 v1 t2 v2,
       deval_term e t1 v1-> id<>xH ->
       deval_term (PTree.set id v1 e) t2 v2 ->
       deval_term e (Dlet id t1 t2) v2
|dapp:forall e t1 fid vl targs vargs d e1 v info,
       deval_term e t1 (dclos fid vl) ->
       recup_fun fid s = Some d->
       deval_list e targs vargs->
       list_norepet (funct_par d) ->
       (forall x, In x (funct_par d) -> x<>xH) ->
       set_local_par (funct_par d) ( (dclos fid vl)::vargs)
           (@PTree.empty dval) =Some e1->
       deval_term e1 (funct_body d) v ->
       (info = None \/ info = Some fid) ->
       deval_term e (Dapp info t1 targs) v
|dmatch : forall e a pl n vl xl p e1 v,
       deval_term e a (dconstr n vl) ->
       nth_error pl n = Some (DPatc xl p) ->
       (forall x, In x xl-> x<>xH) ->
       list_norepet xl ->
       set_local_par xl vl e = Some e1->
       deval_term e1 p v ->
       deval_term e (Dmatch a pl) v
with deval_list:env->list Dterm->list dval->Prop:=
|dnil: forall e, deval_list e nil nil
|dcons: forall e hd vhd tl vtl,
    deval_term e hd vhd ->deval_list e tl vtl->
    deval_list e (hd::tl) (vhd::vtl).

End Dsem.

Definition eval_prog (p:prog) (v:dval):Prop:=
 ~In xH ( (@fst ident def) (prog_def p)) /\
 ~In (Psucc xH) ( (@fst ident def) (prog_def p)) /\
 list_norepet ( (@fst ident def) (prog_def p)) /\
 deval_term (prog_def p) (@PTree.empty dval) (prog_main p) v.