diff options
| -rw-r--r-- | interp/notation.ml | 82 | ||||
| -rw-r--r-- | interp/notation.mli | 9 | ||||
| -rw-r--r-- | plugins/syntax/ascii_syntax.ml | 2 | ||||
| -rw-r--r-- | plugins/syntax/g_numeral.ml4 | 2 | ||||
| -rw-r--r-- | plugins/syntax/int31_syntax.ml | 2 | ||||
| -rw-r--r-- | plugins/syntax/numeral.ml | 34 | ||||
| -rw-r--r-- | plugins/syntax/r_syntax.ml | 2 | ||||
| -rw-r--r-- | plugins/syntax/string_syntax.ml | 2 | ||||
| -rw-r--r-- | test-suite/vio/numeral.v | 21 |
9 files changed, 89 insertions, 67 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index eeee1ca899..02c7812e21 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -379,8 +379,14 @@ module InnerPrimToken = struct end -(* The following two tables of (un)interpreters will *not* be synchronized. - But their indexes will be checked to be unique *) +(* The following two tables of (un)interpreters will *not* be + synchronized. But their indexes will be checked to be unique. + These tables contain primitive token interpreters which are + registered in plugins, such as string and ascii syntax. It is + essential that only plugins add to these tables, and that + vernacular commands do not. See + https://github.com/coq/coq/issues/8401 for details of what goes + wrong when vernacular commands add to these tables. *) let prim_token_interpreters = (Hashtbl.create 7 : (prim_token_uid, InnerPrimToken.interpreter) Hashtbl.t) @@ -701,15 +707,36 @@ let uninterp o (Glob_term.AnyGlobConstr n) = | NotANumber -> None (* all other functions except big2raw *) end +(* A [prim_token_infos], which is synchronized with the document + state, either contains a unique id pointing to an unsynchronized + prim token function, or a numeral notation object describing how to + interpret and uninterpret. We provide [prim_token_infos] because + we expect plugins to provide their own interpretation functions, + rather than going through numeral notations, which are available as + a vernacular. *) + +type prim_token_interp_info = + Uid of prim_token_uid + | NumeralNotation of numeral_notation_obj + +type prim_token_infos = { + pt_local : bool; (** Is this interpretation local? *) + pt_scope : scope_name; (** Concerned scope *) + pt_interp_info : prim_token_interp_info; (** Unique id "pointing" to (un)interp functions, OR a numeral notation object describing (un)interp functions *) + pt_required : required_module; (** Module that should be loaded first *) + pt_refs : GlobRef.t list; (** Entry points during uninterpretation *) + pt_in_match : bool (** Is this prim token legal in match patterns ? *) +} + (* Table from scope_name to backtrack-able informations about interpreters (in particular interpreter unique id). *) let prim_token_interp_infos = - ref (String.Map.empty : (required_module * prim_token_uid) String.Map.t) + ref (String.Map.empty : (required_module * prim_token_interp_info) String.Map.t) (* Table from global_reference to backtrack-able informations about prim_token uninterpretation (in particular uninterpreter unique id). *) let prim_token_uninterp_infos = - ref (GlobRef.Map.empty : (scope_name * prim_token_uid * bool) GlobRef.Map.t) + ref (GlobRef.Map.empty : (scope_name * prim_token_interp_info * bool) GlobRef.Map.t) let hashtbl_check_and_set allow_overwrite uid f h eq = match Hashtbl.find h uid with @@ -739,23 +766,14 @@ let register_string_interpretation ?(allow_overwrite=false) uid (interp, uninter register_gen_interpretation allow_overwrite uid (InnerPrimToken.StringInterp interp, InnerPrimToken.StringUninterp uninterp) -type prim_token_infos = { - pt_local : bool; (** Is this interpretation local? *) - pt_scope : scope_name; (** Concerned scope *) - pt_uid : prim_token_uid; (** Unique id "pointing" to (un)interp functions *) - pt_required : required_module; (** Module that should be loaded first *) - pt_refs : GlobRef.t list; (** Entry points during uninterpretation *) - pt_in_match : bool (** Is this prim token legal in match patterns ? *) -} - let cache_prim_token_interpretation (_,infos) = + let ptii = infos.pt_interp_info in let sc = infos.pt_scope in - let uid = infos.pt_uid in check_scope ~tolerant:true sc; prim_token_interp_infos := - String.Map.add sc (infos.pt_required,infos.pt_uid) !prim_token_interp_infos; + String.Map.add sc (infos.pt_required,ptii) !prim_token_interp_infos; List.iter (fun r -> prim_token_uninterp_infos := - GlobRef.Map.add r (sc,uid,infos.pt_in_match) + GlobRef.Map.add r (sc,ptii,infos.pt_in_match) !prim_token_uninterp_infos) infos.pt_refs @@ -793,7 +811,7 @@ let declare_numeral_interpreter ?(local=false) sc dir interp (patl,uninterp,b) = enable_prim_token_interpretation { pt_local = local; pt_scope = sc; - pt_uid = uid; + pt_interp_info = Uid uid; pt_required = dir; pt_refs = List.map_filter glob_prim_constr_key patl; pt_in_match = b } @@ -803,7 +821,7 @@ let declare_string_interpreter ?(local=false) sc dir interp (patl,uninterp,b) = enable_prim_token_interpretation { pt_local = local; pt_scope = sc; - pt_uid = uid; + pt_interp_info = Uid uid; pt_required = dir; pt_refs = List.map_filter glob_prim_constr_key patl; pt_in_match = b } @@ -919,9 +937,12 @@ let find_prim_token check_allowed ?loc p sc = pat, df with Not_found -> (* Try for a primitive numerical notation *) - let (spdir,uid) = String.Map.find sc !prim_token_interp_infos in + let (spdir,info) = String.Map.find sc !prim_token_interp_infos in check_required_module ?loc sc spdir; - let interp = Hashtbl.find prim_token_interpreters uid in + let interp = match info with + | Uid uid -> Hashtbl.find prim_token_interpreters uid + | NumeralNotation o -> InnerPrimToken.RawNumInterp (Numeral.interp o) + in let pat = InnerPrimToken.do_interp ?loc interp p in check_allowed pat; pat, ((dirpath (fst spdir),DirPath.empty),"") @@ -1097,8 +1118,11 @@ let uninterp_prim_token c = | None -> raise Notation_ops.No_match | Some r -> try - let (sc,uid,_) = GlobRef.Map.find r !prim_token_uninterp_infos in - let uninterp = Hashtbl.find prim_token_uninterpreters uid in + let (sc,info,_) = GlobRef.Map.find r !prim_token_uninterp_infos in + let uninterp = match info with + | Uid uid -> Hashtbl.find prim_token_uninterpreters uid + | NumeralNotation o -> InnerPrimToken.RawNumUninterp (Numeral.uninterp o) + in match InnerPrimToken.do_uninterp uninterp (AnyGlobConstr c) with | None -> raise Notation_ops.No_match | Some n -> (sc,n) @@ -1113,12 +1137,16 @@ let availability_of_prim_token n printer_scope local_scopes = let f scope = try let uid = snd (String.Map.find scope !prim_token_interp_infos) in - let interp = Hashtbl.find prim_token_interpreters uid in let open InnerPrimToken in - match n, interp with - | Numeral _, (RawNumInterp _ | BigNumInterp _) -> true - | String _, StringInterp _ -> true - | _ -> false + match n, uid with + | Numeral _, NumeralNotation _ -> true + | _, NumeralNotation _ -> false + | _, Uid uid -> + let interp = Hashtbl.find prim_token_interpreters uid in + match n, interp with + | Numeral _, (RawNumInterp _ | BigNumInterp _) -> true + | String _, StringInterp _ -> true + | _ -> false with Not_found -> false in let scopes = make_current_scopes local_scopes in diff --git a/interp/notation.mli b/interp/notation.mli index 76bf70d452..734198bbf6 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -139,15 +139,14 @@ type numeral_notation_obj = num_ty : Libnames.qualid; (* for warnings / error messages *) warning : numnot_option } -module Numeral : sig - val interp : numeral_notation_obj -> rawnum prim_token_interpreter - val uninterp : numeral_notation_obj -> rawnum prim_token_uninterpreter -end +type prim_token_interp_info = + Uid of prim_token_uid + | NumeralNotation of numeral_notation_obj type prim_token_infos = { pt_local : bool; (** Is this interpretation local? *) pt_scope : scope_name; (** Concerned scope *) - pt_uid : prim_token_uid; (** Unique id "pointing" to (un)interp functions *) + pt_interp_info : prim_token_interp_info; (** Unique id "pointing" to (un)interp functions, OR a numeral notation object describing (un)interp functions *) pt_required : required_module; (** Module that should be loaded first *) pt_refs : GlobRef.t list; (** Entry points during uninterpretation *) pt_in_match : bool (** Is this prim token legal in match patterns ? *) diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index 5e36fbeb81..53153198f9 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -94,7 +94,7 @@ let _ = at_declare_ml_module enable_prim_token_interpretation { pt_local = false; pt_scope = sc; - pt_uid = sc; + pt_interp_info = Uid sc; pt_required = (ascii_path,ascii_module); pt_refs = [static_glob_Ascii]; pt_in_match = true } diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4 index 68b8178368..55f61a58f9 100644 --- a/plugins/syntax/g_numeral.ml4 +++ b/plugins/syntax/g_numeral.ml4 @@ -10,8 +10,8 @@ DECLARE PLUGIN "numeral_notation_plugin" -open Numeral open Notation +open Numeral open Pp open Names open Vernacinterp diff --git a/plugins/syntax/int31_syntax.ml b/plugins/syntax/int31_syntax.ml index d3ffe936a9..e34a401c2c 100644 --- a/plugins/syntax/int31_syntax.ml +++ b/plugins/syntax/int31_syntax.ml @@ -108,7 +108,7 @@ let _ = at_declare_ml_module enable_prim_token_interpretation { pt_local = false; pt_scope = int31_scope; - pt_uid = int31_scope; + pt_interp_info = Uid int31_scope; pt_required = (int31_path,int31_module); pt_refs = [int31_construct]; pt_in_match = true } diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml index 1a70c9536d..10a0af0b8f 100644 --- a/plugins/syntax/numeral.ml +++ b/plugins/syntax/numeral.ml @@ -27,29 +27,6 @@ let warn_abstract_large_num_no_op = Nametab.pr_global_env (Termops.vars_of_env (Global.env ())) f ++ strbrk ") targets an " ++ strbrk "option type.") -(* Here we only register the interp and uninterp functions - for a particular Numeral Notation (determined by a unique - string). The actual activation of the notation will be done - later (cf. Notation.enable_prim_token_interpretation). - This registration of interp/uninterp must be added in the - libstack, otherwise this won't work through a Require. *) - -let load_numeral_notation _ (_, (uid,opts)) = - Notation.register_rawnumeral_interpretation - ~allow_overwrite:true uid (Notation.Numeral.interp opts, Notation.Numeral.uninterp opts) - -let cache_numeral_notation x = load_numeral_notation 1 x - -(* TODO: substitution ? - TODO: uid pas stable par substitution dans opts - *) - -let inNumeralNotation : string * numeral_notation_obj -> Libobject.obj = - Libobject.declare_object { - (Libobject.default_object "NUMERAL NOTATION") with - Libobject.cache_function = cache_numeral_notation; - Libobject.load_function = load_numeral_notation } - let get_constructors ind = let mib,oib = Global.lookup_inductive ind in let mc = oib.Declarations.mind_consnames in @@ -154,15 +131,12 @@ let vernac_numeral_notation local ty f g scope opts = (match opts, to_kind with | Abstract _, (_, Option) -> warn_abstract_large_num_no_op o.to_ty | _ -> ()); - (* TODO: un hash suffit-il ? *) - let uid = Marshal.to_string o [] in - let i = Notation.( + let i = { pt_local = local; pt_scope = scope; - pt_uid = uid; + pt_interp_info = NumeralNotation o; pt_required = Nametab.path_of_global (IndRef tyc),[]; pt_refs = constructors; - pt_in_match = true }) + pt_in_match = true } in - Lib.add_anonymous_leaf (inNumeralNotation (uid,o)); - Notation.enable_prim_token_interpretation i + enable_prim_token_interpretation i diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index 04946c158b..49497aef54 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -143,7 +143,7 @@ let _ = at_declare_ml_module enable_prim_token_interpretation { pt_local = false; pt_scope = r_scope; - pt_uid = r_scope; + pt_interp_info = Uid r_scope; pt_required = (r_path,["Coq";"Reals";"Rdefinitions"]); pt_refs = [glob_IZR]; pt_in_match = false } diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml index 640bcfde91..7478c1e978 100644 --- a/plugins/syntax/string_syntax.ml +++ b/plugins/syntax/string_syntax.ml @@ -75,7 +75,7 @@ let _ = at_declare_ml_module enable_prim_token_interpretation { pt_local = false; pt_scope = sc; - pt_uid = sc; + pt_interp_info = Uid sc; pt_required = (string_path,["Coq";"Strings";"String"]); pt_refs = [static_glob_String; static_glob_EmptyString]; pt_in_match = true } diff --git a/test-suite/vio/numeral.v b/test-suite/vio/numeral.v new file mode 100644 index 0000000000..f28355bb29 --- /dev/null +++ b/test-suite/vio/numeral.v @@ -0,0 +1,21 @@ +Lemma foo : True. +Proof. +Check 0 : nat. +Check 0 : nat. +exact I. +Qed. + +Lemma bar : True. +Proof. +pose (0 : nat). +exact I. +Qed. + +Require Import Coq.Strings.Ascii. +Open Scope char_scope. + +Lemma baz : True. +Proof. +pose "s". +exact I. +Qed. |