From 0a50912f2577243a1f9e4068b02877b8e61181c9 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 24 Jul 2006 09:32:54 +0000 Subject: [PATCH] more work on matitaprover (no more XML and buris are created). now matita can start on a .p file. --- .../grafite_engine/grafiteEngine.ml | 9 +++-- .../tactics/paramodulation/equality.ml | 2 + helm/software/matita/.depend | 14 +++---- helm/software/matita/Makefile | 1 + helm/software/matita/matita.ml | 9 ++++- helm/software/matita/matitaGui.ml | 38 ++++++++++++++----- helm/software/matita/matitaScript.ml | 5 +++ helm/software/matita/matitaScript.mli | 1 + helm/software/matita/matitaprover.ml | 13 +++++-- helm/software/matita/matitaprover.mli | 29 ++++++++++++++ ...letin_sulle_meta_del_body_spacca_tutto.txt | 8 ++++ 11 files changed, 104 insertions(+), 25 deletions(-) create mode 100644 helm/software/matita/matitaprover.mli create mode 100644 helm/software/matita/tests/TPTP/da_indagare_perche_non_astrarre_i_letin_sulle_meta_del_body_spacca_tutto.txt diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index d99ab8593..6dff5468d 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/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/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml index 2dbc618f7..b7a8a9f6b 100644 --- a/helm/software/components/tactics/paramodulation/equality.ml +++ b/helm/software/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/helm/software/matita/.depend b/helm/software/matita/.depend index f67366bd7..8b64721da 100644 --- a/helm/software/matita/.depend +++ b/helm/software/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/helm/software/matita/Makefile b/helm/software/matita/Makefile index 9043c9ff8..c39fcee85 100644 --- a/helm/software/matita/Makefile +++ b/helm/software/matita/Makefile @@ -35,6 +35,7 @@ CMOS = \ matitaExcPp.cmo \ matitaEngine.cmo \ matitacLib.cmo \ + matitaprover.cmo \ applyTransformation.cmo \ matitaGtkMisc.cmo \ matitaScript.cmo \ diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml index a70063f5f..6e9fa5f23 100644 --- a/helm/software/matita/matita.ml +++ b/helm/software/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/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index b230adecc..bf97b4760 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/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/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index 79c4fc4c5..5ddfb2b9c 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/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/helm/software/matita/matitaScript.mli b/helm/software/matita/matitaScript.mli index bf0a873f2..b0a022683 100644 --- a/helm/software/matita/matitaScript.mli +++ b/helm/software/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/helm/software/matita/matitaprover.ml b/helm/software/matita/matitaprover.ml index 9ddef38e6..b3115ec26 100644 --- a/helm/software/matita/matitaprover.ml +++ b/helm/software/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/helm/software/matita/matitaprover.mli b/helm/software/matita/matitaprover.mli new file mode 100644 index 000000000..6295136b5 --- /dev/null +++ b/helm/software/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/helm/software/matita/tests/TPTP/da_indagare_perche_non_astrarre_i_letin_sulle_meta_del_body_spacca_tutto.txt b/helm/software/matita/tests/TPTP/da_indagare_perche_non_astrarre_i_letin_sulle_meta_del_body_spacca_tutto.txt new file mode 100644 index 000000000..8cdcba593 --- /dev/null +++ b/helm/software/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 -- 2.39.2