1.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon May 17 08:45:46 2010 -0700
1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon May 17 12:00:10 2010 -0700
1.3 @@ -34,8 +34,8 @@
1.4 axiom_clauses: (thm * (string * int)) list option,
1.5 filtered_clauses: (thm * (string * int)) list option}
1.6 datatype failure =
1.7 - Unprovable | TimedOut | OutOfResources | OldSpass | MalformedOutput |
1.8 - UnknownError
1.9 + Unprovable | TimedOut | OutOfResources | OldSpass | MalformedInput |
1.10 + MalformedOutput | UnknownError
1.11 type prover_result =
1.12 {outcome: failure option,
1.13 message: string,
1.14 @@ -95,8 +95,8 @@
1.15 filtered_clauses: (thm * (string * int)) list option};
1.16
1.17 datatype failure =
1.18 - Unprovable | TimedOut | OutOfResources | OldSpass | MalformedOutput |
1.19 - UnknownError
1.20 + Unprovable | TimedOut | OutOfResources | OldSpass | MalformedInput |
1.21 + MalformedOutput | UnknownError
1.22
1.23 type prover_result =
1.24 {outcome: failure option,
2.1 --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Mon May 17 08:45:46 2010 -0700
2.2 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Mon May 17 12:00:10 2010 -0700
2.3 @@ -100,6 +100,9 @@
2.4 (Path.variable "ISABELLE_HOME_USER" ::
2.5 map Path.basic ["etc", "components"]))) ^
2.6 "\" on a line of its own."
2.7 + | string_for_failure MalformedInput =
2.8 + "Internal Sledgehammer error: The ATP problem is malformed. Please report \
2.9 + \this to the Isabelle developers."
2.10 | string_for_failure MalformedOutput = "Error: The ATP output is malformed."
2.11 | string_for_failure UnknownError = "Error: An unknown ATP error occurred."
2.12
2.13 @@ -336,7 +339,8 @@
2.14 known_failures =
2.15 [(Unprovable, "SPASS beiseite: Completion found"),
2.16 (TimedOut, "SPASS beiseite: Ran out of time"),
2.17 - (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded")],
2.18 + (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
2.19 + (MalformedInput, "Undefined symbol")],
2.20 max_axiom_clauses = 40,
2.21 prefers_theory_relevant = true}
2.22 val spass = dfg_prover "spass" spass_config
3.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon May 17 08:45:46 2010 -0700
3.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon May 17 12:00:10 2010 -0700
3.3 @@ -141,9 +141,10 @@
3.4 in
3.5 if is_conjecture then
3.6 (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits),
3.7 - add_type_literals types_sorts)
3.8 + type_literals_for_types types_sorts)
3.9 else
3.10 - let val tylits = add_type_literals (filter (not o default_sort ctxt) types_sorts)
3.11 + let val tylits = filter_out (default_sort ctxt) types_sorts
3.12 + |> type_literals_for_types
3.13 val mtylits = if Config.get ctxt type_lits
3.14 then map (metis_of_type_literals false) tylits else []
3.15 in
3.16 @@ -216,6 +217,8 @@
3.17 fun strip_happ args (Metis.Term.Fn(".",[t,u])) = strip_happ (u::args) t
3.18 | strip_happ args x = (x, args);
3.19
3.20 +fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
3.21 +
3.22 fun fol_type_to_isa _ (Metis.Term.Var v) =
3.23 (case strip_prefix tvar_prefix v of
3.24 SOME w => make_tvar w
3.25 @@ -599,9 +602,9 @@
3.26
3.27 (*Extract TFree constraints from context to include as conjecture clauses*)
3.28 fun init_tfrees ctxt =
3.29 - let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts
3.30 - in
3.31 - add_type_literals (Vartab.fold add (#2 (Variable.constraints_of ctxt)) [])
3.32 + let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts in
3.33 + Vartab.fold add (#2 (Variable.constraints_of ctxt)) []
3.34 + |> type_literals_for_types
3.35 end;
3.36
3.37 (*transform isabelle type / arity clause to metis clause *)
4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon May 17 08:45:46 2010 -0700
4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon May 17 12:00:10 2010 -0700
4.3 @@ -352,7 +352,7 @@
4.4 fun subtract_cls ax_clauses =
4.5 filter_out (Termtab.defined (mk_clause_table ax_clauses) o prop_of)
4.6
4.7 -fun all_valid_thms respect_no_atp ctxt =
4.8 +fun all_valid_thms respect_no_atp ctxt chain_ths =
4.9 let
4.10 val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt);
4.11 val local_facts = ProofContext.facts_of ctxt;
4.12 @@ -371,7 +371,8 @@
4.13 val name2 = Name_Space.extern full_space name;
4.14 val ths = filter_out bad_for_atp ths0;
4.15 in
4.16 - if Facts.is_concealed facts name orelse null ths orelse
4.17 + if Facts.is_concealed facts name orelse
4.18 + forall (member Thm.eq_thm chain_ths) ths orelse
4.19 (respect_no_atp andalso is_package_def name) then
4.20 I
4.21 else case find_first check_thms [name1, name2, name] of
4.22 @@ -396,10 +397,10 @@
4.23
4.24 (* The single-name theorems go after the multiple-name ones, so that single
4.25 names are preferred when both are available. *)
4.26 -fun name_thm_pairs respect_no_atp ctxt =
4.27 +fun name_thm_pairs respect_no_atp ctxt chain_ths =
4.28 let
4.29 val (mults, singles) =
4.30 - List.partition is_multi (all_valid_thms respect_no_atp ctxt)
4.31 + List.partition is_multi (all_valid_thms respect_no_atp ctxt chain_ths)
4.32 val ps = [] |> fold add_single_names singles
4.33 |> fold add_multi_names mults
4.34 in ps |> respect_no_atp ? filter_out (No_ATPs.member ctxt o snd) end;
4.35 @@ -408,11 +409,11 @@
4.36 (warning ("No name for theorem " ^ Display.string_of_thm_without_context th); false)
4.37 | check_named _ = true;
4.38
4.39 -fun get_all_lemmas respect_no_atp ctxt =
4.40 +fun get_all_lemmas respect_no_atp ctxt chain_ths =
4.41 let val included_thms =
4.42 tap (fn ths => trace_msg
4.43 (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems")))
4.44 - (name_thm_pairs respect_no_atp ctxt)
4.45 + (name_thm_pairs respect_no_atp ctxt chain_ths)
4.46 in
4.47 filter check_named included_thms
4.48 end;
4.49 @@ -509,14 +510,14 @@
4.50 fun get_relevant_facts respect_no_atp relevance_threshold relevance_convergence
4.51 defs_relevant max_new theory_relevant
4.52 (relevance_override as {add, only, ...})
4.53 - (ctxt, (chain_ths, th)) goal_cls =
4.54 + (ctxt, (chain_ths, _)) goal_cls =
4.55 if (only andalso null add) orelse relevance_threshold > 1.0 then
4.56 []
4.57 else
4.58 let
4.59 val thy = ProofContext.theory_of ctxt
4.60 val is_FO = is_first_order thy goal_cls
4.61 - val included_cls = get_all_lemmas respect_no_atp ctxt
4.62 + val included_cls = get_all_lemmas respect_no_atp ctxt chain_ths
4.63 |> cnf_rules_pairs thy |> make_unique
4.64 |> restrict_to_logic thy is_FO
4.65 |> remove_unwanted_clauses
5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Mon May 17 08:45:46 2010 -0700
5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Mon May 17 12:00:10 2010 -0700
5.3 @@ -48,7 +48,7 @@
5.4 TyLitVar of string * name |
5.5 TyLitFree of string * name
5.6 exception CLAUSE of string * term
5.7 - val add_type_literals : typ list -> type_literal list
5.8 + val type_literals_for_types : typ list -> type_literal list
5.9 val get_tvar_strs: typ list -> string list
5.10 datatype arLit =
5.11 TConsLit of class * string * string list
5.12 @@ -331,7 +331,8 @@
5.13 | pred_of_sort (TyLitFree (s, _)) = (s, 1)
5.14
5.15 (*Given a list of sorted type variables, return a list of type literals.*)
5.16 -fun add_type_literals Ts = fold (union (op =)) (map sorts_on_typs Ts) []
5.17 +fun type_literals_for_types Ts =
5.18 + fold (union (op =)) (map sorts_on_typs Ts) []
5.19
5.20 (*The correct treatment of TFrees like 'a in lemmas (axiom clauses) is not clear.
5.21 * Ignoring them leads to unsound proofs, since we do nothing to ensure that 'a
5.22 @@ -520,7 +521,7 @@
5.23 dfg_forall vars ("or(" ^ commas lits ^ ")") ^ ",\n" ^
5.24 string_of_clausename (cls_id,ax_name) ^ ").\n\n";
5.25
5.26 -fun string_of_arity (name, num) = "(" ^ name ^ "," ^ Int.toString num ^ ")"
5.27 +fun string_of_arity (name, arity) = "(" ^ name ^ ", " ^ Int.toString arity ^ ")"
5.28
5.29 fun string_of_preds [] = ""
5.30 | string_of_preds preds = "predicates[" ^ commas(map string_of_arity preds) ^ "].\n";
6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Mon May 17 08:45:46 2010 -0700
6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Mon May 17 12:00:10 2010 -0700
6.3 @@ -300,7 +300,7 @@
6.4 let
6.5 val (lits, pool) = pool_map (tptp_literal params) literals pool
6.6 val (tylits, pool) = pool_map (tptp_of_type_literal pos)
6.7 - (add_type_literals ctypes_sorts) pool
6.8 + (type_literals_for_types ctypes_sorts) pool
6.9 in ((lits, tylits), pool) end
6.10
6.11 fun tptp_clause params (cls as HOLClause {axiom_name, clause_id, kind, ...})
6.12 @@ -320,7 +320,8 @@
6.13
6.14 fun dfg_type_literals params pos (HOLClause {literals, ctypes_sorts, ...}) =
6.15 pool_map (dfg_literal params) literals
6.16 - #>> rpair (map (dfg_of_type_literal pos) (add_type_literals ctypes_sorts))
6.17 + #>> rpair (map (dfg_of_type_literal pos)
6.18 + (type_literals_for_types ctypes_sorts))
6.19
6.20 fun get_uvars (CombConst _) vars pool = (vars, pool)
6.21 | get_uvars (CombVar (name, _)) vars pool =
6.22 @@ -531,6 +532,8 @@
6.23
6.24 (* DFG format *)
6.25
6.26 +fun dfg_tfree_predicate s = (first_field "(" s |> the |> fst, 1)
6.27 +
6.28 fun write_dfg_file full_types explicit_apply file clauses =
6.29 let
6.30 (* Some of the helper functions below are not name-pool-aware. However,
6.31 @@ -543,13 +546,16 @@
6.32 val params = (full_types, explicit_apply, cma, cnh)
6.33 val ((conjecture_clss, tfree_litss), pool) =
6.34 pool_map (dfg_clause params) conjectures pool |>> ListPair.unzip
6.35 - and problem_name = Path.implode (Path.base file)
6.36 + val tfree_lits = union_all tfree_litss
6.37 + val problem_name = Path.implode (Path.base file)
6.38 val (axstrs, pool) = pool_map (apfst fst oo dfg_clause params) axclauses pool
6.39 - val tfree_clss = map dfg_tfree_clause (union_all tfree_litss)
6.40 + val tfree_clss = map dfg_tfree_clause tfree_lits
6.41 + val tfree_preds = map dfg_tfree_predicate tfree_lits
6.42 val (helper_clauses_strs, pool) =
6.43 pool_map (apfst fst oo dfg_clause params) helper_clauses pool
6.44 val (funcs, cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses
6.45 - and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
6.46 + val ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
6.47 + val preds = tfree_preds @ cl_preds @ ty_preds
6.48 val conjecture_offset =
6.49 length axclauses + length classrel_clauses + length arity_clauses
6.50 + length helper_clauses
6.51 @@ -559,7 +565,7 @@
6.52 string_of_start problem_name ::
6.53 string_of_descrip problem_name ::
6.54 string_of_symbols (string_of_funcs funcs)
6.55 - (string_of_preds (cl_preds @ ty_preds)) ::
6.56 + (string_of_preds preds) ::
6.57 "list_of_clauses(axioms, cnf).\n" ::
6.58 axstrs @
6.59 map dfg_classrel_clause classrel_clauses @
7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon May 17 08:45:46 2010 -0700
7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon May 17 12:00:10 2010 -0700
7.3 @@ -14,7 +14,6 @@
7.4 val invert_const: string -> string
7.5 val invert_type_const: string -> string
7.6 val num_type_args: theory -> string -> int
7.7 - val make_tvar: string -> typ
7.8 val strip_prefix: string -> string -> string option
7.9 val metis_line: int -> int -> string list -> string
7.10 val metis_proof_text:
7.11 @@ -235,26 +234,27 @@
7.12 SOME c' => c'
7.13 | NONE => c;
7.14
7.15 -fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS);
7.16 -fun make_tparam s = TypeInfer.param 0 (s, HOLogic.typeS)
7.17 -fun make_var (b,T) = Var((b,0),T);
7.18 -
7.19 (* Type variables are given the basic sort "HOL.type". Some will later be
7.20 constrained by information from type literals, or by type inference. *)
7.21 -fun type_from_node (u as IntLeaf _) = raise NODE [u]
7.22 - | type_from_node (u as StrNode (a, us)) =
7.23 - let val Ts = map type_from_node us in
7.24 +fun type_from_node _ (u as IntLeaf _) = raise NODE [u]
7.25 + | type_from_node tfrees (u as StrNode (a, us)) =
7.26 + let val Ts = map (type_from_node tfrees) us in
7.27 case strip_prefix tconst_prefix a of
7.28 SOME b => Type (invert_type_const b, Ts)
7.29 | NONE =>
7.30 if not (null us) then
7.31 raise NODE [u] (* only "tconst"s have type arguments *)
7.32 else case strip_prefix tfree_prefix a of
7.33 - SOME b => TFree ("'" ^ b, HOLogic.typeS)
7.34 + SOME b =>
7.35 + let val s = "'" ^ b in
7.36 + TFree (s, AList.lookup (op =) tfrees s |> the_default HOLogic.typeS)
7.37 + end
7.38 | NONE =>
7.39 case strip_prefix tvar_prefix a of
7.40 - SOME b => make_tvar b
7.41 - | NONE => make_tparam a (* Variable from the ATP, say "X1" *)
7.42 + SOME b => TVar (("'" ^ b, 0), HOLogic.typeS)
7.43 + | NONE =>
7.44 + (* Variable from the ATP, say "X1" *)
7.45 + TypeInfer.param 0 (a, HOLogic.typeS)
7.46 end
7.47
7.48 (*Invert the table of translations between Isabelle and ATPs*)
7.49 @@ -287,7 +287,7 @@
7.50
7.51 (* First-order translation. No types are known for variables. "HOLogic.typeT"
7.52 should allow them to be inferred.*)
7.53 -fun term_from_node thy full_types =
7.54 +fun term_from_node thy full_types tfrees =
7.55 let
7.56 fun aux opt_T args u =
7.57 case u of
7.58 @@ -298,7 +298,8 @@
7.59 | StrNode (a, us) =>
7.60 if a = type_wrapper_name then
7.61 case us of
7.62 - [term_u, typ_u] => aux (SOME (type_from_node typ_u)) args term_u
7.63 + [term_u, typ_u] =>
7.64 + aux (SOME (type_from_node tfrees typ_u)) args term_u
7.65 | _ => raise NODE us
7.66 else case strip_prefix const_prefix a of
7.67 SOME "equal" =>
7.68 @@ -324,7 +325,8 @@
7.69 (* Extra args from "hAPP" come after any arguments
7.70 given directly to the constant. *)
7.71 Sign.const_instance thy (c,
7.72 - map type_from_node (drop num_term_args us)))
7.73 + map (type_from_node tfrees)
7.74 + (drop num_term_args us)))
7.75 in list_comb (t, ts) end
7.76 | NONE => (* a free or schematic variable *)
7.77 let
7.78 @@ -335,21 +337,22 @@
7.79 SOME b => Free (b, T)
7.80 | NONE =>
7.81 case strip_prefix schematic_var_prefix a of
7.82 - SOME b => make_var (b, T)
7.83 + SOME b => Var ((b, 0), T)
7.84 | NONE =>
7.85 (* Variable from the ATP, say "X1" *)
7.86 - make_var (fix_atp_variable_name a, T)
7.87 + Var ((fix_atp_variable_name a, 0), T)
7.88 in list_comb (t, ts) end
7.89 in aux end
7.90
7.91 (* Type class literal applied to a type. Returns triple of polarity, class,
7.92 type. *)
7.93 -fun type_constraint_from_node pos (StrNode ("c_Not", [u])) =
7.94 - type_constraint_from_node (not pos) u
7.95 - | type_constraint_from_node pos u = case u of
7.96 +fun type_constraint_from_node pos tfrees (StrNode ("c_Not", [u])) =
7.97 + type_constraint_from_node (not pos) tfrees u
7.98 + | type_constraint_from_node pos tfrees u = case u of
7.99 IntLeaf _ => raise NODE [u]
7.100 | StrNode (a, us) =>
7.101 - (case (strip_prefix class_prefix a, map type_from_node us) of
7.102 + (case (strip_prefix class_prefix a,
7.103 + map (type_from_node tfrees) us) of
7.104 (SOME b, [T]) => (pos, b, T)
7.105 | _ => raise NODE [u])
7.106
7.107 @@ -395,24 +398,24 @@
7.108 |> clause_for_literals thy
7.109
7.110 (*Accumulate sort constraints in vt, with "real" literals in lits.*)
7.111 -fun lits_of_nodes thy full_types (vt, lits) us =
7.112 - case us of
7.113 - [] => (vt, finish_clause thy lits)
7.114 - | (u :: us) =>
7.115 - lits_of_nodes thy full_types
7.116 - (add_type_constraint (type_constraint_from_node true u) vt, lits) us
7.117 - handle NODE _ =>
7.118 - lits_of_nodes thy full_types
7.119 - (vt, term_from_node thy full_types (SOME @{typ bool})
7.120 - [] u :: lits) us
7.121 +fun lits_of_nodes thy full_types tfrees =
7.122 + let
7.123 + fun aux (vt, lits) [] = (vt, finish_clause thy lits)
7.124 + | aux (vt, lits) (u :: us) =
7.125 + aux (add_type_constraint
7.126 + (type_constraint_from_node true tfrees u) vt, lits) us
7.127 + handle NODE _ =>
7.128 + aux (vt, term_from_node thy full_types tfrees (SOME @{typ bool})
7.129 + [] u :: lits) us
7.130 + in aux end
7.131
7.132 -(*Update TVars/TFrees with detected sort constraints.*)
7.133 -fun repair_sorts vt =
7.134 +(* Update TVars with detected sort constraints. It's not totally clear when
7.135 + this code is necessary. *)
7.136 +fun repair_tvar_sorts vt =
7.137 let
7.138 fun do_type (Type (a, Ts)) = Type (a, map do_type Ts)
7.139 | do_type (TVar (xi, s)) = TVar (xi, the_default s (Vartab.lookup vt xi))
7.140 - | do_type (TFree (x, s)) =
7.141 - TFree (x, the_default s (Vartab.lookup vt (x, ~1)))
7.142 + | do_type (TFree z) = TFree z
7.143 fun do_term (Const (a, T)) = Const (a, do_type T)
7.144 | do_term (Free (a, T)) = Free (a, do_type T)
7.145 | do_term (Var (xi, T)) = Var (xi, do_type T)
7.146 @@ -444,45 +447,28 @@
7.147 (* Interpret a list of syntax trees as a clause, given by "real" literals and
7.148 sort constraints. "vt" holds the initial sort constraints, from the
7.149 conjecture clauses. *)
7.150 -fun clause_of_nodes ctxt full_types vt us =
7.151 +fun clause_of_nodes ctxt full_types tfrees us =
7.152 let
7.153 val thy = ProofContext.theory_of ctxt
7.154 - val (vt, t) = lits_of_nodes thy full_types (vt, []) us
7.155 - in repair_sorts vt t end
7.156 + val (vt, t) = lits_of_nodes thy full_types tfrees (Vartab.empty, []) us
7.157 + in repair_tvar_sorts vt t end
7.158 fun check_formula ctxt =
7.159 TypeInfer.constrain @{typ bool}
7.160 #> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt)
7.161
7.162 -(** Global sort constraints on TFrees (from tfree_tcs) are positive unit
7.163 - clauses. **)
7.164 -
7.165 -fun add_tfree_constraint (true, cl, TFree (a, _)) = add_var ((a, ~1), cl)
7.166 - | add_tfree_constraint _ = I
7.167 -fun tfree_constraints_of_clauses vt [] = vt
7.168 - | tfree_constraints_of_clauses vt ([lit] :: uss) =
7.169 - (tfree_constraints_of_clauses (add_tfree_constraint
7.170 - (type_constraint_from_node true lit) vt) uss
7.171 - handle NODE _ => (* Not a positive type constraint? Ignore the literal. *)
7.172 - tfree_constraints_of_clauses vt uss)
7.173 - | tfree_constraints_of_clauses vt (_ :: uss) =
7.174 - tfree_constraints_of_clauses vt uss
7.175 -
7.176
7.177 (**** Translation of TSTP files to Isar Proofs ****)
7.178
7.179 fun unvarify_term (Var ((s, 0), T)) = Free (s, T)
7.180 | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t])
7.181
7.182 -fun clauses_in_lines (Definition (_, u, us)) = u :: us
7.183 - | clauses_in_lines (Inference (_, us, _)) = us
7.184 -
7.185 -fun decode_line full_types vt (Definition (num, u, us)) ctxt =
7.186 +fun decode_line full_types tfrees (Definition (num, u, us)) ctxt =
7.187 let
7.188 - val t1 = clause_of_nodes ctxt full_types vt [u]
7.189 + val t1 = clause_of_nodes ctxt full_types tfrees [u]
7.190 val vars = snd (strip_comb t1)
7.191 val frees = map unvarify_term vars
7.192 val unvarify_args = subst_atomic (vars ~~ frees)
7.193 - val t2 = clause_of_nodes ctxt full_types vt us
7.194 + val t2 = clause_of_nodes ctxt full_types tfrees us
7.195 val (t1, t2) =
7.196 HOLogic.eq_const HOLogic.typeT $ t1 $ t2
7.197 |> unvarify_args |> uncombine_term |> check_formula ctxt
7.198 @@ -491,19 +477,16 @@
7.199 (Definition (num, t1, t2),
7.200 fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
7.201 end
7.202 - | decode_line full_types vt (Inference (num, us, deps)) ctxt =
7.203 + | decode_line full_types tfrees (Inference (num, us, deps)) ctxt =
7.204 let
7.205 - val t = us |> clause_of_nodes ctxt full_types vt
7.206 + val t = us |> clause_of_nodes ctxt full_types tfrees
7.207 |> unskolemize_term |> uncombine_term |> check_formula ctxt
7.208 in
7.209 (Inference (num, t, deps),
7.210 fold Variable.declare_term (OldTerm.term_frees t) ctxt)
7.211 end
7.212 -fun decode_lines ctxt full_types lines =
7.213 - let
7.214 - val vt = tfree_constraints_of_clauses Vartab.empty
7.215 - (map clauses_in_lines lines)
7.216 - in #1 (fold_map (decode_line full_types vt) lines ctxt) end
7.217 +fun decode_lines ctxt full_types tfrees lines =
7.218 + fst (fold_map (decode_line full_types tfrees) lines ctxt)
7.219
7.220 fun aint_inference _ (Definition _) = true
7.221 | aint_inference t (Inference (_, t', _)) = not (t aconv t')
7.222 @@ -599,8 +582,7 @@
7.223 | extract_num _ = NONE
7.224 in atp_proof |> split_lines |> map_filter (extract_num o tokens_of) end
7.225
7.226 -(* Used to label theorems chained into the Sledgehammer call (or rather
7.227 - goal?) *)
7.228 +(* Used to label theorems chained into the goal. *)
7.229 val chained_hint = "sledgehammer_chained"
7.230
7.231 fun apply_command _ 1 = "by "
7.232 @@ -674,13 +656,13 @@
7.233 forall_vars t,
7.234 ByMetis (fold (add_fact_from_dep thm_names) deps ([], [])))
7.235
7.236 -fun proof_from_atp_proof pool ctxt full_types isar_shrink_factor atp_proof
7.237 - conjecture_shape thm_names params frees =
7.238 +fun proof_from_atp_proof pool ctxt full_types tfrees isar_shrink_factor
7.239 + atp_proof conjecture_shape thm_names params frees =
7.240 let
7.241 val lines =
7.242 atp_proof ^ "$" (* the $ sign acts as a sentinel *)
7.243 |> parse_proof pool
7.244 - |> decode_lines ctxt full_types
7.245 + |> decode_lines ctxt full_types tfrees
7.246 |> rpair [] |-> fold_rev (add_line conjecture_shape thm_names)
7.247 |> rpair [] |-> fold_rev add_nontrivial_line
7.248 |> rpair (0, []) |-> fold_rev (add_desired_line ctxt isar_shrink_factor
7.249 @@ -839,7 +821,7 @@
7.250 apfst (map (fn l => AList.lookup (op =) subst l |> the_default l))
7.251 fun do_step (step as Assume (l, t)) (proof, subst, assums) =
7.252 (case AList.lookup (op aconv) assums t of
7.253 - SOME l' => (proof, (l', l) :: subst, assums)
7.254 + SOME l' => (proof, (l, l') :: subst, assums)
7.255 | NONE => (step :: proof, subst, (t, l) :: assums))
7.256 | do_step (Have (qs, l, t, by)) (proof, subst, assums) =
7.257 (Have (qs, l, t,
7.258 @@ -988,11 +970,12 @@
7.259 val thy = ProofContext.theory_of ctxt
7.260 val (params, hyp_ts, concl_t) = strip_subgoal goal i
7.261 val frees = fold Term.add_frees (concl_t :: hyp_ts) []
7.262 + val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) []
7.263 val n = Logic.count_prems (prop_of goal)
7.264 val (one_line_proof, lemma_names) =
7.265 metis_proof_text (minimize_command, atp_proof, thm_names, goal, i)
7.266 fun isar_proof_for () =
7.267 - case proof_from_atp_proof pool ctxt full_types isar_shrink_factor
7.268 + case proof_from_atp_proof pool ctxt full_types tfrees isar_shrink_factor
7.269 atp_proof conjecture_shape thm_names params
7.270 frees
7.271 |> redirect_proof thy conjecture_shape hyp_ts concl_t