# HG changeset patch # User huffman # Date 1274122810 25200 # Node ID 522ed38eb70aad4a26c8a1367ad486df5b64e716 # Parent fb3fdb4b585e9ee90a9d9f6e9bcfa34887e939e9# Parent 58484df8302abe256542f5f439a20849a9814387 merged diff -r fb3fdb4b585e -r 522ed38eb70a src/HOL/Tools/ATP_Manager/atp_manager.ML --- 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, diff -r fb3fdb4b585e -r 522ed38eb70a src/HOL/Tools/ATP_Manager/atp_systems.ML --- 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 diff -r fb3fdb4b585e -r 522ed38eb70a src/HOL/Tools/Sledgehammer/metis_tactics.ML --- 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 *) diff -r fb3fdb4b585e -r 522ed38eb70a src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- 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 diff -r fb3fdb4b585e -r 522ed38eb70a src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML --- 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"; diff -r fb3fdb4b585e -r 522ed38eb70a src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML --- 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 @ diff -r fb3fdb4b585e -r 522ed38eb70a src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- 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