203 val (cnstr_head, cnstr_args) = strip_comb cnstr |
203 val (cnstr_head, cnstr_args) = strip_comb cnstr |
204 val rhs_elements = strip_bn_fun rhs |
204 val rhs_elements = strip_bn_fun rhs |
205 val included = map (apfst (fn i => length (cnstr_args) - i - 1)) rhs_elements |
205 val included = map (apfst (fn i => length (cnstr_args) - i - 1)) rhs_elements |
206 in |
206 in |
207 (dt_index, (bn_fun, (cnstr_head, included))) |
207 (dt_index, (bn_fun, (cnstr_head, included))) |
|
208 end |
|
209 fun aux2 eq = |
|
210 let |
|
211 val (lhs, rhs) = eq |
|
212 |> strip_qnt_body "all" |
|
213 |> HOLogic.dest_Trueprop |
|
214 |> HOLogic.dest_eq |
|
215 val (bn_fun, [cnstr]) = strip_comb lhs |
|
216 val (_, ty) = dest_Free bn_fun |
|
217 val (ty_name, _) = dest_Type (domain_type ty) |
|
218 val dt_index = find_index (fn x => x = ty_name) dt_names |
|
219 val (cnstr_head, cnstr_args) = strip_comb cnstr |
|
220 val rhs_elements = strip_bn_fun rhs |
|
221 val included = map (apfst (fn i => length (cnstr_args) - i - 1)) rhs_elements |
|
222 in |
|
223 (bn_fun, dt_index, (cnstr_head, included)) |
208 end |
224 end |
209 fun order dts i ts = |
225 fun order dts i ts = |
210 let |
226 let |
211 val dt = nth dts i |
227 val dt = nth dts i |
212 val cts = map (fn (x, _, _) => Binding.name_of x) ((fn (_, _, _, x) => x) dt) |
228 val cts = map (fn (x, _, _) => Binding.name_of x) ((fn (_, _, _, x) => x) dt) |
217 |
233 |
218 val unordered = AList.group (op=) (map aux eqs) |
234 val unordered = AList.group (op=) (map aux eqs) |
219 val unordered' = map (fn (x, y) => (x, AList.group (op=) y)) unordered |
235 val unordered' = map (fn (x, y) => (x, AList.group (op=) y)) unordered |
220 val ordered = map (fn (x, y) => (x, map (fn (v, z) => (v, order dts x z)) y)) unordered' |
236 val ordered = map (fn (x, y) => (x, map (fn (v, z) => (v, order dts x z)) y)) unordered' |
221 val ordered' = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) ordered) |
237 val ordered' = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) ordered) |
222 in |
238 |
223 ordered' |
239 val _ = tracing ("eqs\n" ^ cat_lines (map (Syntax.string_of_term lthy) eqs)) |
|
240 val _ = tracing ("map eqs\n" ^ @{make_string} (map aux2 eqs)) |
|
241 val _ = tracing ("ordered'\n" ^ @{make_string} ordered') |
|
242 in |
|
243 ordered' (*map aux2 eqs*) |
224 end |
244 end |
225 *} |
245 *} |
226 |
246 |
227 ML {* |
247 ML {* |
228 fun raw_nominal_decls dts bn_funs bn_eqs binds lthy = |
248 fun raw_nominal_decls dts bn_funs bn_eqs binds lthy = |
252 |
272 |
253 val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs |
273 val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs |
254 |
274 |
255 val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env binds |
275 val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env binds |
256 |
276 |
257 val raw_bns = prep_bn dt_full_names' raw_dts (map snd raw_bn_eqs) |
277 val raw_bns = prep_bn lthy dt_full_names' raw_dts (map snd raw_bn_eqs) |
258 in |
278 in |
259 lthy |
279 lthy |
260 |> add_datatype_wrapper raw_dt_names raw_dts |
280 |> add_datatype_wrapper raw_dt_names raw_dts |
261 ||>> add_primrec_wrapper raw_bn_funs raw_bn_eqs |
281 ||>> add_primrec_wrapper raw_bn_funs raw_bn_eqs |
262 ||>> pair raw_bclauses |
282 ||>> pair raw_bclauses |