155 fun find [] _ = error ("cannot find element") |
155 fun find [] _ = error ("cannot find element") |
156 | find ((x, z)::xs) y = if (Long_Name.base_name x) = y then z else find xs y |
156 | find ((x, z)::xs) y = if (Long_Name.base_name x) = y then z else find xs y |
157 *} |
157 *} |
158 |
158 |
159 ML {* |
159 ML {* |
160 fun strip_union t = |
160 fun strip_bn_fun t = |
161 case t of |
161 case t of |
162 Const (@{const_name sup}, _) $ l $ r => strip_union l @ strip_union r |
162 Const (@{const_name sup}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r |
163 | (h as (Const (@{const_name insert}, T))) $ x $ y => |
163 | Const (@{const_name append}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r |
164 (h $ x $ Const (@{const_name bot}, range_type (range_type T))) :: strip_union y |
164 | Const (@{const_name insert}, _) $ (Const (@{const_name atom}, _) $ Bound i) $ y => |
|
165 (i, NONE) :: strip_bn_fun y |
|
166 | Const (@{const_name Cons}, _) $ (Const (@{const_name atom}, _) $ Bound i) $ y => |
|
167 (i, NONE) :: strip_bn_fun y |
165 | Const (@{const_name bot}, _) => [] |
168 | Const (@{const_name bot}, _) => [] |
166 | _ => [t] |
169 | Const (@{const_name Nil}, _) => [] |
167 *} |
170 | (f as Free _) $ Bound i => [(i, SOME f)] |
168 |
171 | _ => error ("Unsupported binding function: " ^ (PolyML.makestring t)) |
169 ML {* |
|
170 fun bn_or_atom t = |
|
171 case t of |
|
172 Const (@{const_name insert}, _) $ (Const (@{const_name atom}, _) $ Bound i) $ |
|
173 Const (@{const_name bot}, _) => (i, NONE) |
|
174 | f $ Bound i => (i, SOME f) |
|
175 | _ => error "Unsupported binding function" |
|
176 *} |
172 *} |
177 |
173 |
178 ML {* |
174 ML {* |
179 fun prep_bn dt_names dts eqs = |
175 fun prep_bn dt_names dts eqs = |
180 let |
176 let |
187 val (bn_fun, [cnstr]) = strip_comb lhs |
183 val (bn_fun, [cnstr]) = strip_comb lhs |
188 val (_, ty) = dest_Free bn_fun |
184 val (_, ty) = dest_Free bn_fun |
189 val (ty_name, _) = dest_Type (domain_type ty) |
185 val (ty_name, _) = dest_Type (domain_type ty) |
190 val dt_index = find_index (fn x => x = ty_name) dt_names |
186 val dt_index = find_index (fn x => x = ty_name) dt_names |
191 val (cnstr_head, cnstr_args) = strip_comb cnstr |
187 val (cnstr_head, cnstr_args) = strip_comb cnstr |
192 val rhs_elements = map bn_or_atom (strip_union rhs) |
188 val rhs_elements = strip_bn_fun rhs |
193 val included = map (apfst (fn i => length (cnstr_args) - i - 1)) rhs_elements |
189 val included = map (apfst (fn i => length (cnstr_args) - i - 1)) rhs_elements |
194 in |
190 in |
195 (dt_index, (bn_fun, (cnstr_head, included))) |
191 (dt_index, (bn_fun, (cnstr_head, included))) |
196 end |
192 end |
197 fun order dts i ts = |
193 fun order dts i ts = |