549 in |
549 in |
550 |
550 |
551 fun mash_map ctxt f = |
551 fun mash_map ctxt f = |
552 Synchronized.change global_state (load ctxt ##> (f #> tap (save ctxt))) |
552 Synchronized.change global_state (load ctxt ##> (f #> tap (save ctxt))) |
553 |
553 |
|
554 fun mash_peek ctxt f = |
|
555 Synchronized.change_result global_state (load ctxt #> `snd #>> f) |
|
556 |
554 fun mash_get ctxt = |
557 fun mash_get ctxt = |
555 Synchronized.change_result global_state (load ctxt #> `snd) |
558 Synchronized.change_result global_state (load ctxt #> `snd) |
556 |
559 |
557 fun mash_unlearn ctxt = |
560 fun mash_unlearn ctxt = |
558 Synchronized.change global_state (fn _ => |
561 Synchronized.change global_state (fn _ => |
596 in find_maxes Symtab.empty ([], Graph.maximals fact_G) end |
599 in find_maxes Symtab.empty ([], Graph.maximals fact_G) end |
597 |
600 |
598 (* Generate more suggestions than requested, because some might be thrown out |
601 (* Generate more suggestions than requested, because some might be thrown out |
599 later for various reasons and "meshing" gives better results with some |
602 later for various reasons and "meshing" gives better results with some |
600 slack. *) |
603 slack. *) |
601 fun max_suggs_of max_facts = max_facts + Int.min (200, max_facts) |
604 fun max_suggs_of max_facts = max_facts + Int.min (50, max_facts) |
602 |
605 |
603 fun is_fact_in_graph fact_G (_, th) = |
606 fun is_fact_in_graph fact_G (_, th) = |
604 can (Graph.get_node fact_G) (nickname_of th) |
607 can (Graph.get_node fact_G) (nickname_of th) |
605 |
608 |
606 fun mash_suggested_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts |
609 fun mash_suggested_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts |
607 concl_t facts = |
610 concl_t facts = |
608 let |
611 let |
609 val thy = Proof_Context.theory_of ctxt |
612 val thy = Proof_Context.theory_of ctxt |
610 val fact_G = #fact_G (mash_get ctxt) |
613 val (fact_G, suggs) = |
611 val parents = maximal_in_graph fact_G facts |
614 mash_peek ctxt (fn {fact_G} => |
612 val feats = features_of ctxt prover thy (Local, General) (concl_t :: hyp_ts) |
615 if Graph.is_empty fact_G then |
613 val suggs = |
616 (fact_G, []) |
614 if Graph.is_empty fact_G then [] |
617 else |
615 else mash_QUERY ctxt overlord (max_suggs_of max_facts) (parents, feats) |
618 let |
|
619 val parents = maximal_in_graph fact_G facts |
|
620 val feats = |
|
621 features_of ctxt prover thy (Local, General) (concl_t :: hyp_ts) |
|
622 in |
|
623 (fact_G, mash_QUERY ctxt overlord (max_suggs_of max_facts) |
|
624 (parents, feats)) |
|
625 end) |
616 val selected = |
626 val selected = |
617 facts |> suggested_facts suggs |
627 facts |> suggested_facts suggs |
618 (* The weights currently returned by "mash.py" are too extreme to |
628 (* The weights currently returned by "mash.py" are too extreme to |
619 make any sense. *) |
629 make any sense. *) |
620 |> map fst |> weight_mepo_facts |
630 |> map fst |> weight_mepo_facts |
654 let |
664 let |
655 val thy = Proof_Context.theory_of ctxt |
665 val thy = Proof_Context.theory_of ctxt |
656 val name = freshish_name () |
666 val name = freshish_name () |
657 val feats = features_of ctxt prover thy (Local, General) [t] |
667 val feats = features_of ctxt prover thy (Local, General) [t] |
658 val deps = used_ths |> map nickname_of |
668 val deps = used_ths |> map nickname_of |
659 val {fact_G} = mash_get ctxt |
|
660 val parents = maximal_in_graph fact_G facts |
|
661 in |
669 in |
662 mash_ADD ctxt overlord [(name, parents, feats, deps)]; (true, "") |
670 mash_peek ctxt (fn {fact_G} => |
|
671 let val parents = maximal_in_graph fact_G facts in |
|
672 mash_ADD ctxt overlord [(name, parents, feats, deps)] |
|
673 end); |
|
674 (true, "") |
663 end) |
675 end) |
664 |
676 |
665 fun sendback sub = |
677 fun sendback sub = |
666 Markup.markup Isabelle_Markup.sendback (sledgehammerN ^ " " ^ sub) |
678 Markup.markup Isabelle_Markup.sendback (sledgehammerN ^ " " ^ sub) |
667 |
679 |