57 val instance_arity_cmd: bstring * xstring list * xstring -> theory -> Proof.state |
57 val instance_arity_cmd: bstring * xstring list * xstring -> theory -> Proof.state |
58 end; |
58 end; |
59 |
59 |
60 structure Class : CLASS = |
60 structure Class : CLASS = |
61 struct |
61 struct |
|
62 |
|
63 (*temporary adaption code to mediate between old and new locale code*) |
|
64 |
|
65 structure Old_Locale = |
|
66 struct |
|
67 |
|
68 val intro_locales_tac = Locale.intro_locales_tac; (*already forked!*) |
|
69 |
|
70 val interpretation = Locale.interpretation; |
|
71 val interpretation_in_locale = Locale.interpretation_in_locale; |
|
72 val get_interpret_morph = Locale.get_interpret_morph; |
|
73 val Locale = Locale.Locale; |
|
74 val extern = Locale.extern; |
|
75 val intros = Locale.intros; |
|
76 val dests = Locale.dests; |
|
77 val init = Locale.init; |
|
78 val Merge = Locale.Merge; |
|
79 val parameters_of_expr = Locale.parameters_of_expr; |
|
80 val empty = Locale.empty; |
|
81 val cert_expr = Locale.cert_expr; |
|
82 val read_expr = Locale.read_expr; |
|
83 val parameters_of = Locale.parameters_of; |
|
84 val add_locale = Locale.add_locale; |
|
85 |
|
86 end; |
|
87 |
|
88 structure New_Locale = |
|
89 struct |
|
90 |
|
91 val intro_locales_tac = Locale.intro_locales_tac; (*already forked!*) |
|
92 |
|
93 val interpretation = Locale.interpretation; (*!*) |
|
94 val interpretation_in_locale = Locale.interpretation_in_locale; (*!*) |
|
95 val get_interpret_morph = Locale.get_interpret_morph; (*!*) |
|
96 fun Locale loc = ([(loc, ("", Expression.Positional []))], []); |
|
97 val extern = NewLocale.extern; |
|
98 val intros = Locale.intros; (*!*) |
|
99 val dests = Locale.dests; (*!*) |
|
100 val init = NewLocale.init; |
|
101 fun Merge locs = (map (fn loc => (loc, ("", Expression.Positional []))) locs, []); |
|
102 val parameters_of_expr = Locale.parameters_of_expr; (*!*) |
|
103 val empty = ([], []); |
|
104 val cert_expr = Locale.cert_expr; (*!"*) |
|
105 val read_expr = Locale.read_expr; (*!"*) |
|
106 val parameters_of = NewLocale.params_of; (*why typ option?*) |
|
107 val add_locale = Expression.add_locale; |
|
108 |
|
109 end; |
|
110 |
|
111 structure Locale = Old_Locale; |
|
112 |
|
113 (*proper code again*) |
|
114 |
62 |
115 |
63 (** auxiliary **) |
116 (** auxiliary **) |
64 |
117 |
65 fun prove_interpretation tac prfx_atts expr inst = |
118 fun prove_interpretation tac prfx_atts expr inst = |
66 Locale.interpretation I prfx_atts expr inst |
119 Locale.interpretation I prfx_atts expr inst |
540 foldr1 (Sorts.inter_sort (Sign.classes_of thy)) |
593 foldr1 (Sorts.inter_sort (Sign.classes_of thy)) |
541 (map (#base_sort o the_class_data thy) sups); |
594 (map (#base_sort o the_class_data thy) sups); |
542 val suplocales = map Locale.Locale sups; |
595 val suplocales = map Locale.Locale sups; |
543 val supexpr = Locale.Merge suplocales; |
596 val supexpr = Locale.Merge suplocales; |
544 val supparams = (map fst o Locale.parameters_of_expr thy) supexpr; |
597 val supparams = (map fst o Locale.parameters_of_expr thy) supexpr; |
545 val mergeexpr = Locale.Merge (suplocales); |
598 val mergeexpr = Locale.Merge suplocales; |
546 val constrain = Element.Constrains ((map o apsnd o map_atyps) |
599 val constrain = Element.Constrains ((map o apsnd o map_atyps) |
547 (K (TFree (Name.aT, base_sort))) supparams); |
600 (K (TFree (Name.aT, base_sort))) supparams); |
548 fun fork_syn (Element.Fixes xs) = |
601 fun fork_syn (Element.Fixes xs) = |
549 fold_map (fn (c, ty, syn) => cons (Binding.base_name c, syn) #> pair (c, ty, NoSyn)) xs |
602 fold_map (fn (c, ty, syn) => cons (Binding.base_name c, syn) #> pair (c, ty, NoSyn)) xs |
550 #>> Element.Fixes |
603 #>> Element.Fixes |