480 annotate_types ctxt |
480 annotate_types ctxt |
481 #> with_vanilla_print_mode (Syntax.string_of_term ctxt) |
481 #> with_vanilla_print_mode (Syntax.string_of_term ctxt) |
482 #> simplify_spaces |
482 #> simplify_spaces |
483 #> maybe_quote |
483 #> maybe_quote |
484 val reconstr = Metis (type_enc, lam_trans) |
484 val reconstr = Metis (type_enc, lam_trans) |
485 fun do_metis ind (ls, ss) = |
485 fun do_metis ind options (ls, ss) = |
486 "\n" ^ do_indent (ind + 1) ^ |
486 "\n" ^ do_indent (ind + 1) ^ options ^ |
487 reconstructor_command reconstr 1 1 [] 0 |
487 reconstructor_command reconstr 1 1 [] 0 |
488 (ls |> sort_distinct (prod_ord string_ord int_ord), |
488 (ls |> sort_distinct (prod_ord string_ord int_ord), |
489 ss |> sort_distinct string_ord) |
489 ss |> sort_distinct string_ord) |
490 and do_step ind (Fix xs) = |
490 and do_step ind (Fix xs) = |
491 do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n" |
491 do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n" |
493 do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n" |
493 do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n" |
494 | do_step ind (Assume (l, t)) = |
494 | do_step ind (Assume (l, t)) = |
495 do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n" |
495 do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n" |
496 | do_step ind (Obtain (qs, xs, l, t, By_Metis facts)) = |
496 | do_step ind (Obtain (qs, xs, l, t, By_Metis facts)) = |
497 do_indent ind ^ do_obtain qs xs ^ " " ^ |
497 do_indent ind ^ do_obtain qs xs ^ " " ^ |
498 do_label l ^ do_term t ^ do_metis ind facts ^ "\n" |
498 do_label l ^ do_term t ^ |
|
499 (* The new skolemizer puts the arguments in the same order as the ATPs |
|
500 (E and Vampire -- but see also "atp_proof_reconstruct.ML" regarding |
|
501 Vampire). *) |
|
502 do_metis ind "using [[metis_new_skolem]] " facts ^ "\n" |
499 | do_step ind (Prove (qs, l, t, By_Metis facts)) = |
503 | do_step ind (Prove (qs, l, t, By_Metis facts)) = |
500 do_indent ind ^ do_have qs ^ " " ^ |
504 do_indent ind ^ do_have qs ^ " " ^ |
501 do_label l ^ do_term t ^ do_metis ind facts ^ "\n" |
505 do_label l ^ do_term t ^ do_metis ind "" facts ^ "\n" |
502 | do_step ind (Prove (qs, l, t, Case_Split (proofs, facts))) = |
506 | do_step ind (Prove (qs, l, t, Case_Split (proofs, facts))) = |
503 implode (map (prefix (do_indent ind ^ "moreover\n") o do_block ind) |
507 implode (map (prefix (do_indent ind ^ "moreover\n") o do_block ind) |
504 proofs) ^ |
508 proofs) ^ |
505 do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ |
509 do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ |
506 do_metis ind facts ^ "\n" |
510 do_metis ind "" facts ^ "\n" |
507 and do_steps prefix suffix ind steps = |
511 and do_steps prefix suffix ind steps = |
508 let val s = implode (map (do_step ind) steps) in |
512 let val s = implode (map (do_step ind) steps) in |
509 replicate_string (ind * indent_size - size prefix) " " ^ prefix ^ |
513 replicate_string (ind * indent_size - size prefix) " " ^ prefix ^ |
510 String.extract (s, ind * indent_size, |
514 String.extract (s, ind * indent_size, |
511 SOME (size s - ind * indent_size - 1)) ^ |
515 SOME (size s - ind * indent_size - 1)) ^ |