# HG changeset patch # User blanchet # Date 1280254574 -7200 # Node ID dc56a9a8e19d4329a3d3cbd12a0f6ea85525f5ab # Parent 479dfaae0b521340aa425620baa11c0be4ee80aa# Parent 0c15b8a655cd73eb592cb2a36acddc21c2563d2e merge diff -r 0c15b8a655cd -r dc56a9a8e19d src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Jul 27 17:10:27 2010 +0200 +++ b/src/HOL/IsaMakefile Tue Jul 27 20:16:14 2010 +0200 @@ -269,7 +269,7 @@ $(SRC)/Provers/Arith/extract_common_term.ML \ $(SRC)/Tools/Metis/metis.ML \ Tools/ATP_Manager/async_manager.ML \ - Tools/ATP_Manager/atp_manager.ML \ + Tools/ATP_Manager/atp_problem.ML \ Tools/ATP_Manager/atp_systems.ML \ Tools/choice_specification.ML \ Tools/int_arith.ML \ @@ -319,11 +319,11 @@ Tools/Sledgehammer/meson_tactic.ML \ Tools/Sledgehammer/metis_clauses.ML \ Tools/Sledgehammer/metis_tactics.ML \ + Tools/Sledgehammer/sledgehammer.ML \ Tools/Sledgehammer/sledgehammer_fact_filter.ML \ Tools/Sledgehammer/sledgehammer_fact_minimizer.ML \ Tools/Sledgehammer/sledgehammer_isar.ML \ Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML \ - Tools/Sledgehammer/sledgehammer_tptp_format.ML \ Tools/Sledgehammer/sledgehammer_util.ML \ Tools/SMT/cvc3_solver.ML \ Tools/SMT/smtlib_interface.ML \ diff -r 0c15b8a655cd -r dc56a9a8e19d src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Jul 27 17:10:27 2010 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Jul 27 20:16:14 2010 +0200 @@ -283,7 +283,7 @@ fun default_atp_name () = hd (#atps (Sledgehammer_Isar.default_params thy [])) handle Empty => error "No ATP available." - fun get_prover name = (name, ATP_Manager.get_prover thy name) + fun get_prover name = (name, Sledgehammer.get_prover_fun thy name) in (case AList.lookup (op =) args proverK of SOME name => get_prover name @@ -301,11 +301,11 @@ let 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) + val change_dir = (fn SOME d => Config.put Sledgehammer.dest_dir d | _ => I) val ctxt' = ctxt |> change_dir dir - |> Config.put ATP_Systems.measure_runtime true + |> Config.put Sledgehammer.measure_runtime true val params = Sledgehammer_Isar.default_params thy [] val problem = {subgoal = 1, goal = (ctxt', (facts, goal)), @@ -315,13 +315,13 @@ (case hard_timeout of NONE => I | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs)) - val ({outcome, message, relevant_thm_names, - atp_run_time_in_msecs = time_atp, ...}: ATP_Manager.prover_result, + val ({outcome, message, used_thm_names, + atp_run_time_in_msecs = time_atp, ...} : Sledgehammer.prover_result, time_isa) = time_limit (Mirabelle.cpu_time (prover params (K "") (Time.fromSeconds timeout))) problem in case outcome of - NONE => (message, SH_OK (time_isa, time_atp, relevant_thm_names)) + NONE => (message, SH_OK (time_isa, time_atp, used_thm_names)) | SOME _ => (message, SH_FAIL (time_isa, time_atp)) end handle ERROR msg => ("error: " ^ msg, SH_ERROR) diff -r 0c15b8a655cd -r dc56a9a8e19d src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Tue Jul 27 17:10:27 2010 +0200 +++ b/src/HOL/Sledgehammer.thy Tue Jul 27 20:16:14 2010 +0200 @@ -1,6 +1,6 @@ (* Title: HOL/Sledgehammer.thy - Author: Lawrence C Paulson - Author: Jia Meng, NICTA + Author: Lawrence C. Paulson, Cambridge University Computer Laboratory + Author: Jia Meng, Cambridge University Computer Laboratory and NICTA Author: Fabian Immler, TU Muenchen Author: Jasmin Blanchette, TU Muenchen *) @@ -10,18 +10,18 @@ theory Sledgehammer imports Plain Hilbert_Choice uses - "~~/src/Tools/Metis/metis.ML" + ("Tools/ATP_Manager/async_manager.ML") + ("Tools/ATP_Manager/atp_problem.ML") + ("Tools/ATP_Manager/atp_systems.ML") + ("~~/src/Tools/Metis/metis.ML") ("Tools/Sledgehammer/clausifier.ML") ("Tools/Sledgehammer/meson_tactic.ML") ("Tools/Sledgehammer/metis_clauses.ML") ("Tools/Sledgehammer/metis_tactics.ML") ("Tools/Sledgehammer/sledgehammer_util.ML") ("Tools/Sledgehammer/sledgehammer_fact_filter.ML") - ("Tools/Sledgehammer/sledgehammer_tptp_format.ML") ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML") - ("Tools/ATP_Manager/async_manager.ML") - ("Tools/ATP_Manager/atp_manager.ML") - ("Tools/ATP_Manager/atp_systems.ML") + ("Tools/Sledgehammer/sledgehammer.ML") ("Tools/Sledgehammer/sledgehammer_fact_minimizer.ML") ("Tools/Sledgehammer/sledgehammer_isar.ML") begin @@ -85,6 +85,12 @@ apply (simp add: COMBC_def) done +use "Tools/ATP_Manager/async_manager.ML" +use "Tools/ATP_Manager/atp_problem.ML" +use "Tools/ATP_Manager/atp_systems.ML" +setup ATP_Systems.setup + +use "~~/src/Tools/Metis/metis.ML" use "Tools/Sledgehammer/clausifier.ML" use "Tools/Sledgehammer/meson_tactic.ML" setup Meson_Tactic.setup @@ -94,12 +100,9 @@ use "Tools/Sledgehammer/sledgehammer_util.ML" use "Tools/Sledgehammer/sledgehammer_fact_filter.ML" -use "Tools/Sledgehammer/sledgehammer_tptp_format.ML" use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML" -use "Tools/ATP_Manager/async_manager.ML" -use "Tools/ATP_Manager/atp_manager.ML" -use "Tools/ATP_Manager/atp_systems.ML" -setup ATP_Systems.setup +use "Tools/Sledgehammer/sledgehammer.ML" +setup Sledgehammer.setup use "Tools/Sledgehammer/sledgehammer_fact_minimizer.ML" use "Tools/Sledgehammer/sledgehammer_isar.ML" setup Metis_Tactics.setup diff -r 0c15b8a655cd -r dc56a9a8e19d src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Jul 27 17:10:27 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,171 +0,0 @@ -(* Title: HOL/Tools/ATP_Manager/atp_manager.ML - Author: Fabian Immler, TU Muenchen - Author: Makarius - Author: Jasmin Blanchette, TU Muenchen - -Central manager component for ATP threads. -*) - -signature ATP_MANAGER = -sig - type relevance_override = Sledgehammer_Fact_Filter.relevance_override - type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command - type params = - {debug: bool, - verbose: bool, - overlord: bool, - atps: string list, - full_types: bool, - explicit_apply: bool, - relevance_threshold: real, - relevance_convergence: real, - theory_relevant: bool option, - defs_relevant: bool, - isar_proof: bool, - isar_shrink_factor: int, - timeout: Time.time, - minimize_timeout: Time.time} - type problem = - {subgoal: int, - goal: Proof.context * (thm list * thm), - relevance_override: relevance_override, - axiom_clauses: (string * thm) list option, - filtered_clauses: (string * thm) list option} - datatype failure = - Unprovable | IncompleteUnprovable | CantConnect | TimedOut | - OutOfResources | OldSpass | MalformedInput | MalformedOutput | UnknownError - type prover_result = - {outcome: failure option, - message: string, - pool: string Symtab.table, - relevant_thm_names: string list, - atp_run_time_in_msecs: int, - output: string, - proof: string, - internal_thm_names: string Vector.vector, - conjecture_shape: int list, - filtered_clauses: (string * thm) list} - type prover = - params -> minimize_command -> Time.time -> problem -> prover_result - - val kill_atps: unit -> unit - val running_atps: unit -> unit - val messages: int option -> unit - val add_prover: string * prover -> theory -> theory - val get_prover: theory -> string -> prover - val available_atps: theory -> unit - val start_prover_thread : - params -> int -> int -> relevance_override -> (string -> minimize_command) - -> Proof.state -> string -> unit -end; - -structure ATP_Manager : ATP_MANAGER = -struct - -open Metis_Clauses -open Sledgehammer_Fact_Filter -open Sledgehammer_Proof_Reconstruct - -(** The Sledgehammer **) - -val das_Tool = "Sledgehammer" - -fun kill_atps () = Async_Manager.kill_threads das_Tool "ATPs" -fun running_atps () = Async_Manager.running_threads das_Tool "ATPs" -val messages = Async_Manager.thread_messages das_Tool "ATP" - -(** problems, results, provers, etc. **) - -type params = - {debug: bool, - verbose: bool, - overlord: bool, - atps: string list, - full_types: bool, - explicit_apply: bool, - relevance_threshold: real, - relevance_convergence: real, - theory_relevant: bool option, - defs_relevant: bool, - isar_proof: bool, - isar_shrink_factor: int, - timeout: Time.time, - minimize_timeout: Time.time} - -type problem = - {subgoal: int, - goal: Proof.context * (thm list * thm), - relevance_override: relevance_override, - axiom_clauses: (string * thm) list option, - filtered_clauses: (string * thm) list option} - -datatype failure = - Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources | - OldSpass | MalformedInput | MalformedOutput | UnknownError - -type prover_result = - {outcome: failure option, - message: string, - pool: string Symtab.table, - relevant_thm_names: string list, - atp_run_time_in_msecs: int, - output: string, - proof: string, - internal_thm_names: string Vector.vector, - conjecture_shape: int list, - filtered_clauses: (string * thm) list} - -type prover = - params -> minimize_command -> Time.time -> problem -> prover_result - -(* named provers *) - -structure Data = Theory_Data -( - type T = (prover * stamp) Symtab.table; - val empty = Symtab.empty; - val extend = I; - fun merge data : T = Symtab.merge (eq_snd op =) data - handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".") -); - -fun add_prover (name, prover) thy = - Data.map (Symtab.update_new (name, (prover, stamp ()))) thy - handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".") - -fun get_prover thy name = - the (Symtab.lookup (Data.get thy) name) |> fst - handle Option.Option => error ("Unknown ATP: " ^ name ^ ".") - -fun available_atps thy = - priority ("Available ATPs: " ^ - commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".") - - -(* start prover thread *) - -fun start_prover_thread (params as {verbose, full_types, timeout, ...}) i n - relevance_override minimize_command proof_state name = - let - val birth_time = Time.now () - val death_time = Time.+ (birth_time, timeout) - val prover = get_prover (Proof.theory_of proof_state) name - val {context = ctxt, facts, goal} = Proof.goal proof_state; - val desc = - "ATP " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^ - Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)); - in - Async_Manager.launch das_Tool verbose birth_time death_time desc - (fn () => - let - val problem = - {subgoal = i, goal = (ctxt, (facts, goal)), - relevance_override = relevance_override, axiom_clauses = NONE, - filtered_clauses = NONE} - in - prover params (minimize_command name) timeout problem |> #message - handle ERROR message => "Error: " ^ message ^ "\n" - end) - end - -end; diff -r 0c15b8a655cd -r dc56a9a8e19d src/HOL/Tools/ATP_Manager/atp_problem.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/ATP_Manager/atp_problem.ML Tue Jul 27 20:16:14 2010 +0200 @@ -0,0 +1,152 @@ +(* Title: HOL/Tools/ATP_Manager/atp_problem.ML + Author: Jia Meng, Cambridge University Computer Laboratory and NICTA + Author: Jasmin Blanchette, TU Muenchen + +TPTP syntax. +*) + +signature ATP_PROBLEM = +sig + datatype 'a fo_term = ATerm of 'a * 'a fo_term list + datatype quantifier = AForall | AExists + datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff + datatype ('a, 'b) formula = + AQuant of quantifier * 'a list * ('a, 'b) formula | + AConn of connective * ('a, 'b) formula list | + APred of 'b + + datatype kind = Axiom | Conjecture + datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula + type 'a problem = (string * 'a problem_line list) list + + val timestamp : unit -> string + val is_tptp_variable : string -> bool + val strings_for_tptp_problem : + (string * string problem_line list) list -> string list + val nice_tptp_problem : + bool -> ('a * (string * string) problem_line list) list + -> ('a * string problem_line list) list + * (string Symtab.table * string Symtab.table) option +end; + +structure ATP_Problem : ATP_PROBLEM = +struct + +(** ATP problem **) + +datatype 'a fo_term = ATerm of 'a * 'a fo_term list +datatype quantifier = AForall | AExists +datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff +datatype ('a, 'b) formula = + AQuant of quantifier * 'a list * ('a, 'b) formula | + AConn of connective * ('a, 'b) formula list | + APred of 'b + +datatype kind = Axiom | Conjecture +datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula +type 'a problem = (string * 'a problem_line list) list + +val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now + +fun string_for_term (ATerm (s, [])) = s + | string_for_term (ATerm (s, ts)) = + if s = "equal" then space_implode " = " (map string_for_term ts) + else s ^ "(" ^ commas (map string_for_term ts) ^ ")" +fun string_for_quantifier AForall = "!" + | string_for_quantifier AExists = "?" +fun string_for_connective ANot = "~" + | string_for_connective AAnd = "&" + | string_for_connective AOr = "|" + | string_for_connective AImplies = "=>" + | string_for_connective AIf = "<=" + | string_for_connective AIff = "<=>" + | string_for_connective ANotIff = "<~>" +fun string_for_formula (AQuant (q, xs, phi)) = + string_for_quantifier q ^ "[" ^ commas xs ^ "] : " ^ + string_for_formula phi + | string_for_formula (AConn (ANot, [APred (ATerm ("equal", ts))])) = + space_implode " != " (map string_for_term ts) + | string_for_formula (AConn (c, [phi])) = + string_for_connective c ^ " " ^ string_for_formula phi + | string_for_formula (AConn (c, phis)) = + "(" ^ space_implode (" " ^ string_for_connective c ^ " ") + (map string_for_formula phis) ^ ")" + | string_for_formula (APred tm) = string_for_term tm + +fun string_for_problem_line (Fof (ident, kind, phi)) = + "fof(" ^ ident ^ ", " ^ + (case kind of Axiom => "axiom" | Conjecture => "conjecture") ^ ",\n" ^ + " (" ^ string_for_formula phi ^ ")).\n" +fun strings_for_tptp_problem problem = + "% This file was generated by Isabelle (most likely Sledgehammer)\n\ + \% " ^ timestamp () ^ "\n" :: + maps (fn (_, []) => [] + | (heading, lines) => + "\n% " ^ heading ^ " (" ^ Int.toString (length lines) ^ ")\n" :: + map string_for_problem_line lines) problem + +fun is_tptp_variable s = Char.isUpper (String.sub (s, 0)) + + +(** Nice names **) + +fun empty_name_pool readable_names = + if readable_names then SOME (Symtab.empty, Symtab.empty) else NONE + +fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs +fun pool_map f xs = + pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs [] + +(* "equal" is reserved by some ATPs. "op" is also reserved, to avoid the + unreadable "op_1", "op_2", etc., in the problem files. *) +val reserved_nice_names = ["equal", "op"] +fun readable_name full_name s = + if s = full_name then + s + else + let + val s = s |> Long_Name.base_name + |> Name.desymbolize (Char.isUpper (String.sub (full_name, 0))) + in if member (op =) reserved_nice_names s then full_name else s end + +fun nice_name (full_name, _) NONE = (full_name, NONE) + | nice_name (full_name, desired_name) (SOME the_pool) = + case Symtab.lookup (fst the_pool) full_name of + SOME nice_name => (nice_name, SOME the_pool) + | NONE => + let + val nice_prefix = readable_name full_name desired_name + fun add j = + let + val nice_name = nice_prefix ^ + (if j = 0 then "" else "_" ^ Int.toString j) + in + case Symtab.lookup (snd the_pool) nice_name of + SOME full_name' => + if full_name = full_name' then (nice_name, the_pool) + else add (j + 1) + | NONE => + (nice_name, + (Symtab.update_new (full_name, nice_name) (fst the_pool), + Symtab.update_new (nice_name, full_name) (snd the_pool))) + end + in add 0 |> apsnd SOME end + + +fun nice_term (ATerm (name, ts)) = + nice_name name ##>> pool_map nice_term ts #>> ATerm +fun nice_formula (AQuant (q, xs, phi)) = + pool_map nice_name xs ##>> nice_formula phi + #>> (fn (xs, phi) => AQuant (q, xs, phi)) + | nice_formula (AConn (c, phis)) = + pool_map nice_formula phis #>> curry AConn c + | nice_formula (APred tm) = nice_term tm #>> APred +fun nice_problem_line (Fof (ident, kind, phi)) = + nice_formula phi #>> (fn phi => Fof (ident, kind, phi)) +fun nice_problem problem = + pool_map (fn (heading, lines) => + pool_map nice_problem_line lines #>> pair heading) problem +fun nice_tptp_problem readable_names problem = + nice_problem problem (empty_name_pool readable_names) + +end; diff -r 0c15b8a655cd -r dc56a9a8e19d src/HOL/Tools/ATP_Manager/atp_systems.ML --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Tue Jul 27 17:10:27 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Tue Jul 27 20:16:14 2010 +0200 @@ -7,10 +7,23 @@ signature ATP_SYSTEMS = sig - val trace : bool Unsynchronized.ref - val dest_dir : string Config.T - val problem_prefix : string Config.T - val measure_runtime : bool Config.T + datatype failure = + Unprovable | IncompleteUnprovable | CantConnect | TimedOut | + OutOfResources | OldSpass | MalformedInput | MalformedOutput | UnknownError + + type prover_config = + {home_var: string, + executable: string, + arguments: bool -> Time.time -> string, + proof_delims: (string * string) list, + known_failures: (failure * string) list, + max_new_relevant_facts_per_iter: int, + prefers_theory_relevant: bool, + explicit_forall: bool} + + val add_prover: string * prover_config -> theory -> theory + val get_prover: theory -> string -> prover_config + val available_atps: theory -> unit val refresh_systems_on_tptp : unit -> unit val default_atps_param_value : unit -> string val setup : theory -> theory @@ -19,31 +32,11 @@ structure ATP_Systems : ATP_SYSTEMS = struct -open Metis_Clauses -open Sledgehammer_Util -open Sledgehammer_Fact_Filter -open Sledgehammer_TPTP_Format -open Sledgehammer_Proof_Reconstruct -open ATP_Manager - -val trace = Unsynchronized.ref false -fun trace_msg msg = if !trace then tracing (msg ()) else () - -(** generic ATP **) +(* prover configuration *) -(* external problem files *) - -val (dest_dir, dest_dir_setup) = Attrib.config_string "atp_dest_dir" (K ""); - (*Empty string means create files in Isabelle's temporary files directory.*) - -val (problem_prefix, problem_prefix_setup) = - Attrib.config_string "atp_problem_prefix" (K "prob"); - -val (measure_runtime, measure_runtime_setup) = - Attrib.config_bool "atp_measure_runtime" (K false); - - -(* prover configuration *) +datatype failure = + Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources | + OldSpass | MalformedInput | MalformedOutput | UnknownError type prover_config = {home_var: string, @@ -56,460 +49,32 @@ explicit_forall: bool} -(* basic template *) - -val remotify = prefix "remote_" - -fun with_path cleanup after f path = - Exn.capture f path - |> tap (fn _ => cleanup path) - |> Exn.release - |> tap (after path) - -(* Splits by the first possible of a list of delimiters. *) -fun extract_proof delims output = - case pairself (find_first (fn s => String.isSubstring s output)) - (ListPair.unzip delims) of - (SOME begin_delim, SOME end_delim) => - (output |> first_field begin_delim |> the |> snd - |> first_field end_delim |> the |> fst - |> first_field "\n" |> the |> snd - handle Option.Option => "") - | _ => "" - -fun extract_proof_and_outcome complete res_code proof_delims known_failures - output = - case map_filter (fn (failure, pattern) => - if String.isSubstring pattern output then SOME failure - else NONE) known_failures of - [] => (case extract_proof proof_delims output of - "" => ("", SOME UnknownError) - | proof => if res_code = 0 then (proof, NONE) - else ("", SOME UnknownError)) - | (failure :: _) => - ("", SOME (if failure = IncompleteUnprovable andalso complete then - Unprovable - else - failure)) - -fun string_for_failure Unprovable = "The ATP problem is unprovable." - | string_for_failure IncompleteUnprovable = - "The ATP cannot prove the problem." - | string_for_failure CantConnect = "Can't connect to remote ATP." - | string_for_failure TimedOut = "Timed out." - | string_for_failure OutOfResources = "The ATP ran out of resources." - | string_for_failure OldSpass = - (* FIXME: Change the error message below to point to the Isabelle download - page once the package is there. *) - "Warning: Sledgehammer requires a more recent version of SPASS with \ - \support for the TPTP syntax. To install it, download and untar the \ - \package \"http://isabelle.in.tum.de/~blanchet/spass-3.7.tgz\" and add the \ - \\"spass-3.7\" directory's full path to \"" ^ - Path.implode (Path.expand (Path.appends - (Path.variable "ISABELLE_HOME_USER" :: - map Path.basic ["etc", "components"]))) ^ - "\" on a line of its own." - | string_for_failure MalformedInput = - "Internal Sledgehammer error: The ATP problem is malformed. Please report \ - \this to the Isabelle developers." - | string_for_failure MalformedOutput = "Error: The ATP output is malformed." - | string_for_failure UnknownError = "Error: An unknown ATP error occurred." - - -(* Clause preparation *) - -fun make_clause_table xs = - fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty - -(* Remove existing axiom clauses from the conjecture clauses, as this can - dramatically boost an ATP's performance (for some reason). *) -fun subtract_cls ax_clauses = - filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of) - -fun combformula_for_prop thy = - let - val do_term = combterm_from_term thy - fun do_quant bs q s T t' = - do_formula ((s, T) :: bs) t' - #>> (fn phi => AQuant (q, [`make_bound_var s], phi)) - and do_conn bs c t1 t2 = - do_formula bs t1 ##>> do_formula bs t2 - #>> (fn (phi1, phi2) => AConn (c, [phi1, phi2])) - and do_formula bs t = - case t of - @{const Not} $ t1 => - do_formula bs t1 #>> (fn phi => AConn (ANot, [phi])) - | Const (@{const_name All}, _) $ Abs (s, T, t') => - do_quant bs AForall s T t' - | Const (@{const_name Ex}, _) $ Abs (s, T, t') => - do_quant bs AExists s T t' - | @{const "op &"} $ t1 $ t2 => do_conn bs AAnd t1 t2 - | @{const "op |"} $ t1 $ t2 => do_conn bs AOr t1 t2 - | @{const "op -->"} $ t1 $ t2 => do_conn bs AImplies t1 t2 - | Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])) $ t1 $ t2 => - do_conn bs AIff t1 t2 - | _ => (fn ts => do_term bs (Envir.eta_contract t) - |>> APred ||> union (op =) ts) - in do_formula [] end +(* named provers *) -(* Converts an elim-rule into an equivalent theorem that does not have the - predicate variable. Leaves other theorems unchanged. We simply instantiate - the conclusion variable to False. (Cf. "transform_elim_term" in - "ATP_Systems".) *) -(* FIXME: test! *) -fun transform_elim_term t = - case Logic.strip_imp_concl t of - @{const Trueprop} $ Var (z, @{typ bool}) => - subst_Vars [(z, @{const True})] t - | Var (z, @{typ prop}) => subst_Vars [(z, @{prop True})] t - | _ => t - -(* Removes the lambdas from an equation of the form "t = (%x. u)". - (Cf. "extensionalize_theorem" in "Clausifier".) *) -fun extensionalize_term t = - let - fun aux j (Const (@{const_name "op ="}, Type (_, [Type (_, [_, T']), _])) - $ t2 $ Abs (s, var_T, t')) = - let val var_t = Var (("x", j), var_T) in - Const (@{const_name "op ="}, T' --> T' --> HOLogic.boolT) - $ betapply (t2, var_t) $ subst_bound (var_t, t') - |> aux (j + 1) - end - | aux _ t = t - in aux (maxidx_of_term t + 1) t end - -(* FIXME: Guarantee freshness *) -fun concealed_bound_name j = "Sledgehammer" ^ Int.toString j -fun conceal_bounds Ts t = - subst_bounds (map (Free o apfst concealed_bound_name) - (length Ts - 1 downto 0 ~~ rev Ts), t) -fun reveal_bounds Ts = - subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j)) - (0 upto length Ts - 1 ~~ Ts)) - -fun introduce_combinators_in_term ctxt kind t = - let - val thy = ProofContext.theory_of ctxt - fun aux Ts t = - case t of - @{const Not} $ t1 => @{const Not} $ aux Ts t1 - | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') => - t0 $ Abs (s, T, aux (T :: Ts) t') - | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') => - t0 $ Abs (s, T, aux (T :: Ts) t') - | (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 - | (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 - | (t0 as @{const "op -->"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 - | (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _]))) - $ t1 $ t2 => - t0 $ aux Ts t1 $ aux Ts t2 - | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then - t - else - let - val t = t |> conceal_bounds Ts - |> Envir.eta_contract - val ([t], ctxt') = Variable.import_terms true [t] ctxt - in - t |> cterm_of thy - |> Clausifier.introduce_combinators_in_cterm - |> singleton (Variable.export ctxt' ctxt) - |> prop_of |> Logic.dest_equals |> snd - |> reveal_bounds Ts - end - in t |> not (Meson.is_fol_term thy t) ? aux [] end - handle THM _ => - (* A type variable of sort "{}" will make abstraction fail. *) - case kind of - Axiom => HOLogic.true_const - | Conjecture => HOLogic.false_const - -(* making axiom and conjecture clauses *) -fun make_clause ctxt (formula_name, kind, t) = - let - val thy = ProofContext.theory_of ctxt - (* ### FIXME: perform other transformations previously done by - "Clausifier.to_nnf", e.g. "HOL.If" *) - val t = t |> transform_elim_term - |> Object_Logic.atomize_term thy - |> extensionalize_term - |> introduce_combinators_in_term ctxt kind - val (combformula, ctypes_sorts) = combformula_for_prop thy t [] - in - FOLFormula {formula_name = formula_name, combformula = combformula, - kind = kind, ctypes_sorts = ctypes_sorts} - end - -fun make_axiom_clause ctxt (name, th) = - (name, make_clause ctxt (name, Axiom, prop_of th)) -fun make_conjecture_clauses ctxt ts = - map2 (fn j => fn t => make_clause ctxt (Int.toString j, Conjecture, t)) - (0 upto length ts - 1) ts - -(** Helper clauses **) - -fun count_combterm (CombConst ((s, _), _, _)) = - Symtab.map_entry s (Integer.add 1) - | count_combterm (CombVar _) = I - | count_combterm (CombApp (t1, t2)) = fold count_combterm [t1, t2] -fun count_combformula (AQuant (_, _, phi)) = count_combformula phi - | count_combformula (AConn (_, phis)) = fold count_combformula phis - | count_combformula (APred tm) = count_combterm tm -fun count_fol_formula (FOLFormula {combformula, ...}) = - count_combformula combformula - -val optional_helpers = - [(["c_COMBI", "c_COMBK"], @{thms COMBI_def COMBK_def}), - (["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})] -val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal} - -val init_counters = - Symtab.make (maps (maps (map (rpair 0) o fst)) - [optional_helpers, optional_typed_helpers]) +structure Data = Theory_Data +( + type T = (prover_config * stamp) Symtab.table + val empty = Symtab.empty + val extend = I + fun merge data : T = Symtab.merge (eq_snd op =) data + handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".") +) -fun get_helper_clauses ctxt is_FO full_types conjectures axclauses = - let - val ct = fold (fold count_fol_formula) [conjectures, axclauses] - init_counters - fun is_needed c = the (Symtab.lookup ct c) > 0 - val cnfs = - (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) - in map (snd o make_axiom_clause ctxt) cnfs end - -fun s_not (@{const Not} $ t) = t - | s_not t = @{const Not} $ t - -(* prepare for passing to writer, - create additional clauses based on the information from extra_cls *) -fun prepare_clauses ctxt full_types hyp_ts concl_t axcls extra_cls = - let - val thy = ProofContext.theory_of ctxt - val goal_t = Logic.list_implies (hyp_ts, concl_t) - val is_FO = Meson.is_fol_term thy goal_t - val _ = trace_msg (fn _ => Syntax.string_of_term ctxt goal_t) - val axtms = map (prop_of o snd) extra_cls - val subs = tfree_classes_of_terms [goal_t] - val supers = tvar_classes_of_terms axtms - val tycons = type_consts_of_terms thy (goal_t :: axtms) - (* TFrees in conjecture clauses; TVars in axiom clauses *) - val conjectures = - map (s_not o HOLogic.dest_Trueprop) hyp_ts @ - [HOLogic.dest_Trueprop concl_t] - |> make_conjecture_clauses ctxt - val extra_clauses = map (snd o make_axiom_clause ctxt) extra_cls - val (clnames, axiom_clauses) = - ListPair.unzip (map (make_axiom_clause ctxt) axcls) - (* FIXME: Should it read "extra_clauses" or "axiom_clauses" in the - "get_helper_clauses" call? *) - val helper_clauses = - get_helper_clauses ctxt is_FO full_types conjectures extra_clauses - val (supers', arity_clauses) = make_arity_clauses thy tycons supers - val class_rel_clauses = make_class_rel_clauses thy subs supers' - in - (Vector.fromList clnames, - (conjectures, axiom_clauses, extra_clauses, helper_clauses, - class_rel_clauses, arity_clauses)) - end +fun add_prover (name, config) thy = + Data.map (Symtab.update_new (name, (config, stamp ()))) thy + handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".") -fun extract_clause_sequence output = - let - val tokens_of = String.tokens (not o Char.isAlphaNum) - fun extract_num ("clause" :: (ss as _ :: _)) = - Int.fromString (List.last ss) - | extract_num _ = NONE - in output |> split_lines |> map_filter (extract_num o tokens_of) end - -val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation" - -val parse_clause_formula_pair = - $$ "(" |-- scan_integer --| $$ "," -- Symbol.scan_id --| $$ ")" - --| Scan.option ($$ ",") -val parse_clause_formula_relation = - Scan.this_string set_ClauseFormulaRelationN |-- $$ "(" - |-- Scan.repeat parse_clause_formula_pair -val extract_clause_formula_relation = - Substring.full - #> Substring.position set_ClauseFormulaRelationN - #> snd #> Substring.string #> strip_spaces #> explode - #> parse_clause_formula_relation #> fst - -fun repair_conjecture_shape_and_theorem_names output conjecture_shape - thm_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 "SPASS_TPTP" script is also part - of this hack. *) - let - val j0 = hd conjecture_shape - val seq = extract_clause_sequence output - val name_map = extract_clause_formula_relation output - fun renumber_conjecture j = - AList.find (op =) name_map (conjecture_prefix ^ Int.toString (j - j0)) - |> the_single - |> (fn s => find_index (curry (op =) s) seq + 1) - in - (conjecture_shape |> map renumber_conjecture, - seq |> map (the o AList.lookup (op =) name_map) - |> map (fn s => case try (unprefix axiom_prefix) s of - SOME s' => undo_ascii_of s' - | NONE => "") - |> Vector.fromList) - end - else - (conjecture_shape, thm_names) - - -(* generic TPTP-based provers *) +fun get_prover thy name = + the (Symtab.lookup (Data.get thy) name) |> fst + handle Option.Option => error ("Unknown ATP: " ^ name ^ ".") -fun generic_tptp_prover - (name, {home_var, executable, arguments, proof_delims, known_failures, - max_new_relevant_facts_per_iter, prefers_theory_relevant, - explicit_forall}) - ({debug, overlord, full_types, explicit_apply, 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, (_, th)) = goal; - val thy = ProofContext.theory_of ctxt - (* ### FIXME: (1) preprocessing for "if" etc. *) - val (params, hyp_ts, concl_t) = strip_subgoal th subgoal - val the_filtered_clauses = - case filtered_clauses of - SOME fcls => fcls - | NONE => relevant_facts full_types relevance_threshold - relevance_convergence defs_relevant - max_new_relevant_facts_per_iter - (the_default prefers_theory_relevant theory_relevant) - relevance_override goal hyp_ts concl_t - val the_axiom_clauses = axiom_clauses |> the_default the_filtered_clauses - val (internal_thm_names, clauses) = - prepare_clauses ctxt full_types hyp_ts concl_t the_axiom_clauses - the_filtered_clauses - - (* path to unique problem file *) - val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER" - else Config.get ctxt dest_dir; - val the_problem_prefix = Config.get ctxt problem_prefix; - fun prob_pathname nr = - let - val probfile = - Path.basic ((if overlord then "prob_" ^ name - else the_problem_prefix ^ serial_string ()) - ^ "_" ^ string_of_int nr) - in - if the_dest_dir = "" then File.tmp_path probfile - else if File.exists (Path.explode the_dest_dir) - then Path.append (Path.explode the_dest_dir) probfile - else error ("No such directory: " ^ the_dest_dir ^ ".") - end; +fun available_atps thy = + priority ("Available ATPs: " ^ + commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".") - val home = getenv home_var - val command = Path.explode (home ^ "/" ^ executable) - (* write out problem file and call prover *) - fun command_line complete probfile = - let - val core = File.shell_path command ^ " " ^ arguments complete timeout ^ - " " ^ File.shell_path probfile - in - (if Config.get ctxt measure_runtime then - "TIMEFORMAT='%3U'; { time " ^ core ^ " ; }" - else - "exec " ^ core) ^ " 2>&1" - end - fun split_time s = - let - val split = String.tokens (fn c => str c = "\n"); - val (output, t) = s |> split |> split_last |> apfst cat_lines; - fun as_num f = f >> (fst o read_int); - val num = as_num (Scan.many1 Symbol.is_ascii_digit); - val digit = Scan.one Symbol.is_ascii_digit; - val num3 = as_num (digit ::: digit ::: (digit >> single)); - val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b); - val as_time = the_default 0 o Scan.read Symbol.stopper time o explode; - in (output, as_time t) end; - fun run_on probfile = - if home = "" then - error ("The environment variable " ^ quote home_var ^ " is not set.") - else if File.exists command then - let - fun do_run complete = - let - val command = command_line complete probfile - val ((output, msecs), res_code) = - bash_output command - |>> (if overlord then - prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") - else - I) - |>> (if Config.get ctxt measure_runtime then split_time - else rpair 0) - val (proof, outcome) = - extract_proof_and_outcome complete res_code proof_delims - known_failures output - in (output, msecs, proof, outcome) end - val readable_names = debug andalso overlord - val (pool, conjecture_offset) = - write_tptp_file thy readable_names explicit_forall full_types - explicit_apply probfile clauses - val conjecture_shape = - conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1 - val result = - do_run false - |> (fn (_, msecs0, _, SOME _) => - do_run true - |> (fn (output, msecs, proof, outcome) => - (output, msecs0 + msecs, proof, outcome)) - | result => result) - in ((pool, conjecture_shape), result) end - else - error ("Bad executable: " ^ Path.implode command ^ "."); - - (* If the problem file has not been exported, remove it; otherwise, export - the proof file too. *) - fun cleanup probfile = - if the_dest_dir = "" then try File.rm probfile else NONE - fun export probfile (_, (output, _, _, _)) = - if the_dest_dir = "" then - () - else - File.write (Path.explode (Path.implode probfile ^ "_proof")) output - - val ((pool, conjecture_shape), (output, msecs, proof, outcome)) = - with_path cleanup export run_on (prob_pathname subgoal) - val (conjecture_shape, internal_thm_names) = - repair_conjecture_shape_and_theorem_names output conjecture_shape - internal_thm_names - - val (message, relevant_thm_names) = - case outcome of - NONE => - proof_text isar_proof - (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) - (full_types, minimize_command, proof, internal_thm_names, th, - subgoal) - | SOME failure => (string_for_failure failure ^ "\n", []) - in - {outcome = outcome, message = message, pool = pool, - relevant_thm_names = relevant_thm_names, atp_run_time_in_msecs = msecs, - output = output, proof = proof, internal_thm_names = internal_thm_names, - conjecture_shape = conjecture_shape, - filtered_clauses = the_filtered_clauses} - end - -fun tptp_prover name p = (name, generic_tptp_prover (name, p)); +fun available_atps thy = + priority ("Available ATPs: " ^ + commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".") fun to_generous_secs time = (Time.toMilliseconds time + 999) div 1000 @@ -537,7 +102,7 @@ max_new_relevant_facts_per_iter = 80 (* FIXME *), prefers_theory_relevant = false, explicit_forall = false} -val e = tptp_prover "e" e_config +val e = ("e", e_config) (* The "-VarWeight=3" option helps the higher-order problems, probably by @@ -562,7 +127,7 @@ max_new_relevant_facts_per_iter = 26 (* FIXME *), prefers_theory_relevant = true, explicit_forall = true} -val spass = tptp_prover "spass" spass_config +val spass = ("spass", spass_config) (* Vampire *) @@ -584,11 +149,11 @@ max_new_relevant_facts_per_iter = 40 (* FIXME *), prefers_theory_relevant = false, explicit_forall = false} -val vampire = tptp_prover "vampire" vampire_config +val vampire = ("vampire", vampire_config) (* Remote prover invocation via SystemOnTPTP *) -val systems = Synchronized.var "atp_systems" ([]: string list); +val systems = Synchronized.var "atp_systems" ([]: string list) fun get_systems () = case bash_output "\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w" of @@ -629,27 +194,23 @@ prefers_theory_relevant = prefers_theory_relevant, explicit_forall = explicit_forall} -fun remote_tptp_prover prover atp_prefix args config = - tptp_prover (remotify (fst prover)) (remote_config atp_prefix args config) +val remote_name = prefix "remote_" -val remote_e = remote_tptp_prover e "EP---" "" e_config -val remote_spass = remote_tptp_prover spass "SPASS---" "-x" spass_config -val remote_vampire = remote_tptp_prover vampire "Vampire---9" "" vampire_config +fun remote_prover prover atp_prefix args config = + (remote_name (fst prover), remote_config atp_prefix args config) + +val remote_e = remote_prover e "EP---" "" e_config +val remote_spass = remote_prover spass "SPASS---" "-x" spass_config +val remote_vampire = remote_prover vampire "Vampire---9" "" vampire_config fun maybe_remote (name, _) ({home_var, ...} : prover_config) = - name |> getenv home_var = "" ? remotify + name |> getenv home_var = "" ? remote_name fun default_atps_param_value () = space_implode " " [maybe_remote e e_config, maybe_remote spass spass_config, - remotify (fst vampire)] + remote_name (fst vampire)] val provers = [e, spass, vampire, remote_e, remote_spass, remote_vampire] -val prover_setup = fold add_prover provers - -val setup = - dest_dir_setup - #> problem_prefix_setup - #> measure_runtime_setup - #> prover_setup +val setup = fold add_prover provers end; diff -r 0c15b8a655cd -r dc56a9a8e19d src/HOL/Tools/Nitpick/kodkod.ML --- a/src/HOL/Tools/Nitpick/kodkod.ML Tue Jul 27 17:10:27 2010 +0200 +++ b/src/HOL/Tools/Nitpick/kodkod.ML Tue Jul 27 20:16:14 2010 +0200 @@ -847,7 +847,7 @@ out "solve "; out_outmost_f formula; out ";\n") in out ("// This file was generated by Isabelle (most likely Nitpick)\n" ^ - "// " ^ Sledgehammer_Util.timestamp () ^ "\n"); + "// " ^ ATP_Problem.timestamp () ^ "\n"); map out_problem problems end diff -r 0c15b8a655cd -r dc56a9a8e19d src/HOL/Tools/Nitpick/nitpick_util.ML --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Tue Jul 27 17:10:27 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Tue Jul 27 20:16:14 2010 +0200 @@ -49,7 +49,6 @@ val plural_s : int -> string val plural_s_for_list : 'a list -> string val serial_commas : string -> string list -> string list - val timestamp : unit -> string val parse_bool_option : bool -> string -> string -> bool option val parse_time_option : string -> string -> Time.time option val flip_polarity : polarity -> polarity @@ -223,7 +222,6 @@ val serial_commas = Sledgehammer_Util.serial_commas -val timestamp = Sledgehammer_Util.timestamp val parse_bool_option = Sledgehammer_Util.parse_bool_option val parse_time_option = Sledgehammer_Util.parse_time_option diff -r 0c15b8a655cd -r dc56a9a8e19d src/HOL/Tools/Sledgehammer/clausifier.ML --- a/src/HOL/Tools/Sledgehammer/clausifier.ML Tue Jul 27 17:10:27 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Tue Jul 27 20:16:14 2010 +0200 @@ -1,5 +1,5 @@ (* Title: HOL/Tools/Sledgehammer/clausifier.ML - Author: Jia Meng, Cambridge University Computer Laboratory + Author: Jia Meng, Cambridge University Computer Laboratory and NICTA Author: Jasmin Blanchette, TU Muenchen Transformation of axiom rules (elim/intro/etc) into CNF forms. @@ -8,10 +8,8 @@ signature CLAUSIFIER = sig val introduce_combinators_in_cterm : cterm -> thm - val cnf_axiom: theory -> bool -> thm -> thm list - val cnf_rules_pairs : - theory -> bool -> (string * thm) list -> ((string * int) * thm) list - val neg_clausify: thm -> thm list + val introduce_combinators_in_theorem : thm -> thm + val cnf_axiom: theory -> thm -> thm list end; structure Clausifier : CLAUSIFIER = @@ -198,7 +196,7 @@ (* Given the definition of a Skolem function, return a theorem to replace an existential formula by a use of that function. Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *) -fun skolem_theorem_of_def thy cheat rhs0 = +fun skolem_theorem_of_def thy rhs0 = let val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> Thm.cterm_of thy val rhs' = rhs |> Thm.dest_comb |> snd @@ -214,12 +212,8 @@ Drule.list_comb (rhs, frees) |> Drule.beta_conv cabs |> Thm.capply cTrueprop fun tacf [prem] = - if cheat then - Skip_Proof.cheat_tac thy - else - rewrite_goals_tac skolem_id_def_raw - THEN rtac ((prem |> rewrite_rule skolem_id_def_raw) - RS @{thm someI_ex}) 1 + rewrite_goals_tac skolem_id_def_raw + THEN rtac ((prem |> rewrite_rule skolem_id_def_raw) RS @{thm someI_ex}) 1 in Goal.prove_internal [ex_tm] conc tacf |> forall_intr_list frees @@ -238,11 +232,11 @@ in (th3, ctxt) end; (* Skolemize a named theorem, with Skolem functions as additional premises. *) -fun skolemize_theorem thy cheat th = +fun skolemize_theorem thy th = let val ctxt0 = Variable.global_thm_context th val (nnfth, ctxt) = to_nnf th ctxt0 - val sko_ths = map (skolem_theorem_of_def thy cheat) + val sko_ths = map (skolem_theorem_of_def thy) (assume_skolem_funs nnfth) val (cnfs, ctxt) = Meson.make_cnf sko_ths nnfth ctxt in @@ -255,36 +249,6 @@ (* Convert Isabelle theorems into axiom clauses. *) (* FIXME: is transfer necessary? *) -fun cnf_axiom thy cheat = skolemize_theorem thy cheat o Thm.transfer thy - - -(**** Translate a set of theorems into CNF ****) - -(*The combination of rev and tail recursion preserves the original order*) -(* ### FIXME: kill "cheat" *) -fun cnf_rules_pairs thy cheat = - let - fun do_one _ [] = [] - | do_one ((name, k), th) (cls :: clss) = - ((name, k), cls) :: do_one ((name, k + 1), th) clss - fun do_all pairs [] = pairs - | do_all pairs ((name, th) :: ths) = - let - val new_pairs = do_one ((name, 0), th) (cnf_axiom thy cheat th) - handle THM _ => [] - in do_all (new_pairs @ pairs) ths end - in do_all [] o rev end - - -(*** Converting a subgoal into negated conjecture clauses. ***) - -fun neg_skolemize_tac ctxt = - EVERY' [rtac ccontr, Object_Logic.atomize_prems_tac, Meson.skolemize_tac ctxt] - -val neg_clausify = - single - #> Meson.make_clauses_unsorted - #> map introduce_combinators_in_theorem - #> Meson.finish_cnf +fun cnf_axiom thy = skolemize_theorem thy o Thm.transfer thy end; diff -r 0c15b8a655cd -r dc56a9a8e19d src/HOL/Tools/Sledgehammer/meson_tactic.ML --- a/src/HOL/Tools/Sledgehammer/meson_tactic.ML Tue Jul 27 17:10:27 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/meson_tactic.ML Tue Jul 27 20:16:14 2010 +0200 @@ -1,5 +1,5 @@ (* Title: HOL/Tools/Sledgehammer/meson_tactic.ML - Author: Jia Meng, Cambridge University Computer Laboratory + Author: Jia Meng, Cambridge University Computer Laboratory and NICTA Author: Jasmin Blanchette, TU Muenchen MESON general tactic and proof method. @@ -18,7 +18,7 @@ let val thy = ProofContext.theory_of ctxt val ctxt0 = Classical.put_claset HOL_cs ctxt - in Meson.meson_tac ctxt0 (maps (Clausifier.cnf_axiom thy false) ths) end + in Meson.meson_tac ctxt0 (maps (Clausifier.cnf_axiom thy) ths) end val setup = Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt => diff -r 0c15b8a655cd -r dc56a9a8e19d src/HOL/Tools/Sledgehammer/metis_clauses.ML --- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML Tue Jul 27 17:10:27 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Tue Jul 27 20:16:14 2010 +0200 @@ -1,5 +1,5 @@ (* Title: HOL/Tools/Sledgehammer/metis_clauses.ML - Author: Jia Meng, Cambridge University Computer Laboratory + Author: Jia Meng, Cambridge University Computer Laboratory and NICTA Author: Jasmin Blanchette, TU Muenchen Storing/printing FOL clauses and arity clauses. Typed equality is @@ -9,17 +9,16 @@ signature METIS_CLAUSES = sig type name = string * string - datatype kind = Axiom | Conjecture datatype type_literal = TyLitVar of name * name | TyLitFree of name * name datatype arLit = TConsLit of name * name * name list | TVarLit of name * name - datatype arity_clause = ArityClause of - {axiom_name: string, conclLit: arLit, premLits: arLit list} - datatype class_rel_clause = ClassRelClause of - {axiom_name: string, subclass: name, superclass: name} + datatype arity_clause = + ArityClause of {axiom_name: string, conclLit: arLit, premLits: arLit list} + datatype class_rel_clause = + ClassRelClause of {axiom_name: string, subclass: name, superclass: name} datatype combtyp = CombTVar of name | CombTFree of name | @@ -29,9 +28,6 @@ CombVar of name * combtyp | CombApp of combterm * combterm datatype fol_literal = FOLLiteral of bool * combterm - datatype fol_clause = - FOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind, - literals: fol_literal list, ctypes_sorts: typ list} val type_wrapper_name : string val bound_var_prefix : string @@ -228,8 +224,6 @@ type name = string * string -datatype kind = Axiom | Conjecture - (**** Isabelle FOL clauses ****) (* The first component is the type class; the second is a TVar or TFree. *) @@ -367,10 +361,6 @@ datatype fol_literal = FOLLiteral of bool * combterm -datatype fol_clause = - FOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind, - literals: fol_literal list, ctypes_sorts: typ list} - (*********************************************************************) (* convert a clause with type Term.term to a clause with type clause *) (*********************************************************************) diff -r 0c15b8a655cd -r dc56a9a8e19d src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Tue Jul 27 17:10:27 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Tue Jul 27 20:16:14 2010 +0200 @@ -1,5 +1,7 @@ (* Title: HOL/Tools/Sledgehammer/metis_tactics.ML - Author: Kong W. Susanto and Lawrence C. Paulson, CU Computer Laboratory + Author: Kong W. Susanto, Cambridge University Computer Laboratory + Author: Lawrence C. Paulson, Cambridge University Computer Laboratory + Author: Jasmin Blanchette, TU Muenchen Copyright Cambridge University 2007 HOL setup for the Metis prover. @@ -599,7 +601,7 @@ (* ------------------------------------------------------------------------- *) fun cnf_helper_theorem thy raw th = - if raw then th else the_single (Clausifier.cnf_axiom thy false th) + if raw then th else the_single (Clausifier.cnf_axiom thy th) fun type_ext thy tms = let val subs = tfree_classes_of_terms tms @@ -715,7 +717,7 @@ fun FOL_SOLVE mode ctxt cls ths0 = let val thy = ProofContext.theory_of ctxt val th_cls_pairs = - map (fn th => (Thm.get_name_hint th, Clausifier.cnf_axiom thy false th)) ths0 + map (fn th => (Thm.get_name_hint th, Clausifier.cnf_axiom thy th)) ths0 val ths = maps #2 th_cls_pairs val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES") val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls @@ -773,6 +775,12 @@ val type_has_top_sort = exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false) +val neg_clausify = + single + #> Meson.make_clauses_unsorted + #> map Clausifier.introduce_combinators_in_theorem + #> Meson.finish_cnf + fun generic_metis_tac mode ctxt ths i st0 = let val _ = trace_msg (fn () => @@ -781,7 +789,7 @@ if exists_type type_has_top_sort (prop_of st0) then (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty) else - Meson.MESON (maps Clausifier.neg_clausify) + 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) diff -r 0c15b8a655cd -r dc56a9a8e19d src/HOL/Tools/Sledgehammer/sledgehammer.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Jul 27 20:16:14 2010 +0200 @@ -0,0 +1,882 @@ +(* Title: HOL/Tools/Sledgehammer/sledgehammer.ML + Author: Fabian Immler, TU Muenchen + Author: Makarius + Author: Jasmin Blanchette, TU Muenchen + +Sledgehammer's heart. +*) + +signature SLEDGEHAMMER = +sig + type failure = ATP_Systems.failure + type relevance_override = Sledgehammer_Fact_Filter.relevance_override + type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command + type params = + {debug: bool, + verbose: bool, + overlord: bool, + atps: string list, + full_types: bool, + explicit_apply: bool, + relevance_threshold: real, + relevance_convergence: real, + theory_relevant: bool option, + defs_relevant: bool, + isar_proof: bool, + isar_shrink_factor: int, + timeout: Time.time, + minimize_timeout: Time.time} + type problem = + {subgoal: int, + goal: Proof.context * (thm list * thm), + relevance_override: relevance_override, + axiom_clauses: (string * thm) list option, + filtered_clauses: (string * thm) list option} + type prover_result = + {outcome: failure option, + message: string, + pool: string Symtab.table, + used_thm_names: string list, + atp_run_time_in_msecs: int, + output: string, + proof: string, + internal_thm_names: string Vector.vector, + conjecture_shape: int list, + filtered_clauses: (string * thm) list} + type prover = + params -> minimize_command -> Time.time -> problem -> prover_result + + val dest_dir : string Config.T + val problem_prefix : string Config.T + val measure_runtime : bool Config.T + val kill_atps: unit -> unit + val running_atps: unit -> unit + val messages: int option -> unit + val get_prover_fun : theory -> string -> prover + val start_prover_thread : + params -> int -> int -> relevance_override -> (string -> minimize_command) + -> Proof.state -> string -> unit + val setup : theory -> theory +end; + +structure Sledgehammer : SLEDGEHAMMER = +struct + +open ATP_Problem +open ATP_Systems +open Metis_Clauses +open Sledgehammer_Util +open Sledgehammer_Fact_Filter +open Sledgehammer_Proof_Reconstruct + + +(** The Sledgehammer **) + +val das_Tool = "Sledgehammer" + +fun kill_atps () = Async_Manager.kill_threads das_Tool "ATPs" +fun running_atps () = Async_Manager.running_threads das_Tool "ATPs" +val messages = Async_Manager.thread_messages das_Tool "ATP" + +(** problems, results, provers, etc. **) + +type params = + {debug: bool, + verbose: bool, + overlord: bool, + atps: string list, + full_types: bool, + explicit_apply: bool, + relevance_threshold: real, + relevance_convergence: real, + theory_relevant: bool option, + defs_relevant: bool, + isar_proof: bool, + isar_shrink_factor: int, + timeout: Time.time, + minimize_timeout: Time.time} + +type problem = + {subgoal: int, + goal: Proof.context * (thm list * thm), + relevance_override: relevance_override, + axiom_clauses: (string * thm) list option, + filtered_clauses: (string * thm) list option} + +type prover_result = + {outcome: failure option, + message: string, + pool: string Symtab.table, + used_thm_names: string list, + atp_run_time_in_msecs: int, + output: string, + proof: string, + internal_thm_names: string Vector.vector, + conjecture_shape: int list, + filtered_clauses: (string * thm) list} + +type prover = + params -> minimize_command -> Time.time -> problem -> prover_result + +(* configuration attributes *) + +val (dest_dir, dest_dir_setup) = Attrib.config_string "atp_dest_dir" (K ""); + (*Empty string means create files in Isabelle's temporary files directory.*) + +val (problem_prefix, problem_prefix_setup) = + Attrib.config_string "atp_problem_prefix" (K "prob"); + +val (measure_runtime, measure_runtime_setup) = + Attrib.config_bool "atp_measure_runtime" (K false); + +fun with_path cleanup after f path = + Exn.capture f path + |> tap (fn _ => cleanup path) + |> Exn.release + |> tap (after path) + +(* Splits by the first possible of a list of delimiters. *) +fun extract_proof delims output = + case pairself (find_first (fn s => String.isSubstring s output)) + (ListPair.unzip delims) of + (SOME begin_delim, SOME end_delim) => + (output |> first_field begin_delim |> the |> snd + |> first_field end_delim |> the |> fst + |> first_field "\n" |> the |> snd + handle Option.Option => "") + | _ => "" + +fun extract_proof_and_outcome complete res_code proof_delims known_failures + output = + case map_filter (fn (failure, pattern) => + if String.isSubstring pattern output then SOME failure + else NONE) known_failures of + [] => (case extract_proof proof_delims output of + "" => ("", SOME UnknownError) + | proof => if res_code = 0 then (proof, NONE) + else ("", SOME UnknownError)) + | (failure :: _) => + ("", SOME (if failure = IncompleteUnprovable andalso complete then + Unprovable + else + failure)) + +fun string_for_failure Unprovable = "The ATP problem is unprovable." + | string_for_failure IncompleteUnprovable = + "The ATP cannot prove the problem." + | string_for_failure CantConnect = "Can't connect to remote ATP." + | string_for_failure TimedOut = "Timed out." + | string_for_failure OutOfResources = "The ATP ran out of resources." + | string_for_failure OldSpass = + (* FIXME: Change the error message below to point to the Isabelle download + page once the package is there. *) + "Warning: Sledgehammer requires a more recent version of SPASS with \ + \support for the TPTP syntax. To install it, download and untar the \ + \package \"http://isabelle.in.tum.de/~blanchet/spass-3.7.tgz\" and add the \ + \\"spass-3.7\" directory's full path to \"" ^ + Path.implode (Path.expand (Path.appends + (Path.variable "ISABELLE_HOME_USER" :: + map Path.basic ["etc", "components"]))) ^ + "\" on a line of its own." + | string_for_failure MalformedInput = + "Internal Sledgehammer error: The ATP problem is malformed. Please report \ + \this to the Isabelle developers." + | string_for_failure MalformedOutput = "Error: The ATP output is malformed." + | string_for_failure UnknownError = "Error: An unknown ATP error occurred." + + +(* Clause preparation *) + +datatype fol_formula = + FOLFormula of {formula_name: string, + kind: kind, + combformula: (name, combterm) formula, + ctypes_sorts: typ list} + +fun mk_anot phi = AConn (ANot, [phi]) +fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2]) +fun mk_ahorn [] phi = phi + | mk_ahorn (phi :: phis) psi = + AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi]) + +(* ### FIXME: reintroduce +fun make_clause_table xs = + fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty +(* Remove existing axiom clauses from the conjecture clauses, as this can + dramatically boost an ATP's performance (for some reason). *) +fun subtract_cls ax_clauses = + filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of) +*) + +fun combformula_for_prop thy = + let + val do_term = combterm_from_term thy + fun do_quant bs q s T t' = + do_formula ((s, T) :: bs) t' + #>> (fn phi => AQuant (q, [`make_bound_var s], phi)) + and do_conn bs c t1 t2 = + do_formula bs t1 ##>> do_formula bs t2 + #>> (fn (phi1, phi2) => AConn (c, [phi1, phi2])) + and do_formula bs t = + case t of + @{const Not} $ t1 => + do_formula bs t1 #>> (fn phi => AConn (ANot, [phi])) + | Const (@{const_name All}, _) $ Abs (s, T, t') => + do_quant bs AForall s T t' + | Const (@{const_name Ex}, _) $ Abs (s, T, t') => + do_quant bs AExists s T t' + | @{const "op &"} $ t1 $ t2 => do_conn bs AAnd t1 t2 + | @{const "op |"} $ t1 $ t2 => do_conn bs AOr t1 t2 + | @{const "op -->"} $ t1 $ t2 => do_conn bs AImplies t1 t2 + | Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])) $ t1 $ t2 => + do_conn bs AIff t1 t2 + | _ => (fn ts => do_term bs (Envir.eta_contract t) + |>> APred ||> union (op =) ts) + in do_formula [] end + +(* Converts an elim-rule into an equivalent theorem that does not have the + predicate variable. Leaves other theorems unchanged. We simply instantiate + the conclusion variable to False. (Cf. "transform_elim_term" in + "ATP_Systems".) *) +(* FIXME: test! *) +fun transform_elim_term t = + case Logic.strip_imp_concl t of + @{const Trueprop} $ Var (z, @{typ bool}) => + subst_Vars [(z, @{const True})] t + | Var (z, @{typ prop}) => subst_Vars [(z, @{prop True})] t + | _ => t + +(* Removes the lambdas from an equation of the form "t = (%x. u)". + (Cf. "extensionalize_theorem" in "Clausifier".) *) +fun extensionalize_term t = + let + fun aux j (Const (@{const_name "op ="}, Type (_, [Type (_, [_, T']), _])) + $ t2 $ Abs (s, var_T, t')) = + let val var_t = Var (("x", j), var_T) in + Const (@{const_name "op ="}, T' --> T' --> HOLogic.boolT) + $ betapply (t2, var_t) $ subst_bound (var_t, t') + |> aux (j + 1) + end + | aux _ t = t + in aux (maxidx_of_term t + 1) t end + +(* FIXME: Guarantee freshness *) +fun concealed_bound_name j = "Sledgehammer" ^ Int.toString j +fun conceal_bounds Ts t = + subst_bounds (map (Free o apfst concealed_bound_name) + (length Ts - 1 downto 0 ~~ rev Ts), t) +fun reveal_bounds Ts = + subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j)) + (0 upto length Ts - 1 ~~ Ts)) + +fun introduce_combinators_in_term ctxt kind t = + let + val thy = ProofContext.theory_of ctxt + fun aux Ts t = + case t of + @{const Not} $ t1 => @{const Not} $ aux Ts t1 + | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') => + t0 $ Abs (s, T, aux (T :: Ts) t') + | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') => + t0 $ Abs (s, T, aux (T :: Ts) t') + | (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 + | (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 + | (t0 as @{const "op -->"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 + | (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _]))) + $ t1 $ t2 => + t0 $ aux Ts t1 $ aux Ts t2 + | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then + t + else + let + val t = t |> conceal_bounds Ts + |> Envir.eta_contract + val ([t], ctxt') = Variable.import_terms true [t] ctxt + in + t |> cterm_of thy + |> Clausifier.introduce_combinators_in_cterm + |> singleton (Variable.export ctxt' ctxt) + |> prop_of |> Logic.dest_equals |> snd + |> reveal_bounds Ts + end + in t |> not (Meson.is_fol_term thy t) ? aux [] end + handle THM _ => + (* A type variable of sort "{}" will make abstraction fail. *) + case kind of + Axiom => HOLogic.true_const + | Conjecture => HOLogic.false_const + +(* making axiom and conjecture clauses *) +fun make_clause ctxt (formula_name, kind, t) = + let + val thy = ProofContext.theory_of ctxt + (* ### FIXME: perform other transformations previously done by + "Clausifier.to_nnf", e.g. "HOL.If" *) + val t = t |> transform_elim_term + |> Object_Logic.atomize_term thy + |> extensionalize_term + |> introduce_combinators_in_term ctxt kind + val (combformula, ctypes_sorts) = combformula_for_prop thy t [] + in + FOLFormula {formula_name = formula_name, combformula = combformula, + kind = kind, ctypes_sorts = ctypes_sorts} + end + +fun make_axiom_clause ctxt (name, th) = + (name, make_clause ctxt (name, Axiom, prop_of th)) +fun make_conjecture_clauses ctxt ts = + map2 (fn j => fn t => make_clause ctxt (Int.toString j, Conjecture, t)) + (0 upto length ts - 1) ts + +(** Helper clauses **) + +fun count_combterm (CombConst ((s, _), _, _)) = + Symtab.map_entry s (Integer.add 1) + | count_combterm (CombVar _) = I + | count_combterm (CombApp (t1, t2)) = fold count_combterm [t1, t2] +fun count_combformula (AQuant (_, _, phi)) = count_combformula phi + | count_combformula (AConn (_, phis)) = fold count_combformula phis + | count_combformula (APred tm) = count_combterm tm +fun count_fol_formula (FOLFormula {combformula, ...}) = + count_combformula combformula + +val optional_helpers = + [(["c_COMBI", "c_COMBK"], @{thms COMBI_def COMBK_def}), + (["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})] +val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal} + +val init_counters = + Symtab.make (maps (maps (map (rpair 0) o fst)) + [optional_helpers, optional_typed_helpers]) + +fun get_helper_clauses ctxt is_FO full_types conjectures axclauses = + let + val ct = fold (fold count_fol_formula) [conjectures, axclauses] + init_counters + fun is_needed c = the (Symtab.lookup ct c) > 0 + val cnfs = + (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) + in map (snd o make_axiom_clause ctxt) cnfs end + +fun s_not (@{const Not} $ t) = t + | s_not t = @{const Not} $ t + +(* prepare for passing to writer, + create additional clauses based on the information from extra_cls *) +fun prepare_clauses ctxt full_types hyp_ts concl_t axcls extra_cls = + let + val thy = ProofContext.theory_of ctxt + val goal_t = Logic.list_implies (hyp_ts, concl_t) + val is_FO = Meson.is_fol_term thy goal_t + val axtms = map (prop_of o snd) extra_cls + val subs = tfree_classes_of_terms [goal_t] + val supers = tvar_classes_of_terms axtms + val tycons = type_consts_of_terms thy (goal_t :: axtms) + (* TFrees in conjecture clauses; TVars in axiom clauses *) + val conjectures = + map (s_not o HOLogic.dest_Trueprop) hyp_ts @ + [HOLogic.dest_Trueprop concl_t] + |> make_conjecture_clauses ctxt + val extra_clauses = map (snd o make_axiom_clause ctxt) extra_cls + val (clnames, axiom_clauses) = + ListPair.unzip (map (make_axiom_clause ctxt) axcls) + (* FIXME: Should it read "extra_clauses" or "axiom_clauses" in the + "get_helper_clauses" call? *) + val helper_clauses = + get_helper_clauses ctxt is_FO full_types conjectures extra_clauses + val (supers', arity_clauses) = make_arity_clauses thy tycons supers + val class_rel_clauses = make_class_rel_clauses thy subs supers' + in + (Vector.fromList clnames, + (conjectures, axiom_clauses, extra_clauses, helper_clauses, + class_rel_clauses, arity_clauses)) + end + +val axiom_prefix = "ax_" +val conjecture_prefix = "conj_" +val arity_clause_prefix = "clsarity_" +val tfrees_name = "tfrees" + +fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t]) + +fun fo_term_for_combtyp (CombTVar name) = ATerm (name, []) + | fo_term_for_combtyp (CombTFree name) = ATerm (name, []) + | fo_term_for_combtyp (CombType (name, tys)) = + ATerm (name, map fo_term_for_combtyp tys) + +fun fo_literal_for_type_literal (TyLitVar (class, name)) = + (true, ATerm (class, [ATerm (name, [])])) + | fo_literal_for_type_literal (TyLitFree (class, name)) = + (true, ATerm (class, [ATerm (name, [])])) + +fun formula_for_fo_literal (pos, t) = APred t |> not pos ? mk_anot + +fun fo_term_for_combterm full_types = + let + fun aux top_level u = + let + val (head, args) = strip_combterm_comb u + val (x, ty_args) = + case head of + CombConst (name, _, ty_args) => + if fst name = "equal" then + (if top_level andalso length args = 2 then name + else ("c_fequal", @{const_name fequal}), []) + else + (name, if full_types then [] else ty_args) + | CombVar (name, _) => (name, []) + | CombApp _ => raise Fail "impossible \"CombApp\"" + val t = ATerm (x, map fo_term_for_combtyp ty_args @ + map (aux false) args) + in + if full_types then wrap_type (fo_term_for_combtyp (combtyp_of u)) t else t + end + in aux true end + +fun formula_for_combformula full_types = + let + fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi) + | aux (AConn (c, phis)) = AConn (c, map aux phis) + | aux (APred tm) = APred (fo_term_for_combterm full_types tm) + in aux end + +fun formula_for_axiom full_types (FOLFormula {combformula, ctypes_sorts, ...}) = + mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal) + (type_literals_for_types ctypes_sorts)) + (formula_for_combformula full_types combformula) + +fun problem_line_for_axiom full_types + (formula as FOLFormula {formula_name, kind, ...}) = + Fof (axiom_prefix ^ ascii_of formula_name, kind, + formula_for_axiom full_types formula) + +fun problem_line_for_class_rel_clause + (ClassRelClause {axiom_name, subclass, superclass, ...}) = + let val ty_arg = ATerm (("T", "T"), []) in + Fof (ascii_of axiom_name, Axiom, + AConn (AImplies, [APred (ATerm (subclass, [ty_arg])), + APred (ATerm (superclass, [ty_arg]))])) + end + +fun fo_literal_for_arity_literal (TConsLit (c, t, args)) = + (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)])) + | fo_literal_for_arity_literal (TVarLit (c, sort)) = + (false, ATerm (c, [ATerm (sort, [])])) + +fun problem_line_for_arity_clause + (ArityClause {axiom_name, conclLit, premLits, ...}) = + Fof (arity_clause_prefix ^ ascii_of axiom_name, Axiom, + mk_ahorn (map (formula_for_fo_literal o apfst not + o fo_literal_for_arity_literal) premLits) + (formula_for_fo_literal + (fo_literal_for_arity_literal conclLit))) + +fun problem_line_for_conjecture full_types + (FOLFormula {formula_name, kind, combformula, ...}) = + Fof (conjecture_prefix ^ formula_name, kind, + formula_for_combformula full_types combformula) + +fun free_type_literals_for_conjecture (FOLFormula {ctypes_sorts, ...}) = + map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts) + +fun problem_line_for_free_type lit = + Fof (tfrees_name, Conjecture, mk_anot (formula_for_fo_literal lit)) +fun problem_lines_for_free_types conjectures = + let + val litss = map free_type_literals_for_conjecture conjectures + val lits = fold (union (op =)) litss [] + in map problem_line_for_free_type lits end + +(** "hBOOL" and "hAPP" **) + +type const_info = {min_arity: int, max_arity: int, sub_level: bool} + +fun consider_term top_level (ATerm ((s, _), ts)) = + (if is_tptp_variable s then + I + else + let val n = length ts in + Symtab.map_default + (s, {min_arity = n, max_arity = 0, sub_level = false}) + (fn {min_arity, max_arity, sub_level} => + {min_arity = Int.min (n, min_arity), + max_arity = Int.max (n, max_arity), + sub_level = sub_level orelse not top_level}) + end) + #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts +fun consider_formula (AQuant (_, _, phi)) = consider_formula phi + | consider_formula (AConn (_, phis)) = fold consider_formula phis + | consider_formula (APred tm) = consider_term true tm + +fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi +fun consider_problem problem = fold (fold consider_problem_line o snd) problem + +fun const_table_for_problem explicit_apply problem = + if explicit_apply then NONE + else SOME (Symtab.empty |> consider_problem problem) + +val tc_fun = make_fixed_type_const @{type_name fun} + +fun min_arity_of thy full_types NONE s = + (if s = "equal" orelse s = type_wrapper_name orelse + String.isPrefix type_const_prefix s orelse + String.isPrefix class_prefix s then + 16383 (* large number *) + else if full_types then + 0 + else case strip_prefix_and_undo_ascii const_prefix s of + SOME s' => num_type_args thy (invert_const s') + | NONE => 0) + | min_arity_of _ _ (SOME the_const_tab) s = + case Symtab.lookup the_const_tab s of + SOME ({min_arity, ...} : const_info) => min_arity + | NONE => 0 + +fun full_type_of (ATerm ((s, _), [ty, _])) = + if s = type_wrapper_name then ty else raise Fail "expected type wrapper" + | full_type_of _ = raise Fail "expected type wrapper" + +fun list_hAPP_rev _ t1 [] = t1 + | list_hAPP_rev NONE t1 (t2 :: ts2) = + ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2]) + | list_hAPP_rev (SOME ty) t1 (t2 :: ts2) = + let val ty' = ATerm (`make_fixed_type_const @{type_name fun}, + [full_type_of t2, ty]) in + ATerm (`I "hAPP", [wrap_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2]) + end + +fun repair_applications_in_term thy full_types const_tab = + let + fun aux opt_ty (ATerm (name as (s, _), ts)) = + if s = type_wrapper_name then + case ts of + [t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2]) + | _ => raise Fail "malformed type wrapper" + else + let + val ts = map (aux NONE) ts + val (ts1, ts2) = chop (min_arity_of thy full_types const_tab s) ts + in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end + in aux NONE end + +fun boolify t = ATerm (`I "hBOOL", [t]) + +(* True if the constant ever appears outside of the top-level position in + literals, or if it appears with different arities (e.g., because of different + type instantiations). If false, the constant always receives all of its + arguments and is used as a predicate. *) +fun is_predicate NONE s = + s = "equal" orelse String.isPrefix type_const_prefix s orelse + String.isPrefix class_prefix s + | is_predicate (SOME the_const_tab) s = + case Symtab.lookup the_const_tab s of + SOME {min_arity, max_arity, sub_level} => + not sub_level andalso min_arity = max_arity + | NONE => false + +fun repair_predicates_in_term const_tab (t as ATerm ((s, _), ts)) = + if s = type_wrapper_name then + case ts of + [_, t' as ATerm ((s', _), _)] => + if is_predicate const_tab s' then t' else boolify t + | _ => raise Fail "malformed type wrapper" + else + t |> not (is_predicate const_tab s) ? boolify + +fun close_universally phi = + let + fun term_vars bounds (ATerm (name as (s, _), tms)) = + (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)) = + formula_vars (xs @ bounds) phi + | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis + | formula_vars bounds (APred tm) = term_vars bounds tm + in + case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi) + end + +fun repair_formula thy explicit_forall full_types const_tab = + let + fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi) + | aux (AConn (c, phis)) = AConn (c, map aux phis) + | aux (APred tm) = + APred (tm |> repair_applications_in_term thy full_types const_tab + |> repair_predicates_in_term const_tab) + in aux #> explicit_forall ? close_universally end + +fun repair_problem_line thy explicit_forall full_types const_tab + (Fof (ident, kind, phi)) = + Fof (ident, kind, repair_formula thy explicit_forall full_types const_tab phi) +fun repair_problem_with_const_table thy = + map o apsnd o map ooo repair_problem_line thy + +fun repair_problem thy explicit_forall full_types explicit_apply problem = + repair_problem_with_const_table thy explicit_forall full_types + (const_table_for_problem explicit_apply problem) problem + +fun write_tptp_file thy readable_names explicit_forall full_types explicit_apply + file (conjectures, axiom_clauses, extra_clauses, + helper_clauses, class_rel_clauses, arity_clauses) = + let + val axiom_lines = map (problem_line_for_axiom full_types) axiom_clauses + val class_rel_lines = + map problem_line_for_class_rel_clause class_rel_clauses + val arity_lines = map problem_line_for_arity_clause arity_clauses + val helper_lines = map (problem_line_for_axiom full_types) helper_clauses + val conjecture_lines = + map (problem_line_for_conjecture full_types) conjectures + val tfree_lines = problem_lines_for_free_types conjectures + (* Reordering these might or might not confuse the proof reconstruction + code or the SPASS Flotter hack. *) + val problem = + [("Relevant facts", axiom_lines), + ("Class relationships", class_rel_lines), + ("Arity declarations", arity_lines), + ("Helper facts", helper_lines), + ("Conjectures", conjecture_lines), + ("Type variables", tfree_lines)] + |> repair_problem thy explicit_forall full_types explicit_apply + val (problem, pool) = nice_tptp_problem readable_names problem + val conjecture_offset = + length axiom_lines + length class_rel_lines + length arity_lines + + length helper_lines + val _ = File.write_list file (strings_for_tptp_problem problem) + in + (case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty, + conjecture_offset) + end + +fun extract_clause_sequence output = + let + val tokens_of = String.tokens (not o Char.isAlphaNum) + fun extract_num ("clause" :: (ss as _ :: _)) = + Int.fromString (List.last ss) + | extract_num _ = NONE + in output |> split_lines |> map_filter (extract_num o tokens_of) end + +val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation" + +val parse_clause_formula_pair = + $$ "(" |-- scan_integer --| $$ "," -- Symbol.scan_id --| $$ ")" + --| Scan.option ($$ ",") +val parse_clause_formula_relation = + Scan.this_string set_ClauseFormulaRelationN |-- $$ "(" + |-- Scan.repeat parse_clause_formula_pair +val extract_clause_formula_relation = + Substring.full + #> Substring.position set_ClauseFormulaRelationN + #> snd #> Substring.string #> strip_spaces #> explode + #> parse_clause_formula_relation #> fst + +fun repair_conjecture_shape_and_theorem_names output conjecture_shape + thm_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 "SPASS_TPTP" script is also part + of this hack. *) + let + val j0 = hd conjecture_shape + val seq = extract_clause_sequence output + val name_map = extract_clause_formula_relation output + fun renumber_conjecture j = + AList.find (op =) name_map (conjecture_prefix ^ Int.toString (j - j0)) + |> the_single + |> (fn s => find_index (curry (op =) s) seq + 1) + in + (conjecture_shape |> map renumber_conjecture, + seq |> map (the o AList.lookup (op =) name_map) + |> map (fn s => case try (unprefix axiom_prefix) s of + SOME s' => undo_ascii_of s' + | NONE => "") + |> Vector.fromList) + end + else + (conjecture_shape, thm_names) + + +(* generic TPTP-based provers *) + +fun prover_fun name + {home_var, executable, arguments, proof_delims, known_failures, + max_new_relevant_facts_per_iter, prefers_theory_relevant, + explicit_forall} + ({debug, overlord, full_types, explicit_apply, 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, (_, th)) = goal; + val thy = ProofContext.theory_of ctxt + (* ### FIXME: (1) preprocessing for "if" etc. *) + val (params, hyp_ts, concl_t) = strip_subgoal th subgoal + val the_filtered_clauses = + case filtered_clauses of + SOME fcls => fcls + | NONE => relevant_facts full_types relevance_threshold + relevance_convergence defs_relevant + max_new_relevant_facts_per_iter + (the_default prefers_theory_relevant theory_relevant) + relevance_override goal hyp_ts concl_t + val the_axiom_clauses = axiom_clauses |> the_default the_filtered_clauses + val (internal_thm_names, clauses) = + prepare_clauses ctxt full_types hyp_ts concl_t the_axiom_clauses + the_filtered_clauses + + (* path to unique problem file *) + val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER" + else Config.get ctxt dest_dir; + val the_problem_prefix = Config.get ctxt problem_prefix; + fun prob_pathname nr = + let + val probfile = + Path.basic ((if overlord then "prob_" ^ name + else the_problem_prefix ^ serial_string ()) + ^ "_" ^ string_of_int nr) + in + if the_dest_dir = "" then File.tmp_path probfile + else if File.exists (Path.explode the_dest_dir) + then Path.append (Path.explode the_dest_dir) probfile + else error ("No such directory: " ^ the_dest_dir ^ ".") + end; + + val home = getenv home_var + val command = Path.explode (home ^ "/" ^ executable) + (* write out problem file and call prover *) + fun command_line complete probfile = + let + val core = File.shell_path command ^ " " ^ arguments complete timeout ^ + " " ^ File.shell_path probfile + in + (if Config.get ctxt measure_runtime then + "TIMEFORMAT='%3U'; { time " ^ core ^ " ; }" + else + "exec " ^ core) ^ " 2>&1" + end + fun split_time s = + let + val split = String.tokens (fn c => str c = "\n"); + val (output, t) = s |> split |> split_last |> apfst cat_lines; + fun as_num f = f >> (fst o read_int); + val num = as_num (Scan.many1 Symbol.is_ascii_digit); + val digit = Scan.one Symbol.is_ascii_digit; + val num3 = as_num (digit ::: digit ::: (digit >> single)); + val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b); + val as_time = the_default 0 o Scan.read Symbol.stopper time o explode; + in (output, as_time t) end; + fun run_on probfile = + if home = "" then + error ("The environment variable " ^ quote home_var ^ " is not set.") + else if File.exists command then + let + fun do_run complete = + let + val command = command_line complete probfile + val ((output, msecs), res_code) = + bash_output command + |>> (if overlord then + prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") + else + I) + |>> (if Config.get ctxt measure_runtime then split_time + else rpair 0) + val (proof, outcome) = + extract_proof_and_outcome complete res_code proof_delims + known_failures output + in (output, msecs, proof, outcome) end + val readable_names = debug andalso overlord + val (pool, conjecture_offset) = + write_tptp_file thy readable_names explicit_forall full_types + explicit_apply probfile clauses + val conjecture_shape = + conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1 + val result = + do_run false + |> (fn (_, msecs0, _, SOME _) => + do_run true + |> (fn (output, msecs, proof, outcome) => + (output, msecs0 + msecs, proof, outcome)) + | result => result) + in ((pool, conjecture_shape), result) end + else + error ("Bad executable: " ^ Path.implode command ^ "."); + + (* If the problem file has not been exported, remove it; otherwise, export + the proof file too. *) + fun cleanup probfile = + if the_dest_dir = "" then try File.rm probfile else NONE + fun export probfile (_, (output, _, _, _)) = + if the_dest_dir = "" then + () + else + File.write (Path.explode (Path.implode probfile ^ "_proof")) output + + val ((pool, conjecture_shape), (output, msecs, proof, outcome)) = + with_path cleanup export run_on (prob_pathname subgoal) + val (conjecture_shape, internal_thm_names) = + repair_conjecture_shape_and_theorem_names output conjecture_shape + internal_thm_names + + val (message, used_thm_names) = + case outcome of + NONE => + proof_text isar_proof + (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) + (full_types, minimize_command, proof, internal_thm_names, th, + subgoal) + | SOME failure => (string_for_failure failure ^ "\n", []) + in + {outcome = outcome, message = message, pool = pool, + used_thm_names = used_thm_names, atp_run_time_in_msecs = msecs, + output = output, proof = proof, internal_thm_names = internal_thm_names, + conjecture_shape = conjecture_shape, + filtered_clauses = the_filtered_clauses} + end + +fun get_prover_fun thy name = prover_fun name (get_prover thy name) + +(* start prover thread *) +fun start_prover_thread (params as {verbose, full_types, timeout, ...}) i n + relevance_override minimize_command proof_state name = + let + val thy = Proof.theory_of proof_state + val birth_time = Time.now () + val death_time = Time.+ (birth_time, timeout) + val prover = get_prover_fun thy name + val {context = ctxt, facts, goal} = Proof.goal proof_state; + val desc = + "ATP " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^ + Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)); + in + Async_Manager.launch das_Tool verbose birth_time death_time desc + (fn () => + let + val problem = + {subgoal = i, goal = (ctxt, (facts, goal)), + relevance_override = relevance_override, axiom_clauses = NONE, + filtered_clauses = NONE} + in + prover params (minimize_command name) timeout problem |> #message + handle ERROR message => "Error: " ^ message ^ "\n" + end) + end + +val setup = + dest_dir_setup + #> problem_prefix_setup + #> measure_runtime_setup + +end; diff -r 0c15b8a655cd -r dc56a9a8e19d src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Jul 27 17:10:27 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Jul 27 20:16:14 2010 +0200 @@ -1,5 +1,5 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML - Author: Jia Meng, Cambridge University Computer Laboratory, NICTA + Author: Jia Meng, Cambridge University Computer Laboratory and NICTA Author: Jasmin Blanchette, TU Muenchen *) diff -r 0c15b8a655cd -r dc56a9a8e19d src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Tue Jul 27 17:10:27 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Tue Jul 27 20:16:14 2010 +0200 @@ -7,8 +7,8 @@ signature SLEDGEHAMMER_FACT_MINIMIZER = sig - type params = ATP_Manager.params - type prover_result = ATP_Manager.prover_result + type params = Sledgehammer.params + type prover_result = Sledgehammer.prover_result val minimize_theorems : params -> int -> int -> Proof.state -> (string * thm list) list @@ -21,19 +21,7 @@ open Metis_Clauses open Sledgehammer_Util open Sledgehammer_Proof_Reconstruct -open ATP_Manager - -(* Linear minimization algorithm *) - -fun linear_minimize test s = - let - fun aux [] p = p - | aux (x :: xs) (needed, result) = - case test (xs @ needed) of - SOME result => aux xs (needed, result) - | NONE => aux xs (x :: needed, result) - in aux s end - +open Sledgehammer (* wrapper for calling external prover *) @@ -52,8 +40,15 @@ let val thy = Proof.theory_of state val num_theorems = length name_thms_pairs - val _ = priority ("Testing " ^ string_of_int num_theorems ^ - " theorem" ^ plural_s num_theorems ^ "...") + val _ = + priority ("Testing " ^ string_of_int num_theorems ^ + " theorem" ^ plural_s num_theorems ^ + (if num_theorems > 0 then + ": " ^ space_implode " " + (name_thms_pairs + |> map fst |> sort_distinct string_ord) + else + "") ^ "...") val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs val {context = ctxt, facts, goal} = Proof.goal state val problem = @@ -69,62 +64,62 @@ (* minimalization of thms *) +fun filter_used_facts used = filter (member (op =) used o fst) + +fun sublinear_minimize _ [] p = p + | sublinear_minimize test (x :: xs) (seen, result) = + case test (xs @ seen) of + result as {outcome = NONE, proof, used_thm_names, ...} + : prover_result => + sublinear_minimize test (filter_used_facts used_thm_names xs) + (filter_used_facts used_thm_names seen, result) + | _ => sublinear_minimize test xs (x :: seen, result) + fun minimize_theorems (params as {debug, atps, full_types, minimize_timeout, isar_proof, isar_shrink_factor, ...}) i n state name_thms_pairs = let val thy = Proof.theory_of state val prover = case atps of - [atp_name] => get_prover thy atp_name + [atp_name] => get_prover_fun thy atp_name | _ => error "Expected a single ATP." val msecs = Time.toMilliseconds minimize_timeout val _ = priority ("Sledgehammer minimizer: ATP " ^ quote (the_single atps) ^ " with a time limit of " ^ string_of_int msecs ^ " ms.") - val test_thms_fun = + val test_facts = sledgehammer_test_theorems params prover minimize_timeout i state - fun test_thms filtered thms = - case test_thms_fun filtered thms of - (result as {outcome = NONE, ...}) => SOME result - | _ => NONE - 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 - result as {outcome = NONE, pool, internal_thm_names, conjecture_shape, - filtered_clauses, ...} => - let - val used = internal_thm_names |> Vector.foldr (op ::) [] - |> sort_distinct string_ord - val to_use = - if length used < length name_thms_pairs then - filter (fn (name1, _) => exists (curry (op =) name1) used) - name_thms_pairs - else name_thms_pairs - val (min_thms, {proof, internal_thm_names, ...}) = - linear_minimize (test_thms (SOME filtered_clauses)) to_use - ([], result) - val m = length min_thms - val _ = priority (cat_lines - ["Minimized: " ^ string_of_int m ^ " theorem" ^ plural_s m] ^ ".") - in - (SOME min_thms, - proof_text isar_proof - (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) - (full_types, K "", proof, internal_thm_names, goal, i) |> fst) - end - | {outcome = SOME TimedOut, ...} => - (NONE, "Timeout: You can increase the time limit using the \"timeout\" \ - \option (e.g., \"timeout = " ^ - string_of_int (10 + msecs div 1000) ^ " s\").") - | {outcome = SOME UnknownError, ...} => - (* Failure sometimes mean timeout, unfortunately. *) - (NONE, "Failure: No proof was found with the current time limit. You \ - \can increase the time limit using the \"timeout\" \ - \option (e.g., \"timeout = " ^ - string_of_int (10 + msecs div 1000) ^ " s\").") - | {message, ...} => (NONE, "ATP error: " ^ message)) + (case test_facts NONE name_thms_pairs of + result as {outcome = NONE, pool, proof, used_thm_names, + conjecture_shape, filtered_clauses, ...} => + let + val (min_thms, {proof, internal_thm_names, ...}) = + sublinear_minimize (test_facts (SOME filtered_clauses)) + (filter_used_facts used_thm_names name_thms_pairs) + ([], result) + val m = length min_thms + val _ = priority (cat_lines + ["Minimized: " ^ string_of_int m ^ " theorem" ^ plural_s m] ^ ".") + in + (SOME min_thms, + proof_text isar_proof + (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) + (full_types, K "", proof, internal_thm_names, goal, i) |> fst) + end + | {outcome = SOME TimedOut, ...} => + (NONE, "Timeout: You can increase the time limit using the \"timeout\" \ + \option (e.g., \"timeout = " ^ + string_of_int (10 + msecs div 1000) ^ " s\").") + | {outcome = SOME UnknownError, ...} => + (* Failure sometimes mean timeout, unfortunately. *) + (NONE, "Failure: No proof was found with the current time limit. You \ + \can increase the time limit using the \"timeout\" \ + \option (e.g., \"timeout = " ^ + string_of_int (10 + msecs div 1000) ^ " s\").") + | {message, ...} => (NONE, "ATP error: " ^ message)) handle ERROR msg => (NONE, "Error: " ^ msg) end diff -r 0c15b8a655cd -r dc56a9a8e19d src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Jul 27 17:10:27 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Jul 27 20:16:14 2010 +0200 @@ -6,7 +6,7 @@ signature SLEDGEHAMMER_ISAR = sig - type params = ATP_Manager.params + type params = Sledgehammer.params val atps: string Unsynchronized.ref val timeout: int Unsynchronized.ref @@ -17,10 +17,10 @@ structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR = struct +open ATP_Systems open Sledgehammer_Util open Sledgehammer_Fact_Filter -open ATP_Manager -open ATP_Systems +open Sledgehammer open Sledgehammer_Fact_Minimizer (** Sledgehammer commands **) diff -r 0c15b8a655cd -r dc56a9a8e19d src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Jul 27 17:10:27 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Jul 27 20:16:14 2010 +0200 @@ -1,5 +1,6 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML - Author: Lawrence C Paulson and Claire Quigley, Cambridge University Computer Laboratory + Author: Lawrence C. Paulson, Cambridge University Computer Laboratory + Author: Claire Quigley, Cambridge University Computer Laboratory Author: Jasmin Blanchette, TU Muenchen Transfer of proofs from external provers. @@ -26,14 +27,34 @@ structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT = struct +open ATP_Problem open Metis_Clauses open Sledgehammer_Util open Sledgehammer_Fact_Filter -open Sledgehammer_TPTP_Format type minimize_command = string list -> string -fun mk_anot phi = AConn (ANot, [phi]) +(* Simple simplifications to ensure that sort annotations don't leave a trail of + spurious "True"s. *) +fun s_not @{const False} = @{const True} + | s_not @{const True} = @{const False} + | s_not (@{const Not} $ t) = t + | s_not t = @{const Not} $ t +fun s_conj (@{const True}, t2) = t2 + | s_conj (t1, @{const True}) = t1 + | s_conj p = HOLogic.mk_conj p +fun s_disj (@{const False}, t2) = t2 + | s_disj (t1, @{const False}) = t1 + | s_disj p = HOLogic.mk_disj p +fun s_imp (@{const True}, t2) = t2 + | s_imp (t1, @{const False}) = s_not t1 + | s_imp p = HOLogic.mk_imp p +fun s_iff (@{const True}, t2) = t2 + | s_iff (t1, @{const True}) = t1 + | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2 + +fun mk_anot (AConn (ANot, [phi])) = phi + | mk_anot phi = AConn (ANot, [phi]) fun mk_aconn c (phi1, phi2) = AConn (c, [phi1, phi2]) val index_in_shape : int -> int list -> int = find_index o curry (op =) @@ -220,6 +241,20 @@ Type_Infer.param 0 (a, HOLogic.typeS) end +(* Type class literal applied to a type. Returns triple of polarity, class, + type. *) +fun type_constraint_from_term pos tfrees (u as ATerm (a, us)) = + case (strip_prefix_and_undo_ascii class_prefix a, + map (type_from_fo_term tfrees) us) of + (SOME b, [T]) => (pos, b, T) + | _ => raise FO_TERM [u] + +(** Accumulate type constraints in a clause: negative type literals **) +fun add_var (key, z) = Vartab.map_default (key, []) (cons z) +fun add_type_constraint (false, cl, TFree (a ,_)) = add_var ((a, ~1), cl) + | add_type_constraint (false, cl, TVar (ix, _)) = add_var (ix, cl) + | add_type_constraint _ = I + fun fix_atp_variable_name s = let fun subscript_name s n = s ^ nat_subscript n @@ -238,8 +273,8 @@ end (* First-order translation. No types are known for variables. "HOLogic.typeT" - should allow them to be inferred.*) -fun term_from_fo_term thy full_types tfrees opt_T = + should allow them to be inferred. *) +fun raw_term_from_pred thy full_types tfrees = let fun aux opt_T extra_us u = case u of @@ -289,32 +324,19 @@ case strip_prefix_and_undo_ascii schematic_var_prefix a of SOME b => Var ((b, 0), T) | NONE => - (* Variable from the ATP, say "X1" *) - Var ((fix_atp_variable_name a, 0), T) + if is_tptp_variable a then + Var ((fix_atp_variable_name a, 0), T) + else + raise Fail ("Unexpected constant: " ^ quote a) in list_comb (t, ts) end - in aux opt_T [] end + in aux (SOME HOLogic.boolT) [] end -(* Type class literal applied to a type. Returns triple of polarity, class, - type. *) -fun type_constraint_from_formula pos tfrees (AConn (ANot, [u])) = - type_constraint_from_formula (not pos) tfrees u - | type_constraint_from_formula pos tfrees (phi as APred (ATerm (a, us))) = - (case (strip_prefix_and_undo_ascii class_prefix a, - map (type_from_fo_term tfrees) us) of - (SOME b, [T]) => (pos, b, T) - | _ => raise FORMULA [phi]) - | type_constraint_from_formula _ _ phi = raise FORMULA [phi] - -(** Accumulate type constraints in a clause: negative type literals **) - -fun add_var (key, z) = Vartab.map_default (key, []) (cons z) - -fun add_type_constraint (false, cl, TFree (a ,_)) = add_var ((a, ~1), cl) - | add_type_constraint (false, cl, TVar (ix, _)) = add_var (ix, cl) - | add_type_constraint _ = I - -fun is_positive_literal (@{const Not} $ _) = false - | is_positive_literal _ = true +fun term_from_pred thy full_types tfrees pos (u as ATerm (s, _)) = + if String.isPrefix class_prefix s then + add_type_constraint (type_constraint_from_term pos tfrees u) + #> pair @{const True} + else + pair (raw_term_from_pred thy full_types tfrees u) val combinator_table = [(@{const_name COMBI}, @{thm COMBI_def_raw}), @@ -331,12 +353,9 @@ | NONE => t) | uncombine_term t = t -fun disjuncts (AConn (AOr, phis)) = maps disjuncts phis - | disjuncts phi = [phi] - (* Update schematic type variables with detected sort constraints. It's not totally clear when this code is necessary. *) -fun repair_tvar_sorts (tvar_tab, t) = +fun repair_tvar_sorts (t, tvar_tab) = let fun do_type (Type (a, Ts)) = Type (a, map do_type Ts) | do_type (TVar (xi, s)) = @@ -350,58 +369,39 @@ | do_term (t1 $ t2) = do_term t1 $ do_term t2 in t |> not (Vartab.is_empty tvar_tab) ? do_term end -fun s_disj (t1, @{const False}) = t1 - | s_disj p = HOLogic.mk_disj p - fun quantify_over_free quant_s free_s body_t = case Term.add_frees body_t [] |> filter (curry (op =) free_s o fst) of [] => body_t | frees as (_, free_T) :: _ => Abs (free_s, free_T, fold (curry abstract_over) (map Free frees) body_t) - (* Interpret a list of syntax trees as a clause, given by "real" literals and - sort constraints. Accumulates sort constraints in "tvar_tab", with "real" - literals in "lits". *) -fun prop_from_formula thy full_types tfrees = - let - val do_sort_constraint = - add_type_constraint o type_constraint_from_formula true tfrees - fun do_real_literal phi = +(* Interpret a list of syntax trees as a clause, extracting sort constraints + as they appear in the formula. *) +fun prop_from_formula thy full_types tfrees phi = + let + fun do_formula pos phi = case phi of - AQuant (_, [], phi) => do_real_literal phi + AQuant (_, [], phi) => do_formula pos phi | AQuant (q, x :: xs, phi') => - let - val body = do_real_literal (AQuant (q, xs, phi')) - val quant_s = case q of - AForall => @{const_name All} - | AExists => @{const_name Ex} - in quantify_over_free quant_s x body end - | AConn (ANot, [phi']) => HOLogic.mk_not (do_real_literal phi') + do_formula pos (AQuant (q, xs, phi')) + #>> quantify_over_free (case q of + AForall => @{const_name All} + | AExists => @{const_name Ex}) x + | AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not | AConn (c, [phi1, phi2]) => - (phi1, phi2) - |> pairself do_real_literal - |> (case c of - AAnd => HOLogic.mk_conj - | AOr => HOLogic.mk_disj - | AImplies => HOLogic.mk_imp - | AIff => (fn (t1, t2) => HOLogic.eq_const HOLogic.boolT $ t1 $ t2)) - | APred tm => - term_from_fo_term thy full_types tfrees (SOME @{typ bool}) tm + do_formula (pos |> c = AImplies ? not) phi1 + ##>> do_formula pos phi2 + #>> (case c of + AAnd => s_conj + | AOr => s_disj + | AImplies => s_imp + | AIff => s_iff) + | APred tm => term_from_pred thy full_types tfrees pos tm | _ => raise FORMULA [phi] - fun do_literals (tvar_tab, t) [] = (tvar_tab, t) - | do_literals (tvar_tab, t) (u :: us) = - (do_literals (tvar_tab |> do_sort_constraint u, t) us - handle FO_TERM _ => raise SAME () - | FORMULA _ => raise SAME ()) - handle SAME () => - do_literals (tvar_tab, s_disj (do_real_literal u, t)) us - in - repair_tvar_sorts o do_literals (Vartab.empty, HOLogic.false_const) - o disjuncts - end + in repair_tvar_sorts (do_formula true phi Vartab.empty) end fun check_formula ctxt = - Type_Infer.constrain @{typ bool} + Type_Infer.constrain HOLogic.boolT #> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt) @@ -565,17 +565,18 @@ val unprefix_chained = perhaps (try (unprefix chained_prefix)) +fun used_facts thm_names = + extract_formula_numbers_in_atp_proof + #> filter (is_axiom_clause_number thm_names) + #> map (fn i => Vector.sub (thm_names, i - 1)) + #> List.partition (String.isPrefix chained_prefix) + #>> map (unprefix chained_prefix) + #> pairself (sort_distinct string_ord) + fun metis_proof_text (full_types, minimize_command, atp_proof, thm_names, goal, i) = let - val raw_lemmas = - atp_proof |> extract_formula_numbers_in_atp_proof - |> filter (is_axiom_clause_number thm_names) - |> map (fn i => Vector.sub (thm_names, i - 1)) - val (chained_lemmas, other_lemmas) = - raw_lemmas |> List.partition (String.isPrefix chained_prefix) - |>> map (unprefix chained_prefix) - |> pairself (sort_distinct string_ord) + val (chained_lemmas, other_lemmas) = used_facts thm_names atp_proof val lemmas = other_lemmas @ chained_lemmas val n = Logic.count_prems (prop_of goal) in @@ -937,8 +938,6 @@ (other_params as (full_types, _, atp_proof, thm_names, goal, i)) = let - (* ### FIXME: avoid duplication with ATP_Systems -- and move strip_subgoal - to ATP_Systems *) val (params, hyp_ts, concl_t) = strip_subgoal goal i val frees = fold Term.add_frees (concl_t :: hyp_ts) [] val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) [] diff -r 0c15b8a655cd -r dc56a9a8e19d src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Tue Jul 27 17:10:27 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,429 +0,0 @@ -(* Title: HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML - Author: Jia Meng, NICTA - Author: Jasmin Blanchette, TU Muenchen - -TPTP syntax. -*) - -signature SLEDGEHAMMER_TPTP_FORMAT = -sig - type name = Metis_Clauses.name - type kind = Metis_Clauses.kind - type combterm = Metis_Clauses.combterm - type class_rel_clause = Metis_Clauses.class_rel_clause - type arity_clause = Metis_Clauses.arity_clause - - datatype 'a fo_term = ATerm of 'a * 'a fo_term list - datatype quantifier = AForall | AExists - datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff - datatype ('a, 'b) formula = - AQuant of quantifier * 'a list * ('a, 'b) formula | - AConn of connective * ('a, 'b) formula list | - APred of 'b - - datatype fol_formula = - FOLFormula of {formula_name: string, - kind: kind, - combformula: (name, combterm) formula, - ctypes_sorts: typ list} - - val axiom_prefix : string - val conjecture_prefix : string - val write_tptp_file : - theory -> bool -> bool -> bool -> bool -> Path.T - -> fol_formula list * fol_formula list * fol_formula list * fol_formula list - * class_rel_clause list * arity_clause list - -> string Symtab.table * int -end; - -structure Sledgehammer_TPTP_Format : SLEDGEHAMMER_TPTP_FORMAT = -struct - -open Metis_Clauses -open Sledgehammer_Util - - -(** ATP problem **) - -datatype 'a fo_term = ATerm of 'a * 'a fo_term list -datatype quantifier = AForall | AExists -datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff -datatype ('a, 'b) formula = - AQuant of quantifier * 'a list * ('a, 'b) formula | - AConn of connective * ('a, 'b) formula list | - APred of 'b - -fun mk_anot phi = AConn (ANot, [phi]) -fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2]) -fun mk_ahorn [] phi = phi - | mk_ahorn (phi :: phis) psi = - AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi]) - -datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula -type 'a problem = (string * 'a problem_line list) list - -fun string_for_term (ATerm (s, [])) = s - | string_for_term (ATerm (s, ts)) = - if s = "equal" then space_implode " = " (map string_for_term ts) - else s ^ "(" ^ commas (map string_for_term ts) ^ ")" -fun string_for_quantifier AForall = "!" - | string_for_quantifier AExists = "?" -fun string_for_connective ANot = "~" - | string_for_connective AAnd = "&" - | string_for_connective AOr = "|" - | string_for_connective AImplies = "=>" - | string_for_connective AIf = "<=" - | string_for_connective AIff = "<=>" - | string_for_connective ANotIff = "<~>" -fun string_for_formula (AQuant (q, xs, phi)) = - string_for_quantifier q ^ "[" ^ commas xs ^ "]: " ^ - string_for_formula phi - | string_for_formula (AConn (ANot, [APred (ATerm ("equal", ts))])) = - space_implode " != " (map string_for_term ts) - | string_for_formula (AConn (c, [phi])) = - string_for_connective c ^ " " ^ string_for_formula phi - | string_for_formula (AConn (c, phis)) = - "(" ^ space_implode (" " ^ string_for_connective c ^ " ") - (map string_for_formula phis) ^ ")" - | string_for_formula (APred tm) = string_for_term tm - -fun string_for_problem_line (Fof (ident, kind, phi)) = - "fof(" ^ ident ^ ", " ^ - (case kind of Axiom => "axiom" | Conjecture => "conjecture") ^ ",\n" ^ - " (" ^ string_for_formula phi ^ ")).\n" -fun strings_for_problem problem = - "% This file was generated by Isabelle (most likely Sledgehammer)\n\ - \% " ^ timestamp () ^ "\n" :: - maps (fn (_, []) => [] - | (heading, lines) => - "\n% " ^ heading ^ " (" ^ Int.toString (length lines) ^ ")\n" :: - map string_for_problem_line lines) problem - - -(** Nice names **) - -fun empty_name_pool readable_names = - if readable_names then SOME (Symtab.empty, Symtab.empty) else NONE - -fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs -fun pool_map f xs = - pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs [] - -(* "equal" is reserved by some ATPs. "op" is also reserved, to avoid the - unreadable "op_1", "op_2", etc., in the problem files. *) -val reserved_nice_names = ["equal", "op"] -fun readable_name full_name s = - if s = full_name then - s - else - let - val s = s |> Long_Name.base_name - |> Name.desymbolize (Char.isUpper (String.sub (full_name, 0))) - in if member (op =) reserved_nice_names s then full_name else s end - -fun nice_name (full_name, _) NONE = (full_name, NONE) - | nice_name (full_name, desired_name) (SOME the_pool) = - case Symtab.lookup (fst the_pool) full_name of - SOME nice_name => (nice_name, SOME the_pool) - | NONE => - let - val nice_prefix = readable_name full_name desired_name - fun add j = - let - val nice_name = nice_prefix ^ - (if j = 0 then "" else "_" ^ Int.toString j) - in - case Symtab.lookup (snd the_pool) nice_name of - SOME full_name' => - if full_name = full_name' then (nice_name, the_pool) - else add (j + 1) - | NONE => - (nice_name, - (Symtab.update_new (full_name, nice_name) (fst the_pool), - Symtab.update_new (nice_name, full_name) (snd the_pool))) - end - in add 0 |> apsnd SOME end - - -fun nice_term (ATerm (name, ts)) = - nice_name name ##>> pool_map nice_term ts #>> ATerm -fun nice_formula (AQuant (q, xs, phi)) = - pool_map nice_name xs ##>> nice_formula phi - #>> (fn (xs, phi) => AQuant (q, xs, phi)) - | nice_formula (AConn (c, phis)) = - pool_map nice_formula phis #>> curry AConn c - | nice_formula (APred tm) = nice_term tm #>> APred -fun nice_problem_line (Fof (ident, kind, phi)) = - nice_formula phi #>> (fn phi => Fof (ident, kind, phi)) -fun nice_problem problem = - pool_map (fn (heading, lines) => - pool_map nice_problem_line lines #>> pair heading) problem - - -(** Sledgehammer stuff **) - -datatype fol_formula = - FOLFormula of {formula_name: string, - kind: kind, - combformula: (name, combterm) formula, - ctypes_sorts: typ list} - -val axiom_prefix = "ax_" -val conjecture_prefix = "conj_" -val arity_clause_prefix = "clsarity_" -val tfrees_name = "tfrees" - -fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t]) - -fun fo_term_for_combtyp (CombTVar name) = ATerm (name, []) - | fo_term_for_combtyp (CombTFree name) = ATerm (name, []) - | fo_term_for_combtyp (CombType (name, tys)) = - ATerm (name, map fo_term_for_combtyp tys) - -fun fo_literal_for_type_literal (TyLitVar (class, name)) = - (true, ATerm (class, [ATerm (name, [])])) - | fo_literal_for_type_literal (TyLitFree (class, name)) = - (true, ATerm (class, [ATerm (name, [])])) - -fun formula_for_fo_literal (pos, t) = APred t |> not pos ? mk_anot - -fun fo_term_for_combterm full_types = - let - fun aux top_level u = - let - val (head, args) = strip_combterm_comb u - val (x, ty_args) = - case head of - CombConst (name, _, ty_args) => - if fst name = "equal" then - (if top_level andalso length args = 2 then name - else ("c_fequal", @{const_name fequal}), []) - else - (name, if full_types then [] else ty_args) - | CombVar (name, _) => (name, []) - | CombApp _ => raise Fail "impossible \"CombApp\"" - val t = ATerm (x, map fo_term_for_combtyp ty_args @ - map (aux false) args) - in - if full_types then wrap_type (fo_term_for_combtyp (combtyp_of u)) t else t - end - in aux true end - -fun formula_for_combformula full_types = - let - fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi) - | aux (AConn (c, phis)) = AConn (c, map aux phis) - | aux (APred tm) = APred (fo_term_for_combterm full_types tm) - in aux end - -fun formula_for_axiom full_types (FOLFormula {combformula, ctypes_sorts, ...}) = - mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal) - (type_literals_for_types ctypes_sorts)) - (formula_for_combformula full_types combformula) - -fun problem_line_for_axiom full_types - (formula as FOLFormula {formula_name, kind, ...}) = - Fof (axiom_prefix ^ ascii_of formula_name, kind, - formula_for_axiom full_types formula) - -fun problem_line_for_class_rel_clause - (ClassRelClause {axiom_name, subclass, superclass, ...}) = - let val ty_arg = ATerm (("T", "T"), []) in - Fof (ascii_of axiom_name, Axiom, - AConn (AImplies, [APred (ATerm (subclass, [ty_arg])), - APred (ATerm (superclass, [ty_arg]))])) - end - -fun fo_literal_for_arity_literal (TConsLit (c, t, args)) = - (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)])) - | fo_literal_for_arity_literal (TVarLit (c, sort)) = - (false, ATerm (c, [ATerm (sort, [])])) - -fun problem_line_for_arity_clause - (ArityClause {axiom_name, conclLit, premLits, ...}) = - Fof (arity_clause_prefix ^ ascii_of axiom_name, Axiom, - mk_ahorn (map (formula_for_fo_literal o apfst not - o fo_literal_for_arity_literal) premLits) - (formula_for_fo_literal - (fo_literal_for_arity_literal conclLit))) - -fun problem_line_for_conjecture full_types - (FOLFormula {formula_name, kind, combformula, ...}) = - Fof (conjecture_prefix ^ formula_name, kind, - formula_for_combformula full_types combformula) - -fun free_type_literals_for_conjecture (FOLFormula {ctypes_sorts, ...}) = - map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts) - -fun problem_line_for_free_type lit = - Fof (tfrees_name, Conjecture, mk_anot (formula_for_fo_literal lit)) -fun problem_lines_for_free_types conjectures = - let - val litss = map free_type_literals_for_conjecture conjectures - val lits = fold (union (op =)) litss [] - in map problem_line_for_free_type lits end - -(** "hBOOL" and "hAPP" **) - -type const_info = {min_arity: int, max_arity: int, sub_level: bool} - -fun is_variable s = Char.isUpper (String.sub (s, 0)) - -fun consider_term top_level (ATerm ((s, _), ts)) = - (if is_variable s then - I - else - let val n = length ts in - Symtab.map_default - (s, {min_arity = n, max_arity = 0, sub_level = false}) - (fn {min_arity, max_arity, sub_level} => - {min_arity = Int.min (n, min_arity), - max_arity = Int.max (n, max_arity), - sub_level = sub_level orelse not top_level}) - end) - #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts -fun consider_formula (AQuant (_, _, phi)) = consider_formula phi - | consider_formula (AConn (_, phis)) = fold consider_formula phis - | consider_formula (APred tm) = consider_term true tm - -fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi -fun consider_problem problem = fold (fold consider_problem_line o snd) problem - -fun const_table_for_problem explicit_apply problem = - if explicit_apply then NONE - else SOME (Symtab.empty |> consider_problem problem) - -val tc_fun = make_fixed_type_const @{type_name fun} - -fun min_arity_of thy full_types NONE s = - (if s = "equal" orelse s = type_wrapper_name orelse - String.isPrefix type_const_prefix s orelse - String.isPrefix class_prefix s then - 16383 (* large number *) - else if full_types then - 0 - else case strip_prefix_and_undo_ascii const_prefix s of - SOME s' => num_type_args thy (invert_const s') - | NONE => 0) - | min_arity_of _ _ (SOME the_const_tab) s = - case Symtab.lookup the_const_tab s of - SOME ({min_arity, ...} : const_info) => min_arity - | NONE => 0 - -fun full_type_of (ATerm ((s, _), [ty, _])) = - if s = type_wrapper_name then ty else raise Fail "expected type wrapper" - | full_type_of _ = raise Fail "expected type wrapper" - -fun list_hAPP_rev _ t1 [] = t1 - | list_hAPP_rev NONE t1 (t2 :: ts2) = - ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2]) - | list_hAPP_rev (SOME ty) t1 (t2 :: ts2) = - let val ty' = ATerm (`make_fixed_type_const @{type_name fun}, - [full_type_of t2, ty]) in - ATerm (`I "hAPP", [wrap_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2]) - end - -fun repair_applications_in_term thy full_types const_tab = - let - fun aux opt_ty (ATerm (name as (s, _), ts)) = - if s = type_wrapper_name then - case ts of - [t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2]) - | _ => raise Fail "malformed type wrapper" - else - let - val ts = map (aux NONE) ts - val (ts1, ts2) = chop (min_arity_of thy full_types const_tab s) ts - in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end - in aux NONE end - -fun boolify t = ATerm (`I "hBOOL", [t]) - -(* True if the constant ever appears outside of the top-level position in - literals, or if it appears with different arities (e.g., because of different - type instantiations). If false, the constant always receives all of its - arguments and is used as a predicate. *) -fun is_predicate NONE s = - s = "equal" orelse String.isPrefix type_const_prefix s orelse - String.isPrefix class_prefix s - | is_predicate (SOME the_const_tab) s = - case Symtab.lookup the_const_tab s of - SOME {min_arity, max_arity, sub_level} => - not sub_level andalso min_arity = max_arity - | NONE => false - -fun repair_predicates_in_term const_tab (t as ATerm ((s, _), ts)) = - if s = type_wrapper_name then - case ts of - [_, t' as ATerm ((s', _), _)] => - if is_predicate const_tab s' then t' else boolify t - | _ => raise Fail "malformed type wrapper" - else - t |> not (is_predicate const_tab s) ? boolify - -fun close_universally phi = - let - fun term_vars bounds (ATerm (name as (s, _), tms)) = - (is_variable s andalso not (member (op =) bounds name)) - ? insert (op =) name - #> fold (term_vars bounds) tms - fun formula_vars bounds (AQuant (q, xs, phi)) = - formula_vars (xs @ bounds) phi - | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis - | formula_vars bounds (APred tm) = term_vars bounds tm - in - case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi) - end - -fun repair_formula thy explicit_forall full_types const_tab = - let - fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi) - | aux (AConn (c, phis)) = AConn (c, map aux phis) - | aux (APred tm) = - APred (tm |> repair_applications_in_term thy full_types const_tab - |> repair_predicates_in_term const_tab) - in aux #> explicit_forall ? close_universally end - -fun repair_problem_line thy explicit_forall full_types const_tab - (Fof (ident, kind, phi)) = - Fof (ident, kind, repair_formula thy explicit_forall full_types const_tab phi) -fun repair_problem_with_const_table thy = - map o apsnd o map ooo repair_problem_line thy - -fun repair_problem thy explicit_forall full_types explicit_apply problem = - repair_problem_with_const_table thy explicit_forall full_types - (const_table_for_problem explicit_apply problem) problem - -fun write_tptp_file thy readable_names explicit_forall full_types explicit_apply - file (conjectures, axiom_clauses, extra_clauses, - helper_clauses, class_rel_clauses, arity_clauses) = - let - val axiom_lines = map (problem_line_for_axiom full_types) axiom_clauses - val class_rel_lines = - map problem_line_for_class_rel_clause class_rel_clauses - val arity_lines = map problem_line_for_arity_clause arity_clauses - val helper_lines = map (problem_line_for_axiom full_types) helper_clauses - val conjecture_lines = - map (problem_line_for_conjecture full_types) conjectures - val tfree_lines = problem_lines_for_free_types conjectures - (* Reordering these might or might not confuse the proof reconstruction - code or the SPASS Flotter hack. *) - val problem = - [("Relevant facts", axiom_lines), - ("Class relationships", class_rel_lines), - ("Arity declarations", arity_lines), - ("Helper facts", helper_lines), - ("Conjectures", conjecture_lines), - ("Type variables", tfree_lines)] - |> repair_problem thy explicit_forall full_types explicit_apply - val (problem, pool) = nice_problem problem (empty_name_pool readable_names) - val conjecture_offset = - length axiom_lines + length class_rel_lines + length arity_lines - + length helper_lines - val _ = File.write_list file (strings_for_problem problem) - in - (case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty, - conjecture_offset) - end - -end; diff -r 0c15b8a655cd -r dc56a9a8e19d src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue Jul 27 17:10:27 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue Jul 27 20:16:14 2010 +0200 @@ -8,7 +8,6 @@ sig val plural_s : int -> string val serial_commas : string -> string list -> string list - val timestamp : unit -> string val strip_spaces : string -> string val parse_bool_option : bool -> string -> string -> bool option val parse_time_option : string -> string -> Time.time option @@ -32,8 +31,6 @@ | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3] | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss -val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now - fun is_ident_char c = Char.isAlphaNum c orelse c = #"_" fun strip_spaces_in_list [] = ""