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.

3 files changed, 78 insertions, 115 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index da04d8786..9fe890e90 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -112,10 +112,10 @@ let rec constr_expr_eq e1 e2 =
       eq_located Id.equal id1 id2 &&
       List.equal cofix_expr_eq fl1 fl2
     | CProdN(bl1,a1), CProdN(bl2,a2) ->
-      List.equal binder_expr_eq bl1 bl2 &&
+      List.equal local_binder_eq bl1 bl2 &&
       constr_expr_eq a1 a2
     | CLambdaN(bl1,a1), CLambdaN(bl2,a2) ->
-      List.equal binder_expr_eq bl1 bl2 &&
+      List.equal local_binder_eq bl1 bl2 &&
       constr_expr_eq a1 a2
     | CLetIn((_,na1),a1,t1,b1), CLetIn((_,na2),a2,t2,b2) ->
       Name.equal na1 na2 &&
@@ -193,10 +193,6 @@ and branch_expr_eq (_, (p1, e1)) (_, (p2, e2)) =
   List.equal (List.equal cases_pattern_expr_eq) p1 p2 &&
   constr_expr_eq e1 e2
 
-and binder_expr_eq ((n1, _, e1) : binder_expr) (n2, _, e2) =
-  (** Don't care about the [binder_kind] *)
-  List.equal (eq_located Name.equal) n1 n2 && constr_expr_eq e1 e2
-
 and fix_expr_eq (id1,(j1, r1),bl1,a1,b1) (id2,(j2, r2),bl2,a2,b2) =
   (eq_located Id.equal id1 id2) &&
   Option.equal (eq_located Id.equal) j1 j2 &&
@@ -307,14 +303,6 @@ let ids_of_cases_tomatch tms =
          (Option.fold_right (down_located (Name.fold_right Id.Set.add)) ona l))
     tms Id.Set.empty
 
-let rec fold_constr_expr_binders g f n acc b = function
-  | (nal,bk,t)::l ->
-    let nal = snd (List.split nal) in
-    let n' = List.fold_right (Name.fold_right g) nal n in
-    f n (fold_constr_expr_binders g f n' acc b l) t
-  | [] ->
-    f n acc b
-
 let rec fold_local_binders g f n acc b = function
   | CLocalAssum (nal,bk,t)::l ->
     let nal = snd (List.split nal) in
@@ -331,7 +319,7 @@ let rec fold_local_binders g f n acc b = function
 let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
     | CAppExpl ((_,_,_),l) -> List.fold_left (f n) acc l
     | CApp ((_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l)
-    | CProdN (l,b) | CLambdaN (l,b) -> fold_constr_expr_binders g f n acc b l
+    | CProdN (l,b) | CLambdaN (l,b) -> fold_local_binders g f n acc b l
     | CLetIn (na,a,t,b) ->
       f (Name.fold_right g (snd na) n) (Option.fold_left (f n) (f n acc a) t) b
     | CCast (a,(CastConv b|CastVM b|CastNative b)) -> f n (f n acc a) b
@@ -382,12 +370,6 @@ let occur_var_constr_expr id c = Id.Set.mem id (free_vars_of_constr_expr c)
 (* Used in correctness and interface *)
 let map_binder g e nal = List.fold_right (down_located (Name.fold_right g)) nal e
 
-let map_binders f g e bl =
-  (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *)
-  let h (e,bl) (nal,bk,t) = (map_binder g e nal,(nal,bk,f e t)::bl) in
-  let (e,rbl) = List.fold_left h (e,[]) bl in
-  (e, List.rev rbl)
-
 let map_local_binders f g e bl =
   (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *)
   let h (e,bl) = function
@@ -406,9 +388,9 @@ let map_constr_expr_with_binders g f e = CAst.map (function
     | CApp ((p,a),l) ->
       CApp ((p,f e a),List.map (fun (a,i) -> (f e a,i)) l)
     | CProdN (bl,b) ->
-      let (e,bl) = map_binders f g e bl in CProdN (bl,f e b)
+      let (e,bl) = map_local_binders f g e bl in CProdN (bl,f e b)
     | CLambdaN (bl,b) ->
-      let (e,bl) = map_binders f g e bl in CLambdaN (bl,f e b)
+      let (e,bl) = map_local_binders f g e bl in CLambdaN (bl,f e b)
     | CLetIn (na,a,t,b) ->
       CLetIn (na,f e a,Option.map (f e) t,f (Name.fold_right g (snd na) e) b)
     | CCast (a,c) -> CCast (f e a, Miscops.map_cast_type (f e) c)
@@ -529,9 +511,9 @@ let split_at_annot bl na =
 let mkIdentC id   = CAst.make @@ CRef (Ident (Loc.tag id),None)
 let mkRefC r      = CAst.make @@ CRef (r,None)
 let mkCastC (a,k) = CAst.make @@ CCast (a,k)
-let mkLambdaC (idl,bk,a,b) = CAst.make @@ CLambdaN ([idl,bk,a],b)
+let mkLambdaC (idl,bk,a,b) = CAst.make @@ CLambdaN ([CLocalAssum (idl,bk,a)],b)
 let mkLetInC  (id,a,t,b)   = CAst.make @@ CLetIn (id,a,t,b)
-let mkProdC   (idl,bk,a,b) = CAst.make @@ CProdN ([idl,bk,a],b)
+let mkProdC   (idl,bk,a,b) = CAst.make @@ CProdN ([CLocalAssum (idl,bk,a)],b)
 
 let mkAppC (f,l) =
   let l = List.map (fun x -> (x,None)) l in
@@ -539,56 +521,11 @@ let mkAppC (f,l) =
   | CApp (g,l') -> CAst.make @@ CApp (g, l' @ l)
   | _           -> CAst.make @@ CApp ((None, f), l)
 
-let add_name_in_env env n =
-  match snd n with
-  | Anonymous -> env
-  | Name id -> id :: env
-
-let fresh_var env c =
-  Namegen.next_ident_away (Id.of_string "pat")
-    (List.fold_left (fun accu id -> Id.Set.add id accu) (free_vars_of_constr_expr c) env)
-
-let expand_binders ?loc mkC bl c =
-  let rec loop ?loc bl c =
-    match bl with
-    | [] -> ([], c)
-    | b :: bl ->
-      match b with
-      | CLocalDef ((loc1,_) as n, oty, b) ->
-        let env, c = loop ?loc:(Loc.merge_opt loc1 loc) bl c in
-        let env = add_name_in_env env n in
-        (env, CAst.make ?loc @@ CLetIn (n,oty,b,c))
-      | CLocalAssum ((loc1,_)::_ as nl, bk, t) ->
-        let env, c = loop ?loc:(Loc.merge_opt loc1 loc) bl c in
-        let env = List.fold_left add_name_in_env env nl in
-        (env, mkC ?loc (nl,bk,t) c)
-      | CLocalAssum ([],_,_) -> loop ?loc bl c
-      | CLocalPattern (loc1, (p, ty)) ->
-        let env, c = loop ?loc:(Loc.merge_opt loc1 loc) bl c in
-        let ni = fresh_var env c in
-        let id = (loc1, Name ni) in
-        let ty = match ty with
-          | Some ty -> ty
-          | None -> CAst.make ?loc:loc1 @@ CHole (None, IntroAnonymous, None)
-        in
-        let e = CAst.make @@ CRef (Libnames.Ident (loc1, ni), None) in
-        let c = CAst.make ?loc @@
-          CCases
-            (LetPatternStyle, None, [(e,None,None)],
-             [(Loc.tag ?loc:loc1 ([[p]], c))])
-        in
-        (ni :: env, mkC ?loc ([id],Default Explicit,ty) c)
-  in
-  let (_, c) = loop ?loc bl c in
-  c
-
 let mkCProdN ?loc bll c =
-  let mk ?loc b c = CAst.make ?loc @@ CProdN ([b],c) in
-  expand_binders ?loc mk bll c
+  CAst.make ?loc @@ CProdN (bll,c)
 
 let mkCLambdaN ?loc bll c =
-  let mk ?loc b c = CAst.make ?loc @@ CLambdaN ([b],c) in
-  expand_binders ?loc mk bll c
+  CAst.make ?loc @@ CLambdaN (bll,c)
 
 let coerce_reference_to_id = function
   | Ident (_,id) -> id
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 4f7d537d3..ef20086e6 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -533,6 +533,10 @@ let occur_name na aty =
     | Name id -> occur_var_constr_expr id aty
     | Anonymous -> false
 
+let is_gvar id c = match DAst.get c with
+| GVar id' -> Id.equal id id'
+| _ -> false
+
 let is_projection nargs = function
   | Some r when not !Flags.in_debugger && not !Flags.raw_print && !print_projections ->
     (try
@@ -817,13 +821,11 @@ let rec extern inctx scopes vars r =
 
   | GProd (na,bk,t,c) ->
       let t = extern_typ scopes vars t in
-      let (idl,c) = factorize_prod scopes (add_vname vars na) na bk t c in
-      CProdN ([(Loc.tag na)::idl,Default bk,t],c)
+      factorize_prod scopes (add_vname vars na) na bk t c
 
   | GLambda (na,bk,t,c) ->
       let t = extern_typ scopes vars t in
-      let (idl,c) = factorize_lambda inctx scopes (add_vname vars na) na bk t c in
-      CLambdaN ([(Loc.tag na)::idl,Default bk,t],c)
+      factorize_lambda inctx scopes (add_vname vars na) na bk t c
 
   | GCases (sty,rtntypopt,tml,eqns) ->
     let vars' =
@@ -919,24 +921,48 @@ and extern_typ (_,scopes) =
 and sub_extern inctx (_,scopes) = extern inctx (None,scopes)
 
 and factorize_prod scopes vars na bk aty c =
-  let c = extern_typ scopes vars c in
-  match na, c with
-  | Name id, { CAst.loc ; v = CProdN ([nal,Default bk',ty],c) }
-      when binding_kind_eq bk bk' && constr_expr_eq aty ty
-      && not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) ->
-      nal,c
-  | _ ->
-      [],c
+  match na, DAst.get c with
+  | Name id, GCases (LetPatternStyle, None, [(e,(Anonymous,None))],[(_,(_,[p],b))])
+         when is_gvar id e && not (occur_glob_constr id b) ->
+      let b = extern_typ scopes vars b in
+      let p = extern_cases_pattern_in_scope scopes vars p in
+      let binder = CLocalPattern (c.loc,(p,None)) in
+      (match b.v with
+      | CProdN (bl,b) -> CProdN (binder::bl,b)
+      | _ -> CProdN ([binder],b))
+  | _, _ ->
+      let c = extern_typ scopes vars c in
+      match na, c.v with
+      | Name id, CProdN (CLocalAssum(nal,Default bk',ty)::bl,b)
+           when binding_kind_eq bk bk' && constr_expr_eq aty ty
+                && not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) ->
+         CProdN (CLocalAssum(Loc.tag na::nal,Default bk,aty)::bl,b)
+      | _, CProdN (bl,b) ->
+         CProdN (CLocalAssum([Loc.tag na],Default bk,aty)::bl,b)
+      | _, _ ->
+         CProdN ([CLocalAssum([Loc.tag na],Default bk,aty)],c)
 
 and factorize_lambda inctx scopes vars na bk aty c =
-  let c = sub_extern inctx scopes vars c in
-  match c with
-  | { CAst.loc; v = CLambdaN ([nal,Default bk',ty],c) }
-      when binding_kind_eq bk bk' && constr_expr_eq aty ty
-      && not (occur_name na ty) (* avoid na in ty escapes scope *) ->
-      nal,c
-  | _ ->
-      [],c
+  match na, DAst.get c with
+  | Name id, GCases (LetPatternStyle, None, [(e,(Anonymous,None))],[(_,(_,[p],b))])
+         when is_gvar id e && not (occur_glob_constr id b) ->
+      let b = sub_extern inctx scopes vars b in
+      let p = extern_cases_pattern_in_scope scopes vars p in
+      let binder = CLocalPattern (c.loc,(p,None)) in
+      (match b.v with
+      | CLambdaN (bl,b) -> CLambdaN (binder::bl,b)
+      | _ -> CLambdaN ([binder],b))
+  | _, _ ->
+      let c = sub_extern inctx scopes vars c in
+      match c.v with
+      | CLambdaN (CLocalAssum(nal,Default bk',ty)::bl,b)
+           when binding_kind_eq bk bk' && constr_expr_eq aty ty
+                && not (occur_name na ty) (* avoid na in ty escapes scope *) ->
+         CLambdaN (CLocalAssum(Loc.tag na::nal,Default bk,aty)::bl,b)
+      | CLambdaN (bl,b) ->
+         CLambdaN (CLocalAssum([Loc.tag na],Default bk,aty)::bl,b)
+      | _ ->
+         CLambdaN ([CLocalAssum([Loc.tag na],Default bk,aty)],c)
 
 and extern_local_binder scopes vars = function
     [] -> ([],[],[])
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 2761b6528..7276b917f 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -302,15 +302,8 @@ let set_type_scope env = {env with tmp_scope = Notation.current_type_scope_name
 
 let reset_tmp_scope env = {env with tmp_scope = None}
 
-let rec it_mkGProd ?loc env body =
-  match env with
-      (loc2, (na, bk, t)) :: tl -> it_mkGProd ?loc:loc2 tl (DAst.make ?loc:(Loc.merge_opt loc loc2) @@ GProd (na, bk, t, body))
-    | [] -> body
-
-let rec it_mkGLambda ?loc env body =
-  match env with
-      (loc2, (na, bk, t)) :: tl -> it_mkGLambda ?loc:loc2 tl (DAst.make ?loc:(Loc.merge_opt loc loc2) @@ GLambda (na, bk, t, body))
-    | [] -> body
+let mkGProd ?loc (na,bk,t) body = DAst.make ?loc @@ GProd (na, bk, t, body)
+let mkGLambda ?loc (na,bk,t) body = DAst.make ?loc @@ GLambda (na, bk, t, body)
 
 (**********************************************************************)
 (* Utilities for binders                                              *)
@@ -508,6 +501,20 @@ let intern_generalization intern env lvar loc bk ak c =
 	  (env', abs lid acc)) fvs (env,c)
   in c'
 
+let rec expand_binders ?loc mk bl c =
+  match bl with
+  | [] -> c
+  | b :: bl ->
+     match DAst.get b with
+     | GLocalDef (n, bk, b, oty) ->
+        expand_binders ?loc mk bl (DAst.make ?loc @@ GLetIn (n, b, oty, c))
+     | GLocalAssum (n, bk, t) ->
+        expand_binders ?loc mk bl (mk ?loc (n,bk,t) c)
+     | GLocalPattern ((pat,ids), id, bk, ty) ->
+        let tm = DAst.make ?loc (GVar id) in
+        let c = DAst.make ?loc @@ GCases (Misctypes.LetPatternStyle, None, [tm,(Anonymous,None)], [loc,(ids,[pat], c)]) in
+        expand_binders ?loc mk bl (mk ?loc (Name id,Explicit,ty) c)
+
 (**********************************************************************)
 (* Syntax extensions                                                  *)
 
@@ -1697,14 +1704,15 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
               Array.map (fun (bl,_,_) -> bl) idl,
               Array.map (fun (_,ty,_) -> ty) idl,
               Array.map (fun (_,_,bd) -> bd) idl)
-    | CProdN ([],c2) ->
-        intern_type env c2
-    | CProdN ((nal,bk,ty)::bll,c2) ->
-        iterate_prod ?loc env bk ty (CAst.make ?loc @@ CProdN (bll, c2)) nal
+    | CProdN (bl,c2) ->
+        let (env',bl) = List.fold_left intern_local_binder (env,[]) bl in
+        expand_binders ?loc mkGProd bl (intern_type env' c2)
     | CLambdaN ([],c2) ->
+        (* Such a term is built sometimes: it should not change scope *)
         intern env c2
-    | CLambdaN ((nal,bk,ty)::bll,c2) ->
-	iterate_lam loc (reset_tmp_scope env) bk ty (CAst.make ?loc @@ CLambdaN (bll, c2)) nal
+    | CLambdaN (bl,c2) ->
+        let (env',bl) = List.fold_left intern_local_binder (reset_tmp_scope env,[]) bl in
+        expand_binders ?loc mkGLambda bl (intern env' c2)
     | CLetIn (na,c1,t,c2) ->
 	let inc1 = intern (reset_tmp_scope env) c1 in
 	let int = Option.map (intern_type env) t in
@@ -1979,14 +1987,6 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
       [], None in
     (tm',(snd na,typ)), extra_id, match_td
 
-  and iterate_prod ?loc env bk ty body nal =
-    let env, bl = intern_assumption intern ntnvars env nal bk ty in
-    it_mkGProd ?loc bl (intern_type env body)
-
-  and iterate_lam loc env bk ty body nal =
-    let env, bl = intern_assumption intern ntnvars env nal bk ty in
-    it_mkGLambda ?loc bl (intern env body)
-
   and intern_impargs c env l subscopes args =
     let eargs, rargs = extract_explicit_arg l args in
     if !parsing_explicit then