more work on matitaprover (no more XML and buris are created).

now matita can start on a .p file.

diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml
index d99ab859311367572eb866e6f675bdb5612a3028..6dff5468dc631abf05b87431898fe464e4c844dd 100644 (file)
--- a/components/grafite_engine/grafiteEngine.ml
+++ b/components/grafite_engine/grafiteEngine.ml
@@ -625,9 +625,12 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
           LibraryClean.clean_baseuris [value];
           assert (Http_getter_storage.is_empty value);
         end;
-        HExtlib.mkdir 
-          (Filename.dirname (Http_getter.filename ~writable:true (value ^
-            "/foo.con")));
+        if not (Helm_registry.get_opt_default Helm_registry.bool "matita.nodisk"
+                  ~default:false) 
+        then
+          HExtlib.mkdir 
+            (Filename.dirname (Http_getter.filename ~writable:true (value ^
+              "/foo.con")));
       end;
       GrafiteTypes.set_option status name value,[]
   | GrafiteAst.Drop loc -> raise Drop

diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml
index 2dbc618f7eec4a1d735197993661039b0d1de764..b7a8a9f6b2b0ef31783d8183d226bb1d7b4e8707 100644 (file)
--- a/components/tactics/paramodulation/equality.ml
+++ b/components/tactics/paramodulation/equality.ml
@@ -576,9 +576,11 @@ let parametrize_proof p l r ty =
   let mot = CicUtil.metas_of_term_set in
   let parameters = uniq (mot p @ mot l @ mot r) in 
   (* ?if they are under a lambda? *)
+(*
   let parameters = 
     HExtlib.list_uniq (List.sort Pervasives.compare parameters) 
   in
+*)
   let what = List.map (fun (i,l) -> Cic.Meta (i,l)) parameters in 
   let with_what, lift_no = 
     List.fold_right (fun _ (acc,n) -> ((Cic.Rel n)::acc),n+1) what ([],1) 

diff --git a/matita/.depend b/matita/.depend
index f67366bd7d031104d86dc45fc290ec5a5ffa7798..8b64721dad85a6824d24c9a6af250d6ae4605447 100644 (file)
--- a/matita/.depend
+++ b/matita/.depend
@@ -14,7 +14,7 @@ matitacLib.cmo: matitamakeLib.cmi matitaMisc.cmi matitaInit.cmi \
     matitaExcPp.cmi matitaEngine.cmi buildTimeConf.cmi matitacLib.cmi 
 matitacLib.cmx: matitamakeLib.cmx matitaMisc.cmx matitaInit.cmx \
     matitaExcPp.cmx matitaEngine.cmx buildTimeConf.cmx matitacLib.cmi 
-matitac.cmo: matitaprover.cmo matitamake.cmi matitadep.cmi matitaclean.cmi \
+matitac.cmo: matitaprover.cmi matitamake.cmi matitadep.cmi matitaclean.cmi \
     matitacLib.cmi gragrep.cmi 
 matitac.cmx: matitaprover.cmx matitamake.cmx matitadep.cmx matitaclean.cmx \
     matitacLib.cmx gragrep.cmx 
@@ -28,11 +28,11 @@ matitaGtkMisc.cmo: matitaTypes.cmi matitaGeneratedGui.cmo buildTimeConf.cmi \
     matitaGtkMisc.cmi 
 matitaGtkMisc.cmx: matitaTypes.cmx matitaGeneratedGui.cmx buildTimeConf.cmx \
     matitaGtkMisc.cmi 
-matitaGui.cmo: matitamakeLib.cmi matitaTypes.cmi matitaScript.cmi \
-    matitaMisc.cmi matitaMathView.cmi matitaGtkMisc.cmi \
+matitaGui.cmo: matitaprover.cmi matitamakeLib.cmi matitaTypes.cmi \
+    matitaScript.cmi matitaMisc.cmi matitaMathView.cmi matitaGtkMisc.cmi \
     matitaGeneratedGui.cmo matitaExcPp.cmi buildTimeConf.cmi matitaGui.cmi 
-matitaGui.cmx: matitamakeLib.cmx matitaTypes.cmx matitaScript.cmx \
-    matitaMisc.cmx matitaMathView.cmx matitaGtkMisc.cmx \
+matitaGui.cmx: matitaprover.cmx matitamakeLib.cmx matitaTypes.cmx \
+    matitaScript.cmx matitaMisc.cmx matitaMathView.cmx matitaGtkMisc.cmx \
     matitaGeneratedGui.cmx matitaExcPp.cmx buildTimeConf.cmx matitaGui.cmi 
 matitaInit.cmo: matitamakeLib.cmi buildTimeConf.cmi matitaInit.cmi 
 matitaInit.cmx: matitamakeLib.cmx buildTimeConf.cmx matitaInit.cmi 
@@ -53,9 +53,9 @@ matita.cmo: matitaTypes.cmi matitaScript.cmi matitaMathView.cmi \
 matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMathView.cmx \
     matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx 
 matitaprover.cmo: matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \
-    buildTimeConf.cmi 
+    buildTimeConf.cmi matitaprover.cmi 
 matitaprover.cmx: matitaInit.cmx matitaExcPp.cmx matitaEngine.cmx \
-    buildTimeConf.cmx 
+    buildTimeConf.cmx matitaprover.cmi 
 matitaScript.cmo: matitamakeLib.cmi matitaTypes.cmi matitaMisc.cmi \
     matitaGtkMisc.cmi matitaEngine.cmi buildTimeConf.cmi \
     applyTransformation.cmi matitaScript.cmi 

diff --git a/matita/Makefile b/matita/Makefile
index 9043c9ff83cd00e5e33765cbbf26beb4a5fc8de3..c39fcee85fc2f96d02a1ff78d75e589efde6f737 100644 (file)
--- a/matita/Makefile
+++ b/matita/Makefile
@@ -35,6 +35,7 @@ CMOS =                                \
        matitaExcPp.cmo         \
        matitaEngine.cmo        \
        matitacLib.cmo          \
+       matitaprover.cmo        \
        applyTransformation.cmo \
        matitaGtkMisc.cmo       \
        matitaScript.cmo        \

diff --git a/matita/matita.ml b/matita/matita.ml
index a70063f5fe19508501f0609ab22d7da6927e4078..6e9fa5f2395c2b3cec668f3b78bacbc0d7b1ad02 100644 (file)
--- a/matita/matita.ml
+++ b/matita/matita.ml
@@ -32,7 +32,14 @@ open GrafiteTypes
 
 (** {2 Initialization} *)
 
-let _ = MatitaInit.initialize_all ()
+let _ = 
+  MatitaInit.add_cmdline_spec
+    ["-tptppath",Arg.String 
+      (fun s -> Helm_registry.set_string "matita.tptppath" s),
+      "Where to find the Axioms/ and Problems/ directory"];
+  MatitaInit.initialize_all ()
+;;
+
 (* let _ = Saturation.init () (* ALB to link paramodulation *) *)
 
 (** {2 GUI callbacks} *)

diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml
index b230adecc50f41ae68cb8c22c3facd47b25ac30d..bf97b47607f144dfc42e27f34b6bfc7468571f40 100644 (file)
--- a/matita/matitaGui.ml
+++ b/matita/matitaGui.ml
@@ -1007,16 +1007,34 @@ class gui () =
     method loadScript file =       
       let script = MatitaScript.current () in
       script#reset (); 
-      script#assignFileName file;
-      let content =
-       if Sys.file_exists file then file
-       else BuildTimeConf.script_template
-      in
-       source_view#source_buffer#begin_not_undoable_action ();
-       script#loadFromFile content;
-       source_view#source_buffer#end_not_undoable_action ();
-       console#message ("'"^file^"' loaded.");
-       self#_enableSaveTo file
+      if Pcre.pmatch ~pat:"\\.p$" file then
+        begin
+          let tptppath = 
+            Helm_registry.get_opt_default Helm_registry.string ~default:"./"
+              "matita.tptppath"
+          in
+          let data = Matitaprover.p_to_ma ~filename:file ~tptppath in
+          let filename = Pcre.replace ~pat:"\\.p$" ~templ:".ma" file in
+          script#assignFileName filename;
+          source_view#source_buffer#begin_not_undoable_action ();
+          script#loadFromString data;
+          source_view#source_buffer#end_not_undoable_action ();
+          console#message ("'"^filename^"' loaded.");
+          self#_enableSaveTo filename
+        end
+      else
+        begin
+          script#assignFileName file;
+          let content =
+           if Sys.file_exists file then file
+           else BuildTimeConf.script_template
+          in
+           source_view#source_buffer#begin_not_undoable_action ();
+           script#loadFromFile content;
+           source_view#source_buffer#end_not_undoable_action ();
+           console#message ("'"^file^"' loaded.");
+           self#_enableSaveTo file
+        end
       
     method setStar name b =
       let l = main#scriptLabel in

diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml
index 79c4fc4c57136cb884940ceae897768587613ae5..5ddfb2b9c0a4c026aaffeb00ab8d73831c860b85 100644 (file)
--- a/matita/matitaScript.ml
+++ b/matita/matitaScript.ml
@@ -583,6 +583,11 @@ object (self)
     let grafite_status = self#grafite_status in
     List.iter (fun o -> o lexicon_status grafite_status) observers
 
+  method loadFromString s =
+    buffer#set_text s;
+    self#reset_buffer;
+    buffer#set_modified true
+
   method loadFromFile f =
     buffer#set_text (HExtlib.input_file f);
     self#reset_buffer;

diff --git a/matita/matitaScript.mli b/matita/matitaScript.mli
index bf0a873f29dc1f3e08e76a11e794872c2ab084ba..b0a02268378c133670eee9a42a8c069b09cf55fc 100644 (file)
--- a/matita/matitaScript.mli
+++ b/matita/matitaScript.mli
@@ -54,6 +54,7 @@ object
 
   method assignFileName : string -> unit (* to the current active file *)
   method loadFromFile : string -> unit
+  method loadFromString : string -> unit
   method saveToFile : unit -> unit
   method filename : string
 

diff --git a/matita/matitaprover.ml b/matita/matitaprover.ml
index 9ddef38e6a969c62ee6979e80f7a21f9f15805b6..b3115ec26e6feefff346bfba3ebb9f36b8053035 100644 (file)
--- a/matita/matitaprover.ml
+++ b/matita/matitaprover.ml
@@ -74,6 +74,14 @@ for @{ 'exists ${default
 "
 ;;
 
+let p_to_ma ~tptppath ~filename = 
+  let data = 
+     Tptp2grafite.tptp2grafite ~filename ~tptppath:tptppath
+     ~raw_preamble ()
+  in
+  data
+;;
+
 let main () =
   MatitaInit.fill_registry ();
   let tptppath = ref "./" in
@@ -91,10 +99,7 @@ let main () =
     | [file] -> file
     | _ -> prerr_endline "You must specify exactly one .p file."; exit 1
   in
-  let data = 
-     Tptp2grafite.tptp2grafite ~filename:inputfile ~tptppath:!tptppath
-     ~raw_preamble ()
-  in
+  let data = p_to_ma ~filename:inputfile ~tptppath:!tptppath in
 (*   prerr_endline data; *)
   let is = Ulexing.from_utf8_string data in
   let gs = GrafiteSync.init () in

diff --git a/matita/matitaprover.mli b/matita/matitaprover.mli
new file mode 100644 (file)
index 0000000..6295136
--- /dev/null
+++ b/matita/matitaprover.mli
@@ -0,0 +1,29 @@
+(* Copyright (C) 2006, 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/
+ *)
+
+val main: unit -> unit
+
+val p_to_ma: tptppath:string -> filename:string -> string
+

diff --git a/matita/tests/TPTP/da_indagare_perche_non_astrarre_i_letin_sulle_meta_del_body_spacca_tutto.txt b/matita/tests/TPTP/da_indagare_perche_non_astrarre_i_letin_sulle_meta_del_body_spacca_tutto.txt
new file mode 100644 (file)
index 0000000..8cdcba5
--- /dev/null
+++ b/matita/tests/TPTP/da_indagare_perche_non_astrarre_i_letin_sulle_meta_del_body_spacca_tutto.txt
@@ -0,0 +1,8 @@
+Unsatisfiable/BOO025-1.ma
+Unsatisfiable/BOO072-1.ma
+Unsatisfiable/BOO074-1.ma
+Unsatisfiable/GRP424-1.ma
+Unsatisfiable/GRP441-1.ma
+Unsatisfiable/GRP500-1.ma
+Unsatisfiable/LAT096-1.ma
+Unsatisfiable/LAT097-1.ma