632 if member (op =) qs Show then "show" else "have") |
632 if member (op =) qs Show then "show" else "have") |
633 val do_term = |
633 val do_term = |
634 maybe_quote o fix_print_mode (Syntax.string_of_term ctxt) |
634 maybe_quote o fix_print_mode (Syntax.string_of_term ctxt) |
635 o annotate_types ctxt |
635 o annotate_types ctxt |
636 val reconstr = Metis (type_enc, lam_trans) |
636 val reconstr = Metis (type_enc, lam_trans) |
637 fun do_facts (ls, ss) = |
637 fun do_facts ind (ls, ss) = |
|
638 "\n" ^ do_indent (ind + 1) ^ |
638 reconstructor_command reconstr 1 1 [] 0 |
639 reconstructor_command reconstr 1 1 [] 0 |
639 (ls |> sort_distinct (prod_ord string_ord int_ord), |
640 (ls |> sort_distinct (prod_ord string_ord int_ord), |
640 ss |> sort_distinct string_ord) |
641 ss |> sort_distinct string_ord) |
641 and do_step ind (Fix xs) = |
642 and do_step ind (Fix xs) = |
642 do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n" |
643 do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n" |
644 do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n" |
645 do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n" |
645 | do_step ind (Assume (l, t)) = |
646 | do_step ind (Assume (l, t)) = |
646 do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n" |
647 do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n" |
647 | do_step ind (Prove (qs, l, t, By_Metis facts)) = |
648 | do_step ind (Prove (qs, l, t, By_Metis facts)) = |
648 do_indent ind ^ do_have qs ^ " " ^ |
649 do_indent ind ^ do_have qs ^ " " ^ |
649 do_label l ^ do_term t ^ " " ^ do_facts facts ^ "\n" |
650 do_label l ^ do_term t ^ do_facts ind facts ^ "\n" |
650 | do_step ind (Prove (qs, l, t, Case_Split (proofs, facts))) = |
651 | do_step ind (Prove (qs, l, t, Case_Split (proofs, facts))) = |
651 implode (map (prefix (do_indent ind ^ "moreover\n") o do_block ind) |
652 implode (map (prefix (do_indent ind ^ "moreover\n") o do_block ind) |
652 proofs) ^ |
653 proofs) ^ |
653 do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ " " ^ |
654 do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ |
654 do_facts facts ^ "\n" |
655 do_facts ind facts ^ "\n" |
655 and do_steps prefix suffix ind steps = |
656 and do_steps prefix suffix ind steps = |
656 let val s = implode (map (do_step ind) steps) in |
657 let val s = implode (map (do_step ind) steps) in |
657 replicate_string (ind * indent_size - size prefix) " " ^ prefix ^ |
658 replicate_string (ind * indent_size - size prefix) " " ^ prefix ^ |
658 String.extract (s, ind * indent_size, |
659 String.extract (s, ind * indent_size, |
659 SOME (size s - ind * indent_size - 1)) ^ |
660 SOME (size s - ind * indent_size - 1)) ^ |