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.