Library f2d
Closure conversion : 4th transformation of MLCompCert
Author : Zaynah Dargaye
Created: 29th April 2009
Require Import Coqlib.
Require Import Coqlib2.
Require Import AST.
Require Import Globalenvs.
Require Import Maps.
Require Import Compare_dec.
Require Import EqNat.
Require Import Fml.
Require Import Dml.
I. Free variables computation of Nml terms
Fixpoint notin (n:nat) (l:list nat) {struct l}:bool:=
match l with
| nil => true
| a::m => if (beq_nat n a) then false else (notin n m)
end.
Definition add (n:nat) (l:list nat) :=
if (notin n l ) then n::l else l.
Fixpoint var_free (n:nat) (vf : list nat) (t:term) {struct t}:list nat:=
match t with
| Var m => if ( le_gt_dec n m ) then (add (minus m n) vf) else vf
| tLet t1 t2 => var_free (S n) (var_free n vf t1) t2
| Lamb m t1 => var_free (plus n (S m)) vf t1
| Mu m t1 => var_free (plus n (S (S m))) vf t1
| App t1 t2 =>
let fix var_free_list (n:nat) (vf: list nat) (l:list term) {struct l}:=
match l with
| nil => vf
| a::m => var_free_list n (var_free n vf a) m
end
in
var_free_list n (var_free n vf t1) t2
| Con k ln =>
let fix var_free_list (n:nat) (vf: list nat) (l:list term) {struct l}:=
match l with
| nil => vf
| a::m => var_free_list n (var_free n vf a) m
end
in
var_free_list n vf ln
| Match t1 lpat =>
let fix var_free_pat_list (n:nat) (vf: list nat) (l:list pat) {struct l}:=
match l with
| nil => vf
| a::m => var_free_pat_list n (var_free_pat n vf a) m
end
in
var_free_pat_list n (var_free n vf t1) lpat
end
with var_free_pat (n:nat) (vf:list nat) (p:pat) {struct p}:list nat :=
match p with
| Patc m t => var_free (plus n m ) vf t
end.
Fixpoint var_free_list (n:nat) (vf: list nat) (l:list term) {struct l}:list nat:=
match l with
| nil => vf
| a::m => var_free_list n (var_free n vf a) m
end.
Fixpoint var_free_pat_list (n:nat) (vf: list nat) (l:list pat) {struct l}:list nat:=
match l with
| nil => vf
| a::m => var_free_pat_list n (var_free_pat n vf a) m
end.
II. Translation environments
Inductive var_info:Set:=
| Var_var : ident->var_info
| Var_field : ident ->nat->var_info.
Definition fun_info := option ident.
Definition var_env := list (nat*var_info).
Definition fun_env := list fun_info .
Fixpoint recup (n:nat) (env:var_env ) {struct env}:option var_info:=
match env with
| nil => None
| (k,info)::m =>
if (beq_nat k n) then Some info else recup n m
end.
Definition shift_var_info (delta : nat) ( i_info : nat*var_info) :=
let (m, info) := i_info in (m + delta, info).
III. Translation of variables
Definition transf_var (cenv:var_env) (n:nat) :=
match recup n cenv with
| Some a => match a with
| Var_var n0 => Some (Dvar n0)
| Var_field n0 pos => Some (Dfield (S pos) (Dvar n0)) end
| None =>None end.
Fixpoint transf_varl (ce:var_env) (n:list nat) {struct n}:option (list Dterm) :=
match n with
| nil => Some nil
|a::m =>match transf_var ce a with | None=>None
| Some va => match transf_varl ce m with | None =>None
|Some vm => Some (va::vm) end
end
end.
IV. function optimisation
Definition known_app (fenv: fun_env) (a:term):=
match a with
| Var n => match nth_error fenv n with
| None => None | Some x=> x end
| _ => None
end.
V. The state monads for closure conversion, naming variables and functions
Definition functions := list (ident *def).
Inductive res (A: Set) : Set :=
| Error: res A
| OK: A -> functions -> ident ->ident -> res A.
Definition mon (A: Set) : Set := functions ->ident -> ident -> res A.
Definition ret (A: Set) (x: A) : mon A := fun (s: functions) =>
fun (fid:ident) => fun (vid : ident )=> OK x s fid vid .
Definition error (A: Set) : mon A := fun (s: functions) =>
fun (fid:ident) =>fun (vid:ident) =>Error A.
Definition bind (A B: Set) (f: mon A) (g: A -> mon B) : mon B :=
fun (s: functions) =>
fun (fid:ident) => fun (vid : ident) =>
match f s fid vid with
| Error => Error B
| OK a s' fid vid => g a s' fid vid
end.
Definition add_fundef (fundef:def):=
fun (defs: functions) =>
fun (fid:ident) => fun (vid:ident) =>
ret fid ((fid,fundef)::defs) (Psucc fid) vid.
Definition add_fundef_rec (fundef:def) (fname:ident):=
fun (defs: functions) =>
fun (fid:ident) => fun (vid:ident) =>
ret fid ((fname,fundef)::defs) (Psucc fid) vid.
Definition ident_vars_add_vars (arity : nat):=
fun (s :functions) => fun (fid : ident) => fun (vid:ident) =>
ret vid s fid (Pplus vid (P_of_succ_nat arity)).
Definition ident_vars_add_var :=
fun (s :functions) => fun (fid : ident) => fun (vid:ident) =>
ret vid s fid (Psucc vid).
Definition next_fun :=
fun (s :functions) => fun (fid : ident) => fun (vid:ident) =>
ret fid s (Psucc fid) vid.
Notation "'do' X <- A ; B" := (bind A (fun X => B))
(at level 200, X ident, A at level 100, B at level 200).
VI. Translation environments manipulations
Fixpoint cenv_params (arity : nat) (vid:ident)
(ce:var_env) {struct arity}:var_env:=
match arity with
| O =>ce
| S m => cenv_params m (Psucc vid)
((0, Var_var (Psucc vid))::List.map (shift_var_info 1) ce)
end.
Definition cenv_let (cenv: var_env) (id:ident):=
((0, Var_var id) :: List.map (shift_var_info 1) cenv).
Fixpoint fenv_params (arity:nat) (fenv:fun_env) {struct arity}:fun_env:=
match arity with | O => fenv | S m => None :: fenv_params m fenv end.
Definition fenv_match (arity:nat) (fenv:fun_env):=
fenv_params arity fenv.
Definition fenv_let (fenv:fun_env) (lhs:Dterm) :=
match lhs with
| Clos fid _ => Some fid :: fenv
| _ => None :: fenv
end.
Definition fenv_fun (arity:nat) (fenv:fun_env):= fenv_params arity fenv.
Definition fenv_recfun (fid:ident) (arity:nat) (fenv:fun_env):=
fenv_params arity (Some fid::fenv).
Definition cenv_match (arity : nat) (vid:ident) (ce:var_env):=
cenv_params arity vid (List.map (shift_var_info arity) ce).
Fixpoint cenv_fv (env:ident) (pos:nat) (freevars: list nat)
{struct freevars}:var_env:=
match freevars with
|nil => nil
|v::lv => (v , (Var_field env pos))::
(cenv_fv env (pos+1) lv)
end.
Definition cenv_freevars (env:ident) (freevars:list nat) :=
cenv_fv env 0 freevars.
Fixpoint names_params (arity:nat) (vid:ident) {struct arity}:list ident :=
match arity with
| O => nil
| S m => (Psucc vid) :: names_params m (Psucc vid)
end.
Definition cenv_fun (arity:nat) (freevars:list nat) (env:ident):=
(cenv_params arity env
(cenv_freevars env freevars)) .
Definition cenv_recfun (arity:nat) (freevars:list nat) (env:ident):=
(cenv_params arity env
((0,Var_var env)::(List.map (shift_var_info 1)
(cenv_freevars env freevars)))) .
Definition cenv_case (arity:nat) (ce:var_env) (env:ident):=
(cenv_params arity env ce).
VII. Closure conversion of a Nml for substitution term
Fixpoint transf (cenv:var_env) (fenv :fun_env) (t:term) {struct t}:mon Dterm:=
match t with
| Var n =>
match transf_var cenv n with
| None =>error Dterm
| Some t => ret t
end
|Lamb arity body =>
let freevars := (var_free (S arity) nil body) in
do env<-ident_vars_add_vars (S arity);
do tbody<-transf ( cenv_fun (S arity) freevars env) (fenv_fun (S arity) fenv ) body;
let fdef:= (mkdef (env::(names_params (S arity) env)) tbody) in
(do fname<-add_fundef fdef;
match transf_varl cenv freevars with
| None =>error Dterm
| Some tl => ret (Clos fname tl)
end )
| Mu arity body =>
let freevars := (var_free (S (S arity)) nil body) in
do env<- ident_vars_add_vars (S arity);
do fname1<-next_fun;
do tbody<-transf (cenv_recfun (S arity) freevars env ) (fenv_recfun fname1 (S arity) fenv ) body;
let fdef:= (mkdef (env::(names_params (S arity) env)) tbody) in
do fn <-add_fundef_rec fdef fname1;
match transf_varl cenv freevars with
| None =>error Dterm
| Some tl => ret (Clos fname1 tl)
end
|App t1 tl =>
do d1<- transf cenv fenv t1 ;
(let fix transf_list (cenv:var_env) (fenv:fun_env)
(tl:list term) {struct tl}:mon (list Dterm):=
match tl with
| nil =>ret nil
| a::m => do da<-transf cenv fenv a ;
do dm <-transf_list cenv fenv m;
ret (da::dm)
end
in do dl<-transf_list cenv fenv tl;
ret (Dapp (known_app fenv t1) d1 dl))
|Con n tl =>
(let fix transf_list (cenv:var_env) (fenv:fun_env)
(tl:list term) {struct tl}:mon (list Dterm):=
match tl with
| nil =>ret nil
| a::m => do da<-transf cenv fenv a ;
do dm <-transf_list cenv fenv m;
ret (da::dm)
end
in do dl<-transf_list cenv fenv tl;
ret (Dcon n dl))
|tLet a b =>
do da<-transf cenv fenv a;
do id<- ident_vars_add_var;
do db<- transf (cenv_let cenv id) ( fenv_let fenv da) b;
ret (Dlet id da db)
| Match a pl =>
do da<-transf cenv fenv a;
(let fix transf_plist (cenv:var_env) (fenv:fun_env)
(pl:list pat) {struct pl}: mon (list dpat):=
match pl with
| nil => ret nil
| a::m => do da<- transf_pat cenv fenv a;
do dm<-transf_plist cenv fenv m;
ret (da::dm)
end
in do dpl<-transf_plist cenv fenv pl;
ret (Dmatch da dpl) )
end
with transf_pat (cenv:var_env) (fenv:fun_env) (p:pat) {struct p}:mon dpat:=
match p with
|Patc arity a =>
do env<- ident_vars_add_vars ( arity);
do da<-transf (cenv_case ( arity) cenv env ) (fenv_match ( arity) fenv) a ;
ret (DPatc (names_params ( arity) env) da)
end.
Fixpoint transf_list (cenv:var_env) (fenv:fun_env)
(tl:list term) {struct tl}:mon (list Dterm):=
match tl with
| nil =>ret nil
| a::m => do da<-transf cenv fenv a ;
do dm <-transf_list cenv fenv m;
ret (da::dm)
end.
Fixpoint transf_plist (cenv:var_env) (fenv:fun_env)
(pl:list pat) {struct pl}: mon (list dpat):=
match pl with
| nil => ret nil
| a::m => do da<- transf_pat cenv fenv a;
do dm<-transf_plist cenv fenv m;
ret (da::dm)
end .
VIII. Closure conversion of a program
Definition transf_program (p:term):=
match (transf nil nil p nil (Psucc (Psucc xH)) (Psucc xH)) with
| OK d s _ _ => Some ( mkprog d s)
| _ => None
end.