src/Tools/Metis/src/problems2tptp.sml

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/problems2tptp.sml	Wed Jun 20 22:07:52 2007 +0200
@@ -0,0 +1,122 @@
+(* ========================================================================= *)
+(* SOME SAMPLE PROBLEMS TO TEST PROOF PROCEDURES                             *)
+(* Copyright (c) 2001-2007 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+open Useful;
+
+(* ------------------------------------------------------------------------- *)
+(* The program name.                                                         *)
+(* ------------------------------------------------------------------------- *)
+
+val PROGRAM = "problems2tptp";
+
+(* ------------------------------------------------------------------------- *)
+(* Problem data.                                                             *)
+(* ------------------------------------------------------------------------- *)
+
+use "problems.sml";
+
+(* ------------------------------------------------------------------------- *)
+(* Helper functions.                                                         *)
+(* ------------------------------------------------------------------------- *)
+
+fun addSlash "" = ""
+  | addSlash dir =
+    if String.sub (dir, size dir - 1) = #"/" then dir
+    else dir ^ "/";
+
+fun checkProblems (problems : problem list) =
+    let
+      fun dups [] = ()
+        | dups [_] = ()
+        | dups (x :: (xs as x' :: _)) =
+          if x <> x' then dups xs
+          else raise Error ("duplicate problem name: " ^ x)
+
+      val names = sort String.compare (map #name problems)
+    in
+      dups names
+    end;
+
+fun outputProblem outputDir {name,comments,goal} =
+    let
+      val filename = name ^ ".tptp"
+      val filename =
+          case outputDir of
+            NONE => filename
+          | SOME dir => addSlash dir ^ filename
+
+      val comment_bar = nChars #"-" 77
+      val comment_footer =
+          ["TPTP file created by " ^ host () ^ " at " ^
+           time () ^ " on " ^ date () ^ "."]
+      val comments =
+          [comment_bar] @
+          ["Name: " ^ name] @
+          (if null comments then [] else "" :: comments) @
+          (if null comment_footer then [] else "" :: comment_footer) @
+          [comment_bar]
+
+      val goal = Formula.parse goal
+      val formulas =
+          [Tptp.FofFormula {name = "goal", role = "conjecture", formula = goal}]
+
+      val problem = {comments = comments, formulas = formulas}
+    in
+      Tptp.write {filename = filename} problem
+    end;
+
+(* ------------------------------------------------------------------------- *)
+(* Program options.                                                          *)
+(* ------------------------------------------------------------------------- *)
+
+val OUTPUT_DIRECTORY : string option ref = ref NONE;
+
+local
+  open Useful Options;
+in
+  val specialOptions =
+      [{switches = ["--output"], arguments = ["DIR"],
+        description = "the output directory",
+        processor =
+          beginOpt
+            (stringOpt endOpt)
+            (fn _ => fn d => OUTPUT_DIRECTORY := SOME d)}];
+end;
+
+val VERSION = "1.0";
+
+val versionString = PROGRAM^" v"^VERSION^"\n";
+
+val programOptions =
+    {name    = PROGRAM,
+     version = versionString,
+     header  = "usage: "^PROGRAM^" [option ...]\n" ^
+               "Outputs the set of sample problems in TPTP format.\n",
+     footer  = "",
+     options = specialOptions @ Options.basicOptions};
+
+fun succeed () = Options.succeed programOptions;
+fun fail mesg = Options.fail programOptions mesg;
+fun usage mesg = Options.usage programOptions mesg;
+
+val (opts,work) =
+    Options.processOptions programOptions (CommandLine.arguments ());
+
+val () = if null work then () else usage "too many arguments";
+
+(* ------------------------------------------------------------------------- *)
+(* Top level.                                                                *)
+(* ------------------------------------------------------------------------- *)
+
+val () =
+let
+  val () = checkProblems problems
+
+  val () = app (outputProblem (!OUTPUT_DIRECTORY)) problems
+in
+  succeed ()
+end
+handle Error s => die (PROGRAM^" failed:\n" ^ s)
+     | Bug s => die ("BUG found in "^PROGRAM^" program:\n" ^ s);