equal
deleted
inserted
replaced
119 datatype_cache = Unsynchronized.ref [], |
119 datatype_cache = Unsynchronized.ref [], |
120 constr_cache = Unsynchronized.ref []} : cdata) |
120 constr_cache = Unsynchronized.ref []} : cdata) |
121 |
121 |
122 (* typ -> typ -> bool *) |
122 (* typ -> typ -> bool *) |
123 fun could_exist_alpha_subtype alpha_T (T as Type (_, Ts)) = |
123 fun could_exist_alpha_subtype alpha_T (T as Type (_, Ts)) = |
124 T = alpha_T orelse (not (is_fp_iterator_type T) |
124 T = alpha_T orelse (not (is_fp_iterator_type T) andalso |
125 andalso exists (could_exist_alpha_subtype alpha_T) Ts) |
125 exists (could_exist_alpha_subtype alpha_T) Ts) |
126 | could_exist_alpha_subtype alpha_T T = (T = alpha_T) |
126 | could_exist_alpha_subtype alpha_T T = (T = alpha_T) |
127 (* theory -> typ -> typ -> bool *) |
127 (* theory -> typ -> typ -> bool *) |
128 fun could_exist_alpha_sub_ctype _ (alpha_T as TFree _) T = |
128 fun could_exist_alpha_sub_ctype _ (alpha_T as TFree _) T = |
129 could_exist_alpha_subtype alpha_T T |
129 could_exist_alpha_subtype alpha_T T |
130 | could_exist_alpha_sub_ctype thy alpha_T T = |
130 | could_exist_alpha_sub_ctype thy alpha_T T = |
193 (* typ -> typ -> ctype *) |
193 (* typ -> typ -> ctype *) |
194 fun do_fun T1 T2 = |
194 fun do_fun T1 T2 = |
195 let |
195 let |
196 val C1 = do_type T1 |
196 val C1 = do_type T1 |
197 val C2 = do_type T2 |
197 val C2 = do_type T2 |
198 val a = if is_boolean_type (body_type T2) |
198 val a = if is_boolean_type (body_type T2) andalso |
199 andalso exists_alpha_sub_ctype_fresh C1 then |
199 exists_alpha_sub_ctype_fresh C1 then |
200 V (Unsynchronized.inc max_fresh) |
200 V (Unsynchronized.inc max_fresh) |
201 else |
201 else |
202 S Neg |
202 S Neg |
203 in CFun (C1, a, C2) end |
203 in CFun (C1, a, C2) end |
204 (* typ -> ctype *) |
204 (* typ -> ctype *) |