39348
|
1 |
(* ========================================================================= *)
|
|
2 |
(* SOME SAMPLE PROBLEMS TO TEST PROOF PROCEDURES *)
|
|
3 |
(* Copyright (c) 2001 Joe Hurd, distributed under the GNU GPL version 2 *)
|
|
4 |
(* ========================================================================= *)
|
|
5 |
|
|
6 |
open Useful;
|
|
7 |
|
|
8 |
(* ------------------------------------------------------------------------- *)
|
|
9 |
(* The program name. *)
|
|
10 |
(* ------------------------------------------------------------------------- *)
|
|
11 |
|
|
12 |
val PROGRAM = "problems2tptp";
|
|
13 |
|
|
14 |
(* ------------------------------------------------------------------------- *)
|
|
15 |
(* Problem data. *)
|
|
16 |
(* ------------------------------------------------------------------------- *)
|
|
17 |
|
|
18 |
use "problems.sml";
|
|
19 |
|
|
20 |
(* ------------------------------------------------------------------------- *)
|
|
21 |
(* Helper functions. *)
|
|
22 |
(* ------------------------------------------------------------------------- *)
|
|
23 |
|
|
24 |
fun addSlash "" = ""
|
|
25 |
| addSlash dir =
|
|
26 |
if String.sub (dir, size dir - 1) = #"/" then dir
|
|
27 |
else dir ^ "/";
|
|
28 |
|
|
29 |
fun 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 (map #name problems)
|
|
38 |
in
|
|
39 |
dups names
|
|
40 |
end;
|
|
41 |
|
|
42 |
fun listProblem {name, comments = _, goal = _} = print (name ^ "\n");
|
|
43 |
|
|
44 |
fun 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 null comments then [] else "" :: comments) @
|
|
60 |
(if 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 |
|
|
100 |
datatype mode = OutputMode | ListMode;
|
|
101 |
|
|
102 |
val MODE : mode ref = ref OutputMode;
|
|
103 |
|
|
104 |
val COLLECTION : string option ref = ref NONE;
|
|
105 |
|
|
106 |
val OUTPUT_DIRECTORY : string option ref = ref NONE;
|
|
107 |
|
|
108 |
local
|
|
109 |
open Useful Options;
|
|
110 |
in
|
|
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)}];
|
|
127 |
end;
|
|
128 |
|
|
129 |
val VERSION = "1.0";
|
|
130 |
|
|
131 |
val versionString = PROGRAM^" v"^VERSION^"\n";
|
|
132 |
|
|
133 |
val 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 |
|
|
141 |
fun succeed () = Options.succeed programOptions;
|
|
142 |
fun fail mesg = Options.fail programOptions mesg;
|
|
143 |
fun usage mesg = Options.usage programOptions mesg;
|
|
144 |
|
|
145 |
val (opts,work) =
|
|
146 |
Options.processOptions programOptions (CommandLine.arguments ());
|
|
147 |
|
|
148 |
val () = if null work then () else usage "too many arguments";
|
|
149 |
|
|
150 |
(* ------------------------------------------------------------------------- *)
|
|
151 |
(* Top level. *)
|
|
152 |
(* ------------------------------------------------------------------------- *)
|
|
153 |
|
|
154 |
val () =
|
|
155 |
let
|
|
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
|
|
167 |
in
|
|
168 |
succeed ()
|
|
169 |
end
|
|
170 |
handle Error s => die (PROGRAM^" failed:\n" ^ s)
|
|
171 |
| Bug s => die ("BUG found in "^PROGRAM^" program:\n" ^ s);
|