--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon May 17 08:45:46 2010 -0700
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon May 17 12:00:10 2010 -0700
@@ -34,8 +34,8 @@
axiom_clauses: (thm * (string * int)) list option,
filtered_clauses: (thm * (string * int)) list option}
datatype failure =
- Unprovable | TimedOut | OutOfResources | OldSpass | MalformedOutput |
- UnknownError
+ Unprovable | TimedOut | OutOfResources | OldSpass | MalformedInput |
+ MalformedOutput | UnknownError
type prover_result =
{outcome: failure option,
message: string,
@@ -95,8 +95,8 @@
filtered_clauses: (thm * (string * int)) list option};
datatype failure =
- Unprovable | TimedOut | OutOfResources | OldSpass | MalformedOutput |
- UnknownError
+ Unprovable | TimedOut | OutOfResources | OldSpass | MalformedInput |
+ MalformedOutput | UnknownError
type prover_result =
{outcome: failure option,
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Mon May 17 08:45:46 2010 -0700
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Mon May 17 12:00:10 2010 -0700
@@ -100,6 +100,9 @@
(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."
@@ -336,7 +339,8 @@
known_failures =
[(Unprovable, "SPASS beiseite: Completion found"),
(TimedOut, "SPASS beiseite: Ran out of time"),
- (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded")],
+ (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
+ (MalformedInput, "Undefined symbol")],
max_axiom_clauses = 40,
prefers_theory_relevant = true}
val spass = dfg_prover "spass" spass_config
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon May 17 08:45:46 2010 -0700
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon May 17 12:00:10 2010 -0700
@@ -141,9 +141,10 @@
in
if is_conjecture then
(Metis.Thm.axiom (Metis.LiteralSet.fromList mlits),
- add_type_literals types_sorts)
+ type_literals_for_types types_sorts)
else
- let val tylits = add_type_literals (filter (not o default_sort ctxt) types_sorts)
+ let val tylits = filter_out (default_sort ctxt) types_sorts
+ |> type_literals_for_types
val mtylits = if Config.get ctxt type_lits
then map (metis_of_type_literals false) tylits else []
in
@@ -216,6 +217,8 @@
fun strip_happ args (Metis.Term.Fn(".",[t,u])) = strip_happ (u::args) t
| strip_happ args x = (x, args);
+fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
+
fun fol_type_to_isa _ (Metis.Term.Var v) =
(case strip_prefix tvar_prefix v of
SOME w => make_tvar w
@@ -599,9 +602,9 @@
(*Extract TFree constraints from context to include as conjecture clauses*)
fun init_tfrees ctxt =
- let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts
- in
- add_type_literals (Vartab.fold add (#2 (Variable.constraints_of ctxt)) [])
+ let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts in
+ Vartab.fold add (#2 (Variable.constraints_of ctxt)) []
+ |> type_literals_for_types
end;
(*transform isabelle type / arity clause to metis clause *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon May 17 08:45:46 2010 -0700
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon May 17 12:00:10 2010 -0700
@@ -352,7 +352,7 @@
fun subtract_cls ax_clauses =
filter_out (Termtab.defined (mk_clause_table ax_clauses) o prop_of)
-fun all_valid_thms respect_no_atp ctxt =
+fun all_valid_thms respect_no_atp ctxt chain_ths =
let
val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt);
val local_facts = ProofContext.facts_of ctxt;
@@ -371,7 +371,8 @@
val name2 = Name_Space.extern full_space name;
val ths = filter_out bad_for_atp ths0;
in
- if Facts.is_concealed facts name orelse null ths orelse
+ if Facts.is_concealed facts name orelse
+ forall (member Thm.eq_thm chain_ths) ths orelse
(respect_no_atp andalso is_package_def name) then
I
else case find_first check_thms [name1, name2, name] of
@@ -396,10 +397,10 @@
(* The single-name theorems go after the multiple-name ones, so that single
names are preferred when both are available. *)
-fun name_thm_pairs respect_no_atp ctxt =
+fun name_thm_pairs respect_no_atp ctxt chain_ths =
let
val (mults, singles) =
- List.partition is_multi (all_valid_thms respect_no_atp ctxt)
+ List.partition is_multi (all_valid_thms respect_no_atp ctxt chain_ths)
val ps = [] |> fold add_single_names singles
|> fold add_multi_names mults
in ps |> respect_no_atp ? filter_out (No_ATPs.member ctxt o snd) end;
@@ -408,11 +409,11 @@
(warning ("No name for theorem " ^ Display.string_of_thm_without_context th); false)
| check_named _ = true;
-fun get_all_lemmas respect_no_atp ctxt =
+fun get_all_lemmas respect_no_atp ctxt chain_ths =
let val included_thms =
tap (fn ths => trace_msg
(fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems")))
- (name_thm_pairs respect_no_atp ctxt)
+ (name_thm_pairs respect_no_atp ctxt chain_ths)
in
filter check_named included_thms
end;
@@ -509,14 +510,14 @@
fun get_relevant_facts respect_no_atp relevance_threshold relevance_convergence
defs_relevant max_new theory_relevant
(relevance_override as {add, only, ...})
- (ctxt, (chain_ths, th)) goal_cls =
+ (ctxt, (chain_ths, _)) goal_cls =
if (only andalso null add) orelse relevance_threshold > 1.0 then
[]
else
let
val thy = ProofContext.theory_of ctxt
val is_FO = is_first_order thy goal_cls
- val included_cls = get_all_lemmas respect_no_atp ctxt
+ val included_cls = get_all_lemmas respect_no_atp ctxt chain_ths
|> cnf_rules_pairs thy |> make_unique
|> restrict_to_logic thy is_FO
|> remove_unwanted_clauses
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Mon May 17 08:45:46 2010 -0700
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Mon May 17 12:00:10 2010 -0700
@@ -48,7 +48,7 @@
TyLitVar of string * name |
TyLitFree of string * name
exception CLAUSE of string * term
- val add_type_literals : typ list -> type_literal list
+ val type_literals_for_types : typ list -> type_literal list
val get_tvar_strs: typ list -> string list
datatype arLit =
TConsLit of class * string * string list
@@ -331,7 +331,8 @@
| pred_of_sort (TyLitFree (s, _)) = (s, 1)
(*Given a list of sorted type variables, return a list of type literals.*)
-fun add_type_literals Ts = fold (union (op =)) (map sorts_on_typs Ts) []
+fun type_literals_for_types Ts =
+ fold (union (op =)) (map sorts_on_typs Ts) []
(*The correct treatment of TFrees like 'a in lemmas (axiom clauses) is not clear.
* Ignoring them leads to unsound proofs, since we do nothing to ensure that 'a
@@ -520,7 +521,7 @@
dfg_forall vars ("or(" ^ commas lits ^ ")") ^ ",\n" ^
string_of_clausename (cls_id,ax_name) ^ ").\n\n";
-fun string_of_arity (name, num) = "(" ^ name ^ "," ^ Int.toString num ^ ")"
+fun string_of_arity (name, arity) = "(" ^ name ^ ", " ^ Int.toString arity ^ ")"
fun string_of_preds [] = ""
| string_of_preds preds = "predicates[" ^ commas(map string_of_arity preds) ^ "].\n";
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Mon May 17 08:45:46 2010 -0700
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Mon May 17 12:00:10 2010 -0700
@@ -300,7 +300,7 @@
let
val (lits, pool) = pool_map (tptp_literal params) literals pool
val (tylits, pool) = pool_map (tptp_of_type_literal pos)
- (add_type_literals ctypes_sorts) pool
+ (type_literals_for_types ctypes_sorts) pool
in ((lits, tylits), pool) end
fun tptp_clause params (cls as HOLClause {axiom_name, clause_id, kind, ...})
@@ -320,7 +320,8 @@
fun dfg_type_literals params pos (HOLClause {literals, ctypes_sorts, ...}) =
pool_map (dfg_literal params) literals
- #>> rpair (map (dfg_of_type_literal pos) (add_type_literals ctypes_sorts))
+ #>> rpair (map (dfg_of_type_literal pos)
+ (type_literals_for_types ctypes_sorts))
fun get_uvars (CombConst _) vars pool = (vars, pool)
| get_uvars (CombVar (name, _)) vars pool =
@@ -531,6 +532,8 @@
(* DFG format *)
+fun dfg_tfree_predicate s = (first_field "(" s |> the |> fst, 1)
+
fun write_dfg_file full_types explicit_apply file clauses =
let
(* Some of the helper functions below are not name-pool-aware. However,
@@ -543,13 +546,16 @@
val params = (full_types, explicit_apply, cma, cnh)
val ((conjecture_clss, tfree_litss), pool) =
pool_map (dfg_clause params) conjectures pool |>> ListPair.unzip
- and problem_name = Path.implode (Path.base file)
+ val tfree_lits = union_all tfree_litss
+ val problem_name = Path.implode (Path.base file)
val (axstrs, pool) = pool_map (apfst fst oo dfg_clause params) axclauses pool
- val tfree_clss = map dfg_tfree_clause (union_all tfree_litss)
+ val tfree_clss = map dfg_tfree_clause tfree_lits
+ val tfree_preds = map dfg_tfree_predicate tfree_lits
val (helper_clauses_strs, pool) =
pool_map (apfst fst oo dfg_clause params) helper_clauses pool
val (funcs, cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses
- and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
+ val ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
+ val preds = tfree_preds @ cl_preds @ ty_preds
val conjecture_offset =
length axclauses + length classrel_clauses + length arity_clauses
+ length helper_clauses
@@ -559,7 +565,7 @@
string_of_start problem_name ::
string_of_descrip problem_name ::
string_of_symbols (string_of_funcs funcs)
- (string_of_preds (cl_preds @ ty_preds)) ::
+ (string_of_preds preds) ::
"list_of_clauses(axioms, cnf).\n" ::
axstrs @
map dfg_classrel_clause classrel_clauses @
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon May 17 08:45:46 2010 -0700
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon May 17 12:00:10 2010 -0700
@@ -14,7 +14,6 @@
val invert_const: string -> string
val invert_type_const: string -> string
val num_type_args: theory -> string -> int
- val make_tvar: string -> typ
val strip_prefix: string -> string -> string option
val metis_line: int -> int -> string list -> string
val metis_proof_text:
@@ -235,26 +234,27 @@
SOME c' => c'
| NONE => c;
-fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS);
-fun make_tparam s = TypeInfer.param 0 (s, HOLogic.typeS)
-fun make_var (b,T) = Var((b,0),T);
-
(* Type variables are given the basic sort "HOL.type". Some will later be
constrained by information from type literals, or by type inference. *)
-fun type_from_node (u as IntLeaf _) = raise NODE [u]
- | type_from_node (u as StrNode (a, us)) =
- let val Ts = map type_from_node us in
+fun type_from_node _ (u as IntLeaf _) = raise NODE [u]
+ | type_from_node tfrees (u as StrNode (a, us)) =
+ let val Ts = map (type_from_node tfrees) us in
case strip_prefix tconst_prefix a of
SOME b => Type (invert_type_const b, Ts)
| NONE =>
if not (null us) then
raise NODE [u] (* only "tconst"s have type arguments *)
else case strip_prefix tfree_prefix a of
- SOME b => TFree ("'" ^ b, HOLogic.typeS)
+ SOME b =>
+ let val s = "'" ^ b in
+ TFree (s, AList.lookup (op =) tfrees s |> the_default HOLogic.typeS)
+ end
| NONE =>
case strip_prefix tvar_prefix a of
- SOME b => make_tvar b
- | NONE => make_tparam a (* Variable from the ATP, say "X1" *)
+ SOME b => TVar (("'" ^ b, 0), HOLogic.typeS)
+ | NONE =>
+ (* Variable from the ATP, say "X1" *)
+ TypeInfer.param 0 (a, HOLogic.typeS)
end
(*Invert the table of translations between Isabelle and ATPs*)
@@ -287,7 +287,7 @@
(* First-order translation. No types are known for variables. "HOLogic.typeT"
should allow them to be inferred.*)
-fun term_from_node thy full_types =
+fun term_from_node thy full_types tfrees =
let
fun aux opt_T args u =
case u of
@@ -298,7 +298,8 @@
| StrNode (a, us) =>
if a = type_wrapper_name then
case us of
- [term_u, typ_u] => aux (SOME (type_from_node typ_u)) args term_u
+ [term_u, typ_u] =>
+ aux (SOME (type_from_node tfrees typ_u)) args term_u
| _ => raise NODE us
else case strip_prefix const_prefix a of
SOME "equal" =>
@@ -324,7 +325,8 @@
(* Extra args from "hAPP" come after any arguments
given directly to the constant. *)
Sign.const_instance thy (c,
- map type_from_node (drop num_term_args us)))
+ map (type_from_node tfrees)
+ (drop num_term_args us)))
in list_comb (t, ts) end
| NONE => (* a free or schematic variable *)
let
@@ -335,21 +337,22 @@
SOME b => Free (b, T)
| NONE =>
case strip_prefix schematic_var_prefix a of
- SOME b => make_var (b, T)
+ SOME b => Var ((b, 0), T)
| NONE =>
(* Variable from the ATP, say "X1" *)
- make_var (fix_atp_variable_name a, T)
+ Var ((fix_atp_variable_name a, 0), T)
in list_comb (t, ts) end
in aux end
(* Type class literal applied to a type. Returns triple of polarity, class,
type. *)
-fun type_constraint_from_node pos (StrNode ("c_Not", [u])) =
- type_constraint_from_node (not pos) u
- | type_constraint_from_node pos u = case u of
+fun type_constraint_from_node pos tfrees (StrNode ("c_Not", [u])) =
+ type_constraint_from_node (not pos) tfrees u
+ | type_constraint_from_node pos tfrees u = case u of
IntLeaf _ => raise NODE [u]
| StrNode (a, us) =>
- (case (strip_prefix class_prefix a, map type_from_node us) of
+ (case (strip_prefix class_prefix a,
+ map (type_from_node tfrees) us) of
(SOME b, [T]) => (pos, b, T)
| _ => raise NODE [u])
@@ -395,24 +398,24 @@
|> clause_for_literals thy
(*Accumulate sort constraints in vt, with "real" literals in lits.*)
-fun lits_of_nodes thy full_types (vt, lits) us =
- case us of
- [] => (vt, finish_clause thy lits)
- | (u :: us) =>
- lits_of_nodes thy full_types
- (add_type_constraint (type_constraint_from_node true u) vt, lits) us
- handle NODE _ =>
- lits_of_nodes thy full_types
- (vt, term_from_node thy full_types (SOME @{typ bool})
- [] u :: lits) us
+fun lits_of_nodes thy full_types tfrees =
+ let
+ fun aux (vt, lits) [] = (vt, finish_clause thy lits)
+ | aux (vt, lits) (u :: us) =
+ aux (add_type_constraint
+ (type_constraint_from_node true tfrees u) vt, lits) us
+ handle NODE _ =>
+ aux (vt, term_from_node thy full_types tfrees (SOME @{typ bool})
+ [] u :: lits) us
+ in aux end
-(*Update TVars/TFrees with detected sort constraints.*)
-fun repair_sorts vt =
+(* Update TVars with detected sort constraints. It's not totally clear when
+ this code is necessary. *)
+fun repair_tvar_sorts vt =
let
fun do_type (Type (a, Ts)) = Type (a, map do_type Ts)
| do_type (TVar (xi, s)) = TVar (xi, the_default s (Vartab.lookup vt xi))
- | do_type (TFree (x, s)) =
- TFree (x, the_default s (Vartab.lookup vt (x, ~1)))
+ | do_type (TFree z) = TFree z
fun do_term (Const (a, T)) = Const (a, do_type T)
| do_term (Free (a, T)) = Free (a, do_type T)
| do_term (Var (xi, T)) = Var (xi, do_type T)
@@ -444,45 +447,28 @@
(* Interpret a list of syntax trees as a clause, given by "real" literals and
sort constraints. "vt" holds the initial sort constraints, from the
conjecture clauses. *)
-fun clause_of_nodes ctxt full_types vt us =
+fun clause_of_nodes ctxt full_types tfrees us =
let
val thy = ProofContext.theory_of ctxt
- val (vt, t) = lits_of_nodes thy full_types (vt, []) us
- in repair_sorts vt t end
+ val (vt, t) = lits_of_nodes thy full_types tfrees (Vartab.empty, []) us
+ in repair_tvar_sorts vt t end
fun check_formula ctxt =
TypeInfer.constrain @{typ bool}
#> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt)
-(** Global sort constraints on TFrees (from tfree_tcs) are positive unit
- clauses. **)
-
-fun add_tfree_constraint (true, cl, TFree (a, _)) = add_var ((a, ~1), cl)
- | add_tfree_constraint _ = I
-fun tfree_constraints_of_clauses vt [] = vt
- | tfree_constraints_of_clauses vt ([lit] :: uss) =
- (tfree_constraints_of_clauses (add_tfree_constraint
- (type_constraint_from_node true lit) vt) uss
- handle NODE _ => (* Not a positive type constraint? Ignore the literal. *)
- tfree_constraints_of_clauses vt uss)
- | tfree_constraints_of_clauses vt (_ :: uss) =
- tfree_constraints_of_clauses vt uss
-
(**** Translation of TSTP files to Isar Proofs ****)
fun unvarify_term (Var ((s, 0), T)) = Free (s, T)
| unvarify_term t = raise TERM ("unvarify_term: non-Var", [t])
-fun clauses_in_lines (Definition (_, u, us)) = u :: us
- | clauses_in_lines (Inference (_, us, _)) = us
-
-fun decode_line full_types vt (Definition (num, u, us)) ctxt =
+fun decode_line full_types tfrees (Definition (num, u, us)) ctxt =
let
- val t1 = clause_of_nodes ctxt full_types vt [u]
+ val t1 = clause_of_nodes ctxt full_types tfrees [u]
val vars = snd (strip_comb t1)
val frees = map unvarify_term vars
val unvarify_args = subst_atomic (vars ~~ frees)
- val t2 = clause_of_nodes ctxt full_types vt us
+ val t2 = clause_of_nodes ctxt full_types tfrees us
val (t1, t2) =
HOLogic.eq_const HOLogic.typeT $ t1 $ t2
|> unvarify_args |> uncombine_term |> check_formula ctxt
@@ -491,19 +477,16 @@
(Definition (num, t1, t2),
fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
end
- | decode_line full_types vt (Inference (num, us, deps)) ctxt =
+ | decode_line full_types tfrees (Inference (num, us, deps)) ctxt =
let
- val t = us |> clause_of_nodes ctxt full_types vt
+ val t = us |> clause_of_nodes ctxt full_types tfrees
|> unskolemize_term |> uncombine_term |> check_formula ctxt
in
(Inference (num, t, deps),
fold Variable.declare_term (OldTerm.term_frees t) ctxt)
end
-fun decode_lines ctxt full_types lines =
- let
- val vt = tfree_constraints_of_clauses Vartab.empty
- (map clauses_in_lines lines)
- in #1 (fold_map (decode_line full_types vt) lines ctxt) end
+fun decode_lines ctxt full_types tfrees lines =
+ fst (fold_map (decode_line full_types tfrees) lines ctxt)
fun aint_inference _ (Definition _) = true
| aint_inference t (Inference (_, t', _)) = not (t aconv t')
@@ -599,8 +582,7 @@
| extract_num _ = NONE
in atp_proof |> split_lines |> map_filter (extract_num o tokens_of) end
-(* Used to label theorems chained into the Sledgehammer call (or rather
- goal?) *)
+(* Used to label theorems chained into the goal. *)
val chained_hint = "sledgehammer_chained"
fun apply_command _ 1 = "by "
@@ -674,13 +656,13 @@
forall_vars t,
ByMetis (fold (add_fact_from_dep thm_names) deps ([], [])))
-fun proof_from_atp_proof pool ctxt full_types isar_shrink_factor atp_proof
- conjecture_shape thm_names params frees =
+fun proof_from_atp_proof pool ctxt full_types tfrees isar_shrink_factor
+ atp_proof conjecture_shape thm_names params frees =
let
val lines =
atp_proof ^ "$" (* the $ sign acts as a sentinel *)
|> parse_proof pool
- |> decode_lines ctxt full_types
+ |> decode_lines ctxt full_types tfrees
|> rpair [] |-> fold_rev (add_line conjecture_shape thm_names)
|> rpair [] |-> fold_rev add_nontrivial_line
|> rpair (0, []) |-> fold_rev (add_desired_line ctxt isar_shrink_factor
@@ -839,7 +821,7 @@
apfst (map (fn l => AList.lookup (op =) subst l |> the_default l))
fun do_step (step as Assume (l, t)) (proof, subst, assums) =
(case AList.lookup (op aconv) assums t of
- SOME l' => (proof, (l', l) :: subst, assums)
+ SOME l' => (proof, (l, l') :: subst, assums)
| NONE => (step :: proof, subst, (t, l) :: assums))
| do_step (Have (qs, l, t, by)) (proof, subst, assums) =
(Have (qs, l, t,
@@ -988,11 +970,12 @@
val thy = ProofContext.theory_of ctxt
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) []
val n = Logic.count_prems (prop_of goal)
val (one_line_proof, lemma_names) =
metis_proof_text (minimize_command, atp_proof, thm_names, goal, i)
fun isar_proof_for () =
- case proof_from_atp_proof pool ctxt full_types isar_shrink_factor
+ case proof_from_atp_proof pool ctxt full_types tfrees isar_shrink_factor
atp_proof conjecture_shape thm_names params
frees
|> redirect_proof thy conjecture_shape hyp_ts concl_t