``` ```

# 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. ```