1 (* Title: HOL/Tools/ATP/atp_problem.ML
2 Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
3 Author: Jasmin Blanchette, TU Muenchen
5 Abstract representation of ATP problems and TPTP syntax.
8 signature ATP_PROBLEM =
10 datatype ('a, 'b) ho_term =
11 ATerm of 'a * ('a, 'b) ho_term list |
12 AAbs of ('a * 'b) * ('a, 'b) ho_term
13 datatype quantifier = AForall | AExists
14 datatype connective = ANot | AAnd | AOr | AImplies | AIff
15 datatype ('a, 'b, 'c) formula =
16 AQuant of quantifier * ('a * 'b option) list * ('a, 'b, 'c) formula |
17 AConn of connective * ('a, 'b, 'c) formula list |
21 AType of 'a * 'a ho_type list |
22 AFun of 'a ho_type * 'a ho_type |
23 ATyAbs of 'a list * 'a ho_type
25 datatype tff_polymorphism = TFF_Monomorphic | TFF_Polymorphic
26 datatype tff_explicitness = TFF_Implicit | TFF_Explicit
27 datatype thf_flavor = THF_Without_Choice | THF_With_Choice
32 TFF of tff_polymorphism * tff_explicitness |
35 datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
36 datatype 'a problem_line =
37 Decl of string * 'a * 'a ho_type |
38 Formula of string * formula_kind
39 * ('a, 'a ho_type, ('a, 'a ho_type) ho_term) formula
40 * (string, string ho_type) ho_term option
41 * (string, string ho_type) ho_term option
42 type 'a problem = (string * 'a problem_line list) list
48 val tptp_has_type : string
49 val tptp_type_of_types : string
50 val tptp_bool_type : string
51 val tptp_individual_type : string
52 val tptp_fun_type : string
53 val tptp_product_type : string
54 val tptp_forall : string
55 val tptp_ho_forall : string
56 val tptp_pi_binder : string
57 val tptp_exists : string
58 val tptp_ho_exists : string
59 val tptp_choice : string
63 val tptp_implies : string
66 val tptp_not_iff : string
68 val tptp_not_infix : string
69 val tptp_equal : string
70 val tptp_old_equal : string
71 val tptp_false : string
72 val tptp_true : string
73 val tptp_empty_list : string
74 val is_tptp_equal : string -> bool
75 val is_built_in_tptp_symbol : string -> bool
76 val is_tptp_variable : string -> bool
77 val is_tptp_user_symbol : string -> bool
78 val atype_of_types : (string * string) ho_type
79 val bool_atype : (string * string) ho_type
80 val individual_atype : (string * string) ho_type
81 val mk_anot : ('a, 'b, 'c) formula -> ('a, 'b, 'c) formula
83 connective -> ('a, 'b, 'c) formula -> ('a, 'b, 'c) formula
84 -> ('a, 'b, 'c) formula
86 bool option -> (bool option -> 'a -> 'b -> 'b) -> connective * 'a list
89 bool option -> (bool option -> 'a -> ('b, 'c, 'd) formula)
90 -> connective * 'a list -> ('b, 'c, 'd) formula
92 bool option -> (bool option -> 'c -> 'd -> 'd) -> ('a, 'b, 'c) formula
94 val formula_map : ('c -> 'd) -> ('a, 'b, 'c) formula -> ('a, 'b, 'd) formula
95 val is_format_thf : format -> bool
96 val is_format_typed : format -> bool
97 val tptp_lines_for_atp_problem : format -> string problem -> string list
98 val ensure_cnf_problem :
99 (string * string) problem -> (string * string) problem
100 val filter_cnf_ueq_problem :
101 (string * string) problem -> (string * string) problem
102 val declare_undeclared_syms_in_atp_problem :
103 string -> string -> (string * string) problem -> (string * string) problem
104 val nice_atp_problem :
105 bool -> ('a * (string * string) problem_line list) list
106 -> ('a * string problem_line list) list
107 * (string Symtab.table * string Symtab.table) option
110 structure ATP_Problem : ATP_PROBLEM =
118 datatype ('a, 'b) ho_term =
119 ATerm of 'a * ('a, 'b) ho_term list |
120 AAbs of ('a * 'b) * ('a, 'b) ho_term
121 datatype quantifier = AForall | AExists
122 datatype connective = ANot | AAnd | AOr | AImplies | AIff
123 datatype ('a, 'b, 'c) formula =
124 AQuant of quantifier * ('a * 'b option) list * ('a, 'b, 'c) formula |
125 AConn of connective * ('a, 'b, 'c) formula list |
128 datatype 'a ho_type =
129 AType of 'a * 'a ho_type list |
130 AFun of 'a ho_type * 'a ho_type |
131 ATyAbs of 'a list * 'a ho_type
133 datatype tff_polymorphism = TFF_Monomorphic | TFF_Polymorphic
134 datatype tff_explicitness = TFF_Implicit | TFF_Explicit
135 datatype thf_flavor = THF_Without_Choice | THF_With_Choice
141 TFF of tff_polymorphism * tff_explicitness |
144 datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
145 datatype 'a problem_line =
146 Decl of string * 'a * 'a ho_type |
147 Formula of string * formula_kind * ('a, 'a ho_type, ('a, 'a ho_type) ho_term) formula
148 * (string, string ho_type) ho_term option * (string, string ho_type) ho_term option
149 type 'a problem = (string * 'a problem_line list) list
151 (* official TPTP syntax *)
156 val tptp_has_type = ":"
157 val tptp_type_of_types = "$tType"
158 val tptp_bool_type = "$o"
159 val tptp_individual_type = "$i"
160 val tptp_fun_type = ">"
161 val tptp_product_type = "*"
162 val tptp_forall = "!"
163 val tptp_ho_forall = "!!"
164 val tptp_pi_binder = "!>"
165 val tptp_exists = "?"
166 val tptp_ho_exists = "??"
167 val tptp_choice = "@+"
171 val tptp_implies = "=>"
174 val tptp_not_iff = "<~>"
176 val tptp_not_infix = "!"
178 val tptp_old_equal = "equal"
179 val tptp_false = "$false"
180 val tptp_true = "$true"
181 val tptp_empty_list = "[]"
183 fun is_tptp_equal s = (s = tptp_equal orelse s = tptp_old_equal)
184 fun is_built_in_tptp_symbol s =
185 s = tptp_old_equal orelse not (Char.isAlpha (String.sub (s, 0)))
186 fun is_tptp_variable s = Char.isUpper (String.sub (s, 0))
187 val is_tptp_user_symbol = not o (is_tptp_variable orf is_built_in_tptp_symbol)
189 fun raw_polarities_of_conn ANot = (SOME false, NONE)
190 | raw_polarities_of_conn AAnd = (SOME true, SOME true)
191 | raw_polarities_of_conn AOr = (SOME true, SOME true)
192 | raw_polarities_of_conn AImplies = (SOME false, SOME true)
193 | raw_polarities_of_conn AIff = (NONE, NONE)
194 fun polarities_of_conn NONE = K (NONE, NONE)
195 | polarities_of_conn (SOME pos) =
196 raw_polarities_of_conn #> not pos ? pairself (Option.map not)
198 fun mk_anot (AConn (ANot, [phi])) = phi
199 | mk_anot phi = AConn (ANot, [phi])
200 fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
202 fun aconn_fold pos f (ANot, [phi]) = f (Option.map not pos) phi
203 | aconn_fold pos f (AImplies, [phi1, phi2]) =
204 f (Option.map not pos) phi1 #> f pos phi2
205 | aconn_fold pos f (AAnd, phis) = fold (f pos) phis
206 | aconn_fold pos f (AOr, phis) = fold (f pos) phis
207 | aconn_fold _ f (_, phis) = fold (f NONE) phis
209 fun aconn_map pos f (ANot, [phi]) = AConn (ANot, [f (Option.map not pos) phi])
210 | aconn_map pos f (AImplies, [phi1, phi2]) =
211 AConn (AImplies, [f (Option.map not pos) phi1, f pos phi2])
212 | aconn_map pos f (AAnd, phis) = AConn (AAnd, map (f pos) phis)
213 | aconn_map pos f (AOr, phis) = AConn (AOr, map (f pos) phis)
214 | aconn_map _ f (c, phis) = AConn (c, map (f NONE) phis)
216 fun formula_fold pos f =
218 fun fld pos (AQuant (_, _, phi)) = fld pos phi
219 | fld pos (AConn conn) = aconn_fold pos fld conn
220 | fld pos (AAtom tm) = f pos tm
223 fun formula_map f (AQuant (q, xs, phi)) = AQuant (q, xs, formula_map f phi)
224 | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
225 | formula_map f (AAtom tm) = AAtom (f tm)
227 fun is_format_thf (THF0 _) = true
228 | is_format_thf _ = false
229 fun is_format_typed (TFF _) = true
230 | is_format_typed (THF0 _) = true
231 | is_format_typed _ = false
233 fun string_for_kind Axiom = "axiom"
234 | string_for_kind Definition = "definition"
235 | string_for_kind Lemma = "lemma"
236 | string_for_kind Hypothesis = "hypothesis"
237 | string_for_kind Conjecture = "conjecture"
239 fun flatten_type (ATyAbs (tys, ty)) = ATyAbs (tys, flatten_type ty)
240 | flatten_type (ty as AFun (ty1 as AType _, ty2)) =
241 (case flatten_type ty2 of
242 AFun (ty' as AType (s, tys), ty) =>
243 AFun (AType (tptp_product_type,
244 ty1 :: (if s = tptp_product_type then tys else [ty'])), ty)
246 | flatten_type (ty as AType _) = ty
248 raise Fail "unexpected higher-order type in first-order format"
250 fun str_for_type ty =
252 fun str _ (AType (s, [])) = s
253 | str _ (AType (s, tys)) =
254 tys |> map (str false)
255 |> (if s = tptp_product_type then
256 space_implode (" " ^ tptp_product_type ^ " ")
257 #> length tys > 1 ? enclose "(" ")"
259 commas #> enclose "(" ")" #> prefix s)
260 | str rhs (AFun (ty1, ty2)) =
261 str false ty1 ^ " " ^ tptp_fun_type ^ " " ^ str true ty2
262 |> not rhs ? enclose "(" ")"
263 | str _ (ATyAbs (ss, ty)) =
264 tptp_pi_binder ^ "[" ^
265 commas (map (suffix (" " ^ tptp_has_type ^ " " ^ tptp_type_of_types))
266 ss) ^ "]: " ^ str false ty
269 fun string_for_type (THF0 _) ty = str_for_type ty
270 | string_for_type (TFF _) ty = str_for_type (flatten_type ty)
271 | string_for_type _ _ = raise Fail "unexpected type in untyped format"
273 fun string_for_quantifier AForall = tptp_forall
274 | string_for_quantifier AExists = tptp_exists
276 fun string_for_connective ANot = tptp_not
277 | string_for_connective AAnd = tptp_and
278 | string_for_connective AOr = tptp_or
279 | string_for_connective AImplies = tptp_implies
280 | string_for_connective AIff = tptp_iff
282 fun string_for_bound_var format (s, ty) =
284 (if is_format_typed format then
285 " " ^ tptp_has_type ^ " " ^
286 (ty |> the_default (AType (tptp_individual_type, []))
287 |> string_for_type format)
291 fun string_for_term _ (ATerm (s, [])) = s
292 | string_for_term format (ATerm (s, ts)) =
293 if s = tptp_empty_list then
294 (* used for lists in the optional "source" field of a derivation *)
295 "[" ^ commas (map (string_for_term format) ts) ^ "]"
296 else if is_tptp_equal s then
297 space_implode (" " ^ tptp_equal ^ " ") (map (string_for_term format) ts)
298 |> is_format_thf format ? enclose "(" ")"
300 (case (s = tptp_ho_forall orelse s = tptp_ho_exists,
301 s = tptp_choice andalso format = THF0 THF_With_Choice, ts) of
302 (true, _, [AAbs ((s', ty), tm)]) =>
303 (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever
304 possible, to work around LEO-II 1.2.8 parser limitation. *)
305 string_for_formula format
306 (AQuant (if s = tptp_ho_forall then AForall else AExists,
307 [(s', SOME ty)], AAtom tm))
308 | (_, true, [AAbs ((s', ty), tm)]) =>
309 (*There is code in ATP_Translate to ensure that Eps is always applied
311 tptp_choice ^ "[" ^ s' ^ " : " ^ string_for_type format ty ^ "]: " ^
312 string_for_term format tm ^ ""
316 let val ss = map (string_for_term format) ts in
317 if is_format_thf format then
318 "(" ^ space_implode (" " ^ tptp_app ^ " ") (s :: ss) ^ ")"
320 s ^ "(" ^ commas ss ^ ")"
322 | string_for_term (format as THF0 _) (AAbs ((s, ty), tm)) =
323 "(^[" ^ s ^ " : " ^ string_for_type format ty ^ "]: " ^
324 string_for_term format tm ^ ")"
325 | string_for_term _ _ = raise Fail "unexpected term in first-order format"
326 and string_for_formula format (AQuant (q, xs, phi)) =
327 string_for_quantifier q ^
328 "[" ^ commas (map (string_for_bound_var format) xs) ^ "]: " ^
329 string_for_formula format phi
331 | string_for_formula format
332 (AConn (ANot, [AAtom (ATerm ("=" (* tptp_equal *), ts))])) =
333 space_implode (" " ^ tptp_not_infix ^ tptp_equal ^ " ")
334 (map (string_for_term format) ts)
335 |> is_format_thf format ? enclose "(" ")"
336 | string_for_formula format (AConn (c, [phi])) =
337 string_for_connective c ^ " " ^
338 (string_for_formula format phi |> is_format_thf format ? enclose "(" ")")
340 | string_for_formula format (AConn (c, phis)) =
341 space_implode (" " ^ string_for_connective c ^ " ")
342 (map (string_for_formula format) phis)
344 | string_for_formula format (AAtom tm) = string_for_term format tm
346 fun the_source (SOME source) = source
349 ATerm ("isabelle", []) :: replicate 2 (ATerm ("[]", [])))
351 fun string_for_format CNF = tptp_cnf
352 | string_for_format CNF_UEQ = tptp_cnf
353 | string_for_format FOF = tptp_fof
354 | string_for_format (TFF _) = tptp_tff
355 | string_for_format (THF0 _) = tptp_thf
357 fun string_for_problem_line format (Decl (ident, sym, ty)) =
358 string_for_format format ^ "(" ^ ident ^ ", type,\n " ^ sym ^ " : " ^
359 string_for_type format ty ^ ").\n"
360 | string_for_problem_line format (Formula (ident, kind, phi, source, info)) =
361 string_for_format format ^ "(" ^ ident ^ ", " ^ string_for_kind kind ^
362 ",\n (" ^ string_for_formula format phi ^ ")" ^
363 (case (source, info) of
365 | (SOME tm, NONE) => ", " ^ string_for_term format tm
367 ", " ^ string_for_term format (the_source source) ^
368 ", " ^ string_for_term format tm) ^ ").\n"
369 fun tptp_lines_for_atp_problem format problem =
370 "% This file was generated by Isabelle (most likely Sledgehammer)\n\
371 \% " ^ timestamp () ^ "\n" ::
372 maps (fn (_, []) => []
373 | (heading, lines) =>
374 "\n% " ^ heading ^ " (" ^ string_of_int (length lines) ^ ")\n" ::
375 map (string_for_problem_line format) lines)
379 (** CNF (Metis) and CNF UEQ (Waldmeister) **)
381 fun is_problem_line_negated (Formula (_, _, AConn (ANot, _), _, _)) = true
382 | is_problem_line_negated _ = false
384 fun is_problem_line_cnf_ueq (Formula (_, _, AAtom (ATerm ((s, _), _)), _, _)) =
386 | is_problem_line_cnf_ueq _ = false
388 fun open_conjecture_term (ATerm ((s, s'), tms)) =
389 ATerm (if is_tptp_variable s then (s |> Name.desymbolize false, s')
390 else (s, s'), tms |> map open_conjecture_term)
391 | open_conjecture_term _ = raise Fail "unexpected higher-order term"
392 fun open_formula conj =
394 (* We are conveniently assuming that all bound variable names are
395 distinct, which should be the case for the formulas we generate. *)
396 fun opn (pos as SOME true) (AQuant (AForall, _, phi)) = opn pos phi
397 | opn (pos as SOME false) (AQuant (AExists, _, phi)) = opn pos phi
398 | opn pos (AConn (ANot, [phi])) = mk_anot (opn (Option.map not pos) phi)
399 | opn pos (AConn (c, [phi1, phi2])) =
400 let val (pos1, pos2) = polarities_of_conn pos c in
401 AConn (c, [opn pos1 phi1, opn pos2 phi2])
403 | opn _ (AAtom t) = AAtom (t |> conj ? open_conjecture_term)
405 in opn (SOME (not conj)) end
406 fun open_formula_line (Formula (ident, kind, phi, source, info)) =
407 Formula (ident, kind, open_formula (kind = Conjecture) phi, source, info)
408 | open_formula_line line = line
410 fun negate_conjecture_line (Formula (ident, Conjecture, phi, source, info)) =
411 Formula (ident, Hypothesis, mk_anot phi, source, info)
412 | negate_conjecture_line line = line
414 exception CLAUSIFY of unit
416 (* This "clausification" only expands syntactic sugar, such as "phi => psi" to
417 "~ phi | psi" and "phi <=> psi" to "~ phi | psi" and "~ psi | phi". We don't
418 attempt to distribute conjunctions over disjunctions. *)
419 fun clausify_formula pos (phi as AAtom _) = [phi |> not pos ? mk_anot]
420 | clausify_formula pos (AConn (ANot, [phi])) = clausify_formula (not pos) phi
421 | clausify_formula true (AConn (AOr, [phi1, phi2])) =
422 (phi1, phi2) |> pairself (clausify_formula true)
423 |> uncurry (map_product (mk_aconn AOr))
424 | clausify_formula false (AConn (AAnd, [phi1, phi2])) =
425 (phi1, phi2) |> pairself (clausify_formula false)
426 |> uncurry (map_product (mk_aconn AOr))
427 | clausify_formula true (AConn (AImplies, [phi1, phi2])) =
428 clausify_formula true (AConn (AOr, [mk_anot phi1, phi2]))
429 | clausify_formula true (AConn (AIff, phis)) =
430 clausify_formula true (AConn (AImplies, phis)) @
431 clausify_formula true (AConn (AImplies, rev phis))
432 | clausify_formula _ _ = raise CLAUSIFY ()
434 fun clausify_formula_line (Formula (ident, kind, phi, source, info)) =
436 val (n, phis) = phi |> try (clausify_formula true) |> these |> `length
438 map2 (fn phi => fn j =>
439 Formula (ident ^ replicate_string (j - 1) "x", kind, phi, source,
443 | clausify_formula_line _ = []
445 fun ensure_cnf_problem_line line =
446 line |> open_formula_line |> negate_conjecture_line |> clausify_formula_line
448 fun ensure_cnf_problem problem =
449 problem |> map (apsnd (maps ensure_cnf_problem_line))
451 fun filter_cnf_ueq_problem problem =
453 |> map (apsnd (map open_formula_line
454 #> filter is_problem_line_cnf_ueq
455 #> map negate_conjecture_line))
458 val lines = problem |> maps snd
459 val conjs = lines |> filter is_problem_line_negated
460 in if length conjs = 1 andalso conjs <> lines then problem else [] end)
463 (** Symbol declarations **)
465 (* TFF allows implicit declarations of types, function symbols, and predicate
466 symbols (with "$i" as the type of individuals), but some provers (e.g.,
467 SNARK) require explicit declarations. The situation is similar for THF. *)
469 val atype_of_types = AType (`I tptp_type_of_types, [])
470 val bool_atype = AType (`I tptp_bool_type, [])
471 val individual_atype = AType (`I tptp_individual_type, [])
473 fun default_type pred_sym =
475 fun typ 0 = if pred_sym then bool_atype else individual_atype
476 | typ ary = AFun (individual_atype, typ (ary - 1))
479 fun add_declared_syms_in_problem_line (Decl (_, sym, _)) = insert (op =) sym
480 | add_declared_syms_in_problem_line _ = I
481 fun declared_syms_in_problem problem =
482 fold (fold add_declared_syms_in_problem_line o snd) problem []
484 fun nary_type_constr_type n =
485 funpow n (curry AFun atype_of_types) atype_of_types
487 fun undeclared_syms_in_problem declared problem =
490 if member (op =) declared name then I else AList.default (op =) (name, ty)
491 fun do_type (AType (name as (s, _), tys)) =
492 is_tptp_user_symbol s
493 ? do_sym name (fn _ => nary_type_constr_type (length tys))
495 | do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2
496 | do_type (ATyAbs (_, ty)) = do_type ty
497 fun do_term pred_sym (ATerm (name as (s, _), tms)) =
498 is_tptp_user_symbol s
499 ? do_sym name (fn _ => default_type pred_sym (length tms))
500 #> fold (do_term false) tms
501 | do_term _ (AAbs ((_, ty), tm)) = do_type ty #> do_term false tm
502 fun do_formula (AQuant (_, xs, phi)) =
503 fold do_type (map_filter snd xs) #> do_formula phi
504 | do_formula (AConn (_, phis)) = fold do_formula phis
505 | do_formula (AAtom tm) = do_term true tm
506 fun do_problem_line (Decl (_, _, ty)) = do_type ty
507 | do_problem_line (Formula (_, _, phi, _, _)) = do_formula phi
509 fold (fold do_problem_line o snd) problem []
510 |> filter_out (is_built_in_tptp_symbol o fst o fst)
513 fun declare_undeclared_syms_in_atp_problem prefix heading problem =
515 fun decl_line (x as (s, _), ty) = Decl (prefix ^ s, x, ty ())
516 val declared = problem |> declared_syms_in_problem
518 problem |> undeclared_syms_in_problem declared
519 |> sort_wrt (fst o fst)
521 in (heading, decls) :: problem end
525 fun empty_name_pool readable_names =
526 if readable_names then SOME (Symtab.empty, Symtab.empty) else NONE
528 fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs
530 pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs []
535 | skip (#"." :: cs) = skip cs
536 | skip (c :: cs) = if Char.isAlphaNum c then skip cs else c :: keep cs
538 | keep (#"." :: cs) = skip cs
539 | keep (c :: cs) = c :: keep cs
540 in String.explode #> rev #> keep #> rev #> String.implode end
542 (* Long names can slow down the ATPs. *)
543 val max_readable_name_size = 20
545 (* "equal" is reserved by some ATPs. "op" is also reserved, to avoid the
546 unreadable "op_1", "op_2", etc., in the problem files. "eq" is reserved to
547 ensure that "HOL.eq" is correctly mapped to equality (not clear whether this
548 is still necessary). *)
549 val reserved_nice_names = [tptp_old_equal, "op", "eq"]
551 fun readable_name full_name s =
552 if s = full_name then
556 |> perhaps (try (unprefix "'"))
557 |> Name.desymbolize (Char.isUpper (String.sub (full_name, 0)))
559 if size s > max_readable_name_size then
560 String.substring (s, 0, max_readable_name_size div 2 - 4) ^
561 string_of_int (hash_string full_name) ^
562 String.extract (s, size s - max_readable_name_size div 2 + 4,
566 |> (fn s => if member (op =) reserved_nice_names s then full_name else s)
568 fun nice_name (full_name, _) NONE = (full_name, NONE)
569 | nice_name (full_name, desired_name) (SOME the_pool) =
570 if is_built_in_tptp_symbol full_name then
571 (full_name, SOME the_pool)
572 else case Symtab.lookup (fst the_pool) full_name of
573 SOME nice_name => (nice_name, SOME the_pool)
576 val nice_prefix = readable_name full_name desired_name
580 nice_prefix ^ (if j = 0 then "" else string_of_int j)
582 case Symtab.lookup (snd the_pool) nice_name of
584 if full_name = full_name' then (nice_name, the_pool)
588 (Symtab.update_new (full_name, nice_name) (fst the_pool),
589 Symtab.update_new (nice_name, full_name) (snd the_pool)))
591 in add 0 |> apsnd SOME end
593 fun nice_type (AType (name, tys)) =
594 nice_name name ##>> pool_map nice_type tys #>> AType
595 | nice_type (AFun (ty1, ty2)) = nice_type ty1 ##>> nice_type ty2 #>> AFun
596 | nice_type (ATyAbs (names, ty)) =
597 pool_map nice_name names ##>> nice_type ty #>> ATyAbs
598 fun nice_term (ATerm (name, ts)) =
599 nice_name name ##>> pool_map nice_term ts #>> ATerm
600 | nice_term (AAbs ((name, ty), tm)) =
601 nice_name name ##>> nice_type ty ##>> nice_term tm #>> AAbs
602 fun nice_formula (AQuant (q, xs, phi)) =
603 pool_map nice_name (map fst xs)
604 ##>> pool_map (fn NONE => pair NONE
605 | SOME ty => nice_type ty #>> SOME) (map snd xs)
606 ##>> nice_formula phi
607 #>> (fn ((ss, ts), phi) => AQuant (q, ss ~~ ts, phi))
608 | nice_formula (AConn (c, phis)) =
609 pool_map nice_formula phis #>> curry AConn c
610 | nice_formula (AAtom tm) = nice_term tm #>> AAtom
611 fun nice_problem_line (Decl (ident, sym, ty)) =
612 nice_name sym ##>> nice_type ty #>> (fn (sym, ty) => Decl (ident, sym, ty))
613 | nice_problem_line (Formula (ident, kind, phi, source, info)) =
614 nice_formula phi #>> (fn phi => Formula (ident, kind, phi, source, info))
615 fun nice_problem problem =
616 pool_map (fn (heading, lines) =>
617 pool_map nice_problem_line lines #>> pair heading) problem
618 fun nice_atp_problem readable_names problem =
619 nice_problem problem (empty_name_pool readable_names)