Library p2n

Uncurrying : second transformation of MLCompCert

Author : Zaynah Dargaye <>

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

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

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)) )
      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))
  | 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))))
      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))
  | 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
     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))
 | 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)


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)

Definition Runcurry (tf : PMterm) :=
 match tf with
 | TFun t1 => Some(Runcurry_rec t1 O)
 | _ => None

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

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)
 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)
 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.