blob: e9e06e6d8ec4341ab326adba77b0e95b94576526 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
module Parser : sig
type t
val init : unit -> t
val cur_state : unit -> t
val parse : t -> 'a Pcoq.Entry.t -> Pcoq.Parsable.t -> 'a
end
(** System State *)
module System : sig
(** The system state includes the summary and the libobject *)
type t
(** [protect f x] runs [f x] and discards changes in the system state *)
val protect : ('a -> 'b) -> 'a -> 'b
(** Load / Dump provide unsafe but convenient state dumping from / to disk *)
val dump : string -> unit
val load : string -> unit
end
module LemmaStack : sig
type t
val pop : t -> Declare.Proof.t * t option
val push : t option -> Declare.Proof.t -> t
val map : f:(Declare.Proof.t -> Declare.Proof.t) -> t -> t
val map_top : f:(Declare.Proof.t -> Declare.Proof.t) -> t -> t
val with_top : t -> f:(Declare.Proof.t -> 'a ) -> 'a
end
type t =
{ parsing : Parser.t
(** parsing state [parsing state may not behave 100% functionally yet, beware] *)
; system : System.t
(** summary + libstack *)
; lemmas : LemmaStack.t option
(** proofs of lemmas currently opened *)
; program : Declare.OblState.t
(** program mode table *)
; shallow : bool
(** is the state trimmed down (libstack) *)
}
val freeze_interp_state : marshallable:bool -> t
val unfreeze_interp_state : t -> unit
(* WARNING: Do not use, it will go away in future releases *)
val invalidate_cache : unit -> unit
(** STM-specific state handling *)
module Stm : sig
(** Proof state + meta/evar counters *)
type pstate
val pstate : t -> pstate
val set_pstate : t -> pstate -> t
(** Rest of the state, unfortunately this is used in low-level so we need to expose it *)
type non_pstate = Summary.frozen * Lib.frozen
val non_pstate : t -> non_pstate
(** Checks if two states have the same Environ.env (physical eq) *)
val same_env : t -> t -> bool
(** Call [Lib.drop_objects] on the state *)
val make_shallow : t -> t
end
(* Compatibility module: Do Not Use *)
module Declare : sig
exception NoCurrentProof
val there_are_pending_proofs : unit -> bool
val get_open_goals : unit -> int
val give_me_the_proof : unit -> Proof.t
val give_me_the_proof_opt : unit -> Proof.t option
val get_current_proof_name : unit -> Names.Id.t
val map_proof : (Proof.t -> Proof.t) -> unit
val with_current_proof :
(unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> 'a
val return_proof : unit -> Declare.Proof.closed_proof_output
val return_partial_proof : unit -> Declare.Proof.closed_proof_output
val close_future_proof
: feedback_id:Stateid.t
-> Declare.Proof.closed_proof_output Future.computation
-> Declare.Proof.proof_object
val close_proof
: opaque:Vernacexpr.opacity_flag
-> keep_body_ucst_separate:bool
-> Declare.Proof.proof_object
val discard_all : unit -> unit
val update_sigma_univs : UGraph.t -> unit
val get_current_context : unit -> Evd.evar_map * Environ.env
val get_all_proof_names : unit -> Names.Id.t list
val copy_terminators : src:LemmaStack.t option -> tgt:LemmaStack.t option -> LemmaStack.t option
(* Low-level stuff *)
val get : unit -> LemmaStack.t option
val set : LemmaStack.t option * Declare.OblState.t -> unit
val get_pstate : unit -> Declare.Proof.t option
val freeze : marshallable:bool -> LemmaStack.t option
val unfreeze : LemmaStack.t -> unit
end
[@@ocaml.deprecated "This module is internal and should not be used, instead, thread the proof state"]
|
