(* 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. *)
-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 ng_status =
+ | ProofMode of NTacStatus.tac_status
+ | CommandMode of NEstatus.extra_status
type status = {
moo_content_rev: GrafiteMarshal.moo;
proof_status: proof_status;
- options: options;
objects: UriManager.uri list;
- coercions: UriManager.uri list;
- universe:Universe.universe;
+ coercions: CoercDb.coerc_db;
+ automation_cache:AutomationCache.cache;
+ baseuri: string;
+ ng_status: ng_status;
}
+let get_lexicon x =
+ match x.ng_status with
+ | ProofMode t -> t.NTacStatus.istatus.NTacStatus.estatus.NEstatus.lstatus
+ | CommandMode e -> e.NEstatus.lstatus
+;;
+
+let set_lexicon new_lexicon_status new_grafite_status =
+ { new_grafite_status with ng_status =
+ match new_grafite_status.ng_status with
+ | CommandMode estatus ->
+ CommandMode
+ { estatus with NEstatus.lstatus = new_lexicon_status }
+ | ProofMode t ->
+ ProofMode
+ { t with NTacStatus.istatus =
+ { t.NTacStatus.istatus with NTacStatus.estatus =
+ { t.NTacStatus.istatus.NTacStatus.estatus with NEstatus.lstatus =
+ new_lexicon_status }}}}
+;;
+
+let set_coercions db new_grafite_status =
+ { new_grafite_status with ng_status =
+ match new_grafite_status.ng_status with
+ | CommandMode estatus ->
+ CommandMode
+ { estatus with NEstatus.rstatus =
+ { estatus.NEstatus.rstatus with NRstatus.coerc_db = db }}
+ | ProofMode t ->
+ ProofMode
+ { t with NTacStatus.istatus =
+ { t.NTacStatus.istatus with NTacStatus.estatus =
+ { t.NTacStatus.istatus.NTacStatus.estatus with NEstatus.rstatus =
+ { t.NTacStatus.istatus.NTacStatus.estatus.NEstatus.rstatus with NRstatus.coerc_db = db
+ }}}}}
+;;
+
+let get_estatus x =
+ match x.ng_status with
+ | ProofMode t -> t.NTacStatus.istatus.NTacStatus.estatus
+ | CommandMode e -> e
+;;
+
let get_current_proof status =
match status.proof_status with
| Incomplete_proof { proof = p } -> p
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
+
+let get_coercions new_grafite_status =
+ let e = get_estatus new_grafite_status in
+ e.NEstatus.rstatus.NRstatus.coerc_db
+;;
+