1(* ========================================================================= *)
2(* INTERFACE TO TPTP PROBLEM FILES                                           *)
3(* Copyright (c) 2001-2004 Joe Hurd.                                         *)
4(* ========================================================================= *)
5
6(*
7app load ["mlibStream", "mlibUseful", "mlibParser", "mlibTerm", "mlibSubst"];
8*)
9
10(*
11*)
12structure mlibTptp :> mlibTptp =
13struct
14
15open mlibParser mlibUseful mlibTerm;
16
17infixr 9 >>++;
18infixr 8 ++;
19infixr 7 >>;
20infixr 6 ||;
21infix |-> ## ::>;
22
23structure S = mlibStream; local open mlibStream in end;
24
25val |<>| = mlibSubst.|<>|;
26val op ::> = mlibSubst.::>;
27val term_subst = mlibSubst.term_subst;
28
29(* ------------------------------------------------------------------------- *)
30(* Abbreviating relation and function names in TPTP problems.                *)
31(* ------------------------------------------------------------------------- *)
32
33type rename = {tptp : string, fol : string, arity : int};
34
35val renaming : rename list ref = ref
36  [(* Mapping TPTP functions to nice symbols *)
37   {tptp = "equal",      fol = "=",  arity = 2},
38   {tptp = "equalish",   fol = "==", arity = 2},
39   {tptp = "less_equal", fol = "<=", arity = 2},
40   {tptp = "multiply",   fol = "*",  arity = 2},
41   {tptp = "divide",     fol = "/",  arity = 2},
42   {tptp = "add",        fol = "+",  arity = 2},
43   {tptp = "subtract",   fol = "-",  arity = 2},
44
45   (* Mapping HOL symbols to TPTP alphanumerics *)
46   {tptp = "bool",       fol = "$",  arity = 1},
47   {tptp = "type",       fol = ":",  arity = 2},
48   {tptp = "apply",      fol = "%",  arity = 2}]
49
50(* ------------------------------------------------------------------------- *)
51(* Reading from a TPTP file in CNF/FOF format: pass in a filename.           *)
52(* ------------------------------------------------------------------------- *)
53
54val comment = equal #"%" o hd o explode;
55
56val input_lines = S.filter (non comment) o S.from_textfile;
57
58val input_chars = S.flatten o S.map (S.from_list o explode);
59
60datatype tok_type = Lower | Upper | Punct;
61
62local
63  fun f [] = raise Bug "exact_puncts"
64    | f [x] = x | f (h :: t) = (h ++ f t) >> K ();
65in
66  val exact_puncts = f o map (fn c => exact (Punct, str c) >> K ()) o explode;
67end;
68
69val lexer =
70  (many (some space) ++
71   (((some lower || some digit) ++ many (some alphanum) >>
72     (fn (a, b) => (Lower, implode (a :: b)))) ||
73    (some upper ++ many (some alphanum) >>
74     (fn (a, b) => (Upper, implode (a :: b)))) ||
75    ((some symbol || some punct) >> (fn c => (Punct, str c))))) >> snd;
76
77val lex = many lexer ++ (many (some space) ++ finished) >> fst;
78
79val input_toks = S.from_list o fst o lex;
80
81local
82  fun mapped (f,a) (m : rename list) =
83    let fun g {tptp, arity, fol = _} = tptp = f andalso arity = length a
84    in case List.find g m of SOME {fol, ...} => (fol, a) | NONE => (f, a)
85    end;
86in
87  fun Fn' A = Fn (mapped A (!renaming));
88end;
89
90val var_parser = some (equal Upper o fst) >> snd;
91
92fun term_parser input =
93  ((var_parser >> Var) ||
94   ((some (equal Lower o fst) >> snd) ++
95    (optional
96     (exact (Punct, "(") ++ term_parser ++
97      many ((exact (Punct, ",") ++ term_parser) >> snd) ++
98      exact (Punct, ")")) >>
99     (fn SOME (_,(t,(ts,_))) => t :: ts | NONE => [])) >>
100    Fn')) input;
101
102val atom_parser =
103  term_parser >> (fn t => Atom (case t of Var v => Fn (v,[]) | _ => t));
104
105val literal_parser =
106  (((exact_puncts "++" >> K true) || (exact_puncts "--" >> K false)) ++
107   atom_parser) >> mk_literal;
108
109val clause_parser =
110  (exact (Lower, "input_clause") ++ exact (Punct, "(") ++ any ++
111   exact (Punct, ",") ++ any ++ exact (Punct, ",") ++ exact (Punct, "[") ++
112   literal_parser ++ many ((exact (Punct, ",") ++ literal_parser) >> snd) ++
113   exact (Punct, "]") ++ exact (Punct, ")") ++ exact (Punct, ".")) >>
114  (fn (_,(_,(name,(_,(typ,(_,(_,(l,(ls,_))))))))) =>
115   (snd name, snd typ, list_mk_disj (l :: ls)));
116
117val varl_parser =
118  (exact (Punct, "[") ++ var_parser ++
119   many ((exact (Punct, ",") ++ var_parser) >> snd) ++ exact (Punct, "]")) >>
120  (fn (_,(h,(t,_))) => h :: t);
121
122fun form_parser inp =
123  (qform_parser ++
124   (iform_parser "|" Or ||
125    iform_parser "&" And ||
126    iform_parser "<=>" Iff ||
127    iform_parser "<~>" (Not o Iff) ||
128    iform_parser "=>" Imp ||
129    iform_parser "<=" (Imp o swap) ||
130    iform_parser "~|" (Not o Or) ||
131    iform_parser "~&" (Not o And) ||
132    (nothing >> (fn () => I))) >>
133   (fn (a,f) => f a)) inp
134and iform_parser sym con inp =
135  (atleastone ((exact_puncts sym ++ qform_parser) >> snd)
136   >> (fn l => fn i =>
137       let val x = rev (i :: l) in foldl con (hd x) (tl x) end)) inp
138and qform_parser inp =
139  (((exact (Punct, "~") ++ qform_parser) >> (Not o snd)) ||
140   ((exact (Punct, "!") ++ varl_parser ++ exact (Punct, ":") ++ qform_parser)
141    >> (fn (_,(v,(_,b))) => list_mk_forall (v,b))) ||
142   ((exact (Punct, "?") ++ varl_parser ++ exact (Punct, ":") ++ qform_parser)
143    >> (fn (_,(v,(_,b))) => list_mk_exists (v,b))) ||
144   ((exact (Punct, "(") ++ form_parser ++ exact (Punct, ")"))
145    >> (fst o snd)) ||
146   atom_parser) inp;
147
148val fof_parser =
149  (exact (Lower, "input_formula") ++ exact (Punct, "(") ++ any ++
150   exact (Punct, ",") ++ any ++ exact (Punct, ",") ++ form_parser ++
151   exact (Punct, ")") ++ exact (Punct, ".")) >>
152  (fn (_,(_,(name,(_,(typ,(_,(f,_))))))) => (snd name, snd typ, f));
153
154datatype problem = CNF | FOF;
155
156val problem_parser =
157  fst o
158  (((many clause_parser ++ finished) >> (fn (a,_) => (CNF,a))) ||
159   ((many fof_parser ++ finished) >> (fn (a,_) => (FOF,a))));
160
161local
162  val to_form = list_mk_conj o map (fn (_,_,a) => generalize a);
163in
164  val input_problem =
165    (fn (CNF,(a,b)) => Imp (to_form a, Imp (to_form b, False))
166      | (FOF,(a,b)) => Imp (to_form a, if null b then False else to_form b)) o
167    (I ## List.partition (not o equal "conjecture" o #2)) o
168    problem_parser;
169end;
170
171val read = input_problem o input_toks o input_chars o input_lines;
172
173(* Quick testing
174installPP mlibTerm.pp_formula;
175val num1 = read "../../test/NUM001-1.tptp";
176val lcl9 = read "../../test/LCL009-1.tptp";
177val set11 = read "../../test/SET011+3.fof";
178*)
179
180(* ------------------------------------------------------------------------- *)
181(* Writing to a TPTP file in CNF format: pass in a formula and filename.     *)
182(* ------------------------------------------------------------------------- *)
183
184local
185  val separator =
186    "%-------------------------------------" ^
187    "-------------------------------------\n";
188
189  fun name n = "% File     : " ^ n ^ "\n";
190
191  fun varify s =
192    case explode s of [] => raise Error "write_cnf: empty string variable"
193    | x :: xs => if Char.isUpper x then s else implode (Char.toUpper x :: xs);
194
195  fun funify r s =
196    let
197      fun g {fol, arity, tptp = _} = fol = s andalso arity = r
198    in
199      case List.find g (!renaming) of SOME {tptp, ...} => tptp
200      | NONE =>
201        case explode s of [] => raise Error "write_cnf: empty string function"
202        | x :: y => if Char.isLower x then s else implode (Char.toLower x :: y)
203    end;
204
205  fun term pr =
206    let
207      fun tm (Var v) = pr (varify v)
208        | tm (Fn (f, l)) = (pr (funify (length l) f); tms l)
209      and tms [] = ()
210        | tms (x :: y) = (pr "("; tm x; app (fn z => (pr ","; tm z)) y)
211    in
212      tm
213    end
214
215  fun literal pr (Not (Atom a)) = (pr "--"; term pr a)
216    | literal pr (Atom a) = (pr "++"; term pr a)
217    | literal _ _ = raise Error "write_cnf: not in CNF";
218
219  fun clause pr ty (cl, n) =
220    let
221      val () = if n = 0 then () else pr "\n"
222      val () = pr ("input_clause(clause" ^ int_to_string n ^ "," ^ ty ^ ",\n")
223      val () = pr "    [";
224      val () =
225        case (strip_disj o snd o strip_forall) cl of [] => ()
226        | x :: y => (literal pr x; app (fn z => (pr ",\n     ";literal pr z)) y)
227      val () = pr "]).\n"
228    in
229      n + 1
230    end;
231in
232  fun write {filename = n} (Imp (a, Imp (b, False))) =
233    let
234      open TextIO
235      val h = openOut n
236      fun pr x = output (h, x)
237      val () = pr separator
238      val () = pr (name n)
239      val () = pr separator
240      val n = foldl (clause pr "hypothesis") 0 (strip_conj a)
241      val n = foldl (clause pr "conjecture") n (strip_conj b)
242      val () = assert (0 < n) (Error "write: no clauses")
243      val () = pr separator
244      val () = closeOut h
245    in
246      ()
247    end
248    | write _ _ = raise Error "write: not in CNF format";
249end;
250
251(* Quick testing
252val () = write num1 "../file";
253*)
254
255(* ------------------------------------------------------------------------- *)
256(* Making TPTP formulas more palatable.                                      *)
257(* ------------------------------------------------------------------------- *)
258
259local
260  fun cycle _ ([], _) = raise Bug "cycle"
261    | cycle f (h :: t, avoid) =
262    let val h' = f h avoid in (h', (t @ [h], h' :: avoid)) end;
263
264  exception Too_many_vars;
265
266  val vars = ["x", "y", "z", "v", "w"];
267
268  val MAX_PRIME = 3 * length vars;
269
270  fun f _ True = True
271    | f _ False = False
272    | f (s,_,_) (Atom tm) = Atom (term_subst s tm)
273    | f x (Not a) = Not (f x a)
274    | f x (And (a,b)) = And (f x a, f x b)
275    | f x (Or (a,b)) = Or (f x a, f x b)
276    | f x (Iff (a,b)) = Iff (f x a, f x b)
277    | f x (Imp (a,b)) = Imp (f x a, f x b)
278    | f x (Forall (v,b)) = g x Forall v b
279    | f x (Exists (v,b)) = g x Exists v b
280  and g (_,0,_) _ _ _ = raise Too_many_vars
281    | g (s,n,x) quant v b =
282    let
283      val variant_fn = if 0 <= n then variant else variant_num
284      val n = n - 1
285      val (w,x) = cycle variant_fn x
286      val s = (v |-> Var w) ::> s
287    in
288      quant (w, f (s,n,x) b)
289    end;
290
291  val prettify1 = f (|<>|, MAX_PRIME, (vars, []));
292  val prettify2 = f (|<>|, ~1, (vars, []));
293in
294  fun prettify fm = prettify1 fm handle Too_many_vars => prettify2 fm;
295end;
296
297(* Quick testing
298installPP mlibTerm.pp_formula;
299val num1 = (prettify o read) "../../test/NUM001-1.tptp";
300val lcl9 = (prettify o read) "../../test/LCL009-1.tptp";
301val set11 = (prettify o read) "../../test/SET011+3.tptp";
302*)
303
304end
305