X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgrafite_engine%2FgrafiteTypes.ml;fp=helm%2Focaml%2Fgrafite_engine%2FgrafiteTypes.ml;h=a13cc074e81f7a12379f6404405542485e741c8b;hb=827e35d6058ebba3a4a4fa6eb3c160f0cd0fd1e8;hp=0000000000000000000000000000000000000000;hpb=5b306342bf9befa57abd870527d6bd92b0a5ba50;p=helm.git

diff --git a/helm/ocaml/grafite_engine/grafiteTypes.ml b/helm/ocaml/grafite_engine/grafiteTypes.ml
new file mode 100644
index 000000000..a13cc074e
--- /dev/null
+++ b/helm/ocaml/grafite_engine/grafiteTypes.ml
@@ -0,0 +1,193 @@
+(* 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/
+ *)
+
+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. *)
+
+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;
+}
+
+let get_current_proof status =
+  match status.proof_status with
+  | Incomplete_proof { 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, _, proof, ty) } as incomplete_proof) ->
+        Incomplete_proof
+          { incomplete_proof with proof = (uri, metasenv, proof, ty) }
+    | 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 _ ->
+            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_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 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
+  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 }
+
+
+let get_string_option status name =
+  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";
+  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";
+  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