35 val extract_suggestions : string -> string * string list |
35 val extract_suggestions : string -> string * string list |
36 |
36 |
37 structure MaSh: |
37 structure MaSh: |
38 sig |
38 sig |
39 val unlearn : Proof.context -> bool -> unit |
39 val unlearn : Proof.context -> bool -> unit |
40 val learn : |
40 val learn : Proof.context -> bool -> bool -> |
41 Proof.context -> bool -> bool |
41 (string * string list * string list list * string list) list -> unit |
42 -> (string * string list * string list list * string list) list -> unit |
42 val relearn : Proof.context -> bool -> bool -> (string * string list) list -> unit |
43 val relearn : |
43 val query : Proof.context -> bool -> int -> |
44 Proof.context -> bool -> bool -> (string * string list) list -> unit |
44 (string * string list * string list list * string list) list * string list * string list * |
45 val query : |
45 (string list * real) list -> |
46 Proof.context -> bool -> int |
46 string list |
47 -> (string * string list * string list list * string list) list |
|
48 * string list * string list * (string list * real) list |
|
49 -> string list |
|
50 end |
47 end |
51 |
48 |
52 val mash_unlearn : Proof.context -> params -> unit |
49 val mash_unlearn : Proof.context -> params -> unit |
53 val is_mash_enabled : unit -> bool |
50 val is_mash_enabled : unit -> bool |
54 val nickname_of_thm : thm -> string |
51 val nickname_of_thm : thm -> string |
55 val find_suggested_facts : |
52 val find_suggested_facts : Proof.context -> ('b * thm) list -> string list -> ('b * thm) list |
56 Proof.context -> ('b * thm) list -> string list -> ('b * thm) list |
53 val mesh_facts : ('a * 'a -> bool) -> int -> (real * (('a * real) list * 'a list)) list -> 'a list |
57 val mesh_facts : |
|
58 ('a * 'a -> bool) -> int -> (real * (('a * real) list * 'a list)) list |
|
59 -> 'a list |
|
60 val crude_thm_ord : thm * thm -> order |
54 val crude_thm_ord : thm * thm -> order |
61 val thm_less : thm * thm -> bool |
55 val thm_less : thm * thm -> bool |
62 val goal_of_thm : theory -> thm -> thm |
56 val goal_of_thm : theory -> thm -> thm |
63 val run_prover_for_mash : |
57 val run_prover_for_mash : Proof.context -> params -> string -> string -> fact list -> thm -> |
64 Proof.context -> params -> string -> string -> fact list -> thm -> prover_result |
58 prover_result |
65 val features_of : |
59 val features_of : Proof.context -> theory -> int -> int Symtab.table -> stature -> bool -> |
66 Proof.context -> theory -> int -> int Symtab.table -> stature -> bool -> term list -> |
60 term list -> (string list * real) list |
67 (string list * real) list |
|
68 val trim_dependencies : string list -> string list option |
61 val trim_dependencies : string list -> string list option |
69 val isar_dependencies_of : |
62 val isar_dependencies_of : string Symtab.table * string Symtab.table -> thm -> string list |
70 string Symtab.table * string Symtab.table -> thm -> string list |
63 val prover_dependencies_of : Proof.context -> params -> string -> int -> raw_fact list -> |
71 val prover_dependencies_of : |
64 string Symtab.table * string Symtab.table -> thm -> bool * string list |
72 Proof.context -> params -> string -> int -> raw_fact list |
65 val attach_parents_to_facts : ('a * thm) list -> ('a * thm) list -> |
73 -> string Symtab.table * string Symtab.table -> thm |
66 (string list * ('a * thm)) list |
74 -> bool * string list |
|
75 val attach_parents_to_facts : |
|
76 ('a * thm) list -> ('a * thm) list -> (string list * ('a * thm)) list |
|
77 val num_extra_feature_facts : int |
67 val num_extra_feature_facts : int |
78 val extra_feature_factor : real |
68 val extra_feature_factor : real |
79 val weight_facts_smoothly : 'a list -> ('a * real) list |
69 val weight_facts_smoothly : 'a list -> ('a * real) list |
80 val weight_facts_steeply : 'a list -> ('a * real) list |
70 val weight_facts_steeply : 'a list -> ('a * real) list |
81 val find_mash_suggestions : |
71 val find_mash_suggestions : Proof.context -> int -> string list -> ('b * thm) list -> |
82 Proof.context -> int -> string list -> ('b * thm) list -> ('b * thm) list |
72 ('b * thm) list -> ('b * thm) list -> ('b * thm) list * ('b * thm) list |
83 -> ('b * thm) list -> ('b * thm) list * ('b * thm) list |
|
84 val add_const_counts : term -> int Symtab.table -> int Symtab.table |
73 val add_const_counts : term -> int Symtab.table -> int Symtab.table |
85 val mash_suggested_facts : |
74 val mash_suggested_facts : Proof.context -> params -> int -> term list -> term -> raw_fact list -> |
86 Proof.context -> params -> int -> term list -> term -> raw_fact list -> fact list * fact list |
75 fact list * fact list |
87 val mash_learn_proof : Proof.context -> params -> term -> ('a * thm) list -> thm list -> unit |
76 val mash_learn_proof : Proof.context -> params -> term -> ('a * thm) list -> thm list -> unit |
88 val mash_learn : |
77 val mash_learn : Proof.context -> params -> fact_override -> thm list -> bool -> unit |
89 Proof.context -> params -> fact_override -> thm list -> bool -> unit |
|
90 |
78 |
91 val mash_can_suggest_facts : Proof.context -> bool -> bool |
79 val mash_can_suggest_facts : Proof.context -> bool -> bool |
92 val generous_max_facts : int -> int |
80 val generous_max_facts : int -> int |
93 val mepo_weight : real |
81 val mepo_weight : real |
94 val mash_weight : real |
82 val mash_weight : real |
95 val relevant_facts : |
83 val relevant_facts : Proof.context -> params -> string -> int -> fact_override -> term list -> |
96 Proof.context -> params -> string -> int -> fact_override -> term list |
84 term -> raw_fact list -> (string * fact list) list |
97 -> term -> raw_fact list -> (string * fact list) list |
|
98 val kill_learners : Proof.context -> params -> unit |
85 val kill_learners : Proof.context -> params -> unit |
99 val running_learners : unit -> unit |
86 val running_learners : unit -> unit |
100 end; |
87 end; |
101 |
88 |
102 structure Sledgehammer_MaSh : SLEDGEHAMMER_MASH = |
89 structure Sledgehammer_MaSh : SLEDGEHAMMER_MASH = |
264 |
251 |
265 fun unlearn ctxt overlord = |
252 fun unlearn ctxt overlord = |
266 let val path = mash_model_dir () in |
253 let val path = mash_model_dir () in |
267 trace_msg ctxt (K "MaSh unlearn"); |
254 trace_msg ctxt (K "MaSh unlearn"); |
268 shutdown ctxt overlord; |
255 shutdown ctxt overlord; |
269 try (File.fold_dir (fn file => fn _ => |
256 try (File.fold_dir (fn file => fn _ => try File.rm (Path.append path (Path.basic file))) path) |
270 try File.rm (Path.append path (Path.basic file))) |
257 NONE; |
271 path) NONE; |
|
272 () |
258 () |
273 end |
259 end |
274 |
260 |
275 fun learn _ _ _ [] = () |
261 fun learn _ _ _ [] = () |
276 | learn ctxt overlord save (learns : (string * string list * string list list * string list) list) (*##*) |
262 | learn ctxt overlord save learns = |
277 = |
|
278 let val names = elide_string 1000 (space_implode " " (map #1 learns)) in |
263 let val names = elide_string 1000 (space_implode " " (map #1 learns)) in |
279 (trace_msg ctxt (fn () => "MaSh learn" ^ (if names = "" then "" else " " ^ names)); |
264 (trace_msg ctxt (fn () => "MaSh learn" ^ (if names = "" then "" else " " ^ names)); |
280 run_mash_tool ctxt overlord ([] |> save ? cons save_models_arg) false |
265 run_mash_tool ctxt overlord ([] |> save ? cons save_models_arg) false (learns, str_of_learn) |
281 (learns, str_of_learn) (K ())) |
266 (K ())) |
282 end |
267 end |
283 |
268 |
284 fun relearn _ _ _ [] = () |
269 fun relearn _ _ _ [] = () |
285 | relearn ctxt overlord save relearns = |
270 | relearn ctxt overlord save relearns = |
286 (trace_msg ctxt (fn () => "MaSh relearn " ^ |
271 (trace_msg ctxt (fn () => "MaSh relearn " ^ |
287 elide_string 1000 (space_implode " " (map #1 relearns))); |
272 elide_string 1000 (space_implode " " (map #1 relearns))); |
288 run_mash_tool ctxt overlord ([] |> save ? cons save_models_arg) false |
273 run_mash_tool ctxt overlord ([] |> save ? cons save_models_arg) false |
289 (relearns, str_of_relearn) (K ())) |
274 (relearns, str_of_relearn) (K ())) |
290 |
275 |
291 fun query ctxt overlord max_suggs (query as (_, _, _, feats)) = |
276 fun query ctxt overlord max_suggs (query as (_, _, _, feats)) = |
292 (trace_msg ctxt (fn () => "MaSh query " ^ encode_features feats); |
277 (trace_msg ctxt (fn () => "MaSh query " ^ encode_features feats); |
293 run_mash_tool ctxt overlord [] false ([query], str_of_query max_suggs) (fn suggs => |
278 run_mash_tool ctxt overlord [] false ([query], str_of_query max_suggs) (fn suggs => |
294 (case suggs () of |
279 (case suggs () of |
464 let |
447 let |
465 fun add (fact as (_, th)) = Symtab.default (nickname_of_thm th, fact) |
448 fun add (fact as (_, th)) = Symtab.default (nickname_of_thm th, fact) |
466 val tab = fold add facts Symtab.empty |
449 val tab = fold add facts Symtab.empty |
467 fun lookup nick = |
450 fun lookup nick = |
468 Symtab.lookup tab nick |
451 Symtab.lookup tab nick |
469 |> tap (fn NONE => trace_msg ctxt (fn () => "Cannot find " ^ quote nick) |
452 |> tap (fn NONE => trace_msg ctxt (fn () => "Cannot find " ^ quote nick) | _ => ()) |
470 | _ => ()) |
|
471 in map_filter lookup end |
453 in map_filter lookup end |
472 |
454 |
473 fun scaled_avg [] = 0 |
455 fun scaled_avg [] = 0 |
474 | scaled_avg xs = |
456 | scaled_avg xs = Real.ceil (100000000.0 * fold (curry (op +)) xs 0.0) div length xs |
475 Real.ceil (100000000.0 * fold (curry (op +)) xs 0.0) div length xs |
|
476 |
457 |
477 fun avg [] = 0.0 |
458 fun avg [] = 0.0 |
478 | avg xs = fold (curry (op +)) xs 0.0 / Real.fromInt (length xs) |
459 | avg xs = fold (curry (op +)) xs 0.0 / Real.fromInt (length xs) |
479 |
460 |
480 fun normalize_scores _ [] = [] |
461 fun normalize_scores _ [] = [] |
481 | normalize_scores max_facts xs = |
462 | normalize_scores max_facts xs = |
482 let val avg = avg (map snd (take max_facts xs)) in |
463 map (apsnd (curry Real.* (1.0 / avg (map snd (take max_facts xs))))) xs |
483 map (apsnd (curry Real.* (1.0 / avg))) xs |
|
484 end |
|
485 |
464 |
486 fun mesh_facts _ max_facts [(_, (sels, unks))] = |
465 fun mesh_facts _ max_facts [(_, (sels, unks))] = |
487 map fst (take max_facts sels) @ take (max_facts - length sels) unks |
466 map fst (take max_facts sels) @ take (max_facts - length sels) unks |
488 | mesh_facts fact_eq max_facts mess = |
467 | mesh_facts fact_eq max_facts mess = |
489 let |
468 let |
490 val mess = mess |> map (apsnd (apfst (normalize_scores max_facts))) |
469 val mess = mess |> map (apsnd (apfst (normalize_scores max_facts))) |
|
470 |
491 fun score_in fact (global_weight, (sels, unks)) = |
471 fun score_in fact (global_weight, (sels, unks)) = |
492 let |
472 let val score_at = try (nth sels) #> Option.map (fn (_, score) => global_weight * score) in |
493 val score_at = try (nth sels) #> Option.map (fn (_, score) => global_weight * score) |
|
494 in |
|
495 (case find_index (curry fact_eq fact o fst) sels of |
473 (case find_index (curry fact_eq fact o fst) sels of |
496 ~1 => if member fact_eq unks fact then NONE else SOME 0.0 |
474 ~1 => if member fact_eq unks fact then NONE else SOME 0.0 |
497 | rank => score_at rank) |
475 | rank => score_at rank) |
498 end |
476 end |
|
477 |
499 fun weight_of fact = mess |> map_filter (score_in fact) |> scaled_avg |
478 fun weight_of fact = mess |> map_filter (score_in fact) |> scaled_avg |
500 val facts = fold (union fact_eq o map fst o take max_facts o fst o snd) mess [] |
|
501 in |
479 in |
502 facts |> map (`weight_of) |> sort (int_ord o swap o pairself fst) |
480 fold (union fact_eq o map fst o take max_facts o fst o snd) mess [] |
503 |> map snd |> take max_facts |
481 |> map (`weight_of) |> sort (int_ord o swap o pairself fst) |
|
482 |> map snd |> take max_facts |
504 end |
483 end |
505 |
484 |
506 val default_weight = 1.0 |
485 val default_weight = 1.0 |
507 fun free_feature_of s = (["f" ^ s], 40.0 (* FUDGE *)) |
486 fun free_feature_of s = (["f" ^ s], 40.0 (* FUDGE *)) |
508 fun thy_feature_of s = (["y" ^ s], 8.0 (* FUDGE *)) |
487 fun thy_feature_of s = (["y" ^ s], 8.0 (* FUDGE *)) |
561 val pat_var_prefix = "_" |
540 val pat_var_prefix = "_" |
562 |
541 |
563 (* try "Long_Name.base_name" for shorter names *) |
542 (* try "Long_Name.base_name" for shorter names *) |
564 fun massage_long_name s = if s = @{class type} then "T" else s |
543 fun massage_long_name s = if s = @{class type} then "T" else s |
565 |
544 |
566 val crude_str_of_sort = |
545 val crude_str_of_sort = space_implode ":" o map massage_long_name o subtract (op =) @{sort type} |
567 space_implode ":" o map massage_long_name o subtract (op =) @{sort type} |
|
568 |
546 |
569 fun crude_str_of_typ (Type (s, [])) = massage_long_name s |
547 fun crude_str_of_typ (Type (s, [])) = massage_long_name s |
570 | crude_str_of_typ (Type (s, Ts)) = |
548 | crude_str_of_typ (Type (s, Ts)) = massage_long_name s ^ implode (map crude_str_of_typ Ts) |
571 massage_long_name s ^ implode (map crude_str_of_typ Ts) |
|
572 | crude_str_of_typ (TFree (_, S)) = crude_str_of_sort S |
549 | crude_str_of_typ (TFree (_, S)) = crude_str_of_sort S |
573 | crude_str_of_typ (TVar (_, S)) = crude_str_of_sort S |
550 | crude_str_of_typ (TVar (_, S)) = crude_str_of_sort S |
574 |
551 |
575 fun maybe_singleton_str _ "" = [] |
552 fun maybe_singleton_str _ "" = [] |
576 | maybe_singleton_str pref s = [pref ^ s] |
553 | maybe_singleton_str pref s = [pref ^ s] |
608 val classes = Sign.classes_of thy |
586 val classes = Sign.classes_of thy |
609 |
587 |
610 fun add_classes @{sort type} = I |
588 fun add_classes @{sort type} = I |
611 | add_classes S = |
589 | add_classes S = |
612 fold (`(Sorts.super_classes classes) |
590 fold (`(Sorts.super_classes classes) |
613 #> swap #> op :: |
591 #> swap #> op :: |
614 #> subtract (op =) @{sort type} #> map massage_long_name |
592 #> subtract (op =) @{sort type} #> map massage_long_name |
615 #> map class_feature_of |
593 #> map class_feature_of |
616 #> union (eq_fst (op =))) S |
594 #> union (eq_fst (op =))) S |
617 |
595 |
618 fun pattify_type 0 _ = [] |
596 fun pattify_type 0 _ = [] |
619 | pattify_type _ (Type (s, [])) = |
597 | pattify_type _ (Type (s, [])) = |
620 if member (op =) bad_types s then [] else [massage_long_name s] |
598 if member (op =) bad_types s then [] else [massage_long_name s] |
621 | pattify_type depth (Type (s, U :: Ts)) = |
599 | pattify_type depth (Type (s, U :: Ts)) = |
622 let |
600 let |
623 val T = Type (s, Ts) |
601 val T = Type (s, Ts) |
624 val ps = keep max_pat_breadth (pattify_type depth T) |
602 val ps = keep max_pat_breadth (pattify_type depth T) |
625 val qs = keep max_pat_breadth ("" :: pattify_type (depth - 1) U) |
603 val qs = keep max_pat_breadth ("" :: pattify_type (depth - 1) U) |
626 in map_product (fn p => fn "" => p | q => p ^ "(" ^ q ^ ")") ps qs end |
604 in |
|
605 map_product (fn p => fn "" => p | q => p ^ "(" ^ q ^ ")") ps qs |
|
606 end |
627 | pattify_type _ (TFree (_, S)) = |
607 | pattify_type _ (TFree (_, S)) = |
628 maybe_singleton_str pat_tvar_prefix (crude_str_of_sort S) |
608 maybe_singleton_str pat_tvar_prefix (crude_str_of_sort S) |
629 | pattify_type _ (TVar (_, S)) = |
609 | pattify_type _ (TVar (_, S)) = |
630 maybe_singleton_str pat_tvar_prefix (crude_str_of_sort S) |
610 maybe_singleton_str pat_tvar_prefix (crude_str_of_sort S) |
|
611 |
631 fun add_type_pat depth T = |
612 fun add_type_pat depth T = |
632 union (eq_fst (op =)) (map type_feature_of (pattify_type depth T)) |
613 union (eq_fst (op =)) (map type_feature_of (pattify_type depth T)) |
|
614 |
633 fun add_type_pats 0 _ = I |
615 fun add_type_pats 0 _ = I |
634 | add_type_pats depth t = |
616 | add_type_pats depth t = |
635 add_type_pat depth t #> add_type_pats (depth - 1) t |
617 add_type_pat depth t #> add_type_pats (depth - 1) t |
|
618 |
636 fun add_type T = |
619 fun add_type T = |
637 add_type_pats type_max_depth T |
620 add_type_pats type_max_depth T |
638 #> fold_atyps_sorts (add_classes o snd) T |
621 #> fold_atyps_sorts (add_classes o snd) T |
|
622 |
639 fun add_subtypes (T as Type (_, Ts)) = add_type T #> fold add_subtypes Ts |
623 fun add_subtypes (T as Type (_, Ts)) = add_type T #> fold add_subtypes Ts |
640 | add_subtypes T = add_type T |
624 | add_subtypes T = add_type T |
641 |
625 |
642 fun weight_of_const s = |
626 fun weight_of_const s = |
643 16.0 + |
627 16.0 + |
697 map_product (fn ppw as (p :: _, pw) => |
682 map_product (fn ppw as (p :: _, pw) => |
698 fn ([], _) => ppw |
683 fn ([], _) => ppw |
699 | (q :: _, qw) => ([p ^ "(" ^ q ^ ")"], pw + qw)) ps qs |
684 | (q :: _, qw) => ([p ^ "(" ^ q ^ ")"], pw + qw)) ps qs |
700 end |
685 end |
701 | pattify_term _ _ _ = [] |
686 | pattify_term _ _ _ = [] |
|
687 |
702 fun add_term_pat Ts = union (eq_fst (op =)) oo pattify_term Ts |
688 fun add_term_pat Ts = union (eq_fst (op =)) oo pattify_term Ts |
|
689 |
703 fun add_term_pats _ 0 _ = I |
690 fun add_term_pats _ 0 _ = I |
704 | add_term_pats Ts depth t = |
691 | add_term_pats Ts depth t = |
705 add_term_pat Ts depth t #> add_term_pats Ts (depth - 1) t |
692 add_term_pat Ts depth t #> add_term_pats Ts (depth - 1) t |
|
693 |
706 fun add_term Ts = add_term_pats Ts term_max_depth |
694 fun add_term Ts = add_term_pats Ts term_max_depth |
|
695 |
707 fun add_subterms Ts t = |
696 fun add_subterms Ts t = |
708 (case strip_comb t of |
697 (case strip_comb t of |
709 (Const (s, T), args) => |
698 (Const (s, T), args) => |
710 (not (is_widely_irrelevant_const s) ? add_term Ts t) |
699 (not (is_widely_irrelevant_const s) ? add_term Ts t) |
711 #> add_subtypes T |
700 #> add_subtypes T |
728 thy_feature_of thy_name :: |
719 thy_feature_of thy_name :: |
729 term_features_of ctxt thy_name num_facts const_tab term_max_depth type_max_depth in_goal ts |
720 term_features_of ctxt thy_name num_facts const_tab term_max_depth type_max_depth in_goal ts |
730 |> scope <> Global ? cons local_feature |
721 |> scope <> Global ? cons local_feature |
731 end |
722 end |
732 |
723 |
733 (* Too many dependencies is a sign that a decision procedure is at work. There |
724 (* Too many dependencies is a sign that a decision procedure is at work. There is not much to learn |
734 is not much to learn from such proofs. *) |
725 from such proofs. *) |
735 val max_dependencies = 20 |
726 val max_dependencies = 20 |
736 |
727 |
737 val prover_default_max_facts = 25 |
728 val prover_default_max_facts = 25 |
738 |
729 |
739 (* "type_definition_xxx" facts are characterized by their use of "CollectI". *) |
730 (* "type_definition_xxx" facts are characterized by their use of "CollectI". *) |
740 val typedef_dep = nickname_of_thm @{thm CollectI} |
731 val typedef_dep = nickname_of_thm @{thm CollectI} |
741 (* Mysterious parts of the class machinery create lots of proofs that refer |
732 (* Mysterious parts of the class machinery create lots of proofs that refer exclusively to |
742 exclusively to "someI_ex" (and to some internal constructions). *) |
733 "someI_ex" (and to some internal constructions). *) |
743 val class_some_dep = nickname_of_thm @{thm someI_ex} |
734 val class_some_dep = nickname_of_thm @{thm someI_ex} |
744 |
735 |
745 val fundef_ths = |
736 val fundef_ths = |
746 @{thms fundef_ex1_existence fundef_ex1_uniqueness fundef_ex1_iff |
737 @{thms fundef_ex1_existence fundef_ex1_uniqueness fundef_ex1_iff fundef_default_value} |
747 fundef_default_value} |
|
748 |> map nickname_of_thm |
738 |> map nickname_of_thm |
749 |
739 |
750 (* "Rep_xxx_inject", "Abs_xxx_inverse", etc., are derived using these facts. *) |
740 (* "Rep_xxx_inject", "Abs_xxx_inverse", etc., are derived using these facts. *) |
751 val typedef_ths = |
741 val typedef_ths = |
752 @{thms type_definition.Abs_inverse type_definition.Rep_inverse |
742 @{thms type_definition.Abs_inverse type_definition.Rep_inverse type_definition.Rep |
753 type_definition.Rep type_definition.Rep_inject |
743 type_definition.Rep_inject type_definition.Abs_inject type_definition.Rep_cases |
754 type_definition.Abs_inject type_definition.Rep_cases |
744 type_definition.Abs_cases type_definition.Rep_induct type_definition.Abs_induct |
755 type_definition.Abs_cases type_definition.Rep_induct |
745 type_definition.Rep_range type_definition.Abs_image} |
756 type_definition.Abs_induct type_definition.Rep_range |
|
757 type_definition.Abs_image} |
|
758 |> map nickname_of_thm |
746 |> map nickname_of_thm |
759 |
747 |
760 fun is_size_def [dep] th = |
748 fun is_size_def [dep] th = |
761 (case first_field ".rec" dep of |
749 (case first_field ".rec" dep of |
762 SOME (pref, _) => |
750 SOME (pref, _) => |
763 (case first_field ".size" (nickname_of_thm th) of |
751 (case first_field ".size" (nickname_of_thm th) of |
764 SOME (pref', _) => pref = pref' |
752 SOME (pref', _) => pref = pref' |
765 | NONE => false) |
753 | NONE => false) |
766 | NONE => false) |
754 | NONE => false) |
767 | is_size_def _ _ = false |
755 | is_size_def _ _ = false |
768 |
756 |
769 fun no_dependencies_for_status status = |
757 fun no_dependencies_for_status status = |
770 status = Non_Rec_Def orelse status = Rec_Def |
758 status = Non_Rec_Def orelse status = Rec_Def |
771 |
759 |
772 fun trim_dependencies deps = |
760 fun trim_dependencies deps = |
773 if length deps > max_dependencies then NONE else SOME deps |
761 if length deps > max_dependencies then NONE else SOME deps |
774 |
762 |
775 fun isar_dependencies_of name_tabs th = |
763 fun isar_dependencies_of name_tabs th = |
776 let val deps = thms_in_proof (SOME name_tabs) th in |
764 let val deps = thms_in_proof (SOME name_tabs) th in |
777 if deps = [typedef_dep] orelse |
765 if deps = [typedef_dep] orelse deps = [class_some_dep] orelse |
778 deps = [class_some_dep] orelse |
766 exists (member (op =) fundef_ths) deps orelse exists (member (op =) typedef_ths) deps orelse |
779 exists (member (op =) fundef_ths) deps orelse |
|
780 exists (member (op =) typedef_ths) deps orelse |
|
781 is_size_def deps th then |
767 is_size_def deps th then |
782 [] |
768 [] |
783 else |
769 else |
784 deps |
770 deps |
785 end |
771 end |
786 |
772 |
787 fun prover_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover |
773 fun prover_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover auto_level facts |
788 auto_level facts name_tabs th = |
774 name_tabs th = |
789 (case isar_dependencies_of name_tabs th of |
775 (case isar_dependencies_of name_tabs th of |
790 [] => (false, []) |
776 [] => (false, []) |
791 | isar_deps => |
777 | isar_deps => |
792 let |
778 let |
793 val thy = Proof_Context.theory_of ctxt |
779 val thy = Proof_Context.theory_of ctxt |
794 val goal = goal_of_thm thy th |
780 val goal = goal_of_thm thy th |
795 val name = nickname_of_thm th |
781 val name = nickname_of_thm th |
796 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt |
782 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt |
797 val facts = facts |> filter (fn (_, th') => thm_less (th', th)) |
783 val facts = facts |> filter (fn (_, th') => thm_less (th', th)) |
|
784 |
798 fun nickify ((_, stature), th) = ((nickname_of_thm th, stature), th) |
785 fun nickify ((_, stature), th) = ((nickname_of_thm th, stature), th) |
|
786 |
799 fun is_dep dep (_, th) = nickname_of_thm th = dep |
787 fun is_dep dep (_, th) = nickname_of_thm th = dep |
|
788 |
800 fun add_isar_dep facts dep accum = |
789 fun add_isar_dep facts dep accum = |
801 if exists (is_dep dep) accum then |
790 if exists (is_dep dep) accum then |
802 accum |
791 accum |
803 else |
792 else |
804 (case find_first (is_dep dep) facts of |
793 (case find_first (is_dep dep) facts of |
805 SOME ((_, status), th) => accum @ [(("", status), th)] |
794 SOME ((_, status), th) => accum @ [(("", status), th)] |
806 | NONE => accum (* should not happen *)) |
795 | NONE => accum (* should not happen *)) |
|
796 |
807 val mepo_facts = |
797 val mepo_facts = |
808 facts |
798 facts |
809 |> mepo_suggested_facts ctxt params (max_facts |> the_default prover_default_max_facts) NONE |
799 |> mepo_suggested_facts ctxt params (max_facts |> the_default prover_default_max_facts) NONE |
810 hyp_ts concl_t |
800 hyp_ts concl_t |
811 val facts = |
801 val facts = |
844 fun insert_parent new parents = |
834 fun insert_parent new parents = |
845 let val parents = parents |> filter_out (fn p => thm_less_eq (p, new)) in |
835 let val parents = parents |> filter_out (fn p => thm_less_eq (p, new)) in |
846 parents |> forall (fn p => not (thm_less_eq (new, p))) parents |
836 parents |> forall (fn p => not (thm_less_eq (new, p))) parents |
847 ? cons new |
837 ? cons new |
848 end |
838 end |
|
839 |
849 fun rechunk seen (rest as th' :: ths) = |
840 fun rechunk seen (rest as th' :: ths) = |
850 if thm_less_eq (th', th) then (rev seen, rest) |
841 if thm_less_eq (th', th) then (rev seen, rest) |
851 else rechunk (th' :: seen) ths |
842 else rechunk (th' :: seen) ths |
|
843 |
852 fun do_chunk [] accum = accum |
844 fun do_chunk [] accum = accum |
853 | do_chunk (chunk as hd_chunk :: _) (chunks, parents) = |
845 | do_chunk (chunk as hd_chunk :: _) (chunks, parents) = |
854 if thm_less_eq (hd_chunk, th) then |
846 if thm_less_eq (hd_chunk, th) then |
855 (chunk :: chunks, insert_parent hd_chunk parents) |
847 (chunk :: chunks, insert_parent hd_chunk parents) |
856 else if thm_less_eq (List.last chunk, th) then |
848 else if thm_less_eq (List.last chunk, th) then |
878 if thm_less_eq (th, th') andalso |
870 if thm_less_eq (th, th') andalso |
879 thy_name_of_thm th = thy_name_of_thm th' then |
871 thy_name_of_thm th = thy_name_of_thm th' then |
880 (chunks, [nickname_of_thm th]) |
872 (chunks, [nickname_of_thm th]) |
881 else |
873 else |
882 chunks_and_parents_for chunks th' |
874 chunks_and_parents_for chunks th' |
883 in (parents, fact) :: do_facts chunks_and_parents' facts end |
875 in |
|
876 (parents, fact) :: do_facts chunks_and_parents' facts |
|
877 end |
884 in |
878 in |
885 old_facts @ facts |
879 old_facts @ facts |
886 |> do_facts (chunks_and_parents_for [[]] th) |
880 |> do_facts (chunks_and_parents_for [[]] th) |
887 |> drop (length old_facts) |
881 |> drop (length old_facts) |
888 end |
882 end |
889 |
883 |
890 fun maximal_wrt_graph G keys = |
884 fun maximal_wrt_graph G keys = |
891 let |
885 let |
892 val tab = Symtab.empty |> fold (fn name => Symtab.default (name, ())) keys |
886 val tab = Symtab.empty |> fold (fn name => Symtab.default (name, ())) keys |
|
887 |
893 fun insert_new seen name = |
888 fun insert_new seen name = |
894 not (Symtab.defined seen name) ? insert (op =) name |
889 not (Symtab.defined seen name) ? insert (op =) name |
|
890 |
895 fun num_keys keys = Graph.Keys.fold (K (Integer.add 1)) keys 0 |
891 fun num_keys keys = Graph.Keys.fold (K (Integer.add 1)) keys 0 |
|
892 |
896 fun find_maxes _ (maxs, []) = map snd maxs |
893 fun find_maxes _ (maxs, []) = map snd maxs |
897 | find_maxes seen (maxs, new :: news) = |
894 | find_maxes seen (maxs, new :: news) = |
898 find_maxes |
895 find_maxes |
899 (seen |> num_keys (Graph.imm_succs G new) > 1 |
896 (seen |> num_keys (Graph.imm_succs G new) > 1 |
900 ? Symtab.default (new, ())) |
897 ? Symtab.default (new, ())) |
956 (0.1 (* FUDGE *), (weight_facts_steeply raw_mash, raw_unknown))] |
955 (0.1 (* FUDGE *), (weight_facts_steeply raw_mash, raw_unknown))] |
957 val unknown = |
956 val unknown = |
958 raw_unknown |
957 raw_unknown |
959 |> fold (subtract (eq_snd Thm.eq_thm_prop)) |
958 |> fold (subtract (eq_snd Thm.eq_thm_prop)) |
960 [unknown_chained, unknown_proximate] |
959 [unknown_chained, unknown_proximate] |
961 in (mesh_facts (eq_snd Thm.eq_thm_prop) max_facts mess, unknown) end |
960 in |
|
961 (mesh_facts (eq_snd Thm.eq_thm_prop) max_facts mess, unknown) |
|
962 end |
962 |
963 |
963 fun add_const_counts t = |
964 fun add_const_counts t = |
964 fold (fn s => Symtab.map_default (s, 0) (Integer.add 1)) |
965 fold (fn s => Symtab.map_default (s, 0) (Integer.add 1)) (Term.add_const_names t []) |
965 (Term.add_const_names t []) |
|
966 |
966 |
967 fun mash_suggested_facts ctxt ({debug, overlord, ...} : params) max_facts hyp_ts concl_t facts = |
967 fun mash_suggested_facts ctxt ({debug, overlord, ...} : params) max_facts hyp_ts concl_t facts = |
968 let |
968 let |
969 val thy = Proof_Context.theory_of ctxt |
969 val thy = Proof_Context.theory_of ctxt |
970 val thy_name = Context.theory_name thy |
970 val thy_name = Context.theory_name thy |
1021 try_graph ctxt "updating graph" accum (fn () => |
1020 try_graph ctxt "updating graph" accum (fn () => |
1022 (from :: parents, Graph.add_edge_acyclic (from, name) graph)) |
1021 (from :: parents, Graph.add_edge_acyclic (from, name) graph)) |
1023 val graph = graph |> Graph.default_node (name, (Isar_Proof, feats, deps)) |
1022 val graph = graph |> Graph.default_node (name, (Isar_Proof, feats, deps)) |
1024 val (parents, graph) = ([], graph) |> fold maybe_learn_from parents |
1023 val (parents, graph) = ([], graph) |> fold maybe_learn_from parents |
1025 val (deps, _) = ([], graph) |> fold maybe_learn_from deps |
1024 val (deps, _) = ([], graph) |> fold maybe_learn_from deps |
1026 in ((name, parents, feats, deps) :: learns, graph) end |
1025 in |
|
1026 ((name, parents, feats, deps) :: learns, graph) |
|
1027 end |
1027 |
1028 |
1028 fun relearn_wrt_access_graph ctxt (name, deps) (relearns, graph) = |
1029 fun relearn_wrt_access_graph ctxt (name, deps) (relearns, graph) = |
1029 let |
1030 let |
1030 fun maybe_relearn_from from (accum as (parents, graph)) = |
1031 fun maybe_relearn_from from (accum as (parents, graph)) = |
1031 try_graph ctxt "updating graph" accum (fn () => |
1032 try_graph ctxt "updating graph" accum (fn () => |
1032 (from :: parents, Graph.add_edge_acyclic (from, name) graph)) |
1033 (from :: parents, Graph.add_edge_acyclic (from, name) graph)) |
1033 val graph = graph |> Graph.map_node name (fn (_, feats, _) => (Automatic_Proof, feats, deps)) |
1034 val graph = graph |> Graph.map_node name (fn (_, feats, _) => (Automatic_Proof, feats, deps)) |
1034 val (deps, _) = ([], graph) |> fold maybe_relearn_from deps |
1035 val (deps, _) = ([], graph) |> fold maybe_relearn_from deps |
1035 in ((name, deps) :: relearns, graph) end |
1036 in |
|
1037 ((name, deps) :: relearns, graph) |
|
1038 end |
1036 |
1039 |
1037 fun flop_wrt_access_graph name = |
1040 fun flop_wrt_access_graph name = |
1038 Graph.map_node name (fn (_, feats, deps) => (Isar_Proof_wegen_Prover_Flop, feats, deps)) |
1041 Graph.map_node name (fn (_, feats, deps) => (Isar_Proof_wegen_Prover_Flop, feats, deps)) |
1039 |
1042 |
1040 val learn_timeout_slack = 2.0 |
1043 val learn_timeout_slack = 2.0 |
1043 let |
1046 let |
1044 val hard_timeout = time_mult learn_timeout_slack timeout |
1047 val hard_timeout = time_mult learn_timeout_slack timeout |
1045 val birth_time = Time.now () |
1048 val birth_time = Time.now () |
1046 val death_time = Time.+ (birth_time, hard_timeout) |
1049 val death_time = Time.+ (birth_time, hard_timeout) |
1047 val desc = ("Machine learner for Sledgehammer", "") |
1050 val desc = ("Machine learner for Sledgehammer", "") |
1048 in Async_Manager.thread MaShN birth_time death_time desc task end |
1051 in |
|
1052 Async_Manager.thread MaShN birth_time death_time desc task |
|
1053 end |
1049 |
1054 |
1050 fun mash_learn_proof ctxt ({overlord, timeout, ...} : params) t facts used_ths = |
1055 fun mash_learn_proof ctxt ({overlord, timeout, ...} : params) t facts used_ths = |
1051 if is_mash_enabled () then |
1056 if is_mash_enabled () then |
1052 launch_thread timeout (fn () => |
1057 launch_thread timeout (fn () => |
1053 let |
1058 let |
1054 val thy = Proof_Context.theory_of ctxt |
1059 val thy = Proof_Context.theory_of ctxt |
1055 val feats = features_of ctxt thy 0 Symtab.empty (Local, General) false [t] |> map fst |
1060 val feats = features_of ctxt thy 0 Symtab.empty (Local, General) false [t] |> map fst |
1056 in |
1061 in |
1057 peek_state ctxt overlord (fn {access_G, ...} => |
1062 peek_state ctxt overlord (fn {access_G, ...} => |
1058 let |
1063 let |
1059 val parents = maximal_wrt_access_graph access_G facts |
1064 val parents = maximal_wrt_access_graph access_G facts |
1060 val deps = |
1065 val deps = |
1061 used_ths |> filter (is_fact_in_graph access_G) |
1066 used_ths |> filter (is_fact_in_graph access_G) |
1062 |> map nickname_of_thm |
1067 |> map nickname_of_thm |
1063 in |
1068 in |
1064 MaSh.learn ctxt overlord true [("", parents, feats, deps)] |
1069 MaSh.learn ctxt overlord true [("", parents, feats, deps)] |
1065 end); |
1070 end); |
1066 (true, "") |
1071 (true, "") |
1067 end) |
1072 end) |
1068 else |
1073 else |
1069 () |
1074 () |
1070 |
1075 |
1071 fun sendback sub = |
1076 fun sendback sub = |
1072 Active.sendback_markup [Markup.padding_command] (sledgehammerN ^ " " ^ sub) |
1077 Active.sendback_markup [Markup.padding_command] (sledgehammerN ^ " " ^ sub) |
1229 end |
1234 end |
1230 in |
1235 in |
1231 if verbose orelse auto_level < 2 then |
1236 if verbose orelse auto_level < 2 then |
1232 "Learned " ^ string_of_int n ^ " nontrivial " ^ |
1237 "Learned " ^ string_of_int n ^ " nontrivial " ^ |
1233 (if run_prover then "automatic and " else "") ^ "Isar proof" ^ plural_s n ^ |
1238 (if run_prover then "automatic and " else "") ^ "Isar proof" ^ plural_s n ^ |
1234 (if verbose then " in " ^ string_of_time (Timer.checkRealTimer timer) |
1239 (if verbose then " in " ^ string_of_time (Timer.checkRealTimer timer) else "") ^ "." |
1235 else "") ^ "." |
|
1236 else |
1240 else |
1237 "" |
1241 "" |
1238 end |
1242 end |
1239 end |
1243 end |
1240 |
1244 |
1241 fun mash_learn ctxt (params as {provers, timeout, ...}) fact_override chained run_prover = |
1245 fun mash_learn ctxt (params as {provers, timeout, ...}) fact_override chained run_prover = |
1242 let |
1246 let |
1243 val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt |
1247 val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt |
1244 val ctxt = ctxt |> Config.put instantiate_inducts false |
1248 val ctxt = ctxt |> Config.put instantiate_inducts false |
1245 val facts = |
1249 val facts = nearly_all_facts ctxt false fact_override Symtab.empty css chained [] @{prop True} |
1246 nearly_all_facts ctxt false fact_override Symtab.empty css chained [] |
|
1247 @{prop True} |
|
1248 |> sort (crude_thm_ord o pairself snd o swap) |
1250 |> sort (crude_thm_ord o pairself snd o swap) |
1249 val num_facts = length facts |
1251 val num_facts = length facts |
1250 val prover = hd provers |
1252 val prover = hd provers |
|
1253 |
1251 fun learn auto_level run_prover = |
1254 fun learn auto_level run_prover = |
1252 mash_learn_facts ctxt params prover true auto_level run_prover one_year facts |
1255 mash_learn_facts ctxt params prover true auto_level run_prover one_year facts |
1253 |> Output.urgent_message |
1256 |> Output.urgent_message |
1254 in |
1257 in |
1255 if run_prover then |
1258 if run_prover then |
1256 ("MaShing through " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ |
1259 ("MaShing through " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ |
1257 " for automatic proofs (" ^ quote prover ^ " timeout: " ^ string_of_time timeout ^ |
1260 " for automatic proofs (" ^ quote prover ^ " timeout: " ^ string_of_time timeout ^ |
1258 ").\n\nCollecting Isar proofs first..." |
1261 ").\n\nCollecting Isar proofs first..." |
1259 |> Output.urgent_message; |
1262 |> Output.urgent_message; |
1260 learn 1 false; |
1263 learn 1 false; |
1261 "Now collecting automatic proofs. This may take several hours. You can \ |
1264 "Now collecting automatic proofs. This may take several hours. You can safely stop the \ |
1262 \safely stop the learning process at any point." |
1265 \learning process at any point." |
1263 |> Output.urgent_message; |
1266 |> Output.urgent_message; |
1264 learn 0 true) |
1267 learn 0 true) |
1265 else |
1268 else |
1266 ("MaShing through " ^ string_of_int num_facts ^ " fact" ^ |
1269 (Output.urgent_message ("MaShing through " ^ string_of_int num_facts ^ " fact" ^ |
1267 plural_s num_facts ^ " for Isar proofs..." |
1270 plural_s num_facts ^ " for Isar proofs..."); |
1268 |> Output.urgent_message; |
|
1269 learn 0 false) |
1271 learn 0 false) |
1270 end |
1272 end |
1271 |
1273 |
1272 fun mash_can_suggest_facts ctxt overlord = |
1274 fun mash_can_suggest_facts ctxt overlord = |
1273 not (Graph.is_empty (#access_G (peek_state ctxt overlord I))) |
1275 not (Graph.is_empty (#access_G (peek_state ctxt overlord I))) |