451 end |
451 end |
452 |
452 |
453 fun annotate_eqns thy algbr eqngr (c, ty) eqns = |
453 fun annotate_eqns thy algbr eqngr (c, ty) eqns = |
454 map (apfst (fn (args, (rhs, some_abs)) => (args, |
454 map (apfst (fn (args, (rhs, some_abs)) => (args, |
455 (annotate thy algbr eqngr (c, ty) args rhs, some_abs)))) eqns |
455 (annotate thy algbr eqngr (c, ty) args rhs, some_abs)))) eqns |
|
456 |
|
457 |
|
458 (* abstract dictionary construction *) |
|
459 |
|
460 datatype typarg_witness = |
|
461 Weakening of (class * class) list * plain_typarg_witness |
|
462 and plain_typarg_witness = |
|
463 Global of (string * class) * typarg_witness list list |
|
464 | Local of string * (int * sort); |
|
465 |
|
466 fun construct_dictionaries thy (proj_sort, algebra) permissive some_thm (ty, sort) (dep, program) = |
|
467 let |
|
468 fun class_relation ((Weakening (classrels, x)), sub_class) super_class = |
|
469 Weakening ((sub_class, super_class) :: classrels, x); |
|
470 fun type_constructor (tyco, _) dss class = |
|
471 Weakening ([], Global ((tyco, class), (map o map) fst dss)); |
|
472 fun type_variable (TFree (v, sort)) = |
|
473 let |
|
474 val sort' = proj_sort sort; |
|
475 in map_index (fn (n, class) => (Weakening ([], Local (v, (n, sort'))), class)) sort' end; |
|
476 val typarg_witnesses = Sorts.of_sort_derivation algebra |
|
477 {class_relation = K (Sorts.classrel_derivation algebra class_relation), |
|
478 type_constructor = type_constructor, |
|
479 type_variable = type_variable} (ty, proj_sort sort) |
|
480 handle Sorts.CLASS_ERROR e => not_wellsorted thy permissive some_thm ty sort e; |
|
481 in (typarg_witnesses, (dep, program)) end; |
456 |
482 |
457 |
483 |
458 (* translation *) |
484 (* translation *) |
459 |
485 |
460 fun ensure_tyco thy algbr eqngr permissive tyco = |
486 fun ensure_tyco thy algbr eqngr permissive tyco = |
693 and translate_tyvar_sort thy (algbr as (proj_sort, _)) eqngr permissive (v, sort) = |
719 and translate_tyvar_sort thy (algbr as (proj_sort, _)) eqngr permissive (v, sort) = |
694 fold_map (ensure_class thy algbr eqngr permissive) (proj_sort sort) |
720 fold_map (ensure_class thy algbr eqngr permissive) (proj_sort sort) |
695 #>> (fn sort => (unprefix "'" v, sort)) |
721 #>> (fn sort => (unprefix "'" v, sort)) |
696 and translate_dicts thy (algbr as (proj_sort, algebra)) eqngr permissive some_thm (ty, sort) = |
722 and translate_dicts thy (algbr as (proj_sort, algebra)) eqngr permissive some_thm (ty, sort) = |
697 let |
723 let |
698 datatype typarg_witness = |
|
699 Weakening of (class * class) list * plain_typarg_witness |
|
700 and plain_typarg_witness = |
|
701 Global of (string * class) * typarg_witness list list |
|
702 | Local of string * (int * sort); |
|
703 fun class_relation ((Weakening (classrels, x)), sub_class) super_class = |
|
704 Weakening ((sub_class, super_class) :: classrels, x); |
|
705 fun type_constructor (tyco, _) dss class = |
|
706 Weakening ([], Global ((tyco, class), (map o map) fst dss)); |
|
707 fun type_variable (TFree (v, sort)) = |
|
708 let |
|
709 val sort' = proj_sort sort; |
|
710 in map_index (fn (n, class) => (Weakening ([], Local (v, (n, sort'))), class)) sort' end; |
|
711 val typarg_witnesses = Sorts.of_sort_derivation algebra |
|
712 {class_relation = K (Sorts.classrel_derivation algebra class_relation), |
|
713 type_constructor = type_constructor, |
|
714 type_variable = type_variable} (ty, proj_sort sort) |
|
715 handle Sorts.CLASS_ERROR e => not_wellsorted thy permissive some_thm ty sort e; |
|
716 fun mk_dict (Weakening (classrels, x)) = |
724 fun mk_dict (Weakening (classrels, x)) = |
717 fold_map (ensure_classrel thy algbr eqngr permissive) classrels |
725 fold_map (ensure_classrel thy algbr eqngr permissive) classrels |
718 ##>> mk_plain_dict x |
726 ##>> mk_plain_dict x |
719 #>> Dict |
727 #>> Dict |
720 and mk_plain_dict (Global (inst, dss)) = |
728 and mk_plain_dict (Global (inst, dss)) = |
721 ensure_inst thy algbr eqngr permissive inst |
729 ensure_inst thy algbr eqngr permissive inst |
722 ##>> (fold_map o fold_map) mk_dict dss |
730 ##>> (fold_map o fold_map) mk_dict dss |
723 #>> (fn (inst, dss) => Dict_Const (inst, dss)) |
731 #>> (fn (inst, dss) => Dict_Const (inst, dss)) |
724 | mk_plain_dict (Local (v, (n, sort))) = |
732 | mk_plain_dict (Local (v, (n, sort))) = |
725 pair (Dict_Var (unprefix "'" v, (n, length sort))) |
733 pair (Dict_Var (unprefix "'" v, (n, length sort))) |
726 in fold_map mk_dict typarg_witnesses end; |
734 in |
|
735 construct_dictionaries thy algbr permissive some_thm (ty, sort) |
|
736 #-> (fn typarg_witnesses => fold_map mk_dict typarg_witnesses) |
|
737 end; |
727 |
738 |
728 |
739 |
729 (* store *) |
740 (* store *) |
730 |
741 |
731 structure Program = Code_Data |
742 structure Program = Code_Data |