# HG changeset patch # User blanchet # Date 1277226612 -7200 # Node ID f9af8a863bd3bd7eff6e75f24dd6075351a0dbe9 # Parent 9de1add14bac1fb496481415608be53935f3b833# Parent de91b800c34e98021fd691091f6762f079d3148c merged diff -r 9de1add14bac -r f9af8a863bd3 doc-src/Sledgehammer/sledgehammer.tex --- a/doc-src/Sledgehammer/sledgehammer.tex Tue Jun 22 18:15:44 2010 +0200 +++ b/doc-src/Sledgehammer/sledgehammer.tex Tue Jun 22 19:10:12 2010 +0200 @@ -341,11 +341,6 @@ download page. Sledgehammer requires version 3.5 or above. See \S\ref{installation} for details. -\item[$\bullet$] \textbf{\textit{spass\_dfg}:} Same as the above, except that -Sledgehammer communicates with SPASS using the native DFG syntax rather than the -TPTP syntax. Sledgehammer requires version 3.0 or above. This ATP is provided -for compatibility reasons. - \item[$\bullet$] \textbf{\textit{vampire}:} Vampire is an ATP developed by Andrei Voronkov and his colleagues \cite{riazanov-voronkov-2002}. To use Vampire, set the environment variable \texttt{VAMPIRE\_HOME} to the directory diff -r 9de1add14bac -r f9af8a863bd3 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Jun 22 18:15:44 2010 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Jun 22 19:10:12 2010 +0200 @@ -299,6 +299,7 @@ fun run_sh prover hard_timeout timeout dir st = let + val _ = Sledgehammer_Fact_Filter.use_natural_form := true (* experimental *) val {context = ctxt, facts, goal} = Proof.goal st val thy = ProofContext.theory_of ctxt val change_dir = (fn SOME d => Config.put ATP_Systems.dest_dir d | _ => I) @@ -324,7 +325,7 @@ NONE => (message, SH_OK (time_isa, time_atp, relevant_thm_names)) | SOME _ => (message, SH_FAIL (time_isa, time_atp)) end - handle Sledgehammer_HOL_Clause.TRIVIAL => ("trivial", SH_OK (0, 0, [])) + handle Sledgehammer_HOL_Clause.TRIVIAL () => ("trivial", SH_OK (0, 0, [])) | ERROR msg => ("error: " ^ msg, SH_ERROR) | TimeLimit.TimeOut => ("timeout", SH_ERROR) diff -r 9de1add14bac -r f9af8a863bd3 src/HOL/Nitpick_Examples/Mini_Nits.thy --- a/src/HOL/Nitpick_Examples/Mini_Nits.thy Tue Jun 22 18:15:44 2010 +0200 +++ b/src/HOL/Nitpick_Examples/Mini_Nits.thy Tue Jun 22 19:10:12 2010 +0200 @@ -14,14 +14,19 @@ ML {* exception FAIL -(* int -> term -> string *) +val has_kodkodi = (getenv "KODKODI" <> "") + fun minipick n t = map (fn k => Minipick.kodkod_problem_from_term @{context} (K k) t) (1 upto n) |> Minipick.solve_any_kodkod_problem @{theory} -(* int -> term -> bool *) -fun none n t = (minipick n t = "none" orelse raise FAIL) -fun genuine n t = (minipick n t = "genuine" orelse raise FAIL) -fun unknown n t = (minipick n t = "unknown" orelse raise FAIL) +fun minipick_expect expect n t = + if has_kodkodi then + if minipick n t = expect then () else raise FAIL + else + () +val none = minipick_expect "none" +val genuine = minipick_expect "genuine" +val unknown = minipick_expect "unknown" *} ML {* genuine 1 @{prop "x = Not"} *} diff -r 9de1add14bac -r f9af8a863bd3 src/HOL/Nitpick_Examples/ROOT.ML --- a/src/HOL/Nitpick_Examples/ROOT.ML Tue Jun 22 18:15:44 2010 +0200 +++ b/src/HOL/Nitpick_Examples/ROOT.ML Tue Jun 22 19:10:12 2010 +0200 @@ -5,8 +5,4 @@ Nitpick examples. *) -if getenv "KODKODI" = "" then - () -else - setmp_noncritical quick_and_dirty true use_thys - ["Nitpick_Examples"]; +setmp_noncritical quick_and_dirty true use_thys ["Nitpick_Examples"]; diff -r 9de1add14bac -r f9af8a863bd3 src/HOL/Nitpick_Examples/Tests_Nits.thy --- a/src/HOL/Nitpick_Examples/Tests_Nits.thy Tue Jun 22 18:15:44 2010 +0200 +++ b/src/HOL/Nitpick_Examples/Tests_Nits.thy Tue Jun 22 19:10:12 2010 +0200 @@ -11,6 +11,6 @@ imports Main begin -ML {* Nitpick_Tests.run_all_tests () *} +ML {* () |> getenv "KODKODI" <> "" ? Nitpick_Tests.run_all_tests *} end diff -r 9de1add14bac -r f9af8a863bd3 src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Jun 22 18:15:44 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Jun 22 19:10:12 2010 +0200 @@ -8,7 +8,8 @@ signature ATP_MANAGER = sig - type name_pool = Sledgehammer_HOL_Clause.name_pool + type name_pool = Sledgehammer_FOL_Clause.name_pool + type cnf_thm = Sledgehammer_Fact_Preprocessor.cnf_thm type relevance_override = Sledgehammer_Fact_Filter.relevance_override type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command type params = @@ -31,8 +32,8 @@ {subgoal: int, goal: Proof.context * (thm list * thm), relevance_override: relevance_override, - axiom_clauses: (thm * (string * int)) list option, - filtered_clauses: (thm * (string * int)) list option} + axiom_clauses: cnf_thm list option, + filtered_clauses: cnf_thm list option} datatype failure = Unprovable | IncompleteUnprovable | TimedOut | OutOfResources | OldSpass | MalformedInput | MalformedOutput | UnknownError @@ -46,7 +47,7 @@ proof: string, internal_thm_names: string Vector.vector, conjecture_shape: int list list, - filtered_clauses: (thm * (string * int)) list} + filtered_clauses: cnf_thm list} type prover = params -> minimize_command -> Time.time -> problem -> prover_result @@ -66,6 +67,7 @@ open Sledgehammer_Util open Sledgehammer_Fact_Filter +open Sledgehammer_HOL_Clause open Sledgehammer_Proof_Reconstruct (** problems, results, provers, etc. **) @@ -91,8 +93,8 @@ {subgoal: int, goal: Proof.context * (thm list * thm), relevance_override: relevance_override, - axiom_clauses: (thm * (string * int)) list option, - filtered_clauses: (thm * (string * int)) list option}; + axiom_clauses: cnf_thm list option, + filtered_clauses: cnf_thm list option} datatype failure = Unprovable | IncompleteUnprovable | TimedOut | OutOfResources | OldSpass | @@ -108,7 +110,7 @@ proof: string, internal_thm_names: string Vector.vector, conjecture_shape: int list list, - filtered_clauses: (thm * (string * int)) list}; + filtered_clauses: cnf_thm list} type prover = params -> minimize_command -> Time.time -> problem -> prover_result @@ -354,7 +356,7 @@ filtered_clauses = NONE} val message = #message (prover params (minimize_command name) timeout problem) - handle Sledgehammer_HOL_Clause.TRIVIAL => metis_line full_types i n [] + handle TRIVIAL () => metis_line full_types i n [] | ERROR message => "Error: " ^ message ^ "\n" val _ = unregister params message (Thread.self ()); in () end) diff -r 9de1add14bac -r f9af8a863bd3 src/HOL/Tools/ATP_Manager/atp_systems.ML --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Tue Jun 22 18:15:44 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Tue Jun 22 19:10:12 2010 +0200 @@ -110,33 +110,39 @@ fun shape_of_clauses _ [] = [] | shape_of_clauses j ([] :: clauses) = [] :: shape_of_clauses j clauses - | shape_of_clauses j ((lit :: lits) :: clauses) = + | shape_of_clauses j ((_ :: lits) :: clauses) = let val shape = shape_of_clauses (j + 1) (lits :: clauses) in (j :: hd shape) :: tl shape end -fun generic_prover overlord get_facts prepare write_file home_var executable - args proof_delims known_failures name - ({debug, full_types, explicit_apply, isar_proof, isar_shrink_factor, - ...} : params) minimize_command +(* generic TPTP-based provers *) + +fun generic_tptp_prover + (name, {home_var, executable, arguments, proof_delims, known_failures, + max_axiom_clauses, prefers_theory_relevant}) + ({debug, overlord, full_types, explicit_apply, respect_no_atp, + relevance_threshold, relevance_convergence, theory_relevant, + defs_relevant, isar_proof, isar_shrink_factor, ...} : params) + minimize_command timeout ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses} : problem) = let (* get clauses and prepare them for writing *) - val (ctxt, (chained_ths, th)) = goal; + val (ctxt, (_, th)) = goal; val thy = ProofContext.theory_of ctxt; val goal_clss = #1 (neg_conjecture_clauses ctxt th subgoal) val goal_cls = List.concat goal_clss val the_filtered_clauses = (case filtered_clauses of - NONE => get_facts relevance_override goal goal_cls + NONE => relevant_facts full_types respect_no_atp relevance_threshold + relevance_convergence defs_relevant max_axiom_clauses + (the_default prefers_theory_relevant theory_relevant) + relevance_override goal goal_cls | SOME fcls => fcls); - val the_axiom_clauses = - (case axiom_clauses of - NONE => the_filtered_clauses - | SOME axcls => axcls); + val the_axiom_clauses = axiom_clauses |> the_default the_filtered_clauses val (internal_thm_names, clauses) = - prepare goal_cls chained_ths the_axiom_clauses the_filtered_clauses thy; + prepare_clauses full_types goal_cls the_axiom_clauses the_filtered_clauses + thy (* path to unique problem file *) val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER" @@ -161,10 +167,10 @@ fun command_line probfile = (if Config.get ctxt measure_runtime then "TIMEFORMAT='%3U'; { time " ^ - space_implode " " [File.shell_path command, args, + space_implode " " [File.shell_path command, arguments timeout, File.shell_path probfile] ^ " ; } 2>&1" else - space_implode " " ["exec", File.shell_path command, args, + space_implode " " ["exec", File.shell_path command, arguments timeout, File.shell_path probfile, "2>&1"]) ^ (if overlord then " | sed 's/,/, /g' \ @@ -189,7 +195,8 @@ if Config.get ctxt measure_runtime then split_time s else (s, 0) fun run_on probfile = if File.exists command then - write_file full_types explicit_apply probfile clauses + write_tptp_file (debug andalso overlord) full_types explicit_apply + probfile clauses |> pair (apfst split_time' (bash_output (command_line probfile))) else if home = "" then error ("The environment variable " ^ quote home_var ^ " is not set.") @@ -233,26 +240,7 @@ proof = proof, internal_thm_names = internal_thm_names, conjecture_shape = conjecture_shape, filtered_clauses = the_filtered_clauses} - end; - - -(* generic TPTP-based provers *) - -fun generic_tptp_prover - (name, {home_var, executable, arguments, proof_delims, known_failures, - max_axiom_clauses, prefers_theory_relevant}) - (params as {debug, overlord, full_types, respect_no_atp, - relevance_threshold, relevance_convergence, theory_relevant, - defs_relevant, isar_proof, ...}) - minimize_command timeout = - generic_prover overlord - (relevant_facts full_types respect_no_atp relevance_threshold - relevance_convergence defs_relevant max_axiom_clauses - (the_default prefers_theory_relevant theory_relevant)) - (prepare_clauses false full_types) - (write_tptp_file (debug andalso overlord)) home_var - executable (arguments timeout) proof_delims known_failures name params - minimize_command + end fun tptp_prover name p = (name, generic_tptp_prover (name, p)); @@ -313,31 +301,14 @@ (* SPASS *) -fun generic_dfg_prover - (name, {home_var, executable, arguments, proof_delims, known_failures, - max_axiom_clauses, prefers_theory_relevant}) - (params as {overlord, full_types, respect_no_atp, relevance_threshold, - relevance_convergence, theory_relevant, defs_relevant, ...}) - minimize_command timeout = - generic_prover overlord - (relevant_facts full_types respect_no_atp relevance_threshold - relevance_convergence defs_relevant max_axiom_clauses - (the_default prefers_theory_relevant theory_relevant)) - (prepare_clauses true full_types) write_dfg_file home_var executable - (arguments timeout) proof_delims known_failures name params - minimize_command - -fun dfg_prover name p = (name, generic_dfg_prover (name, p)) - (* The "-VarWeight=3" option helps the higher-order problems, probably by counteracting the presence of "hAPP". *) -fun generic_spass_config dfg : prover_config = +val spass_config : prover_config = {home_var = "SPASS_HOME", executable = "SPASS", arguments = fn timeout => - "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \ - \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_generous_secs timeout) - |> not dfg ? prefix "-TPTP ", + "-TPTP -Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \ + \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_generous_secs timeout), proof_delims = [("Here is a proof", "Formulae used in the proof")], known_failures = [(IncompleteUnprovable, "SPASS beiseite: Completion found"), @@ -349,10 +320,6 @@ (OldSpass, "Unrecognized option TPTP")], max_axiom_clauses = 40, prefers_theory_relevant = true} -val spass_dfg_config = generic_spass_config true -val spass_dfg = dfg_prover "spass_dfg" spass_dfg_config - -val spass_config = generic_spass_config false val spass = tptp_prover "spass" spass_config (* remote prover invocation via SystemOnTPTP *) @@ -414,8 +381,7 @@ space_implode " " [maybe_remote e e_config, maybe_remote spass spass_config, remotify (fst vampire)] -val provers = - [spass, spass_dfg, vampire, e, remote_vampire, remote_spass, remote_e] +val provers = [spass, vampire, e, remote_vampire, remote_spass, remote_e] val prover_setup = fold add_prover provers val setup = diff -r 9de1add14bac -r f9af8a863bd3 src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Jun 22 18:15:44 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Jun 22 19:10:12 2010 +0200 @@ -943,15 +943,15 @@ fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto i n step subst orig_assm_ts orig_t = - let - val warning_m = if auto then K () else warning - val unknown_outcome = ("unknown", state) - in + let val warning_m = if auto then K () else warning in if getenv "KODKODI" = "" then + (* The "expect" argument is deliberately ignored if Kodkodi is missing so + that the "Nitpick_Examples" can be processed on any machine. *) (warning_m (Pretty.string_of (plazy install_kodkodi_message)); - unknown_outcome) + ("no_kodkodi", state)) else let + val unknown_outcome = ("unknown", state) val deadline = Option.map (curry Time.+ (Time.now ())) timeout val outcome as (outcome_code, _) = time_limit (if debug then NONE else timeout) diff -r 9de1add14bac -r f9af8a863bd3 src/HOL/Tools/Sledgehammer/meson_tactic.ML --- a/src/HOL/Tools/Sledgehammer/meson_tactic.ML Tue Jun 22 18:15:44 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/meson_tactic.ML Tue Jun 22 19:10:12 2010 +0200 @@ -17,11 +17,11 @@ open Sledgehammer_Fact_Preprocessor (*Expand all new definitions of abstraction or Skolem functions in a proof state.*) -fun is_absko (Const (@{const_name "=="}, _) $ Free (a, _) $ u) = +fun is_absko (Const (@{const_name "=="}, _) $ Free (a, _) $ _) = String.isPrefix skolem_prefix a | is_absko _ = false; -fun is_okdef xs (Const (@{const_name "=="}, _) $ t $ u) = (*Definition of Free, not in certain terms*) +fun is_okdef xs (Const (@{const_name "=="}, _) $ t $ _) = (*Definition of Free, not in certain terms*) is_Free t andalso not (member (op aconv) xs t) | is_okdef _ _ = false diff -r 9de1add14bac -r f9af8a863bd3 src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Tue Jun 22 18:15:44 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Tue Jun 22 19:10:12 2010 +0200 @@ -58,7 +58,7 @@ (* Finding the relative location of an untyped term within a list of terms *) fun get_index lit = let val lit = Envir.eta_contract lit - fun get n [] = raise Empty + fun get _ [] = raise Empty | get n (x::xs) = if untyped_aconv lit (Envir.eta_contract (HOLogic.dest_Trueprop x)) then n else get (n+1) xs in get 1 end; @@ -238,7 +238,7 @@ | NONE => raise Fail ("fol_type_to_isa: " ^ x)); fun reveal_skolem_somes skolem_somes = - map_aterms (fn t as Const (s, T) => + map_aterms (fn t as Const (s, _) => if String.isPrefix skolem_theory_name s then AList.lookup (op =) skolem_somes s |> the |> map_types Type_Infer.paramify_vars @@ -348,8 +348,7 @@ | hol_term_from_fol _ = hol_term_from_fol_PT fun hol_terms_from_fol ctxt mode skolem_somes fol_tms = - let val thy = ProofContext.theory_of ctxt - val ts = map (hol_term_from_fol mode ctxt) fol_tms + let val ts = map (hol_term_from_fol mode ctxt) fol_tms val _ = trace_msg (fn () => " calling type inference:") val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts val ts' = ts |> map (reveal_skolem_somes skolem_somes) |> infer_types ctxt @@ -694,11 +693,10 @@ tfrees = union (op =) tfree_lits tfrees, skolem_somes = skolem_somes} end; - val lmap as {skolem_somes, ...} = - {axioms = [], tfrees = init_tfrees ctxt, skolem_somes = []} - |> fold (add_thm true) cls - |> add_tfrees - |> fold (add_thm false) ths + val lmap = {axioms = [], tfrees = init_tfrees ctxt, skolem_somes = []} + |> fold (add_thm true) cls + |> add_tfrees + |> fold (add_thm false) ths val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap) fun is_used c = exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists diff -r 9de1add14bac -r f9af8a863bd3 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Jun 22 18:15:44 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Jun 22 19:10:12 2010 +0200 @@ -5,17 +5,17 @@ signature SLEDGEHAMMER_FACT_FILTER = sig + type cnf_thm = Sledgehammer_Fact_Preprocessor.cnf_thm type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause type arity_clause = Sledgehammer_FOL_Clause.arity_clause - type axiom_name = Sledgehammer_HOL_Clause.axiom_name type hol_clause = Sledgehammer_HOL_Clause.hol_clause - type hol_clause_id = Sledgehammer_HOL_Clause.hol_clause_id type relevance_override = {add: Facts.ref list, del: Facts.ref list, only: bool} + val use_natural_form : bool Unsynchronized.ref val name_thms_pair_from_ref : Proof.context -> thm list -> Facts.ref -> string * thm list val tvar_classes_of_terms : term list -> string list @@ -24,15 +24,12 @@ val is_quasi_fol_term : theory -> term -> bool val relevant_facts : bool -> bool -> real -> real -> bool -> int -> bool -> relevance_override - -> Proof.context * (thm list * 'a) -> thm list - -> (thm * (string * int)) list + -> Proof.context * (thm list * 'a) -> thm list -> cnf_thm list val prepare_clauses : - bool -> bool -> thm list -> thm list - -> (thm * (axiom_name * hol_clause_id)) list - -> (thm * (axiom_name * hol_clause_id)) list -> theory - -> axiom_name vector - * (hol_clause list * hol_clause list * hol_clause list * - hol_clause list * classrel_clause list * arity_clause list) + bool -> thm list -> cnf_thm list -> cnf_thm list -> theory + -> string vector + * (hol_clause list * hol_clause list * hol_clause list + * hol_clause list * classrel_clause list * arity_clause list) end; structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER = @@ -42,6 +39,9 @@ open Sledgehammer_Fact_Preprocessor open Sledgehammer_HOL_Clause +(* Experimental feature: Filter theorems in natural form or in CNF? *) +val use_natural_form = Unsynchronized.ref false + type relevance_override = {add: Facts.ref list, del: Facts.ref list, @@ -54,36 +54,13 @@ fun strip_Trueprop (@{const Trueprop} $ t) = t | strip_Trueprop t = t; -(*A surprising number of theorems contain only a few significant constants. - These include all induction rules, and other general theorems. Filtering - theorems in clause form reveals these complexities in the form of Skolem - functions. If we were instead to filter theorems in their natural form, - some other method of measuring theorem complexity would become necessary.*) - -fun log_weight2 (x:real) = 1.0 + 2.0/Math.ln (x+1.0); - -(*The default seems best in practice. A constant function of one ignores - the constant frequencies.*) -val weight_fn = log_weight2; - - -(*Including equality in this list might be expected to stop rules like subset_antisym from - being chosen, but for some reason filtering works better with them listed. The - logical signs All, Ex, &, and --> are omitted because any remaining occurrrences - must be within comprehensions.*) -val standard_consts = - [@{const_name Trueprop}, @{const_name "==>"}, @{const_name all}, - @{const_name "=="}, @{const_name "op |"}, @{const_name Not}, - @{const_name "op ="}]; - - (*** constants with types ***) (*An abstraction of Isabelle types*) datatype const_typ = CTVar | CType of string * const_typ list (*Is the second type an instance of the first one?*) -fun match_type (CType(con1,args1)) (CType(con2,args2)) = +fun match_type (CType(con1,args1)) (CType(con2,args2)) = con1=con2 andalso match_types args1 args2 | match_type CTVar _ = true | match_type _ CTVar = false @@ -91,63 +68,85 @@ | match_types (a1::as1) (a2::as2) = match_type a1 a2 andalso match_types as1 as2; (*Is there a unifiable constant?*) -fun uni_mem gctab (c,c_typ) = - case Symtab.lookup gctab c of - NONE => false - | SOME ctyps_list => exists (match_types c_typ) ctyps_list; - +fun uni_mem goal_const_tab (c, c_typ) = + exists (match_types c_typ) (these (Symtab.lookup goal_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) +fun const_typ_of (Type (c,typs)) = CType (c, map const_typ_of typs) | const_typ_of (TFree _) = CTVar | const_typ_of (TVar _) = CTVar (*Pairs a constant with the list of its type instantiations (using const_typ)*) -fun const_with_typ thy (c,typ) = +fun const_with_typ thy (c,typ) = let val tvars = Sign.const_typargs thy (c,typ) in (c, map const_typ_of tvars) end - handle TYPE _ => (c,[]); (*Variable (locale constant): monomorphic*) + handle TYPE _ => (c,[]); (*Variable (locale constant): monomorphic*) (*Add a const/type pair to the table, but a [] entry means a standard connective, which we ignore.*) -fun add_const_typ_table ((c,ctyps), tab) = - Symtab.map_default (c, [ctyps]) (fn [] => [] | ctyps_list => insert (op =) ctyps ctyps_list) - tab; +fun add_const_type_to_table (c, ctyps) = + Symtab.map_default (c, [ctyps]) + (fn [] => [] | ctypss => insert (op =) ctyps ctypss) + +val fresh_Ex_prefix = "Sledgehammer.Ex." -(*Free variables are included, as well as constants, to handle locales*) -fun add_term_consts_typs_rm thy (Const(c, typ), tab) = - add_const_typ_table (const_with_typ thy (c,typ), tab) - | add_term_consts_typs_rm thy (Free(c, typ), tab) = - add_const_typ_table (const_with_typ thy (c,typ), tab) - | add_term_consts_typs_rm _ (Const (@{const_name skolem_id}, _) $ _, tab) = - tab - | add_term_consts_typs_rm thy (t $ u, tab) = - add_term_consts_typs_rm thy (t, add_term_consts_typs_rm thy (u, tab)) - | add_term_consts_typs_rm thy (Abs(_,_,t), tab) = add_term_consts_typs_rm thy (t, tab) - | add_term_consts_typs_rm _ (_, tab) = tab; - -(*The empty list here indicates that the constant is being ignored*) -fun add_standard_const (s,tab) = Symtab.update (s,[]) tab; - -val null_const_tab : const_typ list list Symtab.table = - List.foldl add_standard_const Symtab.empty standard_consts; - -fun get_goal_consts_typs thy = List.foldl (add_term_consts_typs_rm thy) null_const_tab; +fun get_goal_consts_typs thy goals = + let + val use_natural_form = !use_natural_form + (* Free variables are included, as well as constants, to handle locales. + "skolem_id" is included to increase the complexity of theorems containing + Skolem functions. In non-CNF form, "Ex" is included but each occurrence + is considered fresh, to simulate the effect of Skolemization. *) + fun aux (Const (x as (s, _))) = + (if s = @{const_name Ex} andalso use_natural_form then + (gensym fresh_Ex_prefix, []) + else + (const_with_typ thy x)) + |> add_const_type_to_table + | aux (Free x) = add_const_type_to_table (const_with_typ thy x) + | aux ((t as Const (@{const_name skolem_id}, _)) $ _) = aux t + | aux (t $ u) = aux t #> aux u + | aux (Abs (_, _, t)) = aux t + | aux _ = I + (* Including equality in this list might be expected to stop rules like + subset_antisym from being chosen, but for some reason filtering works better + with them listed. The logical signs All, Ex, &, and --> are omitted for CNF + because any remaining occurrences must be within comprehensions. *) + val standard_consts = + [@{const_name Trueprop}, @{const_name "==>"}, @{const_name all}, + @{const_name "=="}, @{const_name "op |"}, @{const_name Not}, + @{const_name "op ="}] @ + (if use_natural_form then + [@{const_name All}, @{const_name Ex}, @{const_name "op &"}, + @{const_name "op -->"}] + else + []) + in + Symtab.empty |> fold (Symtab.update o rpair []) standard_consts + |> fold aux goals + end (*Inserts a dummy "constant" referring to the theory name, so that relevance takes the given theory into account.*) fun const_prop_of theory_relevant th = - if theory_relevant then - let val name = Context.theory_name (theory_of_thm th) - val t = Const (name ^ ". 1", HOLogic.boolT) - in t $ prop_of th end - else prop_of th; + if theory_relevant then + let + val name = Context.theory_name (theory_of_thm th) + val t = Const (name ^ ". 1", @{typ bool}) + in t $ prop_of th end + else + prop_of th + +fun appropriate_prop_of theory_relevant (cnf_thm, (_, orig_thm)) = + (if !use_natural_form then orig_thm else cnf_thm) + |> const_prop_of theory_relevant (**** Constant / Type Frequencies ****) (*A two-dimensional symbol table counts frequencies of constants. It's keyed first by constant name and second by its list of type instantiations. For the latter, we need a linear ordering on type const_typ list.*) - + local fun cons_nr CTVar = 0 @@ -165,137 +164,149 @@ structure CTtab = Table(type key = const_typ list val ord = dict_ord const_typ_ord); -fun count_axiom_consts theory_relevant thy ((thm,_), tab) = - let fun count_const (a, T, tab) = - let val (c, cts) = const_with_typ thy (a,T) - in (*Two-dimensional table update. Constant maps to types maps to count.*) - Symtab.map_default (c, CTtab.empty) - (CTtab.map_default (cts,0) (fn n => n+1)) tab - end - fun count_term_consts (Const(a,T), tab) = count_const(a,T,tab) - | count_term_consts (Free(a,T), tab) = count_const(a,T,tab) - | count_term_consts (t $ u, tab) = - count_term_consts (t, count_term_consts (u, tab)) - | count_term_consts (Abs(_,_,t), tab) = count_term_consts (t, tab) - | count_term_consts (_, tab) = tab - in count_term_consts (const_prop_of theory_relevant thm, tab) end; +fun count_axiom_consts theory_relevant thy axiom = + let + fun do_const (a, T) = + let val (c, cts) = const_with_typ thy (a,T) in + (* Two-dimensional table update. Constant maps to types maps to + count. *) + CTtab.map_default (cts, 0) (Integer.add 1) + |> Symtab.map_default (c, CTtab.empty) + end + fun do_term (Const x) = do_const x + | do_term (Free x) = do_const x + | do_term (Const (@{const_name skolem_id}, _) $ _) = I + | do_term (t $ u) = do_term t #> do_term u + | do_term (Abs (_, _, t)) = do_term t + | do_term _ = I + in axiom |> appropriate_prop_of theory_relevant |> do_term end (**** Actual Filtering Code ****) (*The frequency of a constant is the sum of those of all instances of its type.*) -fun const_frequency ctab (c, cts) = +fun const_frequency const_tab (c, cts) = CTtab.fold (fn (cts', m) => match_types cts cts' ? Integer.add m) - (the (Symtab.lookup ctab c)) 0 + (the (Symtab.lookup const_tab c) + handle Option.Option => raise Fail ("Const: " ^ c)) 0 -(*Add in a constant's weight, as determined by its frequency.*) -fun add_ct_weight ctab ((c,T), w) = - w + weight_fn (real (const_frequency ctab (c,T))); +(*A surprising number of theorems contain only a few significant constants. + These include all induction rules, and other general theorems. Filtering + theorems in clause form reveals these complexities in the form of Skolem + functions. If we were instead to filter theorems in their natural form, + some other method of measuring theorem complexity would become necessary.*) -(*Relevant constants are weighted according to frequency, +(* "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) + +(* Computes a constant's weight, as determined by its frequency. *) +val ct_weight = log_weight2 o real oo const_frequency + +(*Relevant constants are weighted according to frequency, but irrelevant constants are simply counted. Otherwise, Skolem functions, which are rare, would harm a clause's chances of being picked.*) -fun clause_weight ctab gctyps consts_typs = +fun clause_weight const_tab gctyps consts_typs = let val rel = filter (uni_mem gctyps) consts_typs - val rel_weight = List.foldl (add_ct_weight ctab) 0.0 rel + val rel_weight = fold (curry Real.+ o ct_weight const_tab) rel 0.0 in rel_weight / (rel_weight + real (length consts_typs - length rel)) 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 consts_typs_of_term thy t = - let val tab = add_term_consts_typs_rm thy (t, null_const_tab) - in Symtab.fold add_expand_pairs tab [] end; +fun consts_typs_of_term thy t = + Symtab.fold add_expand_pairs (get_goal_consts_typs thy [t]) [] -fun pair_consts_typs_axiom theory_relevant thy (p as (thm, _)) = - (p, (consts_typs_of_term thy (const_prop_of theory_relevant thm))); +fun pair_consts_typs_axiom theory_relevant thy axiom = + (axiom, axiom |> appropriate_prop_of theory_relevant + |> consts_typs_of_term thy) -exception ConstFree; -fun dest_ConstFree (Const aT) = aT - | dest_ConstFree (Free aT) = aT - | dest_ConstFree _ = raise ConstFree; +exception CONST_OR_FREE of unit + +fun dest_Const_or_Free (Const x) = x + | dest_Const_or_Free (Free x) = x + | dest_Const_or_Free _ = raise CONST_OR_FREE () (*Look for definitions of the form f ?x1 ... ?xn = t, but not reversed.*) fun defines thy thm gctypes = let val tm = prop_of thm fun defs lhs rhs = let val (rator,args) = strip_comb lhs - val ct = const_with_typ thy (dest_ConstFree rator) + 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 []) end - handle ConstFree => false - in + handle CONST_OR_FREE () => false + in case tm of - @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ lhs $ rhs) => - defs lhs rhs + @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ lhs $ rhs) => + defs lhs rhs | _ => false end; -type annotd_cls = (thm * (string * int)) * ((string * const_typ list) list); - +type annotated_clause = cnf_thm * ((string * const_typ list) list) + (*For a reverse sort, putting the largest values first.*) -fun compare_pairs ((_,w1),(_,w2)) = Real.compare (w2,w1); +fun compare_pairs ((_, w1), (_, w2)) = Real.compare (w2, w1) (*Limit the number of new clauses, to prevent runaway acceptance.*) -fun take_best max_new (newpairs : (annotd_cls*real) list) = +fun take_best max_new (newpairs : (annotated_clause * real) list) = let val nnew = length newpairs in if nnew <= max_new then (map #1 newpairs, []) - else + else let val cls = sort compare_pairs newpairs val accepted = List.take (cls, max_new) in - trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^ + 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 (fn (((_,(name,_)),_),_) => name) accepted)); + space_implode ", " (map (fn (((_,((name,_), _)),_),_) => name) accepted)); (map #1 accepted, map #1 (List.drop (cls, max_new))) end end; -fun cnf_for_facts ctxt = - let val thy = ProofContext.theory_of ctxt in - maps (maps (cnf_axiom thy) o ProofContext.get_fact ctxt) - end - fun relevant_clauses ctxt relevance_convergence defs_relevant max_new - (relevance_override as {add, del, only}) ctab = + ({add, del, ...} : relevance_override) const_tab = let val thy = ProofContext.theory_of ctxt - val add_thms = cnf_for_facts ctxt add - val del_thms = cnf_for_facts ctxt del - fun iter threshold rel_consts = + val add_thms = maps (ProofContext.get_fact ctxt) add + val del_thms = maps (ProofContext.get_fact ctxt) del + fun iter threshold rel_const_tab = let fun relevant ([], _) [] = [] (* Nothing added this iteration *) | relevant (newpairs, rejects) [] = let val (newrels, more_rejects) = take_best max_new newpairs val new_consts = maps #2 newrels - val rel_consts' = List.foldl add_const_typ_table rel_consts new_consts + val rel_const_tab = + rel_const_tab |> fold add_const_type_to_table new_consts val threshold = threshold + (1.0 - threshold) / relevance_convergence in trace_msg (fn () => "relevant this iteration: " ^ Int.toString (length newrels)); - map #1 newrels @ iter threshold rel_consts' + map #1 newrels @ iter threshold rel_const_tab (more_rejects @ rejects) end | relevant (newrels, rejects) - ((ax as (clsthm as (thm, (name, n)), consts_typs)) :: axs) = + ((ax as (clsthm as (_, ((name, n), orig_th)), + consts_typs)) :: axs) = let - val weight = if member Thm.eq_thm add_thms thm then 1.0 - else if member Thm.eq_thm del_thms thm then 0.0 - else clause_weight ctab rel_consts consts_typs + val weight = + if member Thm.eq_thm add_thms orig_th then 1.0 + else if member Thm.eq_thm del_thms orig_th then 0.0 + else clause_weight const_tab rel_const_tab consts_typs in if weight >= threshold orelse - (defs_relevant andalso defines thy (#1 clsthm) rel_consts) then - (trace_msg (fn () => name ^ " clause " ^ Int.toString n ^ + (defs_relevant andalso + defines thy (#1 clsthm) rel_const_tab) then + (trace_msg (fn () => name ^ " clause " ^ Int.toString n ^ " passes: " ^ Real.toString weight); relevant ((ax, weight) :: newrels, rejects) axs) else @@ -307,14 +318,14 @@ relevant ([], []) end in iter end - + fun relevance_filter ctxt relevance_threshold relevance_convergence defs_relevant max_new theory_relevant relevance_override - thy axioms goals = + thy (axioms : cnf_thm list) goals = if relevance_threshold > 0.0 then let - val const_tab = List.foldl (count_axiom_consts theory_relevant thy) - Symtab.empty axioms + val const_tab = fold (count_axiom_consts theory_relevant thy) axioms + Symtab.empty val goal_const_tab = get_goal_consts_typs thy goals val _ = trace_msg (fn () => "Initial constants: " ^ @@ -398,7 +409,7 @@ fun multi_name a th (n, pairs) = (n + 1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs); -fun add_names (a, []) pairs = 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)) @@ -453,16 +464,16 @@ fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x)) | fold_type_consts _ _ x = x; -val add_type_consts_in_type = fold_type_consts setinsert; - (*Type constructors used to instantiate overloaded constants are the only ones needed.*) fun add_type_consts_in_term thy = - let val const_typargs = Sign.const_typargs thy - fun add_tcs (Const cT) x = fold add_type_consts_in_type (const_typargs cT) x - | add_tcs (Abs (_, _, u)) x = add_tcs u x - | add_tcs (t $ u) x = add_tcs t (add_tcs u x) - | add_tcs _ x = x - in add_tcs end + let + val const_typargs = Sign.const_typargs thy + fun aux (Const cT) = fold (fold_type_consts setinsert) (const_typargs cT) + | aux (Abs (_, _, u)) = aux u + | aux (Const (@{const_name skolem_id}, _) $ _) = I + | aux (t $ u) = aux t #> aux u + | aux _ = I + in aux end fun type_consts_of_terms thy ts = Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty); @@ -478,7 +489,7 @@ (*Ensures that no higher-order theorems "leak out"*) fun restrict_to_logic thy true cls = filter (is_quasi_fol_term thy o prop_of o fst) cls - | restrict_to_logic thy false cls = cls; + | restrict_to_logic _ false cls = cls (**** Predicates to detect unwanted clauses (prolific or likely to cause unsoundness) ****) @@ -524,16 +535,14 @@ omitted. *) fun is_dangerous_term _ @{prop True} = true | is_dangerous_term full_types t = - not full_types andalso + not full_types andalso (has_typed_var dangerous_types t orelse forall too_general_equality (HOLogic.disjuncts (strip_Trueprop t))) -fun is_dangerous_theorem full_types add_thms thm = - not (member Thm.eq_thm add_thms thm) andalso - is_dangerous_term full_types (prop_of thm) - fun remove_dangerous_clauses full_types add_thms = - filter_out (is_dangerous_theorem full_types add_thms o fst) + filter_out (fn (cnf_th, (_, orig_th)) => + not (member Thm.eq_thm add_thms orig_th) andalso + is_dangerous_term full_types (prop_of cnf_th)) fun is_fol_goal thy = forall (Meson.is_fol_term thy) o map prop_of @@ -555,8 +564,11 @@ |> cnf_rules_pairs thy |> not has_override ? make_unique |> not only ? restrict_to_logic thy is_FO - |> (if only then I - else remove_dangerous_clauses full_types (cnf_for_facts ctxt add)) + |> (if only then + I + else + remove_dangerous_clauses full_types + (maps (ProofContext.get_fact ctxt) add)) in relevance_filter ctxt relevance_threshold relevance_convergence defs_relevant max_new theory_relevant relevance_override @@ -566,7 +578,7 @@ (* prepare for passing to writer, create additional clauses based on the information from extra_cls *) -fun prepare_clauses dfg full_types goal_cls chained_ths axcls extra_cls thy = +fun prepare_clauses full_types goal_cls axcls extra_cls thy = let val is_FO = is_fol_goal thy goal_cls val ccls = subtract_cls extra_cls goal_cls @@ -577,12 +589,12 @@ and supers = tvar_classes_of_terms axtms and tycons = type_consts_of_terms thy (ccltms @ axtms) (*TFrees in conjecture clauses; TVars in axiom clauses*) - val conjectures = make_conjecture_clauses dfg thy ccls - val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses dfg thy extra_cls) - val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses dfg thy axcls) + val conjectures = make_conjecture_clauses thy ccls + val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses thy extra_cls) + val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses thy axcls) val helper_clauses = - get_helper_clauses dfg thy is_FO full_types conjectures extra_cls - val (supers', arity_clauses) = make_arity_clauses_dfg dfg thy tycons supers + get_helper_clauses thy is_FO full_types conjectures extra_cls + val (supers', arity_clauses) = make_arity_clauses thy tycons supers val classrel_clauses = make_classrel_clauses thy subs supers' in (Vector.fromList clnames, diff -r 9de1add14bac -r f9af8a863bd3 src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Tue Jun 22 18:15:44 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Tue Jun 22 19:10:12 2010 +0200 @@ -20,6 +20,7 @@ open Sledgehammer_Util open Sledgehammer_Fact_Preprocessor +open Sledgehammer_HOL_Clause open Sledgehammer_Proof_Reconstruct open ATP_Manager @@ -47,8 +48,8 @@ fun string_for_outcome NONE = "Success." | string_for_outcome (SOME failure) = string_for_failure failure -fun sledgehammer_test_theorems (params as {full_types, ...} : params) prover - timeout subgoal state filtered_clauses name_thms_pairs = +fun sledgehammer_test_theorems (params : params) prover timeout subgoal state + filtered_clauses name_thms_pairs = let val num_theorems = length name_thms_pairs val _ = priority ("Testing " ^ string_of_int num_theorems ^ @@ -88,7 +89,7 @@ (result as {outcome = NONE, ...}) => SOME result | _ => NONE - val {context = ctxt, facts, goal} = Proof.goal state; + val {context = ctxt, goal, ...} = Proof.goal state; in (* try prove first to check result and get used theorems *) (case test_thms_fun NONE name_thms_pairs of @@ -125,8 +126,7 @@ \option (e.g., \"timeout = " ^ string_of_int (10 + msecs div 1000) ^ " s\").") | {message, ...} => (NONE, "ATP error: " ^ message)) - handle Sledgehammer_HOL_Clause.TRIVIAL => - (SOME [], metis_line full_types i n []) + handle TRIVIAL () => (SOME [], metis_line full_types i n []) | ERROR msg => (NONE, "Error: " ^ msg) end diff -r 9de1add14bac -r f9af8a863bd3 src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Tue Jun 22 18:15:44 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Tue Jun 22 19:10:12 2010 +0200 @@ -7,6 +7,7 @@ signature SLEDGEHAMMER_FACT_PREPROCESSOR = sig + type cnf_thm = thm * ((string * int) * thm) val chained_prefix: string val trace: bool Unsynchronized.ref val trace_msg: (unit -> string) -> unit @@ -18,11 +19,10 @@ val multi_base_blacklist: string list val is_theorem_bad_for_atps: thm -> bool val type_has_topsort: typ -> bool - val cnf_rules_pairs: - theory -> (string * thm) list -> (thm * (string * int)) list - val use_skolem_cache: bool Unsynchronized.ref + val cnf_rules_pairs : theory -> (string * thm) list -> cnf_thm list + val saturate_skolem_cache: theory -> theory option + val auto_saturate_skolem_cache: bool Unsynchronized.ref (* for emergency use where the Skolem cache causes problems *) - val strip_subgoal : thm -> int -> (string * typ) list * term list * term val neg_clausify: thm -> thm list val neg_conjecture_clauses: Proof.context -> thm -> int -> thm list list * (string * typ) list @@ -35,6 +35,8 @@ open Sledgehammer_FOL_Clause +type cnf_thm = thm * ((string * int) * thm) + (* Used to label theorems chained into the goal. *) val chained_prefix = "Sledgehammer.chained_" @@ -132,12 +134,12 @@ | dec_sko (@{const "op &"} $ p $ q) thx = dec_sko q (dec_sko p thx) | dec_sko (@{const "op |"} $ p $ q) thx = dec_sko q (dec_sko p thx) | dec_sko (@{const Trueprop} $ p) thx = dec_sko p thx - | dec_sko t thx = thx + | dec_sko _ thx = thx in dec_sko (prop_of th) ([], thy) end fun mk_skolem_id t = let val T = fastype_of t in - Const (@{const_name skolem_id}, T --> T) $ Envir.beta_norm t + Const (@{const_name skolem_id}, T --> T) $ t end (*Traverse a theorem, accumulating Skolem function definitions.*) @@ -153,10 +155,11 @@ val cT = Ts ---> T (* FIXME: use "skolem_type_and_args" *) val id = skolem_name s (Unsynchronized.inc skolem_count) s' val c = Free (id, cT) - val rhs = list_abs_free (map dest_Free args, - HOLogic.choice_const T $ body) - |> inline ? mk_skolem_id - (*Forms a lambda-abstraction over the formal parameters*) + (* Forms a lambda-abstraction over the formal parameters *) + val rhs = + list_abs_free (map dest_Free args, + HOLogic.choice_const T $ body) + |> inline ? mk_skolem_id val def = Logic.mk_equals (c, rhs) val comb = list_comb (if inline then rhs else c, args) in dec_sko (subst_bound (comb, p)) (def :: defs) end @@ -167,7 +170,7 @@ | dec_sko (@{const "op &"} $ p $ q) defs = dec_sko q (dec_sko p defs) | dec_sko (@{const "op |"} $ p $ q) defs = dec_sko q (dec_sko p defs) | dec_sko (@{const Trueprop} $ p) defs = dec_sko p defs - | dec_sko t defs = defs (*Do nothing otherwise*) + | dec_sko _ defs = defs in dec_sko (prop_of th) [] end; @@ -409,7 +412,6 @@ val ctxt0 = Variable.global_thm_context th val (nnfth, ctxt) = to_nnf th ctxt0 val inline = exists_type (exists_subtype (can dest_TFree)) (prop_of nnfth) - val inline = false (* FIXME: temporary *) val defs = skolem_theorems_of_assume inline s nnfth val (cnfs, ctxt) = Meson.make_cnf defs nnfth ctxt in @@ -447,20 +449,20 @@ (**** Translate a set of theorems into CNF ****) -fun pair_name_cls _ (_, []) = [] - | pair_name_cls k (n, cls::clss) = (cls, (n,k)) :: pair_name_cls (k+1) (n, clss) - (*The combination of rev and tail recursion preserves the original order*) fun cnf_rules_pairs thy = let - fun aux pairs [] = pairs - | aux pairs ((name, th) :: ths) = + fun do_one _ [] = [] + | do_one ((name, k), th) (cls :: clss) = + (cls, ((name, k), th)) :: do_one ((name, k + 1), th) clss + fun do_all pairs [] = pairs + | do_all pairs ((name, th) :: ths) = let - val new_pairs = pair_name_cls 0 (name, cnf_axiom thy th) + val new_pairs = do_one ((name, 0), th) (cnf_axiom thy th) handle THM _ => [] | CLAUSE _ => [] - in aux (new_pairs @ pairs) ths end - in aux [] o rev end + in do_all (new_pairs @ pairs) ths end + in do_all [] o rev end (**** Convert all facts of the theory into FOL or HOL clauses ****) @@ -520,22 +522,11 @@ end; -val use_skolem_cache = Unsynchronized.ref true - -fun clause_cache_endtheory thy = - if !use_skolem_cache then saturate_skolem_cache thy else NONE - +val auto_saturate_skolem_cache = Unsynchronized.ref true -(* The cache can be kept smaller by inspecting the prop of each thm. Can ignore - all that are quasi-lambda-free, but then the individual theory caches become - much bigger. *) +fun conditionally_saturate_skolem_cache thy = + if !auto_saturate_skolem_cache then saturate_skolem_cache thy else NONE -fun strip_subgoal goal i = - let - val (t, frees) = Logic.goal_params (prop_of goal) i - val hyp_ts = t |> Logic.strip_assums_hyp |> map (curry subst_bounds frees) - val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees - in (rev (map dest_Free frees), hyp_ts, concl_t) end (*** Converting a subgoal into negated conjecture clauses. ***) @@ -574,7 +565,7 @@ (** setup **) val setup = - perhaps saturate_skolem_cache - #> Theory.at_end clause_cache_endtheory + perhaps conditionally_saturate_skolem_cache + #> Theory.at_end conditionally_saturate_skolem_cache end; diff -r 9de1add14bac -r f9af8a863bd3 src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Tue Jun 22 18:15:44 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Tue Jun 22 19:10:12 2010 +0200 @@ -28,8 +28,8 @@ val make_fixed_var : string -> string val make_schematic_type_var : string * int -> string val make_fixed_type_var : string -> string - val make_fixed_const : bool -> string -> string - val make_fixed_type_const : bool -> string -> string + val make_fixed_const : string -> string + val make_fixed_type_const : string -> string val make_type_class : string -> string type name = string * string type name_pool = string Symtab.table * string Symtab.table @@ -37,7 +37,6 @@ val pool_map : ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b val nice_name : name -> name_pool option -> string * name_pool option datatype kind = Axiom | Conjecture - type axiom_name = string datatype fol_type = TyVar of name | TyFree of name | @@ -49,37 +48,15 @@ TyLitFree of string * name exception CLAUSE of string * term val type_literals_for_types : typ list -> type_literal list - val get_tvar_strs: typ list -> string list datatype arLit = TConsLit of class * string * string list | TVarLit of class * string datatype arity_clause = ArityClause of - {axiom_name: axiom_name, conclLit: arLit, premLits: arLit list} + {axiom_name: string, conclLit: arLit, premLits: arLit list} datatype classrel_clause = ClassrelClause of - {axiom_name: axiom_name, subclass: class, superclass: class} + {axiom_name: string, subclass: class, superclass: class} val make_classrel_clauses: theory -> class list -> class list -> classrel_clause list - val make_arity_clauses_dfg: bool -> theory -> string list -> class list -> class list * arity_clause list val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list - val add_type_sort_preds: typ -> int Symtab.table -> int Symtab.table - val add_classrel_clause_preds : - classrel_clause -> int Symtab.table -> int Symtab.table - val class_of_arityLit: arLit -> class - val add_arity_clause_preds: arity_clause -> int Symtab.table -> int Symtab.table - val add_fol_type_funcs: fol_type -> int Symtab.table -> int Symtab.table - val add_arity_clause_funcs: - arity_clause -> int Symtab.table -> int Symtab.table - val init_functab: int Symtab.table - val dfg_sign: bool -> string -> string - val dfg_of_type_literal: bool -> type_literal -> string - val gen_dfg_cls: int * string * kind * string list * string list * string list -> string - val string_of_preds: (string * Int.int) list -> string - val string_of_funcs: (string * int) list -> string - val string_of_symbols: string -> string -> string - val string_of_start: string -> string - val string_of_descrip : string -> string - val dfg_tfree_clause : string -> string - val dfg_classrel_clause: classrel_clause -> string - val dfg_arity_clause: arity_clause -> string val tptp_sign: bool -> string -> string val tptp_of_type_literal : bool -> type_literal -> name_pool option -> string * name_pool option @@ -196,31 +173,21 @@ tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i)); fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x)); -val max_dfg_symbol_length = 63 - -(* HACK because SPASS 3.0 truncates identifiers to 63 characters. *) -fun controlled_length dfg s = - if dfg andalso size s > max_dfg_symbol_length then - String.extract (s, 0, SOME (max_dfg_symbol_length div 2 - 1)) ^ "__" ^ - String.extract (s, size s - max_dfg_symbol_length div 2 + 1, NONE) - else - s +fun lookup_const c = + case Symtab.lookup const_trans_table c of + SOME c' => c' + | NONE => ascii_of c -fun lookup_const dfg c = - case Symtab.lookup const_trans_table c of - SOME c' => c' - | NONE => controlled_length dfg (ascii_of c); - -fun lookup_type_const dfg c = - case Symtab.lookup type_const_trans_table c of - SOME c' => c' - | NONE => controlled_length dfg (ascii_of c); +fun lookup_type_const c = + case Symtab.lookup type_const_trans_table c of + SOME c' => c' + | NONE => ascii_of c (* "op =" MUST BE "equal" because it's built into ATPs. *) -fun make_fixed_const _ (@{const_name "op ="}) = "equal" - | make_fixed_const dfg c = const_prefix ^ lookup_const dfg c; +fun make_fixed_const @{const_name "op ="} = "equal" + | make_fixed_const c = const_prefix ^ lookup_const c -fun make_fixed_type_const dfg c = tconst_prefix ^ lookup_type_const dfg c; +fun make_fixed_type_const c = tconst_prefix ^ lookup_type_const c fun make_type_class clas = class_prefix ^ ascii_of clas; @@ -287,13 +254,10 @@ the_pool |> apsnd SOME -(**** Definitions and functions for FOL clauses, for conversion to TPTP or DFG - format ****) +(**** Definitions and functions for FOL clauses for TPTP format output ****) datatype kind = Axiom | Conjecture; -type axiom_name = string; - (**** Isabelle FOL clauses ****) datatype fol_type = @@ -329,39 +293,19 @@ fun sorts_on_typs (TFree (a,s)) = sorts_on_typs_aux ((a,~1),s) | sorts_on_typs (TVar (v,s)) = sorts_on_typs_aux (v,s); -fun pred_of_sort (TyLitVar (s, _)) = (s, 1) - | pred_of_sort (TyLitFree (s, _)) = (s, 1) - (*Given a list of sorted type variables, return a list of type literals.*) fun type_literals_for_types Ts = fold (union (op =)) (map sorts_on_typs Ts) [] -(*The correct treatment of TFrees like 'a in lemmas (axiom clauses) is not clear. - * Ignoring them leads to unsound proofs, since we do nothing to ensure that 'a - in a lemma has the same sort as 'a in the conjecture. - * Deleting such clauses will lead to problems with locales in other use of local results - where 'a is fixed. Probably we should delete clauses unless the sorts agree. - * Currently we include a class constraint in the clause, exactly as with TVars. -*) - (** make axiom and conjecture clauses. **) -fun get_tvar_strs [] = [] - | get_tvar_strs ((TVar (indx,s))::Ts) = - insert (op =) (make_schematic_type_var indx) (get_tvar_strs Ts) - | get_tvar_strs((TFree _)::Ts) = get_tvar_strs Ts - - - (**** Isabelle arities ****) datatype arLit = TConsLit of class * string * string list | TVarLit of class * string; datatype arity_clause = - ArityClause of {axiom_name: axiom_name, - conclLit: arLit, - premLits: arLit list}; + ArityClause of {axiom_name: string, conclLit: arLit, premLits: arLit list} fun gen_TVars 0 = [] @@ -372,25 +316,23 @@ | pack_sort(tvar, cls::srt) = (cls, tvar) :: pack_sort(tvar, srt); (*Arity of type constructor tcon :: (arg1,...,argN)res*) -fun make_axiom_arity_clause dfg (tcons, axiom_name, (cls,args)) = +fun make_axiom_arity_clause (tcons, axiom_name, (cls,args)) = let val tvars = gen_TVars (length args) val tvars_srts = ListPair.zip (tvars,args) in - ArityClause {axiom_name = axiom_name, - conclLit = TConsLit (cls, make_fixed_type_const dfg tcons, tvars), - premLits = map TVarLit (union_all(map pack_sort tvars_srts))} + ArityClause {axiom_name = axiom_name, + conclLit = TConsLit (cls, make_fixed_type_const tcons, tvars), + premLits = map TVarLit (union_all(map pack_sort tvars_srts))} end; (**** Isabelle class relations ****) datatype classrel_clause = - ClassrelClause of {axiom_name: axiom_name, - subclass: class, - superclass: class}; + ClassrelClause of {axiom_name: string, subclass: class, superclass: class} (*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*) -fun class_pairs thy [] supers = [] +fun class_pairs _ [] _ = [] | class_pairs thy subs supers = let val class_less = Sorts.class_less (Sign.classes_of thy) @@ -409,20 +351,20 @@ (** Isabelle arities **) -fun arity_clause dfg _ _ (tcons, []) = [] - | arity_clause dfg seen n (tcons, ("HOL.type",_)::ars) = (*ignore*) - arity_clause dfg seen n (tcons,ars) - | arity_clause dfg seen n (tcons, (ar as (class,_)) :: ars) = +fun arity_clause _ _ (_, []) = [] + | arity_clause seen n (tcons, ("HOL.type",_)::ars) = (*ignore*) + arity_clause seen n (tcons,ars) + | arity_clause seen n (tcons, (ar as (class,_)) :: ars) = if member (op =) seen class then (*multiple arities for the same tycon, class pair*) - make_axiom_arity_clause dfg (tcons, lookup_type_const dfg tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) :: - arity_clause dfg seen (n+1) (tcons,ars) + make_axiom_arity_clause (tcons, lookup_type_const tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) :: + arity_clause seen (n+1) (tcons,ars) else - make_axiom_arity_clause dfg (tcons, lookup_type_const dfg tcons ^ "_" ^ class, ar) :: - arity_clause dfg (class::seen) n (tcons,ars) + make_axiom_arity_clause (tcons, lookup_type_const tcons ^ "_" ^ class, ar) :: + arity_clause (class::seen) n (tcons,ars) -fun multi_arity_clause dfg [] = [] - | multi_arity_clause dfg ((tcons, ars) :: tc_arlists) = - arity_clause dfg [] 1 (tcons, ars) @ multi_arity_clause dfg tc_arlists +fun multi_arity_clause [] = [] + | multi_arity_clause ((tcons, ars) :: tc_arlists) = + arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists (*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy provided its arguments have the corresponding sorts.*) @@ -436,7 +378,7 @@ in map try_classes tycons end; (*Proving one (tycon, class) membership may require proving others, so iterate.*) -fun iter_type_class_pairs thy tycons [] = ([], []) +fun iter_type_class_pairs _ _ [] = ([], []) | iter_type_class_pairs thy tycons classes = let val cpairs = type_class_pairs thy tycons classes val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs))) @@ -444,130 +386,16 @@ val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses in (union (op =) classes' classes, union (op =) cpairs' cpairs) end; -fun make_arity_clauses_dfg dfg thy tycons classes = +fun make_arity_clauses thy tycons classes = let val (classes', cpairs) = iter_type_class_pairs thy tycons classes - in (classes', multi_arity_clause dfg cpairs) end; -val make_arity_clauses = make_arity_clauses_dfg false; - -(**** Find occurrences of predicates in clauses ****) - -(*FIXME: multiple-arity checking doesn't work, as update_new is the wrong - function (it flags repeated declarations of a function, even with the same arity)*) - -fun update_many keypairs = fold Symtab.update keypairs - -val add_type_sort_preds = update_many o map pred_of_sort o sorts_on_typs - -fun add_classrel_clause_preds (ClassrelClause {subclass, superclass, ...}) = - Symtab.update (subclass, 1) #> Symtab.update (superclass, 1) - -fun class_of_arityLit (TConsLit (tclass, _, _)) = tclass - | class_of_arityLit (TVarLit (tclass, _)) = tclass; - -fun add_arity_clause_preds (ArityClause {conclLit, premLits, ...}) = - let - val classes = map (make_type_class o class_of_arityLit) - (conclLit :: premLits) - in fold (Symtab.update o rpair 1) classes end; - -(*** Find occurrences of functions in clauses ***) - -fun add_fol_type_funcs (TyVar _) = I - | add_fol_type_funcs (TyFree (s, _)) = Symtab.update (s, 0) - | add_fol_type_funcs (TyConstr ((s, _), tys)) = - Symtab.update (s, length tys) #> fold add_fol_type_funcs tys - -(*TFrees are recorded as constants*) -fun add_type_sort_funcs (TVar _, funcs) = funcs - | add_type_sort_funcs (TFree (a, _), funcs) = - Symtab.update (make_fixed_type_var a, 0) funcs - -fun add_arity_clause_funcs (ArityClause {conclLit,...}) funcs = - let val TConsLit (_, tcons, tvars) = conclLit - in Symtab.update (tcons, length tvars) funcs end; - -(*This type can be overlooked because it is built-in...*) -val init_functab = Symtab.update ("tc_itself", 1) Symtab.empty; - - -(**** String-oriented operations ****) - -fun string_of_clausename (cls_id,ax_name) = - clause_prefix ^ ascii_of ax_name ^ "_" ^ Int.toString cls_id; - -fun string_of_type_clsname (cls_id,ax_name,idx) = - string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx); - - -(**** Producing DFG files ****) - -(*Attach sign in DFG syntax: false means negate.*) -fun dfg_sign true s = s - | dfg_sign false s = "not(" ^ s ^ ")" - -fun dfg_of_type_literal pos (TyLitVar (s, (s', _))) = - dfg_sign pos (s ^ "(" ^ s' ^ ")") - | dfg_of_type_literal pos (TyLitFree (s, (s', _))) = - dfg_sign pos (s ^ "(" ^ s' ^ ")"); - -(*Enclose the clause body by quantifiers, if necessary*) -fun dfg_forall [] body = body - | dfg_forall vars body = "forall([" ^ commas vars ^ "],\n" ^ body ^ ")" - -fun gen_dfg_cls (cls_id, ax_name, Axiom, lits, tylits, vars) = - "clause( %(axiom)\n" ^ - dfg_forall vars ("or(" ^ commas (tylits@lits) ^ ")") ^ ",\n" ^ - string_of_clausename (cls_id,ax_name) ^ ").\n\n" - | gen_dfg_cls (cls_id, ax_name, Conjecture, lits, _, vars) = - "clause( %(negated_conjecture)\n" ^ - dfg_forall vars ("or(" ^ commas lits ^ ")") ^ ",\n" ^ - string_of_clausename (cls_id,ax_name) ^ ").\n\n"; - -fun string_of_arity (name, arity) = "(" ^ name ^ ", " ^ Int.toString arity ^ ")" - -fun string_of_preds [] = "" - | string_of_preds preds = "predicates[" ^ commas(map string_of_arity preds) ^ "].\n"; - -fun string_of_funcs [] = "" - | string_of_funcs funcs = "functions[" ^ commas(map string_of_arity funcs) ^ "].\n" ; - -fun string_of_symbols predstr funcstr = - "list_of_symbols.\n" ^ predstr ^ funcstr ^ "end_of_list.\n\n"; - -fun string_of_start name = "begin_problem(" ^ name ^ ").\n\n"; - -fun string_of_descrip name = - "list_of_descriptions.\nname({*" ^ name ^ - "*}).\nauthor({*Isabelle*}).\nstatus(unknown).\ndescription({*auto-generated*}).\nend_of_list.\n\n" - -fun dfg_tfree_clause tfree_lit = - "clause( %(negated_conjecture)\n" ^ "or( " ^ tfree_lit ^ "),\n" ^ "tfree_tcs" ^ ").\n\n" - -fun dfg_of_arLit (TConsLit (c,t,args)) = - dfg_sign true (make_type_class c ^ "(" ^ t ^ paren_pack args ^ ")") - | dfg_of_arLit (TVarLit (c,str)) = - dfg_sign false (make_type_class c ^ "(" ^ str ^ ")") - -fun dfg_classrelLits sub sup = "not(" ^ sub ^ "(T)), " ^ sup ^ "(T)"; - -fun dfg_classrel_clause (ClassrelClause {axiom_name,subclass,superclass,...}) = - "clause(forall([T],\nor( " ^ dfg_classrelLits subclass superclass ^ ")),\n" ^ - axiom_name ^ ").\n\n"; - -fun string_of_ar axiom_name = arclause_prefix ^ ascii_of axiom_name; - -fun dfg_arity_clause (ArityClause{axiom_name,conclLit,premLits,...}) = - let val TConsLit (_,_,tvars) = conclLit - val lits = map dfg_of_arLit (conclLit :: premLits) - in - "clause( %(axiom)\n" ^ - dfg_forall tvars ("or( " ^ commas lits ^ ")") ^ ",\n" ^ - string_of_ar axiom_name ^ ").\n\n" - end; + in (classes', multi_arity_clause cpairs) end; (**** Produce TPTP files ****) +fun string_of_clausename (cls_id, ax_name) = + clause_prefix ^ ascii_of ax_name ^ "_" ^ Int.toString cls_id + fun tptp_sign true s = s | tptp_sign false s = "~ " ^ s @@ -594,15 +422,16 @@ | tptp_of_arLit (TVarLit (c,str)) = tptp_sign false (make_type_class c ^ "(" ^ str ^ ")") -fun tptp_arity_clause (ArityClause{axiom_name,conclLit,premLits,...}) = - tptp_cnf (string_of_ar axiom_name) "axiom" +fun tptp_arity_clause (ArityClause {axiom_name, conclLit, premLits, ...}) = + tptp_cnf (arclause_prefix ^ ascii_of axiom_name) "axiom" (tptp_clause (map tptp_of_arLit (conclLit :: premLits))) fun tptp_classrelLits sub sup = let val tvar = "(T)" in tptp_clause [tptp_sign false (sub^tvar), tptp_sign true (sup^tvar)] end; -fun tptp_classrel_clause (ClassrelClause {axiom_name,subclass,superclass,...}) = +fun tptp_classrel_clause (ClassrelClause {axiom_name, subclass, superclass, + ...}) = tptp_cnf axiom_name "axiom" (tptp_classrelLits subclass superclass) end; diff -r 9de1add14bac -r f9af8a863bd3 src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Tue Jun 22 18:15:44 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Tue Jun 22 19:10:12 2010 +0200 @@ -7,15 +7,14 @@ signature SLEDGEHAMMER_HOL_CLAUSE = sig + type cnf_thm = Sledgehammer_Fact_Preprocessor.cnf_thm type name = Sledgehammer_FOL_Clause.name type name_pool = Sledgehammer_FOL_Clause.name_pool type kind = Sledgehammer_FOL_Clause.kind type fol_type = Sledgehammer_FOL_Clause.fol_type type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause type arity_clause = Sledgehammer_FOL_Clause.arity_clause - type axiom_name = string type polarity = bool - type hol_clause_id = int datatype combterm = CombConst of name * fol_type * fol_type list (* Const and Free *) | @@ -23,28 +22,23 @@ CombApp of combterm * combterm datatype literal = Literal of polarity * combterm datatype hol_clause = - HOLClause of {clause_id: hol_clause_id, axiom_name: axiom_name, th: thm, - kind: kind, literals: literal list, ctypes_sorts: typ list} + HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind, + literals: literal list, ctypes_sorts: typ list} val type_of_combterm : combterm -> fol_type val strip_combterm_comb : combterm -> combterm * combterm list val literals_of_term : theory -> term -> literal list * typ list val conceal_skolem_somes : int -> (string * term) list -> term -> (string * term) list * term - exception TRIVIAL - val make_conjecture_clauses : bool -> theory -> thm list -> hol_clause list - val make_axiom_clauses : bool -> theory -> - (thm * (axiom_name * hol_clause_id)) list -> (axiom_name * hol_clause) list + exception TRIVIAL of unit + val make_conjecture_clauses : theory -> thm list -> hol_clause list + val make_axiom_clauses : theory -> cnf_thm list -> (string * hol_clause) list val type_wrapper_name : string val get_helper_clauses : - bool -> theory -> bool -> bool -> hol_clause list - -> (thm * (axiom_name * hol_clause_id)) list -> hol_clause list + theory -> bool -> bool -> hol_clause list -> cnf_thm list -> hol_clause list val write_tptp_file : bool -> bool -> bool -> Path.T -> hol_clause list * hol_clause list * hol_clause list * hol_clause list * classrel_clause list * arity_clause list -> name_pool option * int - val write_dfg_file : bool -> bool -> Path.T -> - hol_clause list * hol_clause list * hol_clause list * hol_clause list * - classrel_clause list * arity_clause list -> name_pool option * int end structure Sledgehammer_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE = @@ -67,9 +61,7 @@ (* data types for typed combinator expressions *) (******************************************************) -type axiom_name = string; -type polarity = bool; -type hol_clause_id = int; +type polarity = bool datatype combterm = CombConst of name * fol_type * fol_type list (* Const and Free *) | @@ -79,8 +71,8 @@ datatype literal = Literal of polarity * combterm; datatype hol_clause = - HOLClause of {clause_id: hol_clause_id, axiom_name: axiom_name, th: thm, - kind: kind, literals: literal list, ctypes_sorts: typ list}; + HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind, + literals: literal list, ctypes_sorts: typ list} (*********************************************************************) @@ -98,65 +90,66 @@ fun isTaut (HOLClause {literals,...}) = exists isTrue literals; -fun type_of dfg (Type (a, Ts)) = - let val (folTypes,ts) = types_of dfg Ts in - (TyConstr (`(make_fixed_type_const dfg) a, folTypes), ts) +fun type_of (Type (a, Ts)) = + let val (folTypes,ts) = types_of Ts in + (TyConstr (`make_fixed_type_const a, folTypes), ts) end - | type_of _ (tp as TFree (a, _)) = (TyFree (`make_fixed_type_var a), [tp]) - | type_of _ (tp as TVar (x, _)) = + | type_of (tp as TFree (a, _)) = (TyFree (`make_fixed_type_var a), [tp]) + | type_of (tp as TVar (x, _)) = (TyVar (make_schematic_type_var x, string_of_indexname x), [tp]) -and types_of dfg Ts = - let val (folTyps,ts) = ListPair.unzip (map (type_of dfg) Ts) - in (folTyps, union_all ts) end; +and types_of Ts = + let val (folTyps, ts) = ListPair.unzip (map type_of Ts) in + (folTyps, union_all ts) + end (* same as above, but no gathering of sort information *) -fun simp_type_of dfg (Type (a, Ts)) = - TyConstr (`(make_fixed_type_const dfg) a, map (simp_type_of dfg) Ts) - | simp_type_of _ (TFree (a, _)) = TyFree (`make_fixed_type_var a) - | simp_type_of _ (TVar (x, _)) = - TyVar (make_schematic_type_var x, string_of_indexname x); +fun simp_type_of (Type (a, Ts)) = + TyConstr (`make_fixed_type_const a, map simp_type_of Ts) + | simp_type_of (TFree (a, _)) = TyFree (`make_fixed_type_var a) + | simp_type_of (TVar (x, _)) = + TyVar (make_schematic_type_var x, string_of_indexname x) (* convert a Term.term (with combinators) into a combterm, also accummulate sort info *) -fun combterm_of dfg thy (Const (c, T)) = +fun combterm_of thy (Const (c, T)) = let - val (tp, ts) = type_of dfg T + val (tp, ts) = type_of T val tvar_list = (if String.isPrefix skolem_theory_name c then [] |> Term.add_tvarsT T |> map TVar else (c, T) |> Sign.const_typargs thy) - |> map (simp_type_of dfg) - val c' = CombConst (`(make_fixed_const dfg) c, tp, tvar_list) + |> map simp_type_of + val c' = CombConst (`make_fixed_const c, tp, tvar_list) in (c',ts) end - | combterm_of dfg _ (Free(v, T)) = - let val (tp,ts) = type_of dfg T + | combterm_of _ (Free(v, T)) = + let val (tp,ts) = type_of T val v' = CombConst (`make_fixed_var v, tp, []) in (v',ts) end - | combterm_of dfg _ (Var(v, T)) = - let val (tp,ts) = type_of dfg T + | combterm_of _ (Var(v, T)) = + let val (tp,ts) = type_of T val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp) in (v',ts) end - | combterm_of dfg thy (P $ Q) = - let val (P',tsP) = combterm_of dfg thy P - val (Q',tsQ) = combterm_of dfg thy Q - in (CombApp(P',Q'), union (op =) tsP tsQ) end - | combterm_of _ _ (t as Abs _) = raise CLAUSE ("HOL clause", t); - -fun predicate_of dfg thy ((@{const Not} $ P), polarity) = predicate_of dfg thy (P, not polarity) - | predicate_of dfg thy (t,polarity) = (combterm_of dfg thy (Envir.eta_contract t), polarity); + | combterm_of thy (P $ Q) = + let val (P', tsP) = combterm_of thy P + val (Q', tsQ) = combterm_of thy Q + in (CombApp (P', Q'), union (op =) tsP tsQ) end + | combterm_of _ (t as Abs _) = raise CLAUSE ("HOL clause", t) -fun literals_of_term1 dfg thy args (@{const Trueprop} $ P) = literals_of_term1 dfg thy args P - | literals_of_term1 dfg thy args (@{const "op |"} $ P $ Q) = - literals_of_term1 dfg thy (literals_of_term1 dfg thy args P) Q - | literals_of_term1 dfg thy (lits,ts) P = - let val ((pred,ts'),pol) = predicate_of dfg thy (P,true) - in - (Literal(pol,pred)::lits, union (op =) ts ts') - end; +fun predicate_of thy ((@{const Not} $ P), polarity) = + predicate_of thy (P, not polarity) + | predicate_of thy (t, polarity) = + (combterm_of thy (Envir.eta_contract t), polarity) -fun literals_of_term_dfg dfg thy P = literals_of_term1 dfg thy ([],[]) P; -val literals_of_term = literals_of_term_dfg false; +fun literals_of_term1 args thy (@{const Trueprop} $ P) = + literals_of_term1 args thy P + | literals_of_term1 args thy (@{const "op |"} $ P $ Q) = + literals_of_term1 (literals_of_term1 args thy P) thy Q + | literals_of_term1 (lits, ts) thy P = + let val ((pred, ts'), pol) = predicate_of thy (P, true) in + (Literal (pol, pred) :: lits, union (op =) ts ts') + end +val literals_of_term = literals_of_term1 ([], []) fun skolem_name i j num_T_args = skolem_prefix ^ (space_implode "_" (map Int.toString [i, j, num_T_args])) ^ @@ -168,6 +161,7 @@ fun aux skolem_somes (t as (Const (@{const_name skolem_id}, Type (_, [_, T])) $ _)) = let + val t = Envir.beta_eta_contract t val (skolem_somes, s) = if i = ~1 then (skolem_somes, @{const_name undefined}) @@ -195,46 +189,43 @@ (skolem_somes, t) (* Trivial problem, which resolution cannot handle (empty clause) *) -exception TRIVIAL; +exception TRIVIAL of unit (* making axiom and conjecture clauses *) -fun make_clause dfg thy (clause_id, axiom_name, kind, th) skolem_somes = +fun make_clause thy (clause_id, axiom_name, kind, th) skolem_somes = let val (skolem_somes, t) = th |> prop_of |> conceal_skolem_somes clause_id skolem_somes - val (lits, ctypes_sorts) = literals_of_term_dfg dfg thy t + val (lits, ctypes_sorts) = literals_of_term thy t in if forall isFalse lits then - raise TRIVIAL + raise TRIVIAL () else (skolem_somes, HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th, kind = kind, literals = lits, ctypes_sorts = ctypes_sorts}) end -fun add_axiom_clause dfg thy (th, (name, id)) (skolem_somes, clss) = +fun add_axiom_clause thy (th, ((name, id), _ : thm)) (skolem_somes, clss) = let - val (skolem_somes, cls) = - make_clause dfg thy (id, name, Axiom, th) skolem_somes + val (skolem_somes, cls) = make_clause thy (id, name, Axiom, th) skolem_somes in (skolem_somes, clss |> not (isTaut cls) ? cons (name, cls)) end -fun make_axiom_clauses dfg thy clauses = - ([], []) |> fold (add_axiom_clause dfg thy) clauses |> snd +fun make_axiom_clauses thy clauses = + ([], []) |> fold (add_axiom_clause thy) clauses |> snd -fun make_conjecture_clauses dfg thy = +fun make_conjecture_clauses thy = let fun aux _ _ [] = [] | aux n skolem_somes (th :: ths) = let val (skolem_somes, cls) = - make_clause dfg thy (n, "conjecture", Conjecture, th) skolem_somes + make_clause thy (n, "conjecture", Conjecture, th) skolem_somes in cls :: aux (n + 1) skolem_somes ths end in aux 0 [] end (**********************************************************************) -(* convert clause into ATP specific formats: *) -(* TPTP used by Vampire and E *) -(* DFG used by SPASS *) +(* convert clause into TPTP format *) (**********************************************************************) (*Result of a function type; no need to check that the argument type matches.*) @@ -314,17 +305,11 @@ string_of_combterm params c #>> prefix "hBOOL" o paren_pack o single fun string_of_predicate (params as (_, explicit_apply, _, cnh)) t = - case t of - (CombApp (CombApp (CombConst (("equal", _), _, _), t1), t2)) => - (* DFG only: new TPTP prefers infix equality *) - pool_map (string_of_combterm params) [t1, t2] - #>> prefix "equal" o paren_pack - | _ => - case #1 (strip_combterm_comb t) of - CombConst ((s, _), _, _) => - (if needs_hBOOL explicit_apply cnh s then boolify else string_of_combterm) - params t - | _ => boolify params t + case #1 (strip_combterm_comb t) of + CombConst ((s, _), _, _) => + (if needs_hBOOL explicit_apply cnh s then boolify else string_of_combterm) + params t + | _ => boolify params t (*** TPTP format ***) @@ -352,7 +337,7 @@ fun tptp_clause params (cls as HOLClause {axiom_name, clause_id, kind, ...}) pool = -let + let val ((lits, tylits), pool) = tptp_type_literals params (kind = Conjecture) cls pool in @@ -360,94 +345,6 @@ end -(*** DFG format ***) - -fun dfg_literal params (Literal (pos, pred)) = - string_of_predicate params pred #>> dfg_sign pos - -fun dfg_type_literals params pos (HOLClause {literals, ctypes_sorts, ...}) = - pool_map (dfg_literal params) literals - #>> rpair (map (dfg_of_type_literal pos) - (type_literals_for_types ctypes_sorts)) - -fun get_uvars (CombConst _) vars pool = (vars, pool) - | get_uvars (CombVar (name, _)) vars pool = - nice_name name pool |>> (fn var => var :: vars) - | get_uvars (CombApp (P, Q)) vars pool = - let val (vars, pool) = get_uvars P vars pool in get_uvars Q vars pool end - -fun get_uvars_l (Literal (_, c)) = get_uvars c []; - -fun dfg_vars (HOLClause {literals, ...}) = - pool_map get_uvars_l literals #>> union_all - -fun dfg_clause params (cls as HOLClause {axiom_name, clause_id, kind, - ctypes_sorts, ...}) pool = - let - val ((lits, tylits), pool) = - dfg_type_literals params (kind = Conjecture) cls pool - val (vars, pool) = dfg_vars cls pool - val tvars = get_tvar_strs ctypes_sorts - in - ((gen_dfg_cls (clause_id, axiom_name, kind, lits, tylits, tvars @ vars), - tylits), pool) - end - - -(** For DFG format: accumulate function and predicate declarations **) - -fun add_types tvars = fold add_fol_type_funcs tvars - -fun add_decls (full_types, explicit_apply, cma, cnh) - (CombConst ((c, _), ctp, tvars)) (funcs, preds) = - (if c = "equal" then - (add_types tvars funcs, preds) - else - let val arity = min_arity_of cma c - val ntys = if not full_types then length tvars else 0 - val addit = Symtab.update(c, arity + ntys) - in - if needs_hBOOL explicit_apply cnh c then - (add_types tvars (addit funcs), preds) - else - (add_types tvars funcs, addit preds) - end) |>> full_types ? add_fol_type_funcs ctp - | add_decls _ (CombVar (_, ctp)) (funcs, preds) = - (add_fol_type_funcs ctp funcs, preds) - | add_decls params (CombApp (P, Q)) decls = - decls |> add_decls params P |> add_decls params Q - -fun add_literal_decls params (Literal (_, c)) = add_decls params c - -fun add_clause_decls params (HOLClause {literals, ...}) decls = - fold (add_literal_decls params) literals decls - handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities") - -fun decls_of_clauses (params as (full_types, explicit_apply, _, _)) clauses - arity_clauses = - let - val functab = - init_functab - |> fold Symtab.update [(type_wrapper_name, 2), ("hAPP", 2), - ("tc_bool", 0)] - val predtab = Symtab.empty |> Symtab.update ("hBOOL", 1) - val (functab, predtab) = - (functab, predtab) |> fold (add_clause_decls params) clauses - |>> fold add_arity_clause_funcs arity_clauses - in (Symtab.dest functab, Symtab.dest predtab) end - -fun add_clause_preds (HOLClause {ctypes_sorts, ...}) preds = - fold add_type_sort_preds ctypes_sorts preds - handle Symtab.DUP a => error ("predicate " ^ a ^ " has multiple arities") - -(*Higher-order clauses have only the predicates hBOOL and type classes.*) -fun preds_of_clauses clauses clsrel_clauses arity_clauses = - Symtab.empty - |> fold add_clause_preds clauses - |> fold add_arity_clause_preds arity_clauses - |> fold add_classrel_clause_preds clsrel_clauses - |> Symtab.dest - (**********************************************************************) (* write clauses to files *) (**********************************************************************) @@ -461,7 +358,7 @@ fun count_clause (HOLClause {literals, ...}) = fold count_literal literals -val raw_cnf_rules_pairs = map (fn (name, thm) => (thm, (name, 0))) +val raw_cnf_rules_pairs = map (fn (name, thm) => (thm, ((name, 0), thm))) fun cnf_helper_thms thy raw = map (`Thm.get_name_hint) #> (if raw then raw_cnf_rules_pairs else cnf_rules_pairs thy) @@ -479,9 +376,9 @@ Symtab.make (maps (maps (map (rpair 0) o fst)) [optional_helpers, optional_typed_helpers]) -fun get_helper_clauses dfg thy is_FO full_types conjectures axcls = +fun get_helper_clauses thy is_FO full_types conjectures axcls = let - val axclauses = map snd (make_axiom_clauses dfg thy axcls) + val axclauses = map snd (make_axiom_clauses thy axcls) val ct = fold (fold count_clause) [conjectures, axclauses] init_counters fun is_needed c = the (Symtab.lookup ct c) > 0 val cnfs = @@ -491,7 +388,7 @@ if exists is_needed ss then cnf_helper_thms thy raw ths else [])) @ (if is_FO then [] else cnf_helper_thms thy false mandatory_helpers) - in map snd (make_axiom_clauses dfg thy cnfs) end + in map snd (make_axiom_clauses thy cnfs) end (*Find the minimal arity of each function mentioned in the term. Also, note which uses are not at top level, to see if hBOOL is needed.*) @@ -520,7 +417,7 @@ (const_min_arity, const_needs_hBOOL) = fold count_constants_lit literals (const_min_arity, const_needs_hBOOL); -fun display_arity explicit_apply const_needs_hBOOL (c,n) = +fun display_arity explicit_apply const_needs_hBOOL (c, n) = trace_msg (fn () => "Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^ (if needs_hBOOL explicit_apply const_needs_hBOOL c then @@ -540,10 +437,6 @@ in (const_min_arity, const_needs_hBOOL) end else (Symtab.empty, Symtab.empty); -fun header () = - "% This file was generated by Isabelle (most likely Sledgehammer)\n" ^ - "% " ^ timestamp () ^ "\n" - (* TPTP format *) fun write_tptp_file readable_names full_types explicit_apply file clauses = @@ -571,7 +464,8 @@ + length helper_clss val _ = File.write_list file - (header () :: + ("% This file was generated by Isabelle (most likely Sledgehammer)\n\ + \% " ^ timestamp () ^ "\n" :: section "Relevant fact" ax_clss @ section "Class relationship" classrel_clss @ section "Arity declaration" arity_clss @ @@ -580,53 +474,4 @@ section "Type variable" tfree_clss) in (pool, conjecture_offset) end -(* DFG format *) - -fun dfg_tfree_predicate s = (first_field "(" s |> the |> fst, 1) - -fun write_dfg_file full_types explicit_apply file clauses = - let - (* Some of the helper functions below are not name-pool-aware. However, - there's no point in adding name pool support if the DFG format is on its - way out anyway. *) - val pool = NONE - val (conjectures, axclauses, _, helper_clauses, - classrel_clauses, arity_clauses) = clauses - val (cma, cnh) = count_constants explicit_apply clauses - val params = (full_types, explicit_apply, cma, cnh) - val ((conjecture_clss, tfree_litss), pool) = - pool_map (dfg_clause params) conjectures pool |>> ListPair.unzip - val tfree_lits = union_all tfree_litss - val problem_name = Path.implode (Path.base file) - val (axstrs, pool) = pool_map (apfst fst oo dfg_clause params) axclauses pool - val tfree_clss = map dfg_tfree_clause tfree_lits - val tfree_preds = map dfg_tfree_predicate tfree_lits - val (helper_clauses_strs, pool) = - pool_map (apfst fst oo dfg_clause params) helper_clauses pool - val (funcs, cl_preds) = - decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses - val ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses - val preds = tfree_preds @ cl_preds @ ty_preds - val conjecture_offset = - length axclauses + length classrel_clauses + length arity_clauses - + length helper_clauses - val _ = - File.write_list file - (header () :: - string_of_start problem_name :: - string_of_descrip problem_name :: - string_of_symbols (string_of_funcs funcs) - (string_of_preds preds) :: - "list_of_clauses(axioms, cnf).\n" :: - axstrs @ - map dfg_classrel_clause classrel_clauses @ - map dfg_arity_clause arity_clauses @ - helper_clauses_strs @ - ["end_of_list.\n\nlist_of_clauses(conjectures, cnf).\n"] @ - conjecture_clss @ - tfree_clss @ - ["end_of_list.\n\n", - "end_problem.\n"]) - in (pool, conjecture_offset) end - end; diff -r 9de1add14bac -r f9af8a863bd3 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Jun 22 18:15:44 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Jun 22 19:10:12 2010 +0200 @@ -58,7 +58,6 @@ {add = [], del = ns, only = false} fun only_relevance_override ns : relevance_override = {add = ns, del = [], only = true} -val no_relevance_override = add_to_relevance_override [] fun merge_relevance_override_pairwise (r1 : relevance_override) (r2 : relevance_override) = {add = #add r1 @ #add r2, del = #del r1 @ #del r2, @@ -166,7 +165,7 @@ val infinity_time_in_secs = 60 * 60 * 24 * 365 val the_timeout = the_default (Time.fromSeconds infinity_time_in_secs) -fun extract_params thy default_params override_params = +fun extract_params default_params override_params = let val override_params = map unalias_raw_param override_params val raw_params = rev override_params @ rev default_params @@ -216,7 +215,7 @@ timeout = timeout, minimize_timeout = minimize_timeout} end -fun get_params thy = extract_params thy (default_raw_params thy) +fun get_params thy = extract_params (default_raw_params thy) fun default_params thy = get_params thy o map (apsnd single) val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal @@ -264,7 +263,6 @@ val running_atpsN = "running_atps" val kill_atpsN = "kill_atps" val refresh_tptpN = "refresh_tptp" -val helpN = "help" fun minimizize_raw_param_name "timeout" = "minimize_timeout" | minimizize_raw_param_name name = name diff -r 9de1add14bac -r f9af8a863bd3 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Jun 22 18:15:44 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Jun 22 19:10:12 2010 +0200 @@ -368,7 +368,7 @@ | add_type_constraint _ = I fun is_positive_literal (@{const Not} $ _) = false - | is_positive_literal t = true + | is_positive_literal _ = true fun negate_term thy (Const (@{const_name All}, T) $ Abs (s, T', t')) = Const (@{const_name Ex}, T) $ Abs (s, T', negate_term thy t') @@ -551,11 +551,11 @@ (* Vampire is keen on producing these. *) fun is_trivial_formula (@{const Not} $ (Const (@{const_name "op ="}, _) $ t1 $ t2)) = (t1 aconv t2) - | is_trivial_formula t = false + | is_trivial_formula _ = false -fun add_desired_line _ _ _ _ _ (line as Definition (num, _, _)) (j, lines) = +fun add_desired_line _ _ _ _ (line as Definition (num, _, _)) (j, lines) = (j, line :: map (replace_deps_in_line (num, [])) lines) - | add_desired_line ctxt isar_shrink_factor conjecture_shape thm_names frees + | add_desired_line isar_shrink_factor conjecture_shape thm_names frees (Inference (num, t, deps)) (j, lines) = (j + 1, if is_axiom_clause_number thm_names num orelse @@ -667,7 +667,7 @@ fun forall_vars t = fold_rev forall_of (map Var (Term.add_vars t [])) t -fun step_for_line _ _ (Definition (num, t1, t2)) = Let (t1, t2) +fun step_for_line _ _ (Definition (_, t1, t2)) = Let (t1, t2) | step_for_line _ _ (Inference (num, t, [])) = Assume ((raw_prefix, num), t) | step_for_line thm_names j (Inference (num, t, deps)) = Have (if j = 1 then [Show] else [], (raw_prefix, num), @@ -683,7 +683,7 @@ |> decode_lines ctxt full_types tfrees |> rpair [] |-> fold_rev (add_line conjecture_shape thm_names) |> rpair [] |-> fold_rev add_nontrivial_line - |> rpair (0, []) |-> fold_rev (add_desired_line ctxt isar_shrink_factor + |> rpair (0, []) |-> fold_rev (add_desired_line isar_shrink_factor conjecture_shape thm_names frees) |> snd in @@ -722,7 +722,7 @@ else if forall (curry (op =) (hd proof1) o hd) (tl proofs) then aux (hd proof1 :: proof_tail) (map tl proofs) else case hd proof1 of - Have ([], l, t, by) => + Have ([], l, t, _) => (* FIXME: should we really ignore the "by"? *) if forall (fn Have ([], l', t', _) :: _ => (l, t) = (l', t') | _ => false) (tl proofs) andalso not (exists (member (op =) (maps new_labels_of proofs)) @@ -755,7 +755,7 @@ first_pass (proof, contra) |>> cons step | first_pass ((step as Let _) :: proof, contra) = first_pass (proof, contra) |>> cons step - | first_pass ((step as Assume (l as (_, num), t)) :: proof, contra) = + | first_pass ((step as Assume (l as (_, num), _)) :: proof, contra) = if member (op =) concl_ls l then first_pass (proof, contra ||> l = hd concl_ls ? cons step) else @@ -992,6 +992,13 @@ do_indent 0 ^ (if n <> 1 then "next" else "qed") ^ "\n" in do_proof end +fun strip_subgoal goal i = + let + val (t, frees) = Logic.goal_params (prop_of goal) i + val hyp_ts = t |> Logic.strip_assums_hyp |> map (curry subst_bounds frees) + val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees + in (rev (map dest_Free frees), hyp_ts, concl_t) end + fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) (other_params as (full_types, _, atp_proof, thm_names, goal, i)) = diff -r 9de1add14bac -r f9af8a863bd3 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue Jun 22 18:15:44 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue Jun 22 19:10:12 2010 +0200 @@ -6,7 +6,6 @@ signature SLEDGEHAMMER_UTIL = sig - val pairf : ('a -> 'b) -> ('a -> 'c) -> 'a -> 'b * 'c val plural_s : int -> string val serial_commas : string -> string list -> string list val replace_all : string -> string -> string -> string @@ -24,8 +23,6 @@ structure Sledgehammer_Util : SLEDGEHAMMER_UTIL = struct -fun pairf f g x = (f x, g x) - fun plural_s n = if n = 1 then "" else "s" fun serial_commas _ [] = ["??"]