Library d2m
Require Import List.
Require Import Coqlib.
Require Import Coqlib2.
Require Import AST.
Require Import Globalenvs.
Require Import Maps.
Require Import Dml.
Require Import Mml.
I. atomization
Inductive atom_case :Set:=
|caseA : atom->atom_case | defaultA :atom_case.
Definition atCase (f:Fterm) :=
match f with | Atom a => caseA a | _ =>defaultA end.
Definition atomize (b :Fterm) (k:atom->Fterm) (id:ident):=
match atCase b with
| caseA a=> k a
| defaultA => (Flet (xI id) b (k (Fvar (xI id))))
end.
Fixpoint atom_list (bl:list Fterm) (args:list atom)
(k:list atom->Fterm) (id:ident) {struct bl}:Fterm:=
match bl with
| nil => k (List.rev args)
| hd::tl => atomize hd (fun a=>(atom_list tl (a::args) k (Psucc id)))
id
end.
Definition atomize_list (bl:list Fterm)
(k:list atom->Fterm) (id:ident):=
atom_list bl nil k id.
II. Smart constructors - atomization contexts
Definition mk_Var (id:ident) := Atom (Fvar (xO id)).
Definition mk_Field (n:nat) (b:Fterm) (lid:ident):=
atomize b (fun a => Atom (Ffield n a)) lid.
Definition mk_Clos (fn:ident) (args:list Fterm) (lid:ident):=
atomize_list args (fun args' => (Fclos fn args')) lid.
Definition mk_App (info:option ident) (b1:Fterm)
(bl:list Fterm) (lid:ident):=
atomize b1 (fun a1 => atomize_list bl (fun al =>
(Fapp info a1 al))(Psucc lid) ) lid.
Definition mk_Con (cstr:nat) (args:list Fterm) (lid:ident):=
atomize_list args (fun args' => (Fcon cstr args')) lid.
Definition mk_Match (b:Fterm) (cases:list fpat) (lid:ident):=
atomize b (fun a => (Fmatch a cases)) lid.
Fixpoint transl (d:Dterm) (lid:ident){struct d}:Fterm*ident:=
match d with
| Dvar n => (mk_Var n,lid)
| Dfield n e =>
let (b,zid):= transl e (Psucc lid) in
(mk_Field n b lid,zid)
| Clos id el =>
let fix transl_list (dl : list Dterm)
(lid:ident) {struct dl}:(list Fterm)*ident:=
match dl with
| nil => (nil, Psucc lid)
| a::m =>
let (b,zid):=transl a (Psucc lid) in
let (l,wid):= (transl_list m zid) in
(b::l,wid)
end
in let (l,zid):= transl_list el (Psucc lid) in
(mk_Clos id l lid,zid)
| Dapp info d1 dl =>
let fix transl_list (dl : list Dterm)
(lid:ident) {struct dl}:(list Fterm)*ident:=
match dl with
| nil => (nil, Psucc lid)
| a::m =>
let (b,zid):=transl a (Psucc lid) in
let (l,wid):= (transl_list m zid) in
(b::l,wid)
end
in let (a,yid):= transl d1 (Psucc lid) in
let (l,zid) := transl_list dl yid in
(mk_App info a l lid, zid)
| Dlet x d1 d2 =>
let (a,yid) := transl d1 (Psucc lid) in
let (b,zid) := transl d2 yid in
(Flet (xO x) a b, zid)
| Dcon n el =>
let fix transl_list (dl : list Dterm)
(lid:ident) {struct dl}:(list Fterm)*ident:=
match dl with
| nil => (nil, Psucc lid)
| a::m =>
let (b,zid):=transl a (Psucc lid) in
let (l,wid):= (transl_list m zid) in
(b::l,wid)
end
in let (l,zid):= transl_list el (Psucc lid) in
(mk_Con n l lid, zid)
| Dmatch d1 pl =>
let fix transl_plist (dl : list dpat)
(lid:ident) {struct dl}:(list fpat)*ident:=
match dl with
| nil => (nil, Psucc lid)
| a::m =>
let (b,yid):= transl_pat a (Psucc lid) in
let (l,zid):= transl_plist m yid in
(( b::l),zid)
end
in
let (a,yid):= transl d1 (Psucc lid) in
let (b,zid):= transl_plist pl yid in
(mk_Match a b lid,zid)
end
with transl_pat (p:dpat) (lid:ident){struct p}:fpat*ident:=
match p with
| DPatc m t =>
let (a,zid):= transl t (Psucc lid) in
(FPatc (map (fun x=>xO x) m) a,zid) end.
Fixpoint transl_list (dl : list Dterm)
(lid:ident) {struct dl}:(list Fterm)*ident:=
match dl with
| nil => (nil, Psucc lid)
| a::m =>
let (b,zid):=transl a (Psucc lid) in
let (l,wid):= (transl_list m zid) in
(b::l,wid)
end .
Fixpoint transl_plist (dl : list dpat)
(lid:ident) {struct dl}:(list fpat)*ident:=
match dl with
| nil => (nil, Psucc lid)
| a::m =>
let (b,yid):= transl_pat a (Psucc lid) in
let (l,zid):= transl_plist m yid in
(( b::l),zid)
end .
Definition transl_def (fn_d:ident*def) :=
let (fn,d):=fn_d in
(fn ,(mkfunct (List.map (fun n=> (xO n)) d.(funct_par))
(fst (transl d.(funct_body) (Psucc xH))))) .
Definition transl_prog (p:prog):=
(mkfprog (fst(transl p.(prog_main) (Psucc xH))) (List.map transl_def p.(prog_def)) ).