535 | aggr_neutr f y (x::xs) = aggr_neutr f (f y x) xs; |
536 | aggr_neutr f y (x::xs) = aggr_neutr f (f y x) xs; |
536 |
537 |
537 fun aggregate f [] = NONE |
538 fun aggregate f [] = NONE |
538 | aggregate f (x::xs) = SOME (aggr_neutr f x xs); |
539 | aggregate f (x::xs) = SOME (aggr_neutr f x xs); |
539 |
540 |
540 fun inter_sorts thy = |
541 fun inter_sorts algebra = |
541 let |
542 aggregate (map2 (curry (Sorts.inter_sort algebra))); |
542 val algebra = Sign.classes_of thy; |
|
543 val inters = curry (Sorts.inter_sort algebra); |
|
544 in aggregate (map2 inters) end; |
|
545 |
543 |
546 fun specific_constraints thy (class, tyco) = |
544 fun specific_constraints thy (class, tyco) = |
547 let |
545 let |
548 val vs = Name.invents Name.context "" (Sign.arity_number thy tyco); |
546 val vs = Name.invents Name.context "" (Sign.arity_number thy tyco); |
549 val classparams = (map fst o these o try (#params o AxClass.get_info thy)) class; |
547 val classparams = (map fst o these o try (#params o AxClass.get_info thy)) class; |
550 val funcs = classparams |
548 val funcs = classparams |
551 |> map (fn c => Class.inst_const thy (c, tyco)) |
549 |> map_filter (fn c => try (Class.inst_const thy) (c, tyco)) |
552 |> map (Symtab.lookup ((the_funcs o the_exec) thy)) |
550 |> map (Symtab.lookup ((the_funcs o the_exec) thy)) |
553 |> (map o Option.map) (Susp.force o fst o snd) |
551 |> (map o Option.map) (Susp.force o fst o snd) |
554 |> maps these |
552 |> maps these |
555 |> map (Thm.transfer thy) |
553 |> map (Thm.transfer thy) |
556 fun sorts_of [Type (_, tys)] = map (snd o dest_TVar) tys |
554 fun sorts_of [Type (_, tys)] = map (snd o dest_TVar) tys |
557 | sorts_of tys = map (snd o dest_TVar) tys; |
555 | sorts_of tys = map (snd o dest_TVar) tys; |
558 val sorts = map (sorts_of o Sign.const_typargs thy o CodeUnit.head_func) funcs; |
556 val sorts = map (sorts_of o Sign.const_typargs thy o CodeUnit.head_func) funcs; |
559 in sorts end; |
557 in sorts end; |
560 |
558 |
561 fun weakest_constraints thy (class, tyco) = |
559 fun weakest_constraints thy algebra (class, tyco) = |
562 let |
560 let |
563 val all_superclasses = Sign.complete_sort thy [class]; |
561 val all_superclasses = Sorts.complete_sort algebra [class]; |
564 in case inter_sorts thy (maps (fn class => specific_constraints thy (class, tyco)) all_superclasses) |
562 in case inter_sorts algebra (maps (fn class => specific_constraints thy (class, tyco)) all_superclasses) |
565 of SOME sorts => sorts |
563 of SOME sorts => sorts |
566 | NONE => Sign.arity_sorts thy tyco [class] |
564 | NONE => Sorts.mg_domain algebra tyco [class] |
567 end; |
565 end; |
568 |
566 |
569 fun strongest_constraints thy (class, tyco) = |
567 fun strongest_constraints thy algebra (class, tyco) = |
570 let |
568 let |
571 val algebra = Sign.classes_of thy; |
|
572 val all_subclasses = class :: Graph.all_preds ((#classes o Sorts.rep_algebra) algebra) [class]; |
569 val all_subclasses = class :: Graph.all_preds ((#classes o Sorts.rep_algebra) algebra) [class]; |
573 val inst_subclasses = filter (can (Sorts.mg_domain algebra tyco) o single) all_subclasses; |
570 val inst_subclasses = filter (can (Sorts.mg_domain algebra tyco) o single) all_subclasses; |
574 in case inter_sorts thy (maps (fn class => specific_constraints thy (class, tyco)) inst_subclasses) |
571 in case inter_sorts algebra (maps (fn class => specific_constraints thy (class, tyco)) inst_subclasses) |
575 of SOME sorts => sorts |
572 of SOME sorts => sorts |
576 | NONE => replicate |
573 | NONE => replicate |
577 (Sign.arity_number thy tyco) (Sign.minimize_sort thy (Sign.all_classes thy)) |
574 (Sign.arity_number thy tyco) (Sorts.minimize_sort algebra (Sorts.all_classes algebra)) |
|
575 end; |
|
576 |
|
577 fun get_algebra thy (class, tyco) = |
|
578 let |
|
579 val base_algebra = Sign.classes_of thy; |
|
580 in if can (Sorts.mg_domain base_algebra tyco) [class] |
|
581 then base_algebra |
|
582 else let |
|
583 val superclasses = Sorts.super_classes base_algebra class; |
|
584 val sorts = inter_sorts base_algebra |
|
585 (map_filter (fn class => try (Sorts.mg_domain base_algebra tyco) [class]) superclasses) |
|
586 |> the_default (replicate (Sign.arity_number thy tyco) []) |
|
587 in |
|
588 base_algebra |
|
589 |> Sorts.add_arities (Sign.pp thy) (tyco, [(class, sorts)]) |
|
590 end |
578 end; |
591 end; |
579 |
592 |
580 fun gen_classparam_typ constr thy class (c, tyco) = |
593 fun gen_classparam_typ constr thy class (c, tyco) = |
581 let |
594 let |
|
595 val algebra = get_algebra thy (class, tyco); |
582 val cs = these (try (#params o AxClass.get_info thy) class); |
596 val cs = these (try (#params o AxClass.get_info thy) class); |
583 val ty = (the o AList.lookup (op =) cs) c; |
597 val SOME ty = AList.lookup (op =) cs c; |
584 val sort_args = Name.names (Name.declare Name.aT Name.context) Name.aT |
598 val sort_args = Name.names (Name.declare Name.aT Name.context) Name.aT |
585 (constr thy (class, tyco)); |
599 (constr thy algebra (class, tyco)); |
586 val ty_inst = Type (tyco, map TFree sort_args); |
600 val ty_inst = Type (tyco, map TFree sort_args); |
587 in Logic.varifyT (map_type_tfree (K ty_inst) ty) end; |
601 in Logic.varifyT (map_type_tfree (K ty_inst) ty) end; |
588 |
602 |
589 fun retrieve_algebra thy operational = |
603 fun retrieve_algebra thy operational = |
590 Sorts.subalgebra (Sign.pp thy) operational |
604 Sorts.subalgebra (Sign.pp thy) operational |
591 (weakest_constraints thy) |
605 (weakest_constraints thy (Sign.classes_of thy)) |
592 (Sign.classes_of thy); |
606 (Sign.classes_of thy); |
593 |
607 |
594 in |
608 in |
595 |
609 |
596 fun coregular_algebra thy = retrieve_algebra thy (K true) |> snd; |
610 fun coregular_algebra thy = retrieve_algebra thy (K true) |> snd; |
761 end; |
775 end; |
762 |
776 |
763 val add_default_func_attr = Attrib.internal (fn _ => Thm.declaration_attribute |
777 val add_default_func_attr = Attrib.internal (fn _ => Thm.declaration_attribute |
764 (fn thm => Context.mapping (add_default_func thm) I)); |
778 (fn thm => Context.mapping (add_default_func thm) I)); |
765 |
779 |
|
780 structure TypeInterpretation = InterpretationFun(type T = string * string list val eq = op =); |
|
781 val type_interpretation = TypeInterpretation.interpretation; |
|
782 |
766 fun add_datatype raw_cs thy = |
783 fun add_datatype raw_cs thy = |
767 let |
784 let |
768 val cs = map (fn c_ty as (_, ty) => (Class.unoverload_const thy c_ty, ty)) raw_cs; |
785 val cs = map (fn c_ty as (_, ty) => (Class.unoverload_const thy c_ty, ty)) raw_cs; |
769 val (tyco, vs_cos) = CodeUnit.constrset_of_consts thy cs; |
786 val (tyco, vs_cos) = CodeUnit.constrset_of_consts thy cs; |
770 val purge_cs = map fst (snd vs_cos); |
787 val cs' = map fst (snd vs_cos); |
771 val purge_cs' = case Symtab.lookup ((the_dtyps o the_exec) thy) tyco |
788 val purge_cs = case Symtab.lookup ((the_dtyps o the_exec) thy) tyco |
772 of SOME (vs, cos) => if null cos then NONE else SOME (purge_cs @ map fst cos) |
789 of SOME (vs, cos) => if null cos then NONE else SOME (cs' @ map fst cos) |
773 | NONE => NONE; |
790 | NONE => NONE; |
774 in |
791 in |
775 thy |
792 thy |
776 |> map_exec_purge purge_cs' (map_dtyps (Symtab.update (tyco, vs_cos)) |
793 |> map_exec_purge purge_cs (map_dtyps (Symtab.update (tyco, vs_cos)) |
777 #> map_funcs (fold (Symtab.delete_safe o fst) cs)) |
794 #> map_funcs (fold (Symtab.delete_safe o fst) cs)) |
|
795 |> TypeInterpretation.data (tyco, cs') |
778 end; |
796 end; |
779 |
797 |
780 fun add_datatype_cmd raw_cs thy = |
798 fun add_datatype_cmd raw_cs thy = |
781 let |
799 let |
782 val cs = map (CodeUnit.read_bare_const thy) raw_cs; |
800 val cs = map (CodeUnit.read_bare_const thy) raw_cs; |
835 add_attribute (name, Scan.succeed (mk_attribute f)); |
853 add_attribute (name, Scan.succeed (mk_attribute f)); |
836 fun add_del_attribute (name, (add, del)) = |
854 fun add_del_attribute (name, (add, del)) = |
837 add_attribute (name, Args.del |-- Scan.succeed (mk_attribute del) |
855 add_attribute (name, Args.del |-- Scan.succeed (mk_attribute del) |
838 || Scan.succeed (mk_attribute add)) |
856 || Scan.succeed (mk_attribute add)) |
839 in |
857 in |
840 add_del_attribute ("func", (add_func, del_func)) |
858 TypeInterpretation.init |
|
859 #> add_del_attribute ("func", (add_func, del_func)) |
841 #> add_del_attribute ("inline", (add_inline, del_inline)) |
860 #> add_del_attribute ("inline", (add_inline, del_inline)) |
842 #> add_del_attribute ("post", (add_post, del_post)) |
861 #> add_del_attribute ("post", (add_post, del_post)) |
843 end); |
862 end); |
844 |
863 |
845 |
864 |