Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.

The motivations are:

- To reflect the concrete syntax more closely.
- To factorize the different places where "contexts" are internalized:
  before this patch, there is a different treatment of `Definition f
  '(x,y) := x+y` and `Definition f := fun '(x,y) => x+y`, and a hack
  to interpret `Definition f `pat := c : t`. With the patch, the fix
  to avoid seeing a variable named `pat` works for both `fun 'x =>
  ...` and `Definition f 'x := ...`.

The drawbacks are:

- Counterpart to reflecting the concrete syntax more closerly, there
  are more redundancies in the syntax. For instance, the case `CLetIn
  (na,b,t,c)` can appears also in the form `CProdN (CLocalDef
  (na,b,t)::rest,d)` and `CLambdaN (CLocalDef (na,b,t)::rest,d)`.
- Changes in the API, hence adaptation of plugins referring to `constr_expr` needed.

1 files changed, 2 insertions, 66 deletions

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 1146b42a0..c58d9eb9a 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -394,68 +394,6 @@ let tag_var = tag Tag.variable
     if is_open then pr_delimited_binders pr_com_at sep pr_c
     else pr_undelimited_binders sep pr_c
 
-  let rec extract_prod_binders = let open CAst in function
-  (*  | CLetIn (loc,na,b,c) as x ->
-      let bl,c = extract_prod_binders c in
-      if bl = [] then [], x else CLocalDef (na,b) :: bl, c*)
-    | { v = CProdN ([],c) } ->
-      extract_prod_binders c
-    | { loc; v = CProdN ([[_,Name id],bk,t],
-              { v = CCases (LetPatternStyle,None, [{ v = CRef (Ident (_,id'),None)},None,None],[(_,([[p]],b))])} ) }
-         when Id.equal id id' && not (Id.Set.mem id (free_vars_of_constr_expr b)) ->
-      let bl,c = extract_prod_binders b in
-      CLocalPattern (loc, (p,None)) :: bl, c
-    | { loc; v = CProdN ((nal,bk,t)::bl,c) } ->
-      let bl,c = extract_prod_binders (CAst.make ?loc @@ CProdN(bl,c)) in
-      CLocalAssum (nal,bk,t) :: bl, c
-    | c -> [], c
-
-  let rec extract_lam_binders ce = let open CAst in match ce.v with
-  (*  | CLetIn (loc,na,b,c) as x ->
-      let bl,c = extract_lam_binders c in
-      if bl = [] then [], x else CLocalDef (na,b) :: bl, c*)
-    | CLambdaN ([],c) ->
-      extract_lam_binders c
-    | CLambdaN ([[_,Name id],bk,t],
-                { v = CCases (LetPatternStyle,None, [{ v = CRef (Ident (_,id'),None)},None,None],[(_,([[p]],b))])} )
-         when Id.equal id id' && not (Id.Set.mem id (free_vars_of_constr_expr b)) ->
-      let bl,c = extract_lam_binders b in
-      CLocalPattern (ce.loc,(p,None)) :: bl, c
-    | CLambdaN ((nal,bk,t)::bl,c) ->
-      let bl,c = extract_lam_binders (CAst.make ?loc:ce.loc @@ CLambdaN(bl,c)) in
-      CLocalAssum (nal,bk,t) :: bl, c
-    | _ -> [], ce
-
-  let split_lambda = CAst.with_loc_val (fun ?loc -> function
-    | CLambdaN ([[na],bk,t],c) -> (na,t,c)
-    | CLambdaN (([na],bk,t)::bl,c) -> (na,t, CAst.make ?loc @@ CLambdaN(bl,c))
-    | CLambdaN ((na::nal,bk,t)::bl,c) -> (na,t, CAst.make ?loc @@ CLambdaN((nal,bk,t)::bl,c))
-    | _ -> anomaly (Pp.str "ill-formed fixpoint body.")
-    )
-
-  let rename na na' t c =
-    match (na,na') with
-      | (_,Name id), (_,Name id') ->
-        (na',t,replace_vars_constr_expr (Id.Map.singleton id id') c)
-      | (_,Name id), (_,Anonymous) -> (na,t,c)
-      | _ -> (na',t,c)
-
-  let split_product na' = CAst.with_loc_val (fun ?loc -> function
-    | CProdN ([[na],bk,t],c) -> rename na na' t c
-    | CProdN (([na],bk,t)::bl,c) -> rename na na' t (CAst.make ?loc @@ CProdN(bl,c))
-    | CProdN ((na::nal,bk,t)::bl,c) ->
-      rename na na' t (CAst.make ?loc @@ CProdN((nal,bk,t)::bl,c))
-    | _ -> anomaly (Pp.str "ill-formed fixpoint body.")
-    )
-
-  let rec split_fix n typ def =
-    if Int.equal n 0 then ([],typ,def)
-    else
-      let (na,_,def) = split_lambda def in
-      let (na,t,typ) = split_product na typ in
-      let (bl,typ,def) = split_fix (n-1) typ def in
-      (CLocalAssum ([na],default_binder_kind,t)::bl,typ,def)
-
   let pr_recursive_decl pr pr_dangling dangling_with_for id bl annot t c =
     let pr_body =
       if dangling_with_for then pr_dangling else pr in
@@ -574,8 +512,7 @@ let tag_var = tag Tag.variable
                    (pr_cofixdecl (pr mt) (pr_dangling_with_for mt pr)) (snd id) cofix),
           lfix
         )
-      | CProdN _ ->
-        let (bl,a) = extract_prod_binders a in
+      | CProdN (bl,a) ->
         return (
           hov 0 (
             hov 2 (pr_delimited_binders pr_forall spc
@@ -583,8 +520,7 @@ let tag_var = tag Tag.variable
               str "," ++ pr spc ltop a),
           lprod
         )
-      | CLambdaN _ ->
-        let (bl,a) = extract_lam_binders a in
+      | CLambdaN (bl,a) ->
         return (
           hov 0 (
             hov 2 (pr_delimited_binders pr_fun spc