Merge PR #8929: Fix fixpoint related lifting in open recursors + related cleanups

8 files changed, 101 insertions, 223 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index cfc4bea85f..96f1ce5e60 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -296,6 +296,8 @@ let decompose_prod_n_assum sigma n c =
 
 let existential_type = Evd.existential_type
 
+let lift n c = of_constr (Vars.lift n (unsafe_to_constr c))
+
 let map_under_context f n c =
   let f c = unsafe_to_constr (f (of_constr c)) in
   of_constr (Constr.map_under_context f n (unsafe_to_constr c))
@@ -306,137 +308,21 @@ let map_return_predicate f ci p =
   let f c = unsafe_to_constr (f (of_constr c)) in
   of_constr (Constr.map_return_predicate f ci (unsafe_to_constr p))
 
-let map_gen userview sigma f c = match kind sigma c with
-  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _) -> c
-  | Cast (b,k,t) ->
-      let b' = f b in
-      let t' = f t in
-      if b'==b && t' == t then c
-      else mkCast (b', k, t')
-  | Prod (na,t,b) ->
-      let b' = f b in
-      let t' = f t in
-      if b'==b && t' == t then c
-      else mkProd (na, t', b')
-  | Lambda (na,t,b) ->
-      let b' = f b in
-      let t' = f t in
-      if b'==b && t' == t then c
-      else mkLambda (na, t', b')
-  | LetIn (na,b,t,k) ->
-      let b' = f b in
-      let t' = f t in
-      let k' = f k in
-      if b'==b && t' == t && k'==k then c
-      else mkLetIn (na, b', t', k')
-  | App (b,l) ->
-      let b' = f b in
-      let l' = Array.Smart.map f l in
-      if b'==b && l'==l then c
-      else mkApp (b', l')
-  | Proj (p,t) ->
-      let t' = f t in
-      if t' == t then c
-      else mkProj (p, t')
-  | Evar (e,l) ->
-      let l' = Array.Smart.map f l in
-      if l'==l then c
-      else mkEvar (e, l')
-  | Case (ci,p,b,bl) when userview ->
-      let b' = f b in
-      let p' = map_return_predicate f ci p in
-      let bl' = map_branches f ci bl in
-      if b'==b && p'==p && bl'==bl then c
-      else mkCase (ci, p', b', bl')
-  | Case (ci,p,b,bl) ->
-      let b' = f b in
-      let p' = f p in
-      let bl' = Array.Smart.map f bl in
-      if b'==b && p'==p && bl'==bl then c
-      else mkCase (ci, p', b', bl')
-  | Fix (ln,(lna,tl,bl)) ->
-      let tl' = Array.Smart.map f tl in
-      let bl' = Array.Smart.map f bl in
-      if tl'==tl && bl'==bl then c
-      else mkFix (ln,(lna,tl',bl'))
-  | CoFix(ln,(lna,tl,bl)) ->
-      let tl' = Array.Smart.map f tl in
-      let bl' = Array.Smart.map f bl in
-      if tl'==tl && bl'==bl then c
-      else mkCoFix (ln,(lna,tl',bl'))
-
-let map_user_view = map_gen true
-let map = map_gen false
-
-let map_with_binders sigma g f l c0 = match kind sigma c0 with
-  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _) -> c0
-  | Cast (c, k, t) ->
-    let c' = f l c in
-    let t' = f l t in
-    if c' == c && t' == t then c0
-    else mkCast (c', k, t')
-  | Prod (na, t, c) ->
-    let t' = f l t in
-    let c' = f (g l) c in
-    if t' == t && c' == c then c0
-    else mkProd (na, t', c')
-  | Lambda (na, t, c) ->
-    let t' = f l t in
-    let c' = f (g l) c in
-    if t' == t && c' == c then c0
-    else mkLambda (na, t', c')
-  | LetIn (na, b, t, c) ->
-    let b' = f l b in
-    let t' = f l t in
-    let c' = f (g l) c in
-    if b' == b && t' == t && c' == c then c0
-    else mkLetIn (na, b', t', c')
-  | App (c, al) ->
-    let c' = f l c in
-    let al' = Array.Fun1.Smart.map f l al in
-    if c' == c && al' == al then c0
-    else mkApp (c', al')
-  | Proj (p, t) ->
-    let t' = f l t in
-    if t' == t then c0
-    else mkProj (p, t')
-  | Evar (e, al) ->
-    let al' = Array.Fun1.Smart.map f l al in
-    if al' == al then c0
-    else mkEvar (e, al')
-  | Case (ci, p, c, bl) ->
-    let p' = f l p in
-    let c' = f l c in
-    let bl' = Array.Fun1.Smart.map f l bl in
-    if p' == p && c' == c && bl' == bl then c0
-    else mkCase (ci, p', c', bl')
-  | Fix (ln, (lna, tl, bl)) ->
-    let tl' = Array.Fun1.Smart.map f l tl in
-    let l' = iterate g (Array.length tl) l in
-    let bl' = Array.Fun1.Smart.map f l' bl in
-    if tl' == tl && bl' == bl then c0
-    else mkFix (ln,(lna,tl',bl'))
-  | CoFix(ln,(lna,tl,bl)) ->
-    let tl' = Array.Fun1.Smart.map f l tl in
-    let l' = iterate g (Array.length tl) l in
-    let bl' = Array.Fun1.Smart.map f l' bl in
-    mkCoFix (ln,(lna,tl',bl'))
-
-let iter sigma f c = match kind sigma c with
-  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _) -> ()
-  | Cast (c,_,t) -> f c; f t
-  | Prod (_,t,c) -> f t; f c
-  | Lambda (_,t,c) -> f t; f c
-  | LetIn (_,b,t,c) -> f b; f t; f c
-  | App (c,l) -> f c; Array.iter f l
-  | Proj (p,c) -> f c
-  | Evar (_,l) -> Array.iter f l
-  | Case (_,p,c,bl) -> f p; f c; Array.iter f bl
-  | Fix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
-  | CoFix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
+let map_user_view sigma f c =
+  let f c = unsafe_to_constr (f (of_constr c)) in
+  of_constr (Constr.map_user_view f (unsafe_to_constr (whd_evar sigma c)))
+
+let map sigma f c =
+  let f c = unsafe_to_constr (f (of_constr c)) in
+  of_constr (Constr.map f (unsafe_to_constr (whd_evar sigma c)))
+
+let map_with_binders sigma g f l c =
+  let f l c = unsafe_to_constr (f l (of_constr c)) in
+  of_constr (Constr.map_with_binders g f l (unsafe_to_constr (whd_evar sigma c)))
+
+let iter sigma f c =
+  let f c = f (of_constr c) in
+  Constr.iter f (unsafe_to_constr (whd_evar sigma c))
 
 let iter_with_full_binders sigma g f n c =
   let open Context.Rel.Declaration in
@@ -453,31 +339,20 @@ let iter_with_full_binders sigma g f n c =
   | Proj (p,c) -> f n c
   | Fix (_,(lna,tl,bl)) ->
     Array.iter (f n) tl;
-    let n' = Array.fold_left2 (fun n na t -> g (LocalAssum (na,t)) n) n lna tl in
+    let n' = Array.fold_left2_i (fun i n na t -> g (LocalAssum (na, lift i t)) n) n lna tl in
     Array.iter (f n') bl
   | CoFix (_,(lna,tl,bl)) ->
     Array.iter (f n) tl;
-    let n' = Array.fold_left2 (fun n na t -> g (LocalAssum (na,t)) n) n lna tl in
+    let n' = Array.fold_left2_i (fun i n na t -> g (LocalAssum (na,lift i t)) n) n lna tl in
     Array.iter (f n') bl
 
 let iter_with_binders sigma g f n c =
-  iter_with_full_binders sigma (fun _ acc -> g acc) f n c
+  let f l c = f l (of_constr c) in
+  Constr.iter_with_binders g f n (unsafe_to_constr (whd_evar sigma c))
 
-let fold sigma f acc c = match kind sigma c with
-  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _) -> acc
-  | Cast (c,_,t) -> f (f acc c) t
-  | Prod (_,t,c) -> f (f acc t) c
-  | Lambda (_,t,c) -> f (f acc t) c
-  | LetIn (_,b,t,c) -> f (f (f acc b) t) c
-  | App (c,l) -> Array.fold_left f (f acc c) l
-  | Proj (p,c) -> f acc c
-  | Evar (_,l) -> Array.fold_left f acc l
-  | Case (_,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl
-  | Fix (_,(lna,tl,bl)) ->
-    Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl
-  | CoFix (_,(lna,tl,bl)) ->
-    Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl
+let fold sigma f acc c =
+  let f acc c = f acc (of_constr c) in
+  Constr.fold f acc (unsafe_to_constr (whd_evar sigma c))
 
 let compare_gen k eq_inst eq_sort eq_constr nargs c1 c2 =
   (c1 == c2) || Constr.compare_head_gen_with k k eq_inst eq_sort eq_constr nargs c1 c2
@@ -712,7 +587,7 @@ let to_rel_decl = unsafe_to_rel_decl
 type substl = t list
 
 (** Operations that commute with evar-normalization *)
-let lift n c = of_constr (Vars.lift n (to_constr c))
+let lift = lift
 let liftn n m c = of_constr (Vars.liftn n m (to_constr c))
 
 let substnl subst n c = of_constr (Vars.substnl (cast_list unsafe_eq subst) n (to_constr c))
diff --git a/engine/termops.ml b/engine/termops.ml
index ada6311067..98300764df 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -721,18 +721,16 @@ let map_constr_with_full_binders_gen userview sigma g f l cstr =
       let bl' = Array.map (f l) bl in
       if p==p' && c==c' && Array.for_all2 (==) bl bl' then cstr else
         mkCase (ci, p', c', bl')
-  | Fix (ln,(lna,tl,bl)) ->
+  | Fix (ln,(lna,tl,bl as fx)) ->
       let tl' = Array.map (f l) tl in
-      let l' =
-        Array.fold_left2 (fun l na t -> g (RelDecl.LocalAssum (na, t)) l) l lna tl in
+      let l' = fold_rec_types g fx l in
       let bl' = Array.map (f l') bl in
       if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
       then cstr
       else mkFix (ln,(lna,tl',bl'))
-  | CoFix(ln,(lna,tl,bl)) ->
+  | CoFix(ln,(lna,tl,bl as fx)) ->
       let tl' = Array.map (f l) tl in
-      let l' =
-        Array.fold_left2 (fun l na t -> g (RelDecl.LocalAssum (na, t)) l) l lna tl in
+      let l' = fold_rec_types g fx l in
       let bl' = Array.map (f l') bl in
       if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
       then cstr
@@ -759,34 +757,17 @@ let fold_constr_with_full_binders sigma g f n acc c =
   Constr.fold_with_full_binders g f n acc c
 
 let fold_constr_with_binders sigma g f n acc c =
-  fold_constr_with_full_binders sigma (fun _ x -> g x) f n acc c
+  let open EConstr in
+  let f l acc c = f l acc (of_constr c) in
+  let c = Unsafe.to_constr (whd_evar sigma c) in
+  Constr.fold_constr_with_binders g f n acc c
 
 (* [iter_constr_with_full_binders g f acc c] iters [f acc] on the immediate
    subterms of [c]; it carries an extra data [acc] which is processed by [g] at
    each binder traversal; it is not recursive and the order with which
    subterms are processed is not specified *)
 
-let iter_constr_with_full_binders sigma g f l c =
-  let open RelDecl in
-  match EConstr.kind sigma c with
-  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _) -> ()
-  | Cast (c,_, t) -> f l c; f l t
-  | Prod (na,t,c) -> f l t; f (g (LocalAssum (na,t)) l) c
-  | Lambda (na,t,c) -> f l t; f (g (LocalAssum (na,t)) l) c
-  | LetIn (na,b,t,c) -> f l b; f l t; f (g (LocalDef (na,b,t)) l) c
-  | App (c,args) -> f l c; Array.iter (f l) args
-  | Proj (p,c) -> f l c
-  | Evar (_,args) -> Array.iter (f l) args
-  | Case (_,p,c,bl) -> f l p; f l c; Array.iter (f l) bl
-  | Fix (_,(lna,tl,bl)) ->
-      let l' = Array.fold_left2 (fun l na t -> g (LocalAssum (na,t)) l) l lna tl in
-      Array.iter (f l) tl;
-      Array.iter (f l') bl
-  | CoFix (_,(lna,tl,bl)) ->
-      let l' = Array.fold_left2 (fun l na t -> g (LocalAssum (na,t)) l) l lna tl in
-      Array.iter (f l) tl;
-      Array.iter (f l') bl
+let iter_constr_with_full_binders = EConstr.iter_with_full_binders
 
 (***************************)
 (* occurs check functions  *)
diff --git a/engine/termops.mli b/engine/termops.mli
index 6c3d4fa612..eef8452e64 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -88,6 +88,7 @@ val iter_constr_with_full_binders : Evd.evar_map ->
   (rel_declaration -> 'a -> 'a) ->
   ('a -> constr -> unit) -> 'a ->
   constr -> unit
+[@@ocaml.deprecated "Use [EConstr.iter_with_full_binders]."]
 
 (**********************************************************************)
 
diff --git a/interp/impargs.ml b/interp/impargs.ml
index d8582d856e..d024a9e808 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -19,7 +19,6 @@ open Decl_kinds
 open Lib
 open Libobject
 open EConstr
-open Termops
 open Reductionops
 open Constrexpr
 open Namegen
@@ -200,16 +199,16 @@ let add_free_rels_until strict strongly_strict revpat bound env sigma m pos acc
 	acc.(i) <- update pos rig acc.(i)
     | App (f,_) when rig && is_flexible_reference env sigma bound depth f ->
 	if strict then () else
-          iter_constr_with_full_binders sigma push_lift (frec false) ed c
+          iter_with_full_binders sigma push_lift (frec false) ed c
     | Proj (p,c) when rig ->
       if strict then () else
-        iter_constr_with_full_binders sigma push_lift (frec false) ed c
+        iter_with_full_binders sigma push_lift (frec false) ed c
     | Case _ when rig ->
 	if strict then () else
-          iter_constr_with_full_binders sigma push_lift (frec false) ed c
+          iter_with_full_binders sigma push_lift (frec false) ed c
     | Evar _ -> ()
     | _ ->
-        iter_constr_with_full_binders sigma push_lift (frec rig) ed c
+        iter_with_full_binders sigma push_lift (frec rig) ed c
   in
   let () = if not (Vars.noccur_between sigma 1 bound m) then frec true (env,1) m in
   acc
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 704e6de6b8..8e5d15dd2d 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -452,27 +452,6 @@ let fold f acc c = match kind c with
   | CoFix (_,(_lna,tl,bl)) ->
     Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl
 
-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 _ -> 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) -> Array.fold_left (f n) acc l
-  | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
-  | Fix (_,(lna,tl,bl)) ->
-      let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n,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 (fun c n t -> g (LocalAssum (n,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
-
 (* [iter f c] iters [f] on the immediate subterms of [c]; it is
    not recursive and the order with which subterms are processed is
    not specified *)
@@ -534,12 +513,12 @@ let fold_constr_with_binders g f n acc c =
   | Proj (_p,c) -> f n acc c
   | Evar (_,l) -> Array.fold_left (f n) acc l
   | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
-  | Fix (_,(lna,tl,bl)) ->
-      let n' = CArray.fold_left2 (fun c _n _t -> g c) n lna tl in
+  | Fix (_,(_,tl,bl)) ->
+      let n' = iterate g (Array.length tl) n 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 (fun c _n _t -> g c) n lna tl in
+  | CoFix (_,(_,tl,bl)) ->
+      let n' = iterate g (Array.length tl) n 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
 
@@ -799,6 +778,49 @@ let map_with_binders g f l c0 = match kind c0 with
     let bl' = Array.Fun1.Smart.map f l' bl in
     mkCoFix (ln,(lna,tl',bl'))
 
+(*********************)
+(*      Lifting      *)
+(*********************)
+
+(* The generic lifting function *)
+let rec exliftn el c =
+  let open Esubst in
+  match kind c with
+  | Rel i -> mkRel(reloc_rel i el)
+  | _ -> map_with_binders el_lift exliftn el c
+
+(* Lifting the binding depth across k bindings *)
+
+let liftn n k c =
+  let open Esubst in
+  match el_liftn (pred k) (el_shft n el_id) with
+    | ELID -> c
+    | el -> exliftn el 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 _ -> 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) -> Array.fold_left (f n) acc l
+  | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) 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
+
+
 type 'univs instance_compare_fn = GlobRef.t -> int ->
   'univs -> 'univs -> bool
 
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 1be1f63ff7..f2cedcdabb 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -383,6 +383,17 @@ type rel_context = rel_declaration list
 type named_context = named_declaration list
 type compacted_context = compacted_declaration list
 
+(** {6 Relocation and substitution } *)
+
+(** [exliftn el c] lifts [c] with lifting [el] *)
+val exliftn : Esubst.lift -> constr -> constr
+
+(** [liftn n k c] lifts by [n] indexes above or equal to [k] in [c] *)
+val liftn : int -> int -> constr -> constr
+
+(** [lift n c] lifts by [n] the positive indexes in [c] *)
+val lift : int -> constr -> constr
+
 (** {6 Functionals working on expressions canonically abstracted over
        a local context (possibly with let-ins)} *)
 
diff --git a/kernel/vars.ml b/kernel/vars.ml
index 7380a860dd..f9c576ca4a 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Names
-open Esubst
 
 module RelDecl = Context.Rel.Declaration
 
@@ -80,19 +79,9 @@ let noccur_with_meta n m term =
 (*      Lifting      *)
 (*********************)
 
-(* The generic lifting function *)
-let rec exliftn el c = match Constr.kind c with
-  | Constr.Rel i -> Constr.mkRel(reloc_rel i el)
-  | _ -> Constr.map_with_binders el_lift exliftn el c
-
-(* Lifting the binding depth across k bindings *)
-
-let liftn n k c =
-  match el_liftn (pred k) (el_shft n el_id) with
-    | ELID -> c
-    | el -> exliftn el c
-
-let lift n = liftn n 1
+let exliftn = Constr.exliftn
+let liftn = Constr.liftn
+let lift = Constr.lift
 
 (*********************)
 (*   Substituting    *)
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 14358dd02a..10d8451947 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -759,6 +759,6 @@ let control_only_guard env sigma c =
   in
   let rec iter env c =
     check_fix_cofix env c;
-    iter_constr_with_full_binders sigma EConstr.push_rel iter env c
+    EConstr.iter_with_full_binders sigma EConstr.push_rel iter env c
   in
   iter env c