105 |
105 |
106 fun is_complete_type dtypes facto (Type (@{type_name fun}, [T1, T2])) = |
106 fun is_complete_type dtypes facto (Type (@{type_name fun}, [T1, T2])) = |
107 is_concrete_type dtypes facto T1 andalso is_complete_type dtypes facto T2 |
107 is_concrete_type dtypes facto T1 andalso is_complete_type dtypes facto T2 |
108 | is_complete_type dtypes facto (Type (@{type_name fin_fun}, [T1, T2])) = |
108 | is_complete_type dtypes facto (Type (@{type_name fin_fun}, [T1, T2])) = |
109 is_exact_type dtypes facto T1 andalso is_complete_type dtypes facto T2 |
109 is_exact_type dtypes facto T1 andalso is_complete_type dtypes facto T2 |
110 | is_complete_type dtypes facto (Type (@{type_name "*"}, Ts)) = |
110 | is_complete_type dtypes facto (Type (@{type_name Product_Type.prod}, Ts)) = |
111 forall (is_complete_type dtypes facto) Ts |
111 forall (is_complete_type dtypes facto) Ts |
112 | is_complete_type dtypes facto T = |
112 | is_complete_type dtypes facto T = |
113 not (is_integer_like_type T) andalso not (is_bit_type T) andalso |
113 not (is_integer_like_type T) andalso not (is_bit_type T) andalso |
114 fun_from_pair (#complete (the (datatype_spec dtypes T))) facto |
114 fun_from_pair (#complete (the (datatype_spec dtypes T))) facto |
115 handle Option.Option => true |
115 handle Option.Option => true |
116 and is_concrete_type dtypes facto (Type (@{type_name fun}, [T1, T2])) = |
116 and is_concrete_type dtypes facto (Type (@{type_name fun}, [T1, T2])) = |
117 is_complete_type dtypes facto T1 andalso is_concrete_type dtypes facto T2 |
117 is_complete_type dtypes facto T1 andalso is_concrete_type dtypes facto T2 |
118 | is_concrete_type dtypes facto (Type (@{type_name fin_fun}, [_, T2])) = |
118 | is_concrete_type dtypes facto (Type (@{type_name fin_fun}, [_, T2])) = |
119 is_concrete_type dtypes facto T2 |
119 is_concrete_type dtypes facto T2 |
120 | is_concrete_type dtypes facto (Type (@{type_name "*"}, Ts)) = |
120 | is_concrete_type dtypes facto (Type (@{type_name Product_Type.prod}, Ts)) = |
121 forall (is_concrete_type dtypes facto) Ts |
121 forall (is_concrete_type dtypes facto) Ts |
122 | is_concrete_type dtypes facto T = |
122 | is_concrete_type dtypes facto T = |
123 fun_from_pair (#concrete (the (datatype_spec dtypes T))) facto |
123 fun_from_pair (#concrete (the (datatype_spec dtypes T))) facto |
124 handle Option.Option => true |
124 handle Option.Option => true |
125 and is_exact_type dtypes facto = |
125 and is_exact_type dtypes facto = |