Merge PR #13548: Move *_with_full_binders variants out of the kernel.

Reviewed-by: SkySkimmer
Ack-by: herbelin

2 files changed, 0 insertions, 70 deletions

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