Merge PR #11417: Move kind_of_type from the kernel to EConstr.

Reviewed-by: SkySkimmer
Reviewed-by: gares

14 files changed, 80 insertions, 73 deletions

diff --git a/dev/ci/user-overlays/11417-ppedrot-rm-kind-of-type.sh b/dev/ci/user-overlays/11417-ppedrot-rm-kind-of-type.sh
new file mode 100644
index 0000000000..5fb29e1826
--- /dev/null
+++ b/dev/ci/user-overlays/11417-ppedrot-rm-kind-of-type.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "11417" ] || [ "$CI_BRANCH" = "rm-kind-of-type" ]; then
+
+    elpi_CI_REF=rm-kind-of-type
+    elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi
+
+fi
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index e37a58be61..08e283f524 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -739,6 +739,26 @@ let fresh_global ?loc ?rigid ?names env sigma reference =
 
 let is_global = isRefX
 
+(** Kind of type *)
+
+type kind_of_type =
+  | SortType   of ESorts.t
+  | CastType   of types * t
+  | ProdType   of Name.t Context.binder_annot * t * t
+  | LetInType  of Name.t Context.binder_annot * t * t * t
+  | AtomicType of t * t array
+
+let kind_of_type sigma t = match kind sigma t with
+  | Sort s -> SortType s
+  | Cast (c,_,t) -> CastType (c, t)
+  | Prod (na,t,c) -> ProdType (na, t, c)
+  | LetIn (na,b,t,c) -> LetInType (na, b, t, c)
+  | App (c,l) -> AtomicType (c, l)
+  | (Rel _ | Meta _ | Var _ | Evar _ | Const _
+  | Proj _ | Case _ | Fix _ | CoFix _ | Ind _)
+    -> AtomicType (t,[||])
+  | (Lambda _ | Construct _ | Int _ | Float _) -> failwith "Not a type"
+
 module Unsafe =
 struct
 let to_sorts = ESorts.unsafe_to_sorts
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 181714460d..ead7d88176 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -80,7 +80,14 @@ val to_constr : ?abort_on_undefined_evars:bool -> Evd.evar_map -> t -> Constr.t
 val to_constr_opt : Evd.evar_map -> t -> Constr.t option
 (** Same as [to_constr], but returns [None] if some unresolved evars remain *)
 
-val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type
+type kind_of_type =
+  | SortType   of ESorts.t
+  | CastType   of types * t
+  | ProdType   of Name.t Context.binder_annot * t * t
+  | LetInType  of Name.t Context.binder_annot * t * t * t
+  | AtomicType of t * t array
+
+val kind_of_type : Evd.evar_map -> t -> kind_of_type
 
 (** {5 Constructors} *)
 
diff --git a/engine/evd.ml b/engine/evd.ml
index 70f58163fd..4bfa7c45e3 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1364,7 +1364,6 @@ module MiniEConstr = struct
 
   let kind sigma c = Constr.kind (whd_evar sigma c)
   let kind_upto = kind
-  let kind_of_type sigma c = Term.kind_of_type (whd_evar sigma c)
   let of_kind = Constr.of_kind
   let of_constr c = c
   let of_constr_array v = v
diff --git a/engine/evd.mli b/engine/evd.mli
index 82e1003a65..2c1194a5de 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -711,7 +711,6 @@ module MiniEConstr : sig
 
   val kind : evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_term
   val kind_upto : evar_map -> constr -> (constr, types, Sorts.t, Univ.Instance.t) Constr.kind_of_term
-  val kind_of_type : evar_map -> t -> (t, t) Term.kind_of_type
 
   val whd_evar : evar_map -> t -> t
 
diff --git a/kernel/term.ml b/kernel/term.ml
index 87678b911e..a2586e74f7 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -363,24 +363,3 @@ let rec isArity c =
   | Cast (c,_,_)      -> isArity c
   | Sort _          -> true
   | _               -> false
-
-(** Kind of type *)
-
-(* Experimental, used in Presburger contrib *)
-type ('constr, 'types) kind_of_type =
-  | SortType   of Sorts.t
-  | CastType   of 'types * 'types
-  | ProdType   of Name.t Context.binder_annot * 'types * 'types
-  | LetInType  of Name.t Context.binder_annot * 'constr * 'types * 'types
-  | AtomicType of 'constr * 'constr array
-
-let kind_of_type t = match kind t with
-  | Sort s -> SortType s
-  | Cast (c,_,t) -> CastType (c, t)
-  | Prod (na,t,c) -> ProdType (na, t, c)
-  | LetIn (na,b,t,c) -> LetInType (na, b, t, c)
-  | App (c,l) -> AtomicType (c, l)
-  | (Rel _ | Meta _ | Var _ | Evar _ | Const _
-  | Proj _ | Case _ | Fix _ | CoFix _ | Ind _)
-    -> AtomicType (t,[||])
-  | (Lambda _ | Construct _ | Int _ | Float _) -> failwith "Not a type"
diff --git a/kernel/term.mli b/kernel/term.mli
index d2de4177ce..1fef54257a 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -181,17 +181,6 @@ val destArity : types -> arity
 (** Tell if a term has the form of an arity *)
 val isArity : types -> bool
 
-(** {5 Kind of type} *)
-
-type ('constr, 'types) kind_of_type =
-  | SortType   of Sorts.t
-  | CastType   of 'types * 'types
-  | ProdType   of Name.t Context.binder_annot * 'types * 'types
-  | LetInType  of Name.t Context.binder_annot * 'constr * 'types * 'types
-  | AtomicType of 'constr * 'constr array
-
-val kind_of_type : types -> (constr, types) kind_of_type
-
 (* Deprecated *)
 type sorts_family = Sorts.family = InSProp | InProp | InSet | InType
 [@@ocaml.deprecated "Alias for Sorts.family"]
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index de3c660938..f95672a15d 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -906,10 +906,11 @@ let pf_interp_ty ?(resolve_typeclasses=false) ist gl ty =
      | _ -> (mkCCast ty (mkCType None)).v)) ty in
      mk_term ' ' (force_type ty) in
    let strip_cast (sigma, t) =
-     let rec aux t = match EConstr.kind_of_type sigma t with
-     | CastType (t, ty) when !n_binders = 0 && EConstr.isSort sigma ty -> t
-     | ProdType(n,s,t) -> decr n_binders; EConstr.mkProd (n, s, aux t)
-     | LetInType(n,v,ty,t) -> decr n_binders; EConstr.mkLetIn (n, v, ty, aux t)
+     let open EConstr in
+     let rec aux t = match kind_of_type sigma t with
+     | CastType (t, ty) when !n_binders = 0 && isSort sigma ty -> t
+     | ProdType(n,s,t) -> decr n_binders; mkProd (n, s, aux t)
+     | LetInType(n,v,ty,t) -> decr n_binders; mkLetIn (n, v, ty, aux t)
      | _ -> anomaly "pf_interp_ty: ssr Type cast deleted by typecheck" in
      sigma, aux t in
    let sigma, cty as ty = strip_cast (interp_term ist gl ty) in
@@ -930,11 +931,12 @@ exception NotEnoughProducts
 let saturate ?(beta=false) ?(bi_types=false) env sigma c ?(ty=Retyping.get_type_of env sigma c) m
 =
   let rec loop ty args sigma n =
+  let open EConstr in
   if n = 0 then
     let args = List.rev args in
      (if beta then Reductionops.whd_beta sigma else fun x -> x)
       (EConstr.mkApp (c, Array.of_list (List.map snd args))), ty, args, sigma
-  else match EConstr.kind_of_type sigma ty with
+  else match kind_of_type sigma ty with
   | ProdType (_, src, tgt) ->
       let sigma = create_evar_defs sigma in
       let (sigma, x) =
@@ -947,7 +949,7 @@ let saturate ?(beta=false) ?(bi_types=false) env sigma c ?(ty=Retyping.get_type_
   | AtomicType _ ->
       let ty =  (* FIXME *)
         (Reductionops.whd_all env sigma) ty in
-      match EConstr.kind_of_type sigma ty with
+      match kind_of_type sigma ty with
       | ProdType _ -> loop ty args sigma n
       | _ -> raise NotEnoughProducts
   in
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 26962ee87b..7baccd3d75 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -13,7 +13,6 @@
 open Util
 open Names
 open Printer
-open Term
 open Constr
 open Context
 open Termops
@@ -35,16 +34,17 @@ module RelDecl = Context.Rel.Declaration
  * argument (index), it computes it's arity and the arity of the eliminator and
  * checks if the eliminator is recursive or not *)
 let analyze_eliminator elimty env sigma =
-  let rec loop ctx t = match EConstr.kind_of_type sigma t with
-  | AtomicType (hd, args) when EConstr.isRel sigma hd ->
-    ctx, EConstr.destRel sigma hd, not (EConstr.Vars.noccurn sigma 1 t), Array.length args, t
+  let open EConstr in
+  let rec loop ctx t = match kind_of_type sigma t with
+  | AtomicType (hd, args) when isRel sigma hd ->
+    ctx, destRel sigma hd, not (Vars.noccurn sigma 1 t), Array.length args, t
   | CastType (t, _) -> loop ctx t
   | ProdType (x, ty, t) -> loop (RelDecl.LocalAssum (x, ty) :: ctx) t
-  | LetInType (x,b,ty,t) -> loop (RelDecl.LocalDef (x, b, ty) :: ctx) (EConstr.Vars.subst1 b t)
+  | LetInType (x,b,ty,t) -> loop (RelDecl.LocalDef (x, b, ty) :: ctx) (Vars.subst1 b t)
   | _ ->
-    let env' = EConstr.push_rel_context ctx env in
+    let env' = push_rel_context ctx env in
     let t' = Reductionops.whd_all env' sigma t in
-    if not (EConstr.eq_constr sigma t t') then loop ctx t' else
+    if not (eq_constr sigma t t') then loop ctx t' else
       errorstrm Pp.(str"The eliminator has the wrong shape."++spc()++
       str"A (applied) bound variable was expected as the conclusion of "++
       str"the eliminator's"++Pp.cut()++str"type:"++spc()++pr_econstr_env env' sigma elimty) in
@@ -243,7 +243,8 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
     let sigma = project gl in
     ppdebug(lazy Pp.(str"elim= "++ pr_econstr_pat env sigma elim));
     ppdebug(lazy Pp.(str"elimty= "++ pr_econstr_pat env sigma elimty)) in
-  let inf_deps_r = match EConstr.kind_of_type (project gl) elimty with
+  let open EConstr in
+  let inf_deps_r = match kind_of_type (project gl) elimty with
     | AtomicType (_, args) -> List.rev (Array.to_list args)
     | _ -> assert false in
   let saturate_until gl c c_ty f =
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index df001b6084..895f491510 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -13,7 +13,6 @@
 open Ltac_plugin
 open Util
 open Names
-open Term
 open Constr
 open Context
 open Vars
@@ -379,7 +378,8 @@ let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_
         let hd_ty = Retyping.get_type_of env sigma hd in
         let names = let rec aux t = function 0 -> [] | n ->
           let t = Reductionops.whd_all env sigma t in
-          match EConstr.kind_of_type sigma t with
+          let open EConstr in
+          match kind_of_type sigma t with
           | ProdType (name, _, t) -> name.binder_name :: aux t (n-1)
           | _ -> assert false in aux hd_ty (Array.length args) in
         hd_ty, Util.List.map_filter (fun (t, name) ->
@@ -412,7 +412,8 @@ let rwcltac ?under ?map_redex cl rdx dir sr gl =
       let env, sigma, c, c_eq = pf_env gl, fst sr, snd sr, Coqlib.(lib_ref "core.eq.type") in
       let sigma, c_ty = Typing.type_of env sigma c in
         ppdebug(lazy Pp.(str"c_ty@rwcltac=" ++ pr_econstr_env env sigma c_ty));
-      match EConstr.kind_of_type sigma (Reductionops.whd_all env sigma c_ty) with
+      let open EConstr in
+      match kind_of_type sigma (Reductionops.whd_all env sigma c_ty) with
       | AtomicType(e, a) when Ssrcommon.is_ind_ref sigma e c_eq ->
           let new_rdx = if dir = L2R then a.(2) else a.(1) in
           pirrel_rewrite ?under ?map_redex cl rdx rdxt new_rdx dir (sigma,c) c_ty, tclIDTAC, gl
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 235dfc257d..a6b9a43778 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -361,8 +361,9 @@ let intro_lock ipats =
         let c = Proofview.Goal.concl gl in
         let sigma = Proofview.Goal.sigma gl in
         let env = Proofview.Goal.env gl in
-        match EConstr.kind_of_type sigma c with
-        | Term.AtomicType(hd, args) when
+        let open EConstr in
+        match kind_of_type sigma c with
+        | AtomicType(hd, args) when
             Array.length args >= 2 && is_app_evar sigma (Array.last args) &&
             Ssrequality.ssr_is_setoid env sigma hd args
             (* if the last condition above [ssr_is_setoid ...] holds
@@ -375,8 +376,8 @@ let intro_lock ipats =
           protect_subgoal env sigma hd args
         | _ ->
         let t = Reductionops.whd_all env sigma c in
-        match EConstr.kind_of_type sigma t with
-        | Term.AtomicType(hd, args) when
+        match kind_of_type sigma t with
+        | AtomicType(hd, args) when
             Ssrcommon.is_ind_ref sigma hd (Coqlib.lib_ref "core.eq.type") &&
             Array.length args = 3 && is_app_evar sigma args.(2) ->
           protect_subgoal env sigma hd args
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index 580c0423e9..843adb40ac 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -610,8 +610,9 @@ let tclCompileIPats = IpatMachine.tclCompileIPats
 let with_defective maintac deps clr = Goal.enter begin fun g ->
   let sigma, concl = Goal.(sigma g, concl g) in
   let top_id =
-    match EConstr.kind_of_type sigma concl with
-    | Term.ProdType ({binder_name=Name id}, _, _)
+    let open EConstr in
+    match kind_of_type sigma concl with
+    | ProdType ({binder_name=Name id}, _, _)
       when Ssrcommon.is_discharged_id id -> id
     | _ -> Ssrcommon.top_id in
   let top_gen = Ssrequality.mkclr clr, Ssrmatching.cpattern_of_id top_id in
@@ -641,10 +642,11 @@ let elim_intro_tac ipats ?seed what eqid ssrelim is_rec clr =
     | Some (IPatId ipat) when not is_rec ->
        let rec intro_eq () = Goal.enter begin fun g ->
          let sigma, env, concl = Goal.(sigma g, env g, concl g) in
-         match EConstr.kind_of_type sigma concl with
-         | Term.ProdType (_, src, tgt) -> begin
-             match EConstr.kind_of_type sigma src with
-             | Term.AtomicType (hd, _) when Ssrcommon.is_protect hd env sigma ->
+         let open EConstr in
+         match kind_of_type sigma concl with
+         | ProdType (_, src, tgt) -> begin
+             match kind_of_type sigma src with
+             | AtomicType (hd, _) when Ssrcommon.is_protect hd env sigma ->
                 V82.tactic ~nf_evars:false Ssrcommon.unprotecttac <*>
                 Ssrcommon.tclINTRO_ID ipat
              | _ -> Ssrcommon.tclINTRO_ANON () <*> intro_eq ()
@@ -669,8 +671,9 @@ let elim_intro_tac ipats ?seed what eqid ssrelim is_rec clr =
          let sigma, eq =
            EConstr.fresh_global env sigma (Coqlib.lib_ref "core.eq.type") in
          let ctx, last = EConstr.decompose_prod_assum sigma concl in
-         let args = match EConstr.kind_of_type sigma last with
-           | Term.AtomicType (hd, args) ->
+         let open EConstr in
+         let args = match kind_of_type sigma last with
+           | AtomicType (hd, args) ->
                if Ssrcommon.is_protect hd env sigma then args
                else Ssrcommon.errorstrm
                   (Pp.str "Too many names in intro pattern")
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index f91b5e7aa2..d051836ebc 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -95,8 +95,9 @@ applied to the first assumption in the goal *)
 let vsBOOTSTRAP = Goal.enter_one ~__LOC__ begin fun gl ->
   let concl = Goal.concl gl in
   let id = (* We keep the orig name for checks in "in" tcl *)
-    match EConstr.kind_of_type (Goal.sigma gl) concl with
-    | Term.ProdType({binder_name=Name.Name id}, _, _)
+    let open EConstr in
+    match kind_of_type (Goal.sigma gl) concl with
+    | ProdType({binder_name=Name.Name id}, _, _)
       when Ssrcommon.is_discharged_id id -> id
     | _ -> mk_anon_id "view_subject" (Tacmach.New.pf_ids_of_hyps gl) in
   let view = EConstr.mkVar id in
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index 36f35a67c3..59ca418a39 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -11,7 +11,6 @@
 (*i*)
 open Names
 open Globnames
-open Term
 open Constr
 open Context
 open Environ
@@ -78,14 +77,14 @@ let rename_type ty ref =
   let rec rename_type_aux c = function
     | [] -> c
     | rename :: rest as renamings ->
-        match kind_of_type c with
-        | ProdType (old, s, t) ->
+        match Constr.kind c with
+        | Prod (old, s, t) ->
             mkProd (name_override old rename, s, rename_type_aux t rest)
-        | LetInType(old, s, b, t) ->
+        | LetIn (old, s, b, t) ->
             mkLetIn (old ,s, b, rename_type_aux t renamings)
-        | CastType (t,_) -> rename_type_aux t renamings
-        | SortType _ -> c
-        | AtomicType _ -> c in
+        | Cast (t,_, _) -> rename_type_aux t renamings
+        | _ -> c
+  in
   try rename_type_aux ty (arguments_names ref)
   with Not_found -> ty