--- 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)
--- 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
--- 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")
--- 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)
--- 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;
--- 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;
-
--- 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
--- 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=<prover>] <lemmas> *)
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;