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
type options = option_value StringMap.t
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 *)
- moo_content_rev: string list;(*CSC: GrafiteAst.command list would be better *)
- proof_status: proof_status;
+ aliases: DisambiguateTypes.environment; (** disambiguation aliases *)
+ multi_aliases: DisambiguateTypes.multiple_environment;
+ 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
val get_string_option : status -> StringMap.key -> string
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
+