X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftptp_grafite%2Ftptp2grafite.ml;h=a19fa67c20d3281967d8ec77a754f84ede510a51;hb=a7237500e8a2a4237a6ae8ba4b8301f7bbcb6acb;hp=667b7e3d6e3dbe052078b583b9efb02f384676e2;hpb=d765468f2df1976b995a2047fe76a6032c84840b;p=helm.git

diff --git a/helm/software/components/tptp_grafite/tptp2grafite.ml b/helm/software/components/tptp_grafite/tptp2grafite.ml
index 667b7e3d6..a19fa67c2 100644
--- a/helm/software/components/tptp_grafite/tptp2grafite.ml
+++ b/helm/software/components/tptp_grafite/tptp2grafite.ml
@@ -84,11 +84,18 @@ let rec convert_term = function
       PT.Appl (mk_ident name :: List.map convert_term args)
 ;;
 
-let rec atom_of_formula = function
-    | A.Disjunction (a,b) -> 
-        atom_of_formula a @ atom_of_formula b
-    | A.NegAtom a -> [a] (* removes the negation *)
-    | A.Atom a -> [a]
+let rec atom_of_formula neg pos = function
+    | A.Disjunction (a,b) ->
+        let neg, pos = atom_of_formula neg pos a in
+        atom_of_formula neg pos b 
+    | A.NegAtom a -> a::neg, pos 
+    | A.Atom (A.NotEq (a,b)) -> (A.Eq (a,b) :: neg), pos
+    | A.Atom a -> neg, a::pos
+;;
+
+let atom_of_formula f =
+  let neg, pos = atom_of_formula [] [] f in
+  neg @ pos
 ;;
   
 let rec mk_arrow component tail = function
@@ -207,7 +214,113 @@ 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.NDot(floc)])) ]
+  @      
+  (HExtlib.list_mapi
+   (fun (name,_) _-> 
+     GA.Executable(floc,GA.NTactic(floc, 
+      [GA.NIntro (floc,(try List.assoc name kw with Not_found -> name));
+       GA.NDot(floc)])))
+   arities)
+  @
+  (HExtlib.list_mapi
+   (fun _ i-> 
+     GA.Executable(floc,GA.NTactic(floc, 
+      [GA.NIntro (floc,"H"^string_of_int i);GA.NDot(floc)])))
+   context)
+  @
+(if fv <> [] then     
+  (List.flatten
+    (List.map 
+      (fun _ -> 
+        [GA.Executable(floc,GA.NTactic(floc, 
+          [GA.NApply (floc,
+            PT.Appl [mk_ident "ex_intro";PT.Implicit;PT.Implicit;
+              PT.Implicit;PT.Implicit]);GA.NBranch floc]));
+         GA.Executable(floc,GA.NTactic(floc, 
+          [GA.NPos (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.NSemicolon(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.NShift floc;
+               GA.NSkip floc; GA.NMerge floc]))])
+      fv)) 
+ else [])@
+    [GA.Executable(floc,GA.NTactic(floc,[GA.NTry(floc, GA.NAssumption(floc));
+					 GA.NSemicolon(floc)]))]@
+  [GA.Executable(floc,GA.NCommand(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 = 
@@ -233,53 +346,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 !depth])
-            ),
-              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 
@@ -310,7 +391,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
@@ -326,7 +407,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
@@ -335,30 +416,33 @@ let tptp2grafite ?(timeout=600) ?(def_depth=10) ?raw_preamble ~tptppath ~filenam
      * which will show up using the following command line:
      * ./tptp2grafite -tptppath ~tassi/TPTP-v3.1.1 GRP170-1 *)
     let width = max_int in
-    let term_pp content_term =
+    let term_pp prec content_term =
       let pres_term = TermContentPres.pp_ast content_term in
-      let dummy_tbl = Hashtbl.create 1 in
-      let markup = CicNotationPres.render dummy_tbl pres_term in
+      let lookup_uri = fun _ -> None in
+      let markup = CicNotationPres.render ~lookup_uri ~prec 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;
+    CicNotationPp.set_pp_term (term_pp 90);
     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:(term_pp 19) ~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
     | None -> 
-       pp (GA.Executable(floc,
-           GA.Command(floc,GA.Include(floc,"logic/equality.ma"))))
+      pp
+       (GA.Executable(floc,
+         GA.Command(floc,GA.Include(floc,true,`OldAndNew,"logic/equality.ma"))))
     | Some s -> s buri
   in
   let extra_statements_end = [] in