1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML Thu Jan 19 21:37:12 2012 +0100
1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML Thu Jan 19 21:37:12 2012 +0100
1.3 @@ -19,11 +19,11 @@
1.4 General | Helper | Induction | Intro | Elim | Simp | Local | Assum | Chained
1.5
1.6 datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
1.7 - datatype soundness = Sound_Modulo_Infinity | Sound
1.8 + datatype strictness = Strict | Non_Strict
1.9 datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars
1.10 datatype type_level =
1.11 All_Types |
1.12 - Noninf_Nonmono_Types of soundness * granularity |
1.13 + Noninf_Nonmono_Types of strictness * granularity |
1.14 Fin_Nonmono_Types of granularity |
1.15 Const_Arg_Types |
1.16 No_Types
1.17 @@ -88,7 +88,7 @@
1.18 val level_of_type_enc : type_enc -> type_level
1.19 val is_type_enc_quasi_sound : type_enc -> bool
1.20 val is_type_enc_fairly_sound : type_enc -> bool
1.21 - val type_enc_from_string : soundness -> string -> type_enc
1.22 + val type_enc_from_string : strictness -> string -> type_enc
1.23 val adjust_type_enc : atp_format -> type_enc -> type_enc
1.24 val mk_aconns :
1.25 connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
1.26 @@ -546,11 +546,11 @@
1.27
1.28 datatype order = First_Order | Higher_Order
1.29 datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
1.30 -datatype soundness = Sound_Modulo_Infinity | Sound
1.31 +datatype strictness = Strict | Non_Strict
1.32 datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars
1.33 datatype type_level =
1.34 All_Types |
1.35 - Noninf_Nonmono_Types of soundness * granularity |
1.36 + Noninf_Nonmono_Types of strictness * granularity |
1.37 Fin_Nonmono_Types of granularity |
1.38 Const_Arg_Types |
1.39 No_Types
1.40 @@ -608,7 +608,7 @@
1.41 | NONE => (constr All_Vars, s))
1.42 | NONE => fallback s
1.43
1.44 -fun type_enc_from_string soundness s =
1.45 +fun type_enc_from_string strictness s =
1.46 (case try (unprefix "poly_") s of
1.47 SOME s => (SOME Polymorphic, s)
1.48 | NONE =>
1.49 @@ -620,7 +620,7 @@
1.50 | NONE => (NONE, s))
1.51 ||> (pair All_Types
1.52 |> try_nonmono Fin_Nonmono_Types bangs
1.53 - |> try_nonmono (curry Noninf_Nonmono_Types soundness) queries)
1.54 + |> try_nonmono (curry Noninf_Nonmono_Types strictness) queries)
1.55 |> (fn (poly, (level, core)) =>
1.56 case (core, (poly, level)) of
1.57 ("simple", (SOME poly, _)) =>
1.58 @@ -1281,8 +1281,8 @@
1.59 val known_infinite_types =
1.60 [@{typ nat}, HOLogic.intT, HOLogic.realT, @{typ "nat => bool"}]
1.61
1.62 -fun is_type_kind_of_surely_infinite ctxt soundness cached_Ts T =
1.63 - soundness <> Sound andalso is_type_surely_infinite ctxt true cached_Ts T
1.64 +fun is_type_kind_of_surely_infinite ctxt strictness cached_Ts T =
1.65 + strictness <> Strict andalso is_type_surely_infinite ctxt true cached_Ts T
1.66
1.67 (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
1.68 dangerous because their "exhaust" properties can easily lead to unsound ATP
1.69 @@ -1292,12 +1292,12 @@
1.70 fun should_encode_type _ (_ : monotonicity_info) All_Types _ = true
1.71 | should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
1.72 maybe_nonmono_Ts, ...}
1.73 - (Noninf_Nonmono_Types (soundness, grain)) T =
1.74 + (Noninf_Nonmono_Types (strictness, grain)) T =
1.75 grain = Ghost_Type_Arg_Vars orelse
1.76 (exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
1.77 not (exists (type_instance ctxt T) surely_infinite_Ts orelse
1.78 (not (member (type_equiv ctxt) maybe_finite_Ts T) andalso
1.79 - is_type_kind_of_surely_infinite ctxt soundness surely_infinite_Ts
1.80 + is_type_kind_of_surely_infinite ctxt strictness surely_infinite_Ts
1.81 T)))
1.82 | should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts,
1.83 maybe_nonmono_Ts, ...}
1.84 @@ -2046,7 +2046,7 @@
1.85 maybe_infinite_Ts = known_infinite_types,
1.86 surely_infinite_Ts =
1.87 case level of
1.88 - Noninf_Nonmono_Types (Sound, _) => []
1.89 + Noninf_Nonmono_Types (Strict, _) => []
1.90 | _ => known_infinite_types,
1.91 maybe_nonmono_Ts = [@{typ bool}]}
1.92
1.93 @@ -2059,11 +2059,11 @@
1.94 surely_infinite_Ts, maybe_nonmono_Ts}) =
1.95 if is_tptp_equal s andalso exists is_maybe_universal_var [tm1, tm2] then
1.96 case level of
1.97 - Noninf_Nonmono_Types (soundness, _) =>
1.98 + Noninf_Nonmono_Types (strictness, _) =>
1.99 if exists (type_instance ctxt T) surely_infinite_Ts orelse
1.100 member (type_equiv ctxt) maybe_finite_Ts T then
1.101 mono
1.102 - else if is_type_kind_of_surely_infinite ctxt soundness
1.103 + else if is_type_kind_of_surely_infinite ctxt strictness
1.104 surely_infinite_Ts T then
1.105 {maybe_finite_Ts = maybe_finite_Ts,
1.106 surely_finite_Ts = surely_finite_Ts,