Merge PR #13519: Better primitive type support in custom string and numeral notations.

Reviewed-by: jfehrle
Reviewed-by: proux01
Ack-by: Zimmi48
Ack-by: SkySkimmer

2 files changed, 19 insertions, 0 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index a5f81d1e59..6f2aeab203 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -571,11 +571,26 @@ let is_primitive env c =
   | Declarations.Primitive _ -> true
   | _ -> false
 
+let is_int63_type env c =
+  match env.retroknowledge.Retroknowledge.retro_int63 with
+  | None -> false
+  | Some c' -> Constant.CanOrd.equal c c'
+
+let is_float64_type env c =
+  match env.retroknowledge.Retroknowledge.retro_float64 with
+  | None -> false
+  | Some c' -> Constant.CanOrd.equal c c'
+
 let is_array_type env c =
   match env.retroknowledge.Retroknowledge.retro_array with
   | None -> false
   | Some c' -> Constant.CanOrd.equal c c'
 
+let is_primitive_type env c =
+  (* dummy match to force an update if we add a primitive type, seperated clauses to satisfy ocaml 4.05 *)
+  let _ = function CPrimitives.(PTE(PT_int63)) -> () | CPrimitives.(PTE(PT_float64)) -> () | CPrimitives.(PTE(PT_array)) -> () in
+  is_int63_type env c || is_float64_type env c || is_array_type env c
+
 let polymorphic_constant cst env =
   Declareops.constant_is_polymorphic (lookup_constant cst env)
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 900e2128ea..dfd9173d10 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -250,6 +250,10 @@ val constant_opt_value_in : env -> Constant.t puniverses -> constr option
 val is_primitive : env -> Constant.t -> bool
 
 val is_array_type : env -> Constant.t -> bool
+val is_int63_type : env -> Constant.t -> bool
+val is_float64_type : env -> Constant.t -> bool
+val is_primitive_type : env -> Constant.t -> bool
+
 
 (** {6 Primitive projections} *)