X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftptp_grafite%2Ftptp2grafite.ml;fp=helm%2Fsoftware%2Fcomponents%2Ftptp_grafite%2Ftptp2grafite.ml;h=b4675066f6c0aac3fa85416463452cb96909c72f;hb=11e495dda047bcdfa4267c06cad2d074fcffe3e3;hp=10ed2bc720fa8420eee1f09b7cd69763bd59363f;hpb=b7587a7dd68463086e8a6b7c14f10c1dc33f64ba;p=helm.git

diff --git a/helm/software/components/tptp_grafite/tptp2grafite.ml b/helm/software/components/tptp_grafite/tptp2grafite.ml
index 10ed2bc72..b4675066f 100644
--- a/helm/software/components/tptp_grafite/tptp2grafite.ml
+++ b/helm/software/components/tptp_grafite/tptp2grafite.ml
@@ -214,7 +214,109 @@ let rec check_if_formula_is_negative = function
   | A.Atom a -> check_if_atom_is_negative a
 ;;
 
-let convert_ast statements context = function
+let ng_generate_tactics fv ueq_case context arities =
+  [ GA.Executable(floc,GA.NTactic(floc, 
+      (GA.NIntro (floc,"Univ")),GA.Dot(floc))) ]
+  @      
+  (HExtlib.list_mapi
+   (fun (name,_) _-> 
+     GA.Executable(floc,GA.NTactic(floc, 
+      (GA.NIntro (floc,name)),GA.Dot(floc))))
+   arities)
+  @
+  (HExtlib.list_mapi
+   (fun _ i-> 
+     GA.Executable(floc,GA.NTactic(floc, 
+      (GA.NIntro (floc,"H"^string_of_int i)),GA.Dot(floc))))
+   context)
+  @
+(if fv <> [] then     
+  (List.flatten
+    (List.map 
+      (fun _ -> 
+        [GA.Executable(floc,GA.NTactic(floc, 
+          (GA.NApply (floc,mk_ident "ex_intro")),GA.Branch floc));
+         GA.Executable(floc,GA.NTactic(floc, GA.NId floc ,
+          (GA.Pos (floc,[2]))))])
+      fv)) 
+ else [])@
+  [GA.Executable(floc,GA.NTactic(floc, (
+    if (*ueq_case*) true then
+        GA.NAuto (floc,(
+          HExtlib.list_mapi 
+            (fun _ i -> 
+               mk_ident ("H" ^ string_of_int i)) 
+            context    
+                ,[]))
+    else
+        GA.NAuto (floc,([],[
+                "depth",string_of_int 5;
+                "width",string_of_int 5;
+                "size",string_of_int 20;
+                "timeout",string_of_int 10;
+        ]))
+  ),
+    GA.Semicolon(floc)));
+(*
+  GA.Executable(floc,GA.NTactic(floc, Some (GA.Try(floc,
+    GA.Assumption floc)), GA.Dot(floc)))
+*)
+  ]@
+(if fv <> [] then     
+  (List.flatten
+    (List.map 
+      (fun _ -> 
+        [GA.Executable(floc,GA.NTactic(floc, GA.NId floc, GA.Shift floc));
+         GA.Executable(floc,GA.NNonPunctuationTactical(floc, GA.Skip floc,
+         (GA.Merge floc)))])
+      fv)) 
+ else [])@
+  [GA.Executable(floc,GA.Command(floc, GA.NQed(floc)))]
+;;
+
+let generate_tactics fv ueq_case =
+  [GA.Executable(floc,GA.Tactic(floc, Some
+   (GA.Intros (floc,(None,[]))),GA.Dot(floc)))] @
+(if fv <> [] then     
+  (List.flatten
+    (List.map 
+      (fun _ -> 
+        [GA.Executable(floc,GA.Tactic(floc, Some
+          (GA.Exists floc),GA.Branch floc));
+         GA.Executable(floc,GA.Tactic(floc, None,
+          (GA.Pos (floc,[2]))))])
+      fv)) 
+ else [])@
+  [GA.Executable(floc,GA.Tactic(floc, Some (
+    if true (*ueq_case*) then
+        GA.AutoBatch (floc,([],["paramodulation","";
+        "timeout",string_of_int !paramod_timeout]))
+    else
+        GA.AutoBatch (floc,([],[
+                "depth",string_of_int 5;
+                "width",string_of_int 5;
+                "size",string_of_int 20;
+                "timeout",string_of_int 10;
+        ]))
+  ),
+    GA.Semicolon(floc)));
+  GA.Executable(floc,GA.Tactic(floc, Some (GA.Try(floc,
+    GA.Assumption floc)), GA.Dot(floc)))
+  ]@
+(if fv <> [] then     
+  (List.flatten
+    (List.map 
+      (fun _ -> 
+        [GA.Executable(floc,GA.Tactic(floc, None, GA.Shift floc));
+         GA.Executable(floc,GA.NonPunctuationTactical(floc, GA.Skip floc,
+         (GA.Merge floc)))])
+      fv)) 
+ else [])@
+  [GA.Executable(floc,GA.Command(floc, GA.Print(floc,"proofterm")));
+   GA.Executable(floc,GA.Command(floc, GA.Qed(floc)))]
+;;
+
+let convert_ast ng statements context = function
   | A.Comment s -> 
       let s = String.sub s 1 (String.length s - 1) in
       let s = 
@@ -240,58 +342,21 @@ let convert_ast statements context = function
       | A.Negated_conjecture ->
           let ueq_case = is_formulae_1eq_negated f in
           let fv = collect_fv_1stord_from_formulae f in 
-(*
-          if fv <> [] then 
-            prerr_endline ("FREE VARIABLES: " ^ String.concat "," fv);
-*)
+          let old_f = f in
           let f = 
             PT.Binder 
              (`Forall,
-               (mk_ident universe,Some (PT.Sort `Set)), 
+               (mk_ident universe,Some (PT.Sort (`Type (CicUniv.fresh ())))), 
                convert_formula fv false context f)
           in
           let o = PT.Theorem (`Theorem,name,f,None) in
-          statements @ [
-            GA.Executable(floc,GA.Command(floc,GA.Obj(floc,o)));
-            GA.Executable(floc,GA.Tactic(floc, Some
-             (GA.Intros (floc,(None,[]))),GA.Dot(floc)))] @
-          (if fv <> [] then     
-            (List.flatten
-              (List.map 
-                (fun _ -> 
-                  [GA.Executable(floc,GA.Tactic(floc, Some
-                    (GA.Exists floc),GA.Branch floc));
-                   GA.Executable(floc,GA.Tactic(floc, None,
-                    (GA.Pos (floc,[2]))))])
-                fv)) 
-           else [])@
-            [GA.Executable(floc,GA.Tactic(floc, Some (
-              if ueq_case then
-                  GA.AutoBatch (floc,([],["paramodulation","";
-                  "timeout",string_of_int !paramod_timeout]))
-              else
-                  GA.AutoBatch (floc,([],[
-                          "depth",string_of_int 5;
-                          "width",string_of_int 5;
-                          "size",string_of_int 20;
-                          "timeout",string_of_int 10;
-                  ]))
-            ),
-              GA.Semicolon(floc)));
-            GA.Executable(floc,GA.Tactic(floc, Some (GA.Try(floc,
-              GA.Assumption floc)), GA.Dot(floc)))
-            ]@
-          (if fv <> [] then     
-            (List.flatten
-              (List.map 
-                (fun _ -> 
-                  [GA.Executable(floc,GA.Tactic(floc, None, GA.Shift floc));
-                   GA.Executable(floc,GA.NonPunctuationTactical(floc, GA.Skip floc,
-                   (GA.Merge floc)))])
-                fv)) 
-           else [])@
-            [GA.Executable(floc,GA.Command(floc, GA.Print(floc,"proofterm")));
-             GA.Executable(floc,GA.Command(floc, GA.Qed(floc)))],
+          (statements @ 
+          [ GA.Executable(floc,GA.Command(floc,
+             (*if ng then GA.NObj (floc,o) else*) GA.Obj(floc,o))); ] @
+          if ng then 
+            ng_generate_tactics fv ueq_case context
+              (let atom = atom_of_formula old_f in collect_arities atom context)
+          else generate_tactics fv ueq_case),
           context
       | A.Definition 
       | A.Lemma 
@@ -322,7 +387,7 @@ let resolve ~tptppath s =
 ;;
 
 (* MAIN *)
-let tptp2grafite ?(timeout=600) ?(def_depth=10) ?raw_preamble ~tptppath ~filename () =
+let tptp2grafite ?(timeout=600) ?(def_depth=10) ?raw_preamble ~tptppath ~filename ~ng () =
   paramod_timeout := timeout;
   depth := def_depth;
   let rec aux = function
@@ -338,7 +403,7 @@ let tptp2grafite ?(timeout=600) ?(def_depth=10) ?raw_preamble ~tptppath ~filenam
   let grafite_ast_statements,_ = 
     List.fold_left 
       (fun (st, ctx) f -> 
-        let newst, ctx = convert_ast st ctx f in
+        let newst, ctx = convert_ast ng st ctx f in
         newst, ctx)
       ([],[]) statements 
   in
@@ -353,18 +418,20 @@ let tptp2grafite ?(timeout=600) ?(def_depth=10) ?raw_preamble ~tptppath ~filenam
       let markup = CicNotationPres.render ~lookup_uri pres_term in
       let s = BoxPp.render_to_string List.hd width markup ~map_unicode_to_tex:false in
       Pcre.substitute 
-        ~pat:"\\\\forall [Ha-z][a-z0-9_]*" ~subst:(fun x -> "\n" ^ x) s
+       ~rex:(Pcre.regexp ~flags:[`UTF8] "∀[Ha-z][a-z0-9_]*") ~subst:(fun x -> "\n" ^ x) 
+       s
     in
     CicNotationPp.set_pp_term term_pp;
     let lazy_term_pp = fun x -> assert false in
     let obj_pp = CicNotationPp.pp_obj CicNotationPp.pp_term in
-    GrafiteAstPp.pp_statement
-     ~map_unicode_to_tex:false ~term_pp ~lazy_term_pp ~obj_pp t
+    Pcre.replace ~pat:"theorem" ~templ:"ntheorem" 
+     (GrafiteAstPp.pp_statement
+       ~map_unicode_to_tex:false ~term_pp ~lazy_term_pp ~obj_pp t)
   in
   let buri = Pcre.replace ~pat:"\\.p$" ("cic:/matita/TPTP/" ^ filename) in
   let extra_statements_start = [
-    GA.Executable(floc,GA.Command(floc,
-    GA.Set(floc,"baseuri",buri)))]
+    (*GA.Executable(floc,GA.Command(floc,
+    GA.Set(floc,"baseuri",buri)))*)]
   in
   let preamble = 
     match raw_preamble with