# HG changeset patch # User blanchet # Date 1272529526 -7200 # Node ID 81dc2c20f05287ba91fd951dbe294574513f6192 # Parent 8ff45c2076da8b52e6db69dba8fd1120678a5fc3 use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables) diff -r 8ff45c2076da -r 81dc2c20f052 src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Apr 29 01:17:14 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Apr 29 10:25:26 2010 +0200 @@ -123,14 +123,16 @@ in (map (hol_literal_to_fol mode) lits, types_sorts) end; (*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*) -fun metis_of_typeLit pos (LTVar (s,x)) = metis_lit pos s [Metis.Term.Var x] - | metis_of_typeLit pos (LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])]; +fun metis_of_type_literals pos (TyLitVar (s, (s', _))) = + metis_lit pos s [Metis.Term.Var s'] + | metis_of_type_literals pos (TyLitFree (s, (s', _))) = + metis_lit pos s [Metis.Term.Fn (s',[])] fun default_sort _ (TVar _) = false | default_sort ctxt (TFree (x, s)) = (s = the_default [] (Variable.def_sort ctxt (x, ~1))); fun metis_of_tfree tf = - Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_typeLit true tf)); + Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_type_literals true tf)); fun hol_thm_to_fol is_conjecture ctxt mode th = let val thy = ProofContext.theory_of ctxt @@ -138,11 +140,12 @@ (literals_of_hol_thm thy mode o HOLogic.dest_Trueprop o prop_of) th in if is_conjecture then - (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), add_typs types_sorts) + (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), + add_type_literals types_sorts) else - let val tylits = add_typs (filter (not o default_sort ctxt) types_sorts) + let val tylits = add_type_literals (filter (not o default_sort ctxt) types_sorts) val mtylits = if Config.get ctxt type_lits - then map (metis_of_typeLit false) tylits else [] + then map (metis_of_type_literals false) tylits else [] in (Metis.Thm.axiom (Metis.LiteralSet.fromList(mtylits @ mlits)), []) end @@ -598,7 +601,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_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end; + in + add_type_literals (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) + end; (*transform isabelle type / arity clause to metis clause *) fun add_type_thm [] lmap = lmap @@ -669,7 +674,7 @@ val (mode, {axioms,tfrees}) = build_map mode ctxt cls ths val _ = if null tfrees then () else (trace_msg (fn () => "TFREE CLAUSES"); - app (fn tf => trace_msg (fn _ => tptp_of_typeLit true tf)) tfrees) + app (fn tf => trace_msg (fn _ => tptp_of_type_literal true tf NONE |> fst)) tfrees) val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS") val thms = map #1 axioms val _ = app (fn th => trace_msg (fn () => Metis.Thm.toString th)) thms diff -r 8ff45c2076da -r 81dc2c20f052 src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Thu Apr 29 01:17:14 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Thu Apr 29 10:25:26 2010 +0200 @@ -44,9 +44,11 @@ TyConstr of name * fol_type list val string_of_fol_type : fol_type -> name_pool option -> string * name_pool option - datatype type_literal = LTVar of string * string | LTFree of string * string + datatype type_literal = + TyLitVar of string * name | + TyLitFree of string * name exception CLAUSE of string * term - val add_typs : typ list -> type_literal list + val add_type_literals : typ list -> type_literal list val get_tvar_strs: typ list -> string list datatype arLit = TConsLit of class * string * string list @@ -68,7 +70,7 @@ arity_clause -> int Symtab.table -> int Symtab.table val init_functab: int Symtab.table val dfg_sign: bool -> string -> string - val dfg_of_typeLit: bool -> type_literal -> string + val dfg_of_type_literal: bool -> type_literal -> string val gen_dfg_cls: int * string * kind * string list * string list * string list -> string val string_of_preds: (string * Int.int) list -> string val string_of_funcs: (string * int) list -> string @@ -79,7 +81,8 @@ val dfg_classrel_clause: classrel_clause -> string val dfg_arity_clause: arity_clause -> string val tptp_sign: bool -> string -> string - val tptp_of_typeLit : bool -> type_literal -> string + val tptp_of_type_literal : + bool -> type_literal -> name_pool option -> string * name_pool option val gen_tptp_cls : int * string * kind * string list * string list -> string val tptp_tfree_clause : string -> string val tptp_arity_clause : arity_clause -> string @@ -173,9 +176,7 @@ fun paren_pack [] = "" (*empty argument list*) | paren_pack strings = "(" ^ commas strings ^ ")"; -(*TSTP format uses (...) rather than the old [...]*) -fun tptp_pack strings = "(" ^ space_implode " | " strings ^ ")"; - +fun tptp_clause strings = "(" ^ space_implode " | " strings ^ ")" (*Remove the initial ' character from a type variable, if it is present*) fun trim_type_var s = @@ -230,9 +231,9 @@ fun empty_name_pool readable_names = if readable_names then SOME (`I Symtab.empty) else NONE +fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs fun pool_map f xs = - fold_rev (fn x => fn (ys, pool) => f x pool |>> (fn y => y :: ys)) xs - o pair [] + pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs [] fun add_nice_name full_name nice_prefix j the_pool = let @@ -306,8 +307,10 @@ val (ss, pool) = pool_map string_of_fol_type tys pool in (s ^ paren_pack ss, pool) end -(*First string is the type class; the second is a TVar or TFfree*) -datatype type_literal = LTVar of string * string | LTFree of string * string; +(* The first component is the type class; the second is a TVar or TFree. *) +datatype type_literal = + TyLitVar of string * name | + TyLitFree of string * name exception CLAUSE of string * term; @@ -317,21 +320,21 @@ let val sorts = sorts_on_typs_aux ((x,i), ss) in if s = "HOL.type" then sorts - else if i = ~1 then LTFree(make_type_class s, make_fixed_type_var x) :: sorts - else LTVar(make_type_class s, make_schematic_type_var (x,i)) :: sorts + else if i = ~1 then TyLitFree (make_type_class s, `make_fixed_type_var x) :: sorts + else TyLitVar (make_type_class s, (make_schematic_type_var (x,i), x)) :: sorts end; fun sorts_on_typs (TFree (a,s)) = sorts_on_typs_aux ((a,~1),s) | sorts_on_typs (TVar (v,s)) = sorts_on_typs_aux (v,s); -fun pred_of_sort (LTVar (s,ty)) = (s,1) - | pred_of_sort (LTFree (s,ty)) = (s,1) +fun pred_of_sort (TyLitVar (s, _)) = (s, 1) + | pred_of_sort (TyLitFree (s, _)) = (s, 1) (*Given a list of sorted type variables, return a list of type literals.*) -fun add_typs Ts = fold (union (op =)) (map sorts_on_typs Ts) [] +fun add_type_literals 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 + * Ignoring them leads to unsound proofs, since we do nothing to ensure that 'a in a lemma has the same sort as 'a in the conjecture. * Deleting such clauses will lead to problems with locales in other use of local results where 'a is fixed. Probably we should delete clauses unless the sorts agree. @@ -499,8 +502,10 @@ fun dfg_sign true s = s | dfg_sign false s = "not(" ^ s ^ ")" -fun dfg_of_typeLit pos (LTVar (s,ty)) = dfg_sign pos (s ^ "(" ^ ty ^ ")") - | dfg_of_typeLit pos (LTFree (s,ty)) = dfg_sign pos (s ^ "(" ^ ty ^ ")"); +fun dfg_of_type_literal pos (TyLitVar (s, (s', _))) = + dfg_sign pos (s ^ "(" ^ s' ^ ")") + | dfg_of_type_literal pos (TyLitFree (s, (s', _))) = + dfg_sign pos (s ^ "(" ^ s' ^ ")"); (*Enclose the clause body by quantifiers, if necessary*) fun dfg_forall [] body = body @@ -563,21 +568,23 @@ fun tptp_sign true s = s | tptp_sign false s = "~ " ^ s -fun tptp_of_typeLit pos (LTVar (s, ty)) = tptp_sign pos (s ^ "(" ^ ty ^ ")") - | tptp_of_typeLit pos (LTFree (s, ty)) = tptp_sign pos (s ^ "(" ^ ty ^ ")") +fun tptp_of_type_literal pos (TyLitVar (s, name)) = + nice_name name #>> (fn s' => tptp_sign pos (s ^ "(" ^ s' ^ ")")) + | tptp_of_type_literal pos (TyLitFree (s, name)) = + nice_name name #>> (fn s' => tptp_sign pos (s ^ "(" ^ s' ^ ")")) fun tptp_cnf name kind formula = "cnf(" ^ name ^ ", " ^ kind ^ ",\n " ^ formula ^ ").\n" fun gen_tptp_cls (cls_id, ax_name, Axiom, lits, tylits) = tptp_cnf (string_of_clausename (cls_id, ax_name)) "axiom" - (tptp_pack (tylits @ lits)) + (tptp_clause (tylits @ lits)) | gen_tptp_cls (cls_id, ax_name, Conjecture, lits, _) = tptp_cnf (string_of_clausename (cls_id, ax_name)) "negated_conjecture" - (tptp_pack lits) + (tptp_clause lits) fun tptp_tfree_clause tfree_lit = - tptp_cnf "tfree_tcs" "negated_conjecture" (tptp_pack [tfree_lit]) + tptp_cnf "tfree_tcs" "negated_conjecture" (tptp_clause [tfree_lit]) fun tptp_of_arLit (TConsLit (c,t,args)) = tptp_sign true (make_type_class c ^ "(" ^ t ^ paren_pack args ^ ")") @@ -586,11 +593,11 @@ fun tptp_arity_clause (ArityClause{axiom_name,conclLit,premLits,...}) = tptp_cnf (string_of_ar axiom_name) "axiom" - (tptp_pack (map tptp_of_arLit (conclLit :: premLits))) + (tptp_clause (map tptp_of_arLit (conclLit :: premLits))) fun tptp_classrelLits sub sup = let val tvar = "(T)" - in tptp_pack [tptp_sign false (sub^tvar), tptp_sign true (sup^tvar)] end; + in tptp_clause [tptp_sign false (sub^tvar), tptp_sign true (sup^tvar)] end; fun tptp_classrel_clause (ClassrelClause {axiom_name,subclass,superclass,...}) = tptp_cnf axiom_name "axiom" (tptp_classrelLits subclass superclass) diff -r 8ff45c2076da -r 81dc2c20f052 src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Thu Apr 29 01:17:14 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Thu Apr 29 10:25:26 2010 +0200 @@ -302,9 +302,13 @@ (* Given a clause, returns its literals paired with a list of literals concerning TFrees; the latter should only occur in conjecture clauses. *) -fun tptp_type_literals params pos (HOLClause {literals, ctypes_sorts, ...}) = - pool_map (tptp_literal params) literals - #>> rpair (map (tptp_of_typeLit pos) (add_typs ctypes_sorts)) +fun tptp_type_literals params pos (HOLClause {literals, ctypes_sorts, ...}) + pool = + 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 + in ((lits, tylits), pool) end fun tptp_clause params (cls as HOLClause {axiom_name, clause_id, kind, ...}) pool = @@ -323,7 +327,7 @@ fun dfg_type_literals params pos (HOLClause {literals, ctypes_sorts, ...}) = pool_map (dfg_literal params) literals - #>> rpair (map (dfg_of_typeLit pos) (add_typs ctypes_sorts)) + #>> rpair (map (dfg_of_type_literal pos) (add_type_literals ctypes_sorts)) fun get_uvars (CombConst _) vars pool = (vars, pool) | get_uvars (CombVar (name, _)) vars pool = diff -r 8ff45c2076da -r 81dc2c20f052 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu Apr 29 01:17:14 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu Apr 29 10:25:26 2010 +0200 @@ -377,16 +377,18 @@ (*Update TVars/TFrees with detected sort constraints.*) fun repair_sorts vt = - let fun tysubst (Type (a, Ts)) = Type (a, map tysubst Ts) - | tysubst (TVar (xi, s)) = TVar (xi, the_default s (Vartab.lookup vt xi)) - | tysubst (TFree (x, s)) = TFree (x, the_default s (Vartab.lookup vt (x, ~1))) - fun tmsubst (Const (a, T)) = Const (a, tysubst T) - | tmsubst (Free (a, T)) = Free (a, tysubst T) - | tmsubst (Var (xi, T)) = Var (xi, tysubst T) - | tmsubst (t as Bound _) = t - | tmsubst (Abs (a, T, t)) = Abs (a, tysubst T, tmsubst t) - | tmsubst (t1 $ t2) = tmsubst t1 $ tmsubst t2 - in not (Vartab.is_empty vt) ? tmsubst end + 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))) + 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) + | do_term (t as Bound _) = t + | do_term (Abs (a, T, t)) = Abs (a, do_type T, do_term t) + | do_term (t1 $ t2) = do_term t1 $ do_term t2 + in not (Vartab.is_empty vt) ? do_term end fun unskolemize_term t = fold forall_of (Term.add_consts t [] @@ -414,7 +416,7 @@ let val (vt, t) = lits_of_nodes (ProofContext.theory_of ctxt) (vt, []) us in t |> repair_sorts vt end -fun check_clause ctxt = +fun check_formula ctxt = TypeInfer.constrain HOLogic.boolT #> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt) @@ -450,7 +452,7 @@ val t2 = clause_of_nodes ctxt vt us val (t1, t2) = HOLogic.eq_const HOLogic.typeT $ t1 $ t2 - |> unvarify_args |> uncombine_term |> check_clause ctxt + |> unvarify_args |> uncombine_term |> check_formula ctxt |> HOLogic.dest_eq in (Definition (num, t1, t2), @@ -459,7 +461,7 @@ | decode_line vt (Inference (num, us, deps)) ctxt = let val t = us |> clause_of_nodes ctxt vt - |> unskolemize_term |> uncombine_term |> check_clause ctxt + |> unskolemize_term |> uncombine_term |> check_formula ctxt in (Inference (num, t, deps), fold Variable.declare_term (OldTerm.term_frees t) ctxt) @@ -655,12 +657,13 @@ "drop_ls" are those that should be dropped in a case split. *) type backpatches = (label * facts) list * (label list * label list) -fun using_of_step (Have (_, _, _, by)) = +fun used_labels_of_step (Have (_, _, _, by)) = (case by of Facts (ls, _) => ls - | CaseSplit (proofs, (ls, _)) => fold (union (op =) o using_of) proofs ls) - | using_of_step _ = [] -and using_of proof = fold (union (op =) o using_of_step) proof [] + | CaseSplit (proofs, (ls, _)) => + fold (union (op =) o used_labels_of) proofs ls) + | used_labels_of_step _ = [] +and used_labels_of proof = fold (union (op =) o used_labels_of_step) proof [] fun new_labels_of_step (Fix _) = [] | new_labels_of_step (Let _) = [] @@ -681,7 +684,7 @@ if forall (fn Have ([], l', t', _) :: _ => (l, t) = (l', t') | _ => false) (tl proofs) andalso not (exists (member (op =) (maps new_labels_of proofs)) - (using_of proof_tail)) then + (used_labels_of proof_tail)) then SOME (l, t, map rev proofs, proof_tail) else NONE @@ -823,17 +826,17 @@ fun kill_useless_labels_in_proof proof = let - val used_ls = using_of proof + val used_ls = used_labels_of proof fun do_label l = if member (op =) used_ls l then l else no_label - fun kill (Assume (l, t)) = Assume (do_label l, t) - | kill (Have (qs, l, t, by)) = + fun do_step (Assume (l, t)) = Assume (do_label l, t) + | do_step (Have (qs, l, t, by)) = Have (qs, do_label l, t, case by of CaseSplit (proofs, facts) => - CaseSplit (map (map kill) proofs, facts) + CaseSplit (map (map do_step) proofs, facts) | _ => by) - | kill step = step - in map kill proof end + | do_step step = step + in map do_step proof end fun prefix_for_depth n = replicate_string (n + 1) @@ -891,11 +894,9 @@ else if member (op =) qs Show then "show" else "have") val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt) - fun do_using [] = "" - | do_using ls = "using " ^ (space_implode " " (map do_raw_label ls)) ^ " " - fun do_by_facts [] = "by metis" - | do_by_facts ss = "by (metis " ^ space_implode " " ss ^ ")" - fun do_facts (ls, ss) = do_using ls ^ do_by_facts ss + fun do_facts ([], []) = "by metis" + | do_facts (ls, ss) = + "by (metis " ^ space_implode " " (map do_raw_label ls @ ss) ^ ")" and do_step ind (Fix xs) = do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n" | do_step ind (Let (t1, t2)) =