(* 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
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
+
+let get_coercions new_grafite_status =
+ let e = get_estatus new_grafite_status in
+ e.NEstatus.rstatus.NRstatus.coerc_db
+;;
+
projects / helm.git / blobdiff