--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+(* $Id$ *)
+
+exception Option_error of string * string
+exception Statement_error of string
+exception Command_error of string
+
+let command_error msg = raise (Command_error msg)
+
+type incomplete_proof = {
+ proof: ProofEngineTypes.proof;
+ stack: Continuationals.Stack.t;
+}
+
+type proof_status =
+ | No_proof
+ | 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
+ * 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 status = {
+ moo_content_rev: GrafiteMarshal.moo;
+ proof_status: proof_status;
+(* options: options; *)
+ objects: UriManager.uri list;
+ coercions: UriManager.uri list;
+ universe:Universe.universe;
+ baseuri: string;
+}
+
+let get_current_proof status =
+ match status.proof_status with
+ | Incomplete_proof { proof = p } -> p
+ | Proof p -> p
+ | _ -> raise (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_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
+
+let set_metasenv metasenv status =
+ let proof_status =
+ match status.proof_status with
+ | No_proof -> Intermediate metasenv
+ | Incomplete_proof ({ proof = (uri, _, subst, proof, ty, attrs) } as incomplete_proof) ->
+ Incomplete_proof
+ { incomplete_proof with proof = (uri, metasenv, subst, proof, ty, attrs) }
+ | Intermediate _ -> Intermediate metasenv
+ | Proof (_, metasenv', _, _, _, _) ->
+ assert (metasenv = metasenv');
+ status.proof_status
+ in
+ { status with proof_status = proof_status }
+
+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
+ | _ -> raise (Statement_error "no ongoing proof")
+
+let add_moo_content cmds status =
+ let content = status.moo_content_rev in
+ let content' =
+ List.fold_right
+ (fun cmd acc ->
+(* prerr_endline ("adding to moo command: " ^ GrafiteAstPp.pp_command cmd); *)
+ match cmd with
+ | GrafiteAst.Default _
+ | GrafiteAst.Index _
+ | GrafiteAst.Coercion _ ->
+ if List.mem cmd content then acc
+ else cmd :: acc
+ | _ -> cmd :: acc)
+ cmds content
+ in
+(* prerr_endline ("new moo content: " ^ String.concat " " (List.map
+ 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 types = [ (* no set options defined! *) ] in
+ let ty_and_mangler =
+ try List.assoc name types
+ with Not_found ->
+ command_error (Printf.sprintf "Unknown option \"%s\"" name)
+ in
+ let value =
+ match ty_and_mangler with
+ | `String, f -> String (f value)
+ | `Int, f ->
+ (try
+ Int (int_of_string (f value))
+ with Failure _ ->
+ command_error (Printf.sprintf "Not an integer value \"%s\"" value))
+ in
+ { status with options = StringMap.add name value status.options }
+
+
+let get_string_option status name =
+ match get_option status name with
+ | String s -> s
+ | _ -> raise (Option_error (name, "not a string value"))
+*)
+
+let dump_status status =
+ 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");
+ HLog.message "status.options\n";
+(* REMOVEME
+ StringMap.iter (fun k v ->
+ let v =
+ match v with
+ | String s -> s
+ | 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
+
projects / helm.git / blobdiff