528 fold (fn (dtco, (_, spec)) => CodegenData.add_datatype (dtco, spec)) dtspecs; |
528 fold (fn (dtco, (_, spec)) => CodegenData.add_datatype (dtco, spec)) dtspecs; |
529 |
529 |
530 |
530 |
531 (* instrumentalizing the sort algebra *) |
531 (* instrumentalizing the sort algebra *) |
532 |
532 |
533 (*fun assume_arities_of_sort thy arities ty_sort = |
|
534 let |
|
535 val pp = Sign.pp thy; |
|
536 val algebra = Sign.classes_of thy |
|
537 |> fold (fn (tyco, asorts, sort) => |
|
538 Sorts.add_arities pp (tyco, map (fn class => (class, asorts)) sort)) arities; |
|
539 in Sorts.of_sort algebra ty_sort end; |
|
540 |
|
541 fun get_codetypes_arities thy tycos sort = |
|
542 let |
|
543 val algebra = Sign.classes_of thy; |
|
544 val (vs_proto, css_proto) = the_codetypes_mut_specs thy tycos; |
|
545 val vs = map (fn (v, vsort) => (v, Sorts.inter_sort algebra (vsort, sort))) vs_proto; |
|
546 fun inst_type tyco (c, tys) = |
|
547 let |
|
548 val tys' = (map o map_atyps) |
|
549 (fn TFree (v, _) => TFree (v, the (AList.lookup (op =) vs v))) tys |
|
550 in (c, tys') end; |
|
551 val css = map (fn (tyco, (_, cs)) => (tyco, (map (inst_type tyco) cs))) css_proto; |
|
552 fun mk_arity tyco = (tyco, map snd vs, sort); |
|
553 fun typ_of_sort ty = |
|
554 let |
|
555 val arities = map (fn (tyco, _) => (tyco, map snd vs, sort)) css; |
|
556 in assume_arities_of_sort thy arities (ty, sort) end; |
|
557 fun mk_cons tyco (c, tys) = |
|
558 let |
|
559 val ts = Name.names Name.context "a" tys; |
|
560 val ty = tys ---> Type (tyco, map TFree vs); |
|
561 in list_comb (Const (c, ty), map Free ts) end; |
|
562 in if forall (fn (_, cs) => forall (fn (_, tys) => forall typ_of_sort tys) cs) css |
|
563 then SOME ( |
|
564 map (fn (tyco, cs) => (tyco, (mk_arity tyco, map (mk_cons tyco) cs))) css |
|
565 ) else NONE |
|
566 end;*) |
|
567 |
|
568 fun get_codetypes_arities thy tycos sort = |
533 fun get_codetypes_arities thy tycos sort = |
569 let |
534 let |
570 val pp = Sign.pp thy; |
535 val pp = Sign.pp thy; |
571 val algebra = Sign.classes_of thy; |
536 val algebra = Sign.classes_of thy; |
572 val (vs_proto, css_proto) = the_codetypes_mut_specs thy tycos; |
537 val (vs_proto, css_proto) = the_codetypes_mut_specs thy tycos; |