Better primitive type support in custom string and numeral notations.

- float and array values are now supported for printing and parsing in custom notations (and in notations defined using the ocaml API)
- the three constants bound to the primitive float, int and array type are now allowed anywhere inside a term to print, to handle them similar to `real` type constructors
- Grants #13484: String notations for primitive arrays
- Fixes #13517: String notation printing fails with primitive integers inside lists

1 files changed, 15 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)