aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/syntax')
-rw-r--r--plugins/syntax/g_numeral.mlg41
-rw-r--r--plugins/syntax/g_string.mlg25
-rw-r--r--plugins/syntax/int31_syntax.ml114
-rw-r--r--plugins/syntax/int31_syntax_plugin.mlpack1
-rw-r--r--plugins/syntax/numeral.ml142
-rw-r--r--plugins/syntax/numeral.mli17
-rw-r--r--plugins/syntax/numeral_notation_plugin.mlpack2
-rw-r--r--plugins/syntax/plugin_base.dune27
-rw-r--r--plugins/syntax/r_syntax.ml141
-rw-r--r--plugins/syntax/r_syntax.mli9
-rw-r--r--plugins/syntax/r_syntax_plugin.mlpack1
-rw-r--r--plugins/syntax/string_notation.ml98
-rw-r--r--plugins/syntax/string_notation.mli16
-rw-r--r--plugins/syntax/string_notation_plugin.mlpack2
14 files changed, 636 insertions, 0 deletions
diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg
new file mode 100644
index 0000000000..13e0bcbd47
--- /dev/null
+++ b/plugins/syntax/g_numeral.mlg
@@ -0,0 +1,41 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
+
+DECLARE PLUGIN "numeral_notation_plugin"
+
+{
+
+open Notation
+open Numeral
+open Pp
+open Names
+open Ltac_plugin
+open Stdarg
+open Pcoq.Prim
+
+let pr_numnot_option _ _ _ = function
+ | Nop -> mt ()
+ | Warning n -> str "(warning after " ++ str n ++ str ")"
+ | Abstract n -> str "(abstract after " ++ str n ++ str ")"
+
+}
+
+ARGUMENT EXTEND numnotoption
+ PRINTED BY { pr_numnot_option }
+| [ ] -> { Nop }
+| [ "(" "warning" "after" bigint(waft) ")" ] -> { Warning waft }
+| [ "(" "abstract" "after" bigint(n) ")" ] -> { Abstract n }
+END
+
+VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF
+ | #[ locality = Attributes.locality; ] [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":"
+ ident(sc) numnotoption(o) ] ->
+ { vernac_numeral_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) o }
+END
diff --git a/plugins/syntax/g_string.mlg b/plugins/syntax/g_string.mlg
new file mode 100644
index 0000000000..1e06cd8ddb
--- /dev/null
+++ b/plugins/syntax/g_string.mlg
@@ -0,0 +1,25 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
+
+DECLARE PLUGIN "string_notation_plugin"
+
+{
+
+open String_notation
+open Names
+open Stdarg
+
+}
+
+VERNAC COMMAND EXTEND StringNotation CLASSIFIED AS SIDEFF
+ | #[ locality = Attributes.locality; ] [ "String" "Notation" reference(ty) reference(f) reference(g) ":"
+ ident(sc) ] ->
+ { vernac_string_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) }
+END
diff --git a/plugins/syntax/int31_syntax.ml b/plugins/syntax/int31_syntax.ml
new file mode 100644
index 0000000000..e34a401c2c
--- /dev/null
+++ b/plugins/syntax/int31_syntax.ml
@@ -0,0 +1,114 @@
+(************************************************************************)
+(* * 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
new file mode 100644
index 0000000000..54a5bc0cd1
--- /dev/null
+++ b/plugins/syntax/int31_syntax_plugin.mlpack
@@ -0,0 +1 @@
+Int31_syntax
diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml
new file mode 100644
index 0000000000..470deb4a60
--- /dev/null
+++ b/plugins/syntax/numeral.ml
@@ -0,0 +1,142 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
+
+open Pp
+open Util
+open Names
+open Libnames
+open Globnames
+open Constrexpr
+open Constrexpr_ops
+open Notation
+
+(** * Numeral notation *)
+
+let warn_abstract_large_num_no_op =
+ CWarnings.create ~name:"abstract-large-number-no-op" ~category:"numbers"
+ (fun f ->
+ strbrk "The 'abstract after' directive has no effect when " ++
+ strbrk "the parsing function (" ++
+ Nametab.pr_global_env (Termops.vars_of_env (Global.env ())) f ++ strbrk ") targets an " ++
+ strbrk "option type.")
+
+let get_constructors ind =
+ let mib,oib = Global.lookup_inductive ind in
+ let mc = oib.Declarations.mind_consnames in
+ Array.to_list
+ (Array.mapi (fun j c -> ConstructRef (ind, j + 1)) mc)
+
+let q_z = qualid_of_string "Coq.Numbers.BinNums.Z"
+let q_positive = qualid_of_string "Coq.Numbers.BinNums.positive"
+let q_int = qualid_of_string "Coq.Init.Decimal.int"
+let q_uint = qualid_of_string "Coq.Init.Decimal.uint"
+let q_option = qualid_of_string "Coq.Init.Datatypes.option"
+
+let unsafe_locate_ind q =
+ match Nametab.locate q with
+ | IndRef i -> i
+ | _ -> raise Not_found
+
+let locate_ind q =
+ try unsafe_locate_ind q
+ with Not_found -> Nametab.error_global_not_found q
+
+let locate_z () =
+ try
+ Some { z_ty = unsafe_locate_ind q_z;
+ pos_ty = unsafe_locate_ind q_positive }
+ with Not_found -> None
+
+let locate_int () =
+ { uint = locate_ind q_uint;
+ int = locate_ind q_int }
+
+let has_type f ty =
+ let (sigma, env) = Pfedit.get_current_context () in
+ let c = mkCastC (mkRefC f, Glob_term.CastConv ty) in
+ try let _ = Constrintern.interp_constr env sigma c in true
+ with Pretype_errors.PretypeError _ -> false
+
+let type_error_to f ty loadZ =
+ 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" ++
+ (if loadZ then str " (require BinNums first)." else str "."))
+
+let type_error_of g ty loadZ =
+ 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" ++
+ (if loadZ then str " (require BinNums first)." else str "."))
+
+let vernac_numeral_notation local ty f g scope opts =
+ let int_ty = locate_int () in
+ let z_pos_ty = locate_z () 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
+ let cty = mkRefC ty in
+ let app x y = mkAppC (x,[y]) in
+ let cref q = mkRefC q in
+ let arrow x y =
+ mkProdC ([CAst.make Anonymous],Default Decl_kinds.Explicit, x, y)
+ in
+ let cZ = cref q_z in
+ let cint = cref q_int in
+ let cuint = cref q_uint in
+ let coption = cref q_option in
+ let opt r = app coption r in
+ let constructors = get_constructors tyc in
+ (* Check the type of f *)
+ let to_kind =
+ if has_type f (arrow cint cty) then Int int_ty, Direct
+ else if has_type f (arrow cint (opt cty)) then Int int_ty, Option
+ else if has_type f (arrow cuint cty) then UInt int_ty.uint, Direct
+ else if has_type f (arrow cuint (opt cty)) then UInt int_ty.uint, Option
+ else
+ match z_pos_ty with
+ | Some z_pos_ty ->
+ if has_type f (arrow cZ cty) then Z z_pos_ty, Direct
+ else if has_type f (arrow cZ (opt cty)) then Z z_pos_ty, Option
+ else type_error_to f ty false
+ | None -> type_error_to f ty true
+ in
+ (* Check the type of g *)
+ let of_kind =
+ if has_type g (arrow cty cint) then Int int_ty, Direct
+ else if has_type g (arrow cty (opt cint)) then Int int_ty, Option
+ else if has_type g (arrow cty cuint) then UInt int_ty.uint, Direct
+ else if has_type g (arrow cty (opt cuint)) then UInt int_ty.uint, Option
+ else
+ match z_pos_ty with
+ | Some z_pos_ty ->
+ if has_type g (arrow cty cZ) then Z z_pos_ty, Direct
+ else if has_type g (arrow cty (opt cZ)) then Z z_pos_ty, Option
+ else type_error_of g ty false
+ | None -> type_error_of g ty true
+ in
+ let o = { to_kind; to_ty; of_kind; of_ty;
+ ty_name = ty;
+ warning = opts }
+ in
+ (match opts, to_kind with
+ | Abstract _, (_, Option) -> warn_abstract_large_num_no_op o.to_ty
+ | _ -> ());
+ let i =
+ { pt_local = local;
+ pt_scope = scope;
+ pt_interp_info = NumeralNotation o;
+ pt_required = Nametab.path_of_global (IndRef tyc),[];
+ pt_refs = constructors;
+ pt_in_match = true }
+ in
+ enable_prim_token_interpretation i
diff --git a/plugins/syntax/numeral.mli b/plugins/syntax/numeral.mli
new file mode 100644
index 0000000000..f96b8321f8
--- /dev/null
+++ b/plugins/syntax/numeral.mli
@@ -0,0 +1,17 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
+
+open Libnames
+open Vernacexpr
+open Notation
+
+(** * Numeral notation *)
+
+val vernac_numeral_notation : locality_flag -> qualid -> qualid -> qualid -> Notation_term.scope_name -> numnot_option -> unit
diff --git a/plugins/syntax/numeral_notation_plugin.mlpack b/plugins/syntax/numeral_notation_plugin.mlpack
new file mode 100644
index 0000000000..f4d9cae3ff
--- /dev/null
+++ b/plugins/syntax/numeral_notation_plugin.mlpack
@@ -0,0 +1,2 @@
+Numeral
+G_numeral
diff --git a/plugins/syntax/plugin_base.dune b/plugins/syntax/plugin_base.dune
new file mode 100644
index 0000000000..1ab16c700d
--- /dev/null
+++ b/plugins/syntax/plugin_base.dune
@@ -0,0 +1,27 @@
+(library
+ (name numeral_notation_plugin)
+ (public_name coq.plugins.numeral_notation)
+ (synopsis "Coq numeral notation plugin")
+ (modules g_numeral numeral)
+ (libraries coq.plugins.ltac))
+
+(library
+ (name string_notation_plugin)
+ (public_name coq.plugins.string_notation)
+ (synopsis "Coq string notation plugin")
+ (modules g_string string_notation)
+ (libraries coq.vernac))
+
+(library
+ (name r_syntax_plugin)
+ (public_name coq.plugins.r_syntax)
+ (synopsis "Coq syntax plugin: reals")
+ (modules r_syntax)
+ (libraries coq.vernac))
+
+(library
+ (name int31_syntax_plugin)
+ (public_name coq.plugins.int31_syntax)
+ (synopsis "Coq syntax plugin: int31")
+ (modules int31_syntax)
+ (libraries coq.vernac))
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
new file mode 100644
index 0000000000..d90b7d754c
--- /dev/null
+++ b/plugins/syntax/r_syntax.ml
@@ -0,0 +1,141 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
+
+open Util
+open Names
+open Globnames
+open Glob_term
+open Bigint
+
+(* Poor's man DECLARE PLUGIN *)
+let __coq_plugin_name = "r_syntax_plugin"
+let () = Mltop.add_known_module __coq_plugin_name
+
+exception Non_closed_number
+
+(**********************************************************************)
+(* Parsing positive via scopes *)
+(**********************************************************************)
+
+let binnums = ["Coq";"Numbers";"BinNums"]
+
+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 positive_modpath = MPfile (make_dir binnums)
+
+let positive_kn = MutInd.make2 positive_modpath (Label.make "positive")
+let path_of_xI = ((positive_kn,0),1)
+let path_of_xO = ((positive_kn,0),2)
+let path_of_xH = ((positive_kn,0),3)
+let glob_xI = ConstructRef path_of_xI
+let glob_xO = ConstructRef path_of_xO
+let glob_xH = ConstructRef path_of_xH
+
+let pos_of_bignat ?loc x =
+ let ref_xI = DAst.make @@ GRef (glob_xI, None) in
+ let ref_xH = DAst.make @@ GRef (glob_xH, None) in
+ let ref_xO = DAst.make @@ GRef (glob_xO, None) in
+ let rec pos_of x =
+ match div2_with_rest x with
+ | (q,false) -> DAst.make @@ GApp (ref_xO,[pos_of q])
+ | (q,true) when not (Bigint.equal q zero) -> DAst.make @@ GApp (ref_xI,[pos_of q])
+ | (q,true) -> ref_xH
+ in
+ pos_of x
+
+(**********************************************************************)
+(* Printing positive via scopes *)
+(**********************************************************************)
+
+let rec bignat_of_pos c = match DAst.get c with
+ | GApp (r, [a]) when is_gr r glob_xO -> mult_2(bignat_of_pos a)
+ | GApp (r, [a]) when is_gr r glob_xI -> add_1(mult_2(bignat_of_pos a))
+ | GRef (a, _) when GlobRef.equal a glob_xH -> Bigint.one
+ | _ -> raise Non_closed_number
+
+(**********************************************************************)
+(* Parsing Z via scopes *)
+(**********************************************************************)
+
+let z_kn = MutInd.make2 positive_modpath (Label.make "Z")
+let path_of_ZERO = ((z_kn,0),1)
+let path_of_POS = ((z_kn,0),2)
+let path_of_NEG = ((z_kn,0),3)
+let glob_ZERO = ConstructRef path_of_ZERO
+let glob_POS = ConstructRef path_of_POS
+let glob_NEG = ConstructRef path_of_NEG
+
+let z_of_int ?loc n =
+ if not (Bigint.equal n zero) then
+ let sgn, n =
+ if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in
+ DAst.make @@ GApp(DAst.make @@ GRef (sgn,None), [pos_of_bignat ?loc n])
+ else
+ DAst.make @@ GRef (glob_ZERO, None)
+
+(**********************************************************************)
+(* Printing Z via scopes *)
+(**********************************************************************)
+
+let bigint_of_z c = match DAst.get c with
+ | GApp (r,[a]) when is_gr r glob_POS -> bignat_of_pos a
+ | GApp (r,[a]) when is_gr r glob_NEG -> Bigint.neg (bignat_of_pos a)
+ | GRef (a, _) when GlobRef.equal a glob_ZERO -> Bigint.zero
+ | _ -> raise Non_closed_number
+
+(**********************************************************************)
+(* Parsing R via scopes *)
+(**********************************************************************)
+
+let rdefinitions = ["Coq";"Reals";"Rdefinitions"]
+let r_modpath = MPfile (make_dir rdefinitions)
+let r_path = make_path rdefinitions "R"
+
+let glob_IZR = ConstRef (Constant.make2 r_modpath @@ Label.make "IZR")
+
+let r_of_int ?loc z =
+ DAst.make @@ GApp (DAst.make @@ GRef(glob_IZR,None), [z_of_int ?loc z])
+
+(**********************************************************************)
+(* Printing R via scopes *)
+(**********************************************************************)
+
+let bigint_of_r c = match DAst.get c with
+ | GApp (r, [a]) when is_gr r glob_IZR ->
+ bigint_of_z a
+ | _ -> raise Non_closed_number
+
+let uninterp_r (AnyGlobConstr p) =
+ try
+ Some (bigint_of_r p)
+ with Non_closed_number ->
+ None
+
+open Notation
+
+let at_declare_ml_module f x =
+ Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name
+
+let r_scope = "R_scope"
+
+let _ =
+ register_bignumeral_interpretation r_scope (r_of_int,uninterp_r);
+ at_declare_ml_module enable_prim_token_interpretation
+ { pt_local = false;
+ pt_scope = r_scope;
+ pt_interp_info = Uid r_scope;
+ pt_required = (r_path,["Coq";"Reals";"Rdefinitions"]);
+ pt_refs = [glob_IZR];
+ pt_in_match = false }
diff --git a/plugins/syntax/r_syntax.mli b/plugins/syntax/r_syntax.mli
new file mode 100644
index 0000000000..7c3ee60040
--- /dev/null
+++ b/plugins/syntax/r_syntax.mli
@@ -0,0 +1,9 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
diff --git a/plugins/syntax/r_syntax_plugin.mlpack b/plugins/syntax/r_syntax_plugin.mlpack
new file mode 100644
index 0000000000..d4ee75ea48
--- /dev/null
+++ b/plugins/syntax/r_syntax_plugin.mlpack
@@ -0,0 +1 @@
+R_syntax
diff --git a/plugins/syntax/string_notation.ml b/plugins/syntax/string_notation.ml
new file mode 100644
index 0000000000..12ee4c6eda
--- /dev/null
+++ b/plugins/syntax/string_notation.ml
@@ -0,0 +1,98 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
+
+open Pp
+open Util
+open Names
+open Libnames
+open Globnames
+open Constrexpr
+open Constrexpr_ops
+open Notation
+
+(** * String notation *)
+
+let get_constructors ind =
+ let mib,oib = Global.lookup_inductive ind in
+ let mc = oib.Declarations.mind_consnames in
+ Array.to_list
+ (Array.mapi (fun j c -> ConstructRef (ind, j + 1)) mc)
+
+let qualid_of_ref n =
+ n |> Coqlib.lib_ref |> Nametab.shortest_qualid_of_global Id.Set.empty
+
+let q_option () = qualid_of_ref "core.option.type"
+let q_list () = qualid_of_ref "core.list.type"
+let q_byte () = qualid_of_ref "core.byte.type"
+
+let has_type f ty =
+ let (sigma, env) = Pfedit.get_current_context () in
+ let c = mkCastC (mkRefC f, Glob_term.CastConv ty) in
+ try let _ = Constrintern.interp_constr env sigma c in true
+ with Pretype_errors.PretypeError _ -> false
+
+let type_error_to f ty =
+ CErrors.user_err
+ (pr_qualid f ++ str " should go from Byte.byte or (list Byte.byte) to " ++
+ pr_qualid ty ++ str " or (option " ++ pr_qualid ty ++ str ").")
+
+let type_error_of g ty =
+ CErrors.user_err
+ (pr_qualid g ++ str " should go from " ++ pr_qualid ty ++
+ str " to Byte.byte or (option Byte.byte) or (list Byte.byte) or (option (list Byte.byte)).")
+
+let vernac_string_notation local ty f g scope =
+ let app x y = mkAppC (x,[y]) in
+ let cref q = mkRefC q in
+ let cbyte = cref (q_byte ()) in
+ let clist = cref (q_list ()) in
+ let coption = cref (q_option ()) in
+ let opt r = app coption r in
+ let clist_byte = app clist cbyte 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
+ let cty = cref ty in
+ let arrow x y =
+ mkProdC ([CAst.make Anonymous],Default Decl_kinds.Explicit, x, y)
+ in
+ let constructors = get_constructors tyc in
+ (* Check the type of f *)
+ let to_kind =
+ if has_type f (arrow clist_byte cty) then ListByte, Direct
+ else if has_type f (arrow clist_byte (opt cty)) then ListByte, Option
+ else if has_type f (arrow cbyte cty) then Byte, Direct
+ else if has_type f (arrow cbyte (opt cty)) then Byte, Option
+ else type_error_to f ty
+ in
+ (* Check the type of g *)
+ let of_kind =
+ if has_type g (arrow cty clist_byte) then ListByte, Direct
+ else if has_type g (arrow cty (opt clist_byte)) then ListByte, Option
+ else if has_type g (arrow cty cbyte) then Byte, Direct
+ else if has_type g (arrow cty (opt cbyte)) then Byte, Option
+ else type_error_of g ty
+ in
+ let o = { to_kind = to_kind;
+ to_ty = to_ty;
+ of_kind = of_kind;
+ of_ty = of_ty;
+ ty_name = ty;
+ warning = () }
+ in
+ let i =
+ { pt_local = local;
+ pt_scope = scope;
+ pt_interp_info = StringNotation o;
+ pt_required = Nametab.path_of_global (IndRef tyc),[];
+ pt_refs = constructors;
+ pt_in_match = true }
+ in
+ enable_prim_token_interpretation i
diff --git a/plugins/syntax/string_notation.mli b/plugins/syntax/string_notation.mli
new file mode 100644
index 0000000000..9a0174abf2
--- /dev/null
+++ b/plugins/syntax/string_notation.mli
@@ -0,0 +1,16 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
+
+open Libnames
+open Vernacexpr
+
+(** * String notation *)
+
+val vernac_string_notation : locality_flag -> qualid -> qualid -> qualid -> Notation_term.scope_name -> unit
diff --git a/plugins/syntax/string_notation_plugin.mlpack b/plugins/syntax/string_notation_plugin.mlpack
new file mode 100644
index 0000000000..6aa081dab4
--- /dev/null
+++ b/plugins/syntax/string_notation_plugin.mlpack
@@ -0,0 +1,2 @@
+String_notation
+G_string
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 19:12:53 +0000