aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-12-01 19:13:04 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-12-09 18:16:27 +0100
commit8c9166435d6926babf697c3f575a8653f465cc76 (patch)
tree146553666f8bc1cc619d9c30c4230232fea46464 /parsing
parentdea662ae5fd7225c06392e1b3f5acb1cd8e97e91 (diff)
[summary] Allow typed projections from global state + rework of internals.
In the transition towards a less global state handling we have the necessity of mix imperative setting [notably for the modules/section code] and functional handling of state [notably in the STM]. In that scenario, it is very convenient to have typed access to the Coq's `summary`. Thus, I reify the API to support typed access to the `summary`, and implement such access in a couple of convenient places. We also update some internal datatypes to simplify the `frozen` data type. We also remove the use of hashes as it doesn't really make things faster, and most operations are now over `Maps` anyways. I believe this goes in line with recent work by @ppedrot. We also deprecate the non-typed accessors, which were only supposed to be used in the STM, which is now ported to the finer primitives.
Diffstat (limited to 'parsing')
-rw-r--r--parsing/pcoq.ml4
-rw-r--r--parsing/pcoq.mli3
2 files changed, 5 insertions, 2 deletions
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 8e6a01aa3..b766f0c6b 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -611,8 +611,8 @@ let unfreeze (grams, lex) =
the lexer state should not be resetted, since it contains
keywords declared in g_*.ml4 *)
-let _ =
- Summary.declare_summary "GRAMMAR_LEXER"
+let parser_summary_tag =
+ Summary.declare_summary_tag "GRAMMAR_LEXER"
{ Summary.freeze_function = freeze;
Summary.unfreeze_function = unfreeze;
Summary.init_function = Summary.nop }
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index d17ccb0b4..3ca013a96 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -313,3 +313,6 @@ val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b
(** Location Utils *)
val to_coqloc : Ploc.t -> Loc.t
val (!@) : Ploc.t -> Loc.t
+
+type frozen_t
+val parser_summary_tag : frozen_t Summary.Dyn.tag