90 fun mash_state_dir () = |
90 fun mash_state_dir () = |
91 getenv "ISABELLE_HOME_USER" ^ "/mash" |
91 getenv "ISABELLE_HOME_USER" ^ "/mash" |
92 |> tap (Isabelle_System.mkdir o Path.explode) |
92 |> tap (Isabelle_System.mkdir o Path.explode) |
93 fun mash_state_path () = mash_state_dir () ^ "/state" |> Path.explode |
93 fun mash_state_path () = mash_state_dir () ^ "/state" |> Path.explode |
94 |
94 |
|
95 |
95 (*** Isabelle helpers ***) |
96 (*** Isabelle helpers ***) |
96 |
97 |
97 fun meta_char c = |
98 fun meta_char c = |
98 if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse |
99 if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse |
99 c = #")" orelse c = #"," then |
100 c = #")" orelse c = #"," then |
119 fun extract_query line = |
120 fun extract_query line = |
120 case space_explode ":" line of |
121 case space_explode ":" line of |
121 [goal_name, suggs] => (unescape_meta goal_name, unescape_metas suggs) |
122 [goal_name, suggs] => (unescape_meta goal_name, unescape_metas suggs) |
122 | _ => ("", []) |
123 | _ => ("", []) |
123 |
124 |
124 fun find_suggested facts sugg = |
125 fun suggested_facts suggs facts = |
125 find_first (fn (_, th) => Thm.get_name_hint th = sugg) facts |
126 let |
126 fun suggested_facts suggs facts = map_filter (find_suggested facts) suggs |
127 fun add_fact (fact as (_, th)) = Symtab.default (Thm.get_name_hint th, fact) |
|
128 val tab = Symtab.empty |> fold add_fact facts |
|
129 in map_filter (Symtab.lookup tab) suggs end |
127 |
130 |
128 (* Ad hoc score function roughly based on Blanchette's Ringberg 2011 data. *) |
131 (* Ad hoc score function roughly based on Blanchette's Ringberg 2011 data. *) |
129 fun score x = Math.pow (1.5, 15.5 - 0.05 * Real.fromInt x) + 15.0 |
132 fun score x = Math.pow (1.5, 15.5 - 0.05 * Real.fromInt x) + 15.0 |
130 |
133 |
131 fun sum_sq_avg [] = 0 |
134 fun sum_sq_avg [] = 0 |
452 fun mash_can_suggest_facts ctxt = |
455 fun mash_can_suggest_facts ctxt = |
453 not (Graph.is_empty (#fact_graph (mash_get ctxt))) |
456 not (Graph.is_empty (#fact_graph (mash_get ctxt))) |
454 |
457 |
455 fun parents_wrt_facts ctxt facts fact_graph = |
458 fun parents_wrt_facts ctxt facts fact_graph = |
456 let |
459 let |
457 val graph_facts = Symtab.make (map (rpair ()) (Graph.keys fact_graph)) |
460 val facts = [] |> fold (cons o Thm.get_name_hint o snd) facts |
458 val facts = |
461 val tab = Symtab.empty |> fold (fn name => Symtab.update (name, ())) facts |
459 try_graph ctxt "when computing ancestor facts" [] (fn () => |
462 val maxs = Graph.maximals fact_graph |
460 [] |> fold (cons o Thm.get_name_hint o snd) facts |
463 in |
461 |> filter (Symtab.defined graph_facts) |
464 if forall (Symtab.defined tab) maxs then |
462 |> Graph.all_preds fact_graph) |
465 maxs |
463 val facts = Symtab.empty |> fold (fn name => Symtab.update (name, ())) facts |
466 else |
464 in |
467 let |
465 try_graph ctxt "when computing parent facts" [] (fn () => |
468 val graph_facts = Symtab.make (map (rpair ()) (Graph.keys fact_graph)) |
466 fact_graph |> Graph.restrict (Symtab.defined facts) |> Graph.maximals) |
469 val ancestors = |
|
470 try_graph ctxt "when computing ancestor facts" [] (fn () => |
|
471 facts |> filter (Symtab.defined graph_facts) |
|
472 |> Graph.all_preds fact_graph) |
|
473 val ancestors = |
|
474 Symtab.empty |> fold (fn name => Symtab.update (name, ())) ancestors |
|
475 in |
|
476 try_graph ctxt "when computing parent facts" [] (fn () => |
|
477 fact_graph |> Graph.restrict (Symtab.defined ancestors) |
|
478 |> Graph.maximals) |
|
479 end |
467 end |
480 end |
468 |
481 |
469 (* Generate more suggestions than requested, because some might be thrown out |
482 (* Generate more suggestions than requested, because some might be thrown out |
470 later for various reasons and "meshing" gives better results with some |
483 later for various reasons and "meshing" gives better results with some |
471 slack. *) |
484 slack. *) |
475 can (Graph.get_node fact_graph) (Thm.get_name_hint th) |
488 can (Graph.get_node fact_graph) (Thm.get_name_hint th) |
476 |
489 |
477 fun mash_suggest_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts |
490 fun mash_suggest_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts |
478 concl_t facts = |
491 concl_t facts = |
479 let |
492 let |
|
493 val timer = Timer.startRealTimer () |
480 val thy = Proof_Context.theory_of ctxt |
494 val thy = Proof_Context.theory_of ctxt |
|
495 val _ = tracing ("A1: " ^ PolyML.makestring (Timer.checkRealTimer timer)) (*###*) |
481 val fact_graph = #fact_graph (mash_get ctxt) |
496 val fact_graph = #fact_graph (mash_get ctxt) |
|
497 val _ = tracing ("A2: " ^ PolyML.makestring (Timer.checkRealTimer timer)) (*###*) |
482 val parents = parents_wrt_facts ctxt facts fact_graph |
498 val parents = parents_wrt_facts ctxt facts fact_graph |
|
499 val _ = tracing ("A3: " ^ PolyML.makestring (Timer.checkRealTimer timer)) (*###*) |
483 val feats = features_of ctxt prover thy General (concl_t :: hyp_ts) |
500 val feats = features_of ctxt prover thy General (concl_t :: hyp_ts) |
|
501 val _ = tracing ("A4: " ^ PolyML.makestring (Timer.checkRealTimer timer)) (*###*) |
484 val suggs = |
502 val suggs = |
485 if Graph.is_empty fact_graph then [] |
503 if Graph.is_empty fact_graph then [] |
486 else mash_QUERY ctxt overlord (max_suggs_of max_facts) (parents, feats) |
504 else mash_QUERY ctxt overlord (max_suggs_of max_facts) (parents, feats) |
|
505 val _ = tracing ("A5: " ^ PolyML.makestring (Timer.checkRealTimer timer)) (*###*) |
487 val selected = facts |> suggested_facts suggs |
506 val selected = facts |> suggested_facts suggs |
|
507 val _ = tracing ("A6: " ^ PolyML.makestring (Timer.checkRealTimer timer)) (*###*) |
488 val unknown = facts |> filter_out (is_fact_in_graph fact_graph) |
508 val unknown = facts |> filter_out (is_fact_in_graph fact_graph) |
|
509 val _ = tracing ("END: " ^ PolyML.makestring (Timer.checkRealTimer timer)) (*###*) |
489 in (selected, unknown) end |
510 in (selected, unknown) end |
490 |
511 |
491 fun add_thys_for thy = |
512 fun add_thys_for thy = |
492 let fun add comp thy = Symtab.update (Context.theory_name thy, comp) in |
513 let fun add comp thy = Symtab.update (Context.theory_name thy, comp) in |
493 add false thy #> fold (add true) (Theory.ancestors_of thy) |
514 add false thy #> fold (add true) (Theory.ancestors_of thy) |