60 |
60 |
61 val disc_of_ctr_spec: ('c, 'a) ctr_spec -> binding |
61 val disc_of_ctr_spec: ('c, 'a) ctr_spec -> binding |
62 val ctr_of_ctr_spec: ('c, 'a) ctr_spec -> 'c |
62 val ctr_of_ctr_spec: ('c, 'a) ctr_spec -> 'c |
63 val args_of_ctr_spec: ('c, 'a) ctr_spec -> 'a list |
63 val args_of_ctr_spec: ('c, 'a) ctr_spec -> 'a list |
64 |
64 |
|
65 val fake_local_theory_for_sel_defaults: (binding * typ) list -> Proof.context -> Proof.context |
65 val free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list -> |
66 val free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list -> |
66 (((bool * bool) * binding) * (term, binding) ctr_spec list) * term list -> local_theory -> |
67 (((bool * bool) * binding) * (term, binding) ctr_spec list) * term list -> local_theory -> |
67 ctr_sugar * local_theory |
68 ctr_sugar * local_theory |
68 val parse_bound_term: (binding * string) parser |
69 val parse_bound_term: (binding * string) parser |
69 val parse_ctr_options: (bool * bool) parser |
70 val parse_ctr_options: (bool * bool) parser |
326 ((ctr, sel), fold_rev Term.lambda vars rhs) |
327 ((ctr, sel), fold_rev Term.lambda vars rhs) |
327 else |
328 else |
328 malformed () |
329 malformed () |
329 end; |
330 end; |
330 |
331 |
|
332 (* Ideally, we would enrich the context with constants rather than free variables. *) |
|
333 fun fake_local_theory_for_sel_defaults sel_bTs = |
|
334 Proof_Context.allow_dummies |
|
335 #> Proof_Context.add_fixes (map (fn (b, T) => (b, SOME T, NoSyn)) sel_bTs) |
|
336 #> snd; |
|
337 |
331 type ('c, 'a) ctr_spec = (binding * 'c) * 'a list; |
338 type ('c, 'a) ctr_spec = (binding * 'c) * 'a list; |
332 |
339 |
333 fun disc_of_ctr_spec ((disc, _), _) = disc; |
340 fun disc_of_ctr_spec ((disc, _), _) = disc; |
334 fun ctr_of_ctr_spec ((_, ctr), _) = ctr; |
341 fun ctr_of_ctr_spec ((_, ctr), _) = ctr; |
335 fun args_of_ctr_spec (_, args) = args; |
342 fun args_of_ctr_spec (_, args) = args; |
499 val (all_sels_distinct, discs, selss, disc_defs, sel_defs, sel_defss, lthy') = |
506 val (all_sels_distinct, discs, selss, disc_defs, sel_defs, sel_defss, lthy') = |
500 if no_discs_sels then |
507 if no_discs_sels then |
501 (true, [], [], [], [], [], lthy') |
508 (true, [], [], [], [], [], lthy') |
502 else |
509 else |
503 let |
510 let |
504 val sel_bindings = flat sel_bindingss; |
511 val all_sel_bindings = flat sel_bindingss; |
505 val uniq_sel_bindings = distinct Binding.eq_name sel_bindings; |
512 val num_all_sel_bindings = length all_sel_bindings; |
506 val all_sels_distinct = (length uniq_sel_bindings = length sel_bindings); |
513 val uniq_sel_bindings = distinct Binding.eq_name all_sel_bindings; |
|
514 val all_sels_distinct = (length uniq_sel_bindings = num_all_sel_bindings); |
507 |
515 |
508 val sel_binding_index = |
516 val sel_binding_index = |
509 if all_sels_distinct then 1 upto length sel_bindings |
517 if all_sels_distinct then |
510 else map (fn b => find_index (curry Binding.eq_name b) uniq_sel_bindings) sel_bindings; |
518 1 upto num_all_sel_bindings |
511 |
519 else |
512 val all_proto_sels = flat (map3 (fn k => fn xs => map (fn x => (k, (xs, x)))) ks xss xss); |
520 map (fn b => find_index (curry Binding.eq_name b) uniq_sel_bindings) all_sel_bindings; |
|
521 |
|
522 val all_proto_sels = flat (map3 (fn k => fn xs => map (pair k o pair xs)) ks xss xss); |
513 val sel_infos = |
523 val sel_infos = |
514 AList.group (op =) (sel_binding_index ~~ all_proto_sels) |
524 AList.group (op =) (sel_binding_index ~~ all_proto_sels) |
515 |> sort (int_ord o pairself fst) |
525 |> sort (int_ord o pairself fst) |
516 |> map snd |> curry (op ~~) uniq_sel_bindings; |
526 |> map snd |> curry (op ~~) uniq_sel_bindings; |
517 val sel_bindings = map fst sel_infos; |
527 val sel_bindings = map fst sel_infos; |
518 val sel_Ts = map (curry (op -->) fcT o fastype_of o snd o snd o hd o snd) sel_infos; |
|
519 |
|
520 val sel_default_lthy = no_defs_lthy |
|
521 |> Proof_Context.allow_dummies |
|
522 |> Proof_Context.add_fixes |
|
523 (map2 (fn b => fn T => (b, SOME T, NoSyn)) sel_bindings sel_Ts) |
|
524 |> snd; |
|
525 |
528 |
526 val sel_defaults = |
529 val sel_defaults = |
527 map (extract_sel_default sel_default_lthy o prep_term sel_default_lthy) sel_default_eqs; |
530 if null sel_default_eqs then |
|
531 [] |
|
532 else |
|
533 let |
|
534 val sel_Ts = map (curry (op -->) fcT o fastype_of o snd o snd o hd o snd) sel_infos; |
|
535 val fake_lthy = |
|
536 fake_local_theory_for_sel_defaults (sel_bindings ~~ sel_Ts) no_defs_lthy; |
|
537 in |
|
538 map (extract_sel_default fake_lthy o prep_term fake_lthy) sel_default_eqs |
|
539 end; |
528 |
540 |
529 fun disc_free b = Free (Binding.name_of b, mk_pred1T fcT); |
541 fun disc_free b = Free (Binding.name_of b, mk_pred1T fcT); |
530 |
542 |
531 fun disc_spec b exist_xs_u_eq_ctr = mk_Trueprop_eq (disc_free b $ u, exist_xs_u_eq_ctr); |
543 fun disc_spec b exist_xs_u_eq_ctr = mk_Trueprop_eq (disc_free b $ u, exist_xs_u_eq_ctr); |
532 |
544 |