1(* ========================================================================= *)
2(* SOME SAMPLE PROBLEMS TO TEST PROOF PROCEDURES                             *)
3(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
4(* ========================================================================= *)
5
6open Useful;
7
8(* ------------------------------------------------------------------------- *)
9(* The program name.                                                         *)
10(* ------------------------------------------------------------------------- *)
11
12val PROGRAM = "problems2tptp";
13
14(* ------------------------------------------------------------------------- *)
15(* Problem data.                                                             *)
16(* ------------------------------------------------------------------------- *)
17
18use "problems.sml";
19
20(* ------------------------------------------------------------------------- *)
21(* Helper functions.                                                         *)
22(* ------------------------------------------------------------------------- *)
23
24fun addSlash "" = ""
25  | addSlash dir =
26    if String.sub (dir, size dir - 1) = #"/" then dir
27    else dir ^ "/";
28
29fun checkProblems (problems : problem list) =
30    let
31      fun dups [] = ()
32        | dups [_] = ()
33        | dups (x :: (xs as x' :: _)) =
34          if x <> x' then dups xs
35          else raise Error ("duplicate problem name: " ^ x)
36
37      val names = sort String.compare (List.map #name problems)
38    in
39      dups names
40    end;
41
42fun listProblem {name, comments = _, goal = _} = TextIO.print (name ^ "\n");
43
44fun outputProblem outputDir {name,comments,goal} =
45    let
46      val filename = name ^ ".tptp"
47      val filename =
48          case outputDir of
49            NONE => filename
50          | SOME dir => addSlash dir ^ filename
51
52      val comment_bar = nChars #"-" 77
53      val comment_footer =
54          ["TPTP file created by " ^ host () ^ " at " ^
55           time () ^ " on " ^ date () ^ "."]
56      val comments =
57          [comment_bar] @
58          ["Name: " ^ name] @
59          (if List.null comments then [] else "" :: comments) @
60          (if List.null comment_footer then [] else "" :: comment_footer) @
61          [comment_bar]
62
63      val includes = []
64
65      val formulas =
66          let
67            val name = Tptp.FormulaName "goal"
68            val role = Tptp.ConjectureRole
69            val body = Tptp.FofFormulaBody (Formula.parse goal)
70            val source = Tptp.NoFormulaSource
71          in
72            [Tptp.Formula
73               {name = name,
74                role = role,
75                body = body,
76                source = source}]
77          end
78
79      val problem =
80          Tptp.Problem
81            {comments = comments,
82             includes = includes,
83             formulas = formulas}
84
85      val mapping = Tptp.defaultMapping
86
87      val () =
88          Tptp.write
89            {problem = problem,
90             mapping = mapping,
91             filename = filename}
92    in
93      ()
94    end;
95
96(* ------------------------------------------------------------------------- *)
97(* Program options.                                                          *)
98(* ------------------------------------------------------------------------- *)
99
100datatype mode = OutputMode | ListMode;
101
102val MODE : mode ref = ref OutputMode;
103
104val COLLECTION : string option ref = ref NONE;
105
106val OUTPUT_DIRECTORY : string option ref = ref NONE;
107
108local
109  open Useful Options;
110in
111  val specialOptions =
112      [{switches = ["--collection"], arguments = ["C"],
113        description = "restrict to the problems in collection C",
114        processor =
115          beginOpt
116            (stringOpt endOpt)
117            (fn _ => fn c => COLLECTION := SOME c)},
118       {switches = ["--list"], arguments = [],
119        description = "just list the problems",
120        processor = beginOpt endOpt (fn _ => MODE := ListMode)},
121       {switches = ["--output-dir"], arguments = ["DIR"],
122        description = "the output directory",
123        processor =
124          beginOpt
125            (stringOpt endOpt)
126            (fn _ => fn d => OUTPUT_DIRECTORY := SOME d)}];
127end;
128
129val VERSION = "1.0";
130
131val versionString = PROGRAM^" v"^VERSION^"\n";
132
133val programOptions =
134    {name    = PROGRAM,
135     version = versionString,
136     header  = "usage: "^PROGRAM^" [option ...]\n" ^
137               "Outputs the set of sample problems in TPTP format.\n",
138     footer  = "",
139     options = specialOptions @ Options.basicOptions};
140
141fun succeed () = Options.succeed programOptions;
142fun fail mesg = Options.fail programOptions mesg;
143fun usage mesg = Options.usage programOptions mesg;
144
145val (opts,work) =
146    Options.processOptions programOptions (CommandLine.arguments ());
147
148val () = if List.null work then () else usage "too many arguments";
149
150(* ------------------------------------------------------------------------- *)
151(* Top level.                                                                *)
152(* ------------------------------------------------------------------------- *)
153
154val () =
155let
156  val problems =
157      case !COLLECTION of
158        NONE => problems
159      | SOME c => List.filter (isCollection c) problems
160
161  val () = checkProblems problems
162
163  val () =
164      case !MODE of
165        ListMode => app listProblem problems
166      | OutputMode => app (outputProblem (!OUTPUT_DIRECTORY)) problems
167in
168  succeed ()
169end
170handle Error s => die (PROGRAM^" failed:\n" ^ s)
171     | Bug s => die ("BUG found in "^PROGRAM^" program:\n" ^ s);
172