Merge PR #6914: Primitive integers

Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Ack-by: maximedenes
Ack-by: ppedrot

7 files changed, 97 insertions, 11 deletions

diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index d9787bc73c..868a6ed3e9 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -245,6 +245,7 @@ let build_beq_scheme mode kn =
         | Fix _   -> raise (EqUnknown "fix")
         | Meta _  -> raise (EqUnknown "meta-variable")
         | Evar _  -> raise (EqUnknown "existential variable")
+        | Int _ -> raise (EqUnknown "int")
     in
       aux t
   in
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 4b8371f5c3..7301e1fff7 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -178,3 +178,29 @@ let do_assumptions kind nl l =
       in
       subst'@subst, status' && status, next_uctx uctx)
     ([], true, uctx) l)
+
+let do_primitive id prim typopt =
+  if Lib.sections_are_opened () then
+    CErrors.user_err Pp.(str "Declaring a primitive is not allowed in sections.");
+  if Dumpglob.dump () then Dumpglob.dump_definition id false "ax";
+  let env = Global.env () in
+  let evd = Evd.from_env env in
+  let evd, typopt = Option.fold_left_map
+      (interp_type_evars_impls ~impls:empty_internalization_env env)
+      evd typopt
+  in
+  let evd = Evd.minimize_universes evd in
+  let uvars, impls, typopt = match typopt with
+    | None -> Univ.LSet.empty, [], None
+    | Some (ty,impls) ->
+      EConstr.universes_of_constr evd ty, impls, Some (EConstr.to_constr evd ty)
+  in
+  let evd = Evd.restrict_universe_context evd uvars in
+  let uctx = UState.check_mono_univ_decl (Evd.evar_universe_context evd) UState.default_univ_decl in
+  let entry = { prim_entry_type = typopt;
+                prim_entry_univs = uctx;
+                prim_entry_content = prim;
+              }
+  in
+  let _kn = declare_constant id.CAst.v (PrimitiveEntry entry,IsPrimitive) in
+  register_message id.CAst.v
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index 56932360a9..c5bf3725a9 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -33,3 +33,5 @@ val declare_assumption : coercion_flag -> assumption_kind ->
   UnivNames.universe_binders -> Impargs.manual_implicits ->
   bool (** implicit *) -> Declaremods.inline -> variable CAst.t ->
   GlobRef.t * Univ.Instance.t * bool
+
+val do_primitive : lident -> CPrimitives.op_or_type -> constr_expr option -> unit
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 79adefdcf7..0664e18130 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -219,12 +219,51 @@ GRAMMAR EXTEND Gram
           { VernacRegister(g, RegisterCoqlib quid) }
       | IDENT "Register"; IDENT "Inline"; g = global ->
           { VernacRegister(g, RegisterInline) }
+      | IDENT "Primitive"; id = identref; typopt = OPT [ ":"; typ = lconstr -> { typ } ]; ":="; r = register_token ->
+          { VernacPrimitive(id, r, typopt) }
       | IDENT "Universe"; l = LIST1 identref -> { VernacUniverse l }
       | IDENT "Universes"; l = LIST1 identref -> { VernacUniverse l }
       | 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 } ] ]
+   ;
+
+   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 }
+       ] ]
+    ;
+
   thm_token:
     [ [ "Theorem" -> { Theorem }
       | IDENT "Lemma" -> { Lemma }
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 5eeeaada2d..d22e52e960 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -1182,6 +1182,12 @@ open Pputils
           hov 2
             (keyword "Register Inline" ++ spc() ++ pr_qualid qid)
         )
+      | VernacPrimitive(id,r,typopt) ->
+         hov 2
+             (keyword "Primitive" ++ spc() ++ pr_lident id ++
+                (Option.cata (fun ty -> spc() ++ str":" ++ pr_spc_lconstr ty) (mt()) typopt) ++ spc() ++
+                str ":=" ++ spc() ++
+                str (CPrimitives.op_or_type_to_string r))
       | VernacComments l ->
         return (
           hov 2
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 996fe320f9..7611355100 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2032,21 +2032,31 @@ let vernac_locate = function
 
 let vernac_register qid r =
   let gr = Smartlocate.global_with_alias qid in
- if Proof_global.there_are_pending_proofs () then
+  if Proof_global.there_are_pending_proofs () then
     user_err Pp.(str "Cannot register a primitive while in proof editing mode.");
   match r with
   | RegisterInline ->
-    if not (isConstRef gr) then
-      user_err Pp.(str "Register inline: a constant is expected");
-    Global.register_inline (destConstRef gr)
+    begin match gr with
+    | ConstRef c -> Global.register_inline c
+    | _ -> CErrors.user_err (Pp.str "Register Inline: expecting a constant")
+    end
   | RegisterCoqlib n ->
-    let path, id = Libnames.repr_qualid n in
-    if DirPath.equal path Retroknowledge.int31_path
-    then
-      let f = Retroknowledge.(KInt31 (int31_field_of_string (Id.to_string id))) in
-      Global.register f gr
-    else
-      Coqlib.register_ref (Libnames.string_of_qualid n) gr
+    let ns, id = Libnames.repr_qualid n in
+    if DirPath.equal (dirpath_of_string "kernel") ns then begin
+      if Lib.sections_are_opened () then
+        user_err Pp.(str "Registering a kernel type is not allowed in sections");
+      let pind = match Id.to_string id with
+        | "ind_bool" -> CPrimitives.PIT_bool
+        | "ind_carry" -> CPrimitives.PIT_carry
+        | "ind_pair" -> CPrimitives.PIT_pair
+        | "ind_cmp" -> CPrimitives.PIT_cmp
+        | k -> CErrors.user_err Pp.(str "Register: unknown identifier “" ++ str k ++ str "” in the “kernel” namespace")
+      in
+      match gr with
+      | IndRef ind -> Global.register_inductive ind pind
+      | _ -> CErrors.user_err (Pp.str "Register in kernel: expecting an inductive type")
+    end
+    else Coqlib.register_ref (Libnames.string_of_qualid n) gr
 
 (********************)
 (* Proof management *)
@@ -2316,6 +2326,7 @@ let interp ?proof ~atts ~st c =
   | VernacLocate l -> unsupported_attributes atts;
     Feedback.msg_notice @@ vernac_locate l
   | VernacRegister (qid, r) -> unsupported_attributes atts; vernac_register qid r
+  | VernacPrimitive (id, prim, typopt) -> unsupported_attributes atts; ComAssumption.do_primitive id prim typopt
   | VernacComments l -> unsupported_attributes atts;
     Flags.if_verbose Feedback.msg_info (str "Comments ok\n")
 
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 68a17e316e..2eb901890b 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -378,6 +378,7 @@ type nonrec vernac_expr =
   | VernacSearch of searchable * Goal_select.t option * search_restriction
   | VernacLocate of locatable
   | VernacRegister of qualid * register_kind
+  | VernacPrimitive of lident * CPrimitives.op_or_type * constr_expr option
   | VernacComments of comment list
 
   (* Proof management *)