--- a/NEWS Thu Jan 19 21:37:12 2012 +0100
+++ b/NEWS Thu Jan 19 21:37:12 2012 +0100
@@ -275,6 +275,7 @@
* Sledgehammer:
- Added "lam_trans" and "minimize" options.
- Renamed "slicing" ("no_slicing") option to "slice" ("dont_slice").
+ - Renamed "sound" option to "strict".
* Metis:
- Added possibility to specify lambda translations scheme as a
--- a/src/HOL/TPTP/atp_export.ML Thu Jan 19 21:37:12 2012 +0100
+++ b/src/HOL/TPTP/atp_export.ML Thu Jan 19 21:37:12 2012 +0100
@@ -169,7 +169,7 @@
fun generate_tptp_inference_file_for_theory ctxt thy format type_enc file_name =
let
- val type_enc = type_enc |> type_enc_from_string Sound
+ val type_enc = type_enc |> type_enc_from_string Strict
|> adjust_type_enc format
val mono = polymorphism_of_type_enc type_enc <> Polymorphic
val path = file_name |> Path.explode
--- a/src/HOL/Tools/ATP/atp_translate.ML Thu Jan 19 21:37:12 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_translate.ML Thu Jan 19 21:37:12 2012 +0100
@@ -19,11 +19,11 @@
General | Helper | Induction | Intro | Elim | Simp | Local | Assum | Chained
datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
- datatype soundness = Sound_Modulo_Infinity | Sound
+ datatype strictness = Strict | Non_Strict
datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars
datatype type_level =
All_Types |
- Noninf_Nonmono_Types of soundness * granularity |
+ Noninf_Nonmono_Types of strictness * granularity |
Fin_Nonmono_Types of granularity |
Const_Arg_Types |
No_Types
@@ -88,7 +88,7 @@
val level_of_type_enc : type_enc -> type_level
val is_type_enc_quasi_sound : type_enc -> bool
val is_type_enc_fairly_sound : type_enc -> bool
- val type_enc_from_string : soundness -> string -> type_enc
+ val type_enc_from_string : strictness -> string -> type_enc
val adjust_type_enc : atp_format -> type_enc -> type_enc
val mk_aconns :
connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
@@ -546,11 +546,11 @@
datatype order = First_Order | Higher_Order
datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
-datatype soundness = Sound_Modulo_Infinity | Sound
+datatype strictness = Strict | Non_Strict
datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars
datatype type_level =
All_Types |
- Noninf_Nonmono_Types of soundness * granularity |
+ Noninf_Nonmono_Types of strictness * granularity |
Fin_Nonmono_Types of granularity |
Const_Arg_Types |
No_Types
@@ -608,7 +608,7 @@
| NONE => (constr All_Vars, s))
| NONE => fallback s
-fun type_enc_from_string soundness s =
+fun type_enc_from_string strictness s =
(case try (unprefix "poly_") s of
SOME s => (SOME Polymorphic, s)
| NONE =>
@@ -620,7 +620,7 @@
| NONE => (NONE, s))
||> (pair All_Types
|> try_nonmono Fin_Nonmono_Types bangs
- |> try_nonmono (curry Noninf_Nonmono_Types soundness) queries)
+ |> try_nonmono (curry Noninf_Nonmono_Types strictness) queries)
|> (fn (poly, (level, core)) =>
case (core, (poly, level)) of
("simple", (SOME poly, _)) =>
@@ -1281,8 +1281,8 @@
val known_infinite_types =
[@{typ nat}, HOLogic.intT, HOLogic.realT, @{typ "nat => bool"}]
-fun is_type_kind_of_surely_infinite ctxt soundness cached_Ts T =
- soundness <> Sound andalso is_type_surely_infinite ctxt true cached_Ts T
+fun is_type_kind_of_surely_infinite ctxt strictness cached_Ts T =
+ strictness <> Strict andalso is_type_surely_infinite ctxt true cached_Ts T
(* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
dangerous because their "exhaust" properties can easily lead to unsound ATP
@@ -1292,12 +1292,12 @@
fun should_encode_type _ (_ : monotonicity_info) All_Types _ = true
| should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
maybe_nonmono_Ts, ...}
- (Noninf_Nonmono_Types (soundness, grain)) T =
+ (Noninf_Nonmono_Types (strictness, grain)) T =
grain = Ghost_Type_Arg_Vars orelse
(exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
not (exists (type_instance ctxt T) surely_infinite_Ts orelse
(not (member (type_equiv ctxt) maybe_finite_Ts T) andalso
- is_type_kind_of_surely_infinite ctxt soundness surely_infinite_Ts
+ is_type_kind_of_surely_infinite ctxt strictness surely_infinite_Ts
T)))
| should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts,
maybe_nonmono_Ts, ...}
@@ -2046,7 +2046,7 @@
maybe_infinite_Ts = known_infinite_types,
surely_infinite_Ts =
case level of
- Noninf_Nonmono_Types (Sound, _) => []
+ Noninf_Nonmono_Types (Strict, _) => []
| _ => known_infinite_types,
maybe_nonmono_Ts = [@{typ bool}]}
@@ -2059,11 +2059,11 @@
surely_infinite_Ts, maybe_nonmono_Ts}) =
if is_tptp_equal s andalso exists is_maybe_universal_var [tm1, tm2] then
case level of
- Noninf_Nonmono_Types (soundness, _) =>
+ Noninf_Nonmono_Types (strictness, _) =>
if exists (type_instance ctxt T) surely_infinite_Ts orelse
member (type_equiv ctxt) maybe_finite_Ts T then
mono
- else if is_type_kind_of_surely_infinite ctxt soundness
+ else if is_type_kind_of_surely_infinite ctxt strictness
surely_infinite_Ts T then
{maybe_finite_Ts = maybe_finite_Ts,
surely_finite_Ts = surely_finite_Ts,
--- a/src/HOL/Tools/Metis/metis_tactic.ML Thu Jan 19 21:37:12 2012 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Thu Jan 19 21:37:12 2012 +0100
@@ -140,7 +140,7 @@
val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls
val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
- val type_enc = type_enc_from_string Sound type_enc
+ val type_enc = type_enc_from_string Strict type_enc
val (sym_tab, axioms, concealed) =
prepare_metis_problem ctxt type_enc lam_trans cls ths
fun get_isa_thm mth Isa_Reflexive_or_Trivial =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Jan 19 21:37:12 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Jan 19 21:37:12 2012 +0100
@@ -87,7 +87,7 @@
("overlord", "false"),
("blocking", "false"),
("type_enc", "smart"),
- ("sound", "false"),
+ ("strict", "false"),
("lam_trans", "smart"),
("relevance_thresholds", "0.45 0.85"),
("max_relevant", "smart"),
@@ -106,13 +106,13 @@
("quiet", "verbose"),
("no_overlord", "overlord"),
("non_blocking", "blocking"),
- ("unsound", "sound"),
+ ("non_strict", "strict"),
("no_isar_proof", "isar_proof"),
("dont_slice", "slice"),
("dont_minimize", "minimize")]
val params_for_minimize =
- ["debug", "verbose", "overlord", "type_enc", "sound", "lam_trans",
+ ["debug", "verbose", "overlord", "type_enc", "strict", "lam_trans",
"max_mono_iters", "max_new_mono_instances", "isar_proof",
"isar_shrink_factor", "timeout", "preplay_timeout"]
@@ -141,7 +141,7 @@
| _ => value)
| NONE => (name, value)
-val any_type_enc = type_enc_from_string Sound "erased"
+val any_type_enc = type_enc_from_string Strict "erased"
(* "provers =", "type_enc =", and "lam_trans" can be omitted. For the last two,
this is a secret feature. *)
@@ -152,7 +152,7 @@
(name, value)
else if is_prover_list ctxt name andalso null value then
("provers", [name])
- else if can (type_enc_from_string Sound) name andalso null value then
+ else if can (type_enc_from_string Strict) name andalso null value then
("type_enc", [name])
else if can (trans_lams_from_string ctxt any_type_enc) name andalso
null value then
@@ -282,8 +282,8 @@
NONE
else case lookup_string "type_enc" of
"smart" => NONE
- | s => (type_enc_from_string Sound s; SOME s)
- val sound = mode = Auto_Try orelse lookup_bool "sound"
+ | s => (type_enc_from_string Strict s; SOME s)
+ val strict = mode = Auto_Try orelse lookup_bool "strict"
val lam_trans = lookup_option lookup_string "lam_trans"
val relevance_thresholds = lookup_real_pair "relevance_thresholds"
val max_relevant = lookup_option lookup_int "max_relevant"
@@ -302,7 +302,7 @@
val expect = lookup_string "expect"
in
{debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
- provers = provers, type_enc = type_enc, sound = sound,
+ provers = provers, type_enc = type_enc, strict = strict,
lam_trans = lam_trans, relevance_thresholds = relevance_thresholds,
max_relevant = max_relevant, max_mono_iters = max_mono_iters,
max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Jan 19 21:37:12 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Jan 19 21:37:12 2012 +0100
@@ -47,8 +47,8 @@
fun print silent f = if silent then () else Output.urgent_message (f ())
fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
- max_new_mono_instances, type_enc, lam_trans, isar_proof,
- isar_shrink_factor, preplay_timeout, ...} : params)
+ max_new_mono_instances, type_enc, strict, lam_trans,
+ isar_proof, isar_shrink_factor, preplay_timeout, ...} : params)
silent (prover : prover) timeout i n state facts =
let
val _ =
@@ -61,7 +61,7 @@
facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n))
val params =
{debug = debug, verbose = verbose, overlord = overlord, blocking = true,
- provers = provers, type_enc = type_enc, sound = true,
+ provers = provers, type_enc = type_enc, strict = strict,
lam_trans = lam_trans, relevance_thresholds = (1.01, 1.01),
max_relevant = SOME (length facts), max_mono_iters = max_mono_iters,
max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jan 19 21:37:12 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jan 19 21:37:12 2012 +0100
@@ -25,7 +25,7 @@
blocking: bool,
provers: string list,
type_enc: string option,
- sound: bool,
+ strict: bool,
lam_trans: string option,
relevance_thresholds: real * real,
max_relevant: int option,
@@ -289,7 +289,7 @@
blocking: bool,
provers: string list,
type_enc: string option,
- sound: bool,
+ strict: bool,
lam_trans: string option,
relevance_thresholds: real * real,
max_relevant: int option,
@@ -580,7 +580,7 @@
fun run_atp mode name
({exec, required_execs, arguments, proof_delims, known_failures,
conj_sym_kind, prem_kind, best_slices, ...} : atp_config)
- (params as {debug, verbose, overlord, type_enc, sound, lam_trans,
+ (params as {debug, verbose, overlord, type_enc, strict, lam_trans,
max_relevant, max_mono_iters, max_new_mono_instances,
isar_proof, isar_shrink_factor, slice, timeout,
preplay_timeout, ...})
@@ -659,7 +659,7 @@
val num_facts =
length facts |> is_none max_relevant
? Integer.min best_max_relevant
- val soundness = if sound then Sound else Sound_Modulo_Infinity
+ val soundness = if strict then Strict else Non_Strict
val type_enc =
type_enc |> choose_type_enc soundness best_type_enc format
val fairly_sound = is_type_enc_fairly_sound type_enc
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Jan 19 21:37:12 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Jan 19 21:37:12 2012 +0100
@@ -73,7 +73,7 @@
(K 5.0)
fun adjust_reconstructor_params override_params
- ({debug, verbose, overlord, blocking, provers, type_enc, sound,
+ ({debug, verbose, overlord, blocking, provers, type_enc, strict,
lam_trans, relevance_thresholds, max_relevant, max_mono_iters,
max_new_mono_instances, isar_proof, isar_shrink_factor, slice,
minimize, timeout, preplay_timeout, expect} : params) =
@@ -88,7 +88,7 @@
val lam_trans = lookup_override "lam_trans" lam_trans
in
{debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
- provers = provers, type_enc = type_enc, sound = sound,
+ provers = provers, type_enc = type_enc, strict = strict,
lam_trans = lam_trans, max_relevant = max_relevant,
relevance_thresholds = relevance_thresholds,
max_mono_iters = max_mono_iters,