Move *_with_full_binders variants out of the kernel.

They are not used there, and removing the redundance of the the case
representation requires access to the environment, so we push their use
further up.

4 files changed, 60 insertions, 83 deletions

diff --git a/engine/termops.ml b/engine/termops.ml
index ccd49ca495..66131e1a8f 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -677,12 +677,21 @@ let map_constr_with_binders_left_to_right sigma g f l c =
       if def' == def && t' == t && ty' == ty then c
       else mkArray(u,t',def',ty')
 
-let map_under_context_with_full_binders sigma g f l n d =
-  let open EConstr in
-  let f l c = Unsafe.to_constr (f l (of_constr c)) in
-  let g d l = g (of_rel_decl d) l in
-  let d = EConstr.Unsafe.to_constr (EConstr.whd_evar sigma d) in
-  EConstr.of_constr (Constr.map_under_context_with_full_binders g f l n d)
+let rec map_under_context_with_full_binders sigma g f l n d =
+  if n = 0 then f l d else
+    match EConstr.kind sigma d with
+    | LetIn (na,b,t,c) ->
+       let b' = f l b in
+       let t' = f l t in
+       let c' = map_under_context_with_full_binders sigma g f (g (Context.Rel.Declaration.LocalDef (na,b,t)) l) (n-1) c in
+       if b' == b && t' == t && c' == c then d
+       else EConstr.mkLetIn (na,b',t',c')
+    | Lambda (na,t,b) ->
+       let t' = f l t in
+       let b' = map_under_context_with_full_binders sigma g f (g (Context.Rel.Declaration.LocalAssum (na,t)) l) (n-1) b in
+       if t' == t && b' == b then d
+       else EConstr.mkLambda (na,t',b')
+    | _ -> CErrors.anomaly (Pp.str "Ill-formed context")
 
 let map_branches_with_full_binders sigma g f l ci bl =
   let tags = Array.map List.length ci.ci_pp_info.cstr_tags in
@@ -775,11 +784,27 @@ let map_constr_with_full_binders_user_view sigma g f =
    each binder traversal; it is not recursive *)
 
 let fold_constr_with_full_binders sigma g f n acc c =
-  let open EConstr in
-  let f l acc c = f l acc (of_constr c) in
-  let g d l  = g (of_rel_decl d) l in
-  let c = Unsafe.to_constr (whd_evar sigma c) in
-  Constr.fold_with_full_binders g f n acc c
+  let open EConstr.Vars in
+  let open Context.Rel.Declaration in
+  match EConstr.kind sigma c with
+  | Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _ | Construct _  | Int _ | Float _ -> acc
+  | Cast (c,_, t) -> f n (f n acc c) t
+  | Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
+  | Lambda (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
+  | LetIn (na,b,t,c) -> f (g (LocalDef (na,b,t)) n) (f n (f n acc b) t) c
+  | App (c,l) -> Array.fold_left (f n) (f n acc c) l
+  | Proj (_,c) -> f n acc c
+  | Evar (_,l) -> List.fold_left (f n) acc l
+  | Case (_,p,iv,c,bl) -> Array.fold_left (f n) (f n (fold_invert (f n) (f n acc p) iv) c) bl
+  | Fix (_,(lna,tl,bl)) ->
+      let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in
+      let fd = Array.map2 (fun t b -> (t,b)) tl bl in
+      Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
+  | CoFix (_,(lna,tl,bl)) ->
+      let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in
+      let fd = Array.map2 (fun t b -> (t,b)) tl bl in
+      Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
+  | Array(_u,t,def,ty) -> f n (f n (Array.fold_left (f n) acc t) def) ty
 
 let fold_constr_with_binders sigma g f n acc c =
   let open EConstr in
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 3157ec9f57..bbaf95c9df 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -624,30 +624,6 @@ let map_branches_with_binders g f l ci bl =
 let map_return_predicate_with_binders g f l ci p =
   map_under_context_with_binders g f l (List.length ci.ci_pp_info.ind_tags) p
 
-let rec map_under_context_with_full_binders g f l n d =
-  if n = 0 then f l d else
-    match kind d with
-    | LetIn (na,b,t,c) ->
-       let b' = f l b in
-       let t' = f l t in
-       let c' = map_under_context_with_full_binders g f (g (Context.Rel.Declaration.LocalDef (na,b,t)) l) (n-1) c in
-       if b' == b && t' == t && c' == c then d
-       else mkLetIn (na,b',t',c')
-    | Lambda (na,t,b) ->
-       let t' = f l t in
-       let b' = map_under_context_with_full_binders g f (g (Context.Rel.Declaration.LocalAssum (na,t)) l) (n-1) b in
-       if t' == t && b' == b then d
-       else mkLambda (na,t',b')
-    | _ -> CErrors.anomaly (Pp.str "Ill-formed context")
-
-let map_branches_with_full_binders g f l ci bl =
-  let tags = Array.map List.length ci.ci_pp_info.cstr_tags in
-  let bl' = Array.map2 (map_under_context_with_full_binders g f l) tags bl in
-  if Array.for_all2 (==) bl' bl then bl else bl'
-
-let map_return_predicate_with_full_binders g f l ci p =
-  map_under_context_with_full_binders g f l (List.length ci.ci_pp_info.ind_tags) p
-
 let map_invert f = function
   | NoInvert -> NoInvert
   | CaseInvert {univs;args;} as orig ->
@@ -886,29 +862,6 @@ let liftn n k c =
 
 let lift n = liftn n 1
 
-let fold_with_full_binders g f n acc c =
-  let open Context.Rel.Declaration in
-  match kind c with
-  | Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _ | Construct _  | Int _ | Float _ -> acc
-  | Cast (c,_, t) -> f n (f n acc c) t
-  | Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
-  | Lambda (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
-  | LetIn (na,b,t,c) -> f (g (LocalDef (na,b,t)) n) (f n (f n acc b) t) c
-  | App (c,l) -> Array.fold_left (f n) (f n acc c) l
-  | Proj (_,c) -> f n acc c
-  | Evar (_,l) -> List.fold_left (f n) acc l
-  | Case (_,p,iv,c,bl) -> Array.fold_left (f n) (f n (fold_invert (f n) (f n acc p) iv) c) bl
-  | Fix (_,(lna,tl,bl)) ->
-      let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in
-      let fd = Array.map2 (fun t b -> (t,b)) tl bl in
-      Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
-  | CoFix (_,(lna,tl,bl)) ->
-      let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in
-      let fd = Array.map2 (fun t b -> (t,b)) tl bl in
-      Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
-  | Array(_u,t,def,ty) -> f n (f n (Array.fold_left (f n) acc t) def) ty
-
-
 type 'univs instance_compare_fn = (GlobRef.t * int) option ->
   'univs -> 'univs -> bool
 
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 62f2555a7e..ed63ac507c 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -478,25 +478,6 @@ val map_branches_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a ->
 
 val map_return_predicate_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_info -> constr -> constr
 
-(** [map_under_context_with_full_binders g f n l c] is similar to
-    [map_under_context_with_binders] except that [g] takes also a full
-    binder as argument and that only the number of binders (and not
-    their signature) is required *)
-
-val map_under_context_with_full_binders : ((constr, constr) Context.Rel.Declaration.pt -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> int -> constr -> constr
-
-(** [map_branches_with_full_binders g f l br] is equivalent to
-   [map_branches_with_binders] but using
-   [map_under_context_with_full_binders] *)
-
-val map_branches_with_full_binders : ((constr, constr) Context.Rel.Declaration.pt -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_info -> constr array -> constr array
-
-(** [map_return_predicate_with_full_binders g f l p] is equivalent to
-   [map_return_predicate_with_binders] but using
-   [map_under_context_with_full_binders] *)
-
-val map_return_predicate_with_full_binders : ((constr, constr) Context.Rel.Declaration.pt -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_info -> constr -> constr
-
 (** {6 Functionals working on the immediate subterm of a construction } *)
 
 (** [fold f acc c] folds [f] on the immediate subterms of [c]
@@ -505,10 +486,6 @@ val map_return_predicate_with_full_binders : ((constr, constr) Context.Rel.Decla
 
 val fold : ('a -> constr -> 'a) -> 'a -> constr -> 'a
 
-val fold_with_full_binders :
-  (rel_declaration -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) ->
-    'a -> 'b -> constr -> 'b
-
 val fold_invert : ('a -> 'b -> 'a) -> 'a -> ('b, 'c) case_invert -> 'a
 
 (** [map f c] maps [f] on the immediate subterms of [c]; it is
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index 848cd501c6..792f07bb89 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -165,6 +165,28 @@ let label_of = let open GlobRef in function
   | ConstructRef ((kn,_),_) -> MutInd.label kn
   | VarRef id -> Label.of_id id
 
+let fold_with_full_binders g f n acc c =
+  let open Context.Rel.Declaration in
+  match kind c with
+  | Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _ | Construct _  | Int _ | Float _ -> acc
+  | Cast (c,_, t) -> f n (f n acc c) t
+  | Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
+  | Lambda (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
+  | LetIn (na,b,t,c) -> f (g (LocalDef (na,b,t)) n) (f n (f n acc b) t) c
+  | App (c,l) -> Array.fold_left (f n) (f n acc c) l
+  | Proj (_,c) -> f n acc c
+  | Evar (_,l) -> List.fold_left (f n) acc l
+  | Case (_,p,iv,c,bl) -> Array.fold_left (f n) (f n (fold_invert (f n) (f n acc p) iv) c) bl
+  | Fix (_,(lna,tl,bl)) ->
+      let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in
+      let fd = Array.map2 (fun t b -> (t,b)) tl bl in
+      Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
+  | CoFix (_,(lna,tl,bl)) ->
+      let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in
+      let fd = Array.map2 (fun t b -> (t,b)) tl bl in
+      Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
+  | Array(_u,t,def,ty) -> f n (f n (Array.fold_left (f n) acc t) def) ty
+
 let rec traverse current ctx accu t =
   let open GlobRef in
   match Constr.kind t with
@@ -189,10 +211,10 @@ let rec traverse current ctx accu t =
         traverse_object
           ~inhabits:(current,ctx,Vars.subst1 mkProp oty) accu body (ConstRef kn)
     | _ ->
-        Constr.fold_with_full_binders
+        fold_with_full_binders
           Context.Rel.add (traverse current) ctx accu t
     end
-| _ -> Constr.fold_with_full_binders
+| _ -> fold_with_full_binders
           Context.Rel.add (traverse current) ctx accu t
 
 and traverse_object ?inhabits (curr, data, ax2ty) body obj =