aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/syntax')
-rw-r--r--plugins/syntax/int31_syntax.ml114
-rw-r--r--plugins/syntax/int31_syntax_plugin.mlpack1
-rw-r--r--plugins/syntax/int63_syntax.ml55
-rw-r--r--plugins/syntax/int63_syntax_plugin.mlpack1
-rw-r--r--plugins/syntax/numeral.ml21
-rw-r--r--plugins/syntax/plugin_base.dune8
6 files changed, 79 insertions, 121 deletions
diff --git a/plugins/syntax/int31_syntax.ml b/plugins/syntax/int31_syntax.ml
deleted file mode 100644
index e34a401c2c..0000000000
--- a/plugins/syntax/int31_syntax.ml
+++ /dev/null
@@ -1,114 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \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 = "int31_syntax_plugin"
-let () = Mltop.add_known_module __coq_plugin_name
-
-(* digit-based syntax for int31 *)
-
-open Bigint
-open Names
-open Globnames
-open Glob_term
-
-(*** Constants for locating int31 constructors ***)
-
-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)
-
-let is_gr c gr = match DAst.get c with
-| GRef (r, _) -> GlobRef.equal r gr
-| _ -> false
-
-let make_mind mp id = Names.MutInd.make2 mp (Label.make id)
-let make_mind_mpfile dir id = make_mind (ModPath.MPfile (make_dir dir)) id
-let make_mind_mpdot dir modname id =
- let mp = ModPath.MPdot (ModPath.MPfile (make_dir dir), Label.make modname)
- in make_mind mp id
-
-
-(* int31 stuff *)
-let int31_module = ["Coq"; "Numbers"; "Cyclic"; "Int31"; "Int31"]
-let int31_path = make_path int31_module "int31"
-let int31_id = make_mind_mpfile int31_module
-let int31_scope = "int31_scope"
-
-let int31_construct = ConstructRef ((int31_id "int31",0),1)
-
-let int31_0 = ConstructRef ((int31_id "digits",0),1)
-let int31_1 = ConstructRef ((int31_id "digits",0),2)
-
-(*** Definition of the Non_closed exception, used in the pretty printing ***)
-exception Non_closed
-
-(*** Parsing for int31 in digital notation ***)
-
-(* parses a *non-negative* integer (from bigint.ml) into an int31
- wraps modulo 2^31 *)
-let int31_of_pos_bigint ?loc n =
- let ref_construct = DAst.make ?loc (GRef (int31_construct, None)) in
- let ref_0 = DAst.make ?loc (GRef (int31_0, None)) in
- let ref_1 = DAst.make ?loc (GRef (int31_1, None)) in
- let rec args counter n =
- if counter <= 0 then
- []
- else
- let (q,r) = div2_with_rest n in
- (if r then ref_1 else ref_0)::(args (counter-1) q)
- in
- DAst.make ?loc (GApp (ref_construct, List.rev (args 31 n)))
-
-let error_negative ?loc =
- CErrors.user_err ?loc ~hdr:"interp_int31" (Pp.str "int31 are only non-negative numbers.")
-
-let interp_int31 ?loc n =
- if is_pos_or_zero n then
- int31_of_pos_bigint ?loc n
- else
- error_negative ?loc
-
-(* Pretty prints an int31 *)
-
-let bigint_of_int31 =
- let rec args_parsing args cur =
- match args with
- | [] -> cur
- | r::l when is_gr r int31_0 -> args_parsing l (mult_2 cur)
- | r::l when is_gr r int31_1 -> args_parsing l (add_1 (mult_2 cur))
- | _ -> raise Non_closed
- in
- fun c -> match DAst.get c with
- | GApp (r, args) when is_gr r int31_construct -> args_parsing args zero
- | _ -> raise Non_closed
-
-let uninterp_int31 (AnyGlobConstr i) =
- try
- Some (bigint_of_int31 i)
- with Non_closed ->
- None
-
-open Notation
-
-let at_declare_ml_module f x =
- Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name
-
-(* Actually declares the interpreter for int31 *)
-
-let _ =
- register_bignumeral_interpretation int31_scope (interp_int31,uninterp_int31);
- at_declare_ml_module enable_prim_token_interpretation
- { pt_local = false;
- pt_scope = int31_scope;
- pt_interp_info = Uid int31_scope;
- pt_required = (int31_path,int31_module);
- pt_refs = [int31_construct];
- pt_in_match = true }
diff --git a/plugins/syntax/int31_syntax_plugin.mlpack b/plugins/syntax/int31_syntax_plugin.mlpack
deleted file mode 100644
index 54a5bc0cd1..0000000000
--- a/plugins/syntax/int31_syntax_plugin.mlpack
+++ /dev/null
@@ -1 +0,0 @@
-Int31_syntax
diff --git a/plugins/syntax/int63_syntax.ml b/plugins/syntax/int63_syntax.ml
new file mode 100644
index 0000000000..992b7a986b
--- /dev/null
+++ b/plugins/syntax/int63_syntax.ml
@@ -0,0 +1,55 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+
+(* 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.Int63.int"
+let q_id_int63 = qualid_of_string "Coq.Numbers.Cyclic.Int63.Int63.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"; "Int63"]
+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;
+ 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 = NumeralNotation o;
+ pt_required = (int63_path, int63_module);
+ pt_refs = [];
+ pt_in_match = false })
+ ()
diff --git a/plugins/syntax/int63_syntax_plugin.mlpack b/plugins/syntax/int63_syntax_plugin.mlpack
new file mode 100644
index 0000000000..d83d554fe6
--- /dev/null
+++ b/plugins/syntax/int63_syntax_plugin.mlpack
@@ -0,0 +1 @@
+Int63_syntax
diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml
index ea564ae2ba..0c6d2ac0d1 100644
--- a/plugins/syntax/numeral.ml
+++ b/plugins/syntax/numeral.ml
@@ -69,6 +69,14 @@ let locate_int () =
}, mkRefC q_int, mkRefC q_uint)
else None
+let locate_int63 () =
+ let int63n = "num.int63.type" in
+ if Coqlib.has_ref int63n
+ then
+ let q_int63 = qualid_of_ref int63n in
+ Some (mkRefC q_int63)
+ else None
+
let has_type f ty =
let (sigma, env) = Pfedit.get_current_context () in
let c = mkCastC (mkRefC f, Glob_term.CastConv ty) in
@@ -79,17 +87,18 @@ let type_error_to f ty =
CErrors.user_err
(pr_qualid f ++ str " should go from Decimal.int to " ++
pr_qualid ty ++ str " or (option " ++ pr_qualid ty ++ str ")." ++
- fnl () ++ str "Instead of Decimal.int, the types Decimal.uint or Z could be used (you may need to require BinNums or Decimal first).")
+ fnl () ++ str "Instead of Decimal.int, the types Decimal.uint or Z or Int63.int could be used (you may need to require BinNums or Decimal or Int63 first).")
let type_error_of g ty =
CErrors.user_err
(pr_qualid g ++ str " should go from " ++ pr_qualid ty ++
str " to Decimal.int or (option Decimal.int)." ++ fnl () ++
- str "Instead of Decimal.int, the types Decimal.uint or Z could be used (you may need to require BinNums or Decimal first).")
+ str "Instead of Decimal.int, the types Decimal.uint or Z or Int63.int could be used (you may need to require BinNums or Decimal or Int63 first).")
let vernac_numeral_notation local ty f g scope opts =
let int_ty = locate_int () in
let z_pos_ty = locate_z () in
+ let int63_ty = locate_int63 () in
let tyc = Smartlocate.global_inductive_with_alias ty in
let to_ty = Smartlocate.global_with_alias f in
let of_ty = Smartlocate.global_with_alias g in
@@ -111,6 +120,10 @@ let vernac_numeral_notation local ty f g scope opts =
match z_pos_ty with
| Some (z_pos_ty, cZ) when has_type f (arrow cZ cty) -> Z z_pos_ty, Direct
| Some (z_pos_ty, cZ) when has_type f (arrow cZ (opt cty)) -> Z z_pos_ty, Option
+ | _ ->
+ match int63_ty with
+ | Some cint63 when has_type f (arrow cint63 cty) -> Int63, Direct
+ | Some cint63 when has_type f (arrow cint63 (opt cty)) -> Int63, Option
| _ -> type_error_to f ty
in
(* Check the type of g *)
@@ -124,6 +137,10 @@ let vernac_numeral_notation local ty f g scope opts =
match z_pos_ty with
| Some (z_pos_ty, cZ) when has_type g (arrow cty cZ) -> Z z_pos_ty, Direct
| Some (z_pos_ty, cZ) when has_type g (arrow cty (opt cZ)) -> Z z_pos_ty, Option
+ | _ ->
+ match int63_ty with
+ | Some cint63 when has_type g (arrow cty cint63) -> Int63, Direct
+ | Some cint63 when has_type g (arrow cty (opt cint63)) -> Int63, Option
| _ -> type_error_of g ty
in
let o = { to_kind; to_ty; of_kind; of_ty;
diff --git a/plugins/syntax/plugin_base.dune b/plugins/syntax/plugin_base.dune
index 1ab16c700d..aac46338ea 100644
--- a/plugins/syntax/plugin_base.dune
+++ b/plugins/syntax/plugin_base.dune
@@ -20,8 +20,8 @@
(libraries coq.vernac))
(library
- (name int31_syntax_plugin)
- (public_name coq.plugins.int31_syntax)
- (synopsis "Coq syntax plugin: int31")
- (modules int31_syntax)
+ (name int63_syntax_plugin)
+ (public_name coq.plugins.int63_syntax)
+ (synopsis "Coq syntax plugin: int63")
+ (modules int63_syntax)
(libraries coq.vernac))
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:23:18 +0000