equal
deleted
inserted
replaced
503 |
503 |
504 structure Var_Set_Tab = Table( |
504 structure Var_Set_Tab = Table( |
505 type key = indexname list |
505 type key = indexname list |
506 val ord = list_ord Term_Ord.fast_indexname_ord) |
506 val ord = list_ord Term_Ord.fast_indexname_ord) |
507 |
507 |
508 (* (1) Generalize Types *) |
508 (* (1) Generalize types *) |
509 fun generalize_types ctxt t = |
509 fun generalize_types ctxt t = |
510 t |> map_types (fn _ => dummyT) |
510 t |> map_types (fn _ => dummyT) |
511 |> Syntax.check_term |
511 |> Syntax.check_term |
512 (Proof_Context.set_mode Proof_Context.mode_pattern ctxt) |
512 (Proof_Context.set_mode Proof_Context.mode_pattern ctxt) |
513 |
513 |
514 (* (2) Typing-spot Table *) |
514 (* (2) Typing-spot table *) |
515 local |
515 local |
516 fun key_of_atype (TVar (z, _)) = |
516 fun key_of_atype (TVar (z, _)) = |
517 Ord_List.insert Term_Ord.fast_indexname_ord z |
517 Ord_List.insert Term_Ord.fast_indexname_ord z |
518 | key_of_atype _ = I |
518 | key_of_atype _ = I |
519 fun key_of_type T = fold_atyps key_of_atype T [] |
519 fun key_of_type T = fold_atyps key_of_atype T [] |
533 in |
533 in |
534 val typing_spot_table = |
534 val typing_spot_table = |
535 post_fold_term_type update_tab (Var_Set_Tab.empty, 0) #> fst |
535 post_fold_term_type update_tab (Var_Set_Tab.empty, 0) #> fst |
536 end |
536 end |
537 |
537 |
538 (* (3) Reverse-Greedy *) |
538 (* (3) Reverse-greedy *) |
539 fun reverse_greedy typing_spot_tab = |
539 fun reverse_greedy typing_spot_tab = |
540 let |
540 let |
541 fun update_count z = |
541 fun update_count z = |
542 fold (fn tvar => fn tab => |
542 fold (fn tvar => fn tab => |
543 let val c = Vartab.lookup tab tvar |> the_default 0 in |
543 let val c = Vartab.lookup tab tvar |> the_default 0 in |
553 (fn kv as (k, _) => apfst (cons kv) #> apsnd (update_count 1 k)) |
553 (fn kv as (k, _) => apfst (cons kv) #> apsnd (update_count 1 k)) |
554 typing_spot_tab ([], Vartab.empty) |
554 typing_spot_tab ([], Vartab.empty) |
555 |>> sort_distinct (rev_order o cost_ord o pairself snd) |
555 |>> sort_distinct (rev_order o cost_ord o pairself snd) |
556 in fold drop_superfluous typing_spots ([], tvar_count_tab) |> fst end |
556 in fold drop_superfluous typing_spots ([], tvar_count_tab) |> fst end |
557 |
557 |
558 (* (4) Introduce Annotations *) |
558 (* (4) Introduce annotations *) |
559 fun introduce_annotations thy spots t t' = |
559 fun introduce_annotations ctxt spots t t' = |
560 let |
560 let |
|
561 val thy = Proof_Context.theory_of ctxt |
561 val get_types = post_fold_term_type (K cons) [] |
562 val get_types = post_fold_term_type (K cons) [] |
562 fun match_types tp = |
563 fun match_types tp = |
563 fold (Sign.typ_match thy) (op ~~ (pairself get_types tp)) Vartab.empty |
564 fold (Sign.typ_match thy) (op ~~ (pairself get_types tp)) Vartab.empty |
564 fun unica' b x [] = if b then [x] else [] |
565 fun unica' b x [] = if b then [x] else [] |
565 | unica' b x (y :: ys) = |
566 | unica' b x (y :: ys) = |
570 val add_all_tfree_namesT = fold_atyps (fn TFree (x, _) => cons x | _ => I) |
571 val add_all_tfree_namesT = fold_atyps (fn TFree (x, _) => cons x | _ => I) |
571 fun erase_unica_tfrees env = |
572 fun erase_unica_tfrees env = |
572 let |
573 let |
573 val unica = |
574 val unica = |
574 Vartab.fold (add_all_tfree_namesT o snd o snd) env [] |
575 Vartab.fold (add_all_tfree_namesT o snd o snd) env [] |
|
576 |> filter_out (Variable.is_declared ctxt) |
575 |> unica fast_string_ord |
577 |> unica fast_string_ord |
576 val erase_unica = map_atyps |
578 val erase_unica = map_atyps |
577 (fn T as TFree (s, _) => |
579 (fn T as TFree (s, _) => |
578 if Ord_List.member fast_string_ord unica s then dummyT else T |
580 if Ord_List.member fast_string_ord unica s then dummyT else T |
579 | T => T) |
581 | T => T) |
609 in post_traverse_term_type post2 (0, rev annots) t |> fst end |
611 in post_traverse_term_type post2 (0, rev annots) t |> fst end |
610 |
612 |
611 (* (5) Annotate *) |
613 (* (5) Annotate *) |
612 fun annotate_types ctxt t = |
614 fun annotate_types ctxt t = |
613 let |
615 let |
614 val thy = Proof_Context.theory_of ctxt |
|
615 val t' = generalize_types ctxt t |
616 val t' = generalize_types ctxt t |
616 val typing_spots = |
617 val typing_spots = |
617 t' |> typing_spot_table |
618 t' |> typing_spot_table |
618 |> reverse_greedy |
619 |> reverse_greedy |
619 |> sort int_ord |
620 |> sort int_ord |
620 in introduce_annotations thy typing_spots t t' end |
621 in introduce_annotations ctxt typing_spots t t' end |
621 |
622 |
622 val indent_size = 2 |
623 val indent_size = 2 |
623 val no_label = ("", ~1) |
624 val no_label = ("", ~1) |
624 |
625 |
625 fun string_for_proof ctxt type_enc lam_trans i n = |
626 fun string_for_proof ctxt type_enc lam_trans i n = |
815 Vector.foldl |
816 Vector.foldl |
816 ((fn (SOME t, (b, s)) => (b, Time.+ (t, s)) |
817 ((fn (SOME t, (b, s)) => (b, Time.+ (t, s)) |
817 | (NONE, (_, s)) => (true, Time.+ (preplay_timeout, s))) o apfst Lazy.force) |
818 | (NONE, (_, s)) => (true, Time.+ (preplay_timeout, s))) o apfst Lazy.force) |
818 (false, seconds 0.0) |
819 (false, seconds 0.0) |
819 |
820 |
820 (* Metis Preplaying *) |
821 (* Metis preplaying *) |
821 fun try_metis timeout (Prove (_, _, t, By_Metis fact_names)) = |
822 fun try_metis timeout (Prove (_, _, t, By_Metis fact_names)) = |
822 if not preplay then (fn () => SOME (seconds 0.0)) else |
823 if not preplay then (fn () => SOME (seconds 0.0)) else |
823 let |
824 let |
824 val facts = |
825 val facts = |
825 fact_names |
826 fact_names |