From 3099be05553dab10b41d864f4981860eb105f145 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Wed, 4 Apr 2018 16:06:50 +0200 Subject: Notation: remove support for prim tokens denoting inductive types in "return" This is prim token notations for inductive *types*, not values. So we're speaking of a scope where 0 is the type nat, 1 is the type bool, etc. To my knowledge, this feature hasn't ever been used, and is very unlikely to be used ever, so let's clean the code a bit by removing it. --- interp/notation.mli | 2 -- 1 file changed, 2 deletions(-) (limited to 'interp/notation.mli') diff --git a/interp/notation.mli b/interp/notation.mli index c921606484..e8408330af 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -110,8 +110,6 @@ val uninterp_prim_token : 'a glob_constr_g -> scope_name * prim_token val uninterp_prim_token_cases_pattern : 'a cases_pattern_g -> Name.t * scope_name * prim_token -val uninterp_prim_token_ind_pattern : - inductive -> cases_pattern list -> scope_name * prim_token val availability_of_prim_token : prim_token -> scope_name -> subscopes -> delimiters option option -- cgit v1.2.3 From b3c75936a4912ca794cdcecfeb92044552336c63 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Wed, 4 Apr 2018 10:43:38 +0200 Subject: prim notations backtrackable, their declarations now in two parts (API change) The first part (e.g. register_bignumeral_interpretation) deals only with the interp/uninterp closures. It should typically be done as a side effect during a syntax plugin loading. No prim notation are active yet after this phase. The second part (enable_prim_token_interpretation) activates the prim notation. It is now correctly talking to Summary and to the LibStack. To avoid "phantom" objects in libstack after a mere Require, this second part should be done inside a Mltop.declare_cache_obj The link between the two parts is a prim_token_uid (a string), which should be unique for each primitive notation. When this primitive notation is specific to a scope, the scope_name could be used as uid. Btw, the list of "patterns" for detecting when an uninterpreter should be considered is now restricted to a list of global_reference (inductive constructors, or injection functions such as IZR). The earlier API was accepting a glob_constr list, but was actually only working well for global_reference. A minimal compatibility is provided (declare_numeral_interpreter), but is discouraged, since it is known to store uncessary objects in the libstack. --- interp/notation.mli | 60 ++++++++++++++++++++++++++++++++++++++++++----------- 1 file changed, 48 insertions(+), 12 deletions(-) (limited to 'interp/notation.mli') diff --git a/interp/notation.mli b/interp/notation.mli index e8408330af..2545e494ef 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Bigint open Names open Libnames open Constrexpr @@ -75,24 +74,61 @@ val find_delimiters_scope : ?loc:Loc.t -> delimiters -> scope_name type notation_location = (DirPath.t * DirPath.t) * string type required_module = full_path * string list -type cases_pattern_status = bool (** true = use prim token in patterns *) +type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign -type 'a prim_token_interpreter = - ?loc:Loc.t -> 'a -> glob_constr +(** The unique id string below will be used to refer to a particular + registered interpreter/uninterpreter of numeral or string notation. + Using the same uid for different (un)interpreters will fail. + If at most one interpretation of prim token is used per scope, + then the scope name could be used as unique id. *) -type 'a prim_token_uninterpreter = - glob_constr list * (any_glob_constr -> 'a option) * cases_pattern_status +type prim_token_uid = string -type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign +type 'a prim_token_interpreter = ?loc:Loc.t -> 'a -> glob_constr +type 'a prim_token_uninterpreter = any_glob_constr -> 'a option -val declare_rawnumeral_interpreter : scope_name -> required_module -> - rawnum prim_token_interpreter -> rawnum prim_token_uninterpreter -> unit +type 'a prim_token_interpretation = + 'a prim_token_interpreter * 'a prim_token_uninterpreter -val declare_numeral_interpreter : scope_name -> required_module -> - bigint prim_token_interpreter -> bigint prim_token_uninterpreter -> unit +val register_rawnumeral_interpretation : + prim_token_uid -> rawnum prim_token_interpretation -> unit + +val register_bignumeral_interpretation : + prim_token_uid -> Bigint.bigint prim_token_interpretation -> unit + +val register_string_interpretation : + prim_token_uid -> string prim_token_interpretation -> unit + +type prim_token_infos = { + 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 : global_reference list; (** Entry points during uninterpretation *) + pt_in_match : bool (** Is this prim token legal in match patterns ? *) +} +(** Note: most of the time, the [pt_refs] field above will contain + inductive constructors (e.g. O and S for nat). But it could also be + injection functions such as IZR for reals. *) + +(** Activate a prim token interpretation whose unique id and functions + have already been registered. *) + +val enable_prim_token_interpretation : prim_token_infos -> unit + +(** Compatibility. + Avoid the next two functions, they will now store unnecessary + objects in the library segment. Instead, combine + [register_*_interpretation] and [enable_prim_token_interpretation] + (the latter inside a [Mltop.declare_cache_obj]). +*) + +val declare_numeral_interpreter : scope_name -> required_module -> + Bigint.bigint prim_token_interpreter -> + glob_constr list * Bigint.bigint prim_token_uninterpreter * bool -> unit val declare_string_interpreter : scope_name -> required_module -> - string prim_token_interpreter -> string prim_token_uninterpreter -> unit + string prim_token_interpreter -> + glob_constr list * string prim_token_uninterpreter * bool -> unit (** Return the [term]/[cases_pattern] bound to a primitive token in a given scope context*) -- cgit v1.2.3 From fa0f378c91286d9127777a06b1dc557f695c22ae Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 14 Jul 2018 06:25:22 -0400 Subject: Fix numeral notation for a rebase on top of master Some of this code is cargo-culted or kludged to work. As I understand it, the situation is as follows: There are two sorts of use-cases that need to be supported: 1. A plugin registers an OCaml function as a numeral interpreter. In this case, the function registration must be synchronized with the document state, but the functions should not be marshelled / stored in the .vo. 2. A vernacular registers a Gallina function as a numeral interpreter. In this case, the registration must be synchronized, and the function should be marshelled / stored in the .vo. In case (1), we can compare functions by pointer equality, and we should be able to rely on globally unique keys, even across backtracking. In case (2), we cannot compare functions by pointer equality (because they must be regenerated on unmarshelling when `Require`ing a .vo file), and we also cannot rely on any sort of unique key being both unique and persistent across files. The solution we use here is that we ask clients to provide "unique" keys, and that clients tell us whether or not to overwrite existing registered functions, i.e., to tell us whether or not we should expect interpreter functions to be globally unique under pointer equality. For plugins, a simple string suffices, as long as the string does not clash between different plugins. In the case of vernacular-registered functions, use marshell a description of all of the data used to generate the function, and use that string as a unique key which is expected to persist across files. Because we cannot rely on function-pointer uniqueness here, we tell the interpretation-registration to allow overwriting. ---- Some of this code is response to comments on the PR ---- Some code is to fix an issue that bignums revealed: Both Int31 and bignums registered numeral notations in int31_scope. We now prepend a globally unique identifier when registering numeral notations from OCaml plugins. This is permissible because we don't store the uid information for such notations in .vo files (assuming I'm understanding the code correctly). --- interp/notation.mli | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'interp/notation.mli') diff --git a/interp/notation.mli b/interp/notation.mli index 2545e494ef..1d01d75c82 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -91,19 +91,19 @@ type 'a prim_token_interpretation = 'a prim_token_interpreter * 'a prim_token_uninterpreter val register_rawnumeral_interpretation : - prim_token_uid -> rawnum prim_token_interpretation -> unit + ?allow_overwrite:bool -> prim_token_uid -> rawnum prim_token_interpretation -> unit val register_bignumeral_interpretation : - prim_token_uid -> Bigint.bigint prim_token_interpretation -> unit + ?allow_overwrite:bool -> prim_token_uid -> Bigint.bigint prim_token_interpretation -> unit val register_string_interpretation : - prim_token_uid -> string prim_token_interpretation -> unit + ?allow_overwrite:bool -> prim_token_uid -> string prim_token_interpretation -> unit type prim_token_infos = { 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 : global_reference list; (** Entry points during uninterpretation *) + pt_refs : GlobRef.t list; (** Entry points during uninterpretation *) pt_in_match : bool (** Is this prim token legal in match patterns ? *) } -- cgit v1.2.3 From e9d44aefa9d6058c72845788745468aa010708b5 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 23 Aug 2018 15:10:58 -0400 Subject: Make Numeral Notation obey Local/Global Thanks to Emilio and Pierre-Marie Pédrot for pointers. --- interp/notation.mli | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'interp/notation.mli') diff --git a/interp/notation.mli b/interp/notation.mli index 1d01d75c82..e5478eff48 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -100,6 +100,7 @@ val register_string_interpretation : ?allow_overwrite:bool -> prim_token_uid -> string prim_token_interpretation -> unit 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 *) @@ -123,10 +124,10 @@ val enable_prim_token_interpretation : prim_token_infos -> unit (the latter inside a [Mltop.declare_cache_obj]). *) -val declare_numeral_interpreter : scope_name -> required_module -> +val declare_numeral_interpreter : ?local:bool -> scope_name -> required_module -> Bigint.bigint prim_token_interpreter -> glob_constr list * Bigint.bigint prim_token_uninterpreter * bool -> unit -val declare_string_interpreter : scope_name -> required_module -> +val declare_string_interpreter : ?local:bool -> scope_name -> required_module -> string prim_token_interpreter -> glob_constr list * string prim_token_uninterpreter * bool -> unit -- cgit v1.2.3