Library Cml
EpsilonML language
Author: Zaynah Dargaye
<dargaye@ensiie.fr>
Created: 29th April 2009.
EpsilonML is the source language of MLCompCert. This is the purely functional fragment of ML with De Bruijn indices
Require Import List.
Require Import Coqlib.
Require Import Coqlib2.
Require Import AST.
I. Syntax
Inductive Epsterm:Set :=
| EpsVar : nat -> Epsterm (** de Bruijn indice **)
| EpsLet : Epsterm -> Epsterm -> Epsterm (** let binding **)
| EpsFun : Epsterm -> Epsterm (** curried abstraction **)
| EpsLetrec : Epsterm -> Epsterm -> Epsterm (** recursive function definition **)
| EpsApply : Epsterm -> Epsterm -> Epsterm (** application **)
| EpsEpsonstr : ident -> list Epsterm -> Epsterm (** data type **)
| EpsMatch : Epsterm -> list cpat -> Epsterm (** pattern-matching **)
with cpat :Set :=
| Epsatc : ident -> nat -> Epsterm -> cpat (** pattern **).
Record program :Set:=
mkprogram {
prog_type : list ((list ident)); (** data types definition **)
prog_term : Epsterm (** term **)
}.
II. Semantics de Epsml
Values
Inductive Epsval :Set:=
| EpsClos : list Epsval ->Epsterm ->Epsval (** env, body **)
| EpsClos_rec: list Epsval ->Epsterm ->Epsval
| Epsconstr: ident -> list Epsval -> Epsval (** num ,param**)
.
Data type evaluation
Definition GMenv:= list ((list ident)) .
Fixpoint extract_constr_match (pl : list cpat) {struct pl}: list ident:=
match pl with
| nil => nil
| a::l => match a with
| Epsatc x m t => x::(extract_constr_match l)
end
end.
Definition exists_constr (c:ident) (g:GMenv):Prop:=
exists l , In l g /\ In c l.
Definition wf_match (pl : list cpat) (g:GMenv) :Prop:=
exists l , In l g /\
list_permut_norepet (ident) l (extract_constr_match pl).
Big-step semantics in CBV with environment
Section EpsSEM.
Variable g : GMenv.
Inductive Epseval: list Epsval ->Epsterm->Epsval->Prop:=
| Epseval_var : forall n e v,
nth_error e n = (Some v)-> Epseval e (EpsVar n) v
| Epseval_fun : forall e t , Epseval e (EpsFun t) (EpsEpslos e t)
| Epseval_let : forall e t1 t2 v1 v ,
Epseval e t1 v1 ->
Epseval (v1::e) t2 v ->
Epseval e (EpsLet t1 t2) v
| Epseval_letrec : forall e t1 t2 v,
Epseval ((EpsClos_rec e t1)::e) t2 v ->
Epseval e (EpsLetrec t1 t2) v
| Epseval_app : forall e e' t t1 t2 v v2,
Epseval e t1 (EpsClos e' t) ->
Epseval e t2 v2 ->
Epseval (v2::e') t v ->
Epseval e (EpsApply t1 t2) v
| Epseval_appr : forall e e' t t1 t2 v v2,
Epseval e t1 (EpsClos_rec e' t) ->
Epseval e t2 v2 ->
Epseval (v2::(EpsClos_rec e' t)::e') t v ->
Epseval e (EpsApply t1 t2) v
| Epseval_constr : forall e tl vl n ,
exists_constr n g ->
Epseval_list e tl vl ->
Epseval e (EpsConstr n tl) (Epsconstr n vl)
| Epseval_match : forall e t c pl vl m tn v,
Epseval e t (Epsconstr c vl) ->
wf_match pl g ->
In (Epsatc c m tn) pl ->
length vl = m ->
Epseval ((rev vl)++e) tn v ->
Epseval e (EpsMatch t pl) v
with
Epseval_list : list Epsval->list Epsterm-> list Epsval ->Prop:=
| Epseval_nil : forall e , Epseval_list e nil nil
| Epseval_cons : forall e t lt v lv ,
Epseval e t v ->
Epseval_list e lt lv ->
Epseval_list e (t::lt) (v::lv)
.
End EpsSEM.
Scheme ceval_term_ind6 := Minimality for Epseval Sort Prop
with ceval_terml_ind6 := Minimality for Epseval_list Sort Prop.
A program evaluation
Inductive eval_prog :program->Epsval->Prop:=
| intro_eval_prg :
forall p v,
list_norepet p.(prog_type) ->
(forall l , In l p.(prog_type) -> list_norepet l) ->
(forall l1 l2, l1<>l2 -> In l1 p.(prog_type) ->
In l2 p.(prog_type) -> list_disjoint l1 l2) ->
Epseval p.(prog_type) (@nil Epsval) p.(prog_term) v ->
eval_prog p v.