29 val fact_filters : string list |
29 val fact_filters : string list |
30 val encode_str : string -> string |
30 val encode_str : string -> string |
31 val encode_strs : string list -> string |
31 val encode_strs : string list -> string |
32 val decode_str : string -> string |
32 val decode_str : string -> string |
33 val decode_strs : string -> string list |
33 val decode_strs : string -> string list |
34 val encode_unweighted_features : string list list -> string |
34 val encode_features : (string * real) list -> string |
35 val encode_features : (string list * real) list -> string |
|
36 val extract_suggestions : string -> string * string list |
35 val extract_suggestions : string -> string * string list |
37 |
36 |
38 val mash_unlearn : Proof.context -> params -> unit |
37 val mash_unlearn : Proof.context -> params -> unit |
39 val nickname_of_thm : thm -> string |
38 val nickname_of_thm : thm -> string |
40 val find_suggested_facts : Proof.context -> ('b * thm) list -> string list -> ('b * thm) list |
39 val find_suggested_facts : Proof.context -> ('b * thm) list -> string list -> ('b * thm) list |
42 val crude_thm_ord : thm * thm -> order |
41 val crude_thm_ord : thm * thm -> order |
43 val thm_less : thm * thm -> bool |
42 val thm_less : thm * thm -> bool |
44 val goal_of_thm : theory -> thm -> thm |
43 val goal_of_thm : theory -> thm -> thm |
45 val run_prover_for_mash : Proof.context -> params -> string -> string -> fact list -> thm -> |
44 val run_prover_for_mash : Proof.context -> params -> string -> string -> fact list -> thm -> |
46 prover_result |
45 prover_result |
47 val features_of : Proof.context -> theory -> int -> int Symtab.table -> stature -> bool -> |
46 val features_of : Proof.context -> theory -> int -> int Symtab.table -> stature -> term list -> |
48 term list -> (string list * real) list |
47 (string * real) list |
49 val trim_dependencies : string list -> string list option |
48 val trim_dependencies : string list -> string list option |
50 val isar_dependencies_of : string Symtab.table * string Symtab.table -> thm -> string list |
49 val isar_dependencies_of : string Symtab.table * string Symtab.table -> thm -> string list |
51 val prover_dependencies_of : Proof.context -> params -> string -> int -> raw_fact list -> |
50 val prover_dependencies_of : Proof.context -> params -> string -> int -> raw_fact list -> |
52 string Symtab.table * string Symtab.table -> thm -> bool * string list |
51 string Symtab.table * string Symtab.table -> thm -> bool * string list |
53 val attach_parents_to_facts : ('a * thm) list -> ('a * thm) list -> |
52 val attach_parents_to_facts : ('a * thm) list -> ('a * thm) list -> |
211 fun safe_str_of_real r = |
210 fun safe_str_of_real r = |
212 if r < 0.00001 then "0.00001" |
211 if r < 0.00001 then "0.00001" |
213 else if r >= 1000000.0 then "1000000" |
212 else if r >= 1000000.0 then "1000000" |
214 else Markup.print_real r |
213 else Markup.print_real r |
215 |
214 |
216 val encode_unweighted_feature = map encode_str #> space_implode "|" |
|
217 val decode_unweighted_feature = space_explode "|" #> map decode_str |
|
218 |
|
219 fun encode_feature (names, weight) = |
215 fun encode_feature (names, weight) = |
220 encode_unweighted_feature names ^ |
216 encode_str names ^ (if Real.== (weight, 1.0) then "" else "=" ^ safe_str_of_real weight) |
221 (if Real.== (weight, 1.0) then "" else "=" ^ safe_str_of_real weight) |
|
222 |
217 |
223 fun decode_feature s = |
218 fun decode_feature s = |
224 (case space_explode "=" s of |
219 (case space_explode "=" s of |
225 [feat, weight] => (decode_unweighted_feature feat, Real.fromString weight |> the_default 1.0) |
220 [feat, weight] => (decode_str feat, Real.fromString weight |> the_default 1.0) |
226 | _ => (decode_unweighted_feature s, 1.0)) |
221 | _ => (decode_str s, 1.0)) |
227 |
|
228 val encode_unweighted_features = map encode_unweighted_feature #> space_implode " " |
|
229 |
222 |
230 val encode_features = map encode_feature #> space_implode " " |
223 val encode_features = map encode_feature #> space_implode " " |
231 val decode_features = space_explode " " #> map decode_feature |
224 val decode_features = space_explode " " #> map decode_feature |
232 |
225 |
233 fun str_of_learn (name, parents, feats, deps) = |
226 fun str_of_learn (name, parents, feats, deps) = |
234 "! " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^ |
227 "! " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^ encode_strs feats ^ "; " ^ |
235 encode_unweighted_features feats ^ "; " ^ encode_strs deps ^ "\n" |
228 encode_strs deps ^ "\n" |
236 |
229 |
237 fun str_of_relearn (name, deps) = "p " ^ encode_str name ^ ": " ^ encode_strs deps ^ "\n" |
230 fun str_of_relearn (name, deps) = "p " ^ encode_str name ^ ": " ^ encode_strs deps ^ "\n" |
238 |
231 |
239 fun str_of_query max_suggs (learns, hints, parents, feats) = |
232 fun str_of_query max_suggs (learns, hints, parents, feats) = |
240 implode (map str_of_learn learns) ^ |
233 implode (map str_of_learn learns) ^ |
507 |
500 |
508 fun map_array_at ary f i = Array.update (ary, i, f (Array.sub (ary, i))) |
501 fun map_array_at ary f i = Array.update (ary, i, f (Array.sub (ary, i))) |
509 |
502 |
510 fun query ctxt engine parents access_G max_suggs hints feats = |
503 fun query ctxt engine parents access_G max_suggs hints feats = |
511 let |
504 let |
512 val str_of_feat = space_implode "|" |
|
513 |
|
514 val visible_facts = Graph.all_preds access_G parents |
505 val visible_facts = Graph.all_preds access_G parents |
515 val visible_fact_set = Symtab.make_set visible_facts |
506 val visible_fact_set = Symtab.make_set visible_facts |
516 |
507 |
517 val all_nodes = |
508 val all_nodes = |
518 (Graph.schedule (fn _ => fn (fact, (_, feats, deps)) => (fact, feats, deps)) access_G |
509 (Graph.schedule (fn _ => fn (fact, (_, feats, deps)) => (fact, feats, deps)) access_G |
526 fun add_feat (feat, weight) (xtab as (n, tab, _)) = |
517 fun add_feat (feat, weight) (xtab as (n, tab, _)) = |
527 (case Symtab.lookup tab feat of |
518 (case Symtab.lookup tab feat of |
528 SOME i => ((i, weight), xtab) |
519 SOME i => ((i, weight), xtab) |
529 | NONE => ((n, weight), add_to_xtab feat xtab)) |
520 | NONE => ((n, weight), add_to_xtab feat xtab)) |
530 |
521 |
531 val (feats', feat_xtab') = fold_map (add_feat o apfst str_of_feat) feats feat_xtab |
522 val (feats', feat_xtab') = fold_map add_feat feats feat_xtab |
532 in |
523 in |
533 (map_filter (Symtab.lookup fact_tab) deps :: rev_depss, feats' :: rev_featss, |
524 (map_filter (Symtab.lookup fact_tab) deps :: rev_depss, feats' :: rev_featss, |
534 add_to_xtab fact fact_xtab, feat_xtab') |
525 add_to_xtab fact fact_xtab, feat_xtab') |
535 end) |
526 end) |
536 all_nodes ([], [], (0, Symtab.empty, []), (0, Symtab.empty, [])) |
527 all_nodes ([], [], (0, Symtab.empty, []), (0, Symtab.empty, [])) |
545 in |
536 in |
546 trace_msg ctxt (fn () => "MaSh_SML query " ^ encode_features feats ^ " from {" ^ |
537 trace_msg ctxt (fn () => "MaSh_SML query " ^ encode_features feats ^ " from {" ^ |
547 elide_string 1000 (space_implode " " (take num_visible_facts facts)) ^ "}"); |
538 elide_string 1000 (space_implode " " (take num_visible_facts facts)) ^ "}"); |
548 (if engine = MaSh_SML_kNN then |
539 (if engine = MaSh_SML_kNN then |
549 let |
540 let |
550 val facts_ary = Array.array (num_feats, []) |
541 val facts_ary = Array.array (num_feats, []) |
551 val _ = |
542 val _ = |
552 fold (fn feats => fn fact => |
543 fold (fn feats => fn fact => |
553 let val fact' = fact - 1 in |
544 let val fact' = fact - 1 in |
554 List.app (fn (feat, weight) => map_array_at facts_ary (cons (fact', weight)) feat) |
545 List.app (fn (feat, weight) => map_array_at facts_ary (cons (fact', weight)) feat) |
555 feats; |
546 feats; |
556 fact' |
547 fact' |
557 end) |
548 end) |
558 rev_featss num_facts |
549 rev_featss num_facts |
559 val get_facts = curry Array.sub facts_ary |
550 val get_facts = curry Array.sub facts_ary |
560 val syms = map_filter (fn (feat, weight) => |
551 val syms = map_filter (fn (feat, weight) => |
561 Option.map (rpair weight) (Symtab.lookup feat_tab (str_of_feat feat))) feats |
552 Option.map (rpair weight) (Symtab.lookup feat_tab feat)) feats |
562 in |
553 in |
563 k_nearest_neighbors num_facts num_visible_facts get_deps get_facts knns max_suggs syms |
554 k_nearest_neighbors num_facts num_visible_facts get_deps get_facts knns max_suggs syms |
564 end |
555 end |
565 else |
556 else |
566 let |
557 let |
567 val unweighted_feats_ary = Vector.fromList (map (map fst) (rev rev_featss)) |
558 val unweighted_feats_ary = Vector.fromList (map (map fst) (rev rev_featss)) |
568 val get_unweighted_feats = curry Vector.sub unweighted_feats_ary |
559 val get_unweighted_feats = curry Vector.sub unweighted_feats_ary |
569 val unweighted_syms = map_filter (Symtab.lookup feat_tab o str_of_feat o fst) feats |
560 val unweighted_syms = map_filter (Symtab.lookup feat_tab o fst) feats |
570 in |
561 in |
571 naive_bayes num_facts num_visible_facts get_deps get_unweighted_feats num_feats ess prior |
562 naive_bayes num_facts num_visible_facts get_deps get_unweighted_feats num_feats ess prior |
572 max_suggs unweighted_syms |
563 max_suggs unweighted_syms |
573 end) |
564 end) |
574 |> map (curry Vector.sub fact_vec o fst) |
565 |> map (curry Vector.sub fact_vec o fst) |
618 string_of_int (length (Graph.keys G)) ^ " node(s), " ^ |
609 string_of_int (length (Graph.keys G)) ^ " node(s), " ^ |
619 string_of_int (fold (Integer.add o length o snd) (Graph.dest G) 0) ^ " edge(s), " ^ |
610 string_of_int (fold (Integer.add o length o snd) (Graph.dest G) 0) ^ " edge(s), " ^ |
620 string_of_int (length (Graph.maximals G)) ^ " maximal" |
611 string_of_int (length (Graph.maximals G)) ^ " maximal" |
621 |
612 |
622 type mash_state = |
613 type mash_state = |
623 {access_G : (proof_kind * (string list * real) list * string list) Graph.T, |
614 {access_G : (proof_kind * (string * real) list * string list) Graph.T, |
624 num_known_facts : int, |
615 num_known_facts : int, |
625 dirty : string list option} |
616 dirty : string list option} |
626 |
617 |
627 val empty_state = {access_G = Graph.empty, num_known_facts = 0, dirty = SOME []} : mash_state |
618 val empty_state = {access_G = Graph.empty, num_known_facts = 0, dirty = SOME []} : mash_state |
628 |
619 |
782 |> map (`weight_of) |> sort (int_ord o swap o pairself fst) |
773 |> map (`weight_of) |> sort (int_ord o swap o pairself fst) |
783 |> map snd |> take max_facts |
774 |> map snd |> take max_facts |
784 end |
775 end |
785 |
776 |
786 val default_weight = 1.0 |
777 val default_weight = 1.0 |
787 fun free_feature_of s = (["f" ^ s], 40.0 (* FUDGE *)) |
778 fun free_feature_of s = ("f" ^ s, 40.0 (* FUDGE *)) |
788 fun thy_feature_of s = (["y" ^ s], 8.0 (* FUDGE *)) |
779 fun thy_feature_of s = ("y" ^ s, 8.0 (* FUDGE *)) |
789 fun type_feature_of s = (["t" ^ s], 4.0 (* FUDGE *)) |
780 fun type_feature_of s = ("t" ^ s, 4.0 (* FUDGE *)) |
790 fun var_feature_of s = ([s], 1.0 (* FUDGE *)) |
781 fun class_feature_of s = ("s" ^ s, 1.0 (* FUDGE *)) |
791 fun class_feature_of s = (["s" ^ s], 1.0 (* FUDGE *)) |
782 val local_feature = ("local", 16.0 (* FUDGE *)) |
792 val local_feature = (["local"], 16.0 (* FUDGE *)) |
|
793 |
783 |
794 fun crude_theory_ord p = |
784 fun crude_theory_ord p = |
795 if Theory.subthy p then |
785 if Theory.subthy p then |
796 if Theory.eq_thy p then EQUAL else LESS |
786 if Theory.eq_thy p then EQUAL else LESS |
797 else if Theory.subthy (swap p) then |
787 else if Theory.subthy (swap p) then |
841 |
831 |
842 val pat_tvar_prefix = "_" |
832 val pat_tvar_prefix = "_" |
843 val pat_var_prefix = "_" |
833 val pat_var_prefix = "_" |
844 |
834 |
845 (* try "Long_Name.base_name" for shorter names *) |
835 (* try "Long_Name.base_name" for shorter names *) |
846 fun massage_long_name s = if s = @{class type} then "T" else s |
836 fun massage_long_name s = s |
847 |
837 |
848 val crude_str_of_sort = space_implode ":" o map massage_long_name o subtract (op =) @{sort type} |
838 val crude_str_of_sort = space_implode ":" o map massage_long_name o subtract (op =) @{sort type} |
849 |
839 |
850 fun crude_str_of_typ (Type (s, [])) = massage_long_name s |
840 fun crude_str_of_typ (Type (s, [])) = massage_long_name s |
851 | crude_str_of_typ (Type (s, Ts)) = massage_long_name s ^ implode (map crude_str_of_typ Ts) |
841 | crude_str_of_typ (Type (s, Ts)) = massage_long_name s ^ implode (map crude_str_of_typ Ts) |
855 fun maybe_singleton_str _ "" = [] |
845 fun maybe_singleton_str _ "" = [] |
856 | maybe_singleton_str pref s = [pref ^ s] |
846 | maybe_singleton_str pref s = [pref ^ s] |
857 |
847 |
858 val max_pat_breadth = 10 (* FUDGE *) |
848 val max_pat_breadth = 10 (* FUDGE *) |
859 |
849 |
860 fun keep m xs = |
850 fun term_features_of ctxt thy_name num_facts const_tab term_max_depth type_max_depth ts = |
861 let val n = length xs in |
|
862 if n <= m then xs else take (m div 2) xs @ drop (n - (m + 1) div 2) xs |
|
863 end |
|
864 |
|
865 fun sort_of_type alg T = |
|
866 let |
|
867 val G = Sorts.classes_of alg |
|
868 |
|
869 fun cls_of S [] = S |
|
870 | cls_of S (cl :: cls) = |
|
871 if Sorts.of_sort alg (T, [cl]) then |
|
872 cls_of (insert (op =) cl S) cls |
|
873 else |
|
874 let val cls' = Sorts.minimize_sort alg (Sorts.super_classes alg cl) in |
|
875 cls_of S (union (op =) cls' cls) |
|
876 end |
|
877 in |
|
878 cls_of [] (Graph.maximals G) |
|
879 end |
|
880 |
|
881 val generalize_goal = false |
|
882 |
|
883 fun term_features_of ctxt thy_name num_facts const_tab term_max_depth type_max_depth in_goal ts = |
|
884 let |
851 let |
885 val thy = Proof_Context.theory_of ctxt |
852 val thy = Proof_Context.theory_of ctxt |
886 val alg = Sign.classes_of thy |
|
887 |
853 |
888 val fixes = map snd (Variable.dest_fixes ctxt) |
854 val fixes = map snd (Variable.dest_fixes ctxt) |
889 val classes = Sign.classes_of thy |
855 val classes = Sign.classes_of thy |
890 |
856 |
891 fun add_classes @{sort type} = I |
857 fun add_classes @{sort type} = I |
900 | pattify_type _ (Type (s, [])) = |
866 | pattify_type _ (Type (s, [])) = |
901 if member (op =) bad_types s then [] else [massage_long_name s] |
867 if member (op =) bad_types s then [] else [massage_long_name s] |
902 | pattify_type depth (Type (s, U :: Ts)) = |
868 | pattify_type depth (Type (s, U :: Ts)) = |
903 let |
869 let |
904 val T = Type (s, Ts) |
870 val T = Type (s, Ts) |
905 val ps = keep max_pat_breadth (pattify_type depth T) |
871 val ps = take max_pat_breadth (pattify_type depth T) |
906 val qs = keep max_pat_breadth ("" :: pattify_type (depth - 1) U) |
872 val qs = take max_pat_breadth ("" :: pattify_type (depth - 1) U) |
907 in |
873 in |
908 map_product (fn p => fn "" => p | q => p ^ "(" ^ q ^ ")") ps qs |
874 map_product (fn p => fn "" => p | q => p ^ "(" ^ q ^ ")") ps qs |
909 end |
875 end |
910 | pattify_type _ (TFree (_, S)) = |
876 | pattify_type _ (TFree (_, S)) = |
911 maybe_singleton_str pat_tvar_prefix (crude_str_of_sort S) |
877 maybe_singleton_str pat_tvar_prefix (crude_str_of_sort S) |
933 else |
899 else |
934 let val count = Symtab.lookup const_tab s |> the_default 1 in |
900 let val count = Symtab.lookup const_tab s |> the_default 1 in |
935 Real.fromInt num_facts / Real.fromInt count (* FUDGE *) |
901 Real.fromInt num_facts / Real.fromInt count (* FUDGE *) |
936 end) |
902 end) |
937 |
903 |
938 fun pattify_term _ 0 _ = ([] : (string list * real) list) |
904 fun pattify_term _ 0 _ = [] |
939 | pattify_term _ _ (Const (x as (s, _))) = |
905 | pattify_term _ _ (Const (s, _)) = |
940 if is_widely_irrelevant_const s then |
906 if is_widely_irrelevant_const s then [] else [(massage_long_name s, weight_of_const s)] |
941 [] |
|
942 else |
|
943 let |
|
944 val strs_of_sort = |
|
945 (if generalize_goal andalso in_goal then Sorts.complete_sort alg |
|
946 else single o hd) |
|
947 #> map massage_long_name |
|
948 fun strs_of_type_arg (T as Type (s, _)) = |
|
949 massage_long_name s :: |
|
950 (if generalize_goal andalso in_goal then strs_of_sort (sort_of_type alg T) else []) |
|
951 | strs_of_type_arg (TFree (_, S)) = strs_of_sort S |
|
952 | strs_of_type_arg (TVar (_, S)) = strs_of_sort S |
|
953 |
|
954 val typargss = |
|
955 these (try (Sign.const_typargs thy) x) |
|
956 |> map strs_of_type_arg |
|
957 |> n_fold_cartesian_product |
|
958 |> keep max_pat_breadth |
|
959 val s' = massage_long_name s |
|
960 val w = weight_of_const s |
|
961 |
|
962 fun str_of_type_args [] = "" |
|
963 | str_of_type_args ss = "(" ^ space_implode "," ss ^ ")" |
|
964 in |
|
965 [(map (curry (op ^) s' o str_of_type_args) typargss, w)] |
|
966 end |
|
967 | pattify_term _ _ (Free (s, T)) = |
907 | pattify_term _ _ (Free (s, T)) = |
968 maybe_singleton_str pat_var_prefix (crude_str_of_typ T) |
908 maybe_singleton_str pat_var_prefix (crude_str_of_typ T) |
969 |> map var_feature_of |
909 |> map (rpair 1.0) |
970 |> (if member (op =) fixes s then |
910 |> (if member (op =) fixes s then |
971 cons (free_feature_of (massage_long_name (thy_name ^ Long_Name.separator ^ s))) |
911 cons (free_feature_of (massage_long_name |
|
912 (thy_name ^ Long_Name.separator ^ s))) |
972 else |
913 else |
973 I) |
914 I) |
974 | pattify_term _ _ (Var (_, T)) = |
915 | pattify_term _ _ (Var (_, T)) = |
975 maybe_singleton_str pat_var_prefix (crude_str_of_typ T) |
916 maybe_singleton_str pat_var_prefix (crude_str_of_typ T) |> map (rpair default_weight) |
976 |> map var_feature_of |
|
977 | pattify_term Ts _ (Bound j) = |
917 | pattify_term Ts _ (Bound j) = |
978 maybe_singleton_str pat_var_prefix (crude_str_of_typ (nth Ts j)) |
918 maybe_singleton_str pat_var_prefix (crude_str_of_typ (nth Ts j)) |
979 |> map var_feature_of |
919 |> map (rpair default_weight) |
980 | pattify_term Ts depth (t $ u) = |
920 | pattify_term Ts depth (t $ u) = |
981 let |
921 let |
982 val ps = keep max_pat_breadth (pattify_term Ts depth t) |
922 val ps = take max_pat_breadth (pattify_term Ts depth t) |
983 val qs = keep max_pat_breadth (([], default_weight) :: pattify_term Ts (depth - 1) u) |
923 val qs = take max_pat_breadth (("", default_weight) :: pattify_term Ts (depth - 1) u) |
984 in |
924 in |
985 map_product (fn ppw as (p :: _, pw) => |
925 map_product (fn ppw as (p, pw) => |
986 fn ([], _) => ppw |
926 fn ("", _) => ppw |
987 | (q :: _, qw) => ([p ^ "(" ^ q ^ ")"], pw + qw)) ps qs |
927 | (q, qw) => (p ^ "(" ^ q ^ ")", pw + qw)) ps qs |
988 end |
928 end |
989 | pattify_term _ _ _ = [] |
929 | pattify_term _ _ _ = [] |
990 |
930 |
991 fun add_term_pat Ts = union (eq_fst (op =)) oo pattify_term Ts |
931 fun add_term_pat Ts = union (eq_fst (op =)) oo pattify_term Ts |
992 |
932 |
993 fun add_term_pats _ 0 _ = I |
933 fun add_term_pats _ 0 _ = I |
994 | add_term_pats Ts depth t = |
934 | add_term_pats Ts depth t = add_term_pat Ts depth t #> add_term_pats Ts (depth - 1) t |
995 add_term_pat Ts depth t #> add_term_pats Ts (depth - 1) t |
|
996 |
935 |
997 fun add_term Ts = add_term_pats Ts term_max_depth |
936 fun add_term Ts = add_term_pats Ts term_max_depth |
998 |
937 |
999 fun add_subterms Ts t = |
938 fun add_subterms Ts t = |
1000 (case strip_comb t of |
939 (case strip_comb t of |
1015 |
954 |
1016 val term_max_depth = 2 |
955 val term_max_depth = 2 |
1017 val type_max_depth = 1 |
956 val type_max_depth = 1 |
1018 |
957 |
1019 (* TODO: Generate type classes for types? *) |
958 (* TODO: Generate type classes for types? *) |
1020 fun features_of ctxt thy num_facts const_tab (scope, _) in_goal ts = |
959 fun features_of ctxt thy num_facts const_tab (scope, _) ts = |
1021 let val thy_name = Context.theory_name thy in |
960 let val thy_name = Context.theory_name thy in |
1022 thy_feature_of thy_name :: |
961 thy_feature_of thy_name :: |
1023 term_features_of ctxt thy_name num_facts const_tab term_max_depth type_max_depth in_goal ts |
962 term_features_of ctxt thy_name num_facts const_tab term_max_depth type_max_depth ts |
1024 |> scope <> Global ? cons local_feature |
963 |> scope <> Global ? cons local_feature |
1025 end |
964 end |
1026 |
965 |
1027 (* Too many dependencies is a sign that a decision procedure is at work. There is not much to learn |
966 (* Too many dependencies is a sign that a decision procedure is at work. There is not much to learn |
1028 from such proofs. *) |
967 from such proofs. *) |
1266 fun fact_has_right_theory (_, th) = |
1205 fun fact_has_right_theory (_, th) = |
1267 thy_name = Context.theory_name (theory_of_thm th) |
1206 thy_name = Context.theory_name (theory_of_thm th) |
1268 |
1207 |
1269 fun chained_or_extra_features_of factor (((_, stature), th), weight) = |
1208 fun chained_or_extra_features_of factor (((_, stature), th), weight) = |
1270 [prop_of th] |
1209 [prop_of th] |
1271 |> features_of ctxt (theory_of_thm th) num_facts const_tab stature false |
1210 |> features_of ctxt (theory_of_thm th) num_facts const_tab stature |
1272 |> map (apsnd (fn r => weight * factor * r)) |
1211 |> map (apsnd (fn r => weight * factor * r)) |
1273 |
1212 |
1274 fun query_args access_G = |
1213 fun query_args access_G = |
1275 let |
1214 let |
1276 val parents = maximal_wrt_access_graph access_G facts |
1215 val parents = maximal_wrt_access_graph access_G facts |
1277 val hints = chained |
1216 val hints = chained |
1278 |> filter (is_fact_in_graph access_G o snd) |
1217 |> filter (is_fact_in_graph access_G o snd) |
1279 |> map (nickname_of_thm o snd) |
1218 |> map (nickname_of_thm o snd) |
1280 |
1219 |
1281 val goal_feats = |
1220 val goal_feats = |
1282 features_of ctxt thy num_facts const_tab (Local, General) true (concl_t :: hyp_ts) |
1221 features_of ctxt thy num_facts const_tab (Local, General) (concl_t :: hyp_ts) |
1283 val chained_feats = chained |
1222 val chained_feats = chained |
1284 |> map (rpair 1.0) |
1223 |> map (rpair 1.0) |
1285 |> map (chained_or_extra_features_of chained_feature_factor) |
1224 |> map (chained_or_extra_features_of chained_feature_factor) |
1286 |> rpair [] |-> fold (union (eq_fst (op =))) |
1225 |> rpair [] |-> fold (union (eq_fst (op =))) |
1287 val extra_feats = |
1226 val extra_feats = |
1373 fun mash_learn_proof ctxt ({overlord, timeout, ...} : params) t facts used_ths = |
1312 fun mash_learn_proof ctxt ({overlord, timeout, ...} : params) t facts used_ths = |
1374 if is_mash_enabled () then |
1313 if is_mash_enabled () then |
1375 launch_thread timeout (fn () => |
1314 launch_thread timeout (fn () => |
1376 let |
1315 let |
1377 val thy = Proof_Context.theory_of ctxt |
1316 val thy = Proof_Context.theory_of ctxt |
1378 val feats = features_of ctxt thy 0 Symtab.empty (Local, General) false [t] |
1317 val feats = features_of ctxt thy 0 Symtab.empty (Local, General) [t] |
1379 in |
1318 in |
1380 map_state ctxt overlord (fn state as {access_G, num_known_facts, dirty} => |
1319 map_state ctxt overlord (fn state as {access_G, num_known_facts, dirty} => |
1381 let |
1320 let |
1382 val name = learned_proof_name () |
1321 val name = learned_proof_name () |
1383 val parents = maximal_wrt_access_graph access_G facts |
1322 val parents = maximal_wrt_access_graph access_G facts |
1475 fun learn_new_fact _ (accum as (_, (_, _, true))) = accum |
1414 fun learn_new_fact _ (accum as (_, (_, _, true))) = accum |
1476 | learn_new_fact (parents, ((_, stature as (_, status)), th)) |
1415 | learn_new_fact (parents, ((_, stature as (_, status)), th)) |
1477 (learns, (n, next_commit, _)) = |
1416 (learns, (n, next_commit, _)) = |
1478 let |
1417 let |
1479 val name = nickname_of_thm th |
1418 val name = nickname_of_thm th |
1480 val feats = |
1419 val feats = features_of ctxt (theory_of_thm th) 0 Symtab.empty stature [prop_of th] |
1481 features_of ctxt (theory_of_thm th) 0 Symtab.empty stature false [prop_of th] |
|
1482 val deps = deps_of status th |> these |
1420 val deps = deps_of status th |> these |
1483 val n = n |> not (null deps) ? Integer.add 1 |
1421 val n = n |> not (null deps) ? Integer.add 1 |
1484 val learns = (name, parents, feats, deps) :: learns |
1422 val learns = (name, parents, feats, deps) :: learns |
1485 val (learns, next_commit) = |
1423 val (learns, next_commit) = |
1486 if Time.> (Timer.checkRealTimer timer, next_commit) then |
1424 if Time.> (Timer.checkRealTimer timer, next_commit) then |