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
(* Status in which the proof could be while it is being processed by the
type options = option_value StringMap.t
let no_options = StringMap.empty
-type ast_command = (CicNotationPt.term, GrafiteAst.obj) GrafiteAst.command
+type ast_command = (CicNotationPt.term, CicNotationPt.obj) GrafiteAst.command
type moo = ast_command list * GrafiteAst.metadata list
type status = {
proof_status: proof_status;
options: options;
objects: (UriManager.uri * string) list;
+ coercions: UriManager.uri list;
notation_ids: CicNotation.notation_id list;
}
let proof_status =
match status.proof_status with
| No_proof -> Intermediate metasenv
- | Incomplete_proof ((uri, _, proof, ty), goal) ->
- Incomplete_proof ((uri, metasenv, proof, ty), goal)
+ | Incomplete_proof ({ proof = (uri, _, proof, ty) } as incomplete_proof) ->
+ Incomplete_proof
+ { incomplete_proof with proof = (uri, metasenv, proof, ty) }
| Intermediate _ -> Intermediate metasenv
| Proof _ -> assert false
in
let dump_status status =
MatitaLog.message "status.aliases:\n";
- MatitaLog.message
- (DisambiguatePp.pp_environment status.aliases ^ "\n");
MatitaLog.message "status.proof_status:";
MatitaLog.message
(match status.proof_status with
?reuse:bool -> entry:mathViewer_entry -> UriManager.uri list -> unit
end
+let qualify status name = get_string_option status "baseuri" ^ "/" ^ name
+
+let get_current_proof status =
+ match status.proof_status with
+ | Incomplete_proof { proof = p } -> p
+ | _ -> statement_error "no ongoing proof"
+
+let get_proof_metasenv status =
+ match status.proof_status with
+ | No_proof -> []
+ | Proof (_, metasenv, _, _)
+ | Incomplete_proof { proof = (_, metasenv, _, _) }
+ | Intermediate metasenv ->
+ metasenv
+
+let get_proof_context status goal =
+ match status.proof_status with
+ | Incomplete_proof { proof = (_, metasenv, _, _) } ->
+ let (_, context, _) = CicUtil.lookup_meta goal metasenv in
+ context
+ | _ -> []
+
+let get_proof_conclusion status goal =
+ match status.proof_status with
+ | Incomplete_proof { proof = (_, metasenv, _, _) } ->
+ let (_, _, conclusion) = CicUtil.lookup_meta goal metasenv in
+ conclusion
+ | _ -> statement_error "no ongoing proof"
+
+let get_stack status =
+ match status.proof_status with
+ | Incomplete_proof p -> p.stack
+ | Proof _ -> Continuationals.Stack.empty
+ | _ -> assert false
+
+let set_stack stack status =
+ match status.proof_status with
+ | Incomplete_proof p ->
+ { status with proof_status = Incomplete_proof { p with stack = stack } }
+ | Proof _ ->
+ assert (Continuationals.Stack.is_empty stack);
+ status
+ | _ -> assert false
+