src/Tools/Metis/src/problems2tptp.sml

GPL -> BSD

(* ========================================================================= *)
(* SOME SAMPLE PROBLEMS TO TEST PROOF PROCEDURES                             *)
(* Copyright (c) 2001-2007 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)

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);