--- a/doc-src/Sledgehammer/sledgehammer.tex Wed Aug 25 11:13:27 2010 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Wed Aug 25 11:13:58 2010 +0200
@@ -447,14 +447,14 @@
\label{relevance-filter}
\begin{enum}
-\opdefault{relevance\_threshold}{int}{50}
+\opdefault{relevance\_threshold}{int}{40}
Specifies the threshold above which facts are considered relevant by the
relevance filter. The option ranges from 0 to 100, where 0 means that all
theorems are relevant.
-\opdefault{relevance\_convergence}{int}{320}
-Specifies the convergence quotient, multiplied by 100, used by the relevance
-filter. This quotient is used by the relevance filter to scale down the
+\opdefault{relevance\_convergence}{int}{31}
+Specifies the convergence factor, expressed as a percentage, used by the
+relevance filter. This factor is used by the relevance filter to scale down the
relevance of facts at each iteration of the filter.
\opdefault{max\_relevant\_per\_iter}{int\_or\_smart}{\textit{smart}}
--- a/src/HOL/HOL.thy Wed Aug 25 11:13:27 2010 +0200
+++ b/src/HOL/HOL.thy Wed Aug 25 11:13:58 2010 +0200
@@ -1998,7 +1998,7 @@
"solve goal by evaluation"
method_setup normalization = {*
- Scan.succeed (K (SIMPLE_METHOD' (CONVERSION Nbe.norm_conv THEN' (fn k => TRY (rtac TrueI k)))))
+ Scan.succeed (K (SIMPLE_METHOD' (CONVERSION Nbe.dynamic_eval_conv THEN' (fn k => TRY (rtac TrueI k)))))
*} "solve goal by normalization"
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Aug 25 11:13:27 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Aug 25 11:13:58 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/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Wed Aug 25 11:13:27 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Wed Aug 25 11:13:58 2010 +0200
@@ -348,6 +348,9 @@
code_pred (modes: i => i => o => bool as "concat", o => o => i => bool as "slice", o => i => i => bool as prefix,
i => o => i => bool as suffix, i => i => i => bool) append .
+code_pred (modes: i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool as "concat", o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as "slice", o \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool as prefix,
+ i \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as suffix, i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool) append .
+
code_pred [dseq] append .
code_pred [random_dseq] append .
@@ -409,6 +412,10 @@
code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
i * o * i => bool, i * i * i => bool) tupled_append .
+
+code_pred (expected_modes: i \<times> i \<times> o \<Rightarrow> bool, o \<times> o \<times> i \<Rightarrow> bool, o \<times> i \<times> i \<Rightarrow> bool,
+ i \<times> o \<times> i \<Rightarrow> bool, i \<times> i \<times> i \<Rightarrow> bool) tupled_append .
+
code_pred [random_dseq] tupled_append .
thm tupled_append.equation
--- a/src/HOL/Quotient.thy Wed Aug 25 11:13:27 2010 +0200
+++ b/src/HOL/Quotient.thy Wed Aug 25 11:13:58 2010 +0200
@@ -571,7 +571,8 @@
apply metis
done
-lemma bex1_bexeq_reg: "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bex1_rel R (\<lambda>x. P x))"
+lemma bex1_bexeq_reg:
+ shows "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bex1_rel R (\<lambda>x. P x))"
apply (simp add: Ex1_def Bex1_rel_def in_respects)
apply clarify
apply auto
@@ -582,6 +583,23 @@
apply auto
done
+lemma bex1_bexeq_reg_eqv:
+ assumes a: "equivp R"
+ shows "(\<exists>!x. P x) \<longrightarrow> Bex1_rel R P"
+ using equivp_reflp[OF a]
+ apply (intro impI)
+ apply (elim ex1E)
+ apply (rule mp[OF bex1_bexeq_reg])
+ apply (rule_tac a="x" in ex1I)
+ apply (subst in_respects)
+ apply (rule conjI)
+ apply assumption
+ apply assumption
+ apply clarify
+ apply (erule_tac x="xa" in allE)
+ apply simp
+ done
+
subsection {* Various respects and preserve lemmas *}
lemma quot_rel_rsp:
--- a/src/HOL/Tools/ATP/atp_systems.ML Wed Aug 25 11:13:27 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Aug 25 11:13:58 2010 +0200
@@ -136,7 +136,8 @@
{exec = ("E_HOME", "eproof"),
required_execs = [],
arguments = fn _ => fn timeout =>
- "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^
+ "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent \
+ \--soft-cpu-limit=" ^
string_of_int (to_generous_secs timeout),
has_incomplete_mode = false,
proof_delims = [tstp_proof_delims],
@@ -149,7 +150,7 @@
"# Cannot determine problem status within resource limit"),
(OutOfResources, "SZS status: ResourceOut"),
(OutOfResources, "SZS status ResourceOut")],
- default_max_relevant_per_iter = 60 (* FUDGE *),
+ default_max_relevant_per_iter = 80 (* FUDGE *),
default_theory_relevant = false,
explicit_forall = false,
use_conjecture_for_hypotheses = true}
@@ -176,7 +177,7 @@
(MalformedInput, "Undefined symbol"),
(MalformedInput, "Free Variable"),
(SpassTooOld, "tptp2dfg")],
- default_max_relevant_per_iter = 32 (* FUDGE *),
+ default_max_relevant_per_iter = 40 (* FUDGE *),
default_theory_relevant = true,
explicit_forall = true,
use_conjecture_for_hypotheses = true}
@@ -228,24 +229,30 @@
fun refresh_systems_on_tptp () =
Synchronized.change systems (fn _ => get_systems ())
-fun get_system prefix =
+fun find_system name [] systems = find_first (String.isPrefix name) systems
+ | find_system name (version :: versions) systems =
+ case find_first (String.isPrefix (name ^ "---" ^ version)) systems of
+ NONE => find_system name versions systems
+ | res => res
+
+fun get_system name versions =
Synchronized.change_result systems
(fn systems => (if null systems then get_systems () else systems)
- |> `(find_first (String.isPrefix prefix)))
+ |> `(find_system name versions))
-fun the_system prefix =
- (case get_system prefix of
- NONE => error ("System " ^ quote prefix ^ " not available at SystemOnTPTP.")
- | SOME sys => sys);
+fun the_system name versions =
+ case get_system name versions of
+ NONE => error ("System " ^ quote name ^ " not available at SystemOnTPTP.")
+ | SOME sys => sys
-fun remote_config system_prefix proof_delims known_failures
+fun remote_config system_name system_versions proof_delims known_failures
default_max_relevant_per_iter default_theory_relevant
use_conjecture_for_hypotheses =
{exec = ("ISABELLE_ATP", "scripts/remote_atp"),
required_execs = [],
arguments = fn _ => fn timeout =>
" -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^
- the_system system_prefix,
+ the_system system_name system_versions,
has_incomplete_mode = false,
proof_delims = insert (op =) tstp_proof_delims proof_delims,
known_failures =
@@ -256,32 +263,32 @@
explicit_forall = true,
use_conjecture_for_hypotheses = use_conjecture_for_hypotheses}
-fun remotify_config system_prefix
+fun remotify_config system_name system_versions
({proof_delims, known_failures, default_max_relevant_per_iter,
default_theory_relevant, use_conjecture_for_hypotheses, ...}
: prover_config) : prover_config =
- remote_config system_prefix proof_delims known_failures
+ remote_config system_name system_versions proof_delims known_failures
default_max_relevant_per_iter default_theory_relevant
use_conjecture_for_hypotheses
val remotify_name = prefix "remote_"
-fun remote_prover name system_prefix proof_delims known_failures
+fun remote_prover name system_name system_versions proof_delims known_failures
default_max_relevant_per_iter default_theory_relevant
use_conjecture_for_hypotheses =
(remotify_name name,
- remote_config system_prefix proof_delims known_failures
+ remote_config system_name system_versions proof_delims known_failures
default_max_relevant_per_iter default_theory_relevant
use_conjecture_for_hypotheses)
-fun remotify_prover (name, config) system_prefix =
- (remotify_name name, remotify_config system_prefix config)
+fun remotify_prover (name, config) system_name system_versions =
+ (remotify_name name, remotify_config system_name system_versions config)
-val remote_e = remotify_prover e "EP---"
-val remote_vampire = remotify_prover vampire "Vampire---9"
+val remote_e = remotify_prover e "EP" ["1.0", "1.1", "1.2"]
+val remote_vampire = remotify_prover vampire "Vampire" ["9.9", "0.6", "1.0"]
val remote_sine_e =
- remote_prover "sine_e" "SInE---" []
+ remote_prover "sine_e" "SInE" [] []
[(Unprovable, "says Unknown")] 150 (* FUDGE *) false true
val remote_snark =
- remote_prover "snark" "SNARK---" [("refutation.", "end_refutation.")] []
+ remote_prover "snark" "SNARK---" [] [("refutation.", "end_refutation.")] []
50 (* FUDGE *) false true
(* Setup *)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Wed Aug 25 11:13:27 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Wed Aug 25 11:13:58 2010 +0200
@@ -200,10 +200,10 @@
(Args.$$$ "i" >> K Input || Args.$$$ "o" >> K Output ||
Args.$$$ "bool" >> K Bool || Args.$$$ "(" |-- parse_mode_expr --| Args.$$$ ")") xs
and parse_mode_tuple_expr xs =
- (parse_mode_basic_expr --| Args.$$$ "*" -- parse_mode_tuple_expr >> Pair || parse_mode_basic_expr)
+ (parse_mode_basic_expr --| (Args.$$$ "*" || Args.$$$ "\<times>") -- parse_mode_tuple_expr >> Pair || parse_mode_basic_expr)
xs
and parse_mode_expr xs =
- (parse_mode_tuple_expr --| Args.$$$ "=>" -- parse_mode_expr >> Fun || parse_mode_tuple_expr) xs
+ (parse_mode_tuple_expr --| (Args.$$$ "=>" || Args.$$$ "\<Rightarrow>") -- parse_mode_expr >> Fun || parse_mode_tuple_expr) xs
val mode_and_opt_proposal = parse_mode_expr --
Scan.optional (Args.$$$ "as" |-- Parse.xname >> SOME) NONE
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Wed Aug 25 11:13:27 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Wed Aug 25 11:13:58 2010 +0200
@@ -686,8 +686,8 @@
rthm
|> asm_full_simplify ss
|> Drule.eta_contraction_rule
- val ((_, [rthm'']), ctxt') = Variable.import false [rthm'] ctxt
- val goal = derive_qtrm ctxt qtys (prop_of rthm'')
+ val ((_, [rthm'']), ctxt') = Variable.import true [rthm'] ctxt
+ val goal = derive_qtrm ctxt' qtys (prop_of rthm'')
in
Goal.prove ctxt' [] [] goal
(K ((asm_full_simp_tac ss THEN' lift_single_tac ctxt' rthm') 1))
--- a/src/HOL/Tools/Quotient/quotient_term.ML Wed Aug 25 11:13:27 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Wed Aug 25 11:13:58 2010 +0200
@@ -225,12 +225,16 @@
val qtyenv = match ctxt absrep_match_err qty_pat qty
val args_aux = map (double_lookup rtyenv qtyenv) vs
val args = map (absrep_fun flag ctxt) args_aux
- val map_fun = mk_mapfun ctxt vs rty_pat
- val result = list_comb (map_fun, args)
in
if forall is_identity args
then absrep_const flag ctxt s'
- else mk_fun_compose flag (absrep_const flag ctxt s', result)
+ else
+ let
+ val map_fun = mk_mapfun ctxt vs rty_pat
+ val result = list_comb (map_fun, args)
+ in
+ mk_fun_compose flag (absrep_const flag ctxt s', result)
+ end
end
| (TFree x, TFree x') =>
if x = x'
@@ -332,14 +336,18 @@
val qtyenv = match ctxt equiv_match_err qty_pat qty
val args_aux = map (double_lookup rtyenv qtyenv) vs
val args = map (equiv_relation ctxt) args_aux
- val rel_map = mk_relmap ctxt vs rty_pat
- val result = list_comb (rel_map, args)
val eqv_rel = get_equiv_rel ctxt s'
val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool})
in
if forall is_eq args
then eqv_rel'
- else mk_rel_compose (result, eqv_rel')
+ else
+ let
+ val rel_map = mk_relmap ctxt vs rty_pat
+ val result = list_comb (rel_map, args)
+ in
+ mk_rel_compose (result, eqv_rel')
+ end
end
| _ => HOLogic.eq_const rty
@@ -740,10 +748,14 @@
false: raw -> quotient
*)
fun mk_ty_subst qtys direction ctxt =
+let
+ val thy = ProofContext.theory_of ctxt
+in
Quotient_Info.quotdata_dest ctxt
|> map (fn x => (#rtyp x, #qtyp x))
- |> filter (fn (_, qty) => member (op =) qtys qty)
+ |> filter (fn (_, qty) => member (Sign.typ_instance thy o swap) qtys qty)
|> map (if direction then swap else I)
+end
fun mk_trm_subst qtys direction ctxt =
let
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Wed Aug 25 11:13:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Wed Aug 25 11:13:58 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 Wed Aug 25 11:13:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Aug 25 11:13:58 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 *)
@@ -229,9 +234,7 @@
case axioms of
SOME axioms => axioms
| NONE =>
- (print_d (fn () => "Selecting relevant facts for " ^ quote atp_name ^
- ".");
- relevant_facts full_types relevance_threshold relevance_convergence
+ (relevant_facts full_types relevance_threshold relevance_convergence
defs_relevant
(the_default default_max_relevant_per_iter
max_relevant_per_iter)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Aug 25 11:13:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Aug 25 11:13:58 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 *)
@@ -66,8 +64,8 @@
| match_types (a1::as1) (a2::as2) = match_type a1 a2 andalso match_types as1 as2;
(*Is there a unifiable constant?*)
-fun uni_mem goal_const_tab (c, c_typ) =
- exists (match_types c_typ) (these (Symtab.lookup goal_const_tab c))
+fun const_mem const_tab (c, c_typ) =
+ exists (match_types c_typ) (these (Symtab.lookup const_tab c))
(*Maps a "real" type to a const_typ*)
fun const_typ_of (Type (c,typs)) = CType (c, map const_typ_of typs)
@@ -82,36 +80,38 @@
(*Add a const/type pair to the table, but a [] entry means a standard connective,
which we ignore.*)
-fun add_const_type_to_table (c, ctyps) =
+fun add_const_to_table (c, ctyps) =
Symtab.map_default (c, [ctyps])
(fn [] => [] | ctypss => insert (op =) ctyps ctypss)
+fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
+
val fresh_prefix = "Sledgehammer.FRESH."
val flip = Option.map not
(* These are typically simplified away by "Meson.presimplify". *)
-val boring_consts = [@{const_name If}, @{const_name Let}]
+val boring_consts =
+ [@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let}]
-fun get_consts_typs thy pos ts =
+fun get_consts thy pos ts =
let
(* We include free variables, as well as constants, to handle locales. For
each quantifiers that must necessarily be skolemized by the ATP, we
introduce a fresh constant to simulate the effect of Skolemization. *)
fun do_term t =
case t of
- Const x => add_const_type_to_table (const_with_typ thy x)
- | Free (s, _) => add_const_type_to_table (s, [])
- | t1 $ t2 => do_term t1 #> do_term t2
+ Const x => add_const_to_table (const_with_typ thy x)
+ | Free (s, _) => add_const_to_table (s, [])
+ | t1 $ t2 => fold do_term [t1, t2]
| Abs (_, _, t') => do_term t'
| _ => I
fun do_quantifier will_surely_be_skolemized body_t =
do_formula pos body_t
#> (if will_surely_be_skolemized then
- add_const_type_to_table (gensym fresh_prefix, [])
+ add_const_to_table (gensym fresh_prefix, [])
else
I)
and do_term_or_formula T =
- if T = @{typ bool} orelse T = @{typ prop} then do_formula NONE
- else do_term
+ if is_formula_type T then do_formula NONE else do_term
and do_formula pos t =
case t of
Const (@{const_name all}, _) $ Abs (_, _, body_t) =>
@@ -207,38 +207,52 @@
(*The frequency of a constant is the sum of those of all instances of its type.*)
fun const_frequency const_tab (c, cts) =
CTtab.fold (fn (cts', m) => match_types cts cts' ? Integer.add m)
- (the (Symtab.lookup const_tab c)
- handle Option.Option => raise Fail ("Const: " ^ c)) 0
+ (the (Symtab.lookup const_tab c)) 0
+ handle Option.Option => 0
+
(* A surprising number of theorems contain only a few significant constants.
These include all induction rules, and other general theorems. *)
(* "log" seems best in practice. A constant function of one ignores the constant
frequencies. *)
-fun log_weight2 (x:real) = 1.0 + 2.0 / Math.ln (x + 1.0)
+fun rel_log (x : real) = 1.0 + 2.0 / Math.ln (x + 1.0)
+fun irrel_log (x : real) = Math.ln (x + 19.0) / 6.4
(* Computes a constant's weight, as determined by its frequency. *)
-val ct_weight = log_weight2 o real oo const_frequency
+val rel_const_weight = rel_log o real oo const_frequency
+val irrel_const_weight = irrel_log o real oo const_frequency
+(* fun irrel_const_weight _ _ = 1.0 FIXME: OLD CODE *)
+fun axiom_weight const_tab relevant_consts axiom_consts =
+ let
+ val (rel, irrel) = List.partition (const_mem relevant_consts) axiom_consts
+ val rel_weight = fold (curry Real.+ o rel_const_weight const_tab) rel 0.0
+ val irrel_weight = fold (curry Real.+ o irrel_const_weight const_tab) irrel 0.0
+ val res = rel_weight / (rel_weight + irrel_weight)
+ in if Real.isFinite res then res else 0.0 end
+
+(* OLD CODE:
(*Relevant constants are weighted according to frequency,
but irrelevant constants are simply counted. Otherwise, Skolem functions,
which are rare, would harm a formula's chances of being picked.*)
-fun formula_weight const_tab gctyps consts_typs =
+fun axiom_weight const_tab relevant_consts axiom_consts =
let
- val rel = filter (uni_mem gctyps) consts_typs
- val rel_weight = fold (curry Real.+ o ct_weight const_tab) rel 0.0
- val res = rel_weight / (rel_weight + real (length consts_typs - length rel))
+ val rel = filter (const_mem relevant_consts) axiom_consts
+ val rel_weight = fold (curry Real.+ o rel_const_weight const_tab) rel 0.0
+ val res = rel_weight / (rel_weight + real (length axiom_consts - length rel))
in if Real.isFinite res then res else 0.0 end
+*)
(*Multiplies out to a list of pairs: 'a * 'b list -> ('a * 'b) list -> ('a * 'b) list*)
-fun add_expand_pairs (x,ys) xys = List.foldl (fn (y,acc) => (x,y)::acc) xys ys;
+fun add_expand_pairs (x, ys) xys = List.foldl (fn (y,acc) => (x,y)::acc) xys ys
-fun consts_typs_of_term thy t =
- Symtab.fold add_expand_pairs (get_consts_typs thy (SOME true) [t]) []
+fun consts_of_term thy t =
+ Symtab.fold add_expand_pairs (get_consts thy (SOME true) [t]) []
-fun pair_consts_typs_axiom theory_relevant thy axiom =
+fun pair_consts_axiom theory_relevant thy axiom =
(axiom, axiom |> snd |> theory_const_prop_of theory_relevant
- |> consts_typs_of_term thy)
+ |> consts_of_term thy)
exception CONST_OR_FREE of unit
@@ -253,8 +267,8 @@
let val (rator,args) = strip_comb lhs
val ct = const_with_typ thy (dest_Const_or_Free rator)
in
- forall is_Var args andalso uni_mem gctypes ct andalso
- subset (op =) (Term.add_vars rhs [], Term.add_vars lhs [])
+ forall is_Var args andalso const_mem gctypes ct andalso
+ subset (op =) (Term.add_vars rhs [], Term.add_vars lhs [])
end
handle CONST_OR_FREE () => false
in
@@ -264,30 +278,34 @@
| _ => 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)
(* Limit the number of new facts, to prevent runaway acceptance. *)
-fun take_best max_new (newpairs : (annotated_thm * real) list) =
- let val nnew = length newpairs in
+fun take_best max_new (new_pairs : (annotated_thm * real) list) =
+ let val nnew = length new_pairs in
if nnew <= max_new then
- (map #1 newpairs, [])
+ (map #1 new_pairs, [])
else
let
- val newpairs = sort compare_pairs newpairs
- val accepted = List.take (newpairs, max_new)
+ val new_pairs = sort compare_pairs new_pairs
+ val accepted = List.take (new_pairs, max_new)
in
trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^
", 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));
- (map #1 accepted, map #1 (List.drop (newpairs, max_new)))
+ 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;
+val threshold_divisor = 2.0
+val ridiculous_threshold = 0.1
+
fun relevance_filter ctxt relevance_threshold relevance_convergence
defs_relevant max_new theory_relevant
({add, del, ...} : relevance_override) axioms goal_ts =
@@ -300,8 +318,7 @@
val thy = ProofContext.theory_of ctxt
val const_tab = fold (count_axiom_consts theory_relevant thy) axioms
Symtab.empty
- val goal_const_tab = get_consts_typs thy (SOME false) goal_ts
- val relevance_threshold = 0.8 * relevance_threshold (* FIXME *)
+ val goal_const_tab = get_consts thy (SOME false) goal_ts
val _ =
trace_msg (fn () => "Initial constants: " ^
commas (goal_const_tab
@@ -310,57 +327,71 @@
|> map fst))
val add_thms = maps (ProofContext.get_fact ctxt) add
val del_thms = maps (ProofContext.get_fact ctxt) del
- fun iter threshold rel_const_tab =
+ fun iter j threshold rel_const_tab =
let
fun relevant ([], rejects) [] =
- (* Nothing was added this iteration: Add "add:" facts. *)
- if null add_thms then
- []
+ (* Nothing was added this iteration. *)
+ if j = 0 andalso threshold >= ridiculous_threshold then
+ (* First iteration? Try again. *)
+ iter 0 (threshold / threshold_divisor) rel_const_tab
+ (map (apsnd SOME) rejects)
else
- map_filter (fn (p as (name, th), _) =>
- if member Thm.eq_thm add_thms th then SOME p
- else NONE) rejects
- | relevant (newpairs, rejects) [] =
+ (* Add "add:" facts. *)
+ if null add_thms then
+ []
+ else
+ map_filter (fn ((p as (_, th), _), _) =>
+ if member Thm.eq_thm add_thms th then SOME p
+ else NONE) rejects
+ | relevant (new_pairs, rejects) [] =
let
- val (newrels, more_rejects) = take_best max_new newpairs
- val new_consts = maps #2 newrels
- val rel_const_tab =
- rel_const_tab |> fold add_const_type_to_table new_consts
+ val (new_rels, more_rejects) = take_best max_new new_pairs
+ val rel_const_tab' =
+ rel_const_tab |> fold add_const_to_table (maps snd new_rels)
+ fun is_dirty c =
+ const_mem rel_const_tab' c andalso
+ not (const_mem rel_const_tab c)
+ val rejects =
+ more_rejects @ rejects
+ |> map (fn (ax as (_, consts), old_weight) =>
+ (ax, if exists is_dirty consts then NONE
+ else SOME old_weight))
val threshold =
- threshold + (1.0 - threshold) / relevance_convergence
+ threshold + (1.0 - threshold) * relevance_convergence
in
trace_msg (fn () => "relevant this iteration: " ^
- Int.toString (length newrels));
- map #1 newrels @ iter threshold rel_const_tab
- (more_rejects @ rejects)
+ Int.toString (length new_rels));
+ map #1 new_rels @ iter (j + 1) threshold rel_const_tab' rejects
end
- | relevant (newrels, rejects)
- ((ax as ((name, th), consts_typs)) :: axs) =
+ | relevant (new_rels, rejects)
+ (((ax as ((name, th), axiom_consts)), cached_weight)
+ :: rest) =
let
val weight =
- if member Thm.eq_thm del_thms th then 0.0
- else formula_weight const_tab rel_const_tab consts_typs
+ case cached_weight of
+ SOME w => w
+ | NONE => axiom_weight const_tab rel_const_tab axiom_consts
in
if weight >= threshold orelse
(defs_relevant andalso defines thy th rel_const_tab) then
(trace_msg (fn () =>
- name ^ " passes: " ^ Real.toString weight
- (* ^ " consts: " ^ commas (map fst consts_typs) *));
- relevant ((ax, weight) :: newrels, rejects) axs)
+ fst (name ()) ^ " passes: " ^ Real.toString weight
+ ^ " consts: " ^ commas (map fst axiom_consts));
+ relevant ((ax, weight) :: new_rels, rejects) rest)
else
- relevant (newrels, ax :: rejects) axs
+ relevant (new_rels, (ax, weight) :: rejects) rest
end
in
trace_msg (fn () => "relevant_facts, current threshold: " ^
Real.toString threshold);
relevant ([], [])
end
- val relevant = iter relevance_threshold goal_const_tab
- (map (pair_consts_typs_axiom theory_relevant thy)
- axioms)
in
- trace_msg (fn () => "Total relevant: " ^ Int.toString (length relevant));
- relevant
+ axioms |> filter_out (member Thm.eq_thm del_thms o snd)
+ |> map (rpair NONE o pair_consts_axiom theory_relevant thy)
+ |> iter 0 relevance_threshold goal_const_tab
+ |> tap (fn res => trace_msg (fn () =>
+ "Total relevant: " ^ Int.toString (length res)))
end
(***************************************************************)
@@ -386,7 +417,9 @@
(* FIXME: put other record thms here, or declare as "no_atp" *)
val multi_base_blacklist =
["defs", "select_defs", "update_defs", "induct", "inducts", "split", "splits",
- "split_asm", "cases", "ext_cases"]
+ "split_asm", "cases", "ext_cases", "eq.simps", "eq.refl", "nchotomy",
+ "case_cong", "weak_case_cong"]
+ |> map (prefix ".")
val max_lambda_nesting = 3
@@ -396,8 +429,6 @@
max = 0 orelse term_has_too_many_lambdas (max - 1) t
| term_has_too_many_lambdas _ _ = false
-fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
-
(* Don't count nested lambdas at the level of formulas, since they are
quantifiers. *)
fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) =
@@ -408,7 +439,7 @@
else
term_has_too_many_lambdas max_lambda_nesting t
-(* The max apply depth of any "metis" call in "Metis_Examples" (on 31-10-2007)
+(* The max apply depth of any "metis" call in "Metis_Examples" (on 2007-10-31)
was 11. *)
val max_apply_depth = 15
@@ -488,9 +519,10 @@
are omitted. *)
fun is_dangerous_term full_types t =
not full_types andalso
- ((has_bound_or_var_of_type dangerous_types t andalso
- has_bound_or_var_of_type dangerous_types (transform_elim_term t))
- orelse is_exhaustive_finite t)
+ let val t = transform_elim_term t in
+ has_bound_or_var_of_type dangerous_types t orelse
+ is_exhaustive_finite t
+ end
fun is_theorem_bad_for_atps full_types thm =
let val t = prop_of thm in
@@ -499,83 +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 valid_facts facts pairs =
- (pairs, []) |-> fold (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
- member (op =) multi_base_blacklist (Long_Name.base_name name) 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
- valid_facts local_facts (unnamed_locals @ named_locals) @
- valid_facts global_facts (Facts.dest_static [] global_facts)
+ [] |> 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 is_named ("", th) =
- (warning ("No name for theorem " ^
- Display.string_of_thm_without_context th); false)
- | is_named _ = true
-fun checked_name_thm_pairs respect_no_atp ctxt =
- name_thm_pairs ctxt respect_no_atp
- #> tap (fn ps => trace_msg
- (fn () => ("Considering " ^ Int.toString (length ps) ^
- " theorems")))
- #> filter is_named
+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 *)
@@ -587,16 +618,23 @@
(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 =
- checked_name_thm_pairs (respect_no_atp andalso not only) ctxt
- (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
+ trace_msg (fn () => "Considering " ^ Int.toString (length axioms) ^
+ " theorems");
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 Wed Aug 25 11:13:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Wed Aug 25 11:13:58 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_isar.ML Wed Aug 25 11:13:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Aug 25 11:13:58 2010 +0200
@@ -67,8 +67,8 @@
("verbose", "false"),
("overlord", "false"),
("explicit_apply", "false"),
- ("relevance_threshold", "50"),
- ("relevance_convergence", "320"),
+ ("relevance_threshold", "40"),
+ ("relevance_convergence", "31"),
("max_relevant_per_iter", "smart"),
("theory_relevant", "smart"),
("defs_relevant", "false"),
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Wed Aug 25 11:13:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Wed Aug 25 11:13:58 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 Wed Aug 25 11:13:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Wed Aug 25 11:13:58 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)
@@ -223,32 +223,32 @@
(["c_COMBB", "c_COMBC"], @{thms COMBB_def COMBC_def}),
(["c_COMBS"], @{thms COMBS_def})]
val optional_typed_helpers =
- [(["c_True", "c_False"], @{thms True_or_False}),
- (["c_If"], @{thms if_True if_False True_or_False})]
+ [(["c_True", "c_False", "c_If"], @{thms True_or_False}),
+ (["c_If"], @{thms if_True if_False})]
val mandatory_helpers = @{thms fequal_def}
val init_counters =
- Symtab.make (maps (maps (map (rpair 0) o fst))
- [optional_helpers, optional_typed_helpers])
+ [optional_helpers, optional_typed_helpers] |> maps (maps fst)
+ |> sort_distinct string_ord |> map (rpair 0) |> Symtab.make
fun get_helper_facts ctxt is_FO full_types conjectures axioms =
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'
@@ -472,7 +472,7 @@
(is_tptp_variable s andalso not (member (op =) bounds name))
? insert (op =) name
#> fold (term_vars bounds) tms
- fun formula_vars bounds (AQuant (q, xs, phi)) =
+ fun formula_vars bounds (AQuant (_, xs, phi)) =
formula_vars (xs @ bounds) phi
| formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
| formula_vars bounds (AAtom tm) = term_vars bounds tm
@@ -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 Wed Aug 25 11:13:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Aug 25 11:13:58 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;
--- a/src/HOL/Tools/inductive.ML Wed Aug 25 11:13:27 2010 +0200
+++ b/src/HOL/Tools/inductive.ML Wed Aug 25 11:13:58 2010 +0200
@@ -195,6 +195,21 @@
+(** equations **)
+
+structure Equation_Data = Generic_Data
+(
+ type T = thm Item_Net.T;
+ val empty = Item_Net.init (op aconv o pairself Thm.prop_of)
+ (single o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of);
+ val extend = I;
+ val merge = Item_Net.merge;
+);
+
+val add_equation = Thm.declaration_attribute (Equation_Data.map o Item_Net.update)
+
+
+
(** misc utilities **)
fun message quiet_mode s = if quiet_mode then () else writeln s;
@@ -548,16 +563,20 @@
fun mk_simp_eq ctxt prop =
let
+ val thy = ProofContext.theory_of ctxt
val ctxt' = Variable.auto_fixes prop ctxt
- val cname = fst (dest_Const (fst (strip_comb (HOLogic.dest_Trueprop prop))))
- val info = the_inductive ctxt cname
- val eq = nth (#eqs (snd info)) (find_index (fn c => c = cname) (#names (fst info)))
- val lhs_eq = fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of eq)))
- val subst = Pattern.match (ProofContext.theory_of ctxt) (lhs_eq, HOLogic.dest_Trueprop prop)
- (Vartab.empty, Vartab.empty)
- val certify = cterm_of (ProofContext.theory_of ctxt)
- val inst = map (fn v => (certify (Var v), certify (Envir.subst_term subst (Var v))))
- (Term.add_vars lhs_eq [])
+ val lhs_of = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of
+ val substs = Item_Net.retrieve (Equation_Data.get (Context.Proof ctxt)) (HOLogic.dest_Trueprop prop)
+ |> map_filter
+ (fn eq => SOME (Pattern.match thy (lhs_of eq, HOLogic.dest_Trueprop prop)
+ (Vartab.empty, Vartab.empty), eq)
+ handle Pattern.MATCH => NONE)
+ val (subst, eq) = case substs of
+ [s] => s
+ | _ => error
+ ("equations matching pattern " ^ Syntax.string_of_term ctxt prop ^ " is not unique")
+ val inst = map (fn v => (cterm_of thy (Var v), cterm_of thy (Envir.subst_term subst (Var v))))
+ (Term.add_vars (lhs_of eq) [])
in
cterm_instantiate inst eq
|> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv
@@ -833,7 +852,8 @@
val (eqs', lthy3) = lthy2 |>
fold_map (fn (name, eq) => Local_Theory.note
- ((Binding.qualify true (Long_Name.base_name name) (Binding.name "simps"), []), [eq])
+ ((Binding.qualify true (Long_Name.base_name name) (Binding.name "simps"),
+ [Attrib.internal (K add_equation)]), [eq])
#> apfst (hd o snd))
(if null eqs then [] else (cnames ~~ eqs))
val (inducts, lthy4) =
--- a/src/HOL/Tools/inductive_set.ML Wed Aug 25 11:13:27 2010 +0200
+++ b/src/HOL/Tools/inductive_set.ML Wed Aug 25 11:13:58 2010 +0200
@@ -477,7 +477,7 @@
eta_contract (member op = cs' orf is_pred pred_arities))) intros;
val cnames_syn' = map (fn (b, _) => (Binding.suffix_name "p" b, NoSyn)) cnames_syn;
val monos' = map (to_pred [] (Context.Proof lthy)) monos;
- val ({preds, intrs, elims, raw_induct, ...}, lthy1) =
+ val ({preds, intrs, elims, raw_induct, eqs, ...}, lthy1) =
Inductive.add_ind_def
{quiet_mode = quiet_mode, verbose = verbose, alt_name = Binding.empty,
coind = coind, no_elim = no_elim, no_ind = no_ind,
@@ -520,14 +520,13 @@
val cnames = map (Local_Theory.full_name lthy3 o #1) cnames_syn; (* FIXME *)
val (intr_names, intr_atts) = split_list (map fst intros);
val raw_induct' = to_set [] (Context.Proof lthy3) raw_induct;
- val eqs = [] (* TODO: define equations *)
val (intrs', elims', eqs', induct, inducts, lthy4) =
Inductive.declare_rules rec_name coind no_ind cnames (map fst defs)
(map (to_set [] (Context.Proof lthy3)) intrs) intr_names intr_atts
(map (fn th => (to_set [] (Context.Proof lthy3) th,
map fst (fst (Rule_Cases.get th)),
Rule_Cases.get_constraints th)) elims)
- eqs raw_induct' lthy3;
+ (map (to_set [] (Context.Proof lthy3)) eqs) raw_induct' lthy3;
in
({intrs = intrs', elims = elims', induct = induct, inducts = inducts,
raw_induct = raw_induct', preds = map fst defs, eqs = eqs'},
--- a/src/Pure/Isar/code.ML Wed Aug 25 11:13:27 2010 +0200
+++ b/src/Pure/Isar/code.ML Wed Aug 25 11:13:58 2010 +0200
@@ -78,7 +78,6 @@
(*infrastructure*)
val set_code_target_attr: (string -> thm -> theory -> theory) -> theory -> theory
- val purge_data: theory -> theory
end;
signature CODE_DATA_ARGS =
@@ -266,8 +265,6 @@
fun map_exec_purge f = Code_Data.map (fn (exec, _) => (f exec, empty_dataref ()));
-val purge_data = (Code_Data.map o apsnd) (fn _ => empty_dataref ());
-
fun change_fun_spec delete c f = (map_exec_purge o map_functions
o (if delete then Symtab.map_entry c else Symtab.map_default (c, ((false, empty_fun_spec), [])))
o apfst) (fn (_, spec) => (true, f spec));
--- a/src/Pure/conv.ML Wed Aug 25 11:13:27 2010 +0200
+++ b/src/Pure/conv.ML Wed Aug 25 11:13:58 2010 +0200
@@ -48,6 +48,7 @@
val concl_conv: int -> conv -> conv
val fconv_rule: conv -> thm -> thm
val gconv_rule: conv -> int -> thm -> thm
+ val tap_thy: (theory -> conv) -> conv
end;
structure Conv: CONV =
@@ -211,6 +212,9 @@
end
| NONE => raise THM ("gconv_rule", i, [th]));
+
+fun tap_thy conv ct = conv (Thm.theory_of_cterm ct) ct;
+
end;
structure Basic_Conv: BASIC_CONV = Conv;
--- a/src/Tools/Code/code_eval.ML Wed Aug 25 11:13:27 2010 +0200
+++ b/src/Tools/Code/code_eval.ML Wed Aug 25 11:13:58 2010 +0200
@@ -62,7 +62,7 @@
val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
^ space_implode " " (map (enclose "(" ")") args) ^ " end";
in ML_Context.evaluate ctxt false reff sml_code end;
- in Code_Thingol.eval thy postproc evaluator t end;
+ in Code_Thingol.dynamic_eval_value thy postproc evaluator t end;
(** instrumentalization by antiquotation **)
--- a/src/Tools/Code/code_haskell.ML Wed Aug 25 11:13:27 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML Wed Aug 25 11:13:58 2010 +0200
@@ -395,8 +395,8 @@
end
in
Code_Target.mk_serialization target
- (fn NONE => K () o map (code_writeln o snd) | SOME file => K () o map
- (write_module (check_destination file)))
+ (fn NONE => K () o map (code_writeln o (fn p => Pretty.block [p, Pretty.fbrk]) o snd)
+ | SOME file => K () o map (write_module (check_destination file)))
(rpair [] o cat_lines o map (code_of_pretty o snd))
(map (uncurry print_module) includes
@ map serialize_module (Symtab.dest hs_program))
--- a/src/Tools/Code/code_preproc.ML Wed Aug 25 11:13:27 2010 +0200
+++ b/src/Tools/Code/code_preproc.ML Wed Aug 25 11:13:58 2010 +0200
@@ -24,11 +24,12 @@
val all: code_graph -> string list
val pretty: theory -> code_graph -> Pretty.T
val obtain: theory -> string list -> term list -> code_algebra * code_graph
- val eval_conv: theory
- -> (code_algebra -> code_graph -> (string * sort) list -> term -> cterm -> thm) -> cterm -> thm
- val eval: theory -> ((term -> term) -> 'a -> 'a)
+ val dynamic_eval_conv: theory
+ -> (code_algebra -> code_graph -> (string * sort) list -> term -> conv) -> conv
+ val dynamic_eval_value: theory -> ((term -> term) -> 'a -> 'a)
-> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a
- val pre_post_conv: theory -> (cterm -> thm) -> cterm -> thm
+ val static_eval_conv: theory -> string list
+ -> (code_algebra -> code_graph -> (string * sort) list -> term -> conv) -> conv
val setup: theory -> theory
end
@@ -74,8 +75,7 @@
if AList.defined (op =) xs key then AList.delete (op =) key xs
else error ("No such " ^ msg ^ ": " ^ quote key);
-fun map_data f = Code.purge_data
- #> (Code_Preproc_Data.map o map_thmproc) f;
+val map_data = Code_Preproc_Data.map o map_thmproc;
val map_pre_post = map_data o apfst;
val map_pre = map_pre_post o apfst;
@@ -422,10 +422,12 @@
(** retrieval and evaluation interfaces **)
-fun obtain thy cs ts = apsnd snd
- (Wellsorted.change_yield thy (extend_arities_eqngr thy cs ts));
+fun obtain thy consts ts = apsnd snd
+ (Wellsorted.change_yield thy (extend_arities_eqngr thy consts ts));
-fun gen_eval thy cterm_of conclude_evaluation evaluator proto_ct =
+fun dest_cterm ct = let val t = Thm.term_of ct in (Term.add_tfrees t [], t) end;
+
+fun dynamic_eval thy cterm_of conclude_evaluation evaluator proto_ct =
let
val pp = Syntax.pp_global thy;
val ct = cterm_of proto_ct;
@@ -433,17 +435,13 @@
(Thm.term_of ct);
val thm = preprocess_conv thy ct;
val ct' = Thm.rhs_of thm;
- val t' = Thm.term_of ct';
- val vs = Term.add_tfrees t' [];
+ val (vs', t') = dest_cterm ct';
val consts = fold_aterms
(fn Const (c, _) => insert (op =) c | _ => I) t' [];
val (algebra', eqngr') = obtain thy consts [t'];
- in conclude_evaluation (evaluator algebra' eqngr' vs t' ct') thm end;
+ in conclude_evaluation (evaluator algebra' eqngr' vs' t' ct') thm end;
-fun simple_evaluator evaluator algebra eqngr vs t ct =
- evaluator algebra eqngr vs t;
-
-fun eval_conv thy =
+fun dynamic_eval_conv thy =
let
fun conclude_evaluation thm2 thm1 =
let
@@ -453,12 +451,22 @@
error ("could not construct evaluation proof:\n"
^ (cat_lines o map (Display.string_of_thm_global thy)) [thm1, thm2, thm3])
end;
- in gen_eval thy I conclude_evaluation end;
+ in dynamic_eval thy I conclude_evaluation end;
+
+fun dynamic_eval_value thy postproc evaluator = dynamic_eval thy (Thm.cterm_of thy)
+ (K o postproc (postprocess_term thy)) (K oooo evaluator);
-fun eval thy postproc evaluator = gen_eval thy (Thm.cterm_of thy)
- (K o postproc (postprocess_term thy)) (simple_evaluator evaluator);
-
-fun pre_post_conv thy conv = (preprocess_conv thy) then_conv conv then_conv (postprocess_conv thy);
+fun static_eval_conv thy consts conv =
+ let
+ val (algebra, eqngr) = obtain thy consts [];
+ fun conv' ct =
+ let
+ val (vs, t) = dest_cterm ct;
+ in
+ Conv.tap_thy (fn thy => (preprocess_conv thy)
+ then_conv (conv algebra eqngr vs t) then_conv (postprocess_conv thy)) ct
+ end;
+ in conv' end;
(** setup **)
--- a/src/Tools/Code/code_simp.ML Wed Aug 25 11:13:27 2010 +0200
+++ b/src/Tools/Code/code_simp.ML Wed Aug 25 11:13:58 2010 +0200
@@ -8,11 +8,11 @@
sig
val no_frees_conv: conv -> conv
val map_ss: (simpset -> simpset) -> theory -> theory
- val current_conv: theory -> conv
- val current_tac: theory -> int -> tactic
- val current_value: theory -> term -> term
- val make_conv: theory -> simpset option -> string list -> conv
- val make_tac: theory -> simpset option -> string list -> int -> tactic
+ val dynamic_eval_conv: theory -> conv
+ val dynamic_eval_tac: theory -> int -> tactic
+ val dynamic_eval_value: theory -> term -> term
+ val static_eval_conv: theory -> simpset option -> string list -> conv
+ val static_eval_tac: theory -> simpset option -> string list -> int -> tactic
val setup: theory -> theory
end;
@@ -67,25 +67,25 @@
(* evaluation with current code context *)
-fun current_conv thy = no_frees_conv (Code_Thingol.eval_conv thy
+fun dynamic_eval_conv thy = no_frees_conv (Code_Thingol.dynamic_eval_conv thy
(fn naming => fn program => fn t => fn deps => rewrite_modulo thy NONE program));
-fun current_tac thy = CONVERSION (current_conv thy) THEN' conclude_tac thy NONE;
+fun dynamic_eval_tac thy = CONVERSION (dynamic_eval_conv thy) THEN' conclude_tac thy NONE;
-fun current_value thy = snd o Logic.dest_equals o Thm.prop_of o current_conv thy o Thm.cterm_of thy;
+fun dynamic_eval_value thy = snd o Logic.dest_equals o Thm.prop_of o dynamic_eval_conv thy o Thm.cterm_of thy;
val setup = Method.setup (Binding.name "code_simp")
- (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo current_tac o ProofContext.theory_of)))
+ (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_eval_tac o ProofContext.theory_of)))
"simplification with code equations"
- #> Value.add_evaluator ("simp", current_value o ProofContext.theory_of);
+ #> Value.add_evaluator ("simp", dynamic_eval_value o ProofContext.theory_of);
(* evaluation with freezed code context *)
-fun make_conv thy some_ss consts = no_frees_conv (Code_Preproc.pre_post_conv thy
- ((rewrite_modulo thy some_ss o snd o snd o Code_Thingol.consts_program thy false) consts));
+fun static_eval_conv thy some_ss consts = no_frees_conv
+ (Code_Thingol.static_eval_conv_simple thy consts (rewrite_modulo thy some_ss));
-fun make_tac thy some_ss consts = CONVERSION (make_conv thy some_ss consts)
+fun static_eval_tac thy some_ss consts = CONVERSION (static_eval_conv thy some_ss consts)
THEN' conclude_tac thy some_ss;
end;
--- a/src/Tools/Code/code_thingol.ML Wed Aug 25 11:13:27 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML Wed Aug 25 11:13:58 2010 +0200
@@ -92,12 +92,17 @@
val read_const_exprs: theory -> string list -> string list * string list
val consts_program: theory -> bool -> string list -> string list * (naming * program)
- val eval_conv: theory
- -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> cterm -> thm)
- -> cterm -> thm
- val eval: theory -> ((term -> term) -> 'a -> 'a)
+ val dynamic_eval_conv: theory
+ -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> conv)
+ -> conv
+ val dynamic_eval_value: theory -> ((term -> term) -> 'a -> 'a)
-> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
-> term -> 'a
+ val static_eval_conv: theory -> string list
+ -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> conv)
+ -> conv
+ val static_eval_conv_simple: theory -> string list
+ -> (program -> conv) -> conv
end;
structure Code_Thingol: CODE_THINGOL =
@@ -846,7 +851,7 @@
fun consts_program thy permissive cs =
let
- fun project_consts cs (naming, program) =
+ fun project_consts cs (naming, program) = (*FIXME only necessary for cache_generation*)
let
val cs_all = Graph.all_succs program cs;
in (cs, (naming, Graph.subgraph (member (op =) cs_all) program)) end;
@@ -895,8 +900,17 @@
val vs'' = map (fn (v, _) => (v, (the o AList.lookup (op =) vs o prefix "'") v)) vs';
in evaluator naming program ((vs'', (vs', ty')), t') deps end;
-fun eval_conv thy = Code_Preproc.eval_conv thy o base_evaluator thy;
-fun eval thy postproc = Code_Preproc.eval thy postproc o base_evaluator thy;
+fun dynamic_eval_conv thy = Code_Preproc.dynamic_eval_conv thy o base_evaluator thy;
+fun dynamic_eval_value thy postproc = Code_Preproc.dynamic_eval_value thy postproc o base_evaluator thy;
+
+fun static_eval_conv thy consts conv =
+ Code_Preproc.static_eval_conv thy consts (base_evaluator thy conv); (*FIXME avoid re-generation*)
+
+fun static_eval_conv_simple thy consts conv =
+ Code_Preproc.static_eval_conv thy consts (fn algebra => fn eqngr => fn _ => fn _ => fn ct =>
+ conv ((NONE, (empty_naming, Graph.empty)) (*FIXME provide abstraction for this kind of invocation*)
+ |> fold_map (ensure_const thy algebra eqngr false) consts
+ |> (snd o snd o snd)) ct);
(** diagnostic commands **)
--- a/src/Tools/nbe.ML Wed Aug 25 11:13:27 2010 +0200
+++ b/src/Tools/nbe.ML Wed Aug 25 11:13:58 2010 +0200
@@ -6,8 +6,8 @@
signature NBE =
sig
- val norm_conv: cterm -> thm
- val norm: theory -> term -> term
+ val dynamic_eval_conv: conv
+ val dynamic_eval_value: theory -> term -> term
datatype Univ =
Const of int * Univ list (*named (uninterpreted) constants*)
@@ -530,12 +530,12 @@
(* compilation, evaluation and reification *)
-fun compile_eval thy program vs_t deps =
+fun compile_eval thy program =
let
val ctxt = ProofContext.init_global thy;
val (gr, (_, idx_tab)) =
Nbe_Functions.change thy (ensure_stmts ctxt program);
- in
+ in fn vs_t => fn deps =>
vs_t
|> eval_term ctxt gr deps
|> term_of_univ thy program idx_tab
@@ -574,12 +574,11 @@
val rhs = Thm.cterm_of thy raw_rhs;
in Thm.mk_binop eq lhs rhs end;
-val (_, raw_norm_oracle) = Context.>>> (Context.map_theory_result
+val (_, raw_oracle) = Context.>>> (Context.map_theory_result
(Thm.add_oracle (Binding.name "norm", fn (thy, program, vsp_ty_t, deps, ct) =>
mk_equals thy ct (normalize thy program vsp_ty_t deps))));
-fun norm_oracle thy program vsp_ty_t deps ct =
- raw_norm_oracle (thy, program, vsp_ty_t, deps, ct);
+fun oracle thy program vsp_ty_t deps ct = raw_oracle (thy, program, vsp_ty_t, deps, ct);
fun no_frees_rew rew t =
let
@@ -588,15 +587,14 @@
t
|> fold_rev lambda frees
|> rew
- |> (fn t' => Term.betapplys (t', frees))
+ |> curry (Term.betapplys o swap) frees
end;
-val norm_conv = Code_Simp.no_frees_conv (fn ct =>
- let
- val thy = Thm.theory_of_cterm ct;
- in lift_triv_classes_conv thy (Code_Thingol.eval_conv thy (K (norm_oracle thy))) ct end);
+val dynamic_eval_conv = Code_Simp.no_frees_conv (Conv.tap_thy
+ (fn thy => lift_triv_classes_conv thy (Code_Thingol.dynamic_eval_conv thy (K (oracle thy)))));
-fun norm thy = lift_triv_classes_rew thy (no_frees_rew (Code_Thingol.eval thy I (K (normalize thy))));
+fun dynamic_eval_value thy = lift_triv_classes_rew thy
+ (no_frees_rew (Code_Thingol.dynamic_eval_value thy I (K (normalize thy))));
(* evaluation command *)
@@ -604,7 +602,7 @@
fun norm_print_term ctxt modes t =
let
val thy = ProofContext.theory_of ctxt;
- val t' = norm thy t;
+ val t' = dynamic_eval_value thy t;
val ty' = Term.type_of t';
val ctxt' = Variable.auto_fixes t ctxt;
val p = Print_Mode.with_modes modes (fn () =>
@@ -619,7 +617,7 @@
let val ctxt = Toplevel.context_of state
in norm_print_term ctxt modes (Syntax.read_term ctxt s) end;
-val setup = Value.add_evaluator ("nbe", norm o ProofContext.theory_of);
+val setup = Value.add_evaluator ("nbe", dynamic_eval_value o ProofContext.theory_of);
val opt_modes =
Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) [];