253 | flatten_type _ = |
281 | flatten_type _ = |
254 raise Fail "unexpected higher-order type in first-order format" |
282 raise Fail "unexpected higher-order type in first-order format" |
255 |
283 |
256 fun str_for_type format ty = |
284 fun str_for_type format ty = |
257 let |
285 let |
258 fun str _ (AType (s, [])) = s |
286 val dfg = (format = DFG_Sorted) |
|
287 fun str _ (AType (s, [])) = |
|
288 if dfg andalso s = tptp_individual_type then "Top" else s |
259 | str _ (AType (s, tys)) = |
289 | str _ (AType (s, tys)) = |
260 let val ss = tys |> map (str false) in |
290 let val ss = tys |> map (str false) in |
261 if s = tptp_product_type then |
291 if s = tptp_product_type then |
262 ss |> space_implode (" " ^ tptp_product_type ^ " ") |
292 ss |> space_implode |
263 |> length ss > 1 ? enclose "(" ")" |
293 (if dfg then ", " else " " ^ tptp_product_type ^ " ") |
|
294 |> (not dfg andalso length ss > 1) ? enclose "(" ")" |
264 else |
295 else |
265 string_for_app format s ss |
296 tptp_string_for_app format s ss |
266 end |
297 end |
267 | str rhs (AFun (ty1, ty2)) = |
298 | str rhs (AFun (ty1, ty2)) = |
268 str false ty1 ^ " " ^ tptp_fun_type ^ " " ^ str true ty2 |
299 (str false ty1 |> dfg ? enclose "(" ")") ^ " " ^ |
|
300 (if dfg then "" else tptp_fun_type ^ " ") ^ str true ty2 |
269 |> not rhs ? enclose "(" ")" |
301 |> not rhs ? enclose "(" ")" |
270 | str _ (ATyAbs (ss, ty)) = |
302 | str _ (ATyAbs (ss, ty)) = |
271 tptp_pi_binder ^ "[" ^ |
303 tptp_pi_binder ^ "[" ^ |
272 commas (map (suffix (" " ^ tptp_has_type ^ " " ^ tptp_type_of_types)) |
304 commas (map (suffix (" " ^ tptp_has_type ^ " " ^ tptp_type_of_types)) |
273 ss) ^ "]: " ^ str false ty |
305 ss) ^ "]: " ^ str false ty |
274 in str true ty end |
306 in str true ty end |
275 |
307 |
276 fun string_for_type (format as THF _) ty = str_for_type format ty |
308 fun string_for_type (format as THF _) ty = str_for_type format ty |
277 | string_for_type (format as TFF _) ty = str_for_type format (flatten_type ty) |
309 | string_for_type format ty = str_for_type format (flatten_type ty) |
278 | string_for_type _ _ = raise Fail "unexpected type in untyped format" |
310 |
279 |
311 fun tptp_string_for_quantifier AForall = tptp_forall |
280 fun string_for_quantifier AForall = tptp_forall |
312 | tptp_string_for_quantifier AExists = tptp_exists |
281 | string_for_quantifier AExists = tptp_exists |
313 |
282 |
314 fun tptp_string_for_connective ANot = tptp_not |
283 fun string_for_connective ANot = tptp_not |
315 | tptp_string_for_connective AAnd = tptp_and |
284 | string_for_connective AAnd = tptp_and |
316 | tptp_string_for_connective AOr = tptp_or |
285 | string_for_connective AOr = tptp_or |
317 | tptp_string_for_connective AImplies = tptp_implies |
286 | string_for_connective AImplies = tptp_implies |
318 | tptp_string_for_connective AIff = tptp_iff |
287 | string_for_connective AIff = tptp_iff |
|
288 |
319 |
289 fun string_for_bound_var format (s, ty) = |
320 fun string_for_bound_var format (s, ty) = |
290 s ^ |
321 s ^ |
291 (if is_format_typed format then |
322 (if is_format_typed format then |
292 " " ^ tptp_has_type ^ " " ^ |
323 " " ^ tptp_has_type ^ " " ^ |
296 "") |
327 "") |
297 |
328 |
298 fun is_format_with_choice (THF (_, _, THF_With_Choice)) = true |
329 fun is_format_with_choice (THF (_, _, THF_With_Choice)) = true |
299 | is_format_with_choice _ = false |
330 | is_format_with_choice _ = false |
300 |
331 |
301 fun string_for_term _ (ATerm (s, [])) = s |
332 fun tptp_string_for_term _ (ATerm (s, [])) = s |
302 | string_for_term format (ATerm (s, ts)) = |
333 | tptp_string_for_term format (ATerm (s, ts)) = |
303 (if s = tptp_empty_list then |
334 (if s = tptp_empty_list then |
304 (* used for lists in the optional "source" field of a derivation *) |
335 (* used for lists in the optional "source" field of a derivation *) |
305 "[" ^ commas (map (string_for_term format) ts) ^ "]" |
336 "[" ^ commas (map (tptp_string_for_term format) ts) ^ "]" |
306 else if is_tptp_equal s then |
337 else if is_tptp_equal s then |
307 space_implode (" " ^ tptp_equal ^ " ") (map (string_for_term format) ts) |
338 space_implode (" " ^ tptp_equal ^ " ") |
|
339 (map (tptp_string_for_term format) ts) |
308 |> is_format_thf format ? enclose "(" ")" |
340 |> is_format_thf format ? enclose "(" ")" |
309 else case (s = tptp_ho_forall orelse s = tptp_ho_exists, |
341 else case (s = tptp_ho_forall orelse s = tptp_ho_exists, |
310 s = tptp_choice andalso is_format_with_choice format, ts) of |
342 s = tptp_choice andalso is_format_with_choice format, ts) of |
311 (true, _, [AAbs ((s', ty), tm)]) => |
343 (true, _, [AAbs ((s', ty), tm)]) => |
312 (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever |
344 (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever |
313 possible, to work around LEO-II 1.2.8 parser limitation. *) |
345 possible, to work around LEO-II 1.2.8 parser limitation. *) |
314 string_for_formula format |
346 tptp_string_for_formula format |
315 (AQuant (if s = tptp_ho_forall then AForall else AExists, |
347 (AQuant (if s = tptp_ho_forall then AForall else AExists, |
316 [(s', SOME ty)], AAtom tm)) |
348 [(s', SOME ty)], AAtom tm)) |
317 | (_, true, [AAbs ((s', ty), tm)]) => |
349 | (_, true, [AAbs ((s', ty), tm)]) => |
318 (* There is code in "ATP_Translate" to ensure that "Eps" is always |
350 (* There is code in "ATP_Translate" to ensure that "Eps" is always |
319 applied to an abstraction. *) |
351 applied to an abstraction. *) |
320 tptp_choice ^ "[" ^ s' ^ " : " ^ string_for_type format ty ^ "]: " ^ |
352 tptp_choice ^ "[" ^ s' ^ " : " ^ string_for_type format ty ^ "]: " ^ |
321 string_for_term format tm ^ "" |
353 tptp_string_for_term format tm ^ "" |
322 |> enclose "(" ")" |
354 |> enclose "(" ")" |
323 | _ => string_for_app format s (map (string_for_term format) ts)) |
355 | _ => tptp_string_for_app format s (map (tptp_string_for_term format) ts)) |
324 | string_for_term (format as THF _) (AAbs ((s, ty), tm)) = |
356 | tptp_string_for_term (format as THF _) (AAbs ((s, ty), tm)) = |
325 "(^[" ^ s ^ " : " ^ string_for_type format ty ^ "]: " ^ |
357 "(^[" ^ s ^ " : " ^ string_for_type format ty ^ "]: " ^ |
326 string_for_term format tm ^ ")" |
358 tptp_string_for_term format tm ^ ")" |
327 | string_for_term _ _ = raise Fail "unexpected term in first-order format" |
359 | tptp_string_for_term _ _ = |
328 and string_for_formula format (AQuant (q, xs, phi)) = |
360 raise Fail "unexpected term in first-order format" |
329 string_for_quantifier q ^ |
361 and tptp_string_for_formula format (AQuant (q, xs, phi)) = |
|
362 tptp_string_for_quantifier q ^ |
330 "[" ^ commas (map (string_for_bound_var format) xs) ^ "]: " ^ |
363 "[" ^ commas (map (string_for_bound_var format) xs) ^ "]: " ^ |
331 string_for_formula format phi |
364 tptp_string_for_formula format phi |
332 |> enclose "(" ")" |
365 |> enclose "(" ")" |
333 | string_for_formula format |
366 | tptp_string_for_formula format |
334 (AConn (ANot, [AAtom (ATerm ("=" (* tptp_equal *), ts))])) = |
367 (AConn (ANot, [AAtom (ATerm ("=" (* tptp_equal *), ts))])) = |
335 space_implode (" " ^ tptp_not_infix ^ tptp_equal ^ " ") |
368 space_implode (" " ^ tptp_not_infix ^ tptp_equal ^ " ") |
336 (map (string_for_term format) ts) |
369 (map (tptp_string_for_term format) ts) |
337 |> is_format_thf format ? enclose "(" ")" |
370 |> is_format_thf format ? enclose "(" ")" |
338 | string_for_formula format (AConn (c, [phi])) = |
371 | tptp_string_for_formula format (AConn (c, [phi])) = |
339 string_for_connective c ^ " " ^ |
372 tptp_string_for_connective c ^ " " ^ |
340 (string_for_formula format phi |> is_format_thf format ? enclose "(" ")") |
373 (tptp_string_for_formula format phi |
|
374 |> is_format_thf format ? enclose "(" ")") |
341 |> enclose "(" ")" |
375 |> enclose "(" ")" |
342 | string_for_formula format (AConn (c, phis)) = |
376 | tptp_string_for_formula format (AConn (c, phis)) = |
343 space_implode (" " ^ string_for_connective c ^ " ") |
377 space_implode (" " ^ tptp_string_for_connective c ^ " ") |
344 (map (string_for_formula format) phis) |
378 (map (tptp_string_for_formula format) phis) |
345 |> enclose "(" ")" |
379 |> enclose "(" ")" |
346 | string_for_formula format (AAtom tm) = string_for_term format tm |
380 | tptp_string_for_formula format (AAtom tm) = tptp_string_for_term format tm |
347 |
381 |
348 fun the_source (SOME source) = source |
382 fun the_source (SOME source) = source |
349 | the_source NONE = |
383 | the_source NONE = |
350 ATerm ("inference", |
384 ATerm ("inference", |
351 ATerm ("isabelle", []) :: replicate 2 (ATerm ("[]", []))) |
385 ATerm ("isabelle", []) :: replicate 2 (ATerm ("[]", []))) |
352 |
386 |
353 fun string_for_format CNF = tptp_cnf |
387 fun tptp_string_for_format CNF = tptp_cnf |
354 | string_for_format CNF_UEQ = tptp_cnf |
388 | tptp_string_for_format CNF_UEQ = tptp_cnf |
355 | string_for_format FOF = tptp_fof |
389 | tptp_string_for_format FOF = tptp_fof |
356 | string_for_format (TFF _) = tptp_tff |
390 | tptp_string_for_format (TFF _) = tptp_tff |
357 | string_for_format (THF _) = tptp_thf |
391 | tptp_string_for_format (THF _) = tptp_thf |
358 |
392 | tptp_string_for_format DFG_Sorted = raise Fail "non-TPTP format" |
359 fun string_for_problem_line format (Decl (ident, sym, ty)) = |
393 |
360 string_for_format format ^ "(" ^ ident ^ ", type,\n " ^ sym ^ " : " ^ |
394 fun tptp_string_for_problem_line format (Decl (ident, sym, ty)) = |
361 string_for_type format ty ^ ").\n" |
395 tptp_string_for_format format ^ "(" ^ ident ^ ", type,\n " ^ sym ^ |
362 | string_for_problem_line format (Formula (ident, kind, phi, source, info)) = |
396 " : " ^ string_for_type format ty ^ ").\n" |
363 string_for_format format ^ "(" ^ ident ^ ", " ^ string_for_kind kind ^ |
397 | tptp_string_for_problem_line format |
364 ",\n (" ^ string_for_formula format phi ^ ")" ^ |
398 (Formula (ident, kind, phi, source, info)) = |
|
399 tptp_string_for_format format ^ "(" ^ ident ^ ", " ^ |
|
400 tptp_string_for_kind kind ^ ",\n (" ^ |
|
401 tptp_string_for_formula format phi ^ ")" ^ |
365 (case (source, info) of |
402 (case (source, info) of |
366 (NONE, NONE) => "" |
403 (NONE, NONE) => "" |
367 | (SOME tm, NONE) => ", " ^ string_for_term format tm |
404 | (SOME tm, NONE) => ", " ^ tptp_string_for_term format tm |
368 | (_, SOME tm) => |
405 | (_, SOME tm) => |
369 ", " ^ string_for_term format (the_source source) ^ |
406 ", " ^ tptp_string_for_term format (the_source source) ^ |
370 ", " ^ string_for_term format tm) ^ ").\n" |
407 ", " ^ tptp_string_for_term format tm) ^ ").\n" |
371 fun tptp_lines_for_atp_problem format problem = |
408 |
372 "% This file was generated by Isabelle (most likely Sledgehammer)\n\ |
409 fun tptp_lines format = |
373 \% " ^ timestamp () ^ "\n" :: |
|
374 maps (fn (_, []) => [] |
410 maps (fn (_, []) => [] |
375 | (heading, lines) => |
411 | (heading, lines) => |
376 "\n% " ^ heading ^ " (" ^ string_of_int (length lines) ^ ")\n" :: |
412 "\n% " ^ heading ^ " (" ^ string_of_int (length lines) ^ ")\n" :: |
377 map (string_for_problem_line format) lines) |
413 map (tptp_string_for_problem_line format) lines) |
378 problem |
414 |
|
415 fun arity_of_type (AFun (_, ty)) = 1 + arity_of_type ty |
|
416 | arity_of_type _ = 0 |
|
417 |
|
418 fun binder_atypes (AFun (ty1, ty2)) = ty1 :: binder_atypes ty2 |
|
419 | binder_atypes _ = [] |
|
420 |
|
421 fun is_function_type (AFun (_, ty)) = is_function_type ty |
|
422 | is_function_type (AType (s, _)) = |
|
423 s <> tptp_type_of_types andalso s <> tptp_bool_type |
|
424 | is_function_type _ = false |
|
425 |
|
426 fun is_predicate_type (AFun (_, ty)) = is_predicate_type ty |
|
427 | is_predicate_type (AType (s, _)) = (s = tptp_bool_type) |
|
428 | is_predicate_type _ = false |
|
429 |
|
430 fun dfg_string_for_formula info = |
|
431 let |
|
432 fun str_for_term simp (ATerm (s, tms)) = |
|
433 (if is_tptp_equal s then "equal" |> simp ? suffix ":lr" |
|
434 else if s = tptp_true then "true" |
|
435 else if s = tptp_false then "false" |
|
436 else s) ^ |
|
437 (if null tms then "" |
|
438 else "(" ^ commas (map (str_for_term false) tms) ^ ")") |
|
439 | str_for_term _ _ = raise Fail "unexpected term in first-order format" |
|
440 fun str_for_quant AForall = "forall" |
|
441 | str_for_quant AExists = "exists" |
|
442 fun str_for_conn _ ANot = "not" |
|
443 | str_for_conn _ AAnd = "and" |
|
444 | str_for_conn _ AOr = "or" |
|
445 | str_for_conn _ AImplies = "implies" |
|
446 | str_for_conn simp AIff = "equiv" |> simp ? suffix ":lr" |
|
447 fun str_for_formula simp (AQuant (q, xs, phi)) = |
|
448 str_for_quant q ^ "(" ^ "[" ^ |
|
449 commas (map (string_for_bound_var DFG_Sorted) xs) ^ "], " ^ |
|
450 str_for_formula simp phi ^ ")" |
|
451 | str_for_formula simp (AConn (c, phis)) = |
|
452 str_for_conn simp c ^ "(" ^ |
|
453 commas (map (str_for_formula false) phis) ^ ")" |
|
454 | str_for_formula simp (AAtom tm) = str_for_term simp tm |
|
455 in str_for_formula (is_isabelle_info simpN info) end |
|
456 |
|
457 fun dfg_lines problem = |
|
458 let |
|
459 fun ary sym ty = |
|
460 "(" ^ sym ^ ", " ^ string_of_int (arity_of_type ty) ^ ")" |
|
461 fun fun_typ sym ty = |
|
462 "function(" ^ sym ^ ", " ^ string_for_type DFG_Sorted ty ^ ")." |
|
463 fun pred_typ sym ty = |
|
464 "predicate(" ^ |
|
465 commas (sym :: map (string_for_type DFG_Sorted) (binder_atypes ty)) ^ ")." |
|
466 fun formula pred (Formula (ident, kind, phi, _, info)) = |
|
467 if pred kind then |
|
468 SOME ("formula(" ^ dfg_string_for_formula info phi ^ ", " ^ ident ^ |
|
469 ").") |
|
470 else |
|
471 NONE |
|
472 | formula _ _ = NONE |
|
473 fun filt f = problem |> map (map_filter f o snd) |> flat |
|
474 val func_aries = |
|
475 filt (fn Decl (_, sym, ty) => |
|
476 if is_function_type ty then SOME (ary sym ty) else NONE |
|
477 | _ => NONE) |
|
478 |> commas |> enclose "functions [" "]." |
|
479 val pred_aries = |
|
480 filt (fn Decl (_, sym, ty) => |
|
481 if is_predicate_type ty then SOME (ary sym ty) else NONE |
|
482 | _ => NONE) |
|
483 |> commas |> enclose "predicates [" "]." |
|
484 val sorts = |
|
485 filt (fn Decl (_, sym, AType (s, [])) => |
|
486 if s = tptp_type_of_types then SOME sym else NONE |
|
487 | _ => NONE) |
|
488 |> commas |> enclose "sorts [" "]." |
|
489 val func_sigs = |
|
490 filt (fn Decl (_, sym, ty) => |
|
491 if is_function_type ty then SOME (fun_typ sym ty) else NONE |
|
492 | _ => NONE) |
|
493 val pred_sigs = |
|
494 filt (fn Decl (_, sym, ty) => |
|
495 if is_predicate_type ty then SOME (pred_typ sym ty) else NONE |
|
496 | _ => NONE) |
|
497 val axioms = filt (formula (curry (op <>) Conjecture)) |
|
498 val conjs = filt (formula (curry (op =) Conjecture)) |
|
499 fun list_of _ [] = [] |
|
500 | list_of heading ss = |
|
501 "list_of_" ^ heading ^ ".\n" :: map (suffix "\n") ss @ |
|
502 ["end_of_list.\n\n"] |
|
503 in |
|
504 "\nbegin_problem(isabelle).\n\n" :: |
|
505 list_of "descriptions" |
|
506 ["name({**}).", "author({**}).", "status(unknown).", |
|
507 "description({**})."] @ |
|
508 list_of "symbols" [func_aries, pred_aries, sorts] @ |
|
509 list_of "declarations" (func_sigs @ pred_sigs) @ |
|
510 list_of "formulae(axioms)" axioms @ |
|
511 list_of "formulae(conjectures)" conjs @ |
|
512 ["end_problem.\n"] |
|
513 end |
|
514 |
|
515 fun lines_for_atp_problem format problem = |
|
516 "% This file was generated by Isabelle (most likely Sledgehammer)\n\ |
|
517 \% " ^ timestamp () ^ "\n" :: |
|
518 (if format = DFG_Sorted then dfg_lines else tptp_lines format) problem |
379 |
519 |
380 |
520 |
381 (** CNF (Metis) and CNF UEQ (Waldmeister) **) |
521 (** CNF (Metis) and CNF UEQ (Waldmeister) **) |
382 |
522 |
383 fun is_problem_line_negated (Formula (_, _, AConn (ANot, _), _, _)) = true |
523 fun is_problem_line_negated (Formula (_, _, AConn (ANot, _), _, _)) = true |