# HG changeset patch # User huffman # Date 1244057049 25200 # Node ID b8bdef62bfa6e65d7256332f7e3207fad93688dd # Parent 1501fc26f11b724119939497f819243872b0b2aa# Parent f2e6b6526092904b10efe66b4bdecabee7a73a64 merged diff -r 1501fc26f11b -r b8bdef62bfa6 src/HOL/Library/Reflection.thy --- a/src/HOL/Library/Reflection.thy Wed Jun 03 12:13:23 2009 -0700 +++ b/src/HOL/Library/Reflection.thy Wed Jun 03 12:24:09 2009 -0700 @@ -22,8 +22,8 @@ (fn (eqs, to) => fn ctxt => SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to)) *} "partial automatic reification" -method_setup reflection = {* -let +method_setup reflection = {* +let fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K (); val onlyN = "only"; val rulesN = "rules"; @@ -35,8 +35,8 @@ Scan.optional (keyword rulesN |-- thms) [] -- Scan.option (keyword onlyN |-- Args.term) >> (fn ((eqs,ths),to) => fn ctxt => - let - val (ceqs,cths) = Reify_Data.get ctxt + let + val (ceqs,cths) = Reify_Data.get ctxt val corr_thms = ths@cths val raw_eqs = eqs@ceqs in SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) end) diff -r 1501fc26f11b -r b8bdef62bfa6 src/HOL/Library/reflection.ML --- a/src/HOL/Library/reflection.ML Wed Jun 03 12:13:23 2009 -0700 +++ b/src/HOL/Library/reflection.ML Wed Jun 03 12:24:09 2009 -0700 @@ -76,13 +76,13 @@ exception REIF of string; -fun dest_listT (Type ("List.list", [T])) = T; +fun dest_listT (Type (@{type_name "list"}, [T])) = T; (* This modified version of divide_and_conquer allows the threading of a state variable *) -fun divide_and_conquer' decomp (s, x) = - let val (ys, recomb) = decomp (s, x) - in recomb (Library.foldl_map (divide_and_conquer' decomp) ys) end; +fun divide_and_conquer' decomp s x = + let val ((ys, recomb), s') = decomp s x + in recomb (fold_map (divide_and_conquer' decomp) ys s') end; fun rearrange congs = let @@ -94,7 +94,7 @@ fun genreif ctxt raw_eqs t = let - fun index_of bds t = + fun index_of t bds = let val tt = HOLogic.listT (fastype_of t) in @@ -106,9 +106,9 @@ val j = find_index_eq t tbs in (if j = ~1 then if i = ~1 - then (AList.update Type.could_unify (tt,(tbs,tats@[t])) bds, - length tbs + length tats) - else (bds, i) else (bds, j)) + then (length tbs + length tats, + AList.update Type.could_unify (tt,(tbs,tats@[t])) bds) + else (i, bds) else (j, bds)) end) end; @@ -121,11 +121,11 @@ (* da is the decomposition for atoms, ie. it returns ([],g) where g returns the right instance f (AtC n) = t , where AtC is the Atoms constructor and n is the number of the atom corresponding to t *) - fun decomp_genreif da cgns (bds, (t,ctxt)) = + fun decomp_genreif da cgns (t,ctxt) bds = let val thy = ProofContext.theory_of ctxt val cert = cterm_of thy - fun tryabsdecomp (bds, (s,ctxt)) = + fun tryabsdecomp (s,ctxt) bds = (case s of Abs(xn,xT,ta) => ( let @@ -136,16 +136,17 @@ of NONE => error "tryabsdecomp: Type not found in the Environement" | SOME (bsT,atsT) => (AList.update Type.could_unify (HOLogic.listT xT, ((x::bsT), atsT)) bds)) - in ((bds, [(ta, ctxt')]), - fn (bds, [th]) => ( - (let val (bsT,asT) = the(AList.lookup Type.could_unify bds (HOLogic.listT xT)) - in AList.update Type.could_unify (HOLogic.listT xT,(tl bsT,asT)) bds - end), - hd (Variable.export ctxt' ctxt [(forall_intr (cert x) th) COMP allI]))) + in (([(ta, ctxt')], + fn ([th], bds) => + (hd (Variable.export ctxt' ctxt [(forall_intr (cert x) th) COMP allI]), + let val (bsT,asT) = the(AList.lookup Type.could_unify bds (HOLogic.listT xT)) + in AList.update Type.could_unify (HOLogic.listT xT,(tl bsT,asT)) bds + end)), + bds) end) - | _ => da (bds, (s,ctxt))) + | _ => da (s,ctxt) bds) in (case cgns of - [] => tryabsdecomp (bds, (t,ctxt)) + [] => tryabsdecomp (t,ctxt) bds | ((vns,cong)::congs) => ((let val cert = cterm_of thy val certy = ctyp_of thy @@ -158,21 +159,21 @@ (map (snd o snd) fnvs, map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) invs) val ctyenv = map (fn ((vn,vi),(s,ty)) => (certy (TVar((vn,vi),s)), certy ty)) (Vartab.dest tyenv) - in ((bds, fts ~~ (replicate (length fts) ctxt)), - Library.apsnd (FWD (instantiate (ctyenv, its) cong))) + in ((fts ~~ (replicate (length fts) ctxt), + Library.apfst (FWD (instantiate (ctyenv, its) cong))), bds) end) - handle MATCH => decomp_genreif da congs (bds, (t,ctxt)))) + handle MATCH => decomp_genreif da congs (t,ctxt) bds)) end; (* looks for the atoms equation and instantiates it with the right number *) - fun mk_decompatom eqs (bds, (t,ctxt)) = ((bds, []), fn (bds, _) => + fun mk_decompatom eqs (t,ctxt) bds = (([], fn (_, bds) => let val tT = fastype_of t fun isat eq = let val rhs = eq |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd in exists_Const - (fn (n,ty) => n="List.nth" + (fn (n,ty) => n = @{const_name "List.nth"} andalso AList.defined Type.could_unify bds (domain_type ty)) rhs andalso Type.could_unify (fastype_of rhs, tT) @@ -180,14 +181,14 @@ fun get_nths t acc = case t of - Const("List.nth",_)$vs$n => insert (fn ((a,_),(b,_)) => a aconv b) (t,(vs,n)) acc + Const(@{const_name "List.nth"},_)$vs$n => insert (fn ((a,_),(b,_)) => a aconv b) (t,(vs,n)) acc | t1$t2 => get_nths t1 (get_nths t2 acc) | Abs(_,_,t') => get_nths t' acc | _ => acc fun - tryeqs bds [] = error "Can not find the atoms equation" - | tryeqs bds (eq::eqs) = (( + tryeqs [] bds = error "Can not find the atoms equation" + | tryeqs (eq::eqs) bds = (( let val rhs = eq |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd val nths = get_nths rhs [] @@ -210,22 +211,22 @@ val subst_ty = map (fn (n,(s,t)) => (certT (TVar (n, s)), certT t)) (Vartab.dest tyenv) val tml = Vartab.dest tmenv - val t's = map (fn xn => snd (valOf (AList.lookup (op =) tml (xn,0)))) xns (* FIXME : Express with sbst*) - val (bds, subst_ns) = Library.foldl_map - (fn (bds, (Const _ $ vs $ n, Var (xn0,T))) => + val t's = map (fn xn => snd (the (AList.lookup (op =) tml (xn,0)))) xns (* FIXME : Express with sbst*) + val (subst_ns, bds) = fold_map + (fn (Const _ $ vs $ n, Var (xn0,T)) => fn bds => let - val name = snd (valOf (AList.lookup (op =) tml xn0)) - val (bds, idx) = index_of bds name - in (bds, (cert n, idx |> (HOLogic.mk_nat #> cert))) end) (bds, subst) + val name = snd (the (AList.lookup (op =) tml xn0)) + val (idx, bds) = index_of name bds + in ((cert n, idx |> (HOLogic.mk_nat #> cert)), bds) end) subst bds val subst_vs = let fun ty (Const _ $ (vs as Var (vsn,lT)) $ n, Var (xn0,T)) = (certT T, certT (sbsT T)) fun h (Const _ $ (vs as Var (vsn,lT)) $ n, Var (xn0,T)) = let - val cns = sbst (Const("List.list.Cons", T --> lT --> lT)) + val cns = sbst (Const(@{const_name "List.Cons"}, T --> lT --> lT)) val lT' = sbsT lT val (bsT,asT) = the (AList.lookup Type.could_unify bds lT) - val vsn = valOf (AList.lookup (op =) vsns_map vs) + val vsn = the (AList.lookup (op =) vsns_map vs) val cvs = cert (fold_rev (fn x => fn xs => cns$x$xs) bsT (Free (vsn, lT'))) in (cert vs, cvs) end in map h subst end @@ -236,9 +237,9 @@ let val ih = Drule.cterm_rule (Thm.instantiate (subst_ty,[])) in map (fn (v,t) => (ih v, ih t)) (subst_ns@subst_vs@cts) end val th = (instantiate (subst_ty, substt) eq) RS sym - in (bds, hd (Variable.export ctxt'' ctxt [th])) end) - handle MATCH => tryeqs bds eqs) - in tryeqs bds (filter isat eqs) end); + in (hd (Variable.export ctxt'' ctxt [th]), bds) end) + handle MATCH => tryeqs eqs bds) + in tryeqs (filter isat eqs) bds end), bds); (* Generic reification procedure: *) (* creates all needed cong rules and then just uses the theorem synthesis *) @@ -259,7 +260,7 @@ val is_Var = can dest_Var fun insteq eq vs = let - val subst = map (fn (v as Var(n,t)) => (cert v, (valOf o valOf) (AList.lookup (op =) vstys t))) + val subst = map (fn (v as Var(n,t)) => (cert v, (the o the) (AList.lookup (op =) vstys t))) (filter is_Var vs) in Thm.instantiate ([],subst) eq end @@ -269,12 +270,12 @@ |> HOLogic.dest_eq |> fst |> strip_comb |> snd |> tl |> (insteq eq)) raw_eqs val (ps,congs) = split_list (map (mk_congeq ctxt' fs) eqs) - in (bds, ps ~~ (Variable.export ctxt' ctxt congs)) + in (ps ~~ (Variable.export ctxt' ctxt congs), bds) end - val (bds, congs) = mk_congs ctxt raw_eqs + val (congs, bds) = mk_congs ctxt raw_eqs val congs = rearrange congs - val (bds, th) = divide_and_conquer' (decomp_genreif (mk_decompatom raw_eqs) congs) (bds, (t,ctxt)) + val (th, bds) = divide_and_conquer' (decomp_genreif (mk_decompatom raw_eqs) congs) (t,ctxt) bds fun is_listVar (Var (_,t)) = can dest_listT t | is_listVar _ = false val vars = th |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd @@ -305,7 +306,7 @@ fun genreify_tac ctxt eqs to i = (fn st => let - fun P () = HOLogic.dest_Trueprop (List.nth (prems_of st, i - 1)) + fun P () = HOLogic.dest_Trueprop (nth (prems_of st) (i - 1)) val t = (case to of NONE => P () | SOME x => x) val th = (genreif ctxt eqs t) RS ssubst in rtac th i st diff -r 1501fc26f11b -r b8bdef62bfa6 src/HOL/Tools/atp_manager.ML --- a/src/HOL/Tools/atp_manager.ML Wed Jun 03 12:13:23 2009 -0700 +++ b/src/HOL/Tools/atp_manager.ML Wed Jun 03 12:24:09 2009 -0700 @@ -19,8 +19,10 @@ val kill: unit -> unit val info: unit -> unit val messages: int option -> unit - type prover = int -> (thm * (string * int)) list option -> string -> int -> - Proof.context * (thm list * thm) -> bool * string * string * string vector + type prover = int -> (thm * (string * int)) list option -> + (int Symtab.table * bool Symtab.table) option -> string -> int -> + Proof.context * (thm list * thm) -> + bool * string * string * string vector * (int Symtab.table * bool Symtab.table) val add_prover: string -> prover -> theory -> theory val print_provers: theory -> unit val get_prover: string -> theory -> prover option @@ -289,8 +291,10 @@ (* named provers *) -type prover = int -> (thm * (string * int)) list option -> string -> int -> - Proof.context * (thm list * thm) -> bool * string * string * string vector +type prover = int -> (thm * (string * int)) list option -> + (int Symtab.table * bool Symtab.table) option -> string -> int -> + Proof.context * (thm list * thm) -> + bool * string * string * string vector * (int Symtab.table * bool Symtab.table) fun err_dup_prover name = error ("Duplicate prover: " ^ quote name); @@ -330,8 +334,8 @@ let val _ = register birthtime deadtime (Thread.self (), desc) val result = - let val (success, message, _, _) = - prover (get_timeout ()) NONE name i (Proof.get_goal proof_state) + let val (success, message, _, _, _) = + prover (get_timeout ()) NONE NONE name i (Proof.get_goal proof_state) in (success, message) end handle ResHolClause.TOO_TRIVIAL => (true, "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis") diff -r 1501fc26f11b -r b8bdef62bfa6 src/HOL/Tools/atp_minimal.ML --- a/src/HOL/Tools/atp_minimal.ML Wed Jun 03 12:13:23 2009 -0700 +++ b/src/HOL/Tools/atp_minimal.ML Wed Jun 03 12:24:09 2009 -0700 @@ -83,9 +83,9 @@ ("# Cannot determine problem status within resource limit", Timeout), ("Error", Error)] -fun produce_answer (success, message, result_string, thm_name_vec) = +fun produce_answer (success, message, result_string, thm_name_vec, const_counts) = if success then - (Success (Vector.foldr op:: [] thm_name_vec), result_string) + (Success (Vector.foldr op:: [] thm_name_vec, const_counts), result_string) else let val failure = failure_strings |> get_first (fn (s, t) => @@ -100,7 +100,7 @@ (* wrapper for calling external prover *) -fun sh_test_thms prover prover_name time_limit subgoalno state name_thms_pairs = +fun sh_test_thms prover prover_name time_limit subgoalno state counts name_thms_pairs = let val _ = println ("Testing " ^ (length_string name_thms_pairs) ^ " theorems... ") val name_thm_pairs = @@ -108,7 +108,8 @@ val _ = debug_fn (fn () => print_names name_thm_pairs) val axclauses = ResAxioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs val (result, proof) = - produce_answer (prover time_limit (SOME axclauses) prover_name subgoalno (Proof.get_goal state)) + produce_answer + (prover time_limit (SOME axclauses) counts prover_name subgoalno (Proof.get_goal state)) val _ = println (string_of_result result) val _ = debug proof in @@ -126,11 +127,11 @@ val _ = debug_fn (fn () => app (fn (n, tl) => (debug n; app (fn t => debug (" " ^ Display.string_of_thm t)) tl)) name_thms_pairs) val test_thms_fun = sh_test_thms prover prover_name time_limit 1 state - fun test_thms thms = case test_thms_fun thms of (Success _, _) => true | _ => false + fun test_thms counts thms = case test_thms_fun counts thms of (Success _, _) => true | _ => false in (* try prove first to check result and get used theorems *) - (case test_thms_fun name_thms_pairs of - (Success used, _) => + (case test_thms_fun NONE name_thms_pairs of + (Success (used, const_counts), _) => let val ordered_used = order_unique used val to_use = @@ -138,7 +139,7 @@ filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs else name_thms_pairs - val min_thms = minimal test_thms to_use + val min_thms = (minimal (test_thms (SOME const_counts)) to_use) val min_names = order_unique (map fst min_thms) val _ = println ("Minimal " ^ (length_string min_thms) ^ " theorems") val _ = debug_fn (fn () => print_names min_thms) diff -r 1501fc26f11b -r b8bdef62bfa6 src/HOL/Tools/atp_wrapper.ML --- a/src/HOL/Tools/atp_wrapper.ML Wed Jun 03 12:13:23 2009 -0700 +++ b/src/HOL/Tools/atp_wrapper.ML Wed Jun 03 12:24:09 2009 -0700 @@ -8,12 +8,6 @@ sig val destdir: string ref val problem_name: string ref - val external_prover: - (unit -> (thm * (string * int)) list) -> - (Path.T -> thm -> int -> (thm * (string * int)) list -> theory -> string vector) -> - Path.T * string -> (string -> string option) -> - (string -> string * string vector * Proof.context * thm * int -> string) -> - AtpManager.prover val tptp_prover_opts_full: int -> bool -> bool -> Path.T * string -> AtpManager.prover val tptp_prover_opts: int -> bool -> Path.T * string -> AtpManager.prover val tptp_prover: Path.T * string -> AtpManager.prover @@ -46,8 +40,8 @@ (* basic template *) -fun external_prover relevance_filter write_problem_file (cmd, args) find_failure produce_answer - timeout axiom_clauses name subgoalno goal = +fun external_prover relevance_filter preparer writer (cmd, args) find_failure produce_answer + timeout axiom_clauses const_counts name subgoalno goal = let (* path to unique problem file *) val destdir' = ! destdir @@ -66,8 +60,24 @@ val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths val probfile = prob_pathname subgoalno val fname = File.platform_path probfile - val the_ax_clauses = case axiom_clauses of NONE => relevance_filter () | SOME axcls => axcls - val thm_names = write_problem_file probfile th subgoalno the_ax_clauses thy + val goal_cls = #1 (ResAxioms.neg_conjecture_clauses th subgoalno) + handle THM ("assume: variables", _, _) => + error "Sledgehammer: Goal contains type variables (TVars)" + val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) goal_cls + val the_axiom_clauses = + case axiom_clauses of + NONE => relevance_filter goal goal_cls + | SOME axcls => axcls + val (thm_names, clauses) = preparer goal_cls chain_ths the_axiom_clauses thy + val the_const_counts = case const_counts of + NONE => + ResHolClause.count_constants( + case axiom_clauses of + NONE => clauses + | SOME axcls => #2(preparer goal_cls chain_ths (relevance_filter goal goal_cls) thy) + ) + | SOME ccs => ccs + val _ = writer fname the_const_counts clauses val cmdline = if File.exists cmd then "exec " ^ File.shell_path cmd ^ " " ^ args else error ("Bad executable: " ^ Path.implode cmd) @@ -83,16 +93,8 @@ if is_some failure then "External prover failed." else if rc <> 0 then "External prover failed: " ^ proof else "Try this command: " ^ produce_answer name (proof, thm_names, ctxt, th, subgoalno) - - val _ = - if is_some failure - then Output.debug (fn () => "Sledgehammer failure: " ^ the failure ^ "\nOutput: " ^ proof) - else () - val _ = - if rc <> 0 - then Output.debug (fn () => "Sledgehammer exited with return code " ^ string_of_int rc ^ ":\n" ^ proof) - else () - in (success, message, proof, thm_names) end; + val _ = Output.debug (fn () => "Sledgehammer response (rc = " ^ string_of_int rc ^ "):\n" ^ proof) + in (success, message, proof, thm_names, the_const_counts) end; @@ -100,14 +102,15 @@ (* generic TPTP-based provers *) -fun tptp_prover_opts_full max_new theory_const full command timeout ax_clauses name n goal = +fun tptp_prover_opts_full max_new theory_const full command timeout ax_clauses ccs name n goal = external_prover - (fn () => ResAtp.get_relevant max_new theory_const goal n) - (ResAtp.write_problem_file false) - command - ResReconstruct.find_failure - (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp) - timeout ax_clauses name n goal; + (ResAtp.get_relevant max_new theory_const) + (ResAtp.prepare_clauses false) + (ResHolClause.tptp_write_file) + command + ResReconstruct.find_failure + (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp) + timeout ax_clauses ccs name n goal; (*arbitrary ATP with TPTP input/output and problemfile as last argument*) fun tptp_prover_opts max_new theory_const = @@ -164,14 +167,15 @@ (* SPASS *) -fun spass_opts max_new theory_const timeout ax_clauses name n goal = external_prover - (fn () => ResAtp.get_relevant max_new theory_const goal n) - (ResAtp.write_problem_file true) +fun spass_opts max_new theory_const timeout ax_clauses ccs name n goal = external_prover + (ResAtp.get_relevant max_new theory_const) + (ResAtp.prepare_clauses true) + ResHolClause.dfg_write_file (Path.explode "$SPASS_HOME/SPASS", "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof -TimeLimit=" ^ string_of_int timeout) ResReconstruct.find_failure ResReconstruct.lemma_list_dfg - timeout ax_clauses name n goal; + timeout ax_clauses ccs name n goal; val spass = spass_opts 40 true; diff -r 1501fc26f11b -r b8bdef62bfa6 src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Wed Jun 03 12:13:23 2009 -0700 +++ b/src/HOL/Tools/res_atp.ML Wed Jun 03 12:24:09 2009 -0700 @@ -6,10 +6,12 @@ val tvar_classes_of_terms : term list -> string list val tfree_classes_of_terms : term list -> string list val type_consts_of_terms : theory -> term list -> string list - val get_relevant : int -> bool -> Proof.context * (thm list * thm) -> int - -> (thm * (string * int)) list - val write_problem_file : bool -> Path.T -> thm -> int -> (thm * (string * int)) list -> theory - -> string vector + val get_relevant : int -> bool -> Proof.context * (thm list * 'a) -> thm list -> + (thm * (string * int)) list + val prepare_clauses : bool -> thm list -> thm list -> + (thm * (ResHolClause.axiom_name * ResHolClause.clause_id)) list -> theory -> + ResHolClause.axiom_name vector * (ResHolClause.clause list * ResHolClause.clause list * + ResHolClause.clause list * ResClause.classrelClause list * ResClause.arityClause list) end; structure ResAtp: RES_ATP = @@ -401,23 +403,20 @@ fun display_thm (name,th) = Output.debug (fn () => name ^ ": " ^ Display.string_of_thm th); (* get lemmas from claset, simpset, atpset and extra supplied rules *) -fun get_clasimp_atp_lemmas ctxt user_thms = +fun get_clasimp_atp_lemmas ctxt = let val included_thms = - if include_all - then (tap (fn ths => Output.debug - (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems"))) - (name_thm_pairs ctxt)) - else - let val atpset_thms = - if include_atpset then ResAxioms.atpset_rules_of ctxt - else [] - val _ = (Output.debug (fn () => "ATP theorems: "); app display_thm atpset_thms) - in atpset_thms end - val user_rules = filter check_named - (map ResAxioms.pairname - (if null user_thms then whitelist else user_thms)) + if include_all + then (tap (fn ths => Output.debug + (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems"))) + (name_thm_pairs ctxt)) + else + let val atpset_thms = + if include_atpset then ResAxioms.atpset_rules_of ctxt + else [] + val _ = (Output.debug (fn () => "ATP theorems: "); app display_thm atpset_thms) + in atpset_thms end in - (filter check_named included_thms, user_rules) + filter check_named included_thms end; (***************************************************************) @@ -516,31 +515,23 @@ | Fol => true | Hol => false -fun get_relevant max_new theory_const (ctxt, (chain_ths, th)) n = +fun get_relevant max_new theory_const (ctxt, (chain_ths, th)) goal_cls = let val thy = ProofContext.theory_of ctxt - val goal_cls = #1 (ResAxioms.neg_conjecture_clauses th n) - handle THM ("assume: variables", _, _) => - error "Sledgehammer: Goal contains type variables (TVars)" - val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt chain_ths + val included_thms = get_clasimp_atp_lemmas ctxt val included_cls = included_thms |> ResAxioms.cnf_rules_pairs thy |> make_unique |> restrict_to_logic thy (isFO thy goal_cls) |> remove_unwanted_clauses - val white_cls = ResAxioms.cnf_rules_pairs thy white_thms - (*clauses relevant to goal gl*) in - white_cls @ relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls) + relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls) end; -(* Write out problem file *) -fun write_problem_file dfg probfile goal n axcls thy = - let val writer = if dfg then ResHolClause.dfg_write_file else ResHolClause.tptp_write_file - val fname = File.platform_path probfile - val axcls = make_unique axcls - val goal_cls = #1 (ResAxioms.neg_conjecture_clauses goal n) - handle THM ("assume: variables", _, _) => - error "Sledgehammer: Goal contains type variables (TVars)" - val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) goal_cls +(* prepare and count clauses before writing *) +fun prepare_clauses dfg goal_cls chain_ths axcls thy = + let + val white_thms = filter check_named (map ResAxioms.pairname (if null chain_ths then whitelist else chain_ths)) + val white_cls = ResAxioms.cnf_rules_pairs thy white_thms + val axcls = white_cls @ axcls val ccls = subtract_cls goal_cls axcls val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) ccls val ccltms = map prop_of ccls @@ -549,13 +540,13 @@ and supers = tvar_classes_of_terms axtms and tycons = type_consts_of_terms thy (ccltms@axtms) (*TFrees in conjecture clauses; TVars in axiom clauses*) + val (clnames, (conjectures, axiom_clauses, helper_clauses)) = + ResHolClause.prepare_clauses dfg thy (isFO thy goal_cls) ccls axcls [] val (supers',arity_clauses) = ResClause.make_arity_clauses_dfg dfg thy tycons supers val classrel_clauses = ResClause.make_classrel_clauses thy subs supers' - val clnames = writer thy (isFO thy goal_cls) ccls fname (axcls,classrel_clauses,arity_clauses) [] in - Vector.fromList clnames - end; + (Vector.fromList clnames, (conjectures, axiom_clauses, helper_clauses, classrel_clauses, arity_clauses)) + end end; - diff -r 1501fc26f11b -r b8bdef62bfa6 src/HOL/Tools/res_hol_clause.ML --- a/src/HOL/Tools/res_hol_clause.ML Wed Jun 03 12:13:23 2009 -0700 +++ b/src/HOL/Tools/res_hol_clause.ML Wed Jun 03 12:24:09 2009 -0700 @@ -23,15 +23,19 @@ | CombVar of string * ResClause.fol_type | CombApp of combterm * combterm datatype literal = Literal of polarity * combterm + datatype clause = Clause of {clause_id: clause_id, axiom_name: axiom_name, th: thm, + kind: ResClause.kind,literals: literal list, ctypes_sorts: typ list} val strip_comb: combterm -> combterm * combterm list val literals_of_term: theory -> term -> literal list * typ list exception TOO_TRIVIAL - val tptp_write_file: theory -> bool -> thm list -> string -> - (thm * (axiom_name * clause_id)) list * ResClause.classrelClause list * - ResClause.arityClause list -> string list -> axiom_name list - val dfg_write_file: theory -> bool -> thm list -> string -> - (thm * (axiom_name * clause_id)) list * ResClause.classrelClause list * - ResClause.arityClause list -> string list -> axiom_name list + val count_constants: clause list * clause list * clause list * 'a * 'b -> + int Symtab.table * bool Symtab.table + val prepare_clauses: bool -> theory -> bool -> thm list -> (thm * (axiom_name * clause_id)) list -> + string list -> axiom_name list * (clause list * clause list * clause list) + val tptp_write_file: string -> int Symtab.table * bool Symtab.table -> + clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list -> unit + val dfg_write_file: string -> int Symtab.table * bool Symtab.table -> + clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list -> unit end structure ResHolClause: RES_HOL_CLAUSE = @@ -294,7 +298,7 @@ (map (tptp_literal cma cnh) literals, map (RC.tptp_of_typeLit pos) (RC.add_typs ctypes_sorts)); -fun clause2tptp cma cnh (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) = +fun clause2tptp (cma, cnh) (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) = let val (lits,tylits) = tptp_type_lits cma cnh (kind = RC.Conjecture) cls in (RC.gen_tptp_cls(clause_id,axiom_name,kind,lits,tylits), tylits) @@ -317,7 +321,7 @@ fun dfg_vars (Clause {literals,...}) = RC.union_all (map get_uvars_l literals); -fun clause2dfg cma cnh (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) = +fun clause2dfg (cma, cnh) (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) = let val (lits,tylits) = dfg_type_lits cma cnh (kind = RC.Conjecture) cls val vars = dfg_vars cls val tvars = RC.get_tvar_strs ctypes_sorts @@ -350,7 +354,7 @@ List.foldl (add_literal_decls cma cnh) decls literals handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities") -fun decls_of_clauses cma cnh clauses arity_clauses = +fun decls_of_clauses (cma, cnh) clauses arity_clauses = let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) RC.init_functab) val init_predtab = Symtab.update ("hBOOL",1) Symtab.empty val (functab,predtab) = (List.foldl (add_clause_decls cma cnh) (init_functab, init_predtab) clauses) @@ -448,7 +452,7 @@ Output.debug (fn () => "Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^ (if needs_hBOOL const_needs_hBOOL c then " needs hBOOL" else "")); -fun count_constants (conjectures, axclauses, helper_clauses) = +fun count_constants (conjectures, axclauses, helper_clauses, _, _) = if minimize_applies then let val (const_min_arity, const_needs_hBOOL) = fold count_constants_clause conjectures (Symtab.empty, Symtab.empty) @@ -460,64 +464,63 @@ (* tptp format *) +fun prepare_clauses dfg thy isFO thms ax_tuples user_lemmas = + let + val conjectures = make_conjecture_clauses dfg thy thms + val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses dfg thy ax_tuples) + val helper_clauses = get_helper_clauses dfg thy isFO (conjectures, axclauses, user_lemmas) + in + (clnames, (conjectures, axclauses, helper_clauses)) + end + (* write TPTP format to a single file *) -fun tptp_write_file thy isFO thms filename (ax_tuples,classrel_clauses,arity_clauses) user_lemmas = - let val _ = Output.debug (fn () => ("Preparing to write the TPTP file " ^ filename)) - val conjectures = make_conjecture_clauses false thy thms - val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses false thy ax_tuples) - val helper_clauses = get_helper_clauses false thy isFO (conjectures, axclauses, user_lemmas) - val (const_min_arity, const_needs_hBOOL) = count_constants (conjectures, axclauses, helper_clauses); - val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp const_min_arity const_needs_hBOOL) conjectures) - val tfree_clss = map RC.tptp_tfree_clause (List.foldl (op union_string) [] tfree_litss) - val out = TextIO.openOut filename - in - List.app (curry TextIO.output out o #1 o (clause2tptp const_min_arity const_needs_hBOOL)) axclauses; - RC.writeln_strs out tfree_clss; - RC.writeln_strs out tptp_clss; - List.app (curry TextIO.output out o RC.tptp_classrelClause) classrel_clauses; - List.app (curry TextIO.output out o RC.tptp_arity_clause) arity_clauses; - List.app (curry TextIO.output out o #1 o (clause2tptp const_min_arity const_needs_hBOOL)) helper_clauses; - TextIO.closeOut out; - clnames - end; +fun tptp_write_file filename const_counts (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) = + let + val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp const_counts) conjectures) + val tfree_clss = map RC.tptp_tfree_clause (List.foldl (op union_string) [] tfree_litss) + val out = TextIO.openOut filename + in + List.app (curry TextIO.output out o #1 o (clause2tptp const_counts)) axclauses; + RC.writeln_strs out tfree_clss; + RC.writeln_strs out tptp_clss; + List.app (curry TextIO.output out o RC.tptp_classrelClause) classrel_clauses; + List.app (curry TextIO.output out o RC.tptp_arity_clause) arity_clauses; + List.app (curry TextIO.output out o #1 o (clause2tptp const_counts)) helper_clauses; + TextIO.closeOut out + end; (* dfg format *) -fun dfg_write_file thy isFO thms filename (ax_tuples,classrel_clauses,arity_clauses) user_lemmas = - let val _ = Output.debug (fn () => ("Preparing to write the DFG file " ^ filename)) - val conjectures = make_conjecture_clauses true thy thms - val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses true thy ax_tuples) - val helper_clauses = get_helper_clauses true thy isFO (conjectures, axclauses, user_lemmas) - val (const_min_arity, const_needs_hBOOL) = count_constants (conjectures, axclauses, helper_clauses); - val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg const_min_arity const_needs_hBOOL) conjectures) - and probname = Path.implode (Path.base (Path.explode filename)) - val axstrs = map (#1 o (clause2dfg const_min_arity const_needs_hBOOL)) axclauses - val tfree_clss = map RC.dfg_tfree_clause (RC.union_all tfree_litss) - val out = TextIO.openOut filename - val helper_clauses_strs = map (#1 o (clause2dfg const_min_arity const_needs_hBOOL)) helper_clauses - val (funcs,cl_preds) = decls_of_clauses const_min_arity const_needs_hBOOL (helper_clauses @ conjectures @ axclauses) arity_clauses - and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses - in - TextIO.output (out, RC.string_of_start probname); - TextIO.output (out, RC.string_of_descrip probname); - TextIO.output (out, RC.string_of_symbols - (RC.string_of_funcs funcs) - (RC.string_of_preds (cl_preds @ ty_preds))); - TextIO.output (out, "list_of_clauses(axioms,cnf).\n"); - RC.writeln_strs out axstrs; - List.app (curry TextIO.output out o RC.dfg_classrelClause) classrel_clauses; - List.app (curry TextIO.output out o RC.dfg_arity_clause) arity_clauses; - RC.writeln_strs out helper_clauses_strs; - TextIO.output (out, "end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n"); - RC.writeln_strs out tfree_clss; - RC.writeln_strs out dfg_clss; - TextIO.output (out, "end_of_list.\n\n"); - (*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*) - TextIO.output (out, "list_of_settings(SPASS).\n{*\nset_flag(VarWeight,3).\n*}\nend_of_list.\n\n"); - TextIO.output (out, "end_problem.\n"); - TextIO.closeOut out; - clnames - end; +fun dfg_write_file filename const_counts (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) = + let + val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg const_counts) conjectures) + and probname = Path.implode (Path.base (Path.explode filename)) + val axstrs = map (#1 o (clause2dfg const_counts)) axclauses + val tfree_clss = map RC.dfg_tfree_clause (RC.union_all tfree_litss) + val out = TextIO.openOut filename + val helper_clauses_strs = map (#1 o (clause2dfg const_counts)) helper_clauses + val (funcs,cl_preds) = decls_of_clauses const_counts (helper_clauses @ conjectures @ axclauses) arity_clauses + and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses + in + TextIO.output (out, RC.string_of_start probname); + TextIO.output (out, RC.string_of_descrip probname); + TextIO.output (out, RC.string_of_symbols + (RC.string_of_funcs funcs) + (RC.string_of_preds (cl_preds @ ty_preds))); + TextIO.output (out, "list_of_clauses(axioms,cnf).\n"); + RC.writeln_strs out axstrs; + List.app (curry TextIO.output out o RC.dfg_classrelClause) classrel_clauses; + List.app (curry TextIO.output out o RC.dfg_arity_clause) arity_clauses; + RC.writeln_strs out helper_clauses_strs; + TextIO.output (out, "end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n"); + RC.writeln_strs out tfree_clss; + RC.writeln_strs out dfg_clss; + TextIO.output (out, "end_of_list.\n\n"); + (*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*) + TextIO.output (out, "list_of_settings(SPASS).\n{*\nset_flag(VarWeight,3).\n*}\nend_of_list.\n\n"); + TextIO.output (out, "end_problem.\n"); + TextIO.closeOut out + end; end diff -r 1501fc26f11b -r b8bdef62bfa6 src/HOL/Tools/res_reconstruct.ML --- a/src/HOL/Tools/res_reconstruct.ML Wed Jun 03 12:13:23 2009 -0700 +++ b/src/HOL/Tools/res_reconstruct.ML Wed Jun 03 12:24:09 2009 -0700 @@ -528,6 +528,10 @@ in get_axiom_names thm_names (get_step_nums proofextract) end; + + (*Used to label theorems chained into the sledgehammer call*) + val chained_hint = "CHAINED"; + val nochained = filter_out (fn y => y = chained_hint) (* metis-command *) fun metis_line [] = "apply metis" @@ -536,13 +540,11 @@ (* atp_minimize [atp=] *) fun minimize_line _ [] = "" | minimize_line name lemmas = "For minimizing the number of lemmas try this command:\n" ^ - (Markup.markup Markup.sendback) ("atp_minimize [atp=" ^ name ^ "] " ^ space_implode " " lemmas) + (Markup.markup Markup.sendback) ("atp_minimize [atp=" ^ name ^ "] " ^ + space_implode " " (nochained lemmas)) - (*Used to label theorems chained into the sledgehammer call*) - val chained_hint = "CHAINED"; fun sendback_metis_nochained lemmas = - let val nochained = filter_out (fn y => y = chained_hint) - in (Markup.markup Markup.sendback o metis_line) (nochained lemmas) end + (Markup.markup Markup.sendback o metis_line) (nochained lemmas) fun lemma_list_tstp name result = let val lemmas = extract_lemmas get_step_nums_tstp result in sendback_metis_nochained lemmas ^ "\n" ^ minimize_line name lemmas end;