exception Option_error of string * string
exception Unbound_identifier of string
+type incomplete_proof = {
+ proof: ProofEngineTypes.proof;
+ stack: Continuationals.Stack.t;
+}
+
type proof_status =
No_proof
- | Incomplete_proof of ProofEngineTypes.status
+ | Incomplete_proof of incomplete_proof
| Proof of ProofEngineTypes.proof
| Intermediate of Cic.metasenv
val no_options : 'a StringMap.t
type ast_command = (CicNotationPt.term, GrafiteAst.obj) GrafiteAst.command
+type moo = ast_command list * GrafiteAst.metadata list (** <moo, metadata> *)
type status = {
- aliases: DisambiguateTypes.environment; (** disambiguation aliases *)
+ aliases: DisambiguateTypes.environment; (** disambiguation aliases *)
multi_aliases: DisambiguateTypes.multiple_environment;
- moo_content_rev: ast_command list;
- proof_status: proof_status;
+ moo_content_rev: moo;
+ proof_status: proof_status; (** logical status *)
options: options;
objects: (UriManager.uri * string) list; (** in-scope objects, with paths *)
- notation_ids: CicNotation.notation_id list; (** in-scope notation ids *)
+ coercions: UriManager.uri list; (** defined coercions *)
+ notation_ids: CicNotation.notation_id list; (** in-scope notation ids *)
}
val set_metasenv: Cic.metasenv -> status -> status
(** list is not reversed, head command will be the first emitted *)
val add_moo_content: ast_command list -> status -> status
+val add_moo_metadata: GrafiteAst.metadata list -> status -> status
val dump_status : status -> unit
val get_option : status -> StringMap.key -> option_value
method show_uri_list :
?reuse:bool -> entry:mathViewer_entry -> UriManager.uri list -> unit
end
+
+val qualify: status -> string -> string
+
+val get_current_proof: status -> ProofEngineTypes.proof
+val get_proof_metasenv: status -> Cic.metasenv
+val get_proof_context: status -> ProofEngineTypes.goal -> Cic.context
+val get_proof_conclusion: status -> ProofEngineTypes.goal -> Cic.term
+val get_stack: status -> Continuationals.Stack.t
+
+val set_stack: Continuationals.Stack.t -> status -> status
+