diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-01 19:13:04 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-09 18:16:27 +0100 |
| commit | 8c9166435d6926babf697c3f575a8653f465cc76 (patch) | |
| tree | 146553666f8bc1cc619d9c30c4230232fea46464 /parsing/pcoq.mli | |
| parent | dea662ae5fd7225c06392e1b3f5acb1cd8e97e91 (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/pcoq.mli')
| -rw-r--r-- | parsing/pcoq.mli | 3 |
1 files changed, 3 insertions, 0 deletions
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 |