# HG changeset patch # User hoelzl # Date 1282727408 -7200 # Node ID 622a620a64745599746218f3f2949faccc5ce186 # Parent 0e2596019119dc57db7e58c43f5b03c597c3aee7# Parent aaee86c0e2373d97f239dd76429df00f2623576c merged diff -r aaee86c0e237 -r 622a620a6474 doc-src/Sledgehammer/sledgehammer.tex --- a/doc-src/Sledgehammer/sledgehammer.tex Tue Aug 24 14:41:37 2010 +0200 +++ b/doc-src/Sledgehammer/sledgehammer.tex Wed Aug 25 11:10:08 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}} diff -r aaee86c0e237 -r 622a620a6474 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Tue Aug 24 14:41:37 2010 +0200 +++ b/src/HOL/HOL.thy Wed Aug 25 11:10:08 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" diff -r aaee86c0e237 -r 622a620a6474 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Aug 24 14:41:37 2010 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Aug 25 11:10:08 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 diff -r aaee86c0e237 -r 622a620a6474 src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Tue Aug 24 14:41:37 2010 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Wed Aug 25 11:10:08 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 \ 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 [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 \ i \ o \ bool, o \ o \ i \ bool, o \ i \ i \ bool, + i \ o \ i \ bool, i \ i \ i \ bool) tupled_append . + code_pred [random_dseq] tupled_append . thm tupled_append.equation diff -r aaee86c0e237 -r 622a620a6474 src/HOL/Quotient.thy --- a/src/HOL/Quotient.thy Tue Aug 24 14:41:37 2010 +0200 +++ b/src/HOL/Quotient.thy Wed Aug 25 11:10:08 2010 +0200 @@ -571,7 +571,8 @@ apply metis done -lemma bex1_bexeq_reg: "(\!x\Respects R. P x) \ (Bex1_rel R (\x. P x))" +lemma bex1_bexeq_reg: + shows "(\!x\Respects R. P x) \ (Bex1_rel R (\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 "(\!x. P x) \ 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: diff -r aaee86c0e237 -r 622a620a6474 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 24 14:41:37 2010 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Aug 25 11:10:08 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 *) diff -r aaee86c0e237 -r 622a620a6474 src/HOL/Tools/Predicate_Compile/predicate_compile.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Tue Aug 24 14:41:37 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Wed Aug 25 11:10:08 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.$$$ "\") -- 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.$$$ "\") -- 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 diff -r aaee86c0e237 -r 622a620a6474 src/HOL/Tools/Quotient/quotient_tacs.ML --- a/src/HOL/Tools/Quotient/quotient_tacs.ML Tue Aug 24 14:41:37 2010 +0200 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Wed Aug 25 11:10:08 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)) diff -r aaee86c0e237 -r 622a620a6474 src/HOL/Tools/Quotient/quotient_term.ML --- a/src/HOL/Tools/Quotient/quotient_term.ML Tue Aug 24 14:41:37 2010 +0200 +++ b/src/HOL/Tools/Quotient/quotient_term.ML Wed Aug 25 11:10:08 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 diff -r aaee86c0e237 -r 622a620a6474 src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Tue Aug 24 14:41:37 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Wed Aug 25 11:10:08 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 diff -r aaee86c0e237 -r 622a620a6474 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Aug 24 14:41:37 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Aug 25 11:10:08 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) diff -r aaee86c0e237 -r 622a620a6474 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Aug 24 14:41:37 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Aug 25 11:10:08 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; diff -r aaee86c0e237 -r 622a620a6474 src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Tue Aug 24 14:41:37 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Wed Aug 25 11:10:08 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!" diff -r aaee86c0e237 -r 622a620a6474 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Aug 24 14:41:37 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Aug 25 11:10:08 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"), diff -r aaee86c0e237 -r 622a620a6474 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Aug 24 14:41:37 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Wed Aug 25 11:10:08 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)) = diff -r aaee86c0e237 -r 622a620a6474 src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Tue Aug 24 14:41:37 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Wed Aug 25 11:10:08 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 diff -r aaee86c0e237 -r 622a620a6474 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue Aug 24 14:41:37 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Aug 25 11:10:08 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; diff -r aaee86c0e237 -r 622a620a6474 src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Tue Aug 24 14:41:37 2010 +0200 +++ b/src/HOL/Tools/inductive.ML Wed Aug 25 11:10:08 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) = diff -r aaee86c0e237 -r 622a620a6474 src/HOL/Tools/inductive_set.ML --- a/src/HOL/Tools/inductive_set.ML Tue Aug 24 14:41:37 2010 +0200 +++ b/src/HOL/Tools/inductive_set.ML Wed Aug 25 11:10:08 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'}, diff -r aaee86c0e237 -r 622a620a6474 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Tue Aug 24 14:41:37 2010 +0200 +++ b/src/Pure/Isar/code.ML Wed Aug 25 11:10:08 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)); diff -r aaee86c0e237 -r 622a620a6474 src/Pure/conv.ML --- a/src/Pure/conv.ML Tue Aug 24 14:41:37 2010 +0200 +++ b/src/Pure/conv.ML Wed Aug 25 11:10:08 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; diff -r aaee86c0e237 -r 622a620a6474 src/Tools/Code/code_eval.ML --- a/src/Tools/Code/code_eval.ML Tue Aug 24 14:41:37 2010 +0200 +++ b/src/Tools/Code/code_eval.ML Wed Aug 25 11:10:08 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 **) diff -r aaee86c0e237 -r 622a620a6474 src/Tools/Code/code_haskell.ML --- a/src/Tools/Code/code_haskell.ML Tue Aug 24 14:41:37 2010 +0200 +++ b/src/Tools/Code/code_haskell.ML Wed Aug 25 11:10:08 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)) diff -r aaee86c0e237 -r 622a620a6474 src/Tools/Code/code_preproc.ML --- a/src/Tools/Code/code_preproc.ML Tue Aug 24 14:41:37 2010 +0200 +++ b/src/Tools/Code/code_preproc.ML Wed Aug 25 11:10:08 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 **) diff -r aaee86c0e237 -r 622a620a6474 src/Tools/Code/code_simp.ML --- a/src/Tools/Code/code_simp.ML Tue Aug 24 14:41:37 2010 +0200 +++ b/src/Tools/Code/code_simp.ML Wed Aug 25 11:10:08 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; diff -r aaee86c0e237 -r 622a620a6474 src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Tue Aug 24 14:41:37 2010 +0200 +++ b/src/Tools/Code/code_thingol.ML Wed Aug 25 11:10:08 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 **) diff -r aaee86c0e237 -r 622a620a6474 src/Tools/nbe.ML --- a/src/Tools/nbe.ML Tue Aug 24 14:41:37 2010 +0200 +++ b/src/Tools/nbe.ML Wed Aug 25 11:10:08 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.$$$ ")")) [];