Optimizer: refactored according to its formal description

[helm.git] / helm / software / components / tptp_grafite / tptp2grafite.ml

diff --git a/helm/software/components/tptp_grafite/tptp2grafite.ml b/helm/software/components/tptp_grafite/tptp2grafite.ml
index 841ac5f5c930948345c6037f682fd780889dba15..5a708ceddb8deb46c9a91602c6652d95a814c8e3 100644 (file)
--- a/helm/software/components/tptp_grafite/tptp2grafite.ml
+++ b/helm/software/components/tptp_grafite/tptp2grafite.ml
@@ -4,6 +4,8 @@ module PT = CicNotationPt;;
 module A = Ast;;
 let floc = HExtlib.dummy_floc;;
 
+let paramod_timeout = ref 600;;
+
 let universe = "Univ" ;;
 
 let kw = [
@@ -203,7 +205,7 @@ let convert_ast statements context = function
                 fv)) 
            else [])@
             [GA.Executable(floc,GA.Tactical(floc, GA.Tactic(floc,
-            GA.Auto (floc,["paramodulation",""])),
+            GA.Auto (floc,["paramodulation","";"timeout",string_of_int !paramod_timeout])),
               Some (GA.Dot(floc))));
             GA.Executable(floc,GA.Tactical(floc, GA.Try(floc,
               GA.Tactic (floc, GA.Assumption floc)), Some (GA.Dot(floc))))
@@ -249,7 +251,8 @@ let resolve ~tptppath s =
 ;;
 
 (* MAIN *)
-let tptp2grafite ?raw_preamble ~tptppath ~filename () =
+let tptp2grafite ?(timeout=600) ?raw_preamble ~tptppath ~filename () =
+  paramod_timeout := timeout;
   let rec aux = function
     | [] -> []
     | ((A.Inclusion (file,_)) as hd) :: tl ->
@@ -282,7 +285,7 @@ let tptp2grafite ?raw_preamble ~tptppath ~filename () =
     in
     CicNotationPp.set_pp_term term_pp;
     let lazy_term_pp = fun x -> assert false in
-    let obj_pp = CicNotationPp.pp_obj in
+    let obj_pp = CicNotationPp.pp_obj CicNotationPp.pp_term in
     GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp t
   in
   let buri = Pcre.replace ~pat:"\\.p$" ("cic:/matita/TPTP/" ^ filename) in