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.

1 files changed, 0 insertions, 47 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