]> matita.cs.unibo.it Git - helm.git/blobdiff - components/tptp_grafite/main.ml
branch for universe
[helm.git] / components / tptp_grafite / main.ml
diff --git a/components/tptp_grafite/main.ml b/components/tptp_grafite/main.ml
new file mode 100644 (file)
index 0000000..e52b77c
--- /dev/null
@@ -0,0 +1,22 @@
+(* OPTIONS *)
+let tptppath = ref "./";;
+let spec = [
+  ("-tptppath", 
+      Arg.String (fun x -> tptppath := x), 
+      "Where to find the Axioms/ and Problems/ directory")
+]
+
+(* MAIN *)
+let _ =
+  let usage = "Usage: tptp2grafite [options] file" in
+  let inputfile = ref "" in
+  Arg.parse spec (fun s -> inputfile := s) usage;
+  if !inputfile = "" then 
+    begin
+      prerr_endline usage;
+      exit 1
+    end;
+  print_endline 
+    (Tptp2grafite.tptp2grafite ~filename:!inputfile ~tptppath:!tptppath ());
+  exit 0
+