# HG changeset patch # User blanchet # Date 1305888479 -7200 # Node ID 91adf04946d1c05002b20cf20da9cec51bd6b363 # Parent 75c94e3319ae9856d81307400fbaa481fb0ada1a reintroduced type encodings "poly_preds_{bang,query}", but this time being more liberal about type variables of known safe sorts diff -r 75c94e3319ae -r 91adf04946d1 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Fri May 20 12:47:59 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Fri May 20 12:47:59 2011 +0200 @@ -141,13 +141,12 @@ case (core, (poly, level, heaviness)) of ("simple", (NONE, _, Light)) => Simple_Types level | ("preds", (SOME Polymorphic, _, _)) => - if level = All_Types then Preds (Polymorphic, level, heaviness) - else raise Same.SAME + Preds (Polymorphic, level, heaviness) | ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness) | ("tags", (SOME Polymorphic, All_Types, _)) => Tags (Polymorphic, All_Types, heaviness) | ("tags", (SOME Polymorphic, Finite_Types, _)) => - (* The light encoding yields too many unsound proofs. *) + (* The actual light encoding yields too many unsound proofs. *) Tags (Polymorphic, Finite_Types, Heavy) | ("tags", (SOME Polymorphic, _, _)) => raise Same.SAME | ("tags", (SOME poly, _, _)) => Tags (poly, level, heaviness) diff -r 75c94e3319ae -r 91adf04946d1 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri May 20 12:47:59 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri May 20 12:47:59 2011 +0200 @@ -122,6 +122,12 @@ | NONE => []) | datatype_constrs _ _ = [] +(* Feel free to extend this list with any sorts that don't have finiteness + axioms. *) +val safe_sorts = + @{sort type} @ @{sort "{default,zero,one,plus,minus,uminus,times,inverse}"} @ + @{sort "{abs,sgn,ord,equal,number}"} + (* Similar to "Nitpick_HOL.bounded_exact_card_of_type". 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 @@ -130,58 +136,61 @@ let 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 *) - | @{typ int} => 0 (* optimization *) - | Type (s, _) => - let val thy = Proof_Context.theory_of ctxt in - 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 => 0 - | 1 => 1 - | _ => default_card) - | [] => default_card - end - | TFree _ => - (* 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.) *) - if default_card = 1 then 2 else default_card - | _ => default_card) + 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 *) + | @{typ int} => 0 (* optimization *) + | Type (s, _) => + let val thy = Proof_Context.theory_of ctxt in + 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 => 0 + | 1 => 1 + | _ => default_card) + | [] => default_card + end + (* 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 then 2 else default_card + (* Schematic type variables that contain only unproblematic sorts + (with no finiteness axiom) can safely be considered infinite. *) + | TVar (_, S) => + if default_card = 0 orelse subset (op =) (S, safe_sorts) then 0 + else default_card in Int.min (max, aux false [] T) end fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt 0 T <> 0