minor refactoring
authorblanchet
Wed Sep 01 23:10:01 2010 +0200 (2010-09-01)
changeset 3900542fcb25de082
parent 39004 f1b465f889b5
child 39006 a02cb5717677
minor refactoring
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Tools/Sledgehammer/sledgehammer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Sep 01 23:04:47 2010 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Sep 01 23:10:01 2010 +0200
     1.3 @@ -321,8 +321,7 @@
     1.4            relevance_override chained_ths hyp_ts concl_t
     1.5      val problem =
     1.6        {ctxt = ctxt', goal = goal, subgoal = i,
     1.7 -       axiom_ts = map (prop_of o snd) axioms,
     1.8 -       prepared_axioms = map (Sledgehammer_Translate.prepare_axiom ctxt) axioms}
     1.9 +       axioms = map (Sledgehammer_Translate.prepare_axiom ctxt) axioms}
    1.10      val time_limit =
    1.11        (case hard_timeout of
    1.12          NONE => I
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Sep 01 23:04:47 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Sep 01 23:10:01 2010 +0200
     2.3 @@ -31,8 +31,7 @@
     2.4      {ctxt: Proof.context,
     2.5       goal: thm,
     2.6       subgoal: int,
     2.7 -     axiom_ts: term list,
     2.8 -     prepared_axioms: ((string * locality) * fol_formula) option list}
     2.9 +     axioms: (term * ((string * locality) * fol_formula) option) list}
    2.10    type prover_result =
    2.11      {outcome: failure option,
    2.12       message: string,
    2.13 @@ -101,8 +100,7 @@
    2.14    {ctxt: Proof.context,
    2.15     goal: thm,
    2.16     subgoal: int,
    2.17 -   axiom_ts: term list,
    2.18 -   prepared_axioms: ((string * locality) * fol_formula) option list}
    2.19 +   axioms: (term * ((string * locality) * fol_formula) option) list}
    2.20  
    2.21  type prover_result =
    2.22    {outcome: failure option,
    2.23 @@ -220,13 +218,11 @@
    2.24           use_conjecture_for_hypotheses}
    2.25          ({debug, verbose, overlord, full_types, explicit_apply,
    2.26            max_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params)
    2.27 -        minimize_command
    2.28 -        ({ctxt, goal, subgoal, axiom_ts, prepared_axioms} : problem) =
    2.29 +        minimize_command ({ctxt, goal, subgoal, axioms} : problem) =
    2.30    let
    2.31      val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
    2.32      val max_relevant = the_default default_max_relevant max_relevant
    2.33 -    val axiom_ts = take max_relevant axiom_ts
    2.34 -    val prepared_axioms = take max_relevant prepared_axioms
    2.35 +    val axioms = take max_relevant axioms
    2.36      (* path to unique problem file *)
    2.37      val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
    2.38                         else Config.get ctxt dest_dir
    2.39 @@ -288,8 +284,7 @@
    2.40              val readable_names = debug andalso overlord
    2.41              val (problem, pool, conjecture_offset, axiom_names) =
    2.42                prepare_problem ctxt readable_names explicit_forall full_types
    2.43 -                              explicit_apply hyp_ts concl_t axiom_ts
    2.44 -                              prepared_axioms
    2.45 +                              explicit_apply hyp_ts concl_t axioms
    2.46              val ss = strings_for_tptp_problem use_conjecture_for_hypotheses
    2.47                                                problem
    2.48              val _ = File.write_list probfile ss
    2.49 @@ -368,8 +363,7 @@
    2.50        let
    2.51          val problem =
    2.52            {ctxt = ctxt, goal = goal, subgoal = i,
    2.53 -           axiom_ts = map (prop_of o snd) axioms,
    2.54 -           prepared_axioms = map (prepare_axiom ctxt) axioms}
    2.55 +           axioms = map (prepare_axiom ctxt) axioms}
    2.56          val (outcome_code, message) =
    2.57            prover_fun atp_name prover params (minimize_command atp_name) problem
    2.58            |> (fn {outcome, message, ...} =>
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Sep 01 23:04:47 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Sep 01 23:10:01 2010 +0200
     3.3 @@ -60,8 +60,7 @@
     3.4      val {context = ctxt, goal, ...} = Proof.goal state
     3.5      val problem =
     3.6        {ctxt = ctxt, goal = goal, subgoal = subgoal,
     3.7 -       axiom_ts = map (prop_of o snd) axioms,
     3.8 -       prepared_axioms = map (prepare_axiom ctxt) axioms}
     3.9 +       axioms = map (prepare_axiom ctxt) axioms}
    3.10      val result as {outcome, used_thm_names, ...} = prover params (K "") problem
    3.11    in
    3.12      priority (case outcome of
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Wed Sep 01 23:04:47 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Wed Sep 01 23:10:01 2010 +0200
     4.3 @@ -18,10 +18,11 @@
     4.4    val arity_clause_prefix : string
     4.5    val tfrees_name : string
     4.6    val prepare_axiom :
     4.7 -    Proof.context -> (string * 'a) * thm -> ((string * 'a) * fol_formula) option
     4.8 +    Proof.context -> (string * 'a) * thm
     4.9 +    -> term * ((string * 'a) * fol_formula) option
    4.10    val prepare_problem :
    4.11      Proof.context -> bool -> bool -> bool -> bool -> term list -> term
    4.12 -    -> term list -> ((string * 'a) * fol_formula) option list
    4.13 +    -> (term * ((string * 'a) * fol_formula) option) list
    4.14      -> string problem * string Symtab.table * int * (string * 'a) list vector
    4.15  end;
    4.16  
    4.17 @@ -249,15 +250,15 @@
    4.18      |> map_filter (Option.map snd o make_axiom ctxt false)
    4.19    end
    4.20  
    4.21 -fun prepare_axiom ctxt = make_axiom ctxt true
    4.22 +fun prepare_axiom ctxt (ax as (_, th)) = (prop_of th, make_axiom ctxt true ax)
    4.23  
    4.24 -fun prepare_formulas ctxt full_types hyp_ts concl_t axiom_ts prepared_axioms =
    4.25 +fun prepare_formulas ctxt full_types hyp_ts concl_t axioms =
    4.26    let
    4.27      val thy = ProofContext.theory_of ctxt
    4.28 -    val hyp_ts =
    4.29 -      (* Remove existing axioms from the conjecture, as this can dramatically
    4.30 -         boost an ATP's performance (for some reason). *)
    4.31 -      hyp_ts |> filter_out (member (op aconv) axiom_ts)
    4.32 +    val (axiom_ts, prepared_axioms) = ListPair.unzip axioms
    4.33 +    (* Remove existing axioms from the conjecture, as this can dramatically
    4.34 +       boost an ATP's performance (for some reason). *)
    4.35 +    val hyp_ts = hyp_ts |> filter_out (member (op aconv) axiom_ts)
    4.36      val goal_t = Logic.list_implies (hyp_ts, concl_t)
    4.37      val is_FO = Meson.is_fol_term thy goal_t
    4.38      val subs = tfree_classes_of_terms [goal_t]
    4.39 @@ -498,12 +499,12 @@
    4.40        (const_table_for_problem explicit_apply problem) problem
    4.41  
    4.42  fun prepare_problem ctxt readable_names explicit_forall full_types
    4.43 -                    explicit_apply hyp_ts concl_t axiom_ts prepared_axioms =
    4.44 +                    explicit_apply hyp_ts concl_t axioms =
    4.45    let
    4.46      val thy = ProofContext.theory_of ctxt
    4.47      val (axiom_names, (conjectures, axioms, helper_facts, class_rel_clauses,
    4.48                         arity_clauses)) =
    4.49 -      prepare_formulas ctxt full_types hyp_ts concl_t axiom_ts prepared_axioms
    4.50 +      prepare_formulas ctxt full_types hyp_ts concl_t axioms
    4.51      val axiom_lines = map (problem_line_for_fact axiom_prefix full_types) axioms
    4.52      val helper_lines =
    4.53        map (problem_line_for_fact helper_prefix full_types) helper_facts