aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/syntax/dune7
-rw-r--r--plugins/syntax/int63_syntax.ml58
-rw-r--r--plugins/syntax/number.ml63
3 files changed, 44 insertions, 84 deletions
diff --git a/plugins/syntax/dune b/plugins/syntax/dune
index f930fc265a..ba53a439a0 100644
--- a/plugins/syntax/dune
+++ b/plugins/syntax/dune
@@ -6,13 +6,6 @@
(libraries coq.vernac))
(library
- (name int63_syntax_plugin)
- (public_name coq.plugins.int63_syntax)
- (synopsis "Coq syntax plugin: int63")
- (modules int63_syntax)
- (libraries coq.vernac))
-
-(library
(name float_syntax_plugin)
(public_name coq.plugins.float_syntax)
(synopsis "Coq syntax plugin: float")
diff --git a/plugins/syntax/int63_syntax.ml b/plugins/syntax/int63_syntax.ml
deleted file mode 100644
index 110b26581f..0000000000
--- a/plugins/syntax/int63_syntax.ml
+++ /dev/null
@@ -1,58 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * Copyright INRIA, CNRS and contributors *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-
-(* Poor's man DECLARE PLUGIN *)
-let __coq_plugin_name = "int63_syntax_plugin"
-let () = Mltop.add_known_module __coq_plugin_name
-
-(* digit-based syntax for int63 *)
-
-open Names
-open Libnames
-
-(*** Constants for locating int63 constructors ***)
-
-let q_int63 = qualid_of_string "Coq.Numbers.Cyclic.Int63.PrimInt63.int"
-let q_id_int63 = qualid_of_string "Coq.Numbers.Cyclic.Int63.PrimInt63.id_int"
-
-let make_dir l = DirPath.make (List.rev_map Id.of_string l)
-let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
-
-(* int63 stuff *)
-let int63_module = ["Coq"; "Numbers"; "Cyclic"; "Int63"; "PrimInt63"]
-let int63_path = make_path int63_module "int"
-let int63_scope = "int63_scope"
-
-let at_declare_ml_module f x =
- Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name
-
-(* Actually declares the interpreter for int63 *)
-
-let _ =
- let open Notation in
- at_declare_ml_module
- (fun () ->
- let id_int63 = Nametab.locate q_id_int63 in
- let o = { to_kind = Int63, Direct;
- to_ty = id_int63;
- to_post = [||];
- of_kind = Int63, Direct;
- of_ty = id_int63;
- ty_name = q_int63;
- warning = Nop } in
- enable_prim_token_interpretation
- { pt_local = false;
- pt_scope = int63_scope;
- pt_interp_info = NumberNotation o;
- pt_required = (int63_path, int63_module);
- pt_refs = [];
- pt_in_match = false })
- ()
diff --git a/plugins/syntax/number.ml b/plugins/syntax/number.ml
index 0e7640f430..80c11dc0d4 100644
--- a/plugins/syntax/number.ml
+++ b/plugins/syntax/number.ml
@@ -106,10 +106,12 @@ let locate_number () =
let locate_int63 () =
let int63n = "num.int63.type" in
- if Coqlib.has_ref int63n
+ let pos_neg_int63n = "num.int63.pos_neg_int63" in
+ if Coqlib.has_ref int63n && Coqlib.has_ref pos_neg_int63n
then
- let q_int63 = qualid_of_ref int63n in
- Some (mkRefC q_int63)
+ let q_pos_neg_int63 = qualid_of_ref pos_neg_int63n in
+ Some ({pos_neg_int63_ty = unsafe_locate_ind q_pos_neg_int63},
+ mkRefC q_pos_neg_int63)
else None
let has_type env sigma f ty =
@@ -121,13 +123,13 @@ let type_error_to f ty =
CErrors.user_err
(pr_qualid f ++ str " should go from Number.int to " ++
pr_qualid ty ++ str " or (option " ++ pr_qualid ty ++ str ")." ++
- fnl () ++ str "Instead of Number.int, the types Number.uint or Z or Int63.int or Number.number could be used (you may need to require BinNums or Number or Int63 first).")
+ fnl () ++ str "Instead of Number.int, the types Number.uint or Z or PrimInt63.pos_neg_int63 or Number.number could be used (you may need to require BinNums or Number or PrimInt63 first).")
let type_error_of g ty =
CErrors.user_err
(pr_qualid g ++ str " should go from " ++ pr_qualid ty ++
str " to Number.int or (option Number.int)." ++ fnl () ++
- str "Instead of Number.int, the types Number.uint or Z or Int63.int or Number.number could be used (you may need to require BinNums or Number or Int63 first).")
+ str "Instead of Number.int, the types Number.uint or Z or PrimInt63.pos_neg_int63 or Number.number could be used (you may need to require BinNums or Number or PrimInt63 first).")
let warn_deprecated_decimal =
CWarnings.create ~name:"decimal-numeral-notation" ~category:"deprecated"
@@ -381,22 +383,37 @@ let elaborate_to_post_via env sigma ty_name ty_ind l =
let pt_refs = List.map (fun (_, cnst, _) -> cnst) (to_post.(0)) in
to_post, pt_refs
-let locate_global_inductive allow_params qid =
- let locate_param_inductive qid =
+type target_type =
+ | TargetInd of (inductive * GlobRef.t option list)
+ | TargetPrim of required_module
+
+let locate_global_inductive_with_params allow_params qid =
+ if not allow_params then raise Not_found else
match Nametab.locate_extended qid with
| Globnames.TrueGlobal _ -> raise Not_found
| Globnames.SynDef kn ->
match Syntax_def.search_syntactic_definition kn with
- | [], Notation_term.(NApp (NRef (GlobRef.IndRef i,None), l)) when allow_params ->
+ | [], Notation_term.(NApp (NRef (GlobRef.IndRef i,None), l)) ->
i,
List.map (function
| Notation_term.NRef (r,None) -> Some r
| Notation_term.NHole _ -> None
| _ -> raise Not_found) l
- | _ -> raise Not_found in
- try locate_param_inductive qid
+ | _ -> raise Not_found
+
+let locate_global_inductive allow_params qid =
+ try locate_global_inductive_with_params allow_params qid
with Not_found -> Smartlocate.global_inductive_with_alias qid, []
+let locate_global_inductive_or_int63 allow_params qid =
+ try TargetInd (locate_global_inductive_with_params allow_params qid)
+ with Not_found ->
+ let int63n = "num.int63.type" in
+ if allow_params && Coqlib.has_ref int63n
+ && GlobRef.equal (Smartlocate.global_with_alias qid) (Coqlib.lib_ref int63n)
+ then TargetPrim (Nametab.path_of_global (Coqlib.lib_ref int63n), [])
+ else TargetInd (Smartlocate.global_inductive_with_alias qid, [])
+
let vernac_number_notation local ty f g opts scope =
let rec parse_opts = function
| [] -> None, Nop
@@ -421,7 +438,7 @@ let vernac_number_notation local ty f g opts scope =
let ty_name = ty in
let ty, via =
match via with None -> ty, via | Some (ty', a) -> ty', Some (ty, a) in
- let tyc, params = locate_global_inductive (via = None) ty in
+ let tyc_params = locate_global_inductive_or_int63 (via = None) ty in
let to_ty = Smartlocate.global_with_alias f in
let of_ty = Smartlocate.global_with_alias g in
let cty = mkRefC ty in
@@ -451,11 +468,14 @@ let vernac_number_notation local ty f g opts scope =
| Some (z_pos_ty, cZ) when has_type env sigma f (arrow cZ (opt cty)) -> Z z_pos_ty, Option
| _ ->
match int63_ty with
- | Some cint63 when has_type env sigma f (arrow cint63 cty) -> Int63, Direct
- | Some cint63 when has_type env sigma f (arrow cint63 (opt cty)) -> Int63, Option
+ | Some (pos_neg_int63_ty, cint63) when has_type env sigma f (arrow cint63 cty) -> Int63 pos_neg_int63_ty, Direct
+ | Some (pos_neg_int63_ty, cint63) when has_type env sigma f (arrow cint63 (opt cty)) -> Int63 pos_neg_int63_ty, Option
| _ -> type_error_to f ty
in
(* Check the type of g *)
+ let cty = match tyc_params with
+ | TargetPrim _ -> mkRefC (qualid_of_string "Coq.Numbers.Cyclic.Int63.PrimInt63.int_wrapper")
+ | TargetInd _ -> cty in
let of_kind =
match num_ty with
| Some (int_ty, cint, _, _, _, _, _, _) when has_type env sigma g (arrow cty cint) -> Int int_ty, Direct
@@ -476,8 +496,8 @@ let vernac_number_notation local ty f g opts scope =
| Some (z_pos_ty, cZ) when has_type env sigma g (arrow cty (opt cZ)) -> Z z_pos_ty, Option
| _ ->
match int63_ty with
- | Some cint63 when has_type env sigma g (arrow cty cint63) -> Int63, Direct
- | Some cint63 when has_type env sigma g (arrow cty (opt cint63)) -> Int63, Option
+ | Some (pos_neg_int63_ty, cint63) when has_type env sigma g (arrow cty cint63) -> Int63 pos_neg_int63_ty, Direct
+ | Some (pos_neg_int63_ty, cint63) when has_type env sigma g (arrow cty (opt cint63)) -> Int63 pos_neg_int63_ty, Option
| _ -> type_error_of g ty
in
(match to_kind, of_kind with
@@ -485,9 +505,14 @@ let vernac_number_notation local ty f g opts scope =
| _, ((DecimalInt _ | DecimalUInt _ | Decimal _), _) ->
warn_deprecated_decimal ()
| _ -> ());
- let to_post, pt_refs = match via with
- | None -> elaborate_to_post_params env sigma tyc params
- | Some (ty, l) -> elaborate_to_post_via env sigma ty tyc l in
+ let to_post, pt_required, pt_refs = match tyc_params with
+ | TargetPrim path -> [||], path, [Coqlib.lib_ref "num.int63.wrap_int"]
+ | TargetInd (tyc, params) ->
+ let to_post, pt_refs =
+ match via with
+ | None -> elaborate_to_post_params env sigma tyc params
+ | Some (ty, l) -> elaborate_to_post_via env sigma ty tyc l in
+ to_post, (Nametab.path_of_global (GlobRef.IndRef tyc), []), pt_refs in
let o = { to_kind; to_ty; to_post; of_kind; of_ty; ty_name;
warning = opts }
in
@@ -498,7 +523,7 @@ let vernac_number_notation local ty f g opts scope =
{ pt_local = local;
pt_scope = scope;
pt_interp_info = NumberNotation o;
- pt_required = Nametab.path_of_global (GlobRef.IndRef tyc),[];
+ pt_required;
pt_refs;
pt_in_match = true }
in
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:17:01 +0000