--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Aug 24 22:38:45 2010 +0800
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Aug 24 20:09:30 2010 +0200
@@ -293,7 +293,7 @@
local
datatype sh_result =
- SH_OK of int * int * string list |
+ SH_OK of int * int * (string * bool) list |
SH_FAIL of int * int |
SH_ERROR
@@ -354,7 +354,9 @@
in
case result of
SH_OK (time_isa, time_atp, names) =>
- let fun get_thms name = (name, thms_of_name (Proof.context_of st) name)
+ let
+ fun get_thms (name, chained) =
+ ((name, chained), thms_of_name (Proof.context_of st) name)
in
change_data id inc_sh_success;
change_data id (inc_sh_lemmas (length names));
@@ -442,7 +444,8 @@
if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal
then () else
let
- val named_thms = Unsynchronized.ref (NONE : (string * thm list) list option)
+ val named_thms =
+ Unsynchronized.ref (NONE : ((string * bool) * thm list) list option)
val minimize = AList.defined (op =) args minimizeK
val metis_ft = AList.defined (op =) args metis_ftK
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Tue Aug 24 22:38:45 2010 +0800
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Tue Aug 24 20:09:30 2010 +0200
@@ -22,8 +22,6 @@
open Metis_Clauses
-exception METIS of string * string
-
val trace = Unsynchronized.ref false;
fun trace_msg msg = if !trace then tracing (msg ()) else ();
@@ -88,7 +86,7 @@
val args = map hol_term_to_fol_FO tms
in Metis.Term.Fn (c, tyargs @ args) end
| (CombVar ((v, _), _), []) => Metis.Term.Var v
- | _ => raise METIS ("hol_term_to_fol_FO", "non first-order combterm")
+ | _ => raise Fail "non-first-order combterm"
fun hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) =
Metis.Term.Fn (fn_isa_to_met_sublevel a, map metis_term_from_combtyp tylist)
@@ -429,8 +427,8 @@
Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
Syntax.string_of_term ctxt (term_of y)))));
in cterm_instantiate substs' i_th end
- handle THM (msg, _, _) => raise METIS ("inst_inf", msg)
- | ERROR msg => raise METIS ("inst_inf", msg)
+ handle THM (msg, _, _) =>
+ error ("Cannot replay Metis proof in Isabelle:\n" ^ msg)
(* INFERENCE RULE: RESOLVE *)
@@ -446,7 +444,6 @@
[th] => th
| _ => raise THM ("resolve_inc_tyvars: unique result expected", i, [tha,thb])
end
- handle TERM (msg, _) => raise METIS ("resolve_inc_tyvars", msg)
fun resolve_inf ctxt mode skolems thpairs atm th1 th2 =
let
@@ -501,8 +498,11 @@
val adjustment = get_ty_arg_size thy tm1
val p' = if adjustment > p then p else p-adjustment
val tm_p = List.nth(args,p')
- handle Subscript => raise METIS ("equality_inf", Int.toString p ^ " adj " ^
- Int.toString adjustment ^ " term " ^ Syntax.string_of_term ctxt tm)
+ handle Subscript =>
+ error ("Cannot replay Metis proof in Isabelle:\n" ^
+ "equality_inf: " ^ Int.toString p ^ " adj " ^
+ Int.toString adjustment ^ " term " ^
+ Syntax.string_of_term ctxt tm)
val _ = trace_msg (fn () => "path_finder: " ^ Int.toString p ^
" " ^ Syntax.string_of_term ctxt tm_p)
val (r,t) = path_finder_FO tm_p ps
@@ -590,9 +590,8 @@
val _ = trace_msg (fn () => "=============================================")
val n_metis_lits =
length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th)))
- val _ =
- if nprems_of th = n_metis_lits then ()
- else raise METIS ("translate", "Proof reconstruction has gone wrong.")
+ val _ = if nprems_of th = n_metis_lits then ()
+ else error "Cannot replay Metis proof in Isabelle."
in (fol_th, th) :: thpairs end
(*Determining which axiom clauses are actually used*)
@@ -805,14 +804,7 @@
Meson.MESON (maps neg_clausify)
(fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
ctxt i st0
- handle ERROR msg => raise METIS ("generic_metis_tac", msg)
end
- handle METIS (loc, msg) =>
- if mode = HO then
- (warning ("Metis: Falling back on \"metisFT\".");
- generic_metis_tac FT ctxt ths i st0)
- else
- Seq.empty
val metis_tac = generic_metis_tac HO
val metisF_tac = generic_metis_tac FO
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Aug 24 22:38:45 2010 +0800
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Aug 24 20:09:30 2010 +0200
@@ -30,16 +30,16 @@
{subgoal: int,
goal: Proof.context * (thm list * thm),
relevance_override: relevance_override,
- axioms: (string * thm) list option}
+ axioms: ((string * bool) * thm) list option}
type prover_result =
{outcome: failure option,
message: string,
pool: string Symtab.table,
- used_thm_names: string list,
+ used_thm_names: (string * bool) list,
atp_run_time_in_msecs: int,
output: string,
proof: string,
- axiom_names: string Vector.vector,
+ axiom_names: (string * bool) vector,
conjecture_shape: int list list}
type prover = params -> minimize_command -> problem -> prover_result
@@ -100,17 +100,17 @@
{subgoal: int,
goal: Proof.context * (thm list * thm),
relevance_override: relevance_override,
- axioms: (string * thm) list option}
+ axioms: ((string * bool) * thm) list option}
type prover_result =
{outcome: failure option,
message: string,
pool: string Symtab.table,
- used_thm_names: string list,
+ used_thm_names: (string * bool) list,
atp_run_time_in_msecs: int,
output: string,
proof: string,
- axiom_names: string Vector.vector,
+ axiom_names: (string * bool) vector,
conjecture_shape: int list list}
type prover = params -> minimize_command -> problem -> prover_result
@@ -180,11 +180,11 @@
#> parse_clause_formula_relation #> fst
fun repair_conjecture_shape_and_theorem_names output conjecture_shape
- thm_names =
+ axiom_names =
if String.isSubstring set_ClauseFormulaRelationN output then
(* This is a hack required for keeping track of axioms after they have been
- clausified by SPASS's Flotter tool. The "ATP/scripts/spass" script is also
- part of this hack. *)
+ clausified by SPASS's Flotter tool. The "ATP/scripts/spass" script is
+ also part of this hack. *)
let
val j0 = hd (hd conjecture_shape)
val seq = extract_clause_sequence output
@@ -193,15 +193,20 @@
conjecture_prefix ^ Int.toString (j - j0)
|> AList.find (fn (s, ss) => member (op =) ss s) name_map
|> map (fn s => find_index (curry (op =) s) seq + 1)
+ fun name_for_number j =
+ let
+ val axioms =
+ j |> AList.lookup (op =) name_map
+ |> these |> map_filter (try (unprefix axiom_prefix))
+ |> map undo_ascii_of
+ val chained = forall (is_true_for axiom_names) axioms
+ in (axioms |> space_implode " ", chained) end
in
(conjecture_shape |> map (maps renumber_conjecture),
- seq |> map (AList.lookup (op =) name_map #> these
- #> map_filter (try (unprefix axiom_prefix))
- #> map undo_ascii_of #> space_implode " ")
- |> Vector.fromList)
+ seq |> map name_for_number |> Vector.fromList)
end
else
- (conjecture_shape, thm_names)
+ (conjecture_shape, axiom_names)
(* generic TPTP-based provers *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Aug 24 22:38:45 2010 +0800
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Aug 24 20:09:30 2010 +0200
@@ -11,13 +11,13 @@
only: bool}
val trace : bool Unsynchronized.ref
- val chained_prefix : string
val name_thms_pair_from_ref :
- Proof.context -> thm list -> Facts.ref -> string * thm list
+ Proof.context -> unit Symtab.table -> thm list -> Facts.ref
+ -> (unit -> string * bool) * thm list
val relevant_facts :
bool -> real -> real -> bool -> int -> bool -> relevance_override
-> Proof.context * (thm list * 'a) -> term list -> term
- -> (string * thm) list
+ -> ((string * bool) * thm) list
end;
structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER =
@@ -36,17 +36,15 @@
only: bool}
val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
-(* Used to label theorems chained into the goal. *)
-val chained_prefix = sledgehammer_prefix ^ "chained_"
-fun name_thms_pair_from_ref ctxt chained_ths xref =
- let
- val ths = ProofContext.get_fact ctxt xref
- val name = Facts.string_of_ref xref
- |> forall (member Thm.eq_thm chained_ths) ths
- ? prefix chained_prefix
- in (name, ths) end
-
+fun name_thms_pair_from_ref ctxt reserved chained_ths xref =
+ let val ths = ProofContext.get_fact ctxt xref in
+ (fn () => let
+ val name = Facts.string_of_ref xref
+ val name = name |> Symtab.defined reserved name ? quote
+ val chained = forall (member Thm.eq_thm chained_ths) ths
+ in (name, chained) end, ths)
+ end
(***************************************************************)
(* Relevance Filtering *)
@@ -280,7 +278,8 @@
| _ => false
end;
-type annotated_thm = (string * thm) * (string * const_typ list) list
+type annotated_thm =
+ ((unit -> string * bool) * thm) * (string * const_typ list) list
(*For a reverse sort, putting the largest values first.*)
fun compare_pairs ((_, w1), (_, w2)) = Real.compare (w2, w1)
@@ -299,7 +298,7 @@
", exceeds the limit of " ^ Int.toString max_new));
trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
trace_msg (fn () => "Actually passed: " ^
- space_implode ", " (map (fst o fst o fst) accepted));
+ space_implode ", " (map (fst o (fn f => f ()) o fst o fst o fst) accepted));
(map #1 accepted, List.drop (new_pairs, max_new))
end
end;
@@ -341,7 +340,7 @@
if null add_thms then
[]
else
- map_filter (fn ((p as (name, th), _), _) =>
+ map_filter (fn ((p as (_, th), _), _) =>
if member Thm.eq_thm add_thms th then SOME p
else NONE) rejects
| relevant (new_pairs, rejects) [] =
@@ -376,7 +375,7 @@
if weight >= threshold orelse
(defs_relevant andalso defines thy th rel_const_tab) then
(trace_msg (fn () =>
- name ^ " passes: " ^ Real.toString weight
+ fst (name ()) ^ " passes: " ^ Real.toString weight
^ " consts: " ^ commas (map fst axiom_consts));
relevant ((ax, weight) :: new_rels, rejects) rest)
else
@@ -532,72 +531,82 @@
is_strange_theorem thm
end
-fun all_name_thms_pairs ctxt full_types add_thms chained_ths =
+fun all_name_thms_pairs ctxt reserved full_types add_thms chained_ths =
let
- val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt);
+ val is_chained = member Thm.eq_thm chained_ths
+ val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt)
val local_facts = ProofContext.facts_of ctxt
val named_locals = local_facts |> Facts.dest_static []
+ (* Unnamed, not chained formulas with schematic variables are omitted,
+ because they are rejected by the backticks (`...`) parser for some
+ reason. *)
+ fun is_bad_unnamed_local th =
+ exists (fn (_, ths) => member Thm.eq_thm ths th) named_locals orelse
+ (exists_subterm is_Var (prop_of th) andalso not (is_chained th))
val unnamed_locals =
- local_facts |> Facts.props
- |> filter_out (fn th => exists (fn (_, ths) => member Thm.eq_thm ths th)
- named_locals)
- |> map (pair "" o single)
+ local_facts |> Facts.props |> filter_out is_bad_unnamed_local
+ |> map (pair "" o single)
val full_space =
Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts);
- fun add_valid_facts xfold facts =
- xfold (fn (name, ths0) =>
- if name <> "" andalso
- forall (not o member Thm.eq_thm add_thms) ths0 andalso
- (Facts.is_concealed facts name orelse
- (respect_no_atp andalso is_package_def name) orelse
- exists (fn s => String.isSuffix s name) multi_base_blacklist orelse
- String.isSuffix "_def_raw" (* FIXME: crude hack *) name) then
+ fun add_valid_facts foldx facts =
+ foldx (fn (name0, ths) =>
+ if name0 <> "" andalso
+ forall (not o member Thm.eq_thm add_thms) ths andalso
+ (Facts.is_concealed facts name0 orelse
+ (respect_no_atp andalso is_package_def name0) orelse
+ exists (fn s => String.isSuffix s name0) multi_base_blacklist orelse
+ String.isSuffix "_def_raw" (* FIXME: crude hack *) name0) then
I
else
let
+ val multi = length ths > 1
+ fun backquotify th =
+ "`" ^ Print_Mode.setmp [Print_Mode.input]
+ (Syntax.string_of_term ctxt) (prop_of th) ^ "`"
fun check_thms a =
- (case try (ProofContext.get_thms ctxt) a of
+ case try (ProofContext.get_thms ctxt) a of
NONE => false
- | SOME ths1 => Thm.eq_thms (ths0, ths1))
- val name1 = Facts.extern facts name;
- val name2 = Name_Space.extern full_space name;
- val ths =
- ths0 |> filter ((not o is_theorem_bad_for_atps full_types) orf
- member Thm.eq_thm add_thms)
- val name' =
- case find_first check_thms [name1, name2, name] of
- SOME name' => name'
- | NONE =>
- ths |> map (fn th =>
- "`" ^ Print_Mode.setmp [Print_Mode.input]
- (Syntax.string_of_term ctxt)
- (prop_of th) ^ "`")
- |> space_implode " "
+ | SOME ths' => Thm.eq_thms (ths, ths')
in
- cons (name' |> forall (member Thm.eq_thm chained_ths) ths0
- ? prefix chained_prefix, ths)
+ pair 1
+ #> fold (fn th => fn (j, rest) =>
+ (j + 1,
+ if is_theorem_bad_for_atps full_types th andalso
+ not (member Thm.eq_thm add_thms th) then
+ rest
+ else
+ (fn () =>
+ (if name0 = "" then
+ th |> backquotify
+ else
+ let
+ val name1 = Facts.extern facts name0
+ val name2 = Name_Space.extern full_space name0
+ in
+ case find_first check_thms [name1, name2, name0] of
+ SOME name =>
+ let
+ val name =
+ name |> Symtab.defined reserved name ? quote
+ in
+ if multi then name ^ "(" ^ Int.toString j ^ ")"
+ else name
+ end
+ | NONE => ""
+ end, is_chained th), (multi, th)) :: rest)) ths
+ #> snd
end)
in
[] |> add_valid_facts fold local_facts (unnamed_locals @ named_locals)
|> add_valid_facts Facts.fold_static global_facts global_facts
end
-fun multi_name a th (n, pairs) =
- (n + 1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs);
-
-fun add_names (_, []) pairs = pairs
- | add_names (a, [th]) pairs = (a, th) :: pairs
- | add_names (a, ths) pairs = #2 (fold (multi_name a) ths (1, pairs))
-
-fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
-
(* The single-name theorems go after the multiple-name ones, so that single
names are preferred when both are available. *)
-fun name_thm_pairs ctxt respect_no_atp name_thms_pairs =
- let
- val (mults, singles) = List.partition is_multi name_thms_pairs
- val ps = [] |> fold add_names singles |> fold add_names mults
- in ps |> respect_no_atp ? filter_out (No_ATPs.member ctxt o snd) end;
+fun name_thm_pairs ctxt respect_no_atp =
+ List.partition (fst o snd) #> op @
+ #> map (apsnd snd)
+ #> respect_no_atp ? filter_out (No_ATPs.member ctxt o snd)
(***************************************************************)
(* ATP invocation methods setup *)
@@ -609,9 +618,13 @@
(ctxt, (chained_ths, _)) hyp_ts concl_t =
let
val add_thms = maps (ProofContext.get_fact ctxt) add
+ val reserved = reserved_isar_keyword_table ()
val axioms =
- (if only then map (name_thms_pair_from_ref ctxt chained_ths) add
- else all_name_thms_pairs ctxt full_types add_thms chained_ths)
+ (if only then
+ maps ((fn (n, ths) => map (pair n o pair false) ths)
+ o name_thms_pair_from_ref ctxt reserved chained_ths) add
+ else
+ all_name_thms_pairs ctxt reserved full_types add_thms chained_ths)
|> name_thm_pairs ctxt (respect_no_atp andalso not only)
|> make_unique
in
@@ -620,7 +633,8 @@
relevance_filter ctxt relevance_threshold relevance_convergence
defs_relevant max_new theory_relevant relevance_override
axioms (concl_t :: hyp_ts)
- |> sort_wrt fst
+ |> map (apfst (fn f => f ()))
+ |> sort_wrt (fst o fst)
end
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Tue Aug 24 22:38:45 2010 +0800
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Tue Aug 24 20:09:30 2010 +0200
@@ -10,8 +10,8 @@
type params = Sledgehammer.params
val minimize_theorems :
- params -> int -> int -> Proof.state -> (string * thm list) list
- -> (string * thm list) list option * string
+ params -> int -> int -> Proof.state -> ((string * bool) * thm list) list
+ -> ((string * bool) * thm list) list option * string
val run_minimize : params -> int -> Facts.ref list -> Proof.state -> unit
end;
@@ -30,14 +30,12 @@
| string_for_failure TimedOut = "Timed out."
| string_for_failure _ = "Unknown error."
-fun n_theorems name_thms_pairs =
- let val n = length name_thms_pairs in
+fun n_theorems names =
+ let val n = length names in
string_of_int n ^ " theorem" ^ plural_s n ^
(if n > 0 then
- ": " ^ space_implode " "
- (name_thms_pairs
- |> map (perhaps (try (unprefix chained_prefix)))
- |> sort_distinct string_ord)
+ ": " ^ (names |> map fst
+ |> sort_distinct string_ord |> space_implode " ")
else
"")
end
@@ -65,8 +63,7 @@
{subgoal = subgoal, goal = (ctxt, (facts, goal)),
relevance_override = {add = [], del = [], only = false},
axioms = SOME axioms}
- val result as {outcome, used_thm_names, ...} =
- prover params (K "") problem
+ val result as {outcome, used_thm_names, ...} = prover params (K "") problem
in
priority (case outcome of
NONE =>
@@ -80,8 +77,7 @@
(* minimalization of thms *)
-fun filter_used_facts used =
- filter (member (op =) used o perhaps (try (unprefix chained_prefix)) o fst)
+fun filter_used_facts used = filter (member (op =) used o fst)
fun sublinear_minimize _ [] p = p
| sublinear_minimize test (x :: xs) (seen, result) =
@@ -130,10 +126,9 @@
val n = length min_thms
val _ = priority (cat_lines
["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^
- (case filter (String.isPrefix chained_prefix o fst) min_thms of
- [] => ""
- | chained => " (including " ^ Int.toString (length chained) ^
- " chained)") ^ ".")
+ (case length (filter (snd o fst) min_thms) of
+ 0 => ""
+ | n => " (including " ^ Int.toString n ^ " chained)") ^ ".")
in
(SOME min_thms,
proof_text isar_proof
@@ -157,8 +152,11 @@
fun run_minimize params i refs state =
let
val ctxt = Proof.context_of state
+ val reserved = reserved_isar_keyword_table ()
val chained_ths = #facts (Proof.goal state)
- val name_thms_pairs = map (name_thms_pair_from_ref ctxt chained_ths) refs
+ val name_thms_pairs =
+ map (apfst (fn f => f ())
+ o name_thms_pair_from_ref ctxt reserved chained_ths) refs
in
case subgoal_count state of
0 => priority "No subgoal!"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Aug 24 22:38:45 2010 +0800
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Aug 24 20:09:30 2010 +0200
@@ -11,16 +11,16 @@
type minimize_command = string list -> string
val metis_proof_text:
- bool * minimize_command * string * string vector * thm * int
- -> string * string list
+ bool * minimize_command * string * (string * bool) vector * thm * int
+ -> string * (string * bool) list
val isar_proof_text:
string Symtab.table * bool * int * Proof.context * int list list
- -> bool * minimize_command * string * string vector * thm * int
- -> string * string list
+ -> bool * minimize_command * string * (string * bool) vector * thm * int
+ -> string * (string * bool) list
val proof_text:
bool -> string Symtab.table * bool * int * Proof.context * int list list
- -> bool * minimize_command * string * string vector * thm * int
- -> string * string list
+ -> bool * minimize_command * string * (string * bool) vector * thm * int
+ -> string * (string * bool) list
end;
structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
@@ -60,7 +60,7 @@
fun index_in_shape x = find_index (exists (curry (op =) x))
fun is_axiom_number axiom_names num =
num > 0 andalso num <= Vector.length axiom_names andalso
- Vector.sub (axiom_names, num - 1) <> ""
+ fst (Vector.sub (axiom_names, num - 1)) <> ""
fun is_conjecture_number conjecture_shape num =
index_in_shape num conjecture_shape >= 0
@@ -564,7 +564,7 @@
"108. ... [input]". *)
fun used_facts_in_atp_proof axiom_names atp_proof =
let
- fun axiom_name num =
+ fun axiom_name_at_index num =
let val j = Int.fromString num |> the_default ~1 in
if is_axiom_number axiom_names j then
SOME (Vector.sub (axiom_names, j - 1))
@@ -573,18 +573,20 @@
end
val tokens_of =
String.tokens (fn c => not (Char.isAlphaNum c) andalso c <> #"_")
- val thm_name_list = Vector.foldr (op ::) [] axiom_names
fun do_line (tag :: num :: "axiom" :: (rest as _ :: _)) =
if tag = "cnf" orelse tag = "fof" then
(case strip_prefix_and_undo_ascii axiom_prefix (List.last rest) of
SOME name =>
- if member (op =) rest "file" then SOME name else axiom_name num
- | NONE => axiom_name num)
+ if member (op =) rest "file" then
+ SOME (name, is_true_for axiom_names name)
+ else
+ axiom_name_at_index num
+ | NONE => axiom_name_at_index num)
else
NONE
- | do_line (num :: "0" :: "Inp" :: _) = axiom_name num
+ | do_line (num :: "0" :: "Inp" :: _) = axiom_name_at_index num
| do_line (num :: rest) =
- (case List.last rest of "input" => axiom_name num | _ => NONE)
+ (case List.last rest of "input" => axiom_name_at_index num | _ => NONE)
| do_line _ = NONE
in atp_proof |> split_proof_lines |> map_filter (do_line o tokens_of) end
@@ -613,30 +615,27 @@
"Try this command: " ^
Markup.markup Markup.sendback (metis_command full_types i n ([], ss)) ^ "."
fun minimize_line _ [] = ""
- | minimize_line minimize_command facts =
- case minimize_command facts of
+ | minimize_line minimize_command ss =
+ case minimize_command ss of
"" => ""
| command =>
"\nTo minimize the number of lemmas, try this: " ^
Markup.markup Markup.sendback command ^ "."
-val unprefix_chained = perhaps (try (unprefix chained_prefix))
-
fun used_facts axiom_names =
used_facts_in_atp_proof axiom_names
- #> List.partition (String.isPrefix chained_prefix)
- #>> map (unprefix chained_prefix)
- #> pairself (sort_distinct string_ord)
+ #> List.partition snd
+ #> pairself (sort_distinct (string_ord) o map fst)
fun metis_proof_text (full_types, minimize_command, atp_proof, axiom_names,
goal, i) =
let
val (chained_lemmas, other_lemmas) = used_facts axiom_names atp_proof
- val lemmas = other_lemmas @ chained_lemmas
val n = Logic.count_prems (prop_of goal)
in
(metis_line full_types i n other_lemmas ^
- minimize_line minimize_command lemmas, lemmas)
+ minimize_line minimize_command (other_lemmas @ chained_lemmas),
+ map (rpair false) other_lemmas @ map (rpair true) chained_lemmas)
end
(** Isar proof construction and manipulation **)
@@ -663,7 +662,7 @@
fun add_fact_from_dep axiom_names num =
if is_axiom_number axiom_names num then
- apsnd (insert (op =) (Vector.sub (axiom_names, num - 1)))
+ apsnd (insert (op =) (fst (Vector.sub (axiom_names, num - 1))))
else
apfst (insert (op =) (raw_prefix, num))
@@ -964,10 +963,9 @@
if member (op =) qs Show then "show" else "have")
val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
fun do_facts (ls, ss) =
- let
- val ls = ls |> sort_distinct (prod_ord string_ord int_ord)
- val ss = ss |> map unprefix_chained |> sort_distinct string_ord
- in metis_command full_types 1 1 (ls, ss) end
+ metis_command full_types 1 1
+ (ls |> sort_distinct (prod_ord string_ord int_ord),
+ ss |> sort_distinct string_ord)
and do_step ind (Fix xs) =
do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"
| do_step ind (Let (t1, t2)) =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Tue Aug 24 22:38:45 2010 +0800
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Tue Aug 24 20:09:30 2010 +0200
@@ -18,8 +18,8 @@
val tfrees_name : string
val prepare_problem :
Proof.context -> bool -> bool -> bool -> bool -> term list -> term
- -> (string * thm) list
- -> string problem * string Symtab.table * int * string Vector.vector
+ -> ((string * bool) * thm) list
+ -> string problem * string Symtab.table * int * (string * bool) vector
end;
structure Sledgehammer_Translate : SLEDGEHAMMER_TRANSLATE =
@@ -194,11 +194,11 @@
ctypes_sorts = ctypes_sorts}
end
-fun make_axiom ctxt presimp (name, th) =
+fun make_axiom ctxt presimp ((name, chained), th) =
case make_formula ctxt presimp name Axiom (prop_of th) of
FOLFormula {combformula = AAtom (CombConst (("c_True", _), _, _)), ...} =>
NONE
- | formula => SOME (name, formula)
+ | formula => SOME ((name, chained), formula)
fun make_conjecture ctxt ts =
let val last = length ts - 1 in
map2 (fn j => make_formula ctxt true (Int.toString j)
@@ -235,20 +235,20 @@
let
val ct = fold (fold count_fol_formula) [conjectures, axioms] init_counters
fun is_needed c = the (Symtab.lookup ct c) > 0
+ fun baptize th = ((Thm.get_name_hint th, false), th)
in
(optional_helpers
|> full_types ? append optional_typed_helpers
|> maps (fn (ss, ths) =>
- if exists is_needed ss then map (`Thm.get_name_hint) ths
- else [])) @
- (if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers)
+ if exists is_needed ss then map baptize ths else [])) @
+ (if is_FO then [] else map baptize mandatory_helpers)
|> map_filter (Option.map snd o make_axiom ctxt false)
end
-fun prepare_formulas ctxt full_types hyp_ts concl_t axioms =
+fun prepare_formulas ctxt full_types hyp_ts concl_t axiom_pairs =
let
val thy = ProofContext.theory_of ctxt
- val axiom_ts = map (prop_of o snd) axioms
+ val axiom_ts = map (prop_of o snd) axiom_pairs
val hyp_ts =
if null hyp_ts then
[]
@@ -267,7 +267,7 @@
(* TFrees in the conjecture; TVars in the axioms *)
val conjectures = make_conjecture ctxt (hyp_ts @ [concl_t])
val (axiom_names, axioms) =
- ListPair.unzip (map_filter (make_axiom ctxt true) axioms)
+ ListPair.unzip (map_filter (make_axiom ctxt true) axiom_pairs)
val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms
val (supers', arity_clauses) = make_arity_clauses thy tycons supers
val class_rel_clauses = make_class_rel_clauses thy subs supers'
@@ -500,12 +500,12 @@
(const_table_for_problem explicit_apply problem) problem
fun prepare_problem ctxt readable_names explicit_forall full_types
- explicit_apply hyp_ts concl_t axiom_ts =
+ explicit_apply hyp_ts concl_t axiom_pairs =
let
val thy = ProofContext.theory_of ctxt
val (axiom_names, (conjectures, axioms, helper_facts, class_rel_clauses,
arity_clauses)) =
- prepare_formulas ctxt full_types hyp_ts concl_t axiom_ts
+ prepare_formulas ctxt full_types hyp_ts concl_t axiom_pairs
val axiom_lines = map (problem_line_for_fact axiom_prefix full_types) axioms
val helper_lines =
map (problem_line_for_fact helper_prefix full_types) helper_facts
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue Aug 24 22:38:45 2010 +0800
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue Aug 24 20:09:30 2010 +0200
@@ -6,6 +6,7 @@
signature SLEDGEHAMMER_UTIL =
sig
+ val is_true_for : (string * bool) vector -> string -> bool
val plural_s : int -> string
val serial_commas : string -> string list -> string list
val strip_spaces : string -> string
@@ -21,11 +22,15 @@
val specialize_type : theory -> (string * typ) -> term -> term
val subgoal_count : Proof.state -> int
val strip_subgoal : thm -> int -> (string * typ) list * term list * term
+ val reserved_isar_keyword_table : unit -> unit Symtab.table
end;
structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
struct
+fun is_true_for v s =
+ Vector.foldl (fn ((s', b'), b) => if s' = s then b' else b) false v
+
fun plural_s n = if n = 1 then "" else "s"
fun serial_commas _ [] = ["??"]
@@ -155,4 +160,8 @@
val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees
in (rev (map dest_Free frees), hyp_ts, concl_t) end
+fun reserved_isar_keyword_table () =
+ union (op =) (Keyword.dest_keywords ()) (Keyword.dest_commands ())
+ |> map (rpair ()) |> Symtab.make
+
end;