(* Status in which the proof could be while it is being processed by the
* engine. No status entering/exiting the engine could be in it. *)
+(* REMOVE
module StringMap = Map.Make (String)
type option_value =
| String of string
| Int of int
-type options = option_value StringMap.t
-let no_options = StringMap.empty
+*)
+(* type options = option_value StringMap.t *)
+(* let no_options = StringMap.empty *)
type status = {
moo_content_rev: GrafiteMarshal.moo;
proof_status: proof_status;
- options: options;
+(* options: options; *)
objects: UriManager.uri list;
coercions: UriManager.uri list;
universe:Universe.universe;
+ baseuri: string;
}
let get_current_proof status =
let get_proof_metasenv status =
match status.proof_status with
| No_proof -> []
- | Proof (_, metasenv, _, _)
- | Incomplete_proof { proof = (_, metasenv, _, _) }
+ | Proof (_, metasenv, _, _, _, _)
+ | Incomplete_proof { proof = (_, metasenv, _, _, _, _) }
| Intermediate metasenv ->
metasenv
let proof_status =
match status.proof_status with
| No_proof -> Intermediate metasenv
- | Incomplete_proof ({ proof = (uri, _, proof, ty) } as incomplete_proof) ->
+ | Incomplete_proof ({ proof = (uri, _, subst, proof, ty, attrs) } as incomplete_proof) ->
Incomplete_proof
- { incomplete_proof with proof = (uri, metasenv, proof, ty) }
+ { incomplete_proof with proof = (uri, metasenv, subst, proof, ty, attrs) }
| Intermediate _ -> Intermediate metasenv
- | Proof (_, metasenv', _, _) ->
+ | Proof (_, metasenv', _, _, _, _) ->
assert (metasenv = metasenv');
status.proof_status
in
let get_proof_context status goal =
match status.proof_status with
- | Incomplete_proof { proof = (_, metasenv, _, _) } ->
+ | 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, _, _) } ->
+ | Incomplete_proof { proof = (_, metasenv, _, _, _, _) } ->
let (_, _, conclusion) = CicUtil.lookup_meta goal metasenv in
conclusion
| _ -> raise (Statement_error "no ongoing proof")
(* prerr_endline ("adding to moo command: " ^ GrafiteAstPp.pp_command cmd); *)
match cmd with
| GrafiteAst.Default _
- | GrafiteAst.Index _ ->
+ | GrafiteAst.Index _
+ | GrafiteAst.Coercion _ ->
if List.mem cmd content then acc
else cmd :: acc
| _ -> cmd :: acc)
GrafiteAstPp.pp_command content')); *)
{ status with moo_content_rev = content' }
+let get_baseuri status = status.baseuri;;
+
+(*
let get_option status name =
try
StringMap.find name status.options
with Not_found -> raise (Option_error (name, "not found"))
-
+
let set_option status name value =
- let mangle_dir s =
- let s = Str.global_replace (Str.regexp "//+") "/" s in
- let s = Str.global_replace (Str.regexp "/$") "" s in
- s
- in
- let types = [ "baseuri", (`String, mangle_dir); ] in
+ let types = [ (* no set options defined! *) ] in
let ty_and_mangler =
- try
- List.assoc name types
+ try List.assoc name types
with Not_found ->
command_error (Printf.sprintf "Unknown option \"%s\"" name)
in
with Failure _ ->
command_error (Printf.sprintf "Not an integer value \"%s\"" value))
in
- if StringMap.mem name status.options && name = "baseuri" then
- command_error "Redefinition of 'baseuri' is forbidden."
- else
{ status with options = StringMap.add name value status.options }
match get_option status name with
| String s -> s
| _ -> raise (Option_error (name, "not a string value"))
-
-let qualify status name = get_string_option status "baseuri" ^ "/" ^ name
+*)
let dump_status status =
HLog.message "status.aliases:\n";
| Proof _ -> "proof\n"
| Intermediate _ -> "Intermediate\n");
HLog.message "status.options\n";
+(* REMOVEME
StringMap.iter (fun k v ->
let v =
match v with
| Int i -> string_of_int i
in
HLog.message (k ^ "::=" ^ v)) status.options;
+*)
HLog.message "status.coercions\n";
HLog.message "status.objects:\n";
List.iter
(fun u -> HLog.message (UriManager.string_of_uri u)) status.objects
+