From 0d1da885cc8ccfb9f995e5dcb0ed79e71e6020db Mon Sep 17 00:00:00 2001
From: Fabian Kunze
Date: Fri, 27 Nov 2020 20:58:19 +0100
Subject: 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

---
 kernel/environ.ml  | 15 +++++++++++++++
 kernel/environ.mli |  4 ++++
 2 files changed, 19 insertions(+)

(limited to 'kernel')

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} *)
 
-- 
cgit v1.2.3