Library p2n
Uncurrying : second transformation of MLCompCert
Author : Zaynah Dargaye
<dargaye@ensiie.fr>
Creadted : 29th April 2009
First order uncurrying, same optimisation as in OCaml compiler
Require Import List.
Require Import Coqlib.
Require Import AST.
Require Import Pml.
Require Import Nml.
I. Static analysis
Inductive arity: Set :=
| Unknown: arity
| Known: nat -> arity .
Definition cenv := list arity .
Fixpoint Unknown_n (n: nat) (ce: cenv) {struct n} : cenv :=
match n with O => ce
| S m => Unknown :: Unknown_n m ce end.
II. Currying combinators
Fixpoint NLam_n (n: nat) (a: Nterm) {struct n} : Nterm :=
match n with O => a | S m => NFun O (NLam_n m a) end.
Fixpoint ncurry_args (n: nat) : list Nterm :=
match n with O => nil | S n' => NVar n' :: ncurry_args n' end.
Definition ncurry_body (n: nat) : Nterm :=
NApply (NVar (S n)) (ncurry_args (S n)).
Definition ncurry_term (n: nat) : Nterm :=
NFun 0 (NLam_n (S n) (ncurry_body n)).
Definition NCurry_opt (n: nat) (a: Nterm) : Nterm :=
match n with O => a | _ => (NApply (ncurry_term n) (a::nil)) end.
III. Variable translation
Definition trad_var (n:nat) (ce:cenv) : Nterm:=
match (List.nth_error ce n) with
| Some (Known ar) => (NCurry_opt ar (NVar n))
| _ => NVar n
end.
IV. Uncurrying of applications
Definition var_has_arity (ce: cenv) (v: nat) (ar: nat) : bool :=
match List.nth_error ce v with
| None => false
| Some Unknown => false
| Some (Known n) => if eq_nat_dec n ar then true else false
end.
Inductive cur_app:Set:=
| unary : cur_app
| nary : nat-> (list Nterm)->cur_app.
V. Implemantation of the uncurrying (functional version)
Fixpoint trad (t: PMterm) (ce:cenv) {struct t}: Nterm:=
match t with
| TVar n => trad_var n ce
| TLet t1 t2 =>
let fix uncurry (tf : PMterm) (ce:cenv) (n:nat) {struct tf}:=
match tf with
| TFun t1 => uncurry t1 ce (S n)
| _ => (n, NFun n (trad tf (Unknown_n (S n) ce)) )
end
in
match t1 with
| TFun a => let (n,t) := (uncurry a ce O) in
NLet t (trad t2 ((Known n)::ce))
| _ => NLet (trad t1 ce) (trad t2 (Unknown::ce))
end
| TFun t1 => NFun O (trad t1 (Unknown::ce))
| TLetrec t1 t2 =>
let fix uncurry_rec (tf : PMterm) (ce:cenv) (n:nat) {struct tf}:=
match tf with
| TFun t1 => uncurry_rec t1 ce (S n)
| _ => (S n, (trad tf (Unknown_n (S (S n)) (Known (S n)::ce))))
end
in
match t1 with
| TFun a => let (n,t):= (uncurry_rec a ce O) in
NLetrec n t (trad t2 ((Known n)::ce))
| _ => NLetrec O (trad t1 (Unknown::Unknown::ce)) (trad t2 (Unknown::ce))
end
| TApply t1 t2 =>
let fix app_curried
(ce: cenv) (a: PMterm) (args: list Nterm) {struct a}
: cur_app :=
match a with
| TVar n =>
if var_has_arity ce n (List.length args)
then (nary n args) else unary
| TApply a1 a2 =>
app_curried ce a1 ((trad a2 ce) :: args)
| _ => unary
end
in
match (app_curried ce t1 nil) with
| unary => (NApply (trad t1 ce) ((trad t2 ce)::nil))
| nary n args => (NApply (NVar n) (args++(trad t2 ce)::nil))
end
| TConstr n tl =>
let fix trad_list (tl:list PMterm) (ce:cenv) {struct tl}:=
match tl with
| nil => nil
| t::l => (trad t ce)::(trad_list l ce)
end in
NConstr n (trad_list tl ce)
| TMatch t pl =>
let trad_pat (p : pat) (ce : cenv) :=
match p with
| Patc n t => NPatc n (trad t (Unknown_n n ce))
end in
let fix trad_pat_list (pl : list pat) (ce:cenv) {struct pl}:=
match pl with
| nil => nil
| p::l => (trad_pat p ce)::(trad_pat_list l ce)
end in
NMatch (trad t ce) (trad_pat_list pl ce)
end.
VI. The uncurrying relationnal version
Fixpoint Runcurry_rec
(tf : PMterm) (n:nat) {struct tf}:nat*PMterm:=
match tf with
| TFun t1 => Runcurry_rec t1 (S n)
| _ => (n, tf)
end.
Definition Runcurry (tf : PMterm) :=
match tf with
| TFun t1 => Some(Runcurry_rec t1 O)
| _ => None
end.
Inductive Rcur_app:Set:=
| Runary : Rcur_app
| Rnary : nat-> (list PMterm)->Rcur_app.
Fixpoint Rapp_curried
(ce:cenv) (a: PMterm) (args: list PMterm) {struct a}: Rcur_app :=
match a with
| TVar n =>
if var_has_arity ce n (List.length args)
then (Rnary n args) else Runary
| TApply a1 a2 =>
Rapp_curried ce a1 (a2:: args)
| _ => Runary
end.
Inductive transl: cenv->PMterm ->Nterm -> Prop:=
| transl_var_other : forall n ce,
(nth_error ce n = None \/ nth_error ce n = Some Unknown) ->
transl ce (TVar n) (NVar n)
| transl_var_known : forall n ce ar,
nth_error ce n = Some (Known ar) ->
transl ce (TVar n) (NCurry_opt ar (NVar n))
| transl_fun : forall t n ce,
transl (Unknown::ce) t n -> transl ce (TFun t) (NFun O n)
| transl_let_default : forall t1 t2 n1 n2 ce,
Runcurry t1 = None ->
transl ce t1 n1 -> transl (Unknown::ce) t2 n2 ->
transl ce (TLet t1 t2) (NLet n1 n2)
| transl_let_fun: forall t1 t2 t n n2 ce ar,
Runcurry t1 = Some (ar, t) ->
transl ( Unknown_n (S ar) ce) t n -> transl ( (Known ar)::ce) t2 n2->
transl ce (TLet t1 t2) (NLet (NFun ar n) n2)
| transl_letrec_default:forall t1 t2 n1 n2 ce,
Runcurry t1 = None ->
transl (Unknown::Unknown::ce) t1 n1 ->
transl (Unknown::ce) t2 n2 ->
transl ce (TLetrec t1 t2) (NLetrec O n1 n2)
| transl_letrec_fun : forall t1 ar t n t2 n2 ce,
Runcurry t1 = Some (ar, t) ->
transl ( Unknown_n (S(S ar)) (Known (S ar)::ce)) t n ->
transl ( (Known (S ar))::ce) t2 n2->
transl ce (TLetrec t1 t2) (NLetrec (S ar) n n2)
| transl_app_un : forall t1 n1 t2 n2 ce,
Rapp_curried ce t1 nil = Runary ->
transl ce t1 n1 -> transl ce t2 n2 ->
transl ce (TApply t1 t2) (NApply n1 (n2::nil))
| transl_app_n: forall t1 n args nargs t2 n2 ce,
Rapp_curried ce t1 nil = Rnary n args ->
transl_list ce args nargs ->
transl ce t2 n2 ->
transl ce (TApply t1 t2) (NApply (NVar n) (nargs++n2::nil) )
| transl_constr: forall n pl npl ce ,
transl_list ce pl npl -> transl ce (TConstr n pl) (NConstr n npl)
| transl_match : forall ce t n pl npl ,
transl ce t n -> transl_pat_list ce pl npl ->
transl ce (TMatch t pl) (NMatch n npl)
with
transl_pat : cenv->pat->npat->Prop:=
| transl_Patc : forall ce m t n ,
transl (Unknown_n m ce) t n ->
transl_pat ce (Patc m t) (NPatc m n)
with transl_pat_list : cenv->list pat -> list npat -> Prop:=
| transl_pnil: forall ce, transl_pat_list ce nil nil
| transl_pcons: forall ce p np pl npl,
transl_pat ce p np -> transl_pat_list ce pl npl ->
transl_pat_list ce (p::pl) (np::npl)
with
transl_list : cenv->list PMterm -> list Nterm -> Prop:=
| transl_nil : forall ce, transl_list ce nil nil
| transl_cons : forall thd ttl nhd ntl ce,
transl ce thd nhd -> transl_list ce ttl ntl ->
transl_list ce (thd::ttl) (nhd::ntl).
Scheme transl_ind6 := Minimality for transl Sort Prop
with transl_pat_ind6 := Minimality for transl_pat Sort Prop
with transl_pat_list_ind6 := Minimality for transl_pat_list Sort Prop
with transl_list_ind6 := Minimality for transl_list Sort Prop.