restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags"
--- a/doc-src/Sledgehammer/sledgehammer.tex Sun May 01 18:37:25 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Sun May 01 18:37:25 2011 +0200
@@ -578,57 +578,71 @@
Monomorphization can simplify reasoning but also leads to larger fact bases,
which can slow down the ATPs.
-\item[$\bullet$] \textbf{\textit{mangled}:} Types are mangled in constant names,
-and predicates restrict the range of bound variables. The problem is
-monomorphized. This corresponds to the traditional encoding of types in an
-untyped logic without overloading (e.g., such as performed by the ToFoF-E
-wrapper).
+\item[$\bullet$] \textbf{\textit{preds}:} Types are encoded using a binary predicate
+$\mathit{has\_type\/}(\tau, t)$ that restricts the range of bound variables.
+Constants are annotated with their types, supplied as extra arguments, to
+resolve overloading.
-\item[$\bullet$] \textbf{\textit{args}:} Constants are annotated with their
-types, which are supplied as extra arguments.
+\item[$\bullet$] \textbf{\textit{mono\_preds}:} Similar to \textit{preds}, but
+the problem is additionally monomorphized. This corresponds to the traditional
+encoding of types in an untyped logic without overloading (e.g., such as
+performed by the ToFoF-E wrapper).
-\item[$\bullet$] \textbf{\textit{mono\_args}:} Similar to \textit{args}, but
-the problem is additionally monomorphized.
+\item[$\bullet$] \textbf{\textit{mangled\_preds}:} Similar to
+\textit{mono\_preds}, but types are mangled in constant names instead of being
+supplied as ground term arguments. The binary predicate
+$\mathit{has\_type\/}(\tau, t)$ becomes a unary predicate
+$\mathit{has\_type\_}\tau(t)$.
-\item[$\bullet$] \textbf{\textit{tags}:} Each term (and subterm) is tagged with
-its type using a special uninterpreted function symbol.
+\item[$\bullet$] \textbf{\textit{tags}:} Each term and subterm is tagged with
+its type using a function $\mathit{type\_info\/}(\tau, t)$.
\item[$\bullet$] \textbf{\textit{mono\_tags}:} Similar to \textit{tags}, but
the problem is additionally monomorphized.
-\item[$\bullet$] \textbf{\textit{none}:} No type information is supplied to the
-ATP.
+\item[$\bullet$] \textbf{\textit{mangled\_tags}:} Similar to
+\textit{mono\_tags}, but types are mangled in constant names instead of being
+supplied as ground term arguments. The binary function
+$\mathit{type\_info\/}(\tau, t)$ becomes a unary function
+$\mathit{type\_info\_}\tau(t)$.
+
+\item[$\bullet$]
+\textbf{%
+\textit{preds}!,
+\textit{mono\_preds}!,
+\textit{mangled\_preds}!, \\
+\textit{tags}!,
+\textit{mono\_tags}!,
+\textit{mangled\_tags}!:} \\
+The type systems \textit{preds}, \textit{mono\_preds}, \textit{mangled\_preds},
+\textit{tags}, \textit{mono\_tags}, and \textit{mangled\_tags} are fully typed
+and virtually sound. For each of these, Sledgehammer also provides a mildly
+unsound variant identified by an exclamation mark (!)\ that types only finite
+(and hence especially dangerous) types.
\item[$\bullet$]
\textbf{%
-\textit{many\_typed}!,
-\textit{mangled}!,
-\textit{args}!,
-\textit{mono\_args}!,
-\textit{tags}!, \\ %% TYPESETTING
-\textit{mono\_tags}!:}
-The type systems \textit{many\_typed}, \textit{mangled},
-(\textit{mono\_})\allowbreak\textit{args}, and
-(\textit{mono\_})\allowbreak\textit{tags} are fully typed and (virtually) sound.
-For each of these, Sledgehammer also provides a mildly unsound variant
-identified by one exclamation mark suffix (!).
+\textit{preds}?,
+\textit{mono\_preds}?,
+\textit{mangled\_preds}?, \\
+\textit{tags}?,
+\textit{mono\_tags}?,
+\textit{mangled\_tags}?:} \\
+If the exclamation mark (!) is replaced by an question mark (?), the type
+systems type only nonmonotonic (and hence especially dangerous) types. Not
+implemented yet.
-\item[$\bullet$]
-\textbf{%
-\textit{many\_typed}!!,
-\textit{mangled}!!,
-\textit{args}!!,
-\textit{mono\_args}!!,
-\textit{tags}!!, \\ %% TYPESETTING
-\textit{mono\_tags}!!:}
-More strongly unsound variants of \textit{many\_typed}, \textit{mangled},
-(\textit{mono\_})\allowbreak\textit{args}, and
-(\textit{mono\_})\allowbreak\textit{tags}, identified by two exclamation marks
-(!!).
+\item[$\bullet$] \textbf{\textit{const\_args}:}
+Constants are annotated with their types, supplied as extra arguments, to
+resolve overloading. Variables are unbounded.
+
+\item[$\bullet$] \textbf{\textit{erased}:} No type information is supplied to
+the ATP. Types are simply erased.
\item[$\bullet$] \textbf{\textit{smart}:} If \textit{full\_types} is enabled,
-uses a fully typed encoding; otherwise, uses a partially typed encoding. The
-actual encoding used depends on the ATP.
+uses a fully typed, virtually sound encoding; otherwise, uses any encoding. The
+actual encoding used depends on the ATP and should be the most efficient for
+that ATP.
\end{enum}
For SMT solvers and ToFoF-E, the type system is always \textit{many\_typed}.
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sun May 01 18:37:25 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sun May 01 18:37:25 2011 +0200
@@ -377,7 +377,8 @@
Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover_name
val relevance_override = {add = [], del = [], only = false}
val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
- val half_sound = Sledgehammer_Provers.is_rich_type_sys_half_sound type_sys
+ val fairly_sound =
+ Sledgehammer_Provers.is_rich_type_sys_fairly_sound type_sys
val time_limit =
(case hard_timeout of
NONE => I
@@ -387,7 +388,7 @@
time_isa) = time_limit (Mirabelle.cpu_time (fn () =>
let
val facts =
- Sledgehammer_Filter.relevant_facts ctxt half_sound
+ Sledgehammer_Filter.relevant_facts ctxt fairly_sound
relevance_thresholds
(the_default default_max_relevant max_relevant) is_built_in_const
relevance_fudge relevance_override chained_ths hyp_ts concl_t
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Sun May 01 18:37:25 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Sun May 01 18:37:25 2011 +0200
@@ -117,18 +117,18 @@
val default_max_relevant =
Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing
prover
- val is_built_in_const =
- Sledgehammer_Provers.is_built_in_const_for_prover ctxt default_prover
+ val is_built_in_const =
+ Sledgehammer_Provers.is_built_in_const_for_prover ctxt default_prover
val relevance_fudge =
extract_relevance_fudge args
(Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover)
val relevance_override = {add = [], del = [], only = false}
val subgoal = 1
val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal subgoal
- val half_sound =
- Sledgehammer_Provers.is_rich_type_sys_half_sound type_sys
+ val fairly_sound =
+ Sledgehammer_Provers.is_rich_type_sys_fairly_sound type_sys
val facts =
- Sledgehammer_Filter.relevant_facts ctxt half_sound
+ Sledgehammer_Filter.relevant_facts ctxt fairly_sound
relevance_thresholds
(the_default default_max_relevant max_relevant) is_built_in_const
relevance_fudge relevance_override facts hyp_ts concl_t
--- a/src/HOL/Tools/ATP/atp_problem.ML Sun May 01 18:37:25 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Sun May 01 18:37:25 2011 +0200
@@ -164,7 +164,7 @@
| keep (c :: cs) = c :: keep cs
in String.explode #> rev #> keep #> rev #> String.implode end
-val max_readable_name_length = 32
+val max_readable_name_length = 24
(* "op" is also reserved, to avoid the unreadable "op_1", "op_2", etc., in the
problem files. "equal" is reserved by some ATPs. "eq" is reserved to ensure
@@ -184,7 +184,7 @@
if size s > max_readable_name_length then
String.substring (s, 0, max_readable_name_length div 2 - 4) ^
Word.toString (hashw_string (full_name, 0w0)) ^
- String.extract (s, max_readable_name_length div 2 - 4, NONE)
+ String.extract (s, max_readable_name_length div 2 + 4, NONE)
else
s)
|> (fn s => if member (op =) reserved_nice_names s then full_name else s)
--- a/src/HOL/Tools/ATP/atp_systems.ML Sun May 01 18:37:25 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Sun May 01 18:37:25 2011 +0200
@@ -11,13 +11,14 @@
type formula_kind = ATP_Problem.formula_kind
type failure = ATP_Proof.failure
- datatype type_level = Sound | Half_Sound | Unsound
+ datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
+ datatype type_level =
+ All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
+
datatype type_system =
Many_Typed |
- Mangled of type_level |
- Args of bool * type_level |
- Tags of bool * type_level |
- No_Types
+ Preds of polymorphism * type_level |
+ Tags of polymorphism * type_level
type atp_config =
{exec : string * string,
@@ -33,7 +34,10 @@
datatype e_weight_method =
E_Slices | E_Auto | E_Fun_Weight | E_Sym_Offset_Weight
+ val polymorphism_of_type_sys : type_system -> polymorphism
val level_of_type_sys : type_system -> type_level
+ val is_type_sys_virtually_sound : type_system -> bool
+ val is_type_sys_fairly_sound : type_system -> bool
(* for experimentation purposes -- do not use in production code *)
val e_weight_method : e_weight_method Unsynchronized.ref
val e_default_fun_weight : real Unsynchronized.ref
@@ -71,19 +75,31 @@
(* ATP configuration *)
-datatype type_level = Sound | Half_Sound | Unsound
+datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
+datatype type_level =
+ All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
+
datatype type_system =
Many_Typed |
- Mangled of type_level |
- Args of bool * type_level |
- Tags of bool * type_level |
- No_Types
+ Preds of polymorphism * type_level |
+ Tags of polymorphism * type_level
+
+fun polymorphism_of_type_sys Many_Typed = Mangled_Monomorphic
+ | polymorphism_of_type_sys (Preds (poly, _)) = poly
+ | polymorphism_of_type_sys (Tags (poly, _)) = poly
-fun level_of_type_sys Many_Typed = Sound
- | level_of_type_sys (Mangled level) = level
- | level_of_type_sys (Args (_, level)) = level
+fun level_of_type_sys Many_Typed = All_Types
+ | level_of_type_sys (Preds (_, level)) = level
| level_of_type_sys (Tags (_, level)) = level
- | level_of_type_sys No_Types = Unsound
+
+val is_type_level_virtually_sound =
+ member (op =) [All_Types, Nonmonotonic_Types]
+val is_type_sys_virtually_sound =
+ is_type_level_virtually_sound o level_of_type_sys
+
+fun is_type_level_fairly_sound level =
+ is_type_level_virtually_sound level orelse level = Finite_Types
+val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys
type atp_config =
{exec : string * string,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Sun May 01 18:37:25 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Sun May 01 18:37:25 2011 +0200
@@ -194,7 +194,7 @@
| using_labels ls =
"using " ^ space_implode " " (map string_for_label ls) ^ " "
fun metis_name type_sys =
- if level_of_type_sys type_sys = Unsound then "metis" else "metisFT"
+ if is_type_sys_fairly_sound type_sys then "metisFT" else "metis"
fun metis_call type_sys ss = command_call (metis_name type_sys) ss
fun metis_command type_sys i n (ls, ss) =
using_labels ls ^ apply_on_subgoal "" i n ^ metis_call type_sys ss
@@ -342,12 +342,7 @@
fun aux opt_T extra_us u =
case u of
ATerm (a, us) =>
- if a = type_tag_name then
- case us of
- [typ_u, term_u] =>
- aux (SOME (typ_from_fo_term tfrees typ_u)) extra_us term_u
- | _ => raise FO_TERM us
- else if String.isPrefix tff_type_prefix a then
+ if String.isPrefix tff_type_prefix a then
@{const True} (* ignore TFF type information *)
else case strip_prefix_and_unascii const_prefix a of
SOME "equal" =>
@@ -360,7 +355,12 @@
end
| SOME b =>
let val (b, mangled_us) = b |> unmangled_const |>> invert_const in
- if b = predicator_base then
+ if b = type_tag_name then
+ case mangled_us @ us of
+ [typ_u, term_u] =>
+ aux (SOME (typ_from_fo_term tfrees typ_u)) extra_us term_u
+ | _ => raise FO_TERM us
+ else if b = predicator_base then
aux (SOME @{typ bool}) [] (hd us)
else if b = explicit_app_base then
aux opt_T (nth us 1 :: extra_us) (hd us)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sun May 01 18:37:25 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sun May 01 18:37:25 2011 +0200
@@ -42,7 +42,9 @@
open Sledgehammer_Util
(* Readable names are often much shorter, especially if types are mangled in
- names. For that reason, they are on by default. *)
+ names. Also, the logic for generating legal SNARK sort names is only
+ implemented for readable names. Finally, readable names are, well, more
+ readable. For these reason, they are enabled by default. *)
val readable_names = Unsynchronized.ref true
val type_decl_prefix = "type_"
@@ -91,29 +93,25 @@
fun fact_lift f ({combformula, ...} : translated_formula) = f combformula
-fun type_sys_declares_sym_types Many_Typed = true
- | type_sys_declares_sym_types (Mangled level) = level <> Unsound
- | type_sys_declares_sym_types (Args (_, level)) = level <> Unsound
- | type_sys_declares_sym_types _ = false
-
val boring_consts = [explicit_app_base, @{const_name Metis.fequal}]
fun should_omit_type_args type_sys s =
- s <> type_pred_base andalso
- (s = @{const_name HOL.eq} orelse
- case type_sys of
- Many_Typed => false
- | Mangled _ => false
- | Tags (_, Sound) => true
- | No_Types => true
- | _ => member (op =) boring_consts s)
+ s <> type_pred_base andalso s <> type_tag_name andalso
+ (s = @{const_name HOL.eq} orelse level_of_type_sys type_sys = No_Types orelse
+ (case type_sys of
+ Tags (_, All_Types) => true
+ | _ => 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
-datatype type_arg_policy = No_Type_Args | Mangled_Types | Explicit_Type_Args
-
-fun general_type_arg_policy Many_Typed = Mangled_Types
- | general_type_arg_policy (Mangled _) = Mangled_Types
- | general_type_arg_policy No_Types = No_Type_Args
- | general_type_arg_policy _ = Explicit_Type_Args
+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
+ else
+ Explicit_Type_Args
fun type_arg_policy type_sys s =
if should_omit_type_args type_sys s then No_Type_Args
@@ -124,7 +122,7 @@
else 0
fun atp_type_literals_for_types type_sys kind Ts =
- if type_sys = No_Types then
+ if level_of_type_sys type_sys = No_Types then
[]
else
Ts |> type_literals_for_types
@@ -486,8 +484,8 @@
let val s'' = invert_const s'' in
case type_arg_policy type_sys s'' of
No_Type_Args => (name, [])
- | Mangled_Types => (mangled_const_name T_args name, [])
| Explicit_Type_Args => (name, T_args)
+ | Mangled_Type_Args => (mangled_const_name T_args name, [])
end)
|> (fn (name, T_args) => CombConst (name, T, T_args))
| aux tm = tm
@@ -504,7 +502,7 @@
fun ti_ti_helper_fact () =
let
fun var s = ATerm (`I s, [])
- fun tag tm = ATerm (`I type_tag_name, [var "X", tm])
+ fun tag tm = ATerm (`make_fixed_const type_tag_name, [var "X", tm])
in
Formula (helper_prefix ^ ascii_of "ti_ti", Axiom,
AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")]))
@@ -521,7 +519,7 @@
((c ^ "_" ^ string_of_int j ^ (if needs_some_types then "T" else ""),
false),
let val t = th |> prop_of in
- t |> (general_type_arg_policy type_sys = Mangled_Types andalso
+ t |> (general_type_arg_policy type_sys = Mangled_Type_Args andalso
not (null (Term.hidden_polymorphism t)))
? (case typ of
SOME T => specialize_type thy (invert_const unmangled_s, T)
@@ -529,12 +527,12 @@
end)
fun make_facts eq_as_iff =
map_filter (make_fact ctxt false eq_as_iff false)
+ val has_some_types = is_type_sys_fairly_sound type_sys
in
metis_helpers
|> maps (fn (metis_s, (needs_some_types, ths)) =>
if metis_s <> unmangled_s orelse
- (needs_some_types andalso
- level_of_type_sys type_sys = Unsound) then
+ (needs_some_types andalso not has_some_types) then
[]
else
ths ~~ (1 upto length ths)
@@ -567,15 +565,13 @@
val tycons = type_consts_of_terms thy all_ts
val conjs = make_conjecture ctxt (hyp_ts @ [concl_t])
val (supers', arity_clauses) =
- if type_sys = No_Types then ([], [])
+ if level_of_type_sys type_sys = No_Types then ([], [])
else make_arity_clauses thy tycons supers
val class_rel_clauses = make_class_rel_clauses thy subs supers'
in
(fact_names |> map single, (conjs, facts, class_rel_clauses, arity_clauses))
end
-fun tag_with_type ty tm = ATerm (`I type_tag_name, [ty, tm])
-
fun fo_literal_from_type_literal (TyLitVar (class, name)) =
(true, ATerm (class, [ATerm (name, [])]))
| fo_literal_from_type_literal (TyLitFree (class, name)) =
@@ -588,39 +584,39 @@
unsound ATP proofs. The checks below are an (unsound) approximation of
finiteness. *)
-fun is_dtyp_dangerous _ (Datatype_Aux.DtTFree _) = true
- | is_dtyp_dangerous ctxt (Datatype_Aux.DtType (s, Us)) =
- is_type_constr_dangerous ctxt s andalso forall (is_dtyp_dangerous ctxt) Us
- | is_dtyp_dangerous _ (Datatype_Aux.DtRec _) = false
-and is_type_dangerous ctxt (Type (s, Ts)) =
- is_type_constr_dangerous ctxt s andalso forall (is_type_dangerous ctxt) Ts
- | is_type_dangerous _ _ = false
-and is_type_constr_dangerous ctxt s =
+fun is_dtyp_finite _ (Datatype_Aux.DtTFree _) = true
+ | is_dtyp_finite ctxt (Datatype_Aux.DtType (s, Us)) =
+ is_type_constr_finite ctxt s andalso forall (is_dtyp_finite ctxt) Us
+ | is_dtyp_finite _ (Datatype_Aux.DtRec _) = false
+and is_type_finite ctxt (Type (s, Ts)) =
+ is_type_constr_finite ctxt s andalso forall (is_type_finite ctxt) Ts
+ | is_type_finite _ _ = false
+and is_type_constr_finite ctxt s =
let val thy = Proof_Context.theory_of ctxt in
case Datatype_Data.get_info thy s of
SOME {descr, ...} =>
forall (fn (_, (_, _, constrs)) =>
- forall (forall (is_dtyp_dangerous ctxt) o snd) constrs) descr
+ forall (forall (is_dtyp_finite ctxt) o snd) constrs) descr
| NONE =>
case Typedef.get_info ctxt s of
- ({rep_type, ...}, _) :: _ => is_type_dangerous ctxt rep_type
+ ({rep_type, ...}, _) :: _ => is_type_finite ctxt rep_type
| [] => true
end
-fun should_encode_type _ Sound _ = true
- | should_encode_type ctxt Half_Sound T = is_type_dangerous ctxt T
- | should_encode_type _ Unsound _ = false
+fun should_encode_type _ All_Types _ = true
+ | should_encode_type ctxt Finite_Types T = is_type_finite ctxt T
+ | should_encode_type _ Nonmonotonic_Types _ =
+ error "Monotonicity inference not implemented yet."
+ | should_encode_type _ _ _ = false
+
+fun should_predicate_on_type ctxt (Preds (_, level)) T =
+ should_encode_type ctxt level T
+ | should_predicate_on_type _ _ _ = false
fun should_tag_with_type ctxt (Tags (_, level)) T =
should_encode_type ctxt level T
| should_tag_with_type _ _ _ = false
-fun should_predicate_on_type ctxt (Mangled level) T =
- should_encode_type ctxt level T
- | should_predicate_on_type ctxt (Args (_, level)) T =
- should_encode_type ctxt level T
- | should_predicate_on_type _ _ _ = false
-
fun type_pred_combatom type_sys T tm =
CombApp (CombConst (`make_fixed_const type_pred_base, T --> @{typ bool}, [T]),
tm)
@@ -629,7 +625,12 @@
fun formula_from_combformula ctxt type_sys =
let
- fun do_term top_level u =
+ fun tag_with_type type_sys T tm =
+ CombConst (`make_fixed_const type_tag_name, T --> T, [T])
+ |> impose_type_arg_policy_in_combterm type_sys
+ |> do_term true
+ |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm]))
+ and do_term top_level u =
let
val (head, args) = strip_combterm_comb u
val (x, T_args) =
@@ -642,7 +643,7 @@
val T = combtyp_of u
in
t |> (if not top_level andalso should_tag_with_type ctxt type_sys T then
- tag_with_type (fo_term_from_typ T)
+ tag_with_type type_sys T
else
I)
end
@@ -735,7 +736,7 @@
let
fun declare_sym (decl as (_, _, T, _, _)) decls =
case type_sys of
- Tags (false, Sound) =>
+ Preds (Polymorphic, All_Types) =>
if exists (curry Type.raw_instance T o #3) decls then
decls
else
@@ -760,7 +761,7 @@
fact_lift (formula_fold
(add_combterm_syms_to_decl_table type_sys repaired_sym_tab))
fun sym_decl_table_for_facts type_sys repaired_sym_tab facts =
- Symtab.empty |> type_sys_declares_sym_types type_sys
+ Symtab.empty |> is_type_sys_fairly_sound type_sys
? fold (add_fact_syms_to_decl_table type_sys repaired_sym_tab)
facts
@@ -787,10 +788,8 @@
bound_names ~~ arg_Ts |> map (fn (name, T) => CombConst (name, T, []))
val bound_Ts =
arg_Ts |> map (if n > 1 then SOME else K NONE)
- val freshener =
- case type_sys of Args _ => string_of_int j ^ "_" | _ => ""
in
- Formula (sym_decl_prefix ^ freshener ^ "_" ^ ascii_of s, Axiom,
+ Formula (sym_decl_prefix ^ ascii_of s ^ "_" ^ string_of_int j, Axiom,
CombConst ((s, s'), T, T_args)
|> fold (curry (CombApp o swap)) bound_tms
|> type_pred_combatom type_sys res_T
@@ -884,7 +883,9 @@
(helpersN, map (formula_line_for_fact ctxt helper_prefix type_sys)
(0 upto length helpers - 1 ~~ helpers)
|> (case type_sys of
- Tags (_, Half_Sound) => cons (ti_ti_helper_fact ())
+ Tags (Polymorphic, level) =>
+ member (op =) [Finite_Types, Nonmonotonic_Types] level
+ ? cons (ti_ti_helper_fact ())
| _ => I)),
(conjsN, map (formula_line_for_conjecture ctxt type_sys) conjs),
(free_typesN, formula_lines_for_free_types type_sys (facts @ conjs))]
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Sun May 01 18:37:25 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Sun May 01 18:37:25 2011 +0200
@@ -777,17 +777,17 @@
(* Facts containing variables of type "unit" or "bool" or of the form
"ALL x. x = A | x = B | x = C" are likely to lead to unsound proofs if types
are omitted. *)
-fun is_dangerous_term half_sound t =
- not half_sound andalso
+fun is_dangerous_term fairly_sound t =
+ not fairly_sound andalso
let val t = transform_elim_term t in
has_bound_or_var_of_type dangerous_types t orelse
is_exhaustive_finite t
end
-fun is_theorem_bad_for_atps half_sound thm =
+fun is_theorem_bad_for_atps fairly_sound thm =
let val t = prop_of thm in
is_formula_too_complex t orelse exists_type type_has_top_sort t orelse
- is_dangerous_term half_sound t orelse exists_sledgehammer_const t orelse
+ is_dangerous_term fairly_sound t orelse exists_sledgehammer_const t orelse
exists_low_level_class_const t orelse is_metastrange_theorem thm orelse
is_that_fact thm
end
@@ -800,7 +800,7 @@
val simps = ctxt |> simpset_of |> dest_ss |> #simps |> map snd
in (mk_fact_table I intros, mk_fact_table I elims, mk_fact_table I simps) end
-fun all_facts ctxt reserved really_all half_sound
+fun all_facts ctxt reserved really_all fairly_sound
({intro_bonus, elim_bonus, simp_bonus, ...} : relevance_fudge)
add_ths chained_ths =
let
@@ -846,7 +846,7 @@
pair 1
#> fold (fn th => fn (j, rest) =>
(j + 1,
- if is_theorem_bad_for_atps half_sound th andalso
+ if is_theorem_bad_for_atps fairly_sound th andalso
not (member Thm.eq_thm add_ths th) then
rest
else
@@ -890,7 +890,7 @@
fun external_frees t =
[] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst)
-fun relevant_facts ctxt half_sound (threshold0, threshold1) max_relevant
+fun relevant_facts ctxt fairly_sound (threshold0, threshold1) max_relevant
is_built_in_const fudge (override as {add, only, ...})
chained_ths hyp_ts concl_t =
let
@@ -908,7 +908,7 @@
maps (map (fn ((name, loc), th) => ((K name, loc), (true, th)))
o fact_from_ref ctxt reserved chained_ths) add
else
- all_facts ctxt reserved false half_sound fudge add_ths chained_ths)
+ all_facts ctxt reserved false fairly_sound fudge add_ths chained_ths)
|> instantiate_inducts
? maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs)
|> rearrange_facts ctxt (respect_no_atp andalso not only)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sun May 01 18:37:25 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sun May 01 18:37:25 2011 +0200
@@ -235,22 +235,29 @@
|> auto ? single o hd
val type_sys = lookup_string "type_sys"
val type_sys =
- (case try (unprefix "mono_") type_sys of
- SOME s => (true, s)
- | NONE => (false, type_sys))
- ||> (fn s => case try (unsuffix " !!") s of
- SOME s => (Unsound, s)
- | NONE => case try (unsuffix " !") s of
- SOME s => (Half_Sound, s)
- | NONE => (Sound, s))
- |> (fn (mono, (level, core)) =>
- case (core, (mono, level)) of
- ("many_typed", (false, Sound)) => Dumb_Type_Sys Many_Typed
- | ("mangled", (false, level)) => Dumb_Type_Sys (Mangled level)
- | ("args", extra) => Dumb_Type_Sys (Args extra)
+ (case try (unprefix "mangled_") type_sys of
+ SOME s => (Mangled_Monomorphic, s)
+ | NONE =>
+ case try (unprefix "mono_") type_sys of
+ SOME s => (Monomorphic, s)
+ | NONE => (Polymorphic, type_sys))
+ ||> (fn s => case try (unsuffix " ?") s of
+ SOME s => (Nonmonotonic_Types, s)
+ | NONE =>
+ case try (unsuffix " !") s of
+ SOME s => (Finite_Types, s)
+ | NONE => (All_Types, s))
+ |> (fn (polymorphism, (level, core)) =>
+ case (core, (polymorphism, level)) of
+ ("many_typed", (Polymorphic (* naja *), All_Types)) =>
+ Dumb_Type_Sys Many_Typed
+ | ("preds", extra) => Dumb_Type_Sys (Preds extra)
| ("tags", extra) => Dumb_Type_Sys (Tags extra)
- | ("none", (false, Sound)) => Dumb_Type_Sys No_Types
- | ("smart", (false, Sound)) =>
+ | ("const_args", (_, All_Types (* naja *))) =>
+ Dumb_Type_Sys (Preds (polymorphism, Const_Arg_Types))
+ | ("erased", (Polymorphic, All_Types (* naja *))) =>
+ Dumb_Type_Sys (Preds (polymorphism, No_Types))
+ | ("smart", (Polymorphic, All_Types) (* naja *)) =>
Smart_Type_Sys (lookup_bool "full_types")
| _ => error ("Unknown type system: " ^ quote type_sys ^ "."))
val relevance_thresholds = lookup_real_pair "relevance_thresholds"
@@ -351,7 +358,7 @@
val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " "
val parse_value =
- Scan.repeat1 (Parse.xname || Parse.float_number || Parse.$$$ "!!"
+ Scan.repeat1 (Parse.xname || Parse.float_number || Parse.$$$ "?"
|| Parse.$$$ "!")
val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) []
val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) []
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun May 01 18:37:25 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun May 01 18:37:25 2011 +0200
@@ -86,7 +86,7 @@
val weight_smt_fact :
theory -> int -> ((string * locality) * thm) * int
-> (string * locality) * (int option * thm)
- val is_rich_type_sys_half_sound : rich_type_system -> bool
+ val is_rich_type_sys_fairly_sound : rich_type_system -> bool
val untranslated_fact : prover_fact -> (string * locality) * thm
val smt_weighted_fact :
theory -> int -> prover_fact * int
@@ -313,9 +313,9 @@
fun weight_smt_fact thy num_facts ((info, th), j) =
(info, (smt_fact_weight j num_facts, th |> Thm.transfer thy))
-fun is_rich_type_sys_half_sound (Dumb_Type_Sys type_sys) =
- level_of_type_sys type_sys <> Unsound
- | is_rich_type_sys_half_sound (Smart_Type_Sys full_types) = full_types
+fun is_rich_type_sys_fairly_sound (Dumb_Type_Sys type_sys) =
+ is_type_sys_fairly_sound type_sys
+ | is_rich_type_sys_fairly_sound (Smart_Type_Sys full_types) = full_types
fun untranslated_fact (Untranslated_Fact p) = p
| untranslated_fact (SMT_Weighted_Fact (info, (_, th))) = (info, th)
@@ -339,17 +339,12 @@
them each time. *)
val atp_important_message_keep_factor = 0.1
-fun type_sys_monomorphizes Many_Typed = true
- | type_sys_monomorphizes (Mangled _) = true
- | type_sys_monomorphizes (Args (mono, _)) = mono
- | type_sys_monomorphizes (Tags (mono, _)) = mono
- | type_sys_monomorphizes No_Types = false
-
-val fallback_best_type_systems = [Args (false, Unsound), Many_Typed]
+val fallback_best_type_systems =
+ [Preds (Polymorphic, Const_Arg_Types), Many_Typed]
fun adjust_dumb_type_sys formats Many_Typed =
if member (op =) formats Tff then (Tff, Many_Typed)
- else (Fof, Mangled Sound)
+ else (Fof, Preds (Mangled_Monomorphic, All_Types))
| adjust_dumb_type_sys formats type_sys =
if member (op =) formats Fof then (Fof, type_sys)
else (Tff, Many_Typed)
@@ -358,8 +353,8 @@
| determine_format_and_type_sys best_type_systems formats
(Smart_Type_Sys full_types) =
best_type_systems @ fallback_best_type_systems
- |> full_types ? filter (curry (op =) Sound o level_of_type_sys)
- |> hd |> adjust_dumb_type_sys formats
+ |> find_first (if full_types then is_type_sys_virtually_sound else K true)
+ |> the |> adjust_dumb_type_sys formats
fun run_atp auto name
({exec, required_execs, arguments, proof_delims, known_failures,
@@ -443,7 +438,8 @@
|> not (null blacklist)
? filter_out (member (op =) blacklist o fst
o untranslated_fact)
- |> type_sys_monomorphizes type_sys ? monomorphize_facts
+ |> polymorphism_of_type_sys type_sys <> Polymorphic
+ ? monomorphize_facts
|> map (atp_translated_fact ctxt)
val real_ms = Real.fromInt o Time.toMilliseconds
val slice_timeout =
@@ -507,7 +503,7 @@
NONE =>
if is_unsound_proof conjecture_shape facts_offset fact_names
atp_proof then
- SOME (UnsoundProof (level_of_type_sys type_sys = Sound))
+ SOME (UnsoundProof (is_type_sys_virtually_sound type_sys))
else
NONE
| SOME Unprovable =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sun May 01 18:37:25 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sun May 01 18:37:25 2011 +0200
@@ -183,7 +183,7 @@
val thy = Proof_Context.theory_of ctxt
val {facts = chained_ths, goal, ...} = Proof.goal state
val (_, hyp_ts, concl_t) = strip_subgoal goal i
- val half_sound = is_rich_type_sys_half_sound type_sys
+ val fairly_sound = is_rich_type_sys_fairly_sound type_sys
val _ = () |> not blocking ? kill_provers
val _ = case find_first (not o is_prover_supported ctxt) provers of
SOME name => error ("No such prover: " ^ name ^ ".")
@@ -212,7 +212,7 @@
|> (if blocking then smart_par_list_map else map) (launch problem)
|> exists fst |> rpair state
end
- fun get_facts label half_sound relevance_fudge provers =
+ fun get_facts label fairly_sound relevance_fudge provers =
let
val max_max_relevant =
case max_relevant of
@@ -225,7 +225,7 @@
val is_built_in_const =
is_built_in_const_for_prover ctxt (hd provers)
in
- relevant_facts ctxt half_sound relevance_thresholds max_max_relevant
+ relevant_facts ctxt fairly_sound relevance_thresholds max_max_relevant
is_built_in_const relevance_fudge relevance_override
chained_ths hyp_ts concl_t
|> tap (fn facts =>
@@ -246,7 +246,7 @@
accum
else
launch_provers state
- (get_facts "ATP" half_sound atp_relevance_fudge o K atps)
+ (get_facts "ATP" fairly_sound atp_relevance_fudge o K atps)
(K (Untranslated_Fact o fst)) (K (K NONE)) atps
fun launch_smts accum =
if null smts then
--- a/src/HOL/ex/sledgehammer_tactics.ML Sun May 01 18:37:25 2011 +0200
+++ b/src/HOL/ex/sledgehammer_tactics.ML Sun May 01 18:37:25 2011 +0200
@@ -32,9 +32,10 @@
Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
val relevance_override = {add = [], del = [], only = false}
val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
- val half_sound = Sledgehammer_Provers.is_rich_type_sys_half_sound type_sys
+ val fairly_sound =
+ Sledgehammer_Provers.is_rich_type_sys_fairly_sound type_sys
val facts =
- Sledgehammer_Filter.relevant_facts ctxt half_sound relevance_thresholds
+ Sledgehammer_Filter.relevant_facts ctxt fairly_sound relevance_thresholds
(the_default default_max_relevant max_relevant) is_built_in_const
relevance_fudge relevance_override chained_ths hyp_ts concl_t
val problem =