| author | wenzelm |
| Sat, 08 Dec 2012 22:41:39 +0100 | |
| changeset 50444 | f2241b8d0db5 |
| parent 50443 | b233d426fa0b (diff) |
| parent 50433 | 9131dadb2bf7 (current diff) |
| child 50445 | 68c9a6538c0e |
--- a/src/HOL/TPTP/MaSh_Eval.thy Sat Dec 08 22:19:24 2012 +0100 +++ b/src/HOL/TPTP/MaSh_Eval.thy Sat Dec 08 22:41:39 2012 +0100 @@ -28,6 +28,7 @@ ML {* if do_it then evaluate_mash_suggestions @{context} params "/tmp/mash_suggestions" + "/tmp/mash_eval.out" else () *}
--- a/src/HOL/TPTP/MaSh_Export.thy Sat Dec 08 22:19:24 2012 +0100 +++ b/src/HOL/TPTP/MaSh_Export.thy Sat Dec 08 22:41:39 2012 +0100 @@ -14,6 +14,8 @@ [provers = spass, max_relevant = 32, strict, dont_slice, type_enc = mono_native, lam_trans = combs_and_lifting, timeout = 2, dont_preplay, minimize] +declare [[sledgehammer_instantiate_inducts]] + ML {* open MaSh_Export *}
--- a/src/HOL/TPTP/atp_theory_export.ML Sat Dec 08 22:19:24 2012 +0100 +++ b/src/HOL/TPTP/atp_theory_export.ML Sat Dec 08 22:41:39 2012 +0100 @@ -123,7 +123,7 @@ val path = file_name |> Path.explode val _ = File.write path "" val facts = - Sledgehammer_Fact.all_facts (Proof_Context.init_global thy) false + Sledgehammer_Fact.all_facts (Proof_Context.init_global thy) true false Symtab.empty [] [] css_table val atp_problem = facts
--- a/src/HOL/TPTP/mash_eval.ML Sat Dec 08 22:19:24 2012 +0100 +++ b/src/HOL/TPTP/mash_eval.ML Sat Dec 08 22:41:39 2012 +0100 @@ -9,7 +9,8 @@ sig type params = Sledgehammer_Provers.params - val evaluate_mash_suggestions : Proof.context -> params -> string -> unit + val evaluate_mash_suggestions : + Proof.context -> params -> string -> string -> unit end; structure MaSh_Eval : MASH_EVAL = @@ -25,16 +26,19 @@ val all_names = map (rpair () o nickname_of) #> Symtab.make -fun evaluate_mash_suggestions ctxt params file_name = +fun evaluate_mash_suggestions ctxt params sugg_file_name out_file_name = let + val out_path = out_file_name |> Path.explode + val _ = File.write out_path "" + fun print s = (tracing s; File.append out_path (s ^ "\n")) val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} = Sledgehammer_Isar.default_params ctxt [] val prover = hd provers val slack_max_facts = generous_max_facts (the max_facts) - val path = file_name |> Path.explode - val lines = path |> File.read_lines + val sugg_path = sugg_file_name |> Path.explode + val lines = sugg_path |> File.read_lines val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt - val facts = all_facts ctxt false Symtab.empty [] [] css + val facts = all_facts ctxt true false Symtab.empty [] [] css val all_names = all_names (facts |> map snd) val mepo_ok = Unsynchronized.ref 0 val mash_ok = Unsynchronized.ref 0 @@ -42,7 +46,8 @@ val isar_ok = Unsynchronized.ref 0 fun with_index facts s = (find_index (curry (op =) s) facts + 1, s) fun index_string (j, s) = s ^ "@" ^ string_of_int j - fun str_of_res label facts ({outcome, run_time, used_facts, ...}: Sledgehammer_Provers.prover_result) = + fun str_of_res label facts ({outcome, run_time, used_facts, ...} + : Sledgehammer_Provers.prover_result) = let val facts = facts |> map (fn ((name, _), _) => name ()) in " " ^ label ^ ": " ^ (if is_none outcome then @@ -76,10 +81,10 @@ Sledgehammer_MePo.mepo_suggested_facts ctxt params prover slack_max_facts NONE hyp_ts concl_t facts |> Sledgehammer_MePo.weight_mepo_facts - val mash_facts = + val (mash_facts, mash_unks) = find_mash_suggestions slack_max_facts suggs facts [] [] - |> weight_mash_facts - val mess = [(0.5, (mepo_facts, [])), (0.5, (mash_facts, []))] + |>> weight_mash_facts + val mess = [(0.5, (mepo_facts, [])), (0.5, (mash_facts, mash_unks))] val mesh_facts = mesh_facts slack_max_facts mess val isar_facts = find_suggested_facts (map (rpair 1.0) isar_deps) facts fun prove ok heading get facts = @@ -93,14 +98,16 @@ run_prover_for_mash ctxt params prover facts goal val _ = if is_none outcome then ok := !ok + 1 else () in str_of_res heading facts res end - val mepo_s = prove mepo_ok MePoN fst mepo_facts - val mash_s = prove mash_ok MaShN fst mash_facts - val mesh_s = prove mesh_ok MeshN I mesh_facts - val isar_s = prove isar_ok IsarN fst isar_facts + val [mepo_s, mash_s, mesh_s, isar_s] = + [fn () => prove mepo_ok MePoN fst mepo_facts, + fn () => prove mash_ok MaShN fst mash_facts, + fn () => prove mesh_ok MeshN I mesh_facts, + fn () => prove isar_ok IsarN fst isar_facts] + |> map (fn f => f ()) in ["Goal " ^ string_of_int j ^ ": " ^ name, mepo_s, mash_s, mesh_s, isar_s] - |> cat_lines |> tracing + |> cat_lines |> print end fun total_of heading ok n = " " ^ heading ^ ": " ^ string_of_int (!ok) ^ " (" ^ @@ -114,15 +121,15 @@ "instantiate_inducts" |> not inst_inducts ? prefix "dont_"] val n = length lines in - tracing " * * *"; - tracing ("Options: " ^ commas options); + print " * * *"; + print ("Options: " ^ commas options); List.app solve_goal (tag_list 1 lines); ["Successes (of " ^ string_of_int n ^ " goals)", total_of MePoN mepo_ok n, total_of MaShN mash_ok n, total_of MeshN mesh_ok n, total_of IsarN isar_ok n] - |> cat_lines |> tracing + |> cat_lines |> print end end;
--- a/src/HOL/TPTP/mash_export.ML Sat Dec 08 22:19:24 2012 +0100 +++ b/src/HOL/TPTP/mash_export.ML Sat Dec 08 22:41:39 2012 +0100 @@ -28,7 +28,6 @@ structure MaSh_Export : MASH_EXPORT = struct -open Sledgehammer_Fact open Sledgehammer_MePo open Sledgehammer_MaSh @@ -45,8 +44,7 @@ fun all_facts ctxt = let val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt in - nearly_all_facts ctxt false no_fact_override Symtab.empty css [] [] - @{prop True} + Sledgehammer_Fact.all_facts ctxt true false Symtab.empty [] [] css end fun add_thy_parent_facts thy_map thy =
--- a/src/HOL/Tools/Sledgehammer/MaSh/src/mash.py Sat Dec 08 22:19:24 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/MaSh/src/mash.py Sat Dec 08 22:41:39 2012 +0100 @@ -29,8 +29,8 @@ parser = ArgumentParser(description='MaSh - Machine Learning for Sledgehammer. \n\n\ MaSh allows to use different machine learning algorithms to predict relevant facts for Sledgehammer.\n\n\ --------------- Example Usage ---------------\n\ -First initialize:\n./mash.py -l test.log -o ../tmp/ --init --inputDir ../data/Nat/ \n\ -Then create predictions:\n./mash.py -i ../data/Nat/mash_commands -p ../tmp/test.pred -l test.log -o ../tmp/ --statistics\n\ +First initialize:\n./mash.py -l test.log -o ../tmp/ --init --inputDir ../data/Jinja/ \n\ +Then create predictions:\n./mash.py -i ../data/Jinja/mash_commands -p ../data/Jinja/mash_suggestions -l test.log -o ../tmp/ --statistics\n\ \n\n\ Author: Daniel Kuehlwein, July 2012',formatter_class=RawDescriptionHelpFormatter) parser.add_argument('-i','--inputFile',help='File containing all problems to be solved.') @@ -40,7 +40,7 @@ parser.add_argument('--numberOfPredictions',default=200,help="Number of premises to write in the output. Default=200.",type=int) parser.add_argument('--init',default=False,action='store_true',help="Initialize Mash. Requires --inputDir to be defined. Default=False.") -parser.add_argument('--inputDir',default='../data/Nat/',\ +parser.add_argument('--inputDir',default='../data/Jinja/',\ help='Directory containing all the input data. MaSh expects the following files: mash_features,mash_dependencies,mash_accessibility') parser.add_argument('--depFile', default='mash_dependencies', help='Name of the file with the premise dependencies. The file must be in inputDir. Default = mash_dependencies') @@ -82,7 +82,7 @@ logger.info('Using the following settings: %s',args) # Pick algorithm if args.nb: - logger.info('Using Naive Bayes for learning.') + logger.info('Using sparse Naive Bayes for learning.') model = NBClassifier() modelFile = os.path.join(args.outputDir,'NB.pickle') elif args.snow: @@ -96,7 +96,7 @@ model = Predefined(predictionFile) modelFile = os.path.join(args.outputDir,'mepo.pickle') else: - logger.info('No algorithm specified. Using Naive Bayes.') + logger.info('No algorithm specified. Using sparse Naive Bayes.') model = NBClassifier() modelFile = os.path.join(args.outputDir,'NB.pickle') dictsFile = os.path.join(args.outputDir,'dicts.pickle') @@ -113,7 +113,7 @@ # Create Model trainData = dicts.featureDict.keys() if args.predef: - dicts = model.initializeModel(trainData,dicts) + model.initializeModel(trainData,dicts) else: model.initializeModel(trainData,dicts) @@ -135,7 +135,7 @@ model.load(modelFile) # IO Streams - OS = open(args.predictions,'a') + OS = open(args.predictions,'w') IS = open(args.inputFile,'r') # Statistics @@ -148,7 +148,7 @@ # try: if True: if line.startswith('!'): - problemId = dicts.parse_fact(line) + problemId = dicts.parse_fact(line) # Statistics if args.statistics and computeStats: computeStats = False @@ -156,7 +156,10 @@ if args.predef: predictions = model.predict(problemId) else: - predictions,_predictionsValues = model.predict(dicts.featureDict[problemId],dicts.expand_accessibles(acc)) + if args.snow: + predictions,_predictionsValues = model.predict(dicts.featureDict[problemId],dicts.expand_accessibles(acc),dicts) + else: + predictions,_predictionsValues = model.predict(dicts.featureDict[problemId],dicts.expand_accessibles(acc)) stats.update(predictions,dicts.dependenciesDict[problemId],statementCounter) if not stats.badPreds == []: bp = string.join([str(dicts.idNameDict[x]) for x in stats.badPreds], ',') @@ -164,7 +167,10 @@ statementCounter += 1 # Update Dependencies, p proves p dicts.dependenciesDict[problemId] = [problemId]+dicts.dependenciesDict[problemId] - model.update(problemId,dicts.featureDict[problemId],dicts.dependenciesDict[problemId]) + if args.snow: + model.update(problemId,dicts.featureDict[problemId],dicts.dependenciesDict[problemId],dicts) + else: + model.update(problemId,dicts.featureDict[problemId],dicts.dependenciesDict[problemId]) elif line.startswith('p'): # Overwrite old proof. problemId,newDependencies = dicts.parse_overwrite(line) @@ -179,7 +185,10 @@ name,features,accessibles = dicts.parse_problem(line) # Create predictions logger.info('Starting computation for problem on line %s',lineCounter) - predictions,predictionValues = model.predict(features,accessibles) + if args.snow: + predictions,predictionValues = model.predict(features,accessibles,dicts) + else: + predictions,predictionValues = model.predict(features,accessibles) assert len(predictions) == len(predictionValues) logger.info('Done. %s seconds needed.',round(time()-startTime,2)) # Output @@ -217,11 +226,11 @@ if __name__ == '__main__': # Example: - # Nat - #args = ['-l','testIsabelle.log','-o','../tmp/','--statistics','--init','--inputDir','../data/Nat/','--predef'] - #args = ['-i', '../data/Nat/mash_commands','-p','../tmp/testIsabelle.pred','-l','testIsabelle.log','--predef','-o','../tmp/','--statistics','--saveStats','../tmp/natATPMP.stats'] - #args = ['-l','testNB.log','-o','../tmp/','--statistics','--init','--inputDir','../data/Nat/'] - #args = ['-i', '../data/Nat/mash_commands','-p','../tmp/testNB.pred','-l','../tmp/testNB.log','--nb','-o','../tmp/','--statistics','--saveStats','../tmp/natATPNB.stats','--cutOff','500'] + # Jinja + #args = ['-l','testIsabelle.log','-o','../tmp/','--statistics','--init','--inputDir','../data/Jinja/','--predef'] + #args = ['-i', '../data/Jinja/mash_commands','-p','../tmp/testIsabelle.pred','-l','testIsabelle.log','--predef','-o','../tmp/','--statistics','--saveStats','../tmp/natATPMP.stats'] + #args = ['-l','testNB.log','-o','../tmp/','--statistics','--init','--inputDir','../data/Jinja/'] + #args = ['-i', '../data/Jinja/mash_commands','-p','../tmp/testNB.pred','-l','../tmp/testNB.log','--nb','-o','../tmp/','--statistics','--saveStats','../tmp/natATPNB.stats','--cutOff','500'] # List #args = ['-l','testIsabelle.log','-o','../tmp/','--statistics','--init','--inputDir','../data/List/','--isabelle'] #args = ['-i', '../data/List/mash_commands','-p','../tmp/testIsabelle.pred','-l','testIsabelle.log','--isabelle','-o','../tmp/','--statistics'] @@ -229,17 +238,23 @@ #args = ['-l','testNB.log','-o','../tmp/','--statistics','--init','--inputDir','../data/Huffman/','--depFile','mash_atp_dependencies'] #args = ['-l','testNB.log','-o','../tmp/','--statistics','--init','--inputDir','../data/Huffman/'] #args = ['-i', '../data/Huffman/mash_commands','-p','../tmp/testNB.pred','-l','testNB.log','--nb','-o','../tmp/','--statistics'] - # Arrow - #args = ['-l','testNB.log','-o','../tmp/','--statistics','--init','--inputDir','../data/Arrow_Order/'] - #args = ['-i', '../data/Arrow_Order/mash_commands','-p','../tmp/testNB.pred','-l','../tmp/testNB.log','--nb','-o','../tmp/','--statistics','--saveStats','../tmp/arrowIsarNB.stats','--cutOff','500'] - # Fundamental_Theorem_Algebra - #args = ['-l','testNB.log','-o','../tmp/','--statistics','--init','--inputDir','../data/Fundamental_Theorem_Algebra/'] - #args = ['-i', '../data/Fundamental_Theorem_Algebra/mash_commands','-p','../tmp/testNB.pred','-l','../tmp/testNB.log','--nb','-o','../tmp/','--statistics','--saveStats','../tmp/Fundamental_Theorem_AlgebraIsarNB.stats','--cutOff','500'] - #args = ['-l','testIsabelle.log','-o','../tmp/','--statistics','--init','--inputDir','../data/Fundamental_Theorem_Algebra/','--predef'] - #args = ['-i', '../data/Fundamental_Theorem_Algebra/mash_commands','-p','../tmp/Fundamental_Theorem_AlgebraMePo.pred','-l','testIsabelle.log','--predef','-o','../tmp/','--statistics','--saveStats','../tmp/Fundamental_Theorem_AlgebraMePo.stats'] # Jinja + # ISAR #args = ['-l','testNB.log','-o','../tmp/','--statistics','--init','--inputDir','../data/Jinja/'] #args = ['-i', '../data/Jinja/mash_commands','-p','../tmp/testNB.pred','-l','../tmp/testNB.log','--nb','-o','../tmp/','--statistics','--saveStats','../tmp/JinjaIsarNB.stats','--cutOff','500'] + #args = ['-l','testIsabelle.log','-o','../tmp/','--statistics','--init','--inputDir','../data/Jinja/','--predef'] + #args = ['-i', '../data/Jinja/mash_commands','-p','../tmp/JinjaMePo.pred','-l','testIsabelle.log','--predef','-o','../tmp/','--statistics','--saveStats','../tmp/JinjaMePo.stats'] + #args = ['-l','testNB.log','-o','../tmp/','--statistics','--init','--inputDir','../data/Jinja/','--depFile','mash_atp_dependencies','--snow'] + #args = ['-i', '../data/Jinja/mash_commands','-p','../tmp/testNB.pred','-l','../tmp/testNB.log','--nb','-o','../tmp/','--statistics','--saveStats','../tmp/JinjaIsarNB.stats','--cutOff','500','--depFile','mash_atp_dependencies'] + + # ATP + #args = ['-l','testNB.log','-o','../tmp/','--statistics','--init','--inputDir','../data/Jinja/','--depFile','mash_atp_dependencies'] + #args = ['-i', '../data/Jinja/mash_commands','-p','../tmp/testNB.pred','-l','../tmp/testNB.log','--nb','-o','../tmp/','--statistics','--saveStats','../tmp/JinjaIsarNB.stats','--cutOff','500','--depFile','mash_atp_dependencies'] + #args = ['-l','testIsabelle.log','-o','../tmp/','--statistics','--init','--inputDir','../data/Jinja/','--predef','--depFile','mash_atp_dependencies'] + #args = ['-i', '../data/Jinja/mash_commands','-p','../tmp/JinjaMePo.pred','-l','testIsabelle.log','--predef','-o','../tmp/','--statistics','--saveStats','../tmp/JinjaMePo.stats','--depFile','mash_atp_dependencies'] + #args = ['-l','testNB.log','-o','../tmp/','--statistics','--init','--inputDir','../data/Jinja/','--depFile','mash_atp_dependencies','--snow'] + #args = ['-i', '../data/Jinja/mash_commands','-p','../tmp/testNB.pred','-l','../tmp/testNB.log','--snow','-o','../tmp/','--statistics','--saveStats','../tmp/JinjaIsarNB.stats','--cutOff','500','--depFile','mash_atp_dependencies'] + #startTime = time()
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Sat Dec 08 22:19:24 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Sat Dec 08 22:41:39 2012 +0100 @@ -30,7 +30,7 @@ -> (((unit -> string) * 'a) * thm) list val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list val all_facts : - Proof.context -> bool -> unit Symtab.table -> thm list -> thm list + Proof.context -> bool -> bool -> unit Symtab.table -> thm list -> thm list -> status Termtab.table -> fact list val nearly_all_facts : Proof.context -> bool -> fact_override -> unit Symtab.table @@ -145,7 +145,7 @@ (* FIXME: put other record thms here, or declare as "no_atp" *) fun multi_base_blacklist ctxt ho_atp = ["defs", "select_defs", "update_defs", "split", "splits", "split_asm", - "cases", "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong", + "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong", "weak_case_cong", "nibble_pair_of_char_simps", "nibble.simps", "nibble.distinct"] |> not (ho_atp orelse (Config.get ctxt instantiate_inducts)) ? @@ -370,7 +370,7 @@ fun maybe_filter_no_atps ctxt = not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd) -fun all_facts ctxt ho_atp reserved add_ths chained css = +fun all_facts ctxt really_all ho_atp reserved add_ths chained css = let val thy = Proof_Context.theory_of ctxt val global_facts = Global_Theory.facts_of thy @@ -387,14 +387,15 @@ Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts) fun add_facts global foldx facts = foldx (fn (name0, ths) => - if name0 <> "" andalso + if not really_all andalso + name0 <> "" andalso forall (not o member Thm.eq_thm_prop add_ths) ths andalso (Facts.is_concealed facts name0 orelse not (can (Proof_Context.get_thms ctxt) name0) orelse (not (Config.get ctxt ignore_no_atp) andalso is_package_def name0) orelse exists (fn s => String.isSuffix s name0) - (multi_base_blacklist ctxt ho_atp)) then + (multi_base_blacklist ctxt ho_atp)) then I else let @@ -453,7 +454,7 @@ o fact_from_ref ctxt reserved chained css) add else let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in - all_facts ctxt ho_atp reserved add chained css + all_facts ctxt false ho_atp reserved add chained css |> filter_out (member Thm.eq_thm_prop del o snd) |> maybe_filter_no_atps ctxt |> uniquify
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sat Dec 08 22:19:24 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sat Dec 08 22:41:39 2012 +0100 @@ -61,10 +61,10 @@ val weight_mash_facts : ('a * thm) list -> (('a * thm) * real) list val find_mash_suggestions : int -> (Symtab.key * 'a) list -> ('b * thm) list -> ('b * thm) list - -> ('b * thm) list -> ('b * thm) list + -> ('b * thm) list -> ('b * thm) list * ('b * thm) list val mash_suggested_facts : Proof.context -> params -> string -> int -> term list -> term -> fact list - -> fact list + -> fact list * fact list val mash_learn_proof : Proof.context -> params -> string -> term -> ('a * thm) list -> thm list -> unit @@ -451,7 +451,7 @@ in case find_index (curry fact_eq fact o fst) sels of ~1 => (case find_index (curry fact_eq fact) unks of - ~1 => score_at sel_len + ~1 => score_at (sel_len - 1) | _ => NONE) | rank => score_at rank end @@ -465,8 +465,8 @@ end fun thy_feature_of s = ("y" ^ s, 0.5 (* FUDGE *)) -fun const_feature_of s = ("c" ^ s, 1.0 (* FUDGE *)) -fun free_feature_of s = ("f" ^ s, 2.0 (* FUDGE *)) +fun const_feature_of s = ("c" ^ s, 4.0 (* FUDGE *)) +fun free_feature_of s = ("f" ^ s, 5.0 (* FUDGE *)) fun type_feature_of s = ("t" ^ s, 0.5 (* FUDGE *)) fun class_feature_of s = ("s" ^ s, 0.25 (* FUDGE *)) fun status_feature_of status = (string_of_status status, 0.5 (* FUDGE *)) @@ -593,9 +593,9 @@ |> exists (exists_Const is_exists) ts ? cons skos_feature end -(* Too many dependencies is a sign that a crazy decision procedure is at work. - There isn't much to learn from such proofs. *) -val max_dependencies = 10 +(* Too many dependencies is a sign that a decision procedure is at work. There + isn't much to learn from such proofs. *) +val max_dependencies = 20 val atp_dependency_default_max_facts = 50 (* "type_definition_xxx" facts are characterized by their use of "CollectI". *) @@ -722,9 +722,6 @@ fun is_fact_in_graph fact_G (_, th) = can (Graph.get_node fact_G) (nickname_of th) -(* factor that controls whether unknown global facts should be included *) -val include_unk_global_factor = 15 - (* use MePo weights for now *) val weight_raw_mash_facts = weight_mepo_facts val weight_mash_facts = weight_raw_mash_facts @@ -736,19 +733,26 @@ fun weight_proximity_facts facts = facts ~~ map weight_of_proximity_fact (0 upto length facts - 1) -fun find_mash_suggestions max_facts suggs facts chained unknown = +val max_proximity_facts = 100 + +fun find_mash_suggestions max_facts suggs facts chained raw_unknown = let val raw_mash = facts |> find_suggested_facts suggs (* The weights currently returned by "mash.py" are too spaced out to make any sense. *) |> map fst - val proximity = facts |> sort (thm_ord o pairself snd o swap) + val proximity = + facts |> sort (thm_ord o pairself snd o swap) + |> take max_proximity_facts val mess = - [(0.8000 (* FUDGE *), (map (rpair 1.0) chained, [])), - (0.1333 (* FUDGE *), (weight_raw_mash_facts raw_mash, unknown)), - (0.0667 (* FUDGE *), (weight_proximity_facts proximity, []))] - in mesh_facts max_facts mess end + [(0.80 (* FUDGE *), (map (rpair 1.0) chained, [])), + (0.16 (* FUDGE *), (weight_raw_mash_facts raw_mash, raw_unknown)), + (0.04 (* FUDGE *), (weight_proximity_facts proximity, []))] + val unknown = + raw_unknown + |> fold (subtract (Thm.eq_thm_prop o pairself snd)) [chained, proximity] + in (mesh_facts max_facts mess, unknown) end fun mash_suggested_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts concl_t facts = @@ -1069,10 +1073,10 @@ fun mash () = mash_suggested_facts ctxt params prover (generous_max_facts max_facts) hyp_ts concl_t facts - |> weight_mash_facts + |>> weight_mash_facts val mess = [] |> (if fact_filter <> mashN then cons (0.5, (mepo (), [])) else I) - |> (if fact_filter <> mepoN then cons (0.5, (mash (), [])) else I) + |> (if fact_filter <> mepoN then cons (0.5, (mash ())) else I) in mesh_facts max_facts mess |> not (null add_ths) ? prepend_facts add_ths