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;
}
{ status with proof_status = proof_status }
let dump_status status =
- MatitaLog.message "status.aliases:\n";
- MatitaLog.message
- (DisambiguatePp.pp_environment status.aliases ^ "\n");
- MatitaLog.message "status.proof_status:";
- MatitaLog.message
+ HLog.message "status.aliases:\n";
+ HLog.message "status.proof_status:";
+ HLog.message
(match status.proof_status with
| No_proof -> "no proof\n"
| Incomplete_proof _ -> "incomplete proof\n"
| Proof _ -> "proof\n"
| Intermediate _ -> "Intermediate\n");
- MatitaLog.message "status.options\n";
+ HLog.message "status.options\n";
StringMap.iter (fun k v ->
let v =
match v with
| String s -> s
| Int i -> string_of_int i
in
- MatitaLog.message (k ^ "::=" ^ v)) status.options;
- MatitaLog.message "status.coercions\n";
- MatitaLog.message "status.objects:\n";
+ HLog.message (k ^ "::=" ^ v)) status.options;
+ HLog.message "status.coercions\n";
+ HLog.message "status.objects:\n";
List.iter
(fun (u,_) ->
- MatitaLog.message (UriManager.string_of_uri u)) status.objects
+ HLog.message (UriManager.string_of_uri u)) status.objects
let get_option status name =
try
let s = Str.global_replace (Str.regexp "/$") "" s in
s
in
- let types =
- [ "baseuri", (`String, mangle_dir);
- "basedir", (`String, mangle_dir);
- ]
- in
+ let types = [ "baseuri", (`String, mangle_dir); ] in
let ty_and_mangler =
try
List.assoc name types
?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
+