# HG changeset patch # User blanchet # Date 1342593843 -7200 # Node ID e5c5037a3104d7370730f658daaf31f2bb3625a6 # Parent 9910021c80a7c2f28864d8cd43a0440114f4a586 started implementing MaSh client-side I/O diff -r 9910021c80a7 -r e5c5037a3104 src/HOL/TPTP/ATP_Theory_Export.thy --- a/src/HOL/TPTP/ATP_Theory_Export.thy Wed Jul 18 08:44:03 2012 +0200 +++ b/src/HOL/TPTP/ATP_Theory_Export.thy Wed Jul 18 08:44:03 2012 +0200 @@ -5,7 +5,7 @@ header {* ATP Theory Exporter *} theory ATP_Theory_Export -imports Complex_Main +imports (* ### Complex_Main *) "~~/src/HOL/Sledgehammer2d" uses "atp_theory_export.ML" begin @@ -15,13 +15,22 @@ *} ML {* -val do_it = false; (* switch to "true" to generate the files *) -val thy = @{theory}; +val do_it = true; (* switch to "true" to generate the files *) +val thy = @{theory List}; val ctxt = @{context} *} ML {* if do_it then + "/tmp/axs_tc_native.dfg" + |> generate_atp_inference_file_for_theory ctxt thy (DFG Polymorphic) + "tc_native" +else + () +*} + +ML {* +if do_it then "/tmp/infs_poly_guards_query_query.tptp" |> generate_atp_inference_file_for_theory ctxt thy FOF "poly_guards_query_query" @@ -38,13 +47,4 @@ () *} -ML {* -if do_it then - "/tmp/axs_tc_native.dfg" - |> generate_atp_inference_file_for_theory ctxt thy (DFG Polymorphic) - "tc_native" -else - () -*} - end diff -r 9910021c80a7 -r e5c5037a3104 src/HOL/TPTP/MaSh_Eval.thy --- a/src/HOL/TPTP/MaSh_Eval.thy Wed Jul 18 08:44:03 2012 +0200 +++ b/src/HOL/TPTP/MaSh_Eval.thy Wed Jul 18 08:44:03 2012 +0200 @@ -5,7 +5,7 @@ header {* MaSh Evaluation Driver *} theory MaSh_Eval -imports Complex_Main +imports (* ### Complex_Main *) "~~/src/HOL/Sledgehammer2d" uses "mash_eval.ML" begin @@ -20,14 +20,14 @@ *} ML {* -val do_it = false (* switch to "true" to generate the files *); -val thy = @{theory List}; +val do_it = true (* switch to "true" to generate the files *); +val thy = @{theory Nat}; val params = Sledgehammer_Isar.default_params @{context} [] *} ML {* if do_it then - evaluate_mash_suggestions @{context} params thy "/tmp/mash_suggestions_list" + evaluate_mash_suggestions @{context} params thy "/Users/blanchet/tum/mash/mash/results/natNB200ATP-15.pred" else () *} diff -r 9910021c80a7 -r e5c5037a3104 src/HOL/TPTP/MaSh_Export.thy --- a/src/HOL/TPTP/MaSh_Export.thy Wed Jul 18 08:44:03 2012 +0200 +++ b/src/HOL/TPTP/MaSh_Export.thy Wed Jul 18 08:44:03 2012 +0200 @@ -5,7 +5,7 @@ header {* MaSh Exporter *} theory MaSh_Export -imports Complex_Main +imports (* ### Complex_Main *) "~~/src/HOL/Sledgehammer2d" uses "mash_export.ML" begin diff -r 9910021c80a7 -r e5c5037a3104 src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML Wed Jul 18 08:44:03 2012 +0200 +++ b/src/HOL/TPTP/atp_theory_export.ML Wed Jul 18 08:44:03 2012 +0200 @@ -50,7 +50,11 @@ let val thy = Proof_Context.theory_of ctxt val prob_file = File.tmp_path (Path.explode "prob") - val atp = case format of DFG _ => spassN | _ => eN + val atp = + case format of + DFG Polymorphic => spass_polyN + | DFG Monomorphic => spassN + | _ => eN val {exec, arguments, proof_delims, known_failures, ...} = get_atp thy atp () val ord = effective_term_order ctxt atp diff -r 9910021c80a7 -r e5c5037a3104 src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 18 08:44:03 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 18 08:44:03 2012 +0200 @@ -55,21 +55,27 @@ open Sledgehammer_Filter_Iter open Sledgehammer_Provers +val mash_dir = "mash" +val model_file = "model" +val state_file = "state" + +fun mash_path file = getenv "ISABELLE_HOME_USER" ^ "/" ^ mash_dir ^ "/" ^ file + (*** Low-level communication with MaSh ***) fun mash_RESET () = - tracing "MaSh RESET" + warning "MaSh RESET" -fun mash_ADD fact (access, feats, deps) = - tracing ("MaSh ADD " ^ fact ^ ": " ^ space_implode " " access ^ "; " ^ +fun mash_ADD fact access feats deps = + warning ("MaSh ADD " ^ fact ^ ": " ^ space_implode " " access ^ "; " ^ space_implode " " feats ^ "; " ^ space_implode " " deps) fun mash_DEL fact = - tracing ("MaSh DEL " ^ fact) + warning ("MaSh DEL " ^ fact) -fun mash_SUGGEST fact (access, feats) = - tracing ("MaSh SUGGEST " ^ fact ^ ": " ^ space_implode " " access ^ "; " ^ +fun mash_SUGGEST access feats = + warning ("MaSh SUGGEST " ^ space_implode " " access ^ "; " ^ space_implode " " feats) @@ -371,18 +377,82 @@ (*** High-level communication with MaSh ***) -fun mash_reset () = () +type mash_state = + {completed_thys : unit Symtab.table, + thy_facts : string list Symtab.table} + +val mash_zero = + {completed_thys = Symtab.empty, + thy_facts = Symtab.empty} + +local + +fun mash_load (state as (true, _)) = state + | mash_load _ = + (true, + case mash_path state_file |> Path.explode |> File.read_lines of + [] => mash_zero + | comp_line :: facts_lines => + let + fun comp_thys_of_line comp_line = + Symtab.make (comp_line |> space_explode " " |> map (rpair ())) + fun add_facts_line line = + case space_explode " " line of + thy :: facts => Symtab.update_new (thy, facts) + | _ => I (* shouldn't happen *) + in + {completed_thys = comp_thys_of_line comp_line, + thy_facts = fold add_facts_line facts_lines Symtab.empty} + end) -fun mash_can_suggest_facts () = true +fun mash_save ({completed_thys, thy_facts} : mash_state) = + let + val path = mash_path state_file |> Path.explode + val comp_line = (completed_thys |> Symtab.keys |> space_implode " ") ^ "\n" + fun fact_line_for (thy, facts) = space_implode " " (thy :: facts) ^ "\n" + in + File.write path comp_line; + Symtab.fold (fn thy_fact => fn () => + File.append path (fact_line_for thy_fact)) thy_facts + end + +val state = + Synchronized.var "Sledgehammer_Filter_MaSh.state" (false, mash_zero) + +in + +fun mash_change f = + Synchronized.change state (apsnd (tap mash_save o f) o mash_load) + +fun mash_value () = Synchronized.change_result state (`snd o mash_load) + +end + +fun mash_reset () = mash_change (fn _ => (mash_RESET (); mash_zero)) + +fun mash_can_suggest_facts () = + not (Symtab.is_empty (#thy_facts (mash_value ()))) fun mash_suggest_facts ctxt params prover max_facts hyp_ts concl_t facts = - (facts, []) + let + val access = [] + val feats = [] + val suggs = mash_SUGGEST access feats + in (facts, []) end -fun mash_can_learn_thy thy = true +fun mash_can_learn_thy thy = + not (Symtab.defined (#completed_thys (mash_value ())) + (Context.theory_name thy)) fun mash_learn_thy thy timeout = () fun mash_learn_proof thy t ths = () +(*### + let + in + mash_ADD + end +*) fun relevant_facts ctxt params prover max_facts ({add, only, ...} : fact_override) hyp_ts concl_t facts = diff -r 9910021c80a7 -r e5c5037a3104 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 18 08:44:03 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 18 08:44:03 2012 +0200 @@ -26,6 +26,7 @@ open Sledgehammer_Fact open Sledgehammer_Provers open Sledgehammer_Minimize +open Sledgehammer_Filter_MaSh open Sledgehammer_Run val runN = "run" @@ -35,6 +36,14 @@ val running_proversN = "running_provers" val kill_proversN = "kill_provers" val refresh_tptpN = "refresh_tptp" +val mash_resetN = "mash_reset" +val mash_learnN = "mash_learn" + +(* experimental *) +val mash_RESET_N = "mash_RESET" +val mash_ADD_N = "mash_ADD" +val mash_DEL_N = "mash_DEL" +val mash_SUGGEST_N = "mash_SUGGEST" val auto = Unsynchronized.ref false @@ -374,6 +383,18 @@ kill_provers () else if subcommand = refresh_tptpN then refresh_systems_on_tptp () + else if subcommand = mash_resetN then + mash_reset () + else if subcommand = mash_learnN then + () (* TODO: implement *) + else if subcommand = mash_RESET_N then + () (* TODO: implement *) + else if subcommand = mash_ADD_N then + () (* TODO: implement *) + else if subcommand = mash_DEL_N then + () (* TODO: implement *) + else if subcommand = mash_SUGGEST_N then + () (* TODO: implement *) else error ("Unknown subcommand: " ^ quote subcommand ^ ".") end