695 |
695 |
696 fun decode_type thy t = |
696 fun decode_type thy t = |
697 let |
697 let |
698 fun get_sort env xi = |
698 fun get_sort env xi = |
699 the_default (Sign.defaultS thy) (AList.lookup (op =) env (xi: indexname)); |
699 the_default (Sign.defaultS thy) (AList.lookup (op =) env (xi: indexname)); |
700 val map_sort = Sign.intern_sort thy; |
|
701 in |
700 in |
702 Syntax.typ_of_term (get_sort (Syntax.term_sorts map_sort t)) map_sort t |
701 Syntax.typ_of_term (get_sort (Syntax.term_sorts t)) t |
703 |> Sign.intern_tycons thy |
|
704 end; |
702 end; |
705 |
703 |
706 |
704 |
707 (* parse translations *) |
705 (* parse translations *) |
708 |
706 |
750 map (Syntax.term_of_typ (! Syntax.show_sorts) o Envir.norm_type subst o varifyT) |
748 map (Syntax.term_of_typ (! Syntax.show_sorts) o Envir.norm_type subst o varifyT) |
751 (but_last alphas); |
749 (but_last alphas); |
752 |
750 |
753 val more' = mk_ext rest; |
751 val more' = mk_ext rest; |
754 in |
752 in |
755 (* FIXME authentic syntax *) |
753 list_comb |
756 list_comb (Syntax.const (suffix ext_typeN ext), alphas' @ [more']) |
754 (Syntax.const (Syntax.mark_type (suffix ext_typeN ext)), alphas' @ [more']) |
757 end |
755 end |
758 | NONE => err ("no fields defined for " ^ ext)) |
756 | NONE => err ("no fields defined for " ^ ext)) |
759 | NONE => err (name ^ " is no proper field")) |
757 | NONE => err (name ^ " is no proper field")) |
760 | mk_ext [] = more; |
758 | mk_ext [] = more; |
761 in |
759 in |
920 val midx = maxidx_of_typ T; |
918 val midx = maxidx_of_typ T; |
921 val varifyT = varifyT midx; |
919 val varifyT = varifyT midx; |
922 |
920 |
923 fun mk_type_abbr subst name alphas = |
921 fun mk_type_abbr subst name alphas = |
924 let val abbrT = Type (name, map (fn a => varifyT (TFree (a, Sign.defaultS thy))) alphas) in |
922 let val abbrT = Type (name, map (fn a => varifyT (TFree (a, Sign.defaultS thy))) alphas) in |
925 Syntax.term_of_typ (! Syntax.show_sorts) |
923 Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT) |
926 (Sign.extern_typ thy (Envir.norm_type subst abbrT)) |
|
927 end; |
924 end; |
928 |
925 |
929 fun match rT T = Sign.typ_match thy (varifyT rT, T) Vartab.empty; |
926 fun match rT T = Sign.typ_match thy (varifyT rT, T) Vartab.empty; |
930 in |
927 in |
931 if ! print_record_type_abbr then |
928 if ! print_record_type_abbr then |
944 |
941 |
945 in |
942 in |
946 |
943 |
947 fun record_ext_type_tr' name = |
944 fun record_ext_type_tr' name = |
948 let |
945 let |
949 val ext_type_name = suffix ext_typeN name; |
946 val ext_type_name = Syntax.mark_type (suffix ext_typeN name); |
950 fun tr' ctxt ts = |
947 fun tr' ctxt ts = |
951 record_type_tr' ctxt (list_comb (Syntax.const ext_type_name, ts)); |
948 record_type_tr' ctxt (list_comb (Syntax.const ext_type_name, ts)); |
952 in (ext_type_name, tr') end; |
949 in (ext_type_name, tr') end; |
953 |
950 |
954 fun record_ext_type_abbr_tr' abbr alphas zeta last_ext schemeT name = |
951 fun record_ext_type_abbr_tr' abbr alphas zeta last_ext schemeT name = |
955 let |
952 let |
956 val ext_type_name = suffix ext_typeN name; |
953 val ext_type_name = Syntax.mark_type (suffix ext_typeN name); |
957 fun tr' ctxt ts = |
954 fun tr' ctxt ts = |
958 record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt |
955 record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt |
959 (list_comb (Syntax.const ext_type_name, ts)); |
956 (list_comb (Syntax.const ext_type_name, ts)); |
960 in (ext_type_name, tr') end; |
957 in (ext_type_name, tr') end; |
961 |
958 |
1947 fun mk_rec args n = |
1944 fun mk_rec args n = |
1948 let |
1945 let |
1949 val (args', more) = chop_last args; |
1946 val (args', more) = chop_last args; |
1950 fun mk_ext' ((name, T), args) more = mk_ext (name, T) (args @ [more]); |
1947 fun mk_ext' ((name, T), args) more = mk_ext (name, T) (args @ [more]); |
1951 fun build Ts = |
1948 fun build Ts = |
1952 fold_rev mk_ext' (drop n ((extension_names ~~ Ts) ~~ chunks parent_chunks args')) |
1949 fold_rev mk_ext' (drop n ((extension_names ~~ Ts) ~~ chunks parent_chunks args')) more; |
1953 more; |
|
1954 in |
1950 in |
1955 if more = HOLogic.unit |
1951 if more = HOLogic.unit |
1956 then build (map_range recT (parent_len + 1)) |
1952 then build (map_range recT (parent_len + 1)) |
1957 else build (map_range rec_schemeT (parent_len + 1)) |
1953 else build (map_range rec_schemeT (parent_len + 1)) |
1958 end; |
1954 end; |
1959 |
1955 |
1960 val r_rec0 = mk_rec all_vars_more 0; |
1956 val r_rec0 = mk_rec all_vars_more 0; |
1961 val r_rec_unit0 = mk_rec (all_vars @ [HOLogic.unit]) 0; |
1957 val r_rec_unit0 = mk_rec (all_vars @ [HOLogic.unit]) 0; |
1962 |
1958 |
1963 fun r n = Free (rN, rec_schemeT n) |
1959 fun r n = Free (rN, rec_schemeT n); |
1964 val r0 = r 0; |
1960 val r0 = r 0; |
1965 fun r_unit n = Free (rN, recT n) |
1961 fun r_unit n = Free (rN, recT n); |
1966 val r_unit0 = r_unit 0; |
1962 val r_unit0 = r_unit 0; |
1967 val w = Free (wN, rec_schemeT 0) |
1963 val w = Free (wN, rec_schemeT 0); |
1968 |
1964 |
1969 |
1965 |
1970 (* print translations *) |
1966 (* print translations *) |
1971 |
|
1972 val external_names = Name_Space.external_names (Sign.naming_of ext_thy); |
|
1973 |
1967 |
1974 val record_ext_type_abbr_tr's = |
1968 val record_ext_type_abbr_tr's = |
1975 let |
1969 let |
1976 val trnames = external_names (hd extension_names); |
1970 val trname = hd extension_names; |
1977 val last_ext = unsuffix ext_typeN (fst extension); |
1971 val last_ext = unsuffix ext_typeN (fst extension); |
1978 in map (record_ext_type_abbr_tr' name alphas zeta last_ext rec_schemeT0) trnames end; |
1972 in [record_ext_type_abbr_tr' name alphas zeta last_ext rec_schemeT0 trname] end; |
1979 |
1973 |
1980 val record_ext_type_tr's = |
1974 val record_ext_type_tr's = |
1981 let |
1975 let |
1982 (*avoid conflict with record_type_abbr_tr's*) |
1976 (*avoid conflict with record_type_abbr_tr's*) |
1983 val trnames = if parent_len > 0 then external_names extension_name else []; |
1977 val trnames = if parent_len > 0 then [extension_name] else []; |
1984 in map record_ext_type_tr' trnames end; |
1978 in map record_ext_type_tr' trnames end; |
1985 |
1979 |
1986 val advanced_print_translation = |
1980 val advanced_print_translation = |
1987 map field_update_tr' (full_moreN :: names) @ [record_ext_tr' extension_name] @ |
1981 map field_update_tr' (full_moreN :: names) @ [record_ext_tr' extension_name] @ |
1988 record_ext_type_tr's @ record_ext_type_abbr_tr's; |
1982 record_ext_type_tr's @ record_ext_type_abbr_tr's; |