# HG changeset patch # User blanchet # Date 1314018165 -7200 # Node ID 6750b4297691f018fe5a1cbd14cda5dc42f7afcc # Parent 7b4104df2be628770d80e8599d4a31d2ae196e85 reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false diff -r 7b4104df2be6 -r 6750b4297691 src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Mon Aug 22 15:02:45 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_translate.ML Mon Aug 22 15:02:45 2011 +0200 @@ -1762,6 +1762,11 @@ | _ => fold add_undefined_const (var_types ()))) end +(* These types witness that the type classes they belong to allow infinite + models and hence that any types with these type classes is monotonic. *) +val known_infinite_types = + [@{typ nat}, Type ("Int.int", []), @{typ "nat => bool"}] + (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it out with monotonicity" paper presented at CADE 2011. *) fun add_iterm_nonmonotonic_types _ _ _ _ (SOME false) _ = I @@ -1771,7 +1776,12 @@ (case level of Noninf_Nonmono_Types => not (is_locality_global locality) orelse - not (is_type_surely_infinite ctxt sound T) + (* Unlike virtually any other polymorphic fact whose type variables can + be instantiated by a known infinite type, extensionality actually + encodes a cardinality constraints. *) + not (is_type_surely_infinite ctxt sound + (if locality = Extensionality then [] + else known_infinite_types) T) | Fin_Nonmono_Types => is_type_surely_finite ctxt false T | _ => true)) ? insert_type ctxt I (deep_freeze_type T) | add_iterm_nonmonotonic_types _ _ _ _ _ _ = I diff -r 7b4104df2be6 -r 6750b4297691 src/HOL/Tools/ATP/atp_util.ML --- a/src/HOL/Tools/ATP/atp_util.ML Mon Aug 22 15:02:45 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_util.ML Mon Aug 22 15:02:45 2011 +0200 @@ -22,7 +22,7 @@ Datatype_Aux.descr -> (Datatype_Aux.dtyp * typ) list -> Datatype_Aux.dtyp -> typ val is_type_surely_finite : Proof.context -> bool -> typ -> bool - val is_type_surely_infinite : Proof.context -> bool -> typ -> bool + val is_type_surely_infinite : Proof.context -> bool -> typ list -> typ -> bool val s_not : term -> term val s_conj : term * term -> term val s_disj : term * term -> term @@ -149,65 +149,71 @@ 0 means infinite type, 1 means singleton type (e.g., "unit"), and 2 means cardinality 2 or more. The specified default cardinality is returned if the cardinality of the type can't be determined. *) -fun tiny_card_of_type ctxt sound default_card T = +fun tiny_card_of_type ctxt sound unsound_assigns default_card T = let val thy = Proof_Context.theory_of ctxt val max = 2 (* 1 would be too small for the "fun" case *) fun aux slack avoid T = if member (op =) avoid T then 0 - else case T of - Type (@{type_name fun}, [T1, T2]) => - (case (aux slack avoid T1, aux slack avoid T2) of - (k, 1) => if slack andalso k = 0 then 0 else 1 - | (0, _) => 0 - | (_, 0) => 0 - | (k1, k2) => - if k1 >= max orelse k2 >= max then max - else Int.min (max, Integer.pow k2 k1)) - | @{typ prop} => 2 - | @{typ bool} => 2 (* optimization *) - | @{typ nat} => 0 (* optimization *) - | Type ("Int.int", []) => 0 (* optimization *) - | Type (s, _) => - (case datatype_constrs thy T of - constrs as _ :: _ => - let - val constr_cards = - map (Integer.prod o map (aux slack (T :: avoid)) o binder_types - o snd) constrs - in - if exists (curry (op =) 0) constr_cards then 0 - else Int.min (max, Integer.sum constr_cards) - end - | [] => - case Typedef.get_info ctxt s of - ({abs_type, rep_type, ...}, _) :: _ => - (* We cheat here by assuming that typedef types are infinite if - their underlying type is infinite. This is unsound in general - but it's hard to think of a realistic example where this would - not be the case. We are also slack with representation types: - If a representation type has the form "sigma => tau", we - consider it enough to check "sigma" for infiniteness. (Look - for "slack" in this function.) *) - (case varify_and_instantiate_type ctxt - (Logic.varifyT_global abs_type) T - (Logic.varifyT_global rep_type) - |> aux true avoid of - 0 => if sound then default_card else 0 - | 1 => 1 - | _ => default_card) - | [] => default_card) - (* Very slightly unsound: Type variables are assumed not to be - constrained to cardinality 1. (In practice, the user would most - likely have used "unit" directly anyway.) *) - | TFree _ => - if default_card = 1 andalso not sound then 2 else default_card - | TVar _ => default_card + else case (sound, AList.lookup (Sign.typ_instance thy o swap) + unsound_assigns T) of + (false, SOME k) => k + | _ => + case T of + Type (@{type_name fun}, [T1, T2]) => + (case (aux slack avoid T1, aux slack avoid T2) of + (k, 1) => if slack andalso k = 0 then 0 else 1 + | (0, _) => 0 + | (_, 0) => 0 + | (k1, k2) => + if k1 >= max orelse k2 >= max then max + else Int.min (max, Integer.pow k2 k1)) + | @{typ prop} => 2 + | @{typ bool} => 2 (* optimization *) + | @{typ nat} => 0 (* optimization *) + | Type ("Int.int", []) => 0 (* optimization *) + | Type (s, _) => + (case datatype_constrs thy T of + constrs as _ :: _ => + let + val constr_cards = + map (Integer.prod o map (aux slack (T :: avoid)) o binder_types + o snd) constrs + in + if exists (curry (op =) 0) constr_cards then 0 + else Int.min (max, Integer.sum constr_cards) + end + | [] => + case Typedef.get_info ctxt s of + ({abs_type, rep_type, ...}, _) :: _ => + (* We cheat here by assuming that typedef types are infinite if + their underlying type is infinite. This is unsound in general + but it's hard to think of a realistic example where this would + not be the case. We are also slack with representation types: + If a representation type has the form "sigma => tau", we + consider it enough to check "sigma" for infiniteness. (Look + for "slack" in this function.) *) + (case varify_and_instantiate_type ctxt + (Logic.varifyT_global abs_type) T + (Logic.varifyT_global rep_type) + |> aux true avoid of + 0 => if sound then default_card else 0 + | 1 => 1 + | _ => default_card) + | [] => default_card) + (* Very slightly unsound: Type variables are assumed not to be + constrained to cardinality 1. (In practice, the user would most + likely have used "unit" directly anyway.) *) + | TFree _ => + if default_card = 1 andalso not sound then 2 else default_card + | TVar _ => default_card in Int.min (max, aux false [] T) end -fun is_type_surely_finite ctxt sound T = tiny_card_of_type ctxt sound 0 T <> 0 -fun is_type_surely_infinite ctxt sound T = tiny_card_of_type ctxt sound 1 T = 0 +fun is_type_surely_finite ctxt sound T = + tiny_card_of_type ctxt sound [] 0 T <> 0 +fun is_type_surely_infinite ctxt sound infinite_Ts T = + tiny_card_of_type ctxt sound (map (rpair 0) infinite_Ts) 1 T = 0 (* Simple simplifications to ensure that sort annotations don't leave a trail of spurious "True"s. *)