Merge PR #9627: Small retroknowledge/primitive cleanup

Ack-by: SkySkimmer
Reviewed-by: ppedrot
Reviewed-by: vbgl

10 files changed, 35 insertions, 24 deletions

diff --git a/checker/checker.ml b/checker/checker.ml
index 3c93ef7d36..d3f346d76b 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -273,6 +273,7 @@ let explain_exn = function
       | IllFormedBranch _ -> str"IllFormedBranch"
       | Generalization _ -> str"Generalization"
       | ActualType _ -> str"ActualType"
+      | IncorrectPrimitive _ -> str"IncorrectPrimitive"
       | CantApplyBadType ((n,a,b),{uj_val = hd; uj_type = hdty},args) ->
         let pp_arg i judge =
           hv 1 (str"arg " ++ int (i+1) ++ str"= " ++
diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml
index da5c4fb07b..fdc93cfa89 100644
--- a/kernel/cPrimitives.ml
+++ b/kernel/cPrimitives.ml
@@ -148,7 +148,7 @@ let prim_ind_to_string = function
   | PIT_cmp -> "cmp"
 
 let prim_type_to_string = function
-  | PT_int63 -> "int63"
+  | PT_int63 -> "int63_type"
 
 let op_or_type_to_string = function
   | OT_op op -> to_string op
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index cd675653cb..9397772415 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -339,9 +339,6 @@ let subst_retro_action subst action =
   | Register_type(prim,c) ->
     let c' = subst_constant subst c in
     if c == c' then action else Register_type(prim, c')
-  | Register_inline(c) ->
-    let c' = subst_constant subst c in
-    if c == c' then action else Register_inline(c')
 
 (* Here the semantics is completely unclear.
    What does "Hint Unfold t" means when "t" is a parameter?
diff --git a/kernel/primred.ml b/kernel/primred.ml
index d95d7de7aa..d6d0a6143a 100644
--- a/kernel/primred.ml
+++ b/kernel/primred.ml
@@ -44,10 +44,6 @@ let add_retroknowledge env action =
         { retro with retro_cmp = Some r }
     in
     set_retroknowledge env retro
-  | Register_inline(c) ->
-    let (cb,r) = lookup_constant_key c env in
-    let cb = {cb with Declarations.const_inline_code = true} in
-    add_constant_key c cb !(fst r) env
 
 let get_int_type env =
   match env.retroknowledge.retro_int63 with
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index 18fafdb6d3..e1c4cec5b5 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -38,4 +38,3 @@ let empty = {
 type action =
   | Register_ind of CPrimitives.prim_ind * inductive
   | Register_type of CPrimitives.prim_type * Constant.t
-  | Register_inline of Constant.t
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
index 1554fe88da..09e8140308 100644
--- a/kernel/retroknowledge.mli
+++ b/kernel/retroknowledge.mli
@@ -25,4 +25,3 @@ val empty : retroknowledge
 type action =
   | Register_ind of CPrimitives.prim_ind * inductive
   | Register_type of CPrimitives.prim_type * Constant.t
-  | Register_inline of Constant.t
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 964d32c6b3..481ffc290c 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -55,6 +55,7 @@ type ('constr, 'types) ptype_error =
   | IllFormedBranch of 'constr * pconstructor * 'constr * 'constr
   | Generalization of (Name.t * 'types) * ('constr, 'types) punsafe_judgment
   | ActualType of ('constr, 'types) punsafe_judgment * 'types
+  | IncorrectPrimitive of (CPrimitives.op_or_type,'types) punsafe_judgment * 'types
   | CantApplyBadType of
       (int * 'constr * 'constr) * ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array
   | CantApplyNonFunctional of ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array
@@ -120,6 +121,9 @@ let error_generalization env nvar c =
 let error_actual_type env j expty =
   raise (TypeError (env, ActualType (j,expty)))
 
+let error_incorrect_primitive env p t =
+  raise (TypeError (env, IncorrectPrimitive (p, t)))
+
 let error_cant_apply_not_functional env rator randl =
   raise (TypeError (env, CantApplyNonFunctional (rator,randl)))
 
@@ -175,6 +179,7 @@ let map_ptype_error f = function
 | IllFormedBranch (c, pc, t1, t2) -> IllFormedBranch (f c, pc, f t1, f t2)
 | Generalization ((na, t), j) -> Generalization ((na, f t), on_judgment f j)
 | ActualType (j, t) -> ActualType (on_judgment f j, f t)
+| IncorrectPrimitive (p, t) -> IncorrectPrimitive ({p with uj_type=f p.uj_type}, f t)
 | CantApplyBadType ((n, c1, c2), j, vj) ->
   CantApplyBadType ((n, f c1, f c2), on_judgment f j, Array.map (on_judgment f) vj)
 | CantApplyNonFunctional (j, jv) -> CantApplyNonFunctional (on_judgment f j, Array.map (on_judgment f) jv)
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 4b832930e1..c5ab9a4e73 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -56,6 +56,7 @@ type ('constr, 'types) ptype_error =
   | IllFormedBranch of 'constr * pconstructor * 'constr * 'constr
   | Generalization of (Name.t * 'types) * ('constr, 'types) punsafe_judgment
   | ActualType of ('constr, 'types) punsafe_judgment * 'types
+  | IncorrectPrimitive of (CPrimitives.op_or_type,'types) punsafe_judgment * 'types
   | CantApplyBadType of
       (int * 'constr * 'constr) * ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array
   | CantApplyNonFunctional of ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array
@@ -112,6 +113,8 @@ val error_generalization : env -> Name.t * types -> unsafe_judgment -> 'a
 
 val error_actual_type : env -> unsafe_judgment -> types -> 'a
 
+val error_incorrect_primitive : env -> (CPrimitives.op_or_type,types) punsafe_judgment -> types -> 'a
+
 val error_cant_apply_not_functional :
   env -> unsafe_judgment -> unsafe_judgment array -> 'a
 
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 7eb8e803b3..227a164549 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -252,6 +252,11 @@ let type_of_prim env t =
   in
   nary_int63_op (CPrimitives.arity t) return_ty
 
+let type_of_prim_or_type env = let open CPrimitives in
+  function
+  | OT_type t -> type_of_prim_type env t
+  | OT_op op -> type_of_prim env op
+
 let judge_of_int env i =
   make_judge (Constr.mkInt i) (type_of_int env)
 
@@ -664,17 +669,7 @@ let judge_of_case env ci pj cj lfj =
 
 (* Building type of primitive operators and type *)
 
-open CPrimitives
-
 let check_primitive_type env op_t t =
-  match op_t with
-  | OT_type PT_int63 ->
-    (try
-      default_conv ~l2r:false CUMUL env mkSet t
-    with NotConvertible ->
-      CErrors.user_err Pp.(str"Was expecting the sort of this primitive type to be Set"))
-  | OT_op p ->
-    (try
-      default_conv ~l2r:false CUMUL env (type_of_prim env p) t
-    with NotConvertible ->
-      CErrors.user_err Pp.(str"Not the expected type for this primitive"))
+  let inft = type_of_prim_or_type env op_t in
+  try default_conv ~l2r:false CUMUL env inft t
+  with NotConvertible -> error_incorrect_primitive env (make_judge op_t inft) t
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 9e92d936d2..2ef2317d86 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -339,6 +339,20 @@ let explain_actual_type env sigma j t reason =
   str "while it is expected to have type" ++ brk(1,1) ++ pt ++
   ppreason ++ str ".")
 
+let explain_incorrect_primitive env sigma j exp =
+  let env = make_all_name_different env sigma in
+  let {uj_val=p;uj_type=t} = j in
+  let t = Reductionops.nf_betaiota env sigma t in
+  let exp = Reductionops.nf_betaiota env sigma exp in
+  (* Actually print *)
+  let pe = pr_ne_context_of (str "In environment") env sigma in
+  let (pt, pct) = pr_explicit env sigma exp t in
+  pe ++
+  hov 0 (
+  str "The primitive" ++ brk(1,1) ++ str (CPrimitives.op_or_type_to_string p) ++ spc () ++
+  str "has type" ++ brk(1,1) ++ pct ++ spc () ++
+  str "while it is expected to have type" ++ brk(1,1) ++ pt ++ str ".")
+
 let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl =
   let randl = jv_nf_betaiotaevar env sigma randl in
   let actualtyp = Reductionops.nf_betaiota env sigma actualtyp in
@@ -720,7 +734,9 @@ let explain_type_error env sigma err =
   | Generalization (nvar, c) ->
       explain_generalization env sigma nvar c
   | ActualType (j, pt) ->
-      explain_actual_type env sigma j pt None
+    explain_actual_type env sigma j pt None
+  | IncorrectPrimitive (j, t) ->
+    explain_incorrect_primitive env sigma j t
   | CantApplyBadType (t, rator, randl) ->
       explain_cant_apply_bad_type env sigma t rator randl
   | CantApplyNonFunctional (rator, randl) ->