tacticals are really tactics now, they have an AST at the same level of

[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 b4675066f6c0aac3fa85416463452cb96909c72f..7950ca15d4e25e329ef2f3f331c6b2b082b5a7c0 100644 (file)
--- a/helm/software/components/tptp_grafite/tptp2grafite.ml
+++ b/helm/software/components/tptp_grafite/tptp2grafite.ml
@@ -216,18 +216,18 @@ let rec check_if_formula_is_negative = function
 
 let ng_generate_tactics fv ueq_case context arities =
   [ GA.Executable(floc,GA.NTactic(floc, 
-      (GA.NIntro (floc,"Univ")),GA.Dot(floc))) ]
+     [GA.NIntro (floc,"Univ") ; GA.NDot(floc)])) ]
   @      
   (HExtlib.list_mapi
    (fun (name,_) _-> 
      GA.Executable(floc,GA.NTactic(floc, 
-      (GA.NIntro (floc,name)),GA.Dot(floc))))
+      [GA.NIntro (floc,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.Dot(floc))))
+      [GA.NIntro (floc,"H"^string_of_int i);GA.NDot(floc)])))
    context)
   @
 (if fv <> [] then     
@@ -235,12 +235,14 @@ let ng_generate_tactics fv ueq_case context arities =
     (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]))))])
+          [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, (
+  [GA.Executable(floc,GA.NTactic(floc, [
     if (*ueq_case*) true then
         GA.NAuto (floc,(
           HExtlib.list_mapi 
@@ -255,8 +257,8 @@ let ng_generate_tactics fv ueq_case context arities =
                 "size",string_of_int 20;
                 "timeout",string_of_int 10;
         ]))
-  ),
-    GA.Semicolon(floc)));
+ ;
+  GA.NSemicolon(floc)]));
 (*
   GA.Executable(floc,GA.NTactic(floc, Some (GA.Try(floc,
     GA.Assumption floc)), GA.Dot(floc)))
@@ -266,9 +268,8 @@ let ng_generate_tactics fv ueq_case context arities =
   (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)))])
+              [GA.Executable(floc,GA.NTactic(floc, [GA.NShift floc;
+               GA.NSkip floc; GA.NMerge floc]))])
       fv)) 
  else [])@
   [GA.Executable(floc,GA.Command(floc, GA.NQed(floc)))]
@@ -412,21 +413,21 @@ 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 lookup_uri = fun _ -> None in
-      let markup = CicNotationPres.render ~lookup_uri pres_term 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 
        ~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
     Pcre.replace ~pat:"theorem" ~templ:"ntheorem" 
      (GrafiteAstPp.pp_statement
-       ~map_unicode_to_tex:false ~term_pp ~lazy_term_pp ~obj_pp t)
+       ~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 = [