Remove # keywords in Primitive

3 files changed, 80 insertions, 57 deletions

diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml
index 3fa376a037..c4036e9677 100644
--- a/kernel/cPrimitives.ml
+++ b/kernel/cPrimitives.ml
@@ -52,6 +52,51 @@ type t =
   | Float64next_up
   | Float64next_down
 
+let parse = function
+  | "int63_head0" -> Int63head0
+  | "int63_tail0" -> Int63tail0
+  | "int63_add" -> Int63add
+  | "int63_sub" -> Int63sub
+  | "int63_mul" -> Int63mul
+  | "int63_div" -> Int63div
+  | "int63_mod" -> Int63mod
+  | "int63_lsr" -> Int63lsr
+  | "int63_lsl" -> Int63lsl
+  | "int63_land" -> Int63land
+  | "int63_lor" -> Int63lor
+  | "int63_lxor" -> Int63lxor
+  | "int63_addc" -> Int63addc
+  | "int63_subc" -> Int63subc
+  | "int63_addcarryc" -> Int63addCarryC
+  | "int63_subcarryc" -> Int63subCarryC
+  | "int63_mulc" -> Int63mulc
+  | "int63_diveucl" -> Int63diveucl
+  | "int63_div21" -> Int63div21
+  | "int63_addmuldiv" -> Int63addMulDiv
+  | "int63_eq" -> Int63eq
+  | "int63_lt" -> Int63lt
+  | "int63_le" -> Int63le
+  | "int63_compare" -> Int63compare
+  | "float64_opp" -> Float64opp
+  | "float64_abs" -> Float64abs
+  | "float64_eq" -> Float64eq
+  | "float64_lt" -> Float64lt
+  | "float64_le" -> Float64le
+  | "float64_compare" -> Float64compare
+  | "float64_classify" -> Float64classify
+  | "float64_add" -> Float64add
+  | "float64_sub" -> Float64sub
+  | "float64_mul" -> Float64mul
+  | "float64_div" -> Float64div
+  | "float64_sqrt" -> Float64sqrt
+  | "float64_of_int63" -> Float64ofInt63
+  | "float64_normfr_mantissa" -> Float64normfr_mantissa
+  | "float64_frshiftexp" -> Float64frshiftexp
+  | "float64_ldshiftexp" -> Float64ldshiftexp
+  | "float64_next_up" -> Float64next_up
+  | "float64_next_down" -> Float64next_down
+  | _ -> raise Not_found
+
 let equal (p1 : t) (p2 : t) =
   p1 == p2
 
@@ -229,3 +274,17 @@ let prim_type_to_string = function
 let op_or_type_to_string = function
   | OT_op op -> to_string op
   | OT_type t -> prim_type_to_string t
+
+let prim_type_of_string = function
+  | "int63_type" -> PT_int63
+  | "float64_type" -> PT_float64
+  | _ -> raise Not_found
+
+let op_or_type_of_string s =
+  try OT_type (prim_type_of_string s)
+  with Not_found -> OT_op (parse s)
+
+let parse_op_or_type ?loc s =
+  try op_or_type_of_string s
+  with Not_found ->
+    CErrors.user_err ?loc Pp.(str ("Built-in #"^s^" does not exist."))
diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli
index 2a0399f1f7..a5db51111f 100644
--- a/kernel/cPrimitives.mli
+++ b/kernel/cPrimitives.mli
@@ -52,6 +52,10 @@ type t =
   | Float64next_up
   | Float64next_down
 
+(** Can raise [Not_found].
+    Beware that this is not exactly the reverse of [to_string] below. *)
+val parse : string -> t
+
 val equal : t -> t -> bool
 
 type arg_kind =
@@ -75,6 +79,10 @@ type prim_type =
   | PT_int63
   | PT_float64
 
+(** Can raise [Not_found] *)
+val prim_type_of_string : string -> prim_type
+val prim_type_to_string : prim_type -> string
+
 type 'a prim_ind =
   | PIT_bool : unit prim_ind
   | PIT_carry : prim_type prim_ind
@@ -90,8 +98,13 @@ type op_or_type =
   | OT_type of prim_type
 
 val prim_ind_to_string : 'a prim_ind -> string
+
+(** Can raise [Not_found] *)
+val op_or_type_of_string : string -> op_or_type
 val op_or_type_to_string : op_or_type -> string
 
+val parse_op_or_type : ?loc:Loc.t -> string -> op_or_type
+
 type ind_or_type =
   | PITT_ind : 'a prim_ind * 'a -> ind_or_type
   | PITT_type : prim_type -> ind_or_type
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 08ba49f92b..75d329e77c 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -68,6 +68,11 @@ let make_bullet s =
 let add_control_flag ~loc ~flag { CAst.v = cmd } =
   CAst.make ~loc { cmd with control = flag :: cmd.control }
 
+let test_hash_ident =
+  let open Pcoq.Lookahead in
+  to_entry "test_hash_ident" begin
+    lk_kw "#" >> lk_ident >> check_no_space
+  end
 }
 
 GRAMMAR EXTEND Gram
@@ -226,63 +231,9 @@ GRAMMAR EXTEND Gram
       | IDENT "Constraint"; l = LIST1 univ_constraint SEP "," -> { VernacConstraint l }
   ] ]
   ;
-
-   register_token:
-     [ [ r = register_prim_token -> { CPrimitives.OT_op r }
-       | r = register_type_token -> { CPrimitives.OT_type r } ] ]
-   ;
-
-   register_type_token:
-     [ [ "#int63_type" -> { CPrimitives.PT_int63 }
-       | "#float64_type" -> { CPrimitives.PT_float64 } ] ]
-   ;
-
-   register_prim_token:
-     [ [ "#int63_head0" -> { CPrimitives.Int63head0 }
-       | "#int63_tail0" -> { CPrimitives.Int63tail0 }
-       | "#int63_add" -> { CPrimitives.Int63add }
-       | "#int63_sub" -> { CPrimitives.Int63sub }
-       | "#int63_mul" -> { CPrimitives.Int63mul }
-       | "#int63_div" -> { CPrimitives.Int63div }
-       | "#int63_mod" -> { CPrimitives.Int63mod }
-       | "#int63_lsr" -> { CPrimitives.Int63lsr }
-       | "#int63_lsl" -> { CPrimitives.Int63lsl }
-       | "#int63_land" -> { CPrimitives.Int63land }
-       | "#int63_lor" -> { CPrimitives.Int63lor }
-       | "#int63_lxor" -> { CPrimitives.Int63lxor }
-       | "#int63_addc" -> { CPrimitives.Int63addc }
-       | "#int63_subc" -> { CPrimitives.Int63subc }
-       | "#int63_addcarryc" -> { CPrimitives.Int63addCarryC }
-       | "#int63_subcarryc" -> { CPrimitives.Int63subCarryC }
-       | "#int63_mulc" -> { CPrimitives.Int63mulc }
-       | "#int63_diveucl" -> { CPrimitives.Int63diveucl }
-       | "#int63_div21" -> { CPrimitives.Int63div21 }
-       | "#int63_addmuldiv" -> { CPrimitives.Int63addMulDiv }
-       | "#int63_eq" -> { CPrimitives.Int63eq }
-       | "#int63_lt" -> { CPrimitives.Int63lt }
-       | "#int63_le" -> { CPrimitives.Int63le }
-       | "#int63_compare" -> { CPrimitives.Int63compare }
-       | "#float64_opp" -> { CPrimitives.Float64opp }
-       | "#float64_abs" -> { CPrimitives.Float64abs }
-       | "#float64_eq" -> { CPrimitives.Float64eq }
-       | "#float64_lt" -> { CPrimitives.Float64lt }
-       | "#float64_le" -> { CPrimitives.Float64le }
-       | "#float64_compare" -> { CPrimitives.Float64compare }
-       | "#float64_classify" -> { CPrimitives.Float64classify }
-       | "#float64_add" -> { CPrimitives.Float64add }
-       | "#float64_sub" -> { CPrimitives.Float64sub }
-       | "#float64_mul" -> { CPrimitives.Float64mul }
-       | "#float64_div" -> { CPrimitives.Float64div }
-       | "#float64_sqrt" -> { CPrimitives.Float64sqrt }
-       | "#float64_of_int63" -> { CPrimitives.Float64ofInt63 }
-       | "#float64_normfr_mantissa" -> { CPrimitives.Float64normfr_mantissa }
-       | "#float64_frshiftexp" -> { CPrimitives.Float64frshiftexp }
-       | "#float64_ldshiftexp" -> { CPrimitives.Float64ldshiftexp }
-       | "#float64_next_up" -> { CPrimitives.Float64next_up }
-       | "#float64_next_down" -> { CPrimitives.Float64next_down }
-       ] ]
-    ;
-
+  register_token:
+    [ [ test_hash_ident; "#"; r = IDENT -> { CPrimitives.parse_op_or_type ~loc r } ] ]
+  ;
   thm_token:
     [ [ "Theorem" -> { Theorem }
       | IDENT "Lemma" -> { Lemma }