aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/syntax')
-rw-r--r--plugins/syntax/ascii_syntax.ml100
-rw-r--r--plugins/syntax/ascii_syntax_plugin.mlpack1
-rw-r--r--plugins/syntax/g_string.mlg25
-rw-r--r--plugins/syntax/numeral.ml2
-rw-r--r--plugins/syntax/plugin_base.dune22
-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
-rw-r--r--plugins/syntax/string_syntax.ml81
-rw-r--r--plugins/syntax/string_syntax_plugin.mlpack1
10 files changed, 149 insertions, 199 deletions
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
deleted file mode 100644
index 94255bab6c..0000000000
--- a/plugins/syntax/ascii_syntax.ml
+++ /dev/null
@@ -1,100 +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 = "ascii_syntax_plugin"
-let () = Mltop.add_known_module __coq_plugin_name
-
-open Pp
-open CErrors
-open Util
-open Names
-open Glob_term
-open Globnames
-open Coqlib
-
-exception Non_closed_ascii
-
-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 ascii_module = ["Coq";"Strings";"Ascii"]
-let ascii_modpath = MPfile (make_dir ascii_module)
-
-let ascii_path = make_path ascii_module "ascii"
-
-let ascii_label = Label.make "ascii"
-let ascii_kn = MutInd.make2 ascii_modpath ascii_label
-let path_of_Ascii = ((ascii_kn,0),1)
-let static_glob_Ascii = ConstructRef path_of_Ascii
-
-let glob_Ascii = lazy (lib_ref "plugins.syntax.Ascii")
-
-open Lazy
-
-let interp_ascii ?loc p =
- let rec aux n p =
- if Int.equal n 0 then [] else
- let mp = p mod 2 in
- (DAst.make ?loc @@ GRef (lib_ref (if Int.equal mp 0 then "core.bool.false" else "core.bool.true"),None))
- :: (aux (n-1) (p/2)) in
- DAst.make ?loc @@ GApp (DAst.make ?loc @@ GRef(force glob_Ascii,None), aux 8 p)
-
-let interp_ascii_string ?loc s =
- let p =
- if Int.equal (String.length s) 1 then int_of_char s.[0]
- else
- if Int.equal (String.length s) 3 && is_digit s.[0] && is_digit s.[1] && is_digit s.[2]
- then int_of_string s
- else
- user_err ?loc ~hdr:"interp_ascii_string"
- (str "Expects a single character or a three-digits ascii code.") in
- interp_ascii ?loc p
-
-let uninterp_ascii r =
- let rec uninterp_bool_list n = function
- | [] when Int.equal n 0 -> 0
- | r::l when is_gr r (lib_ref "core.bool.true") -> 1+2*(uninterp_bool_list (n-1) l)
- | r::l when is_gr r (lib_ref "core.bool.false") -> 2*(uninterp_bool_list (n-1) l)
- | _ -> raise Non_closed_ascii in
- try
- let aux c = match DAst.get c with
- | GApp (r, l) when is_gr r (force glob_Ascii) -> uninterp_bool_list 8 l
- | _ -> raise Non_closed_ascii in
- Some (aux r)
- with
- Non_closed_ascii -> None
-
-let make_ascii_string n =
- if n>=32 && n<=126 then String.make 1 (char_of_int n)
- else Printf.sprintf "%03d" n
-
-let uninterp_ascii_string (AnyGlobConstr r) = Option.map make_ascii_string (uninterp_ascii r)
-
-open Notation
-
-let at_declare_ml_module f x =
- Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name
-
-let _ =
- let sc = "char_scope" in
- register_string_interpretation sc (interp_ascii_string,uninterp_ascii_string);
- at_declare_ml_module enable_prim_token_interpretation
- { pt_local = false;
- pt_scope = sc;
- pt_interp_info = Uid sc;
- pt_required = (ascii_path,ascii_module);
- pt_refs = [static_glob_Ascii];
- pt_in_match = true }
diff --git a/plugins/syntax/ascii_syntax_plugin.mlpack b/plugins/syntax/ascii_syntax_plugin.mlpack
deleted file mode 100644
index 7b9213a0e2..0000000000
--- a/plugins/syntax/ascii_syntax_plugin.mlpack
+++ /dev/null
@@ -1 +0,0 @@
-Ascii_syntax
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/numeral.ml b/plugins/syntax/numeral.ml
index 10a0af0b8f..470deb4a60 100644
--- a/plugins/syntax/numeral.ml
+++ b/plugins/syntax/numeral.ml
@@ -125,7 +125,7 @@ let vernac_numeral_notation local ty f g scope opts =
| None -> type_error_of g ty true
in
let o = { to_kind; to_ty; of_kind; of_ty;
- num_ty = ty;
+ ty_name = ty;
warning = opts }
in
(match opts, to_kind with
diff --git a/plugins/syntax/plugin_base.dune b/plugins/syntax/plugin_base.dune
index bfdd480fe9..1ab16c700d 100644
--- a/plugins/syntax/plugin_base.dune
+++ b/plugins/syntax/plugin_base.dune
@@ -6,6 +6,13 @@
(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")
@@ -13,23 +20,8 @@
(libraries coq.vernac))
(library
- (name ascii_syntax_plugin)
- (public_name coq.plugins.ascii_syntax)
- (synopsis "Coq syntax plugin: ASCII")
- (modules ascii_syntax)
- (libraries coq.vernac))
-
-(library
- (name string_syntax_plugin)
- (public_name coq.plugins.string_syntax)
- (synopsis "Coq syntax plugin: strings")
- (modules string_syntax)
- (libraries coq.plugins.ascii_syntax))
-
-(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/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
diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
deleted file mode 100644
index 59e65a0672..0000000000
--- a/plugins/syntax/string_syntax.ml
+++ /dev/null
@@ -1,81 +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) *)
-(************************************************************************)
-
-open Names
-open Globnames
-open Ascii_syntax_plugin.Ascii_syntax
-open Glob_term
-open Coqlib
-
-(* Poor's man DECLARE PLUGIN *)
-let __coq_plugin_name = "string_syntax_plugin"
-let () = Mltop.add_known_module __coq_plugin_name
-
-exception Non_closed_string
-
-(* make a string term from the string s *)
-
-let string_module = ["Coq";"Strings";"String"]
-
-let string_modpath = MPfile (make_dir string_module)
-let string_path = make_path string_module "string"
-
-let string_kn = MutInd.make2 string_modpath @@ Label.make "string"
-let static_glob_EmptyString = ConstructRef ((string_kn,0),1)
-let static_glob_String = ConstructRef ((string_kn,0),2)
-
-let glob_String = lazy (lib_ref "plugins.syntax.String")
-let glob_EmptyString = lazy (lib_ref "plugins.syntax.EmptyString")
-
-let is_gr c gr = match DAst.get c with
-| GRef (r, _) -> GlobRef.equal r gr
-| _ -> false
-
-open Lazy
-
-let interp_string ?loc s =
- let le = String.length s in
- let rec aux n =
- if n = le then DAst.make ?loc @@ GRef (force glob_EmptyString, None) else
- DAst.make ?loc @@ GApp (DAst.make ?loc @@ GRef (force glob_String, None),
- [interp_ascii ?loc (int_of_char s.[n]); aux (n+1)])
- in aux 0
-
-let uninterp_string (AnyGlobConstr r) =
- try
- let b = Buffer.create 16 in
- let rec aux c = match DAst.get c with
- | GApp (k,[a;s]) when is_gr k (force glob_String) ->
- (match uninterp_ascii a with
- | Some c -> Buffer.add_char b (Char.chr c); aux s
- | _ -> raise Non_closed_string)
- | GRef (z,_) when GlobRef.equal z (force glob_EmptyString) ->
- Some (Buffer.contents b)
- | _ ->
- raise Non_closed_string
- in aux r
- with
- Non_closed_string -> None
-
-open Notation
-
-let at_declare_ml_module f x =
- Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name
-
-let _ =
- let sc = "string_scope" in
- register_string_interpretation sc (interp_string,uninterp_string);
- at_declare_ml_module enable_prim_token_interpretation
- { pt_local = false;
- pt_scope = sc;
- pt_interp_info = Uid sc;
- pt_required = (string_path,["Coq";"Strings";"String"]);
- pt_refs = [static_glob_String; static_glob_EmptyString];
- pt_in_match = true }
diff --git a/plugins/syntax/string_syntax_plugin.mlpack b/plugins/syntax/string_syntax_plugin.mlpack
deleted file mode 100644
index 45d6e0fa23..0000000000
--- a/plugins/syntax/string_syntax_plugin.mlpack
+++ /dev/null
@@ -1 +0,0 @@
-String_syntax
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:28:26 +0000