# HG changeset patch # User blanchet # Date 1273829022 -7200 # Node ID 7d5587f6d5f7ab3f84e69bf93e96b8776ee1a69f # Parent fb18db78be80c6a20935dfd31a13526cc369642a made Sledgehammer's full-typed proof reconstruction work for the first time; previously, Isar proofs and full-type mode were mutually exclusive because both options were hard-coded in the ATP names (e.g., "e_isar" and "full_vampire") -- making the options orthogonal revealed that some code was missing to handle types in the proof reconstruction code diff -r fb18db78be80 -r 7d5587f6d5f7 src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri May 14 11:20:09 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri May 14 11:23:42 2010 +0200 @@ -256,14 +256,13 @@ case strip_prefix const_prefix a of SOME b => let val c = invert_const b - val ntypes = num_typargs thy c + val ntypes = num_type_args thy c val nterms = length ts - ntypes val tts = map tm_to_tt ts val tys = types_of (List.take(tts,ntypes)) - val ntyargs = num_typargs thy c - in if length tys = ntyargs then + in if length tys = ntypes then apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes)) - else error ("Constant " ^ c ^ " expects " ^ Int.toString ntyargs ^ + else error ("Constant " ^ c ^ " expects " ^ Int.toString ntypes ^ " but gets " ^ Int.toString (length tys) ^ " type arguments\n" ^ cat_lines (map (Syntax.string_of_typ ctxt) tys) ^ @@ -460,7 +459,7 @@ in cterm_instantiate [(refl_x, c_t)] REFL_THM end; fun get_ty_arg_size _ (Const (@{const_name "op ="}, _)) = 0 (*equality has no type arguments*) - | get_ty_arg_size thy (Const (c, _)) = (num_typargs thy c handle TYPE _ => 0) + | get_ty_arg_size thy (Const (c, _)) = (num_type_args thy c handle TYPE _ => 0) | get_ty_arg_size _ _ = 0; (* INFERENCE RULE: EQUALITY *) diff -r fb18db78be80 -r 7d5587f6d5f7 src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Fri May 14 11:20:09 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Fri May 14 11:23:42 2010 +0200 @@ -68,8 +68,8 @@ (* minimalization of thms *) -fun minimize_theorems (params as {debug, atps, minimize_timeout, isar_proof, - shrink_factor, ...}) +fun minimize_theorems (params as {debug, atps, full_types, minimize_timeout, + isar_proof, shrink_factor, ...}) i n state name_thms_pairs = let val thy = Proof.theory_of state @@ -110,8 +110,8 @@ in (SOME min_thms, proof_text isar_proof - (pool, debug, shrink_factor, ctxt, conjecture_shape) - (K "", proof, internal_thm_names, goal, i) |> fst) + (pool, debug, full_types, shrink_factor, ctxt, conjecture_shape) + (K "", proof, internal_thm_names, goal, i) |> fst) end | {outcome = SOME TimedOut, ...} => (NONE, "Timeout: You can increase the time limit using the \"timeout\" \ diff -r fb18db78be80 -r 7d5587f6d5f7 src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Fri May 14 11:20:09 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Fri May 14 11:23:42 2010 +0200 @@ -33,6 +33,7 @@ val make_conjecture_clauses : bool -> theory -> thm list -> hol_clause list val make_axiom_clauses : bool -> theory -> (thm * (axiom_name * hol_clause_id)) list -> (axiom_name * hol_clause) list + val type_wrapper_name : string val get_helper_clauses : bool -> theory -> bool -> hol_clause list * (thm * (axiom_name * hol_clause_id)) list * string list -> hol_clause list @@ -198,8 +199,8 @@ (**********************************************************************) (*Result of a function type; no need to check that the argument type matches.*) -fun result_type (TyConstr (("tc_fun", _), [_, tp2])) = tp2 - | result_type _ = raise Fail "Non-function type" +fun result_type (TyConstr (_, [_, tp2])) = tp2 + | result_type _ = raise Fail "non-function type" fun type_of_combterm (CombConst (_, tp, _)) = tp | type_of_combterm (CombVar (_, tp)) = tp @@ -211,7 +212,7 @@ | stripc x = x in stripc(u,[]) end; -val type_wrapper = "ti"; +val type_wrapper_name = "ti" fun head_needs_hBOOL explicit_apply const_needs_hBOOL (CombConst ((c, _), _, _)) = @@ -221,7 +222,7 @@ fun wrap_type full_types (s, ty) pool = if full_types then let val (s', pool) = string_of_fol_type ty pool in - (type_wrapper ^ paren_pack [s, s'], pool) + (type_wrapper_name ^ paren_pack [s, s'], pool) end else (s, pool) @@ -384,7 +385,7 @@ fun decls_of_clauses params clauses arity_clauses = let val functab = - init_functab |> fold Symtab.update [(type_wrapper, 2), ("hAPP", 2), + init_functab |> fold Symtab.update [(type_wrapper_name, 2), ("hAPP", 2), ("tc_bool", 0)] val predtab = Symtab.empty |> Symtab.update ("hBOOL", 1) val (functab, predtab) = diff -r fb18db78be80 -r 7d5587f6d5f7 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri May 14 11:20:09 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri May 14 11:23:42 2010 +0200 @@ -13,7 +13,7 @@ val chained_hint: string val invert_const: string -> string val invert_type_const: string -> string - val num_typargs: theory -> string -> int + 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 @@ -21,11 +21,11 @@ minimize_command * string * string vector * thm * int -> string * string list val isar_proof_text: - name_pool option * bool * int * Proof.context * int list list + name_pool option * bool * bool * int * Proof.context * int list list -> minimize_command * string * string vector * thm * int -> string * string list val proof_text: - bool -> name_pool option * bool * int * Proof.context * int list list + bool -> name_pool option * bool * bool * int * Proof.context * int list list -> minimize_command * string * string vector * thm * int -> string * string list end; @@ -35,6 +35,7 @@ open Sledgehammer_Util open Sledgehammer_FOL_Clause +open Sledgehammer_HOL_Clause open Sledgehammer_Fact_Preprocessor type minimize_command = string list -> string @@ -217,7 +218,7 @@ (**** INTERPRETATION OF TSTP SYNTAX TREES ****) -exception NODE of node +exception NODE of node list (*If string s has the prefix s1, return the result of deleting it.*) fun strip_prefix s1 s = @@ -238,16 +239,16 @@ 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_of_node (u as IntLeaf _) = raise NODE u - | type_of_node (u as StrNode (a, us)) = - let val Ts = map type_of_node us in +(* 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 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 tconsts have type arguments*) + raise NODE [u] (* only "tconst"s have type arguments *) else case strip_prefix tfree_prefix a of SOME b => TFree ("'" ^ b, HOLogic.typeS) | NONE => @@ -264,10 +265,8 @@ fun invert_const c = c |> Symtab.lookup const_trans_table_inv |> the_default c (*The number of type arguments of a constant, zero if it's monomorphic*) -fun num_typargs thy s = length (Sign.const_typargs thy (s, Sign.the_const_type thy s)); - -(*Generates a constant, given its type arguments*) -fun const_of thy (a,Ts) = Const(a, Sign.const_instance thy (a,Ts)); +fun num_type_args thy s = + length (Sign.const_typargs thy (s, Sign.the_const_type thy s)) fun fix_atp_variable_name s = let @@ -286,59 +285,81 @@ | _ => s end -(*First-order translation. No types are known for variables. HOLogic.typeT should allow - them to be inferred.*) -fun term_of_node args thy u = - case u of - IntLeaf _ => raise NODE u - | StrNode ("hBOOL", [u]) => term_of_node [] thy u (* ignore hBOOL *) - | StrNode ("hAPP", [u1, u2]) => term_of_node (u2 :: args) thy u1 - | StrNode (a, us) => - case strip_prefix const_prefix a of - SOME "equal" => - list_comb (Const (@{const_name "op ="}, HOLogic.typeT), - map (term_of_node [] thy) us) - | SOME b => - let - val c = invert_const b - val nterms = length us - num_typargs thy c - val ts = map (term_of_node [] thy) (take nterms us @ args) - (*Extra args from hAPP come AFTER any arguments given directly to the - constant.*) - val Ts = map type_of_node (drop nterms us) - in list_comb(const_of thy (c, Ts), ts) end - | NONE => (*a variable, not a constant*) - let - val opr = - (* a Free variable is typically a Skolem function *) - case strip_prefix fixed_var_prefix a of - SOME b => Free (b, HOLogic.typeT) - | NONE => - case strip_prefix schematic_var_prefix a of - SOME b => make_var (b, HOLogic.typeT) - | NONE => - (* Variable from the ATP, say "X1" *) - make_var (fix_atp_variable_name a, HOLogic.typeT) - in list_comb (opr, map (term_of_node [] thy) (us @ args)) end +(* First-order translation. No types are known for variables. "HOLogic.typeT" + should allow them to be inferred.*) +fun term_from_node thy full_types = + let + fun aux opt_T args u = + case u of + IntLeaf _ => raise NODE [u] + | StrNode ("hBOOL", [u1]) => aux (SOME @{typ bool}) [] u1 + | StrNode ("hAPP", [u1, u2]) => aux opt_T (u2 :: args) u1 + | StrNode ("c_Not", [u1]) => @{const Not} $ aux (SOME @{typ bool}) [] u1 + | 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 + | _ => raise NODE us + else case strip_prefix const_prefix a of + SOME "equal" => + list_comb (Const (@{const_name "op ="}, HOLogic.typeT), + map (aux NONE []) us) + | SOME b => + let + val c = invert_const b + val num_type_args = num_type_args thy c + val actual_num_type_args = if full_types then 0 else num_type_args + val num_term_args = length us - actual_num_type_args + val ts = map (aux NONE []) (take num_term_args us @ args) + val t = + Const (c, if full_types then + case opt_T of + SOME T => map fastype_of ts ---> T + | NONE => + if num_type_args = 0 then + Sign.const_instance thy (c, []) + else + raise Fail ("no type information for " ^ quote c) + else + (* 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))) + in list_comb (t, ts) end + | NONE => (* a free or schematic variable *) + let + val ts = map (aux NONE []) (us @ args) + val T = map fastype_of ts ---> HOLogic.typeT + val t = + case strip_prefix fixed_var_prefix a of + SOME b => Free (b, T) + | NONE => + case strip_prefix schematic_var_prefix a of + SOME b => make_var (b, T) + | NONE => + (* Variable from the ATP, say "X1" *) + make_var (fix_atp_variable_name a, T) + in list_comb (t, ts) end + in aux end (* Type class literal applied to a type. Returns triple of polarity, class, type. *) -fun constraint_of_node pos (StrNode ("c_Not", [u])) = - constraint_of_node (not pos) u - | constraint_of_node pos u = case u of - IntLeaf _ => raise NODE u +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 + IntLeaf _ => raise NODE [u] | StrNode (a, us) => - (case (strip_prefix class_prefix a, map type_of_node us) of + (case (strip_prefix class_prefix a, map type_from_node us) of (SOME b, [T]) => (pos, b, T) - | _ => raise NODE u) + | _ => raise NODE [u]) (** Accumulate type constraints in a clause: negative type literals **) fun add_var (key, z) = Vartab.map_default (key, []) (cons z) -fun add_constraint ((false, cl, TFree(a,_)), vt) = add_var ((a,~1),cl) vt - | add_constraint ((false, cl, TVar(ix,_)), vt) = add_var (ix,cl) vt - | add_constraint (_, vt) = vt; +fun add_type_constraint (false, cl, TFree (a ,_)) = add_var ((a, ~1), cl) + | add_type_constraint (false, cl, TVar (ix, _)) = add_var (ix, cl) + | add_type_constraint _ = I fun is_positive_literal (@{const Not} $ _) = false | is_positive_literal t = true @@ -374,10 +395,16 @@ |> clause_for_literals thy (*Accumulate sort constraints in vt, with "real" literals in lits.*) -fun lits_of_nodes thy (vt, lits) [] = (vt, finish_clause thy lits) - | lits_of_nodes thy (vt, lits) (u :: us) = - lits_of_nodes thy (add_constraint (constraint_of_node true u, vt), lits) us - handle NODE _ => lits_of_nodes thy (vt, term_of_node [] thy u :: lits) us +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 (*Update TVars/TFrees with detected sort constraints.*) fun repair_sorts vt = @@ -395,8 +422,9 @@ in not (Vartab.is_empty vt) ? do_term end fun unskolemize_term t = - fold forall_of (Term.add_consts t [] - |> filter (is_skolem_const_name o fst) |> map Const) t + Term.add_consts t [] + |> filter (is_skolem_const_name o fst) |> map Const + |> rpair t |-> fold forall_of val combinator_table = [(@{const_name COMBI}, @{thm COMBI_def_raw}), @@ -416,12 +444,13 @@ (* 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 vt us = - let val (vt, t) = lits_of_nodes (ProofContext.theory_of ctxt) (vt, []) us in - t |> repair_sorts vt - end +fun clause_of_nodes ctxt full_types vt 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 fun check_formula ctxt = - TypeInfer.constrain HOLogic.boolT + 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 @@ -432,7 +461,7 @@ fun tfree_constraints_of_clauses vt [] = vt | tfree_constraints_of_clauses vt ([lit] :: uss) = (tfree_constraints_of_clauses (add_tfree_constraint - (constraint_of_node true lit) vt) uss + (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) = @@ -447,13 +476,13 @@ fun clauses_in_lines (Definition (_, u, us)) = u :: us | clauses_in_lines (Inference (_, us, _)) = us -fun decode_line vt (Definition (num, u, us)) ctxt = +fun decode_line full_types vt (Definition (num, u, us)) ctxt = let - val t1 = clause_of_nodes ctxt vt [u] + val t1 = clause_of_nodes ctxt full_types vt [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 vt us + val t2 = clause_of_nodes ctxt full_types vt us val (t1, t2) = HOLogic.eq_const HOLogic.typeT $ t1 $ t2 |> unvarify_args |> uncombine_term |> check_formula ctxt @@ -462,19 +491,19 @@ (Definition (num, t1, t2), fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt) end - | decode_line vt (Inference (num, us, deps)) ctxt = + | decode_line full_types vt (Inference (num, us, deps)) ctxt = let - val t = us |> clause_of_nodes ctxt vt + val t = us |> clause_of_nodes ctxt full_types vt |> 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 lines = +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 vt) lines ctxt) end + in #1 (fold_map (decode_line full_types vt) lines ctxt) end fun aint_inference _ (Definition _) = true | aint_inference t (Inference (_, t', _)) = not (t aconv t') @@ -645,20 +674,20 @@ forall_vars t, ByMetis (fold (add_fact_from_dep thm_names) deps ([], []))) -fun proof_from_atp_proof pool ctxt shrink_factor atp_proof conjecture_shape - thm_names frees = +fun proof_from_atp_proof pool ctxt full_types 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 + |> decode_lines ctxt full_types |> rpair [] |-> fold_rev (add_line conjecture_shape thm_names) |> rpair [] |-> fold_rev add_nontrivial_line |> rpair (0, []) |-> fold_rev (add_desired_line ctxt shrink_factor conjecture_shape thm_names frees) |> snd in - (if null frees then [] else [Fix frees]) @ + (if null params then [] else [Fix params]) @ map2 (step_for_line thm_names) (length lines downto 1) lines end @@ -952,17 +981,19 @@ do_indent 0 ^ (if n <> 1 then "next" else "qed") ^ "\n" in do_proof end -fun isar_proof_text (pool, debug, shrink_factor, ctxt, conjecture_shape) +fun isar_proof_text (pool, debug, full_types, shrink_factor, ctxt, + conjecture_shape) (minimize_command, atp_proof, thm_names, goal, i) = let val thy = ProofContext.theory_of ctxt - val (frees, hyp_ts, concl_t) = strip_subgoal goal i + val (params, hyp_ts, concl_t) = strip_subgoal goal i + val frees = fold Term.add_frees (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 shrink_factor atp_proof - conjecture_shape thm_names frees + case proof_from_atp_proof pool ctxt full_types shrink_factor atp_proof + conjecture_shape thm_names params frees |> redirect_proof thy conjecture_shape hyp_ts concl_t |> kill_duplicate_assumptions_in_proof |> then_chain_proof