831 end |
831 end |
832 | aux subst depth nextp (step :: proof) = |
832 | aux subst depth nextp (step :: proof) = |
833 step :: aux subst depth nextp proof |
833 step :: aux subst depth nextp proof |
834 in aux [] 0 (1, 1) end |
834 in aux [] 0 (1, 1) end |
835 |
835 |
836 fun string_for_proof ctxt0 type_enc lam_trans i n = |
836 |
837 let |
837 (** Type annotations **) |
838 val ctxt = ctxt0 |
838 |
839 (* FIXME: Implement proper handling of type constraints: |
839 fun post_traverse_term_type' f _ (t as Const (_, T)) s = f t T s |
840 |> Config.put show_free_types false |
840 | post_traverse_term_type' f _ (t as Free (_, T)) s = f t T s |
841 |> Config.put show_types false |
841 | post_traverse_term_type' f _ (t as Var (_, T)) s = f t T s |
842 |> Config.put show_sorts false |
842 | post_traverse_term_type' f env (t as Bound i) s = f t (nth env i) s |
843 *) |
843 | post_traverse_term_type' f env (Abs (x, T1, b)) s = |
|
844 let |
|
845 val ((b', s'), T2) = post_traverse_term_type' f (T1 :: env) b s |
|
846 in f (Abs (x, T1, b')) (T1 --> T2) s' end |
|
847 | post_traverse_term_type' f env (u $ v) s = |
|
848 let |
|
849 val ((u', s'), Type (_, [_, T])) = post_traverse_term_type' f env u s |
|
850 val ((v', s''), _) = post_traverse_term_type' f env v s' |
|
851 in f (u' $ v') T s'' end |
|
852 |
|
853 fun post_traverse_term_type f s t = |
|
854 post_traverse_term_type' (fn t => fn T => fn s => (f t T s, T)) [] t s |> fst |
|
855 fun post_fold_term_type f s t = |
|
856 post_traverse_term_type (fn t => fn T => fn s => (t, f t T s)) s t |> snd |
|
857 |
|
858 (* Data structures, orders *) |
|
859 val cost_ord = prod_ord int_ord (prod_ord int_ord int_ord) |
|
860 |
|
861 structure Var_Set_Tab = Table( |
|
862 type key = indexname list |
|
863 val ord = list_ord Term_Ord.fast_indexname_ord) |
|
864 |
|
865 (* (1) Generalize Types *) |
|
866 fun generalize_types ctxt t = |
|
867 t |> map_types (fn _ => dummyT) |
|
868 |> Syntax.check_term |
|
869 (Proof_Context.set_mode Proof_Context.mode_pattern ctxt) |
|
870 |
|
871 (* (2) Typing-spot Table *) |
|
872 local |
|
873 fun key_of_atype (TVar (idxn, _)) = |
|
874 Ord_List.insert Term_Ord.fast_indexname_ord idxn |
|
875 | key_of_atype _ = I |
|
876 fun key_of_type T = fold_atyps key_of_atype T [] |
|
877 fun update_tab t T (tab, pos) = |
|
878 (case key_of_type T of |
|
879 [] => tab |
|
880 | key => |
|
881 let val cost = (size_of_typ T, (size_of_term t, pos)) in |
|
882 case Var_Set_Tab.lookup tab key of |
|
883 NONE => Var_Set_Tab.update_new (key, cost) tab |
|
884 | SOME old_cost => |
|
885 (case cost_ord (cost, old_cost) of |
|
886 LESS => Var_Set_Tab.update (key, cost) tab |
|
887 | _ => tab) |
|
888 end, |
|
889 pos + 1) |
|
890 in |
|
891 val typing_spot_table = |
|
892 post_fold_term_type update_tab (Var_Set_Tab.empty, 0) #> fst |
|
893 end |
|
894 |
|
895 (* (3) Reverse-Greedy *) |
|
896 fun reverse_greedy typing_spot_tab = |
|
897 let |
|
898 fun update_count z = |
|
899 fold (fn tvar => fn tab => |
|
900 let val c = Vartab.lookup tab tvar |> the_default 0 in |
|
901 Vartab.update (tvar, c + z) tab |
|
902 end) |
|
903 fun superfluous tcount = |
|
904 forall (fn tvar => the (Vartab.lookup tcount tvar) > 1) |
|
905 fun drop_superfluous (tvars, (_, (_, spot))) (spots, tcount) = |
|
906 if superfluous tcount tvars then (spots, update_count ~1 tvars tcount) |
|
907 else (spot :: spots, tcount) |
|
908 val (typing_spots, tvar_count_tab) = |
|
909 Var_Set_Tab.fold |
|
910 (fn kv as (k, _) => apfst (cons kv) #> apsnd (update_count 1 k)) |
|
911 typing_spot_tab ([], Vartab.empty) |
|
912 |>> sort_distinct (rev_order o cost_ord o pairself snd) |
|
913 in fold drop_superfluous typing_spots ([], tvar_count_tab) |> fst end |
|
914 |
|
915 (* (4) Introduce Annotations *) |
|
916 fun introduce_annotations thy spots t t' = |
|
917 let |
|
918 val get_types = post_fold_term_type (K cons) [] |
|
919 fun match_types tp = |
|
920 fold (Sign.typ_match thy) (op ~~ (pairself get_types tp)) Vartab.empty |
|
921 fun unica' b x [] = if b then [x] else [] |
|
922 | unica' b x (y :: ys) = |
|
923 if x = y then unica' false x ys |
|
924 else unica' true y ys |> b ? cons x |
|
925 fun unica ord xs = |
|
926 case sort ord xs of x :: ys => unica' true x ys | [] => [] |
|
927 val add_all_tfree_namesT = fold_atyps (fn TFree (x, _) => cons x | _ => I) |
|
928 fun erase_unica_tfrees env = |
|
929 let |
|
930 val unica = |
|
931 Vartab.fold (add_all_tfree_namesT o snd o snd) env [] |
|
932 |> unica fast_string_ord |
|
933 val erase_unica = map_atyps |
|
934 (fn T as TFree (s, _) => |
|
935 if Ord_List.member fast_string_ord unica s then dummyT else T |
|
936 | T => T) |
|
937 in Vartab.map (K (apsnd erase_unica)) env end |
|
938 val env = match_types (t', t) |> erase_unica_tfrees |
|
939 fun get_annot env (TFree _) = (false, (env, dummyT)) |
|
940 | get_annot env (T as TVar (v, S)) = |
|
941 let val T' = Envir.subst_type env T in |
|
942 if T' = dummyT then (false, (env, dummyT)) |
|
943 else (true, (Vartab.update (v, (S, dummyT)) env, T')) |
|
944 end |
|
945 | get_annot env (Type (S, Ts)) = |
|
946 (case fold_rev (fn T => fn (b, (env, Ts)) => |
|
947 let |
|
948 val (b', (env', T)) = get_annot env T |
|
949 in (b orelse b', (env', T :: Ts)) end) |
|
950 Ts (false, (env, [])) of |
|
951 (true, (env', Ts)) => (true, (env', Type (S, Ts))) |
|
952 | (false, (env', _)) => (false, (env', dummyT))) |
|
953 fun post1 _ T (env, cp, ps as p :: ps', annots) = |
|
954 if p <> cp then |
|
955 (env, cp + 1, ps, annots) |
|
956 else |
|
957 let val (_, (env', T')) = get_annot env T in |
|
958 (env', cp + 1, ps', (p, T') :: annots) |
|
959 end |
|
960 | post1 _ _ accum = accum |
|
961 val (_, _, _, annots) = post_fold_term_type post1 (env, 0, spots, []) t' |
|
962 fun post2 t _ (cp, annots as (p, T) :: annots') = |
|
963 if p <> cp then (t, (cp + 1, annots)) |
|
964 else (Type.constraint T t, (cp + 1, annots')) |
|
965 | post2 t _ x = (t, x) |
|
966 in post_traverse_term_type post2 (0, rev annots) t |> fst end |
|
967 |
|
968 (* (5) Annotate *) |
|
969 fun annotate_types ctxt t = |
|
970 let |
|
971 val thy = Proof_Context.theory_of ctxt |
|
972 val t' = generalize_types ctxt t |
|
973 val typing_spots = |
|
974 t' |> typing_spot_table |
|
975 |> reverse_greedy |
|
976 |> sort int_ord |
|
977 in introduce_annotations thy typing_spots t t' end |
|
978 |
|
979 fun string_for_proof ctxt type_enc lam_trans i n = |
|
980 let |
844 fun fix_print_mode f x = |
981 fun fix_print_mode f x = |
845 Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) |
982 Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) |
846 (print_mode_value ())) f x |
983 (print_mode_value ())) f x |
847 fun do_indent ind = replicate_string (ind * indent_size) " " |
984 fun do_indent ind = replicate_string (ind * indent_size) " " |
848 fun do_free (s, T) = |
985 fun do_free (s, T) = |