184 EQUAL => string_ord (pairself Context.theory_name p) |
184 EQUAL => string_ord (pairself Context.theory_name p) |
185 | order => order |
185 | order => order |
186 |
186 |
187 val thm_ord = theory_ord o pairself theory_of_thm |
187 val thm_ord = theory_ord o pairself theory_of_thm |
188 |
188 |
|
189 val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}] |
|
190 |
189 fun interesting_terms_types_and_classes ctxt prover term_max_depth |
191 fun interesting_terms_types_and_classes ctxt prover term_max_depth |
190 type_max_depth ts = |
192 type_max_depth ts = |
191 let |
193 let |
192 val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}] |
|
193 fun is_bad_const (x as (s, _)) args = |
194 fun is_bad_const (x as (s, _)) args = |
194 member (op =) atp_logical_consts s orelse |
195 member (op =) atp_logical_consts s orelse |
195 fst (is_built_in_const_for_prover ctxt prover x args) |
196 fst (is_built_in_const_for_prover ctxt prover x args) |
196 fun add_classes @{sort type} = I |
197 fun add_classes @{sort type} = I |
197 | add_classes S = union (op =) (map class_name_of S) |
198 | add_classes S = union (op =) (map class_name_of S) |
247 | Inductive => cons "inductive" |
248 | Inductive => cons "inductive" |
248 | Elim => cons "elim" |
249 | Elim => cons "elim" |
249 | Simp => cons "simp" |
250 | Simp => cons "simp" |
250 | Def => cons "def") |
251 | Def => cons "def") |
251 |
252 |
252 fun isabelle_dependencies_of all_facts = |
253 fun isabelle_dependencies_of all_facts = thms_in_proof (SOME all_facts) |
253 thms_in_proof (SOME all_facts) #> sort string_ord |
|
254 |
254 |
255 val freezeT = Type.legacy_freeze_type |
255 val freezeT = Type.legacy_freeze_type |
256 |
256 |
257 fun freeze (t $ u) = freeze t $ freeze u |
257 fun freeze (t $ u) = freeze t $ freeze u |
258 | freeze (Abs (s, T, t)) = Abs (s, freezeT T, freeze t) |
258 | freeze (Abs (s, T, t)) = Abs (s, freezeT T, freeze t) |
505 (* The timeout is understood in a very slack fashion. *) |
505 (* The timeout is understood in a very slack fashion. *) |
506 fun mash_learn_thy ctxt ({provers, verbose, overlord, ...} : params) thy timeout |
506 fun mash_learn_thy ctxt ({provers, verbose, overlord, ...} : params) thy timeout |
507 facts = |
507 facts = |
508 let |
508 let |
509 val timer = Timer.startRealTimer () |
509 val timer = Timer.startRealTimer () |
510 fun check_timer s = |
|
511 tracing ("*** " ^ s ^ " " ^ PolyML.makestring (Timer.checkRealTimer timer)) |
|
512 val prover = hd provers |
510 val prover = hd provers |
513 fun timed_out frac = |
511 fun timed_out frac = |
514 Time.> (Timer.checkRealTimer timer, time_mult frac timeout) |
512 Time.> (Timer.checkRealTimer timer, time_mult frac timeout) |
515 val _ = check_timer "begin" (*###*) |
|
516 val {fact_graph, ...} = mash_get ctxt |
513 val {fact_graph, ...} = mash_get ctxt |
517 val _ = check_timer " got" (*###*) |
|
518 val new_facts = |
514 val new_facts = |
519 facts |> filter_out (is_fact_in_graph fact_graph) |
515 facts |> filter_out (is_fact_in_graph fact_graph) |
520 |> sort (thm_ord o pairself snd) |
516 |> sort (thm_ord o pairself snd) |
521 val _ = check_timer " new facts" (*###*) |
|
522 in |
517 in |
523 if null new_facts then |
518 if null new_facts then |
524 "" |
519 "" |
525 else |
520 else |
526 let |
521 let |
527 val ths = facts |> map snd |
522 val ths = facts |> map snd |
528 val all_names = |
523 val all_names = |
529 ths |> filter_out is_likely_tautology_or_too_meta |
524 ths |> filter_out is_likely_tautology_or_too_meta |
530 |> map (rpair () o Thm.get_name_hint) |
525 |> map (rpair () o Thm.get_name_hint) |
531 |> Symtab.make |
526 |> Symtab.make |
532 val _ = check_timer " all names" (*###*) |
|
533 fun do_fact _ (accum as (_, true)) = accum |
527 fun do_fact _ (accum as (_, true)) = accum |
534 | do_fact ((_, (_, status)), th) ((parents, upds), false) = |
528 | do_fact ((_, (_, status)), th) ((parents, upds), false) = |
535 let |
529 let |
536 val name = Thm.get_name_hint th |
530 val name = Thm.get_name_hint th |
537 val feats = features_of ctxt prover thy status [prop_of th] |
531 val feats = features_of ctxt prover thy status [prop_of th] |
538 val deps = isabelle_dependencies_of all_names th |
532 val deps = isabelle_dependencies_of all_names th |
539 val upd = (name, parents, feats, deps) |
533 val upd = (name, parents, feats, deps) |
540 in (([name], upd :: upds), timed_out pass1_learn_timeout_factor) end |
534 in (([name], upd :: upds), timed_out pass1_learn_timeout_factor) end |
541 val parents = parents_wrt_facts ctxt facts fact_graph |
535 val parents = parents_wrt_facts ctxt facts fact_graph |
542 val _ = check_timer " parents" (*###*) |
|
543 val ((_, upds), _) = |
536 val ((_, upds), _) = |
544 ((parents, []), false) |> fold do_fact new_facts |>> apsnd rev |
537 ((parents, []), false) |> fold do_fact new_facts |>> apsnd rev |
545 val _ = check_timer " did facts" (*###*) |
|
546 val n = length upds |
538 val n = length upds |
547 fun trans {thys, fact_graph} = |
539 fun trans {thys, fact_graph} = |
548 let |
540 let |
549 val mash_INIT_or_ADD = |
541 val mash_INIT_or_ADD = |
550 if Graph.is_empty fact_graph then mash_INIT else mash_ADD |
542 if Graph.is_empty fact_graph then mash_INIT else mash_ADD |
551 val (upds, fact_graph) = |
543 val (upds, fact_graph) = |
552 ([], fact_graph) |> fold (update_fact_graph ctxt) upds |
544 ([], fact_graph) |> fold (update_fact_graph ctxt) upds |
553 val _ = check_timer " updated" (*###*) |
|
554 in |
545 in |
555 (mash_INIT_or_ADD ctxt overlord (rev upds); |
546 (mash_INIT_or_ADD ctxt overlord (rev upds); |
556 check_timer " inited/added" (*###*); |
|
557 {thys = thys |> add_thys_for thy, |
547 {thys = thys |> add_thys_for thy, |
558 fact_graph = fact_graph}) |
548 fact_graph = fact_graph}) |
559 end |
549 end |
560 in |
550 in |
561 mash_map ctxt trans; |
551 mash_map ctxt trans; |