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. --- plugins/syntax/positive_syntax.ml | 22 ++++++++++++++-------- 1 file changed, 14 insertions(+), 8 deletions(-) (limited to 'plugins/syntax/positive_syntax.ml') diff --git a/plugins/syntax/positive_syntax.ml b/plugins/syntax/positive_syntax.ml index 0c82e47445..6fce4de9ef 100644 --- a/plugins/syntax/positive_syntax.ml +++ b/plugins/syntax/positive_syntax.ml @@ -91,11 +91,17 @@ let uninterp_positive (AnyGlobConstr p) = (* Declaring interpreters and uninterpreters for positive *) (************************************************************************) -let _ = Notation.declare_numeral_interpreter "positive_scope" - (positive_path,binnums) - interp_positive - ([DAst.make @@ GRef (glob_xI, None); - DAst.make @@ GRef (glob_xO, None); - DAst.make @@ GRef (glob_xH, None)], - uninterp_positive, - true) +open Notation + +let at_declare_ml_module f x = + Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name + +let _ = + let scope = "positive_scope" in + register_bignumeral_interpretation scope (interp_positive,uninterp_positive); + at_declare_ml_module enable_prim_token_interpretation + { pt_scope = scope; + pt_uid = scope; + pt_required = (positive_path,binnums); + pt_refs = [glob_xI; glob_xO; glob_xH]; + pt_in_match = true } -- cgit v1.2.3 From ec0ad20de8daf2ad9f3237de92a745247db845f5 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 21 Mar 2017 16:13:24 +0100 Subject: remove legacy syntax plugins subsumed by Numeral Notation --- plugins/syntax/positive_syntax.ml | 107 -------------------------------------- 1 file changed, 107 deletions(-) delete mode 100644 plugins/syntax/positive_syntax.ml (limited to 'plugins/syntax/positive_syntax.ml') diff --git a/plugins/syntax/positive_syntax.ml b/plugins/syntax/positive_syntax.ml deleted file mode 100644 index 6fce4de9ef..0000000000 --- a/plugins/syntax/positive_syntax.ml +++ /dev/null @@ -1,107 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* DAst.make ?loc @@ GApp (ref_xO,[pos_of q]) - | (q,true) when not (Bigint.equal q zero) -> DAst.make ?loc @@ GApp (ref_xI,[pos_of q]) - | (q,true) -> ref_xH - in - pos_of x - -let error_non_positive ?loc = - user_err ?loc ~hdr:"interp_positive" - (str "Only strictly positive numbers in type \"positive\".") - -let interp_positive ?loc n = - if is_strictly_pos n then pos_of_bignat ?loc n - else error_non_positive ?loc - -(**********************************************************************) -(* Printing positive via scopes *) -(**********************************************************************) - -let is_gr c gr = match DAst.get c with -| GRef (r, _) -> GlobRef.equal r gr -| _ -> false - -let rec bignat_of_pos x = DAst.with_val (function - | GApp (r ,[a]) when is_gr r glob_xO -> mult_2(bignat_of_pos a) - | GApp (r ,[a]) when is_gr r glob_xI -> add_1(mult_2(bignat_of_pos a)) - | GRef (a, _) when GlobRef.equal a glob_xH -> Bigint.one - | _ -> raise Non_closed_number - ) x - -let uninterp_positive (AnyGlobConstr p) = - try - Some (bignat_of_pos p) - with Non_closed_number -> - None - -(************************************************************************) -(* Declaring interpreters and uninterpreters for positive *) -(************************************************************************) - -open Notation - -let at_declare_ml_module f x = - Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name - -let _ = - let scope = "positive_scope" in - register_bignumeral_interpretation scope (interp_positive,uninterp_positive); - at_declare_ml_module enable_prim_token_interpretation - { pt_scope = scope; - pt_uid = scope; - pt_required = (positive_path,binnums); - pt_refs = [glob_xI; glob_xO; glob_xH]; - pt_in_match = true } -- cgit v1.2.3