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

---
 interp/notation.ml | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/notation.ml b/interp/notation.ml
index c35ba44aa5..136a45a0be 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -640,7 +640,7 @@ let constr_of_globref allow_constant env sigma = function
   | GlobRef.IndRef c ->
      let sigma,c = Evd.fresh_inductive_instance env sigma c in
      sigma,mkIndU c
-  | GlobRef.ConstRef c when allow_constant ->
+  | GlobRef.ConstRef c when allow_constant || Environ.is_primitive_type env c ->
      let sigma,c = Evd.fresh_constant_instance env sigma c in
      sigma,mkConstU c
   | _ -> raise NotAValidPrimToken
@@ -692,6 +692,13 @@ let rec constr_of_glob allow_constant to_post post env sigma g = match DAst.get
          sigma,mkApp (c, Array.of_list cl)
       end
   | Glob_term.GInt i -> sigma, mkInt i
+  | Glob_term.GFloat f -> sigma, mkFloat f
+  | Glob_term.GArray (_,t,def,ty) ->
+      let sigma, u' = Evd.fresh_array_instance env sigma in
+      let sigma, def' = constr_of_glob allow_constant to_post post env sigma def in
+      let sigma, t' = Array.fold_left_map (constr_of_glob allow_constant to_post post env) sigma t in
+      let sigma, ty' = constr_of_glob allow_constant to_post post env sigma ty in
+       sigma, mkArray (u',t',def',ty')
   | Glob_term.GSort gs ->
       let sigma,c = Evd.fresh_sort_in_family sigma (Glob_ops.glob_sort_family gs) in
       sigma,mkSort c
@@ -712,6 +719,12 @@ let rec glob_of_constr token_kind ?loc env sigma c = match Constr.kind c with
   | Ind (ind, _) -> DAst.make ?loc (Glob_term.GRef (GlobRef.IndRef ind, None))
   | Var id -> DAst.make ?loc (Glob_term.GRef (GlobRef.VarRef id, None))
   | Int i -> DAst.make ?loc (Glob_term.GInt i)
+  | Float f -> DAst.make ?loc (Glob_term.GFloat f)
+  | Array (u,t,def,ty) ->
+      let def' = glob_of_constr token_kind ?loc env sigma def
+      and t' = Array.map (glob_of_constr token_kind ?loc env sigma) t
+      and ty' = glob_of_constr token_kind ?loc env sigma ty in
+      DAst.make ?loc (Glob_term.GArray (None,t',def',ty'))
   | Sort Sorts.SProp -> DAst.make ?loc (Glob_term.GSort (Glob_term.UNamed [Glob_term.GSProp, 0]))
   | Sort Sorts.Prop -> DAst.make ?loc (Glob_term.GSort (Glob_term.UNamed [Glob_term.GProp, 0]))
   | Sort Sorts.Set -> DAst.make ?loc (Glob_term.GSort (Glob_term.UNamed [Glob_term.GSet, 0]))
-- 
cgit v1.2.3