# HG changeset patch # User blanchet # Date 1274091337 -7200 # Node ID 3c804030474b1086a430f3cf122a2aecd768187d # Parent adc11fb3f3aa727355b9dd1d4f2f959cc7e65872 fix bug in Isar proof reconstruction step relabeling + don't try to infer the sorts of TVars, since this often fails miserably diff -r adc11fb3f3aa -r 3c804030474b src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon May 17 10:18:14 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon May 17 12:15:37 2010 +0200 @@ -217,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 diff -r adc11fb3f3aa -r 3c804030474b src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon May 17 10:18:14 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon May 17 12:15:37 2010 +0200 @@ -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') @@ -674,13 +657,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 +822,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 +971,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