54 Proof.context -> ('b * thm) list -> string list -> ('b * thm) list |
54 Proof.context -> ('b * thm) list -> string list -> ('b * thm) list |
55 val mesh_facts : |
55 val mesh_facts : |
56 ('a * 'a -> bool) -> int -> (real * (('a * real) list * 'a list)) list |
56 ('a * 'a -> bool) -> int -> (real * (('a * real) list * 'a list)) list |
57 -> 'a list |
57 -> 'a list |
58 val crude_thm_ord : thm * thm -> order |
58 val crude_thm_ord : thm * thm -> order |
|
59 val thm_less : thm * thm -> bool |
59 val goal_of_thm : theory -> thm -> thm |
60 val goal_of_thm : theory -> thm -> thm |
60 val run_prover_for_mash : |
61 val run_prover_for_mash : |
61 Proof.context -> params -> string -> fact list -> thm -> prover_result |
62 Proof.context -> params -> string -> fact list -> thm -> prover_result |
62 val features_of : |
63 val features_of : |
63 Proof.context -> string -> theory -> stature -> term list |
64 Proof.context -> string -> theory -> stature -> term list |
78 Proof.context -> params -> string -> int -> term list -> term |
79 Proof.context -> params -> string -> int -> term list -> term |
79 -> raw_fact list -> fact list * fact list |
80 -> raw_fact list -> fact list * fact list |
80 val mash_learn_proof : |
81 val mash_learn_proof : |
81 Proof.context -> params -> string -> term -> ('a * thm) list -> thm list |
82 Proof.context -> params -> string -> term -> ('a * thm) list -> thm list |
82 -> unit |
83 -> unit |
|
84 val attach_parents_to_facts : |
|
85 ('a * thm) list -> ('a * thm) list -> (string list * ('a * thm)) list |
83 val mash_learn : |
86 val mash_learn : |
84 Proof.context -> params -> fact_override -> thm list -> bool -> unit |
87 Proof.context -> params -> fact_override -> thm list -> bool -> unit |
85 val is_mash_enabled : unit -> bool |
88 val is_mash_enabled : unit -> bool |
86 val mash_can_suggest_facts : Proof.context -> bool |
89 val mash_can_suggest_facts : Proof.context -> bool |
87 val generous_max_facts : int -> int |
90 val generous_max_facts : int -> int |
900 MaSh.learn ctxt overlord [(name, parents, feats, deps)] |
903 MaSh.learn ctxt overlord [(name, parents, feats, deps)] |
901 end); |
904 end); |
902 (true, "") |
905 (true, "") |
903 end) |
906 end) |
904 |
907 |
|
908 (* In the following functions, chunks are risers w.r.t. "thm_less_eq". *) |
|
909 |
905 fun chunks_and_parents_for chunks th = |
910 fun chunks_and_parents_for chunks th = |
906 let |
911 let |
907 fun insert_parent new parents = |
912 fun insert_parent new parents = |
908 let val parents = parents |> filter_out (fn p => thm_less_eq (p, new)) in |
913 let val parents = parents |> filter_out (fn p => thm_less_eq (p, new)) in |
909 parents |> forall (fn p => not (thm_less_eq (new, p))) parents |
914 parents |> forall (fn p => not (thm_less_eq (new, p))) parents |
923 else |
928 else |
924 (chunk :: chunks, parents) |
929 (chunk :: chunks, parents) |
925 in |
930 in |
926 fold_rev do_chunk chunks ([], []) |
931 fold_rev do_chunk chunks ([], []) |
927 |>> cons [] |
932 |>> cons [] |
|
933 ||> map nickname_of_thm |
928 end |
934 end |
929 |
935 |
930 fun attach_parents_to_facts facts = |
936 fun attach_parents_to_facts _ [] = [] |
931 let |
937 | attach_parents_to_facts old_facts (facts as (_, th) :: _) = |
932 fun do_facts _ _ [] = [] |
938 let |
933 | do_facts _ parents [fact] = [(parents, fact)] |
939 fun do_facts _ [] = [] |
934 | do_facts chunks parents ((fact as (_, th)) :: (facts as (_, th') :: _)) = |
940 | do_facts (_, parents) [fact] = [(parents, fact)] |
935 let |
941 | do_facts (chunks, parents) |
936 val chunks = app_hd (cons th) chunks |
942 ((fact as (_, th)) :: (facts as (_, th') :: _)) = |
937 val (chunks', parents') = |
943 let |
938 (if thm_less_eq (th, th') andalso |
944 val chunks = app_hd (cons th) chunks |
939 thy_name_of_thm th = thy_name_of_thm th' then |
945 val chunks_and_parents' = |
940 (chunks, [th]) |
946 if thm_less_eq (th, th') andalso |
941 else |
947 thy_name_of_thm th = thy_name_of_thm th' then |
942 chunks_and_parents_for chunks th') |
948 (chunks, [nickname_of_thm th]) |
943 ||> map nickname_of_thm |
949 else |
944 in (parents, fact) :: do_facts chunks' parents' facts end |
950 chunks_and_parents_for chunks th' |
945 in |
951 in (parents, fact) :: do_facts chunks_and_parents' facts end |
946 facts |> sort (crude_thm_ord o pairself snd) |
952 in |
947 |> do_facts [[]] [] |
953 old_facts @ facts |
948 end |
954 |> do_facts (chunks_and_parents_for [[]] th) |
|
955 |> drop (length old_facts) |
|
956 end |
949 |
957 |
950 fun sendback sub = Active.sendback_markup (sledgehammerN ^ " " ^ sub) |
958 fun sendback sub = Active.sendback_markup (sledgehammerN ^ " " ^ sub) |
951 |
959 |
952 val commit_timeout = seconds 30.0 |
960 val commit_timeout = seconds 30.0 |
953 |
961 |
1044 val n = |
1052 val n = |
1045 if no_new_facts then |
1053 if no_new_facts then |
1046 0 |
1054 0 |
1047 else |
1055 else |
1048 let |
1056 let |
1049 val facts = |
1057 val new_facts = |
1050 facts |> attach_parents_to_facts |
1058 facts |> attach_parents_to_facts |
1051 |> filter_out (is_in_access_G o snd) |
1059 |> filter_out (is_in_access_G o snd) |
1052 val (learns, (n, _, _)) = |
1060 val (learns, (n, _, _)) = |
1053 ([], (0, next_commit_time (), false)) |
1061 ([], (0, next_commit_time (), false)) |
1054 |> fold learn_new_fact facts |
1062 |> fold learn_new_fact new_facts |
1055 in commit true learns [] []; n end |
1063 in commit true learns [] []; n end |
1056 fun relearn_old_fact _ (accum as (_, (_, _, true))) = accum |
1064 fun relearn_old_fact _ (accum as (_, (_, _, true))) = accum |
1057 | relearn_old_fact ((_, (_, status)), th) |
1065 | relearn_old_fact ((_, (_, status)), th) |
1058 ((relearns, flops), (n, next_commit, _)) = |
1066 ((relearns, flops), (n, next_commit, _)) = |
1059 let |
1067 let |