1.1 --- a/NEWS Thu Jan 19 21:37:12 2012 +0100
1.2 +++ b/NEWS Thu Jan 19 21:37:12 2012 +0100
1.3 @@ -275,6 +275,7 @@
1.4 * Sledgehammer:
1.5 - Added "lam_trans" and "minimize" options.
1.6 - Renamed "slicing" ("no_slicing") option to "slice" ("dont_slice").
1.7 + - Renamed "sound" option to "strict".
1.8
1.9 * Metis:
1.10 - Added possibility to specify lambda translations scheme as a
2.1 --- a/src/HOL/TPTP/atp_export.ML Thu Jan 19 21:37:12 2012 +0100
2.2 +++ b/src/HOL/TPTP/atp_export.ML Thu Jan 19 21:37:12 2012 +0100
2.3 @@ -169,7 +169,7 @@
2.4
2.5 fun generate_tptp_inference_file_for_theory ctxt thy format type_enc file_name =
2.6 let
2.7 - val type_enc = type_enc |> type_enc_from_string Sound
2.8 + val type_enc = type_enc |> type_enc_from_string Strict
2.9 |> adjust_type_enc format
2.10 val mono = polymorphism_of_type_enc type_enc <> Polymorphic
2.11 val path = file_name |> Path.explode
3.1 --- a/src/HOL/Tools/ATP/atp_translate.ML Thu Jan 19 21:37:12 2012 +0100
3.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML Thu Jan 19 21:37:12 2012 +0100
3.3 @@ -19,11 +19,11 @@
3.4 General | Helper | Induction | Intro | Elim | Simp | Local | Assum | Chained
3.5
3.6 datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
3.7 - datatype soundness = Sound_Modulo_Infinity | Sound
3.8 + datatype strictness = Strict | Non_Strict
3.9 datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars
3.10 datatype type_level =
3.11 All_Types |
3.12 - Noninf_Nonmono_Types of soundness * granularity |
3.13 + Noninf_Nonmono_Types of strictness * granularity |
3.14 Fin_Nonmono_Types of granularity |
3.15 Const_Arg_Types |
3.16 No_Types
3.17 @@ -88,7 +88,7 @@
3.18 val level_of_type_enc : type_enc -> type_level
3.19 val is_type_enc_quasi_sound : type_enc -> bool
3.20 val is_type_enc_fairly_sound : type_enc -> bool
3.21 - val type_enc_from_string : soundness -> string -> type_enc
3.22 + val type_enc_from_string : strictness -> string -> type_enc
3.23 val adjust_type_enc : atp_format -> type_enc -> type_enc
3.24 val mk_aconns :
3.25 connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
3.26 @@ -546,11 +546,11 @@
3.27
3.28 datatype order = First_Order | Higher_Order
3.29 datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
3.30 -datatype soundness = Sound_Modulo_Infinity | Sound
3.31 +datatype strictness = Strict | Non_Strict
3.32 datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars
3.33 datatype type_level =
3.34 All_Types |
3.35 - Noninf_Nonmono_Types of soundness * granularity |
3.36 + Noninf_Nonmono_Types of strictness * granularity |
3.37 Fin_Nonmono_Types of granularity |
3.38 Const_Arg_Types |
3.39 No_Types
3.40 @@ -608,7 +608,7 @@
3.41 | NONE => (constr All_Vars, s))
3.42 | NONE => fallback s
3.43
3.44 -fun type_enc_from_string soundness s =
3.45 +fun type_enc_from_string strictness s =
3.46 (case try (unprefix "poly_") s of
3.47 SOME s => (SOME Polymorphic, s)
3.48 | NONE =>
3.49 @@ -620,7 +620,7 @@
3.50 | NONE => (NONE, s))
3.51 ||> (pair All_Types
3.52 |> try_nonmono Fin_Nonmono_Types bangs
3.53 - |> try_nonmono (curry Noninf_Nonmono_Types soundness) queries)
3.54 + |> try_nonmono (curry Noninf_Nonmono_Types strictness) queries)
3.55 |> (fn (poly, (level, core)) =>
3.56 case (core, (poly, level)) of
3.57 ("simple", (SOME poly, _)) =>
3.58 @@ -1281,8 +1281,8 @@
3.59 val known_infinite_types =
3.60 [@{typ nat}, HOLogic.intT, HOLogic.realT, @{typ "nat => bool"}]
3.61
3.62 -fun is_type_kind_of_surely_infinite ctxt soundness cached_Ts T =
3.63 - soundness <> Sound andalso is_type_surely_infinite ctxt true cached_Ts T
3.64 +fun is_type_kind_of_surely_infinite ctxt strictness cached_Ts T =
3.65 + strictness <> Strict andalso is_type_surely_infinite ctxt true cached_Ts T
3.66
3.67 (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
3.68 dangerous because their "exhaust" properties can easily lead to unsound ATP
3.69 @@ -1292,12 +1292,12 @@
3.70 fun should_encode_type _ (_ : monotonicity_info) All_Types _ = true
3.71 | should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
3.72 maybe_nonmono_Ts, ...}
3.73 - (Noninf_Nonmono_Types (soundness, grain)) T =
3.74 + (Noninf_Nonmono_Types (strictness, grain)) T =
3.75 grain = Ghost_Type_Arg_Vars orelse
3.76 (exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
3.77 not (exists (type_instance ctxt T) surely_infinite_Ts orelse
3.78 (not (member (type_equiv ctxt) maybe_finite_Ts T) andalso
3.79 - is_type_kind_of_surely_infinite ctxt soundness surely_infinite_Ts
3.80 + is_type_kind_of_surely_infinite ctxt strictness surely_infinite_Ts
3.81 T)))
3.82 | should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts,
3.83 maybe_nonmono_Ts, ...}
3.84 @@ -2046,7 +2046,7 @@
3.85 maybe_infinite_Ts = known_infinite_types,
3.86 surely_infinite_Ts =
3.87 case level of
3.88 - Noninf_Nonmono_Types (Sound, _) => []
3.89 + Noninf_Nonmono_Types (Strict, _) => []
3.90 | _ => known_infinite_types,
3.91 maybe_nonmono_Ts = [@{typ bool}]}
3.92
3.93 @@ -2059,11 +2059,11 @@
3.94 surely_infinite_Ts, maybe_nonmono_Ts}) =
3.95 if is_tptp_equal s andalso exists is_maybe_universal_var [tm1, tm2] then
3.96 case level of
3.97 - Noninf_Nonmono_Types (soundness, _) =>
3.98 + Noninf_Nonmono_Types (strictness, _) =>
3.99 if exists (type_instance ctxt T) surely_infinite_Ts orelse
3.100 member (type_equiv ctxt) maybe_finite_Ts T then
3.101 mono
3.102 - else if is_type_kind_of_surely_infinite ctxt soundness
3.103 + else if is_type_kind_of_surely_infinite ctxt strictness
3.104 surely_infinite_Ts T then
3.105 {maybe_finite_Ts = maybe_finite_Ts,
3.106 surely_finite_Ts = surely_finite_Ts,
4.1 --- a/src/HOL/Tools/Metis/metis_tactic.ML Thu Jan 19 21:37:12 2012 +0100
4.2 +++ b/src/HOL/Tools/Metis/metis_tactic.ML Thu Jan 19 21:37:12 2012 +0100
4.3 @@ -140,7 +140,7 @@
4.4 val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
4.5 val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls
4.6 val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
4.7 - val type_enc = type_enc_from_string Sound type_enc
4.8 + val type_enc = type_enc_from_string Strict type_enc
4.9 val (sym_tab, axioms, concealed) =
4.10 prepare_metis_problem ctxt type_enc lam_trans cls ths
4.11 fun get_isa_thm mth Isa_Reflexive_or_Trivial =
5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Jan 19 21:37:12 2012 +0100
5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Jan 19 21:37:12 2012 +0100
5.3 @@ -87,7 +87,7 @@
5.4 ("overlord", "false"),
5.5 ("blocking", "false"),
5.6 ("type_enc", "smart"),
5.7 - ("sound", "false"),
5.8 + ("strict", "false"),
5.9 ("lam_trans", "smart"),
5.10 ("relevance_thresholds", "0.45 0.85"),
5.11 ("max_relevant", "smart"),
5.12 @@ -106,13 +106,13 @@
5.13 ("quiet", "verbose"),
5.14 ("no_overlord", "overlord"),
5.15 ("non_blocking", "blocking"),
5.16 - ("unsound", "sound"),
5.17 + ("non_strict", "strict"),
5.18 ("no_isar_proof", "isar_proof"),
5.19 ("dont_slice", "slice"),
5.20 ("dont_minimize", "minimize")]
5.21
5.22 val params_for_minimize =
5.23 - ["debug", "verbose", "overlord", "type_enc", "sound", "lam_trans",
5.24 + ["debug", "verbose", "overlord", "type_enc", "strict", "lam_trans",
5.25 "max_mono_iters", "max_new_mono_instances", "isar_proof",
5.26 "isar_shrink_factor", "timeout", "preplay_timeout"]
5.27
5.28 @@ -141,7 +141,7 @@
5.29 | _ => value)
5.30 | NONE => (name, value)
5.31
5.32 -val any_type_enc = type_enc_from_string Sound "erased"
5.33 +val any_type_enc = type_enc_from_string Strict "erased"
5.34
5.35 (* "provers =", "type_enc =", and "lam_trans" can be omitted. For the last two,
5.36 this is a secret feature. *)
5.37 @@ -152,7 +152,7 @@
5.38 (name, value)
5.39 else if is_prover_list ctxt name andalso null value then
5.40 ("provers", [name])
5.41 - else if can (type_enc_from_string Sound) name andalso null value then
5.42 + else if can (type_enc_from_string Strict) name andalso null value then
5.43 ("type_enc", [name])
5.44 else if can (trans_lams_from_string ctxt any_type_enc) name andalso
5.45 null value then
5.46 @@ -282,8 +282,8 @@
5.47 NONE
5.48 else case lookup_string "type_enc" of
5.49 "smart" => NONE
5.50 - | s => (type_enc_from_string Sound s; SOME s)
5.51 - val sound = mode = Auto_Try orelse lookup_bool "sound"
5.52 + | s => (type_enc_from_string Strict s; SOME s)
5.53 + val strict = mode = Auto_Try orelse lookup_bool "strict"
5.54 val lam_trans = lookup_option lookup_string "lam_trans"
5.55 val relevance_thresholds = lookup_real_pair "relevance_thresholds"
5.56 val max_relevant = lookup_option lookup_int "max_relevant"
5.57 @@ -302,7 +302,7 @@
5.58 val expect = lookup_string "expect"
5.59 in
5.60 {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
5.61 - provers = provers, type_enc = type_enc, sound = sound,
5.62 + provers = provers, type_enc = type_enc, strict = strict,
5.63 lam_trans = lam_trans, relevance_thresholds = relevance_thresholds,
5.64 max_relevant = max_relevant, max_mono_iters = max_mono_iters,
5.65 max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Jan 19 21:37:12 2012 +0100
6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Jan 19 21:37:12 2012 +0100
6.3 @@ -47,8 +47,8 @@
6.4 fun print silent f = if silent then () else Output.urgent_message (f ())
6.5
6.6 fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
6.7 - max_new_mono_instances, type_enc, lam_trans, isar_proof,
6.8 - isar_shrink_factor, preplay_timeout, ...} : params)
6.9 + max_new_mono_instances, type_enc, strict, lam_trans,
6.10 + isar_proof, isar_shrink_factor, preplay_timeout, ...} : params)
6.11 silent (prover : prover) timeout i n state facts =
6.12 let
6.13 val _ =
6.14 @@ -61,7 +61,7 @@
6.15 facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n))
6.16 val params =
6.17 {debug = debug, verbose = verbose, overlord = overlord, blocking = true,
6.18 - provers = provers, type_enc = type_enc, sound = true,
6.19 + provers = provers, type_enc = type_enc, strict = strict,
6.20 lam_trans = lam_trans, relevance_thresholds = (1.01, 1.01),
6.21 max_relevant = SOME (length facts), max_mono_iters = max_mono_iters,
6.22 max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jan 19 21:37:12 2012 +0100
7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jan 19 21:37:12 2012 +0100
7.3 @@ -25,7 +25,7 @@
7.4 blocking: bool,
7.5 provers: string list,
7.6 type_enc: string option,
7.7 - sound: bool,
7.8 + strict: bool,
7.9 lam_trans: string option,
7.10 relevance_thresholds: real * real,
7.11 max_relevant: int option,
7.12 @@ -289,7 +289,7 @@
7.13 blocking: bool,
7.14 provers: string list,
7.15 type_enc: string option,
7.16 - sound: bool,
7.17 + strict: bool,
7.18 lam_trans: string option,
7.19 relevance_thresholds: real * real,
7.20 max_relevant: int option,
7.21 @@ -580,7 +580,7 @@
7.22 fun run_atp mode name
7.23 ({exec, required_execs, arguments, proof_delims, known_failures,
7.24 conj_sym_kind, prem_kind, best_slices, ...} : atp_config)
7.25 - (params as {debug, verbose, overlord, type_enc, sound, lam_trans,
7.26 + (params as {debug, verbose, overlord, type_enc, strict, lam_trans,
7.27 max_relevant, max_mono_iters, max_new_mono_instances,
7.28 isar_proof, isar_shrink_factor, slice, timeout,
7.29 preplay_timeout, ...})
7.30 @@ -659,7 +659,7 @@
7.31 val num_facts =
7.32 length facts |> is_none max_relevant
7.33 ? Integer.min best_max_relevant
7.34 - val soundness = if sound then Sound else Sound_Modulo_Infinity
7.35 + val soundness = if strict then Strict else Non_Strict
7.36 val type_enc =
7.37 type_enc |> choose_type_enc soundness best_type_enc format
7.38 val fairly_sound = is_type_enc_fairly_sound type_enc
8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Jan 19 21:37:12 2012 +0100
8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Jan 19 21:37:12 2012 +0100
8.3 @@ -73,7 +73,7 @@
8.4 (K 5.0)
8.5
8.6 fun adjust_reconstructor_params override_params
8.7 - ({debug, verbose, overlord, blocking, provers, type_enc, sound,
8.8 + ({debug, verbose, overlord, blocking, provers, type_enc, strict,
8.9 lam_trans, relevance_thresholds, max_relevant, max_mono_iters,
8.10 max_new_mono_instances, isar_proof, isar_shrink_factor, slice,
8.11 minimize, timeout, preplay_timeout, expect} : params) =
8.12 @@ -88,7 +88,7 @@
8.13 val lam_trans = lookup_override "lam_trans" lam_trans
8.14 in
8.15 {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
8.16 - provers = provers, type_enc = type_enc, sound = sound,
8.17 + provers = provers, type_enc = type_enc, strict = strict,
8.18 lam_trans = lam_trans, max_relevant = max_relevant,
8.19 relevance_thresholds = relevance_thresholds,
8.20 max_mono_iters = max_mono_iters,