134 |
134 |
135 (* Similar to "Nitpick_HOL.bounded_exact_card_of_type". |
135 (* Similar to "Nitpick_HOL.bounded_exact_card_of_type". |
136 0 means infinite type, 1 means singleton type (e.g., "unit"), and 2 means |
136 0 means infinite type, 1 means singleton type (e.g., "unit"), and 2 means |
137 cardinality 2 or more. The specified default cardinality is returned if the |
137 cardinality 2 or more. The specified default cardinality is returned if the |
138 cardinality of the type can't be determined. *) |
138 cardinality of the type can't be determined. *) |
139 fun tiny_card_of_type ctxt default_card assigns T = |
139 fun tiny_card_of_type ctxt default_card T = |
140 let |
140 let |
141 val thy = Proof_Context.theory_of ctxt |
141 val thy = Proof_Context.theory_of ctxt |
142 val max = 2 (* 1 would be too small for the "fun" case *) |
142 val max = 2 (* 1 would be too small for the "fun" case *) |
143 fun aux slack avoid T = |
143 fun aux slack avoid T = |
144 if member (op =) avoid T then |
144 if member (op =) avoid T then |
145 0 |
145 0 |
146 else case AList.lookup (Sign.typ_instance thy o swap) assigns T of |
146 else case T of |
147 SOME k => k |
147 Type (@{type_name fun}, [T1, T2]) => |
148 | NONE => |
148 (case (aux slack avoid T1, aux slack avoid T2) of |
149 case T of |
149 (k, 1) => if slack andalso k = 0 then 0 else 1 |
150 Type (@{type_name fun}, [T1, T2]) => |
150 | (0, _) => 0 |
151 (case (aux slack avoid T1, aux slack avoid T2) of |
151 | (_, 0) => 0 |
152 (k, 1) => if slack andalso k = 0 then 0 else 1 |
152 | (k1, k2) => |
153 | (0, _) => 0 |
153 if k1 >= max orelse k2 >= max then max |
154 | (_, 0) => 0 |
154 else Int.min (max, Integer.pow k2 k1)) |
155 | (k1, k2) => |
155 | @{typ prop} => 2 |
156 if k1 >= max orelse k2 >= max then max |
156 | @{typ bool} => 2 (* optimization *) |
157 else Int.min (max, Integer.pow k2 k1)) |
157 | @{typ nat} => 0 (* optimization *) |
158 | @{typ prop} => 2 |
158 | Type ("Int.int", []) => 0 (* optimization *) |
159 | @{typ bool} => 2 (* optimization *) |
159 | Type (s, _) => |
160 | @{typ nat} => 0 (* optimization *) |
160 (case datatype_constrs thy T of |
161 | Type ("Int.int", []) => 0 (* optimization *) |
161 constrs as _ :: _ => |
162 | Type (s, _) => |
162 let |
163 (case datatype_constrs thy T of |
163 val constr_cards = |
164 constrs as _ :: _ => |
164 map (Integer.prod o map (aux slack (T :: avoid)) o binder_types |
165 let |
165 o snd) constrs |
166 val constr_cards = |
166 in |
167 map (Integer.prod o map (aux slack (T :: avoid)) o binder_types |
167 if exists (curry (op =) 0) constr_cards then 0 |
168 o snd) constrs |
168 else Int.min (max, Integer.sum constr_cards) |
169 in |
169 end |
170 if exists (curry (op =) 0) constr_cards then 0 |
170 | [] => |
171 else Int.min (max, Integer.sum constr_cards) |
171 case Typedef.get_info ctxt s of |
172 end |
172 ({abs_type, rep_type, ...}, _) :: _ => |
173 | [] => |
173 (* We cheat here by assuming that typedef types are infinite if |
174 case Typedef.get_info ctxt s of |
174 their underlying type is infinite. This is unsound in general |
175 ({abs_type, rep_type, ...}, _) :: _ => |
175 but it's hard to think of a realistic example where this would |
176 (* We cheat here by assuming that typedef types are infinite if |
176 not be the case. We are also slack with representation types: |
177 their underlying type is infinite. This is unsound in general |
177 If a representation type has the form "sigma => tau", we |
178 but it's hard to think of a realistic example where this would |
178 consider it enough to check "sigma" for infiniteness. (Look |
179 not be the case. We are also slack with representation types: |
179 for "slack" in this function.) *) |
180 If a representation type has the form "sigma => tau", we |
180 (case varify_and_instantiate_type ctxt |
181 consider it enough to check "sigma" for infiniteness. (Look |
181 (Logic.varifyT_global abs_type) T |
182 for "slack" in this function.) *) |
182 (Logic.varifyT_global rep_type) |
183 (case varify_and_instantiate_type ctxt |
183 |> aux true avoid of |
184 (Logic.varifyT_global abs_type) T |
184 0 => 0 |
185 (Logic.varifyT_global rep_type) |
185 | 1 => 1 |
186 |> aux true avoid of |
186 | _ => default_card) |
187 0 => 0 |
187 | [] => default_card) |
188 | 1 => 1 |
188 (* Very slightly unsound: Type variables are assumed not to be |
189 | _ => default_card) |
189 constrained to cardinality 1. (In practice, the user would most |
190 | [] => default_card) |
190 likely have used "unit" directly anyway.) *) |
191 (* Very slightly unsound: Type variables are assumed not to be |
191 | TFree _ => if default_card = 1 then 2 else default_card |
192 constrained to cardinality 1. (In practice, the user would most |
192 | TVar _ => default_card |
193 likely have used "unit" directly anyway.) *) |
|
194 | TFree _ => if default_card = 1 then 2 else default_card |
|
195 (* Schematic type variables that contain only unproblematic sorts |
|
196 (with no finiteness axiom) can safely be considered infinite. *) |
|
197 | TVar _ => default_card |
|
198 in Int.min (max, aux false [] T) end |
193 in Int.min (max, aux false [] T) end |
199 |
194 |
200 fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt 0 [] T <> 0 |
195 fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt 0 T <> 0 |
201 fun is_type_surely_infinite ctxt infinite_Ts T = |
196 fun is_type_surely_infinite ctxt T = tiny_card_of_type ctxt 1 T = 0 |
202 tiny_card_of_type ctxt 1 (map (rpair 0) infinite_Ts) T = 0 |
|
203 |
197 |
204 fun monomorphic_term subst = |
198 fun monomorphic_term subst = |
205 map_types (map_type_tvar (fn v => |
199 map_types (map_type_tvar (fn v => |
206 case Type.lookup subst v of |
200 case Type.lookup subst v of |
207 SOME typ => typ |
201 SOME typ => typ |