From b6214bd4d5d3003e9b60411a717e84277feead24 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 3 Sep 2020 13:27:00 +0200 Subject: [string notation] Handle parameterized inductives and non inductives --- plugins/syntax/g_number_string.mlg | 32 ++++++++++++++++++++------------ plugins/syntax/number.mli | 5 +++++ plugins/syntax/string_notation.ml | 27 +++++++++++---------------- plugins/syntax/string_notation.mli | 4 +++- 4 files changed, 39 insertions(+), 29 deletions(-) (limited to 'plugins/syntax') diff --git a/plugins/syntax/g_number_string.mlg b/plugins/syntax/g_number_string.mlg index b584505530..c8badd238d 100644 --- a/plugins/syntax/g_number_string.mlg +++ b/plugins/syntax/g_number_string.mlg @@ -32,7 +32,7 @@ let warn_deprecated_numeral_notation = (fun () -> strbrk "Numeral Notation is deprecated, please use Number Notation instead.") -let pr_number_mapping (b, n, n') = +let pr_number_string_mapping (b, n, n') = if b then str "[" ++ Libnames.pr_qualid n ++ str "]" ++ spc () ++ str "=>" ++ spc () ++ Libnames.pr_qualid n' @@ -40,17 +40,20 @@ let pr_number_mapping (b, n, n') = Libnames.pr_qualid n ++ spc () ++ str "=>" ++ spc () ++ Libnames.pr_qualid n' -let pr_number_via (n, l) = +let pr_number_string_via (n, l) = str "via " ++ Libnames.pr_qualid n ++ str " mapping [" - ++ prlist_with_sep pr_comma pr_number_mapping l ++ str "]" + ++ prlist_with_sep pr_comma pr_number_string_mapping l ++ str "]" let pr_number_modifier = function | After a -> pr_number_after a - | Via nl -> pr_number_via nl + | Via nl -> pr_number_string_via nl let pr_number_options l = str "(" ++ prlist_with_sep pr_comma pr_number_modifier l ++ str ")" +let pr_string_option l = + str "(" ++ pr_number_string_via l ++ str ")" + } VERNAC ARGUMENT EXTEND deprecated_number_modifier @@ -60,22 +63,22 @@ VERNAC ARGUMENT EXTEND deprecated_number_modifier | [ "(" "abstract" "after" bignat(n) ")" ] -> { Abstract (NumTok.UnsignedNat.of_string n) } END -VERNAC ARGUMENT EXTEND number_mapping - PRINTED BY { pr_number_mapping } +VERNAC ARGUMENT EXTEND number_string_mapping + PRINTED BY { pr_number_string_mapping } | [ reference(n) "=>" reference(n') ] -> { false, n, n' } | [ "[" reference(n) "]" "=>" reference(n') ] -> { true, n, n' } END -VERNAC ARGUMENT EXTEND number_via - PRINTED BY { pr_number_via } -| [ "via" reference(n) "mapping" "[" ne_number_mapping_list_sep(l, ",") "]" ] -> { n, l } +VERNAC ARGUMENT EXTEND number_string_via + PRINTED BY { pr_number_string_via } +| [ "via" reference(n) "mapping" "[" ne_number_string_mapping_list_sep(l, ",") "]" ] -> { n, l } END VERNAC ARGUMENT EXTEND number_modifier PRINTED BY { pr_number_modifier } | [ "warning" "after" bignat(waft) ] -> { After (Warning (NumTok.UnsignedNat.of_string waft)) } | [ "abstract" "after" bignat(n) ] -> { After (Abstract (NumTok.UnsignedNat.of_string n)) } -| [ number_via(v) ] -> { Via v } +| [ number_string_via(v) ] -> { Via v } END VERNAC ARGUMENT EXTEND number_options @@ -83,6 +86,11 @@ VERNAC ARGUMENT EXTEND number_options | [ "(" ne_number_modifier_list_sep(l, ",") ")" ] -> { l } END +VERNAC ARGUMENT EXTEND string_option + PRINTED BY { pr_string_option } +| [ "(" number_string_via(v) ")" ] -> { v } +END + VERNAC COMMAND EXTEND NumberNotation CLASSIFIED AS SIDEFF | #[ locality = Attributes.locality; ] [ "Number" "Notation" reference(ty) reference(f) reference(g) number_options_opt(nl) ":" ident(sc) ] -> @@ -96,7 +104,7 @@ VERNAC COMMAND EXTEND NumberNotation CLASSIFIED AS SIDEFF END VERNAC COMMAND EXTEND StringNotation CLASSIFIED AS SIDEFF - | #[ locality = Attributes.locality; ] [ "String" "Notation" reference(ty) reference(f) reference(g) ":" + | #[ locality = Attributes.locality; ] [ "String" "Notation" reference(ty) reference(f) reference(g) string_option_opt(o) ":" ident(sc) ] -> - { vernac_string_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) } + { vernac_string_notation (Locality.make_module_locality locality) ty f g o (Id.to_string sc) } END diff --git a/plugins/syntax/number.mli b/plugins/syntax/number.mli index 5a13d1068b..d7d28b29ed 100644 --- a/plugins/syntax/number.mli +++ b/plugins/syntax/number.mli @@ -24,3 +24,8 @@ val vernac_number_notation : locality_flag -> qualid -> qualid -> number_option list -> Notation_term.scope_name -> unit + +(** These are also used in string notations *) +val locate_global_inductive : bool -> Libnames.qualid -> Names.inductive * Names.GlobRef.t option list +val elaborate_to_post_params : Environ.env -> Evd.evar_map -> Names.inductive -> Names.GlobRef.t option list -> (Names.GlobRef.t * Names.GlobRef.t * Notation.to_post_arg list) list array * Names.GlobRef.t list +val elaborate_to_post_via : Environ.env -> Evd.evar_map -> Libnames.qualid -> Names.inductive -> (bool * Libnames.qualid * Libnames.qualid) list -> (Names.GlobRef.t * Names.GlobRef.t * Notation.to_post_arg list) list array * Names.GlobRef.t list diff --git a/plugins/syntax/string_notation.ml b/plugins/syntax/string_notation.ml index 98ea318c92..774d59dda3 100644 --- a/plugins/syntax/string_notation.ml +++ b/plugins/syntax/string_notation.ml @@ -14,15 +14,10 @@ open Libnames open Constrexpr open Constrexpr_ops open Notation +open Number (** * 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 -> GlobRef.ConstructRef (ind, j + 1)) mc) - let qualid_of_ref n = n |> Coqlib.lib_ref |> Nametab.shortest_qualid_of_global Id.Set.empty @@ -45,7 +40,7 @@ let type_error_of g ty = (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 vernac_string_notation local ty f g via scope = let env = Global.env () in let sigma = Evd.from_env env in let app x y = mkAppC (x,[y]) in @@ -55,14 +50,16 @@ let vernac_string_notation local ty f g scope = 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 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 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 Glob_term.Explicit, x, y) in - let constructors = get_constructors tyc in (* Check the type of f *) let to_kind = if has_type env sigma f (arrow clist_byte cty) then ListByte, Direct @@ -79,12 +76,10 @@ let vernac_string_notation local ty f g scope = else if has_type env sigma 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; - to_post = [||]; - of_kind = of_kind; - of_ty = of_ty; - ty_name = ty; + 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 o = { to_kind; to_ty; to_post; of_kind; of_ty; ty_name; warning = () } in let i = @@ -92,7 +87,7 @@ let vernac_string_notation local ty f g scope = pt_scope = scope; pt_interp_info = StringNotation o; pt_required = Nametab.path_of_global (GlobRef.IndRef tyc),[]; - pt_refs = constructors; + pt_refs; pt_in_match = true } in enable_prim_token_interpretation i diff --git a/plugins/syntax/string_notation.mli b/plugins/syntax/string_notation.mli index 0d99f98d26..f3c7c969c6 100644 --- a/plugins/syntax/string_notation.mli +++ b/plugins/syntax/string_notation.mli @@ -14,5 +14,7 @@ open Vernacexpr (** * String notation *) val vernac_string_notation : locality_flag -> - qualid -> qualid -> qualid -> + qualid -> + qualid -> qualid -> + Number.number_string_via option -> Notation_term.scope_name -> unit -- cgit v1.2.3