# HG changeset patch # User blanchet # Date 1306852716 -7200 # Node ID 0a97f32956425d4f0662e63116893507ea6844da # Parent b870759ce0f3972700b11973a84110a908fbc2c4 compile diff -r b870759ce0f3 -r 0a97f3295642 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue May 31 16:38:36 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue May 31 16:38:36 2011 +0200 @@ -335,7 +335,7 @@ | NONE => get_prover (default_prover_name ())) end -type locality = Sledgehammer_Filter.locality +type locality = ATP_Translate.locality (* hack *) fun reconstructor_from_msg args msg = @@ -361,7 +361,7 @@ fun change_dir (SOME dir) = Config.put Sledgehammer_Provers.dest_dir dir #> Config.put SMT_Config.debug_files - (dir ^ "/" ^ Name.desymbolize false (ATP_Problem.timestamp ()) ^ "_" + (dir ^ "/" ^ Name.desymbolize false (ATP_Util.timestamp ()) ^ "_" ^ serial_string ()) | change_dir NONE = I val st' = @@ -391,14 +391,14 @@ val relevance_fudge = Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover_name val relevance_override = {add = [], del = [], only = false} - val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal ctxt goal i + val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i val time_limit = (case hard_timeout of NONE => I | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs)) fun failed failure = ({outcome = SOME failure, used_facts = [], run_time_in_msecs = NONE, - preplay = K Sledgehammer_ATP_Reconstruct.Failed_to_Play, + preplay = K ATP_Reconstruct.Failed_to_Play, message = K ""}, ~1) val ({outcome, used_facts, run_time_in_msecs, preplay, message} : Sledgehammer_Provers.prover_result, @@ -469,7 +469,7 @@ case result of SH_OK (time_isa, time_prover, names) => let - fun get_thms (_, Sledgehammer_Filter.Chained) = NONE + fun get_thms (_, ATP_Translate.Chained) = NONE | get_thms (name, loc) = SOME ((name, loc), thms_of_name (Proof.context_of st) name) in diff -r b870759ce0f3 -r 0a97f3295642 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Tue May 31 16:38:36 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Tue May 31 16:38:36 2011 +0200 @@ -128,8 +128,7 @@ (Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover) val relevance_override = {add = [], del = [], only = false} val subgoal = 1 - val (_, hyp_ts, concl_t) = - Sledgehammer_Util.strip_subgoal ctxt goal subgoal + val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal subgoal val facts = Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds (the_default default_max_relevant max_relevant) diff -r b870759ce0f3 -r 0a97f3295642 src/HOL/ex/sledgehammer_tactics.ML --- a/src/HOL/ex/sledgehammer_tactics.ML Tue May 31 16:38:36 2011 +0200 +++ b/src/HOL/ex/sledgehammer_tactics.ML Tue May 31 16:38:36 2011 +0200 @@ -32,7 +32,7 @@ val relevance_fudge = Sledgehammer_Provers.relevance_fudge_for_prover ctxt name val relevance_override = {add = [], del = [], only = false} - val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal ctxt goal i + val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i val facts = Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds (the_default default_max_relevant max_relevant) (K true) diff -r b870759ce0f3 -r 0a97f3295642 src/HOL/ex/tptp_export.ML --- a/src/HOL/ex/tptp_export.ML Tue May 31 16:38:36 2011 +0200 +++ b/src/HOL/ex/tptp_export.ML Tue May 31 16:38:36 2011 +0200 @@ -17,9 +17,9 @@ structure TPTP_Export : TPTP_EXPORT = struct -val ascii_of = Metis_Translate.ascii_of +val ascii_of = ATP_Translate.ascii_of -val fact_name_of = prefix Sledgehammer_ATP_Translate.fact_prefix o ascii_of +val fact_name_of = prefix ATP_Translate.fact_prefix o ascii_of fun facts_of thy = Sledgehammer_Filter.all_facts (ProofContext.init_global thy) Symtab.empty @@ -60,9 +60,9 @@ val s = "[" ^ Thm.legacy_get_kind thm ^ "] " ^ (if member (op =) axioms name then "A" else "T") ^ " " ^ - prefix Sledgehammer_ATP_Translate.fact_prefix (ascii_of name) ^ ": " ^ + prefix ATP_Translate.fact_prefix (ascii_of name) ^ ": " ^ commas (theorems_mentioned_in_proof_term thm) ^ "; " ^ - commas (map (prefix Metis_Translate.const_prefix o ascii_of) + commas (map (prefix ATP_Translate.const_prefix o ascii_of) (interesting_const_names ctxt (Thm.prop_of thm))) ^ " \n" in File.append path s end val thms = facts_of thy |> map (snd o snd) @@ -91,21 +91,21 @@ let val format = ATP_Problem.FOF val type_sys = - Sledgehammer_ATP_Translate.Preds - (Sledgehammer_ATP_Translate.Polymorphic, - if full_types then Sledgehammer_ATP_Translate.All_Types - else Sledgehammer_ATP_Translate.Const_Arg_Types, - Sledgehammer_ATP_Translate.Heavy) + ATP_Translate.Preds + (ATP_Translate.Polymorphic, + if full_types then ATP_Translate.All_Types + else ATP_Translate.Const_Arg_Types, + ATP_Translate.Heavy) val path = file_name |> Path.explode val _ = File.write path "" val facts0 = facts_of thy val facts = facts0 |> map_filter (try (fn ((_, loc), (_, th)) => - Sledgehammer_ATP_Translate.translate_atp_fact ctxt format + ATP_Translate.translate_atp_fact ctxt format type_sys true ((Thm.get_name_hint th, loc), th))) val explicit_apply = NONE val (atp_problem, _, _, _, _, _, _) = - Sledgehammer_ATP_Translate.prepare_atp_problem ctxt format + ATP_Translate.prepare_atp_problem ctxt format ATP_Problem.Axiom ATP_Problem.Axiom type_sys explicit_apply [] @{prop False} facts val infers =