full script generation

diff --git a/components/binaries/tptp2grafite/main.ml b/components/binaries/tptp2grafite/main.ml
index 0ecee127eb2d623c6d2d78a940c608abb3e334cd..cbdddf851c9d2a9233e68f5c9465429ffd01c0a9 100644 (file)
--- a/components/binaries/tptp2grafite/main.ml
+++ b/components/binaries/tptp2grafite/main.ml
@@ -1,6 +1,8 @@
 module GA = GrafiteAst;;
+module LA = LexiconAst;;
 module PT = CicNotationPt;;
 module A = Ast;;
+let floc = HExtlib.dummy_floc;;
 
 let rec collect_arities_from_term = function
   | A.Constant name -> [name,0]
@@ -25,7 +27,7 @@ let collect_arities_from_atom a =
     | A.Eq (t1,t2) -> collect_arities_from_term t1 @ collect_arities_from_term t2
     | A.NotEq (t1,t2) -> collect_arities_from_term t1 @ collect_arities_from_term t2
   in
-  HExtlib.list_uniq (List.sort (fun (a,_) (b,_) -> compare a b) (aux a))
+  aux a
 ;;
   
 let collect_fv_from_atom a = 
@@ -58,7 +60,7 @@ let rec mk_arrow component = function
   | n -> 
       PT.Binder 
         (`Forall,
-          ((PT.Variable (PT.FreshVar "_")),Some (PT.Ident (component,None))),
+          ((PT.Ident ("_",None)),Some (PT.Ident (component,None))),
           mk_arrow component (n-1))
 ;;
 
@@ -88,6 +90,12 @@ let convert_atom a =
   build_ctx_for_arities (List.map (fun x -> (x,0)) (collect_fv_from_atom a)) (aux a)
 ;;
 
+let collect_arities atom ctx = 
+  let atoms = atom::(List.map atom_of_formula ctx) in
+  HExtlib.list_uniq (List.sort (fun (a,_) (b,_) -> compare a b) 
+    (List.flatten (List.map collect_arities_from_atom atoms)))
+;;
+
 let rec convert_formula no_arities context f =
   let atom = atom_of_formula f in
   let t = convert_atom atom in
@@ -100,22 +108,26 @@ let rec convert_formula no_arities context f =
                        Some (convert_formula true [] hp)), 
             build_ctx (n+1) tl)
   in
-  let arities = if no_arities then [] else collect_arities_from_atom atom in
+  let arities = if no_arities then [] else collect_arities atom context in
   build_ctx_for_arities arities (build_ctx 0 context) 
 ;;
 
 let convert_ast statements context = function
   | A.Comment s -> 
       let s = String.sub s 1 (String.length s - 1) in
-      if s.[String.length s - 1] = '\n' then
-        s.[String.length s - 1] <- '\000';
-      statements @ [GA.Comment (HExtlib.dummy_floc,GA.Note (HExtlib.dummy_floc,s))],
+      let s = 
+        if s.[String.length s - 1] = '\n' then
+          String.sub s 0 (String.length s - 1)
+        else 
+          s
+      in
+      statements @ [GA.Comment (floc,GA.Note (floc,s))],
       context
   | A.Inclusion (s,_) ->
       statements @ [
         GA.Comment (
-          HExtlib.dummy_floc, GA.Note (
-            HExtlib.dummy_floc,"Inclusion of: " ^ s))], context
+          floc, GA.Note (
+            floc,"Inclusion of: " ^ s))], context
   | A.AnnotatedFormula (name,kind,f,_,_) -> 
       match kind with
       | A.Axiom 
@@ -131,8 +143,8 @@ let convert_ast statements context = function
           let o = PT.Theorem (`Theorem,name,f,None) in
           statements @ [
             GA.Executable(
-              HExtlib.dummy_floc,GA.Command(
-                HExtlib.dummy_floc,GA.Obj(HExtlib.dummy_floc,o)))],
+              floc,GA.Command(
+                floc,GA.Obj(floc,o)))],
           context
       | A.Definition 
       | A.Lemma 
@@ -209,5 +221,24 @@ let _ =
     print_endline 
       (GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp t)
   in
+  let extra_statements_start = [
+    GA.Executable(floc,GA.Command(floc,
+      GA.Set(floc,"baseuri","cic:/matita/TPTP/" ^ !inputfile)));
+    GA.Executable(floc,GA.Command(floc, GA.Include(floc,"legacy/coq.ma")))]
+  in
+  let extra_statements_end = [
+    GA.Executable(floc,GA.Tactical(floc, GA.Tactic(floc,
+      GA.Intros (floc,None,[])),Some (GA.Dot(floc))));
+    GA.Executable(floc,GA.Tactical(floc, GA.Tactic(floc,
+      GA.Auto (floc,None,None,Some "paramodulation",None)),
+      Some (GA.Dot(floc))));
+    GA.Executable(floc,GA.Command(floc, GA.Qed(floc)))]
+  in 
+  List.iter pp extra_statements_start;
+  print_endline
+    (LexiconAstPp.pp_command 
+      (LA.Alias(floc,
+        LA.Ident_alias("eq","cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)"))) ^ ".");
   List.iter pp grafite_ast_statements;
+  List.iter pp extra_statements_end;
   exit 0