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)
--- 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
--- 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)
--- 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 =
--- 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)) =