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