--- a/doc-src/Sledgehammer/sledgehammer.tex Thu May 12 15:29:19 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Thu May 12 15:29:19 2011 +0200
@@ -566,10 +566,6 @@
following values:
\begin{enum}
-%\item[$\bullet$] \textbf{\textit{poly\_types}:} Use the prover's support for
-%polymorphic first-order logic if available; otherwise, fall back on
-%\textit{poly\_preds}.
-
\item[$\bullet$] \textbf{\textit{poly\_preds}:} Types are encoded using a predicate
$\mathit{has\_type\/}(\tau, t)$ that restricts the range of bound variables.
Constants are annotated with their types, supplied as extra arguments, to
@@ -615,8 +611,8 @@
\item[$\bullet$]
\textbf{%
-\textit{simple\_types}?,
-\{\textit{mono},\textit{mangled}\}\textit{\_}\{\textit{preds},\textit{tags}\}?:} \\
+\textit{mono\_preds}?, \textit{mono\_tags}?, \textit{simple\_types}?, \\
+\textit{mangled\_preds}?, \textit{mangled\_tags}?:} \\
The type systems \textit{mono\_preds}, \textit{mono\_tags}, \textit{simple\_types},
\textit{mangled\_preds}, and \textit{mangled\_tags} are fully typed and
virtually sound---except for pathological cases, all found proofs are
@@ -628,8 +624,8 @@
\item[$\bullet$]
\textbf{%
-\textit{simple\_types}!,
-\{\textit{poly},\textit{mono},\textit{mangled}\}\textit{\_}\{\textit{preds},\textit{tags}\}!:} \\
+\textit{poly\_tags}!, \textit{mono\_preds}!, \textit{mono\_tags}!, \\
+\textit{simple\_types}!, \textit{mangled\_preds}!, \textit{mangled\_tags}!:} \\
The type systems \textit{poly\_preds}, \textit{poly\_tags},
\textit{mono\_preds}, \textit{mono\_tags}, \textit{simple\_types},
\textit{mangled\_preds}, and \textit{mangled\_tags} also admit a somewhat
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Thu May 12 15:29:19 2011 +0200
@@ -120,13 +120,22 @@
|> (fn (poly, (level, core)) =>
case (core, (poly, level)) of
("simple_types", (NONE, level)) => Simple_Types level
+ | ("preds", (SOME Polymorphic, level)) =>
+ if level = All_Types then Preds (Polymorphic, level)
+ else raise Same.SAME
| ("preds", (SOME poly, level)) => Preds (poly, level)
+ | ("tags", (SOME Polymorphic, level)) =>
+ if level = All_Types orelse level = Finite_Types then
+ Tags (Polymorphic, level)
+ else
+ raise Same.SAME
| ("tags", (SOME poly, level)) => Tags (poly, level)
| ("args", (SOME poly, All_Types (* naja *))) =>
Preds (poly, Const_Arg_Types)
| ("erased", (NONE, All_Types (* naja *))) =>
Preds (Polymorphic, No_Types)
- | _ => error ("Unknown type system: " ^ quote s ^ "."))
+ | _ => raise Same.SAME)
+ handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
fun polymorphism_of_type_sys (Simple_Types _) = Mangled_Monomorphic
| polymorphism_of_type_sys (Preds (poly, _)) = poly
@@ -188,23 +197,32 @@
| _ => polymorphism_of_type_sys type_sys <> Mangled_Monomorphic andalso
member (op =) boring_consts s))
-datatype type_arg_policy = No_Type_Args | Explicit_Type_Args | Mangled_Type_Args
+(* The Booleans indicate whether all type arguments should be kept. *)
+datatype type_arg_policy =
+ Explicit_Type_Args of bool |
+ Mangled_Type_Args of bool |
+ No_Type_Args
+(* FIXME: Find out whether and when erasing the non-result type arguments is
+ sound. *)
fun general_type_arg_policy type_sys =
if level_of_type_sys type_sys = No_Types then
No_Type_Args
else if polymorphism_of_type_sys type_sys = Mangled_Monomorphic then
- Mangled_Type_Args
+ Mangled_Type_Args (is_type_sys_virtually_sound type_sys)
else
- Explicit_Type_Args
+ Explicit_Type_Args (is_type_sys_virtually_sound type_sys)
fun type_arg_policy type_sys s =
if should_omit_type_args type_sys s then No_Type_Args
else general_type_arg_policy type_sys
fun num_atp_type_args thy type_sys s =
- if type_arg_policy type_sys s = Explicit_Type_Args then num_type_args thy s
- else 0
+ case type_arg_policy type_sys s of
+ Explicit_Type_Args keep_all =>
+ if keep_all then num_type_args thy s
+ else error "not implemented yet" (* FIXME *)
+ | _ => 0
fun atp_type_literals_for_types type_sys kind Ts =
if level_of_type_sys type_sys = No_Types then
@@ -589,10 +607,31 @@
| (head, args) => list_explicit_app head (map aux args)
in aux end
-fun impose_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys =
+fun chop_fun 0 T = ([], T)
+ | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) =
+ chop_fun (n - 1) ran_T |>> cons dom_T
+ | chop_fun _ _ = raise Fail "unexpected non-function"
+
+fun filter_type_args thy s arity T_args =
let
- fun aux (CombApp tmp) = CombApp (pairself aux tmp)
- | aux (CombConst (name as (s, _), T, T_args)) =
+ val U = s |> Sign.the_const_type thy (* may throw "TYPE" *)
+ val res_U = U |> chop_fun arity |> snd
+ val res_U_vars = Term.add_tvarsT res_U []
+ val U_args = (s, U) |> Sign.const_typargs thy
+ in
+ U_args ~~ T_args
+ |> map_filter (fn (U, T) =>
+ if member (op =) res_U_vars (dest_TVar U) then SOME T
+ else NONE)
+ end
+ handle TYPE _ => T_args
+
+fun enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ fun aux arity (CombApp (tm1, tm2)) =
+ CombApp (aux (arity + 1) tm1, aux 0 tm2)
+ | aux arity (CombConst (name as (s, _), T, T_args)) =
let
val level = level_of_type_sys type_sys
val (T, T_args) =
@@ -604,7 +643,7 @@
not (is_type_sys_virtually_sound type_sys) then
T_args |> map (homogenized_type ctxt nonmono_Ts level)
|> (fn Ts => let val T = hd Ts --> nth Ts 1 in
- (T --> T, tl Ts)
+ (T --> T, tl Ts) (* ### FIXME: need tl? *)
end)
else
(T, T_args)
@@ -612,21 +651,26 @@
(case strip_prefix_and_unascii const_prefix s of
NONE => (name, T_args)
| SOME s'' =>
- let val s'' = invert_const s'' in
+ let
+ val s'' = invert_const s''
+ fun filtered_T_args true = T_args
+ | filtered_T_args false = filter_type_args thy s'' arity T_args
+ in
case type_arg_policy type_sys s'' of
- No_Type_Args => (name, [])
- | Explicit_Type_Args => (name, T_args)
- | Mangled_Type_Args => (mangled_const_name T_args name, [])
+ Explicit_Type_Args keep_all => (name, filtered_T_args keep_all)
+ | Mangled_Type_Args keep_all =>
+ (mangled_const_name (filtered_T_args keep_all) name, [])
+ | No_Type_Args => (name, [])
end)
|> (fn (name, T_args) => CombConst (name, T, T_args))
end
- | aux tm = tm
- in aux end
+ | aux _ tm = tm
+ in aux 0 end
fun repair_combterm ctxt nonmono_Ts type_sys sym_tab =
introduce_explicit_apps_in_combterm sym_tab
#> introduce_predicators_in_combterm sym_tab
- #> impose_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys
+ #> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys
fun repair_fact ctxt nonmono_Ts type_sys sym_tab =
update_combformula (formula_map
(repair_combterm ctxt nonmono_Ts type_sys sym_tab))
@@ -653,7 +697,9 @@
((c ^ "_" ^ string_of_int j ^ (if needs_some_types then "T" else ""),
Chained),
let val t = th |> prop_of in
- t |> (general_type_arg_policy type_sys = Mangled_Type_Args andalso
+ t |> ((case general_type_arg_policy type_sys of
+ Mangled_Type_Args _ => true
+ | _ => false) andalso
not (null (Term.hidden_polymorphism t)))
? (case typ of
SOME T => specialize_type thy (invert_const unmangled_s, T)
@@ -716,14 +762,14 @@
fun type_pred_combatom ctxt nonmono_Ts type_sys T tm =
CombApp (CombConst (`make_fixed_const type_pred_base, T --> @{typ bool}, [T]),
tm)
- |> impose_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys
+ |> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys
|> AAtom
fun formula_from_combformula ctxt nonmono_Ts type_sys =
let
fun tag_with_type type_sys T tm =
CombConst (`make_fixed_const type_tag_name, T --> T, [T])
- |> impose_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys
+ |> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys
|> do_term true
|> (fn ATerm (s, tms) => ATerm (s, tms @ [tm]))
and do_term top_level u =
@@ -852,7 +898,7 @@
fun should_declare_sym type_sys pred_sym s =
not (String.isPrefix bound_var_prefix s) andalso s <> "equal" andalso
- not (String.isPrefix "$" s) andalso
+ not (String.isPrefix tptp_special_prefix s) andalso
((case type_sys of Simple_Types _ => true | _ => false) orelse not pred_sym)
fun sym_decl_table_for_facts type_sys repaired_sym_tab (conjs, facts) =
@@ -904,15 +950,10 @@
(* in case helper "True_or_False" is included *)
#> insert_type I @{typ bool})
-fun n_ary_strip_type 0 T = ([], T)
- | n_ary_strip_type n (Type (@{type_name fun}, [dom_T, ran_T])) =
- n_ary_strip_type (n - 1) ran_T |>> cons dom_T
- | n_ary_strip_type _ _ = raise Fail "unexpected non-function"
-
-fun result_type_of_decl (_, _, T, _, ary, _) = n_ary_strip_type ary T |> snd
+fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
fun decl_line_for_sym s (s', _, T, pred_sym, ary, _) =
- let val (arg_Ts, res_T) = n_ary_strip_type ary T in
+ let val (arg_Ts, res_T) = chop_fun ary T in
Decl (sym_decl_prefix ^ s, (s, s'), map mangled_type_name arg_Ts,
if pred_sym then `I tptp_tff_bool_type else mangled_type_name res_T)
end
@@ -925,7 +966,7 @@
val (kind, maybe_negate) =
if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
else (Axiom, I)
- val (arg_Ts, res_T) = n_ary_strip_type ary T
+ val (arg_Ts, res_T) = chop_fun ary T
val bound_names =
1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
val bound_tms =
@@ -1073,7 +1114,7 @@
fun add_term_weights weight (ATerm (s, tms)) =
(not (is_atp_variable s) andalso s <> "equal" andalso
- not (String.isPrefix "$" s)) ? Symtab.default (s, weight)
+ not (String.isPrefix tptp_special_prefix s)) ? Symtab.default (s, weight)
#> fold (add_term_weights weight) tms
fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) =
formula_fold true (K (add_term_weights weight)) phi