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