aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/changelog/03-notations/13519-primitiveArrayNotations.rst8
-rw-r--r--doc/sphinx/user-extensions/syntax-extensions.rst6
-rw-r--r--engine/evd.ml3
-rw-r--r--engine/evd.mli2
-rw-r--r--engine/univGen.ml5
-rw-r--r--engine/univGen.mli2
-rw-r--r--interp/notation.ml15
-rw-r--r--kernel/environ.ml15
-rw-r--r--kernel/environ.mli4
-rw-r--r--test-suite/output/StringSyntaxPrimitive.out20
-rw-r--r--test-suite/output/StringSyntaxPrimitive.v139
11 files changed, 216 insertions, 3 deletions
diff --git a/doc/changelog/03-notations/13519-primitiveArrayNotations.rst b/doc/changelog/03-notations/13519-primitiveArrayNotations.rst
new file mode 100644
index 0000000000..fb2545652c
--- /dev/null
+++ b/doc/changelog/03-notations/13519-primitiveArrayNotations.rst
@@ -0,0 +1,8 @@
+- **Added:**
+ :cmd:`Number Notation` and :cmd:`String Notation` now support
+ parsing and printing of primitive floats, primitive arrays
+ and type constants of primitive types.
+ (`#13519 <https://github.com/coq/coq/pull/13519>`_,
+ fixes `#13484 <https://github.com/coq/coq/issues/13484>`_
+ and `#13517 <https://github.com/coq/coq/issues/13517>`_,
+ by Fabian Kunze, with help of Jason Gross)
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index df73de846f..094a98e225 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1734,7 +1734,8 @@ Number notations
Note that only fully-reduced ground terms (terms containing only
function application, constructors, inductive type families,
- sorts, and primitive integers) will be considered for printing.
+ sorts, primitive integers, primitive floats, primitive arrays and type
+ constants for primitive types) will be considered for printing.
.. _number-string-via:
@@ -1891,7 +1892,8 @@ String notations
Note that only fully-reduced ground terms (terms containing only
function application, constructors, inductive type families,
- sorts, and primitive integers) will be considered for printing.
+ sorts, primitive integers, primitive floats, primitive arrays and type
+ constants for primitive types) will be considered for printing.
:n:`via @qualid__ind mapping [ {+, @qualid__constant => @qualid__constructor } ]`
works as for :ref:`number notations above <number-string-via>`.
diff --git a/engine/evd.ml b/engine/evd.ml
index 59eea97ce9..706e51d4b3 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -983,6 +983,9 @@ let fresh_inductive_instance ?loc ?(rigid=univ_flexible) env evd i =
let fresh_constructor_instance ?loc ?(rigid=univ_flexible) env evd c =
with_context_set ?loc rigid evd (UnivGen.fresh_constructor_instance env c)
+let fresh_array_instance ?loc ?(rigid=univ_flexible) env evd =
+ with_context_set ?loc rigid evd (UnivGen.fresh_array_instance env)
+
let fresh_global ?loc ?(rigid=univ_flexible) ?names env evd gr =
with_context_set ?loc rigid evd (UnivGen.fresh_global_instance ?loc ?names env gr)
diff --git a/engine/evd.mli b/engine/evd.mli
index 911e00c23a..a6d55c2615 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -698,6 +698,8 @@ val fresh_inductive_instance : ?loc:Loc.t -> ?rigid:rigid
-> env -> evar_map -> inductive -> evar_map * pinductive
val fresh_constructor_instance : ?loc:Loc.t -> ?rigid:rigid
-> env -> evar_map -> constructor -> evar_map * pconstructor
+val fresh_array_instance : ?loc:Loc.t -> ?rigid:rigid
+ -> env -> evar_map -> evar_map * Univ.Instance.t
val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> env ->
evar_map -> GlobRef.t -> evar_map * econstr
diff --git a/engine/univGen.ml b/engine/univGen.ml
index 6f27ccb7dc..278ca6bf34 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -65,6 +65,11 @@ let fresh_constructor_instance env c =
let u, ctx = fresh_global_instance env (GlobRef.ConstructRef c) in
(c, u), ctx
+let fresh_array_instance env =
+ let auctx = CPrimitives.typ_univs CPrimitives.PT_array in
+ let u, ctx = fresh_instance_from auctx None in
+ u, ctx
+
let fresh_global_instance ?loc ?names env gr =
let u, ctx = fresh_global_instance ?loc ?names env gr in
mkRef (gr, u), ctx
diff --git a/engine/univGen.mli b/engine/univGen.mli
index 81bdac17ce..05737411f5 100644
--- a/engine/univGen.mli
+++ b/engine/univGen.mli
@@ -42,6 +42,8 @@ val fresh_inductive_instance : env -> inductive ->
pinductive in_universe_context_set
val fresh_constructor_instance : env -> constructor ->
pconstructor in_universe_context_set
+val fresh_array_instance : env ->
+ Instance.t in_universe_context_set
val fresh_global_instance : ?loc:Loc.t -> ?names:Univ.Instance.t -> env -> GlobRef.t ->
constr in_universe_context_set
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]))
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} *)
diff --git a/test-suite/output/StringSyntaxPrimitive.out b/test-suite/output/StringSyntaxPrimitive.out
new file mode 100644
index 0000000000..131975c760
--- /dev/null
+++ b/test-suite/output/StringSyntaxPrimitive.out
@@ -0,0 +1,20 @@
+"abc"
+ : intList
+"abc"
+ : intList
+mk_intList [97%int63; 98%int63; 99%int63]
+ : intList
+"abc"
+ : intArray
+"abc"
+ : intArray
+ = "abc"
+ : nestArray
+"abc"
+ : nestArray
+"100"
+ : floatList
+"100"
+ : floatList
+mk_floatList [1%float; 0%float; 0%float]
+ : floatList
diff --git a/test-suite/output/StringSyntaxPrimitive.v b/test-suite/output/StringSyntaxPrimitive.v
new file mode 100644
index 0000000000..23ef082013
--- /dev/null
+++ b/test-suite/output/StringSyntaxPrimitive.v
@@ -0,0 +1,139 @@
+Require Import Coq.Lists.List.
+Require Import Coq.Strings.String Coq.Strings.Byte Coq.Strings.Ascii.
+Require Coq.Array.PArray Coq.Floats.PrimFloat.
+Require Import Coq.Numbers.BinNums Coq.Numbers.Cyclic.Int63.Int63.
+
+Set Printing Depth 100000.
+Set Printing Width 1000.
+
+Close Scope char_scope.
+Close Scope string_scope.
+
+(* Notations for primitive integers inside polymorphic datatypes *)
+Module Test1.
+ Inductive intList := mk_intList (_ : list int).
+ Definition i63_from_byte (b : byte) : int := Int63.of_Z (BinInt.Z.of_N (Byte.to_N b)).
+ Definition i63_to_byte (i : int) : byte :=
+ match Byte.of_N (BinInt.Z.to_N (Int63.to_Z i)) with Some x => x | None => x00%byte end.
+
+ Definition to_byte_list '(mk_intList a) := List.map i63_to_byte a.
+
+ Definition from_byte_list (xs : list byte) : intList:=
+ mk_intList (List.map i63_from_byte xs).
+
+ Declare Scope intList_scope.
+ Delimit Scope intList_scope with intList.
+
+ String Notation intList from_byte_list to_byte_list : intList_scope.
+
+ Open Scope intList_scope.
+ Import List.ListNotations.
+ Check mk_intList [97; 98; 99]%int63%list.
+ Check "abc"%intList.
+
+ Definition int' := int.
+ Check mk_intList (@cons int' 97 [98; 99])%int63%list.
+End Test1.
+
+Import PArray.
+
+(* Notations for primitive arrays *)
+Module Test2.
+ Inductive intArray := mk_intArray (_ : array int).
+
+ Definition i63_from_byte (b : byte) : Int63.int := Int63.of_Z (BinInt.Z.of_N (Byte.to_N b)).
+ Definition i63_to_byte (i : Int63.int) : byte :=
+ match Byte.of_N (BinInt.Z.to_N (Int63.to_Z i)) with Some x => x | None => x00%byte end.
+
+ Definition i63_to_nat x := BinInt.Z.to_nat (Int63.to_Z x).
+ Local Definition nat_length {X} (x : array X) :nat := i63_to_nat (length x).
+
+ Local Fixpoint list_length_i63 {A} (xs : list A) :int :=
+ match xs with
+ | nil => 0
+ | cons _ xs => 1 + list_length_i63 xs
+ end.
+
+ Definition to_byte_list '(mk_intArray a) :=
+ ((fix go (n : nat) (i : Int63.int) (acc : list byte) :=
+ match n with
+ | 0 => acc
+ | S n => go n (i - 1) (cons (i63_to_byte a.[i]) acc)
+ end) (nat_length a) (length a - 1) nil)%int63.
+
+ Definition from_byte_list (xs : list byte) :=
+ (let arr := make (list_length_i63 xs) 0 in
+ mk_intArray ((fix go i xs acc :=
+ match xs with
+ | nil => acc
+ | cons x xs => go (i + 1) xs (acc.[i <- i63_from_byte x])
+ end) 0 xs arr))%int63.
+
+ Declare Scope intArray_scope.
+ Delimit Scope intArray_scope with intArray.
+
+ String Notation intArray from_byte_list to_byte_list : intArray_scope.
+
+ Open Scope intArray_scope.
+ Check mk_intArray ( [| 97; 98; 99 | 0|])%int63%array.
+ Check "abc"%intArray.
+
+End Test2.
+
+(* Primitive arrays inside primitive arrays *)
+Module Test3.
+
+ Inductive nestArray := mk_nestArray (_ : array (array int)).
+ Definition to_byte_list '(mk_nestArray a) :=
+ ((fix go (n : nat) (i : Int63.int) (acc : list byte) :=
+ match n with
+ | 0 => acc
+ | S n => go n (i - 1) (cons (Test2.i63_to_byte a.[i].[0]) acc)
+ end) (Test2.nat_length a) (length a - 1) nil)%int63.
+
+ Definition from_byte_list (xs : list byte) :=
+ (let arr := make (Test2.list_length_i63 xs) (make 0 0) in
+ mk_nestArray ((fix go i xs acc :=
+ match xs with
+ | nil => acc
+ | cons x xs => go (i + 1) xs (acc.[i <- make 1 (Test2.i63_from_byte x)])
+ end) 0 xs arr))%int63.
+
+ Declare Scope nestArray_scope.
+ Delimit Scope nestArray_scope with nestArray.
+
+ String Notation nestArray from_byte_list to_byte_list : nestArray_scope.
+
+ Open Scope nestArray_scope.
+ Eval cbv in mk_nestArray ( [| make 1 97; make 1 98; make 1 99 | make 0 0|])%int63%array.
+ Check "abc"%nestArray.
+End Test3.
+
+
+
+(* Notations for primitive floats inside polymorphic datatypes *)
+Module Test4.
+ Import PrimFloat.
+ Inductive floatList := mk_floatList (_ : list float).
+ Definition float_from_byte (b : byte) : float :=
+ if Byte.eqb b "0"%byte then PrimFloat.zero else PrimFloat.one.
+ Definition float_to_byte (f : float) : byte :=
+ if PrimFloat.is_zero f then "0" else "1".
+ Definition to_byte_list '(mk_floatList a) := List.map float_to_byte a.
+
+ Definition from_byte_list (xs : list byte) : floatList:=
+ mk_floatList (List.map float_from_byte xs).
+
+ Declare Scope floatList_scope.
+ Delimit Scope floatList_scope with floatList.
+
+ String Notation floatList from_byte_list to_byte_list : floatList_scope.
+
+ Open Scope floatList_scope.
+ Import List.ListNotations.
+ Check mk_floatList [97; 0; 0]%float%list.
+ Check "100"%floatList.
+
+ Definition float' := float.
+ Check mk_floatList (@cons float' 1 [0; 0])%float%list.
+End Test4.
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 09:57:58 +0000