consider "locality" when assigning weights to facts
authorblanchet
Thu Aug 26 10:42:06 2010 +0200 (2010-08-26)
changeset 387526628adcae4a7
parent 38751 01c4d14b2a61
child 38753 3913f58d0fcc
consider "locality" when assigning weights to facts
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Tools/Sledgehammer/sledgehammer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Aug 26 09:23:21 2010 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Aug 26 10:42:06 2010 +0200
     1.3 @@ -290,10 +290,12 @@
     1.4      | NONE => get_prover (default_atp_name ()))
     1.5    end
     1.6  
     1.7 +type locality = Sledgehammer_Fact_Filter.locality
     1.8 +
     1.9  local
    1.10  
    1.11  datatype sh_result =
    1.12 -  SH_OK of int * int * (string * bool) list |
    1.13 +  SH_OK of int * int * (string * locality) list |
    1.14    SH_FAIL of int * int |
    1.15    SH_ERROR
    1.16  
    1.17 @@ -355,8 +357,8 @@
    1.18      case result of
    1.19        SH_OK (time_isa, time_atp, names) =>
    1.20          let
    1.21 -          fun get_thms (name, chained) =
    1.22 -            ((name, chained), thms_of_name (Proof.context_of st) name)
    1.23 +          fun get_thms (name, loc) =
    1.24 +            ((name, loc), thms_of_name (Proof.context_of st) name)
    1.25          in
    1.26            change_data id inc_sh_success;
    1.27            change_data id (inc_sh_lemmas (length names));
    1.28 @@ -445,7 +447,7 @@
    1.29      then () else
    1.30      let
    1.31        val named_thms =
    1.32 -        Unsynchronized.ref (NONE : ((string * bool) * thm list) list option)
    1.33 +        Unsynchronized.ref (NONE : ((string * locality) * thm list) list option)
    1.34        val minimize = AList.defined (op =) args minimizeK
    1.35        val metis_ft = AList.defined (op =) args metis_ftK
    1.36    
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Aug 26 09:23:21 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Aug 26 10:42:06 2010 +0200
     2.3 @@ -9,6 +9,7 @@
     2.4  signature SLEDGEHAMMER =
     2.5  sig
     2.6    type failure = ATP_Systems.failure
     2.7 +  type locality = Sledgehammer_Fact_Filter.locality
     2.8    type relevance_override = Sledgehammer_Fact_Filter.relevance_override
     2.9    type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command
    2.10    type params =
    2.11 @@ -28,16 +29,16 @@
    2.12      {subgoal: int,
    2.13       goal: Proof.context * (thm list * thm),
    2.14       relevance_override: relevance_override,
    2.15 -     axioms: ((string * bool) * thm) list option}
    2.16 +     axioms: ((string * locality) * thm) list option}
    2.17    type prover_result =
    2.18      {outcome: failure option,
    2.19       message: string,
    2.20       pool: string Symtab.table,
    2.21 -     used_thm_names: (string * bool) list,
    2.22 +     used_thm_names: (string * locality) list,
    2.23       atp_run_time_in_msecs: int,
    2.24       output: string,
    2.25       proof: string,
    2.26 -     axiom_names: (string * bool) vector,
    2.27 +     axiom_names: (string * locality) vector,
    2.28       conjecture_shape: int list list}
    2.29    type prover = params -> minimize_command -> problem -> prover_result
    2.30  
    2.31 @@ -96,17 +97,17 @@
    2.32    {subgoal: int,
    2.33     goal: Proof.context * (thm list * thm),
    2.34     relevance_override: relevance_override,
    2.35 -   axioms: ((string * bool) * thm) list option}
    2.36 +   axioms: ((string * locality) * thm) list option}
    2.37  
    2.38  type prover_result =
    2.39    {outcome: failure option,
    2.40     message: string,
    2.41     pool: string Symtab.table,
    2.42 -   used_thm_names: (string * bool) list,
    2.43 +   used_thm_names: (string * locality) list,
    2.44     atp_run_time_in_msecs: int,
    2.45     output: string,
    2.46     proof: string,
    2.47 -   axiom_names: (string * bool) vector,
    2.48 +   axiom_names: (string * locality) vector,
    2.49     conjecture_shape: int list list}
    2.50  
    2.51  type prover = params -> minimize_command -> problem -> prover_result
    2.52 @@ -193,8 +194,11 @@
    2.53            val axioms =
    2.54              j |> AList.lookup (op =) name_map |> these
    2.55                |> map_filter (try (unprefix axiom_prefix)) |> map unascii_of
    2.56 -          val chained = forall (is_true_for axiom_names) axioms
    2.57 -        in (axioms |> space_implode " ", chained) end
    2.58 +          val loc =
    2.59 +            case axioms of
    2.60 +              [axiom] => find_first_in_vector axiom_names axiom General
    2.61 +            | _ => General
    2.62 +        in (axioms |> space_implode " ", loc) end
    2.63      in
    2.64        (conjecture_shape |> map (maps renumber_conjecture),
    2.65         seq |> map name_for_number |> Vector.fromList)
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Aug 26 09:23:21 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Aug 26 10:42:06 2010 +0200
     3.3 @@ -5,6 +5,8 @@
     3.4  
     3.5  signature SLEDGEHAMMER_FACT_FILTER =
     3.6  sig
     3.7 +  datatype locality = General | Theory | Local | Chained
     3.8 +
     3.9    type relevance_override =
    3.10      {add: Facts.ref list,
    3.11       del: Facts.ref list,
    3.12 @@ -13,11 +15,11 @@
    3.13    val trace : bool Unsynchronized.ref
    3.14    val name_thm_pairs_from_ref :
    3.15      Proof.context -> unit Symtab.table -> thm list -> Facts.ref
    3.16 -    -> ((unit -> string * bool) * (bool * thm)) list
    3.17 +    -> ((string * locality) * thm) list
    3.18    val relevant_facts :
    3.19      bool -> real * real -> int -> bool -> relevance_override
    3.20      -> Proof.context * (thm list * 'a) -> term list -> term
    3.21 -    -> ((string * bool) * thm) list
    3.22 +    -> ((string * locality) * thm) list
    3.23  end;
    3.24  
    3.25  structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER =
    3.26 @@ -30,6 +32,8 @@
    3.27  
    3.28  val respect_no_atp = true
    3.29  
    3.30 +datatype locality = General | Theory | Local | Chained
    3.31 +
    3.32  type relevance_override =
    3.33    {add: Facts.ref list,
    3.34     del: Facts.ref list,
    3.35 @@ -47,11 +51,11 @@
    3.36      val name = Facts.string_of_ref xref
    3.37      val multi = length ths > 1
    3.38    in
    3.39 -    fold (fn th => fn (j, rest) =>
    3.40 -             (j + 1, (fn () => (repair_name reserved multi j name,
    3.41 -                                member Thm.eq_thm chained_ths th),
    3.42 -                      (multi, th)) :: rest))
    3.43 -         ths (1, [])
    3.44 +    (ths, (1, []))
    3.45 +    |-> fold (fn th => fn (j, rest) =>
    3.46 +                 (j + 1, ((repair_name reserved multi j name,
    3.47 +                          if member Thm.eq_thm chained_ths th then Chained
    3.48 +                          else General), th) :: rest))
    3.49      |> snd
    3.50    end
    3.51  
    3.52 @@ -245,19 +249,27 @@
    3.53  *)
    3.54  fun irrel_log n = Math.ln (Real.fromInt n + 19.0) / 6.4
    3.55  
    3.56 +(* FUDGE *)
    3.57 +val skolem_weight = 1.0
    3.58 +val abs_weight = 2.0
    3.59 +
    3.60  (* Computes a constant's weight, as determined by its frequency. *)
    3.61  val rel_weight = rel_log oo pseudoconst_freq match_pseudotypes
    3.62  fun irrel_weight const_tab (c as (s, _)) =
    3.63 -  if String.isPrefix skolem_prefix s then 1.0
    3.64 -  else if String.isPrefix abs_prefix s then 2.0
    3.65 +  if String.isPrefix skolem_prefix s then skolem_weight
    3.66 +  else if String.isPrefix abs_prefix s then abs_weight
    3.67    else irrel_log (pseudoconst_freq (match_pseudotypes o swap) const_tab c)
    3.68  (* TODO: experiment
    3.69  fun irrel_weight _ _ = 1.0
    3.70  *)
    3.71  
    3.72 -val chained_bonus_factor = 2.0
    3.73 +(* FUDGE *)
    3.74 +fun locality_multiplier General = 1.0
    3.75 +  | locality_multiplier Theory = 1.1
    3.76 +  | locality_multiplier Local = 1.3
    3.77 +  | locality_multiplier Chained = 2.0
    3.78  
    3.79 -fun axiom_weight chained const_tab relevant_consts axiom_consts =
    3.80 +fun axiom_weight loc const_tab relevant_consts axiom_consts =
    3.81    case axiom_consts |> List.partition (pseudoconst_mem I relevant_consts)
    3.82                      ||> filter_out (pseudoconst_mem swap relevant_consts) of
    3.83      ([], []) => 0.0
    3.84 @@ -265,7 +277,7 @@
    3.85    | (rel, irrel) =>
    3.86      let
    3.87        val rel_weight = fold (curry Real.+ o rel_weight const_tab) rel 0.0
    3.88 -                       |> chained ? curry Real.* chained_bonus_factor
    3.89 +                       |> curry Real.* (locality_multiplier loc)
    3.90        val irrel_weight = fold (curry Real.+ o irrel_weight const_tab) irrel 0.0
    3.91        val res = rel_weight / (rel_weight + irrel_weight)
    3.92      in if Real.isFinite res then res else 0.0 end
    3.93 @@ -294,7 +306,7 @@
    3.94                  |> pseudoconsts_of_term thy)
    3.95  
    3.96  type annotated_thm =
    3.97 -  ((unit -> string * bool) * thm) * (string * pseudotype list) list
    3.98 +  (((unit -> string) * locality) * thm) * (string * pseudotype list) list
    3.99  
   3.100  fun take_most_relevant max_max_imperfect max_relevant remaining_max
   3.101                         (candidates : (annotated_thm * real) list) =
   3.102 @@ -315,12 +327,13 @@
   3.103                          Real.toString (#2 (hd accepts)));
   3.104      trace_msg (fn () => "Actually passed (" ^ Int.toString (length accepts) ^
   3.105          "): " ^ (accepts
   3.106 -                 |> map (fn (((name, _), _), weight) =>
   3.107 -                            fst (name ()) ^ " [" ^ Real.toString weight ^ "]")
   3.108 +                 |> map (fn ((((name, _), _), _), weight) =>
   3.109 +                            name () ^ " [" ^ Real.toString weight ^ "]")
   3.110                   |> commas));
   3.111      (accepts, more_rejects @ rejects)
   3.112    end
   3.113  
   3.114 +(* FUDGE *)
   3.115  val threshold_divisor = 2.0
   3.116  val ridiculous_threshold = 0.1
   3.117  val max_max_imperfect_fudge_factor = 0.66
   3.118 @@ -392,17 +405,17 @@
   3.119                        hopeless_rejects hopeful_rejects)
   3.120              end
   3.121            | relevant candidates rejects hopeless
   3.122 -                     (((ax as ((name, th), axiom_consts)), cached_weight)
   3.123 +                     (((ax as (((_, loc), th), axiom_consts)), cached_weight)
   3.124                        :: hopeful) =
   3.125              let
   3.126                val weight =
   3.127                  case cached_weight of
   3.128                    SOME w => w
   3.129 -                | NONE => axiom_weight (snd (name ())) const_tab rel_const_tab
   3.130 -                                       axiom_consts
   3.131 +                | NONE => axiom_weight loc const_tab rel_const_tab axiom_consts
   3.132  (* TODO: experiment
   3.133 -val _ = if String.isPrefix "lift.simps(3" (fst (name ())) then
   3.134 -tracing ("*** " ^ (fst (name ())) ^ PolyML.makestring (debug_axiom_weight const_tab rel_const_tab axiom_consts))
   3.135 +val name = fst (fst (fst ax)) ()
   3.136 +val _ = if String.isPrefix "lift.simps(3" name then
   3.137 +tracing ("*** " ^ name ^ PolyML.makestring (debug_axiom_weight const_tab rel_const_tab axiom_consts))
   3.138  else
   3.139  ()
   3.140  *)
   3.141 @@ -570,10 +583,12 @@
   3.142  
   3.143  fun all_name_thms_pairs ctxt reserved full_types add_thms chained_ths =
   3.144    let
   3.145 -    val is_chained = member Thm.eq_thm chained_ths
   3.146 -    val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt)
   3.147 +    val thy = ProofContext.theory_of ctxt
   3.148 +    val thy_prefix = Context.theory_name thy ^ Long_Name.separator
   3.149 +    val global_facts = PureThy.facts_of thy
   3.150      val local_facts = ProofContext.facts_of ctxt
   3.151      val named_locals = local_facts |> Facts.dest_static []
   3.152 +    val is_chained = member Thm.eq_thm chained_ths
   3.153      (* Unnamed, not chained formulas with schematic variables are omitted,
   3.154         because they are rejected by the backticks (`...`) parser for some
   3.155         reason. *)
   3.156 @@ -585,7 +600,7 @@
   3.157                    |> map (pair "" o single)
   3.158      val full_space =
   3.159        Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
   3.160 -    fun add_valid_facts foldx facts =
   3.161 +    fun add_facts global foldx facts =
   3.162        foldx (fn (name0, ths) =>
   3.163          if name0 <> "" andalso
   3.164             forall (not o member Thm.eq_thm add_thms) ths andalso
   3.165 @@ -596,6 +611,10 @@
   3.166            I
   3.167          else
   3.168            let
   3.169 +            val base_loc =
   3.170 +              if not global then Local
   3.171 +              else if String.isPrefix thy_prefix name0 then Theory
   3.172 +              else General
   3.173              val multi = length ths > 1
   3.174              fun backquotify th =
   3.175                "`" ^ Print_Mode.setmp [Print_Mode.input]
   3.176 @@ -614,23 +633,24 @@
   3.177                       not (member Thm.eq_thm add_thms th) then
   3.178                      rest
   3.179                    else
   3.180 -                    (fn () =>
   3.181 -                        (if name0 = "" then
   3.182 -                           th |> backquotify
   3.183 -                         else
   3.184 -                           let
   3.185 -                             val name1 = Facts.extern facts name0
   3.186 -                             val name2 = Name_Space.extern full_space name0
   3.187 -                           in
   3.188 -                             case find_first check_thms [name1, name2, name0] of
   3.189 -                               SOME name => repair_name reserved multi j name
   3.190 -                             | NONE => ""
   3.191 -                           end, is_chained th), (multi, th)) :: rest)) ths
   3.192 +                    (((fn () =>
   3.193 +                          if name0 = "" then
   3.194 +                            th |> backquotify
   3.195 +                          else
   3.196 +                            let
   3.197 +                              val name1 = Facts.extern facts name0
   3.198 +                              val name2 = Name_Space.extern full_space name0
   3.199 +                            in
   3.200 +                              case find_first check_thms [name1, name2, name0] of
   3.201 +                                SOME name => repair_name reserved multi j name
   3.202 +                              | NONE => ""
   3.203 +                            end), if is_chained th then Chained else base_loc),
   3.204 +                      (multi, th)) :: rest)) ths
   3.205              #> snd
   3.206            end)
   3.207    in
   3.208 -    [] |> add_valid_facts fold local_facts (unnamed_locals @ named_locals)
   3.209 -       |> add_valid_facts Facts.fold_static global_facts global_facts
   3.210 +    [] |> add_facts false fold local_facts (unnamed_locals @ named_locals)
   3.211 +       |> add_facts true Facts.fold_static global_facts global_facts
   3.212    end
   3.213  
   3.214  (* The single-name theorems go after the multiple-name ones, so that single
   3.215 @@ -653,7 +673,8 @@
   3.216      val reserved = reserved_isar_keyword_table ()
   3.217      val axioms =
   3.218        (if only then
   3.219 -         maps (name_thm_pairs_from_ref ctxt reserved chained_ths) add
   3.220 +         maps (map (fn ((name, loc), th) => ((K name, loc), (true, th)))
   3.221 +               o name_thm_pairs_from_ref ctxt reserved chained_ths) add
   3.222         else
   3.223           all_name_thms_pairs ctxt reserved full_types add_thms chained_ths)
   3.224        |> name_thm_pairs ctxt (respect_no_atp andalso not only)
   3.225 @@ -668,7 +689,7 @@
   3.226       else
   3.227         relevance_filter ctxt threshold0 decay max_relevant theory_relevant
   3.228                          relevance_override axioms (concl_t :: hyp_ts))
   3.229 -    |> map (apfst (fn f => f ())) |> sort_wrt (fst o fst)
   3.230 +    |> map (apfst (apfst (fn f => f ()))) |> sort_wrt (fst o fst)
   3.231    end
   3.232  
   3.233  end;
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML	Thu Aug 26 09:23:21 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML	Thu Aug 26 10:42:06 2010 +0200
     4.3 @@ -7,11 +7,12 @@
     4.4  
     4.5  signature SLEDGEHAMMER_FACT_MINIMIZE =
     4.6  sig
     4.7 +  type locality = Sledgehammer_Fact_Filter.locality
     4.8    type params = Sledgehammer.params
     4.9  
    4.10    val minimize_theorems :
    4.11 -    params -> int -> int -> Proof.state -> ((string * bool) * thm list) list
    4.12 -    -> ((string * bool) * thm list) list option * string
    4.13 +    params -> int -> int -> Proof.state -> ((string * locality) * thm list) list
    4.14 +    -> ((string * locality) * thm list) list option * string
    4.15    val run_minimize : params -> int -> Facts.ref list -> Proof.state -> unit
    4.16  end;
    4.17  
    4.18 @@ -120,7 +121,7 @@
    4.19           val n = length min_thms
    4.20           val _ = priority (cat_lines
    4.21             ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^
    4.22 -            (case length (filter (snd o fst) min_thms) of
    4.23 +            (case length (filter (curry (op =) Chained o snd o fst) min_thms) of
    4.24                 0 => ""
    4.25               | n => " (including " ^ Int.toString n ^ " chained)") ^ ".")
    4.26         in
    4.27 @@ -149,7 +150,7 @@
    4.28      val reserved = reserved_isar_keyword_table ()
    4.29      val chained_ths = #facts (Proof.goal state)
    4.30      val axioms =
    4.31 -      maps (map (fn (name, (_, th)) => (name (), [th]))
    4.32 +      maps (map (apsnd single)
    4.33              o name_thm_pairs_from_ref ctxt reserved chained_ths) refs
    4.34    in
    4.35      case subgoal_count state of
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Aug 26 09:23:21 2010 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Aug 26 10:42:06 2010 +0200
     5.3 @@ -8,19 +8,20 @@
     5.4  
     5.5  signature SLEDGEHAMMER_PROOF_RECONSTRUCT =
     5.6  sig
     5.7 +  type locality = Sledgehammer_Fact_Filter.locality
     5.8    type minimize_command = string list -> string
     5.9  
    5.10    val metis_proof_text:
    5.11 -    bool * minimize_command * string * (string * bool) vector * thm * int
    5.12 -    -> string * (string * bool) list
    5.13 +    bool * minimize_command * string * (string * locality) vector * thm * int
    5.14 +    -> string * (string * locality) list
    5.15    val isar_proof_text:
    5.16      string Symtab.table * bool * int * Proof.context * int list list
    5.17 -    -> bool * minimize_command * string * (string * bool) vector * thm * int
    5.18 -    -> string * (string * bool) list
    5.19 +    -> bool * minimize_command * string * (string * locality) vector * thm * int
    5.20 +    -> string * (string * locality) list
    5.21    val proof_text:
    5.22      bool -> string Symtab.table * bool * int * Proof.context * int list list
    5.23 -    -> bool * minimize_command * string * (string * bool) vector * thm * int
    5.24 -    -> string * (string * bool) list
    5.25 +    -> bool * minimize_command * string * (string * locality) vector * thm * int
    5.26 +    -> string * (string * locality) list
    5.27  end;
    5.28  
    5.29  structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
    5.30 @@ -578,7 +579,7 @@
    5.31            (case strip_prefix_and_unascii axiom_prefix (List.last rest) of
    5.32               SOME name =>
    5.33               if member (op =) rest "file" then
    5.34 -               SOME (name, is_true_for axiom_names name)
    5.35 +               SOME (name, find_first_in_vector axiom_names name General)
    5.36               else
    5.37                 axiom_name_at_index num
    5.38             | NONE => axiom_name_at_index num)
    5.39 @@ -624,8 +625,8 @@
    5.40  
    5.41  fun used_facts axiom_names =
    5.42    used_facts_in_atp_proof axiom_names
    5.43 -  #> List.partition snd
    5.44 -  #> pairself (sort_distinct (string_ord) o map fst)
    5.45 +  #> List.partition (curry (op =) Chained o snd)
    5.46 +  #> pairself (sort_distinct (string_ord o pairself fst))
    5.47  
    5.48  fun metis_proof_text (full_types, minimize_command, atp_proof, axiom_names,
    5.49                        goal, i) =
    5.50 @@ -633,9 +634,9 @@
    5.51      val (chained_lemmas, other_lemmas) = used_facts axiom_names atp_proof
    5.52      val n = Logic.count_prems (prop_of goal)
    5.53    in
    5.54 -    (metis_line full_types i n other_lemmas ^
    5.55 -     minimize_line minimize_command (other_lemmas @ chained_lemmas),
    5.56 -     map (rpair false) other_lemmas @ map (rpair true) chained_lemmas)
    5.57 +    (metis_line full_types i n (map fst other_lemmas) ^
    5.58 +     minimize_line minimize_command (map fst (other_lemmas @ chained_lemmas)),
    5.59 +     other_lemmas @ chained_lemmas)
    5.60    end
    5.61  
    5.62  (** Isar proof construction and manipulation **)
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Thu Aug 26 09:23:21 2010 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Thu Aug 26 10:42:06 2010 +0200
     6.3 @@ -18,8 +18,8 @@
     6.4    val tfrees_name : string
     6.5    val prepare_problem :
     6.6      Proof.context -> bool -> bool -> bool -> bool -> term list -> term
     6.7 -    -> ((string * bool) * thm) list
     6.8 -    -> string problem * string Symtab.table * int * (string * bool) vector
     6.9 +    -> ((string * 'a) * thm) list
    6.10 +    -> string problem * string Symtab.table * int * (string * 'a) vector
    6.11  end;
    6.12  
    6.13  structure Sledgehammer_Translate : SLEDGEHAMMER_TRANSLATE =
    6.14 @@ -39,11 +39,11 @@
    6.15  (* Freshness almost guaranteed! *)
    6.16  val sledgehammer_weak_prefix = "Sledgehammer:"
    6.17  
    6.18 -datatype fol_formula =
    6.19 -  FOLFormula of {name: string,
    6.20 -                 kind: kind,
    6.21 -                 combformula: (name, combterm) formula,
    6.22 -                 ctypes_sorts: typ list}
    6.23 +type fol_formula =
    6.24 +  {name: string,
    6.25 +   kind: kind,
    6.26 +   combformula: (name, combterm) formula,
    6.27 +   ctypes_sorts: typ list}
    6.28  
    6.29  fun mk_anot phi = AConn (ANot, [phi])
    6.30  fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
    6.31 @@ -190,15 +190,14 @@
    6.32                |> kind <> Axiom ? freeze_term
    6.33      val (combformula, ctypes_sorts) = combformula_for_prop thy t []
    6.34    in
    6.35 -    FOLFormula {name = name, combformula = combformula, kind = kind,
    6.36 -                ctypes_sorts = ctypes_sorts}
    6.37 +    {name = name, combformula = combformula, kind = kind,
    6.38 +     ctypes_sorts = ctypes_sorts}
    6.39    end
    6.40  
    6.41 -fun make_axiom ctxt presimp ((name, chained), th) =
    6.42 +fun make_axiom ctxt presimp ((name, loc), th) =
    6.43    case make_formula ctxt presimp name Axiom (prop_of th) of
    6.44 -    FOLFormula {combformula = AAtom (CombConst (("c_True", _), _, _)), ...} =>
    6.45 -    NONE
    6.46 -  | formula => SOME ((name, chained), formula)
    6.47 +    {combformula = AAtom (CombConst (("c_True", _), _, _)), ...} => NONE
    6.48 +  | formula => SOME ((name, loc), formula)
    6.49  fun make_conjecture ctxt ts =
    6.50    let val last = length ts - 1 in
    6.51      map2 (fn j => make_formula ctxt true (Int.toString j)
    6.52 @@ -215,7 +214,7 @@
    6.53  fun count_combformula (AQuant (_, _, phi)) = count_combformula phi
    6.54    | count_combformula (AConn (_, phis)) = fold count_combformula phis
    6.55    | count_combformula (AAtom tm) = count_combterm tm
    6.56 -fun count_fol_formula (FOLFormula {combformula, ...}) =
    6.57 +fun count_fol_formula ({combformula, ...} : fol_formula) =
    6.58    count_combformula combformula
    6.59  
    6.60  val optional_helpers =
    6.61 @@ -326,13 +325,13 @@
    6.62        | aux (AAtom tm) = AAtom (fo_term_for_combterm full_types tm)
    6.63    in aux end
    6.64  
    6.65 -fun formula_for_axiom full_types (FOLFormula {combformula, ctypes_sorts, ...}) =
    6.66 +fun formula_for_axiom full_types
    6.67 +                      ({combformula, ctypes_sorts, ...} : fol_formula) =
    6.68    mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)
    6.69                  (type_literals_for_types ctypes_sorts))
    6.70             (formula_for_combformula full_types combformula)
    6.71  
    6.72 -fun problem_line_for_fact prefix full_types
    6.73 -                          (formula as FOLFormula {name, kind, ...}) =
    6.74 +fun problem_line_for_fact prefix full_types (formula as {name, kind, ...}) =
    6.75    Fof (prefix ^ ascii_of name, kind, formula_for_axiom full_types formula)
    6.76  
    6.77  fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
    6.78 @@ -357,11 +356,11 @@
    6.79                       (fo_literal_for_arity_literal conclLit)))
    6.80  
    6.81  fun problem_line_for_conjecture full_types
    6.82 -                                (FOLFormula {name, kind, combformula, ...}) =
    6.83 +                                ({name, kind, combformula, ...} : fol_formula) =
    6.84    Fof (conjecture_prefix ^ name, kind,
    6.85         formula_for_combformula full_types combformula)
    6.86  
    6.87 -fun free_type_literals_for_conjecture (FOLFormula {ctypes_sorts, ...}) =
    6.88 +fun free_type_literals_for_conjecture ({ctypes_sorts, ...} : fol_formula) =
    6.89    map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts)
    6.90  
    6.91  fun problem_line_for_free_type lit =
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Aug 26 09:23:21 2010 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Aug 26 10:42:06 2010 +0200
     7.3 @@ -6,7 +6,7 @@
     7.4  
     7.5  signature SLEDGEHAMMER_UTIL =
     7.6  sig
     7.7 -  val is_true_for : (string * bool) vector -> string -> bool
     7.8 +  val find_first_in_vector : (''a * 'b) vector -> ''a -> 'b -> 'b
     7.9    val plural_s : int -> string
    7.10    val serial_commas : string -> string list -> string list
    7.11    val simplify_spaces : string -> string
    7.12 @@ -29,8 +29,9 @@
    7.13  structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
    7.14  struct
    7.15  
    7.16 -fun is_true_for v s =
    7.17 -  Vector.foldl (fn ((s', b'), b) => if s' = s then b' else b) false v
    7.18 +fun find_first_in_vector vec key default =
    7.19 +  Vector.foldl (fn ((key', value'), value) =>
    7.20 +                   if key' = key then value' else value) default vec
    7.21  
    7.22  fun plural_s n = if n = 1 then "" else "s"
    7.23