diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-05-27 23:22:04 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-10-17 02:19:11 +0200 |
| commit | 19bbc3fd946555aa1fa1fc23d805a4eb3d13bc45 (patch) | |
| tree | 678afe57f554900aa0c737dc36f53a4c3ece1577 /vernac | |
| parent | d9704f80a4f4b565f77368dbf7c9650d301a233d (diff) | |
[stm] Move interpretation state to Vernacentries
We still don't thread the state there, but this is a start of the
needed infrastructure.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacentries.ml | 19 | ||||
| -rw-r--r-- | vernac/vernacentries.mli | 13 |
2 files changed, 31 insertions, 1 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 66427b709..7f2985aca 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2227,3 +2227,22 @@ let interp ?(verbosely=true) ?proof (loc,c) = in if verbosely then Flags.verbosely (aux false) c else aux false c + +type interp_state = { (* TODO: inline records in OCaml 4.03 *) + system : States.state; (* summary + libstack *) + proof : Proof_global.state; (* proof state *) + shallow : bool (* is the state trimmed down (libstack) *) +} + +let freeze_interp_state marshallable = + { system = States.freeze ~marshallable; + proof = Proof_global.freeze ~marshallable; + shallow = (marshallable = `Shallow) } + +let unfreeze_interp_state { system; proof } = + States.unfreeze system; Proof_global.unfreeze proof + +let _dummy_interp_state = { system = Obj.magic 0; proof = Obj.magic 0; shallow = false } + +let interp ?verbosely ?proof st cmd = + interp ?verbosely ?proof cmd; st diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index a09011d24..5559e6b81 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -14,11 +14,22 @@ val dump_global : Libnames.reference or_by_notation -> unit val vernac_require : Libnames.reference option -> bool option -> Libnames.reference list -> unit +type interp_state = { (* TODO: inline records in OCaml 4.03 *) + system : States.state; (* summary + libstack *) + proof : Proof_global.state; (* proof state *) + shallow : bool (* is the state trimmed down (libstack) *) +} + +val freeze_interp_state : Summary.marshallable -> interp_state +val unfreeze_interp_state : interp_state -> unit +val _dummy_interp_state : interp_state + (** The main interpretation function of vernacular expressions *) val interp : ?verbosely:bool -> ?proof:Proof_global.closed_proof -> - Vernacexpr.vernac_expr Loc.located -> unit + interp_state -> + Vernacexpr.vernac_expr Loc.located -> interp_state (** Prepare a "match" template for a given inductive type. For each branch of the match, we list the constructor name |