98 (* dtype_spec list -> typ -> bool *) |
98 (* dtype_spec list -> typ -> bool *) |
99 fun is_precise_type dtypes (Type ("fun", Ts)) = |
99 fun is_precise_type dtypes (Type ("fun", Ts)) = |
100 forall (is_precise_type dtypes) Ts |
100 forall (is_precise_type dtypes) Ts |
101 | is_precise_type dtypes (Type ("*", Ts)) = forall (is_precise_type dtypes) Ts |
101 | is_precise_type dtypes (Type ("*", Ts)) = forall (is_precise_type dtypes) Ts |
102 | is_precise_type dtypes T = |
102 | is_precise_type dtypes T = |
103 T <> nat_T andalso T <> int_T |
103 not (is_integer_type T) andalso #precise (the (datatype_spec dtypes T)) |
104 andalso #precise (the (datatype_spec dtypes T)) |
|
105 handle Option.Option => true |
104 handle Option.Option => true |
106 fun is_fully_comparable_type dtypes (Type ("fun", [T1, T2])) = |
105 fun is_fully_comparable_type dtypes (Type ("fun", [T1, T2])) = |
107 is_precise_type dtypes T1 andalso is_fully_comparable_type dtypes T2 |
106 is_precise_type dtypes T1 andalso is_fully_comparable_type dtypes T2 |
108 | is_fully_comparable_type dtypes (Type ("*", Ts)) = |
107 | is_fully_comparable_type dtypes (Type ("*", Ts)) = |
109 forall (is_fully_comparable_type dtypes) Ts |
108 forall (is_fully_comparable_type dtypes) Ts |