From 2d44c8246eccba7c1c452cbfbc6751cd222d0a6a Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sat, 12 Sep 2020 09:10:26 +0200 Subject: Renaming Numeral.v into Number.v --- plugins/syntax/numeral.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins') diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml index 2db76719b8..fbf43be91f 100644 --- a/plugins/syntax/numeral.ml +++ b/plugins/syntax/numeral.ml @@ -64,7 +64,7 @@ let locate_numeral () = let hex = "num.hexadecimal.type" in let int = "num.num_int.type" in let uint = "num.num_uint.type" in - let num = "num.numeral.type" in + let num = "num.number.type" in if Coqlib.has_ref dint && Coqlib.has_ref duint && Coqlib.has_ref dec && Coqlib.has_ref hint && Coqlib.has_ref huint && Coqlib.has_ref hex && Coqlib.has_ref int && Coqlib.has_ref uint && Coqlib.has_ref num -- cgit v1.2.3 From 3a25b967a944fe37e1ad54e54a904d90311ef381 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sat, 12 Sep 2020 09:13:44 +0200 Subject: Renaming numnotoption into number_modifier --- plugins/syntax/g_numeral.mlg | 16 ++++++++-------- plugins/syntax/numeral.ml | 22 +++++++++++----------- plugins/syntax/numeral.mli | 8 ++++---- 3 files changed, 23 insertions(+), 23 deletions(-) (limited to 'plugins') diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg index 93d91abea3..48e262c3ef 100644 --- a/plugins/syntax/g_numeral.mlg +++ b/plugins/syntax/g_numeral.mlg @@ -19,7 +19,7 @@ open Names open Stdarg open Pcoq.Prim -let pr_numnot_option = function +let pr_number_modifier = function | Nop -> mt () | Warning n -> str "(warning after " ++ NumTok.UnsignedNat.print n ++ str ")" | Abstract n -> str "(abstract after " ++ NumTok.UnsignedNat.print n ++ str ")" @@ -31,21 +31,21 @@ let warn_deprecated_numeral_notation = } -VERNAC ARGUMENT EXTEND numeral_modifier - PRINTED BY { pr_numnot_option } +VERNAC ARGUMENT EXTEND number_modifier + PRINTED BY { pr_number_modifier } | [ ] -> { Nop } | [ "(" "warning" "after" bignat(waft) ")" ] -> { Warning (NumTok.UnsignedNat.of_string waft) } | [ "(" "abstract" "after" bignat(n) ")" ] -> { Abstract (NumTok.UnsignedNat.of_string n) } END -VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF +VERNAC COMMAND EXTEND NumberNotation CLASSIFIED AS SIDEFF | #[ locality = Attributes.locality; ] [ "Number" "Notation" reference(ty) reference(f) reference(g) ":" - ident(sc) numeral_modifier(o) ] -> + ident(sc) number_modifier(o) ] -> - { vernac_numeral_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) o } + { vernac_number_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) o } | #[ locality = Attributes.locality; ] [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" - ident(sc) numeral_modifier(o) ] -> + ident(sc) number_modifier(o) ] -> { warn_deprecated_numeral_notation (); - vernac_numeral_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) o } + vernac_number_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) o } END diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml index fbf43be91f..313798b102 100644 --- a/plugins/syntax/numeral.ml +++ b/plugins/syntax/numeral.ml @@ -16,7 +16,7 @@ open Constrexpr open Constrexpr_ops open Notation -(** * Numeral notation *) +(** * Number notation *) let warn_abstract_large_num_no_op = CWarnings.create ~name:"abstract-large-number-no-op" ~category:"numbers" @@ -55,7 +55,7 @@ let locate_z () = }, mkRefC q_z) else None -let locate_numeral () = +let locate_number () = let dint = "num.int.type" in let duint = "num.uint.type" in let dec = "num.decimal.type" in @@ -111,27 +111,27 @@ let has_type env sigma f ty = let type_error_to f ty = CErrors.user_err - (pr_qualid f ++ str " should go from Numeral.int to " ++ + (pr_qualid f ++ str " should go from Number.int to " ++ pr_qualid ty ++ str " or (option " ++ pr_qualid ty ++ str ")." ++ - fnl () ++ str "Instead of Numeral.int, the types Numeral.uint or Z or Int63.int or Numeral.numeral could be used (you may need to require BinNums or Numeral or Int63 first).") + 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).") let type_error_of g ty = CErrors.user_err (pr_qualid g ++ str " should go from " ++ pr_qualid ty ++ - str " to Numeral.int or (option Numeral.int)." ++ fnl () ++ - str "Instead of Numeral.int, the types Numeral.uint or Z or Int63.int or Numeral.numeral could be used (you may need to require BinNums or Numeral or Int63 first).") + 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).") let warn_deprecated_decimal = CWarnings.create ~name:"decimal-numeral-notation" ~category:"deprecated" (fun () -> - strbrk "Deprecated Numeral Notation for Decimal.uint, \ - Decimal.int or Decimal.decimal. Use Numeral.uint, \ - Numeral.int or Numeral.numeral respectively.") + strbrk "Deprecated Number Notation for Decimal.uint, \ + Decimal.int or Decimal.decimal. Use Number.uint, \ + Number.int or Number.number respectively.") -let vernac_numeral_notation local ty f g scope opts = +let vernac_number_notation local ty f g scope opts = let env = Global.env () in let sigma = Evd.from_env env in - let num_ty = locate_numeral () in + let num_ty = locate_number () in let z_pos_ty = locate_z () in let int63_ty = locate_int63 () in let tyc = Smartlocate.global_inductive_with_alias ty in diff --git a/plugins/syntax/numeral.mli b/plugins/syntax/numeral.mli index 99252484b4..d5fe42b0b4 100644 --- a/plugins/syntax/numeral.mli +++ b/plugins/syntax/numeral.mli @@ -12,8 +12,8 @@ open Libnames open Vernacexpr open Notation -(** * Numeral notation *) +(** * Number notation *) -val vernac_numeral_notation : locality_flag -> - qualid -> qualid -> qualid -> - Notation_term.scope_name -> numnot_option -> unit +val vernac_number_notation : locality_flag -> + qualid -> qualid -> qualid -> + Notation_term.scope_name -> numnot_option -> unit -- cgit v1.2.3 From da72fafac3b5b4b21330cd097f5728cbc127aea4 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sat, 12 Sep 2020 09:15:06 +0200 Subject: Renaming Numeral into Number --- plugins/ltac/g_tactic.mlg | 6 +++--- plugins/ssr/ssrparser.mlg | 2 +- plugins/syntax/int63_syntax.ml | 2 +- plugins/syntax/numeral.ml | 12 ++++++------ 4 files changed, 11 insertions(+), 11 deletions(-) (limited to 'plugins') diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index 97d75261c5..ecfe6c1664 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -121,8 +121,8 @@ let destruction_arg_of_constr (c,lbind as clbind) = match lbind with end | _ -> ElimOnConstr clbind -let mkNumeral n = - Numeral (NumTok.Signed.of_int_string (string_of_int n)) +let mkNumber n = + Number (NumTok.Signed.of_int_string (string_of_int n)) let mkTacCase with_evar = function | [(clear,ElimOnConstr cl),(None,None),None],None -> @@ -130,7 +130,7 @@ let mkTacCase with_evar = function (* Reinterpret numbers as a notation for terms *) | [(clear,ElimOnAnonHyp n),(None,None),None],None -> TacCase (with_evar, - (clear,(CAst.make @@ CPrim (mkNumeral n), + (clear,(CAst.make @@ CPrim (mkNumber n), NoBindings))) (* Reinterpret ident as notations for variables in the context *) (* because we don't know if they are quantified or not *) diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 35fecfb0a5..ccdf5fa68e 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -350,7 +350,7 @@ let interp_index ist gl idx = | Some c -> let rc = Detyping.detype Detyping.Now false Id.Set.empty (pf_env gl) (project gl) c in begin match Notation.uninterp_prim_token rc (None, []) with - | Constrexpr.Numeral n, _ when NumTok.Signed.is_int n -> + | Constrexpr.Number n, _ when NumTok.Signed.is_int n -> int_of_string (NumTok.Signed.to_string n) | _ -> raise Not_found end diff --git a/plugins/syntax/int63_syntax.ml b/plugins/syntax/int63_syntax.ml index 5f4db8e800..73a9341145 100644 --- a/plugins/syntax/int63_syntax.ml +++ b/plugins/syntax/int63_syntax.ml @@ -50,7 +50,7 @@ let _ = enable_prim_token_interpretation { pt_local = false; pt_scope = int63_scope; - pt_interp_info = NumeralNotation o; + pt_interp_info = NumberNotation o; pt_required = (int63_path, int63_module); pt_refs = []; pt_in_match = false }) diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml index 313798b102..8635f39f1a 100644 --- a/plugins/syntax/numeral.ml +++ b/plugins/syntax/numeral.ml @@ -90,7 +90,7 @@ let locate_number () = int = int_ty; decimal = unsafe_locate_ind q_dec; hexadecimal = unsafe_locate_ind q_hex; - numeral = unsafe_locate_ind q_num; + number = unsafe_locate_ind q_num; } in Some (int_ty, mkRefC q_int, mkRefC q_uint, mkRefC q_dint, mkRefC q_duint, num_ty, mkRefC q_num, mkRefC q_dec) @@ -151,8 +151,8 @@ let vernac_number_notation local ty f g scope opts = | Some (int_ty, cint, _, _, _, _, _, _) when has_type env sigma f (arrow cint (opt cty)) -> Int int_ty, Option | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma f (arrow cuint cty) -> UInt int_ty, Direct | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma f (arrow cuint (opt cty)) -> UInt int_ty, Option - | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma f (arrow cnum cty) -> Numeral num_ty, Direct - | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma f (arrow cnum (opt cty)) -> Numeral num_ty, Option + | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma f (arrow cnum cty) -> Number num_ty, Direct + | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma f (arrow cnum (opt cty)) -> Number num_ty, Option | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma f (arrow cint cty) -> DecimalInt int_ty, Direct | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma f (arrow cint (opt cty)) -> DecimalInt int_ty, Option | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma f (arrow cuint cty) -> DecimalUInt int_ty, Direct @@ -176,8 +176,8 @@ let vernac_number_notation local ty f g scope opts = | Some (int_ty, cint, _, _, _, _, _, _) when has_type env sigma g (arrow cty (opt cint)) -> Int int_ty, Option | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma g (arrow cty cuint) -> UInt int_ty, Direct | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma g (arrow cty (opt cuint)) -> UInt int_ty, Option - | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma g (arrow cty cnum) -> Numeral num_ty, Direct - | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma g (arrow cty (opt cnum)) -> Numeral num_ty, Option + | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma g (arrow cty cnum) -> Number num_ty, Direct + | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma g (arrow cty (opt cnum)) -> Number num_ty, Option | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma g (arrow cty cint) -> DecimalInt int_ty, Direct | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma g (arrow cty (opt cint)) -> DecimalInt int_ty, Option | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma g (arrow cty cuint) -> DecimalUInt int_ty, Direct @@ -209,7 +209,7 @@ let vernac_number_notation local ty f g scope opts = let i = { pt_local = local; pt_scope = scope; - pt_interp_info = NumeralNotation o; + pt_interp_info = NumberNotation o; pt_required = Nametab.path_of_global (GlobRef.IndRef tyc),[]; pt_refs = constructors; pt_in_match = true } -- cgit v1.2.3 From dfcb15141a19db4f1cc61c14d1cdad0275009356 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 3 Sep 2020 13:11:00 +0200 Subject: [numeral notation] Add a pre/postprocessing This will enable to define numeral notation on non inductive by using an inductive type as proxy and those translations to translate to/from the actual type to the inductive type. --- plugins/syntax/int63_syntax.ml | 1 + plugins/syntax/numeral.ml | 2 +- plugins/syntax/string_notation.ml | 1 + 3 files changed, 3 insertions(+), 1 deletion(-) (limited to 'plugins') diff --git a/plugins/syntax/int63_syntax.ml b/plugins/syntax/int63_syntax.ml index 73a9341145..b14b02f3bb 100644 --- a/plugins/syntax/int63_syntax.ml +++ b/plugins/syntax/int63_syntax.ml @@ -43,6 +43,7 @@ let _ = 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; diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml index 8635f39f1a..ad90a9a982 100644 --- a/plugins/syntax/numeral.ml +++ b/plugins/syntax/numeral.ml @@ -199,7 +199,7 @@ let vernac_number_notation local ty f g scope opts = | _, ((DecimalInt _ | DecimalUInt _ | Decimal _), _) -> warn_deprecated_decimal () | _ -> ()); - let o = { to_kind; to_ty; of_kind; of_ty; + let o = { to_kind; to_ty; to_post = [||]; of_kind; of_ty; ty_name = ty; warning = opts } in diff --git a/plugins/syntax/string_notation.ml b/plugins/syntax/string_notation.ml index e7ed0d8061..dbb0e92d5c 100644 --- a/plugins/syntax/string_notation.ml +++ b/plugins/syntax/string_notation.ml @@ -82,6 +82,7 @@ let vernac_string_notation local ty f g scope = in let o = { to_kind = to_kind; to_ty = to_ty; + to_post = [||]; of_kind = of_kind; of_ty = of_ty; ty_name = ty; -- cgit v1.2.3 From 11a8997dd8fa83537607272692a3baf10dab342a Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 3 Sep 2020 13:12:00 +0200 Subject: [numeral notation] Adding the via ... using ... option This enables numeral notations for non inductive types by pre/postprocessing them to a given proxy inductive type. For instance, this should enable the use of numeral notations for R. --- plugins/syntax/g_numeral.mlg | 58 +++++++++-- plugins/syntax/numeral.ml | 233 ++++++++++++++++++++++++++++++++++++++++++- plugins/syntax/numeral.mli | 11 +- 3 files changed, 285 insertions(+), 17 deletions(-) (limited to 'plugins') diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg index 48e262c3ef..e60ae45b01 100644 --- a/plugins/syntax/g_numeral.mlg +++ b/plugins/syntax/g_numeral.mlg @@ -19,33 +19,71 @@ open Names open Stdarg open Pcoq.Prim -let pr_number_modifier = function +let pr_number_after = function | Nop -> mt () - | Warning n -> str "(warning after " ++ NumTok.UnsignedNat.print n ++ str ")" - | Abstract n -> str "(abstract after " ++ NumTok.UnsignedNat.print n ++ str ")" + | Warning n -> str "warning after " ++ NumTok.UnsignedNat.print n + | Abstract n -> str "abstract after " ++ NumTok.UnsignedNat.print n + +let pr_deprecated_number_modifier m = str "(" ++ pr_number_after m ++ str ")" let warn_deprecated_numeral_notation = CWarnings.create ~name:"numeral-notation" ~category:"deprecated" (fun () -> strbrk "Numeral Notation is deprecated, please use Number Notation instead.") +let pr_number_mapping (n, n') = + Libnames.pr_qualid n ++ spc () ++ str "=>" ++ spc () ++ Libnames.pr_qualid n' + +let pr_number_via (n, l) = + str "via " ++ Libnames.pr_qualid n ++ str " mapping [" + ++ prlist_with_sep pr_comma pr_number_mapping l ++ str "]" + +let pr_number_modifier = function + | After a -> pr_number_after a + | Via nl -> pr_number_via nl + +let pr_number_options l = + str "(" ++ prlist_with_sep pr_comma pr_number_modifier l ++ str ")" + } -VERNAC ARGUMENT EXTEND number_modifier - PRINTED BY { pr_number_modifier } +VERNAC ARGUMENT EXTEND deprecated_number_modifier + PRINTED BY { pr_deprecated_number_modifier } | [ ] -> { Nop } | [ "(" "warning" "after" bignat(waft) ")" ] -> { Warning (NumTok.UnsignedNat.of_string waft) } | [ "(" "abstract" "after" bignat(n) ")" ] -> { Abstract (NumTok.UnsignedNat.of_string n) } END +VERNAC ARGUMENT EXTEND number_mapping + PRINTED BY { pr_number_mapping } +| [ reference(n) "=>" reference(n') ] -> { 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 } +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 } +END + +VERNAC ARGUMENT EXTEND number_options + PRINTED BY { pr_number_options } +| [ "(" ne_number_modifier_list_sep(l, ",") ")" ] -> { l } +END + VERNAC COMMAND EXTEND NumberNotation CLASSIFIED AS SIDEFF - | #[ locality = Attributes.locality; ] [ "Number" "Notation" reference(ty) reference(f) reference(g) ":" - ident(sc) number_modifier(o) ] -> + | #[ locality = Attributes.locality; ] [ "Number" "Notation" reference(ty) reference(f) reference(g) number_options_opt(nl) ":" + ident(sc) ] -> - { vernac_number_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) o } + { vernac_number_notation (Locality.make_module_locality locality) ty f g (Option.default [] nl) (Id.to_string sc) } | #[ locality = Attributes.locality; ] [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" - ident(sc) number_modifier(o) ] -> + ident(sc) deprecated_number_modifier(o) ] -> { warn_deprecated_numeral_notation (); - vernac_number_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) o } + vernac_number_notation (Locality.make_module_locality locality) ty f g [After o] (Id.to_string sc) } END diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml index ad90a9a982..316ca456a4 100644 --- a/plugins/syntax/numeral.ml +++ b/plugins/syntax/numeral.ml @@ -16,8 +16,16 @@ open Constrexpr open Constrexpr_ops open Notation +module CSet = CSet.Make (Constr) +module CMap = CMap.Make (Constr) + (** * Number notation *) +type number_string_via = qualid * (qualid * qualid) list +type number_option = + | After of numnot_option + | Via of number_string_via + let warn_abstract_large_num_no_op = CWarnings.create ~name:"abstract-large-number-no-op" ~category:"numbers" (fun f -> @@ -128,12 +136,228 @@ let warn_deprecated_decimal = Decimal.int or Decimal.decimal. Use Number.uint, \ Number.int or Number.number respectively.") -let vernac_number_notation local ty f g scope opts = +let remapping_error ?loc ty ty' ty'' = + CErrors.user_err ?loc + (Printer.pr_global ty + ++ str " was already mapped to" ++ spc () ++ Printer.pr_global ty' + ++ str " and cannot be remapped to" ++ spc () ++ Printer.pr_global ty'' + ++ str ".") + +let error_missing c = + CErrors.user_err + (str "Missing mapping for constructor " ++ Printer.pr_global c ++ str ".") + +let pr_constr env sigma c = + let c = Constrextern.extern_constr env sigma (EConstr.of_constr c) in + Ppconstr.pr_constr_expr env sigma c + +let warn_via_remapping = + CWarnings.create ~name:"via-type-remapping" ~category:"numbers" + (fun (env, sigma, ty, ty', ty'') -> + let constr = pr_constr env sigma in + constr ty ++ str " was already mapped to" ++ spc () ++ constr ty' + ++ str ", mapping it also to" ++ spc () ++ constr ty'' + ++ str " might yield ill typed terms when using the notation.") + +let warn_via_type_mismatch = + CWarnings.create ~name:"via-type-mismatch" ~category:"numbers" + (fun (env, sigma, g, g', exp, actual) -> + let constr = pr_constr env sigma in + str "Type of" ++ spc() ++ Printer.pr_global g + ++ str " seems incompatible with the type of" ++ spc () + ++ Printer.pr_global g' ++ str "." ++ spc () + ++ str "Expected type is: " ++ constr exp ++ spc () + ++ str "instead of " ++ constr actual ++ str "." ++ spc () + ++ str "This might yield ill typed terms when using the notation.") + +let multiple_via_error () = + CErrors.user_err (Pp.str "Multiple 'via' options.") + +let multiple_after_error () = + CErrors.user_err (Pp.str "Multiple 'warning after' or 'abstract after' options.") + +let via_abstract_error () = + CErrors.user_err (Pp.str "'via' and 'abstract' cannot be used together.") + +let locate_global_sort_inductive_or_constant sigma qid = + let locate_sort qid = + match Nametab.locate_extended qid with + | Globnames.TrueGlobal _ -> raise Not_found + | Globnames.SynDef kn -> + match Syntax_def.search_syntactic_definition kn with + | [], Notation_term.NSort r -> + let sigma,c = Evd.fresh_sort_in_family sigma (Glob_ops.glob_sort_family r) in + sigma,Constr.mkSort c + | _ -> raise Not_found in + try locate_sort qid + with Not_found -> + match Smartlocate.global_with_alias qid with + | GlobRef.IndRef i -> sigma, Constr.mkInd i + | _ -> sigma, Constr.mkConst (Smartlocate.global_constant_with_alias qid) + +let locate_global_constructor_inductive_or_constant qid = + let g = Smartlocate.global_with_alias qid in + match g with + | GlobRef.ConstructRef c -> g, Constr.mkConstruct c + | GlobRef.IndRef i -> g, Constr.mkInd i + | _ -> g, Constr.mkConst (Smartlocate.global_constant_with_alias qid) + +(* [get_type env sigma c] retrieves the type of [c] and returns a pair + [l, t] such that [c : l_0 -> ... -> l_n -> t]. *) +let get_type env sigma c = + (* inspired from [compute_implicit_names] in "interp/impargs.ml" *) + let rec aux env acc t = + let t = Reductionops.whd_all env sigma t in + match EConstr.kind sigma t with + | Constr.Prod (na, a, b) -> + let a = Reductionops.whd_all env sigma a in + let rel = Context.Rel.Declaration.LocalAssum (na, a) in + aux (EConstr.push_rel rel env) ((na, a) :: acc) b + | _ -> List.rev acc, t in + let t = Retyping.get_type_of env sigma (EConstr.of_constr c) in + let l, t = aux env [] t in + List.map (fun (na, a) -> na, EConstr.Unsafe.to_constr a) l, + EConstr.Unsafe.to_constr t + +(* [elaborate_to_post env sigma ty_name ty_ind l] builds the [to_post] + translation (c.f., interp/notation.mli) for the number notation to + parse/print type [ty_name] through the inductive [ty_ind] according + to the pairs [constant, constructor] in the list [l]. *) +let elaborate_to_post env sigma ty_name ty_ind l = + let sigma, ty_name = + locate_global_sort_inductive_or_constant sigma ty_name in + let ty_ind = Constr.mkInd ty_ind in + (* Retrieve constants and constructors mappings and their type. + For each constant [cnst] and inductive constructor [indc] in [l], retrieve: + * its location: [lcnst] and [lindc] + * its GlobRef: [cnst] and [indc] + * its type: [tcnst] and [tindc] (decomposed in product by [get_type] above) *) + let l = + let read (cnst, indc) = + let lcnst, lindc = cnst.CAst.loc, indc.CAst.loc in + let cnst, ccnst = locate_global_constructor_inductive_or_constant cnst in + let indc, cindc = + let indc = Smartlocate.global_constructor_with_alias indc in + GlobRef.ConstructRef indc, Constr.mkConstruct indc in + let get_type_wo_params c = + (* ignore parameters of inductive types *) + let rm_params c = match Constr.kind c with + | Constr.App (c, _) when Constr.isInd c -> c + | _ -> c in + let lc, tc = get_type env sigma c in + List.map (fun (n, c) -> n, rm_params c) lc, rm_params tc in + let tcnst, tindc = get_type_wo_params ccnst, get_type_wo_params cindc in + lcnst, cnst, tcnst, lindc, indc, tindc in + List.map read l in + let eq_indc indc (_, _, _, _, indc', _) = GlobRef.equal indc indc' in + (* Collect all inductive types involved. + That is [ty_ind] and all final codomains of [tindc] above. *) + let inds = + List.fold_left (fun s (_, _, _, _, _, tindc) -> CSet.add (snd tindc) s) + (CSet.singleton ty_ind) l in + (* And for each inductive, retrieve its constructors. *) + let constructors = + CSet.fold (fun ind m -> + let inductive, _ = Constr.destInd ind in + CMap.add ind (get_constructors inductive) m) + inds CMap.empty in + (* Error if one [constructor] in some inductive in [inds] + doesn't appear exactly once in [l] *) + let _ = (* check_for duplicate constructor and error *) + List.fold_left (fun already_seen (_, cnst, _, loc, indc, _) -> + try + let cnst' = List.assoc_f GlobRef.equal indc already_seen in + remapping_error ?loc indc cnst' cnst + with Not_found -> (indc, cnst) :: already_seen) + [] l in + let () = (* check for missing constructor and error *) + CMap.iter (fun _ -> + List.iter (fun cstr -> + if not (List.exists (eq_indc cstr) l) then error_missing cstr)) + constructors in + (* Perform some checks on types and warn if they look strange. + These checks are neither sound nor complete, so we only warn. *) + let () = + (* associate inductives to types, and check that this mapping is one to one + and maps [ty_ind] to [ty_name] *) + let ind2ty, ty2ind = + let add loc ckey cval m = + match CMap.find_opt ckey m with + | None -> CMap.add ckey cval m + | Some old_cval -> + if not (Constr.equal old_cval cval) then + warn_via_remapping ?loc (env, sigma, ckey, old_cval, cval); + m in + List.fold_left + (fun (ind2ty, ty2ind) (lcnst, _, (_, tcnst), lindc, _, (_, tindc)) -> + add lcnst tindc tcnst ind2ty, add lindc tcnst tindc ty2ind) + CMap.(singleton ty_ind ty_name, singleton ty_name ty_ind) l in + (* check that type of constants and constructors mapped in [l] + match modulo [ind2ty] *) + let replace m (l, t) = + let apply_m c = try CMap.find c m with Not_found -> c in + List.fold_right (fun (na, a) b -> Constr.mkProd (na, (apply_m a), b)) + l (apply_m t) in + List.iter (fun (_, cnst, tcnst, loc, indc, tindc) -> + let tcnst' = replace CMap.empty tcnst in + if not (Constr.equal tcnst' (replace ind2ty tindc)) then + let actual = replace CMap.empty tindc in + let expected = replace ty2ind tcnst in + warn_via_type_mismatch ?loc (env, sigma, indc, cnst, expected, actual)) + l in + (* Associate an index to each inductive, starting from 0 for [ty_ind]. *) + let ind2num, num2ind, nb_ind = + CMap.fold (fun ind _ (ind2num, num2ind, i) -> + CMap.add ind i ind2num, Int.Map.add i ind num2ind, i + 1) + (CMap.remove ty_ind constructors) + (CMap.singleton ty_ind 0, Int.Map.singleton 0 ty_ind, 1) in + (* Finally elaborate [to_post] *) + let to_post = + let rec map_prod = function + | [] -> [] + | (_, a) :: b -> + let t = match CMap.find_opt a ind2num with + | Some i -> ToPostAs i + | None -> ToPostCopy in + t :: map_prod b in + Array.init nb_ind (fun i -> + List.map (fun indc -> + let _, cnst, _, _, _, tindc = List.find (eq_indc indc) l in + indc, cnst, map_prod (fst tindc)) + (CMap.find (Int.Map.find i num2ind) constructors)) in + (* and use constants mapped to constructors of [ty_ind] as triggers. *) + let pt_refs = List.map (fun (_, cnst, _) -> cnst) (to_post.(0)) in + to_post, pt_refs + +let elaborate_to_post env sigma ty_ind via = + match via with + | None -> [||], get_constructors ty_ind + | Some (ty_name, l) -> elaborate_to_post env sigma ty_name ty_ind l + +let vernac_number_notation local ty f g opts scope = + let rec parse_opts = function + | [] -> None, Nop + | h :: opts -> + let via, opts = parse_opts opts in + let via = match h, via with + | Via _, Some _ -> multiple_via_error () + | Via v, None -> Some v + | _ -> via in + let opts = match h, opts with + | After _, (Warning _ | Abstract _) -> multiple_after_error () + | After a, Nop -> a + | _ -> opts in + via, opts in + let via, opts = parse_opts opts in + (match via, opts with Some _, Abstract _ -> via_abstract_error () | _ -> ()); let env = Global.env () in let sigma = Evd.from_env env in let num_ty = locate_number () in let z_pos_ty = locate_z () in let int63_ty = locate_int63 () 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 = 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 @@ -143,7 +367,6 @@ let vernac_number_notation local ty f g scope opts = mkProdC ([CAst.make Anonymous],Default Glob_term.Explicit, x, y) in let opt r = app (mkRefC (q_option ())) r in - let constructors = get_constructors tyc in (* Check the type of f *) let to_kind = match num_ty with @@ -199,8 +422,8 @@ let vernac_number_notation local ty f g scope opts = | _, ((DecimalInt _ | DecimalUInt _ | Decimal _), _) -> warn_deprecated_decimal () | _ -> ()); - let o = { to_kind; to_ty; to_post = [||]; of_kind; of_ty; - ty_name = ty; + let to_post, pt_refs = elaborate_to_post env sigma tyc via in + let o = { to_kind; to_ty; to_post; of_kind; of_ty; ty_name; warning = opts } in (match opts, to_kind with @@ -211,7 +434,7 @@ let vernac_number_notation local ty f g scope opts = pt_scope = scope; pt_interp_info = NumberNotation 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/numeral.mli b/plugins/syntax/numeral.mli index d5fe42b0b4..1f6896d549 100644 --- a/plugins/syntax/numeral.mli +++ b/plugins/syntax/numeral.mli @@ -14,6 +14,13 @@ open Notation (** * Number notation *) +type number_string_via = qualid * (qualid * qualid) list +type number_option = + | After of numnot_option + | Via of number_string_via + val vernac_number_notation : locality_flag -> - qualid -> qualid -> qualid -> - Notation_term.scope_name -> numnot_option -> unit + qualid -> + qualid -> qualid -> + number_option list -> + Notation_term.scope_name -> unit -- cgit v1.2.3 From b6c13afd432ce1957315e94c1ce8c06aa848fe5a Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 3 Sep 2020 13:19:00 +0200 Subject: [numeral notation] R Previously real constants were parsed by an unproved OCaml code. The parser and printer are now implemented in Coq, which will enable a proof and hopefully make it easier to maintain / make evolve. Previously reals were all parsed as an integer, an integer multiplied by a power of ten or an integer divided by a power of ten. This means 1.02 and 102e-2 were both parsed as 102 / 100 and could not be tell apart when printing. So the printer had to choose between two representations : without exponent or without decimal dot. The choice was made heuristically toward a most compact representation. Now, decimal dot is parsed as a rational and exponents are parsed as a product or division by a power of ten. For instance, 1.02 is parsed as Q2R (102 # 100) whereas 102e-2 is parsed as IZR 102 / IZR (Z.pow_pos 10 2). 1.02 and 102e-2 remain equal (proved by reflexivity) but 1.02e1 = Q2R (102 # 100) * 10 and 10.2 = Q2R (102 # 10) no longer are. --- plugins/syntax/dune | 7 -- plugins/syntax/r_syntax.ml | 214 ---------------------------------- plugins/syntax/r_syntax.mli | 9 -- plugins/syntax/r_syntax_plugin.mlpack | 1 - 4 files changed, 231 deletions(-) delete mode 100644 plugins/syntax/r_syntax.ml delete mode 100644 plugins/syntax/r_syntax.mli delete mode 100644 plugins/syntax/r_syntax_plugin.mlpack (limited to 'plugins') diff --git a/plugins/syntax/dune b/plugins/syntax/dune index b395695c8a..1b3d7598da 100644 --- a/plugins/syntax/dune +++ b/plugins/syntax/dune @@ -12,13 +12,6 @@ (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 int63_syntax_plugin) (public_name coq.plugins.int63_syntax) diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml deleted file mode 100644 index d66b9537b4..0000000000 --- a/plugins/syntax/r_syntax.ml +++ /dev/null @@ -1,214 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* 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 = GlobRef.ConstructRef path_of_xI -let glob_xO = GlobRef.ConstructRef path_of_xO -let glob_xH = GlobRef.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 Z.(div_rem x (of_int 2)) with - | (q,rem) when rem = Z.zero -> DAst.make @@ GApp (ref_xO,[pos_of q]) - | (q,_) when not Z.(equal q zero) -> DAst.make @@ GApp (ref_xI,[pos_of q]) - | (q,_) -> 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 -> Z.mul Z.(of_int 2) (bignat_of_pos a) - | GApp (r, [a]) when is_gr r glob_xI -> Z.add Z.one Z.(mul (of_int 2) (bignat_of_pos a)) - | GRef (a, _) when GlobRef.equal a glob_xH -> Z.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 = GlobRef.ConstructRef path_of_ZERO -let glob_POS = GlobRef.ConstructRef path_of_POS -let glob_NEG = GlobRef.ConstructRef path_of_NEG - -let z_of_int ?loc n = - if not Z.(equal n zero) then - let sgn, n = - if Z.(leq zero n) then glob_POS, n else glob_NEG, Z.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 -> Z.neg (bignat_of_pos a) - | GRef (a, _) when GlobRef.equal a glob_ZERO -> Z.zero - | _ -> raise Non_closed_number - -(**********************************************************************) -(* Parsing R via scopes *) -(**********************************************************************) - -let rdefinitions = ["Coq";"Reals";"Rdefinitions"] -let r_modpath = MPfile (make_dir rdefinitions) -let r_base_modpath = MPdot (r_modpath, Label.make "RbaseSymbolsImpl") -let r_path = make_path ["Coq";"Reals";"Rdefinitions";"RbaseSymbolsImpl"] "R" - -let glob_IZR = GlobRef.ConstRef (Constant.make2 r_modpath @@ Label.make "IZR") -let glob_Rmult = GlobRef.ConstRef (Constant.make2 r_base_modpath @@ Label.make "Rmult") -let glob_Rdiv = GlobRef.ConstRef (Constant.make2 r_modpath @@ Label.make "Rdiv") - -let binintdef = ["Coq";"ZArith";"BinIntDef"] -let z_modpath = MPdot (MPfile (make_dir binintdef), Label.make "Z") - -let glob_pow_pos = GlobRef.ConstRef (Constant.make2 z_modpath @@ Label.make "pow_pos") - -let r_of_rawnum ?loc n = - let n,e = NumTok.Signed.to_bigint_and_exponent n in - let e,p = NumTok.(match e with EDec e -> e, 10 | EBin e -> e, 2) in - let izr z = - DAst.make @@ GApp (DAst.make @@ GRef(glob_IZR,None), [z]) in - let rmult r r' = - DAst.make @@ GApp (DAst.make @@ GRef(glob_Rmult,None), [r; r']) in - let rdiv r r' = - DAst.make @@ GApp (DAst.make @@ GRef(glob_Rdiv,None), [r; r']) in - let pow p e = - let p = z_of_int ?loc (Z.of_int p) in - let e = pos_of_bignat e in - DAst.make @@ GApp (DAst.make @@ GRef(glob_pow_pos,None), [p; e]) in - let n = - izr (z_of_int ?loc n) in - if Int.equal (Z.sign e) 1 then rmult n (izr (pow p e)) - else if Int.equal (Z.sign e) (-1) then rdiv n (izr (pow p (Z.neg e))) - else n (* e = 0 *) - -(**********************************************************************) -(* Printing R via scopes *) -(**********************************************************************) - -let rawnum_of_r c = - (* print i * 10^e, precondition: e <> 0 *) - let numTok_of_int_exp i e = - (* choose between 123e-2 and 1.23, this is purely heuristic - and doesn't play any soundness role *) - let choose_exponent = - if Int.equal (Z.sign e) 1 then - true (* don't print 12 * 10^2 as 1200 to distinguish them *) - else - let i = Z.to_string i in - let li = if i.[0] = '-' then String.length i - 1 else String.length i in - let e = Z.neg e in - let le = String.length (Z.to_string e) in - Z.(lt (add (of_int li) (of_int le)) e) in - (* print 123 * 10^-2 as 123e-2 *) - let numTok_exponent () = - NumTok.Signed.of_bigint_and_exponent i (NumTok.EDec e) in - (* print 123 * 10^-2 as 1.23, precondition e < 0 *) - let numTok_dot () = - let s, i = - if Z.sign i >= 0 then NumTok.SPlus, Z.to_string i - else NumTok.SMinus, Z.(to_string (neg i)) in - let ni = String.length i in - let e = - (Z.to_int e) in - assert (e > 0); - let i, f = - if e < ni then String.sub i 0 (ni - e), String.sub i (ni - e) e - else "0", String.make (e - ni) '0' ^ i in - let i = s, NumTok.UnsignedNat.of_string i in - let f = NumTok.UnsignedNat.of_string f in - NumTok.Signed.of_int_frac_and_exponent i (Some f) None in - if choose_exponent then numTok_exponent () else numTok_dot () in - match DAst.get c with - | GApp (r, [a]) when is_gr r glob_IZR -> - let n = bigint_of_z a in - NumTok.(Signed.of_bigint CDec n) - | GApp (md, [l; r]) when is_gr md glob_Rmult || is_gr md glob_Rdiv -> - begin match DAst.get l, DAst.get r with - | GApp (i, [l]), GApp (i', [r]) - when is_gr i glob_IZR && is_gr i' glob_IZR -> - begin match DAst.get r with - | GApp (p, [t; e]) when is_gr p glob_pow_pos -> - let t = bigint_of_z t in - if not (Z.(equal t (of_int 10))) then - raise Non_closed_number - else - let i = bigint_of_z l in - let e = bignat_of_pos e in - let e = if is_gr md glob_Rdiv then Z.neg e else e in - numTok_of_int_exp i e - | _ -> raise Non_closed_number - end - | _ -> raise Non_closed_number - end - | _ -> raise Non_closed_number - -let uninterp_r (AnyGlobConstr p) = - try - Some (rawnum_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_rawnumeral_interpretation r_scope (r_of_rawnum,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; glob_Rmult; glob_Rdiv]; - pt_in_match = false } diff --git a/plugins/syntax/r_syntax.mli b/plugins/syntax/r_syntax.mli deleted file mode 100644 index b72d544151..0000000000 --- a/plugins/syntax/r_syntax.mli +++ /dev/null @@ -1,9 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* strbrk "Numeral Notation is deprecated, please use Number Notation instead.") -let pr_number_mapping (n, n') = - Libnames.pr_qualid n ++ spc () ++ str "=>" ++ spc () ++ Libnames.pr_qualid n' +let pr_number_mapping (b, n, n') = + if b then + str "[" ++ Libnames.pr_qualid n ++ str "]" ++ spc () ++ str "=>" ++ spc () + ++ Libnames.pr_qualid n' + else + Libnames.pr_qualid n ++ spc () ++ str "=>" ++ spc () + ++ Libnames.pr_qualid n' let pr_number_via (n, l) = str "via " ++ Libnames.pr_qualid n ++ str " mapping [" @@ -56,7 +61,8 @@ END VERNAC ARGUMENT EXTEND number_mapping PRINTED BY { pr_number_mapping } -| [ reference(n) "=>" reference(n') ] -> { n, n' } +| [ reference(n) "=>" reference(n') ] -> { false, n, n' } +| [ "[" reference(n) "]" "=>" reference(n') ] -> { true, n, n' } END VERNAC ARGUMENT EXTEND number_via diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml index 316ca456a4..1efe6b77d1 100644 --- a/plugins/syntax/numeral.ml +++ b/plugins/syntax/numeral.ml @@ -21,7 +21,7 @@ module CMap = CMap.Make (Constr) (** * Number notation *) -type number_string_via = qualid * (qualid * qualid) list +type number_string_via = qualid * (bool * qualid * qualid) list type number_option = | After of numnot_option | Via of number_string_via @@ -231,9 +231,10 @@ let elaborate_to_post env sigma ty_name ty_ind l = For each constant [cnst] and inductive constructor [indc] in [l], retrieve: * its location: [lcnst] and [lindc] * its GlobRef: [cnst] and [indc] - * its type: [tcnst] and [tindc] (decomposed in product by [get_type] above) *) + * its type: [tcnst] and [tindc] (decomposed in product by [get_type] above) + * [impls] are the implicit arguments of [cnst] *) let l = - let read (cnst, indc) = + let read (consider_implicits, cnst, indc) = let lcnst, lindc = cnst.CAst.loc, indc.CAst.loc in let cnst, ccnst = locate_global_constructor_inductive_or_constant cnst in let indc, cindc = @@ -247,13 +248,16 @@ let elaborate_to_post env sigma ty_name ty_ind l = let lc, tc = get_type env sigma c in List.map (fun (n, c) -> n, rm_params c) lc, rm_params tc in let tcnst, tindc = get_type_wo_params ccnst, get_type_wo_params cindc in - lcnst, cnst, tcnst, lindc, indc, tindc in + let impls = + if not consider_implicits then [] else + Impargs.(select_stronger_impargs (implicits_of_global cnst)) in + lcnst, cnst, tcnst, lindc, indc, tindc, impls in List.map read l in - let eq_indc indc (_, _, _, _, indc', _) = GlobRef.equal indc indc' in + let eq_indc indc (_, _, _, _, indc', _, _) = GlobRef.equal indc indc' in (* Collect all inductive types involved. That is [ty_ind] and all final codomains of [tindc] above. *) let inds = - List.fold_left (fun s (_, _, _, _, _, tindc) -> CSet.add (snd tindc) s) + List.fold_left (fun s (_, _, _, _, _, tindc, _) -> CSet.add (snd tindc) s) (CSet.singleton ty_ind) l in (* And for each inductive, retrieve its constructors. *) let constructors = @@ -264,7 +268,7 @@ let elaborate_to_post env sigma ty_name ty_ind l = (* Error if one [constructor] in some inductive in [inds] doesn't appear exactly once in [l] *) let _ = (* check_for duplicate constructor and error *) - List.fold_left (fun already_seen (_, cnst, _, loc, indc, _) -> + List.fold_left (fun already_seen (_, cnst, _, loc, indc, _, _) -> try let cnst' = List.assoc_f GlobRef.equal indc already_seen in remapping_error ?loc indc cnst' cnst @@ -289,16 +293,23 @@ let elaborate_to_post env sigma ty_name ty_ind l = warn_via_remapping ?loc (env, sigma, ckey, old_cval, cval); m in List.fold_left - (fun (ind2ty, ty2ind) (lcnst, _, (_, tcnst), lindc, _, (_, tindc)) -> + (fun (ind2ty, ty2ind) (lcnst, _, (_, tcnst), lindc, _, (_, tindc), _) -> add lcnst tindc tcnst ind2ty, add lindc tcnst tindc ty2ind) CMap.(singleton ty_ind ty_name, singleton ty_name ty_ind) l in (* check that type of constants and constructors mapped in [l] match modulo [ind2ty] *) + let rm_impls impls (l, t) = + let rec aux impls l = match impls, l with + | Some _ :: impls, _ :: b -> aux impls b + | None :: impls, (n, a) :: b -> (n, a) :: aux impls b + | _ -> l in + aux impls l, t in let replace m (l, t) = let apply_m c = try CMap.find c m with Not_found -> c in List.fold_right (fun (na, a) b -> Constr.mkProd (na, (apply_m a), b)) l (apply_m t) in - List.iter (fun (_, cnst, tcnst, loc, indc, tindc) -> + List.iter (fun (_, cnst, tcnst, loc, indc, tindc, impls) -> + let tcnst = rm_impls impls tcnst in let tcnst' = replace CMap.empty tcnst in if not (Constr.equal tcnst' (replace ind2ty tindc)) then let actual = replace CMap.empty tindc in @@ -313,17 +324,21 @@ let elaborate_to_post env sigma ty_name ty_ind l = (CMap.singleton ty_ind 0, Int.Map.singleton 0 ty_ind, 1) in (* Finally elaborate [to_post] *) let to_post = - let rec map_prod = function - | [] -> [] - | (_, a) :: b -> - let t = match CMap.find_opt a ind2num with - | Some i -> ToPostAs i - | None -> ToPostCopy in - t :: map_prod b in + let rec map_prod impls tindc = match impls with + | Some _ :: impls -> ToPostHole :: map_prod impls tindc + | _ -> + match tindc with + | [] -> [] + | (_, a) :: b -> + let t = match CMap.find_opt a ind2num with + | Some i -> ToPostAs i + | None -> ToPostCopy in + let impls = match impls with [] -> [] | _ :: t -> t in + t :: map_prod impls b in Array.init nb_ind (fun i -> List.map (fun indc -> - let _, cnst, _, _, _, tindc = List.find (eq_indc indc) l in - indc, cnst, map_prod (fst tindc)) + let _, cnst, _, _, _, tindc, impls = List.find (eq_indc indc) l in + indc, cnst, map_prod impls (fst tindc)) (CMap.find (Int.Map.find i num2ind) constructors)) in (* and use constants mapped to constructors of [ty_ind] as triggers. *) let pt_refs = List.map (fun (_, cnst, _) -> cnst) (to_post.(0)) in diff --git a/plugins/syntax/numeral.mli b/plugins/syntax/numeral.mli index 1f6896d549..5a13d1068b 100644 --- a/plugins/syntax/numeral.mli +++ b/plugins/syntax/numeral.mli @@ -14,7 +14,7 @@ open Notation (** * Number notation *) -type number_string_via = qualid * (qualid * qualid) list +type number_string_via = qualid * (bool * qualid * qualid) list type number_option = | After of numnot_option | Via of number_string_via -- cgit v1.2.3 From e728a1ef0f8b5fdc4b1815a7d0349c67db15f9b4 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 3 Sep 2020 13:25:00 +0200 Subject: [numeral notation] Add support for parameterized inductives --- plugins/syntax/numeral.ml | 66 +++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 58 insertions(+), 8 deletions(-) (limited to 'plugins') diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml index 1efe6b77d1..89d757a72a 100644 --- a/plugins/syntax/numeral.ml +++ b/plugins/syntax/numeral.ml @@ -136,6 +136,11 @@ let warn_deprecated_decimal = Decimal.int or Decimal.decimal. Use Number.uint, \ Number.int or Number.number respectively.") +let error_params ind = + CErrors.user_err + (str "Wrong number of parameters for inductive" ++ spc () + ++ Printer.pr_global (GlobRef.IndRef ind) ++ str ".") + let remapping_error ?loc ty ty' ty'' = CErrors.user_err ?loc (Printer.pr_global ty @@ -219,11 +224,43 @@ let get_type env sigma c = List.map (fun (na, a) -> na, EConstr.Unsafe.to_constr a) l, EConstr.Unsafe.to_constr t -(* [elaborate_to_post env sigma ty_name ty_ind l] builds the [to_post] +(* [elaborate_to_post_params env sigma ty_ind params] builds the + [to_post] translation (c.f., interp/notation.mli) for the numeral + notation to parse/print type [ty_ind]. This translation is the + identity ([ToPostCopy]) except that it checks ([ToPostCheck]) that + the parameters of the inductive type [ty_ind] match the ones given + in [params]. *) +let elaborate_to_post_params env sigma ty_ind params = + let to_post_for_constructor indc = + let sigma, c = match indc with + | GlobRef.ConstructRef c -> + let sigma,c = Evd.fresh_constructor_instance env sigma c in + sigma, Constr.mkConstructU c + | _ -> assert false in (* c.f. get_constructors *) + let args, t = get_type env sigma c in + let params_indc = match Constr.kind t with + | Constr.App (_, a) -> Array.to_list a | _ -> [] in + let sz = List.length args in + let a = Array.make sz ToPostCopy in + if List.length params <> List.length params_indc then error_params ty_ind; + List.iter2 (fun param param_indc -> + match param, Constr.kind param_indc with + | Some p, Constr.Rel i when i <= sz -> a.(sz - i) <- ToPostCheck p + | _ -> ()) + params params_indc; + indc, indc, Array.to_list a in + let pt_refs = get_constructors ty_ind in + let to_post_0 = List.map to_post_for_constructor pt_refs in + let to_post = + let only_copy (_, _, args) = List.for_all ((=) ToPostCopy) args in + if (List.for_all only_copy to_post_0) then [||] else [|to_post_0|] in + to_post, pt_refs + +(* [elaborate_to_post_via env sigma ty_name ty_ind l] builds the [to_post] translation (c.f., interp/notation.mli) for the number notation to parse/print type [ty_name] through the inductive [ty_ind] according to the pairs [constant, constructor] in the list [l]. *) -let elaborate_to_post env sigma ty_name ty_ind l = +let elaborate_to_post_via env sigma ty_name ty_ind l = let sigma, ty_name = locate_global_sort_inductive_or_constant sigma ty_name in let ty_ind = Constr.mkInd ty_ind in @@ -344,10 +381,21 @@ let elaborate_to_post env sigma ty_name ty_ind l = let pt_refs = List.map (fun (_, cnst, _) -> cnst) (to_post.(0)) in to_post, pt_refs -let elaborate_to_post env sigma ty_ind via = - match via with - | None -> [||], get_constructors ty_ind - | Some (ty_name, l) -> elaborate_to_post env sigma ty_name ty_ind l +let locate_global_inductive allow_params qid = + let locate_param_inductive qid = + 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), l)) when allow_params -> + i, + List.map (function + | Notation_term.NRef r -> Some r + | Notation_term.NHole _ -> None + | _ -> raise Not_found) l + | _ -> raise Not_found in + try locate_param_inductive qid + with Not_found -> Smartlocate.global_inductive_with_alias qid, [] let vernac_number_notation local ty f g opts scope = let rec parse_opts = function @@ -373,7 +421,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 = Smartlocate.global_inductive_with_alias ty 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 = mkRefC ty in @@ -437,7 +485,9 @@ let vernac_number_notation local ty f g opts scope = | _, ((DecimalInt _ | DecimalUInt _ | Decimal _), _) -> warn_deprecated_decimal () | _ -> ()); - let to_post, pt_refs = elaborate_to_post env sigma tyc via in + 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 = opts } in -- cgit v1.2.3 From 3b766fd8859b692e3e93cf83bf87d393e32c572e Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 3 Sep 2020 13:26:00 +0200 Subject: Merge numeral and string notation plugins --- plugins/syntax/dune | 17 +- plugins/syntax/g_number_string.mlg | 102 +++++ plugins/syntax/g_numeral.mlg | 95 ---- plugins/syntax/g_string.mlg | 25 - plugins/syntax/number.ml | 505 +++++++++++++++++++++ plugins/syntax/number.mli | 26 ++ .../syntax/number_string_notation_plugin.mlpack | 3 + plugins/syntax/numeral.ml | 505 --------------------- plugins/syntax/numeral.mli | 26 -- plugins/syntax/numeral_notation_plugin.mlpack | 2 - plugins/syntax/string_notation.ml | 1 - plugins/syntax/string_notation_plugin.mlpack | 2 - 12 files changed, 641 insertions(+), 668 deletions(-) create mode 100644 plugins/syntax/g_number_string.mlg delete mode 100644 plugins/syntax/g_numeral.mlg delete mode 100644 plugins/syntax/g_string.mlg create mode 100644 plugins/syntax/number.ml create mode 100644 plugins/syntax/number.mli create mode 100644 plugins/syntax/number_string_notation_plugin.mlpack delete mode 100644 plugins/syntax/numeral.ml delete mode 100644 plugins/syntax/numeral.mli delete mode 100644 plugins/syntax/numeral_notation_plugin.mlpack delete mode 100644 plugins/syntax/string_notation_plugin.mlpack (limited to 'plugins') diff --git a/plugins/syntax/dune b/plugins/syntax/dune index 1b3d7598da..f930fc265a 100644 --- a/plugins/syntax/dune +++ b/plugins/syntax/dune @@ -1,15 +1,8 @@ (library - (name numeral_notation_plugin) - (public_name coq.plugins.numeral_notation) - (synopsis "Coq numeral notation plugin") - (modules g_numeral numeral) - (libraries coq.vernac)) - -(library - (name string_notation_plugin) - (public_name coq.plugins.string_notation) - (synopsis "Coq string notation plugin") - (modules g_string string_notation) + (name number_string_notation_plugin) + (public_name coq.plugins.number_string_notation) + (synopsis "Coq number and string notation plugin") + (modules g_number_string string_notation number) (libraries coq.vernac)) (library @@ -26,4 +19,4 @@ (modules float_syntax) (libraries coq.vernac)) -(coq.pp (modules g_numeral g_string)) +(coq.pp (modules g_number_string)) diff --git a/plugins/syntax/g_number_string.mlg b/plugins/syntax/g_number_string.mlg new file mode 100644 index 0000000000..b584505530 --- /dev/null +++ b/plugins/syntax/g_number_string.mlg @@ -0,0 +1,102 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* mt () + | Warning n -> str "warning after " ++ NumTok.UnsignedNat.print n + | Abstract n -> str "abstract after " ++ NumTok.UnsignedNat.print n + +let pr_deprecated_number_modifier m = str "(" ++ pr_number_after m ++ str ")" + +let warn_deprecated_numeral_notation = + CWarnings.create ~name:"numeral-notation" ~category:"deprecated" + (fun () -> + strbrk "Numeral Notation is deprecated, please use Number Notation instead.") + +let pr_number_mapping (b, n, n') = + if b then + str "[" ++ Libnames.pr_qualid n ++ str "]" ++ spc () ++ str "=>" ++ spc () + ++ Libnames.pr_qualid n' + else + Libnames.pr_qualid n ++ spc () ++ str "=>" ++ spc () + ++ Libnames.pr_qualid n' + +let pr_number_via (n, l) = + str "via " ++ Libnames.pr_qualid n ++ str " mapping [" + ++ prlist_with_sep pr_comma pr_number_mapping l ++ str "]" + +let pr_number_modifier = function + | After a -> pr_number_after a + | Via nl -> pr_number_via nl + +let pr_number_options l = + str "(" ++ prlist_with_sep pr_comma pr_number_modifier l ++ str ")" + +} + +VERNAC ARGUMENT EXTEND deprecated_number_modifier + PRINTED BY { pr_deprecated_number_modifier } +| [ ] -> { Nop } +| [ "(" "warning" "after" bignat(waft) ")" ] -> { Warning (NumTok.UnsignedNat.of_string waft) } +| [ "(" "abstract" "after" bignat(n) ")" ] -> { Abstract (NumTok.UnsignedNat.of_string n) } +END + +VERNAC ARGUMENT EXTEND number_mapping + PRINTED BY { pr_number_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 } +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 } +END + +VERNAC ARGUMENT EXTEND number_options + PRINTED BY { pr_number_options } +| [ "(" ne_number_modifier_list_sep(l, ",") ")" ] -> { l } +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) ] -> + + { vernac_number_notation (Locality.make_module_locality locality) ty f g (Option.default [] nl) (Id.to_string sc) } + | #[ locality = Attributes.locality; ] [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" + ident(sc) deprecated_number_modifier(o) ] -> + + { warn_deprecated_numeral_notation (); + vernac_number_notation (Locality.make_module_locality locality) ty f g [After o] (Id.to_string sc) } +END + +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/g_numeral.mlg b/plugins/syntax/g_numeral.mlg deleted file mode 100644 index a3cc786a4a..0000000000 --- a/plugins/syntax/g_numeral.mlg +++ /dev/null @@ -1,95 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* mt () - | Warning n -> str "warning after " ++ NumTok.UnsignedNat.print n - | Abstract n -> str "abstract after " ++ NumTok.UnsignedNat.print n - -let pr_deprecated_number_modifier m = str "(" ++ pr_number_after m ++ str ")" - -let warn_deprecated_numeral_notation = - CWarnings.create ~name:"numeral-notation" ~category:"deprecated" - (fun () -> - strbrk "Numeral Notation is deprecated, please use Number Notation instead.") - -let pr_number_mapping (b, n, n') = - if b then - str "[" ++ Libnames.pr_qualid n ++ str "]" ++ spc () ++ str "=>" ++ spc () - ++ Libnames.pr_qualid n' - else - Libnames.pr_qualid n ++ spc () ++ str "=>" ++ spc () - ++ Libnames.pr_qualid n' - -let pr_number_via (n, l) = - str "via " ++ Libnames.pr_qualid n ++ str " mapping [" - ++ prlist_with_sep pr_comma pr_number_mapping l ++ str "]" - -let pr_number_modifier = function - | After a -> pr_number_after a - | Via nl -> pr_number_via nl - -let pr_number_options l = - str "(" ++ prlist_with_sep pr_comma pr_number_modifier l ++ str ")" - -} - -VERNAC ARGUMENT EXTEND deprecated_number_modifier - PRINTED BY { pr_deprecated_number_modifier } -| [ ] -> { Nop } -| [ "(" "warning" "after" bignat(waft) ")" ] -> { Warning (NumTok.UnsignedNat.of_string waft) } -| [ "(" "abstract" "after" bignat(n) ")" ] -> { Abstract (NumTok.UnsignedNat.of_string n) } -END - -VERNAC ARGUMENT EXTEND number_mapping - PRINTED BY { pr_number_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 } -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 } -END - -VERNAC ARGUMENT EXTEND number_options - PRINTED BY { pr_number_options } -| [ "(" ne_number_modifier_list_sep(l, ",") ")" ] -> { l } -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) ] -> - - { vernac_number_notation (Locality.make_module_locality locality) ty f g (Option.default [] nl) (Id.to_string sc) } - | #[ locality = Attributes.locality; ] [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" - ident(sc) deprecated_number_modifier(o) ] -> - - { warn_deprecated_numeral_notation (); - vernac_number_notation (Locality.make_module_locality locality) ty f g [After o] (Id.to_string sc) } -END diff --git a/plugins/syntax/g_string.mlg b/plugins/syntax/g_string.mlg deleted file mode 100644 index 788f9e011d..0000000000 --- a/plugins/syntax/g_string.mlg +++ /dev/null @@ -1,25 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* - { vernac_string_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) } -END diff --git a/plugins/syntax/number.ml b/plugins/syntax/number.ml new file mode 100644 index 0000000000..89d757a72a --- /dev/null +++ b/plugins/syntax/number.ml @@ -0,0 +1,505 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* + 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 -> GlobRef.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 unsafe_locate_ind q = + match Nametab.locate q with + | GlobRef.IndRef i -> i + | _ -> raise Not_found + +let locate_z () = + let zn = "num.Z.type" in + let pn = "num.pos.type" in + if Coqlib.has_ref zn && Coqlib.has_ref pn + then + let q_z = qualid_of_ref zn in + let q_pos = qualid_of_ref pn in + Some ({ + z_ty = unsafe_locate_ind q_z; + pos_ty = unsafe_locate_ind q_pos; + }, mkRefC q_z) + else None + +let locate_number () = + let dint = "num.int.type" in + let duint = "num.uint.type" in + let dec = "num.decimal.type" in + let hint = "num.hexadecimal_int.type" in + let huint = "num.hexadecimal_uint.type" in + let hex = "num.hexadecimal.type" in + let int = "num.num_int.type" in + let uint = "num.num_uint.type" in + let num = "num.number.type" in + if Coqlib.has_ref dint && Coqlib.has_ref duint && Coqlib.has_ref dec + && Coqlib.has_ref hint && Coqlib.has_ref huint && Coqlib.has_ref hex + && Coqlib.has_ref int && Coqlib.has_ref uint && Coqlib.has_ref num + then + let q_dint = qualid_of_ref dint in + let q_duint = qualid_of_ref duint in + let q_dec = qualid_of_ref dec in + let q_hint = qualid_of_ref hint in + let q_huint = qualid_of_ref huint in + let q_hex = qualid_of_ref hex in + let q_int = qualid_of_ref int in + let q_uint = qualid_of_ref uint in + let q_num = qualid_of_ref num in + let int_ty = { + dec_int = unsafe_locate_ind q_dint; + dec_uint = unsafe_locate_ind q_duint; + hex_int = unsafe_locate_ind q_hint; + hex_uint = unsafe_locate_ind q_huint; + int = unsafe_locate_ind q_int; + uint = unsafe_locate_ind q_uint; + } in + let num_ty = { + int = int_ty; + decimal = unsafe_locate_ind q_dec; + hexadecimal = unsafe_locate_ind q_hex; + number = unsafe_locate_ind q_num; + } in + Some (int_ty, mkRefC q_int, mkRefC q_uint, mkRefC q_dint, mkRefC q_duint, + num_ty, mkRefC q_num, mkRefC q_dec) + 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 env sigma f ty = + 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 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).") + +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).") + +let warn_deprecated_decimal = + CWarnings.create ~name:"decimal-numeral-notation" ~category:"deprecated" + (fun () -> + strbrk "Deprecated Number Notation for Decimal.uint, \ + Decimal.int or Decimal.decimal. Use Number.uint, \ + Number.int or Number.number respectively.") + +let error_params ind = + CErrors.user_err + (str "Wrong number of parameters for inductive" ++ spc () + ++ Printer.pr_global (GlobRef.IndRef ind) ++ str ".") + +let remapping_error ?loc ty ty' ty'' = + CErrors.user_err ?loc + (Printer.pr_global ty + ++ str " was already mapped to" ++ spc () ++ Printer.pr_global ty' + ++ str " and cannot be remapped to" ++ spc () ++ Printer.pr_global ty'' + ++ str ".") + +let error_missing c = + CErrors.user_err + (str "Missing mapping for constructor " ++ Printer.pr_global c ++ str ".") + +let pr_constr env sigma c = + let c = Constrextern.extern_constr env sigma (EConstr.of_constr c) in + Ppconstr.pr_constr_expr env sigma c + +let warn_via_remapping = + CWarnings.create ~name:"via-type-remapping" ~category:"numbers" + (fun (env, sigma, ty, ty', ty'') -> + let constr = pr_constr env sigma in + constr ty ++ str " was already mapped to" ++ spc () ++ constr ty' + ++ str ", mapping it also to" ++ spc () ++ constr ty'' + ++ str " might yield ill typed terms when using the notation.") + +let warn_via_type_mismatch = + CWarnings.create ~name:"via-type-mismatch" ~category:"numbers" + (fun (env, sigma, g, g', exp, actual) -> + let constr = pr_constr env sigma in + str "Type of" ++ spc() ++ Printer.pr_global g + ++ str " seems incompatible with the type of" ++ spc () + ++ Printer.pr_global g' ++ str "." ++ spc () + ++ str "Expected type is: " ++ constr exp ++ spc () + ++ str "instead of " ++ constr actual ++ str "." ++ spc () + ++ str "This might yield ill typed terms when using the notation.") + +let multiple_via_error () = + CErrors.user_err (Pp.str "Multiple 'via' options.") + +let multiple_after_error () = + CErrors.user_err (Pp.str "Multiple 'warning after' or 'abstract after' options.") + +let via_abstract_error () = + CErrors.user_err (Pp.str "'via' and 'abstract' cannot be used together.") + +let locate_global_sort_inductive_or_constant sigma qid = + let locate_sort qid = + match Nametab.locate_extended qid with + | Globnames.TrueGlobal _ -> raise Not_found + | Globnames.SynDef kn -> + match Syntax_def.search_syntactic_definition kn with + | [], Notation_term.NSort r -> + let sigma,c = Evd.fresh_sort_in_family sigma (Glob_ops.glob_sort_family r) in + sigma,Constr.mkSort c + | _ -> raise Not_found in + try locate_sort qid + with Not_found -> + match Smartlocate.global_with_alias qid with + | GlobRef.IndRef i -> sigma, Constr.mkInd i + | _ -> sigma, Constr.mkConst (Smartlocate.global_constant_with_alias qid) + +let locate_global_constructor_inductive_or_constant qid = + let g = Smartlocate.global_with_alias qid in + match g with + | GlobRef.ConstructRef c -> g, Constr.mkConstruct c + | GlobRef.IndRef i -> g, Constr.mkInd i + | _ -> g, Constr.mkConst (Smartlocate.global_constant_with_alias qid) + +(* [get_type env sigma c] retrieves the type of [c] and returns a pair + [l, t] such that [c : l_0 -> ... -> l_n -> t]. *) +let get_type env sigma c = + (* inspired from [compute_implicit_names] in "interp/impargs.ml" *) + let rec aux env acc t = + let t = Reductionops.whd_all env sigma t in + match EConstr.kind sigma t with + | Constr.Prod (na, a, b) -> + let a = Reductionops.whd_all env sigma a in + let rel = Context.Rel.Declaration.LocalAssum (na, a) in + aux (EConstr.push_rel rel env) ((na, a) :: acc) b + | _ -> List.rev acc, t in + let t = Retyping.get_type_of env sigma (EConstr.of_constr c) in + let l, t = aux env [] t in + List.map (fun (na, a) -> na, EConstr.Unsafe.to_constr a) l, + EConstr.Unsafe.to_constr t + +(* [elaborate_to_post_params env sigma ty_ind params] builds the + [to_post] translation (c.f., interp/notation.mli) for the numeral + notation to parse/print type [ty_ind]. This translation is the + identity ([ToPostCopy]) except that it checks ([ToPostCheck]) that + the parameters of the inductive type [ty_ind] match the ones given + in [params]. *) +let elaborate_to_post_params env sigma ty_ind params = + let to_post_for_constructor indc = + let sigma, c = match indc with + | GlobRef.ConstructRef c -> + let sigma,c = Evd.fresh_constructor_instance env sigma c in + sigma, Constr.mkConstructU c + | _ -> assert false in (* c.f. get_constructors *) + let args, t = get_type env sigma c in + let params_indc = match Constr.kind t with + | Constr.App (_, a) -> Array.to_list a | _ -> [] in + let sz = List.length args in + let a = Array.make sz ToPostCopy in + if List.length params <> List.length params_indc then error_params ty_ind; + List.iter2 (fun param param_indc -> + match param, Constr.kind param_indc with + | Some p, Constr.Rel i when i <= sz -> a.(sz - i) <- ToPostCheck p + | _ -> ()) + params params_indc; + indc, indc, Array.to_list a in + let pt_refs = get_constructors ty_ind in + let to_post_0 = List.map to_post_for_constructor pt_refs in + let to_post = + let only_copy (_, _, args) = List.for_all ((=) ToPostCopy) args in + if (List.for_all only_copy to_post_0) then [||] else [|to_post_0|] in + to_post, pt_refs + +(* [elaborate_to_post_via env sigma ty_name ty_ind l] builds the [to_post] + translation (c.f., interp/notation.mli) for the number notation to + parse/print type [ty_name] through the inductive [ty_ind] according + to the pairs [constant, constructor] in the list [l]. *) +let elaborate_to_post_via env sigma ty_name ty_ind l = + let sigma, ty_name = + locate_global_sort_inductive_or_constant sigma ty_name in + let ty_ind = Constr.mkInd ty_ind in + (* Retrieve constants and constructors mappings and their type. + For each constant [cnst] and inductive constructor [indc] in [l], retrieve: + * its location: [lcnst] and [lindc] + * its GlobRef: [cnst] and [indc] + * its type: [tcnst] and [tindc] (decomposed in product by [get_type] above) + * [impls] are the implicit arguments of [cnst] *) + let l = + let read (consider_implicits, cnst, indc) = + let lcnst, lindc = cnst.CAst.loc, indc.CAst.loc in + let cnst, ccnst = locate_global_constructor_inductive_or_constant cnst in + let indc, cindc = + let indc = Smartlocate.global_constructor_with_alias indc in + GlobRef.ConstructRef indc, Constr.mkConstruct indc in + let get_type_wo_params c = + (* ignore parameters of inductive types *) + let rm_params c = match Constr.kind c with + | Constr.App (c, _) when Constr.isInd c -> c + | _ -> c in + let lc, tc = get_type env sigma c in + List.map (fun (n, c) -> n, rm_params c) lc, rm_params tc in + let tcnst, tindc = get_type_wo_params ccnst, get_type_wo_params cindc in + let impls = + if not consider_implicits then [] else + Impargs.(select_stronger_impargs (implicits_of_global cnst)) in + lcnst, cnst, tcnst, lindc, indc, tindc, impls in + List.map read l in + let eq_indc indc (_, _, _, _, indc', _, _) = GlobRef.equal indc indc' in + (* Collect all inductive types involved. + That is [ty_ind] and all final codomains of [tindc] above. *) + let inds = + List.fold_left (fun s (_, _, _, _, _, tindc, _) -> CSet.add (snd tindc) s) + (CSet.singleton ty_ind) l in + (* And for each inductive, retrieve its constructors. *) + let constructors = + CSet.fold (fun ind m -> + let inductive, _ = Constr.destInd ind in + CMap.add ind (get_constructors inductive) m) + inds CMap.empty in + (* Error if one [constructor] in some inductive in [inds] + doesn't appear exactly once in [l] *) + let _ = (* check_for duplicate constructor and error *) + List.fold_left (fun already_seen (_, cnst, _, loc, indc, _, _) -> + try + let cnst' = List.assoc_f GlobRef.equal indc already_seen in + remapping_error ?loc indc cnst' cnst + with Not_found -> (indc, cnst) :: already_seen) + [] l in + let () = (* check for missing constructor and error *) + CMap.iter (fun _ -> + List.iter (fun cstr -> + if not (List.exists (eq_indc cstr) l) then error_missing cstr)) + constructors in + (* Perform some checks on types and warn if they look strange. + These checks are neither sound nor complete, so we only warn. *) + let () = + (* associate inductives to types, and check that this mapping is one to one + and maps [ty_ind] to [ty_name] *) + let ind2ty, ty2ind = + let add loc ckey cval m = + match CMap.find_opt ckey m with + | None -> CMap.add ckey cval m + | Some old_cval -> + if not (Constr.equal old_cval cval) then + warn_via_remapping ?loc (env, sigma, ckey, old_cval, cval); + m in + List.fold_left + (fun (ind2ty, ty2ind) (lcnst, _, (_, tcnst), lindc, _, (_, tindc), _) -> + add lcnst tindc tcnst ind2ty, add lindc tcnst tindc ty2ind) + CMap.(singleton ty_ind ty_name, singleton ty_name ty_ind) l in + (* check that type of constants and constructors mapped in [l] + match modulo [ind2ty] *) + let rm_impls impls (l, t) = + let rec aux impls l = match impls, l with + | Some _ :: impls, _ :: b -> aux impls b + | None :: impls, (n, a) :: b -> (n, a) :: aux impls b + | _ -> l in + aux impls l, t in + let replace m (l, t) = + let apply_m c = try CMap.find c m with Not_found -> c in + List.fold_right (fun (na, a) b -> Constr.mkProd (na, (apply_m a), b)) + l (apply_m t) in + List.iter (fun (_, cnst, tcnst, loc, indc, tindc, impls) -> + let tcnst = rm_impls impls tcnst in + let tcnst' = replace CMap.empty tcnst in + if not (Constr.equal tcnst' (replace ind2ty tindc)) then + let actual = replace CMap.empty tindc in + let expected = replace ty2ind tcnst in + warn_via_type_mismatch ?loc (env, sigma, indc, cnst, expected, actual)) + l in + (* Associate an index to each inductive, starting from 0 for [ty_ind]. *) + let ind2num, num2ind, nb_ind = + CMap.fold (fun ind _ (ind2num, num2ind, i) -> + CMap.add ind i ind2num, Int.Map.add i ind num2ind, i + 1) + (CMap.remove ty_ind constructors) + (CMap.singleton ty_ind 0, Int.Map.singleton 0 ty_ind, 1) in + (* Finally elaborate [to_post] *) + let to_post = + let rec map_prod impls tindc = match impls with + | Some _ :: impls -> ToPostHole :: map_prod impls tindc + | _ -> + match tindc with + | [] -> [] + | (_, a) :: b -> + let t = match CMap.find_opt a ind2num with + | Some i -> ToPostAs i + | None -> ToPostCopy in + let impls = match impls with [] -> [] | _ :: t -> t in + t :: map_prod impls b in + Array.init nb_ind (fun i -> + List.map (fun indc -> + let _, cnst, _, _, _, tindc, impls = List.find (eq_indc indc) l in + indc, cnst, map_prod impls (fst tindc)) + (CMap.find (Int.Map.find i num2ind) constructors)) in + (* and use constants mapped to constructors of [ty_ind] as triggers. *) + 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 = + 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), l)) when allow_params -> + i, + List.map (function + | Notation_term.NRef r -> Some r + | Notation_term.NHole _ -> None + | _ -> raise Not_found) l + | _ -> raise Not_found in + try locate_param_inductive qid + with Not_found -> Smartlocate.global_inductive_with_alias qid, [] + +let vernac_number_notation local ty f g opts scope = + let rec parse_opts = function + | [] -> None, Nop + | h :: opts -> + let via, opts = parse_opts opts in + let via = match h, via with + | Via _, Some _ -> multiple_via_error () + | Via v, None -> Some v + | _ -> via in + let opts = match h, opts with + | After _, (Warning _ | Abstract _) -> multiple_after_error () + | After a, Nop -> a + | _ -> opts in + via, opts in + let via, opts = parse_opts opts in + (match via, opts with Some _, Abstract _ -> via_abstract_error () | _ -> ()); + let env = Global.env () in + let sigma = Evd.from_env env in + let num_ty = locate_number () in + let z_pos_ty = locate_z () in + let int63_ty = locate_int63 () 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 = mkRefC ty in + let app x y = mkAppC (x,[y]) in + let arrow x y = + mkProdC ([CAst.make Anonymous],Default Glob_term.Explicit, x, y) + in + let opt r = app (mkRefC (q_option ())) r in + (* Check the type of f *) + let to_kind = + match num_ty with + | Some (int_ty, cint, _, _, _, _, _, _) when has_type env sigma f (arrow cint cty) -> Int int_ty, Direct + | Some (int_ty, cint, _, _, _, _, _, _) when has_type env sigma f (arrow cint (opt cty)) -> Int int_ty, Option + | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma f (arrow cuint cty) -> UInt int_ty, Direct + | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma f (arrow cuint (opt cty)) -> UInt int_ty, Option + | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma f (arrow cnum cty) -> Number num_ty, Direct + | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma f (arrow cnum (opt cty)) -> Number num_ty, Option + | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma f (arrow cint cty) -> DecimalInt int_ty, Direct + | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma f (arrow cint (opt cty)) -> DecimalInt int_ty, Option + | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma f (arrow cuint cty) -> DecimalUInt int_ty, Direct + | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma f (arrow cuint (opt cty)) -> DecimalUInt int_ty, Option + | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma f (arrow cdec cty) -> Decimal num_ty, Direct + | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma f (arrow cdec (opt cty)) -> Decimal num_ty, Option + | _ -> + match z_pos_ty with + | Some (z_pos_ty, cZ) when has_type env sigma f (arrow cZ cty) -> Z z_pos_ty, Direct + | 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 + | _ -> type_error_to f ty + in + (* Check the type of g *) + let of_kind = + match num_ty with + | Some (int_ty, cint, _, _, _, _, _, _) when has_type env sigma g (arrow cty cint) -> Int int_ty, Direct + | Some (int_ty, cint, _, _, _, _, _, _) when has_type env sigma g (arrow cty (opt cint)) -> Int int_ty, Option + | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma g (arrow cty cuint) -> UInt int_ty, Direct + | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma g (arrow cty (opt cuint)) -> UInt int_ty, Option + | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma g (arrow cty cnum) -> Number num_ty, Direct + | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma g (arrow cty (opt cnum)) -> Number num_ty, Option + | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma g (arrow cty cint) -> DecimalInt int_ty, Direct + | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma g (arrow cty (opt cint)) -> DecimalInt int_ty, Option + | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma g (arrow cty cuint) -> DecimalUInt int_ty, Direct + | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma g (arrow cty (opt cuint)) -> DecimalUInt int_ty, Option + | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma g (arrow cty cdec) -> Decimal num_ty, Direct + | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma g (arrow cty (opt cdec)) -> Decimal num_ty, Option + | _ -> + match z_pos_ty with + | Some (z_pos_ty, cZ) when has_type env sigma g (arrow cty cZ) -> Z z_pos_ty, Direct + | 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 + | _ -> type_error_of g ty + in + (match to_kind, of_kind with + | ((DecimalInt _ | DecimalUInt _ | Decimal _), _), _ + | _, ((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 o = { to_kind; to_ty; to_post; of_kind; of_ty; ty_name; + 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 = NumberNotation o; + pt_required = Nametab.path_of_global (GlobRef.IndRef tyc),[]; + pt_refs; + pt_in_match = true } + in + enable_prim_token_interpretation i diff --git a/plugins/syntax/number.mli b/plugins/syntax/number.mli new file mode 100644 index 0000000000..5a13d1068b --- /dev/null +++ b/plugins/syntax/number.mli @@ -0,0 +1,26 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* + qualid -> + qualid -> qualid -> + number_option list -> + Notation_term.scope_name -> unit diff --git a/plugins/syntax/number_string_notation_plugin.mlpack b/plugins/syntax/number_string_notation_plugin.mlpack new file mode 100644 index 0000000000..74c32d3a53 --- /dev/null +++ b/plugins/syntax/number_string_notation_plugin.mlpack @@ -0,0 +1,3 @@ +Number +String_notation +G_number_string diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml deleted file mode 100644 index 89d757a72a..0000000000 --- a/plugins/syntax/numeral.ml +++ /dev/null @@ -1,505 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* - 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 -> GlobRef.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 unsafe_locate_ind q = - match Nametab.locate q with - | GlobRef.IndRef i -> i - | _ -> raise Not_found - -let locate_z () = - let zn = "num.Z.type" in - let pn = "num.pos.type" in - if Coqlib.has_ref zn && Coqlib.has_ref pn - then - let q_z = qualid_of_ref zn in - let q_pos = qualid_of_ref pn in - Some ({ - z_ty = unsafe_locate_ind q_z; - pos_ty = unsafe_locate_ind q_pos; - }, mkRefC q_z) - else None - -let locate_number () = - let dint = "num.int.type" in - let duint = "num.uint.type" in - let dec = "num.decimal.type" in - let hint = "num.hexadecimal_int.type" in - let huint = "num.hexadecimal_uint.type" in - let hex = "num.hexadecimal.type" in - let int = "num.num_int.type" in - let uint = "num.num_uint.type" in - let num = "num.number.type" in - if Coqlib.has_ref dint && Coqlib.has_ref duint && Coqlib.has_ref dec - && Coqlib.has_ref hint && Coqlib.has_ref huint && Coqlib.has_ref hex - && Coqlib.has_ref int && Coqlib.has_ref uint && Coqlib.has_ref num - then - let q_dint = qualid_of_ref dint in - let q_duint = qualid_of_ref duint in - let q_dec = qualid_of_ref dec in - let q_hint = qualid_of_ref hint in - let q_huint = qualid_of_ref huint in - let q_hex = qualid_of_ref hex in - let q_int = qualid_of_ref int in - let q_uint = qualid_of_ref uint in - let q_num = qualid_of_ref num in - let int_ty = { - dec_int = unsafe_locate_ind q_dint; - dec_uint = unsafe_locate_ind q_duint; - hex_int = unsafe_locate_ind q_hint; - hex_uint = unsafe_locate_ind q_huint; - int = unsafe_locate_ind q_int; - uint = unsafe_locate_ind q_uint; - } in - let num_ty = { - int = int_ty; - decimal = unsafe_locate_ind q_dec; - hexadecimal = unsafe_locate_ind q_hex; - number = unsafe_locate_ind q_num; - } in - Some (int_ty, mkRefC q_int, mkRefC q_uint, mkRefC q_dint, mkRefC q_duint, - num_ty, mkRefC q_num, mkRefC q_dec) - 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 env sigma f ty = - 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 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).") - -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).") - -let warn_deprecated_decimal = - CWarnings.create ~name:"decimal-numeral-notation" ~category:"deprecated" - (fun () -> - strbrk "Deprecated Number Notation for Decimal.uint, \ - Decimal.int or Decimal.decimal. Use Number.uint, \ - Number.int or Number.number respectively.") - -let error_params ind = - CErrors.user_err - (str "Wrong number of parameters for inductive" ++ spc () - ++ Printer.pr_global (GlobRef.IndRef ind) ++ str ".") - -let remapping_error ?loc ty ty' ty'' = - CErrors.user_err ?loc - (Printer.pr_global ty - ++ str " was already mapped to" ++ spc () ++ Printer.pr_global ty' - ++ str " and cannot be remapped to" ++ spc () ++ Printer.pr_global ty'' - ++ str ".") - -let error_missing c = - CErrors.user_err - (str "Missing mapping for constructor " ++ Printer.pr_global c ++ str ".") - -let pr_constr env sigma c = - let c = Constrextern.extern_constr env sigma (EConstr.of_constr c) in - Ppconstr.pr_constr_expr env sigma c - -let warn_via_remapping = - CWarnings.create ~name:"via-type-remapping" ~category:"numbers" - (fun (env, sigma, ty, ty', ty'') -> - let constr = pr_constr env sigma in - constr ty ++ str " was already mapped to" ++ spc () ++ constr ty' - ++ str ", mapping it also to" ++ spc () ++ constr ty'' - ++ str " might yield ill typed terms when using the notation.") - -let warn_via_type_mismatch = - CWarnings.create ~name:"via-type-mismatch" ~category:"numbers" - (fun (env, sigma, g, g', exp, actual) -> - let constr = pr_constr env sigma in - str "Type of" ++ spc() ++ Printer.pr_global g - ++ str " seems incompatible with the type of" ++ spc () - ++ Printer.pr_global g' ++ str "." ++ spc () - ++ str "Expected type is: " ++ constr exp ++ spc () - ++ str "instead of " ++ constr actual ++ str "." ++ spc () - ++ str "This might yield ill typed terms when using the notation.") - -let multiple_via_error () = - CErrors.user_err (Pp.str "Multiple 'via' options.") - -let multiple_after_error () = - CErrors.user_err (Pp.str "Multiple 'warning after' or 'abstract after' options.") - -let via_abstract_error () = - CErrors.user_err (Pp.str "'via' and 'abstract' cannot be used together.") - -let locate_global_sort_inductive_or_constant sigma qid = - let locate_sort qid = - match Nametab.locate_extended qid with - | Globnames.TrueGlobal _ -> raise Not_found - | Globnames.SynDef kn -> - match Syntax_def.search_syntactic_definition kn with - | [], Notation_term.NSort r -> - let sigma,c = Evd.fresh_sort_in_family sigma (Glob_ops.glob_sort_family r) in - sigma,Constr.mkSort c - | _ -> raise Not_found in - try locate_sort qid - with Not_found -> - match Smartlocate.global_with_alias qid with - | GlobRef.IndRef i -> sigma, Constr.mkInd i - | _ -> sigma, Constr.mkConst (Smartlocate.global_constant_with_alias qid) - -let locate_global_constructor_inductive_or_constant qid = - let g = Smartlocate.global_with_alias qid in - match g with - | GlobRef.ConstructRef c -> g, Constr.mkConstruct c - | GlobRef.IndRef i -> g, Constr.mkInd i - | _ -> g, Constr.mkConst (Smartlocate.global_constant_with_alias qid) - -(* [get_type env sigma c] retrieves the type of [c] and returns a pair - [l, t] such that [c : l_0 -> ... -> l_n -> t]. *) -let get_type env sigma c = - (* inspired from [compute_implicit_names] in "interp/impargs.ml" *) - let rec aux env acc t = - let t = Reductionops.whd_all env sigma t in - match EConstr.kind sigma t with - | Constr.Prod (na, a, b) -> - let a = Reductionops.whd_all env sigma a in - let rel = Context.Rel.Declaration.LocalAssum (na, a) in - aux (EConstr.push_rel rel env) ((na, a) :: acc) b - | _ -> List.rev acc, t in - let t = Retyping.get_type_of env sigma (EConstr.of_constr c) in - let l, t = aux env [] t in - List.map (fun (na, a) -> na, EConstr.Unsafe.to_constr a) l, - EConstr.Unsafe.to_constr t - -(* [elaborate_to_post_params env sigma ty_ind params] builds the - [to_post] translation (c.f., interp/notation.mli) for the numeral - notation to parse/print type [ty_ind]. This translation is the - identity ([ToPostCopy]) except that it checks ([ToPostCheck]) that - the parameters of the inductive type [ty_ind] match the ones given - in [params]. *) -let elaborate_to_post_params env sigma ty_ind params = - let to_post_for_constructor indc = - let sigma, c = match indc with - | GlobRef.ConstructRef c -> - let sigma,c = Evd.fresh_constructor_instance env sigma c in - sigma, Constr.mkConstructU c - | _ -> assert false in (* c.f. get_constructors *) - let args, t = get_type env sigma c in - let params_indc = match Constr.kind t with - | Constr.App (_, a) -> Array.to_list a | _ -> [] in - let sz = List.length args in - let a = Array.make sz ToPostCopy in - if List.length params <> List.length params_indc then error_params ty_ind; - List.iter2 (fun param param_indc -> - match param, Constr.kind param_indc with - | Some p, Constr.Rel i when i <= sz -> a.(sz - i) <- ToPostCheck p - | _ -> ()) - params params_indc; - indc, indc, Array.to_list a in - let pt_refs = get_constructors ty_ind in - let to_post_0 = List.map to_post_for_constructor pt_refs in - let to_post = - let only_copy (_, _, args) = List.for_all ((=) ToPostCopy) args in - if (List.for_all only_copy to_post_0) then [||] else [|to_post_0|] in - to_post, pt_refs - -(* [elaborate_to_post_via env sigma ty_name ty_ind l] builds the [to_post] - translation (c.f., interp/notation.mli) for the number notation to - parse/print type [ty_name] through the inductive [ty_ind] according - to the pairs [constant, constructor] in the list [l]. *) -let elaborate_to_post_via env sigma ty_name ty_ind l = - let sigma, ty_name = - locate_global_sort_inductive_or_constant sigma ty_name in - let ty_ind = Constr.mkInd ty_ind in - (* Retrieve constants and constructors mappings and their type. - For each constant [cnst] and inductive constructor [indc] in [l], retrieve: - * its location: [lcnst] and [lindc] - * its GlobRef: [cnst] and [indc] - * its type: [tcnst] and [tindc] (decomposed in product by [get_type] above) - * [impls] are the implicit arguments of [cnst] *) - let l = - let read (consider_implicits, cnst, indc) = - let lcnst, lindc = cnst.CAst.loc, indc.CAst.loc in - let cnst, ccnst = locate_global_constructor_inductive_or_constant cnst in - let indc, cindc = - let indc = Smartlocate.global_constructor_with_alias indc in - GlobRef.ConstructRef indc, Constr.mkConstruct indc in - let get_type_wo_params c = - (* ignore parameters of inductive types *) - let rm_params c = match Constr.kind c with - | Constr.App (c, _) when Constr.isInd c -> c - | _ -> c in - let lc, tc = get_type env sigma c in - List.map (fun (n, c) -> n, rm_params c) lc, rm_params tc in - let tcnst, tindc = get_type_wo_params ccnst, get_type_wo_params cindc in - let impls = - if not consider_implicits then [] else - Impargs.(select_stronger_impargs (implicits_of_global cnst)) in - lcnst, cnst, tcnst, lindc, indc, tindc, impls in - List.map read l in - let eq_indc indc (_, _, _, _, indc', _, _) = GlobRef.equal indc indc' in - (* Collect all inductive types involved. - That is [ty_ind] and all final codomains of [tindc] above. *) - let inds = - List.fold_left (fun s (_, _, _, _, _, tindc, _) -> CSet.add (snd tindc) s) - (CSet.singleton ty_ind) l in - (* And for each inductive, retrieve its constructors. *) - let constructors = - CSet.fold (fun ind m -> - let inductive, _ = Constr.destInd ind in - CMap.add ind (get_constructors inductive) m) - inds CMap.empty in - (* Error if one [constructor] in some inductive in [inds] - doesn't appear exactly once in [l] *) - let _ = (* check_for duplicate constructor and error *) - List.fold_left (fun already_seen (_, cnst, _, loc, indc, _, _) -> - try - let cnst' = List.assoc_f GlobRef.equal indc already_seen in - remapping_error ?loc indc cnst' cnst - with Not_found -> (indc, cnst) :: already_seen) - [] l in - let () = (* check for missing constructor and error *) - CMap.iter (fun _ -> - List.iter (fun cstr -> - if not (List.exists (eq_indc cstr) l) then error_missing cstr)) - constructors in - (* Perform some checks on types and warn if they look strange. - These checks are neither sound nor complete, so we only warn. *) - let () = - (* associate inductives to types, and check that this mapping is one to one - and maps [ty_ind] to [ty_name] *) - let ind2ty, ty2ind = - let add loc ckey cval m = - match CMap.find_opt ckey m with - | None -> CMap.add ckey cval m - | Some old_cval -> - if not (Constr.equal old_cval cval) then - warn_via_remapping ?loc (env, sigma, ckey, old_cval, cval); - m in - List.fold_left - (fun (ind2ty, ty2ind) (lcnst, _, (_, tcnst), lindc, _, (_, tindc), _) -> - add lcnst tindc tcnst ind2ty, add lindc tcnst tindc ty2ind) - CMap.(singleton ty_ind ty_name, singleton ty_name ty_ind) l in - (* check that type of constants and constructors mapped in [l] - match modulo [ind2ty] *) - let rm_impls impls (l, t) = - let rec aux impls l = match impls, l with - | Some _ :: impls, _ :: b -> aux impls b - | None :: impls, (n, a) :: b -> (n, a) :: aux impls b - | _ -> l in - aux impls l, t in - let replace m (l, t) = - let apply_m c = try CMap.find c m with Not_found -> c in - List.fold_right (fun (na, a) b -> Constr.mkProd (na, (apply_m a), b)) - l (apply_m t) in - List.iter (fun (_, cnst, tcnst, loc, indc, tindc, impls) -> - let tcnst = rm_impls impls tcnst in - let tcnst' = replace CMap.empty tcnst in - if not (Constr.equal tcnst' (replace ind2ty tindc)) then - let actual = replace CMap.empty tindc in - let expected = replace ty2ind tcnst in - warn_via_type_mismatch ?loc (env, sigma, indc, cnst, expected, actual)) - l in - (* Associate an index to each inductive, starting from 0 for [ty_ind]. *) - let ind2num, num2ind, nb_ind = - CMap.fold (fun ind _ (ind2num, num2ind, i) -> - CMap.add ind i ind2num, Int.Map.add i ind num2ind, i + 1) - (CMap.remove ty_ind constructors) - (CMap.singleton ty_ind 0, Int.Map.singleton 0 ty_ind, 1) in - (* Finally elaborate [to_post] *) - let to_post = - let rec map_prod impls tindc = match impls with - | Some _ :: impls -> ToPostHole :: map_prod impls tindc - | _ -> - match tindc with - | [] -> [] - | (_, a) :: b -> - let t = match CMap.find_opt a ind2num with - | Some i -> ToPostAs i - | None -> ToPostCopy in - let impls = match impls with [] -> [] | _ :: t -> t in - t :: map_prod impls b in - Array.init nb_ind (fun i -> - List.map (fun indc -> - let _, cnst, _, _, _, tindc, impls = List.find (eq_indc indc) l in - indc, cnst, map_prod impls (fst tindc)) - (CMap.find (Int.Map.find i num2ind) constructors)) in - (* and use constants mapped to constructors of [ty_ind] as triggers. *) - 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 = - 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), l)) when allow_params -> - i, - List.map (function - | Notation_term.NRef r -> Some r - | Notation_term.NHole _ -> None - | _ -> raise Not_found) l - | _ -> raise Not_found in - try locate_param_inductive qid - with Not_found -> Smartlocate.global_inductive_with_alias qid, [] - -let vernac_number_notation local ty f g opts scope = - let rec parse_opts = function - | [] -> None, Nop - | h :: opts -> - let via, opts = parse_opts opts in - let via = match h, via with - | Via _, Some _ -> multiple_via_error () - | Via v, None -> Some v - | _ -> via in - let opts = match h, opts with - | After _, (Warning _ | Abstract _) -> multiple_after_error () - | After a, Nop -> a - | _ -> opts in - via, opts in - let via, opts = parse_opts opts in - (match via, opts with Some _, Abstract _ -> via_abstract_error () | _ -> ()); - let env = Global.env () in - let sigma = Evd.from_env env in - let num_ty = locate_number () in - let z_pos_ty = locate_z () in - let int63_ty = locate_int63 () 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 = mkRefC ty in - let app x y = mkAppC (x,[y]) in - let arrow x y = - mkProdC ([CAst.make Anonymous],Default Glob_term.Explicit, x, y) - in - let opt r = app (mkRefC (q_option ())) r in - (* Check the type of f *) - let to_kind = - match num_ty with - | Some (int_ty, cint, _, _, _, _, _, _) when has_type env sigma f (arrow cint cty) -> Int int_ty, Direct - | Some (int_ty, cint, _, _, _, _, _, _) when has_type env sigma f (arrow cint (opt cty)) -> Int int_ty, Option - | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma f (arrow cuint cty) -> UInt int_ty, Direct - | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma f (arrow cuint (opt cty)) -> UInt int_ty, Option - | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma f (arrow cnum cty) -> Number num_ty, Direct - | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma f (arrow cnum (opt cty)) -> Number num_ty, Option - | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma f (arrow cint cty) -> DecimalInt int_ty, Direct - | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma f (arrow cint (opt cty)) -> DecimalInt int_ty, Option - | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma f (arrow cuint cty) -> DecimalUInt int_ty, Direct - | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma f (arrow cuint (opt cty)) -> DecimalUInt int_ty, Option - | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma f (arrow cdec cty) -> Decimal num_ty, Direct - | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma f (arrow cdec (opt cty)) -> Decimal num_ty, Option - | _ -> - match z_pos_ty with - | Some (z_pos_ty, cZ) when has_type env sigma f (arrow cZ cty) -> Z z_pos_ty, Direct - | 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 - | _ -> type_error_to f ty - in - (* Check the type of g *) - let of_kind = - match num_ty with - | Some (int_ty, cint, _, _, _, _, _, _) when has_type env sigma g (arrow cty cint) -> Int int_ty, Direct - | Some (int_ty, cint, _, _, _, _, _, _) when has_type env sigma g (arrow cty (opt cint)) -> Int int_ty, Option - | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma g (arrow cty cuint) -> UInt int_ty, Direct - | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma g (arrow cty (opt cuint)) -> UInt int_ty, Option - | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma g (arrow cty cnum) -> Number num_ty, Direct - | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma g (arrow cty (opt cnum)) -> Number num_ty, Option - | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma g (arrow cty cint) -> DecimalInt int_ty, Direct - | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma g (arrow cty (opt cint)) -> DecimalInt int_ty, Option - | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma g (arrow cty cuint) -> DecimalUInt int_ty, Direct - | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma g (arrow cty (opt cuint)) -> DecimalUInt int_ty, Option - | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma g (arrow cty cdec) -> Decimal num_ty, Direct - | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma g (arrow cty (opt cdec)) -> Decimal num_ty, Option - | _ -> - match z_pos_ty with - | Some (z_pos_ty, cZ) when has_type env sigma g (arrow cty cZ) -> Z z_pos_ty, Direct - | 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 - | _ -> type_error_of g ty - in - (match to_kind, of_kind with - | ((DecimalInt _ | DecimalUInt _ | Decimal _), _), _ - | _, ((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 o = { to_kind; to_ty; to_post; of_kind; of_ty; ty_name; - 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 = NumberNotation o; - pt_required = Nametab.path_of_global (GlobRef.IndRef tyc),[]; - pt_refs; - pt_in_match = true } - in - enable_prim_token_interpretation i diff --git a/plugins/syntax/numeral.mli b/plugins/syntax/numeral.mli deleted file mode 100644 index 5a13d1068b..0000000000 --- a/plugins/syntax/numeral.mli +++ /dev/null @@ -1,26 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* - qualid -> - qualid -> qualid -> - number_option list -> - Notation_term.scope_name -> unit diff --git a/plugins/syntax/numeral_notation_plugin.mlpack b/plugins/syntax/numeral_notation_plugin.mlpack deleted file mode 100644 index f4d9cae3ff..0000000000 --- a/plugins/syntax/numeral_notation_plugin.mlpack +++ /dev/null @@ -1,2 +0,0 @@ -Numeral -G_numeral diff --git a/plugins/syntax/string_notation.ml b/plugins/syntax/string_notation.ml index dbb0e92d5c..98ea318c92 100644 --- a/plugins/syntax/string_notation.ml +++ b/plugins/syntax/string_notation.ml @@ -9,7 +9,6 @@ (************************************************************************) open Pp -open Util open Names open Libnames open Constrexpr diff --git a/plugins/syntax/string_notation_plugin.mlpack b/plugins/syntax/string_notation_plugin.mlpack deleted file mode 100644 index 6aa081dab4..0000000000 --- a/plugins/syntax/string_notation_plugin.mlpack +++ /dev/null @@ -1,2 +0,0 @@ -String_notation -G_string -- cgit v1.2.3 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') 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