haftmann@18168
|
1 |
(* Title: Pure/Tools/class_package.ML
|
haftmann@18168
|
2 |
ID: $Id$
|
haftmann@18168
|
3 |
Author: Florian Haftmann, TU Muenchen
|
haftmann@18168
|
4 |
|
haftmann@18755
|
5 |
Type classes, simulated by locales.
|
haftmann@18168
|
6 |
*)
|
haftmann@18168
|
7 |
|
haftmann@18168
|
8 |
signature CLASS_PACKAGE =
|
haftmann@18168
|
9 |
sig
|
haftmann@19150
|
10 |
val class: bstring -> class list -> Element.context list -> theory
|
haftmann@18515
|
11 |
-> ProofContext.context * theory
|
haftmann@19150
|
12 |
val class_i: bstring -> class list -> Element.context_i list -> theory
|
haftmann@18515
|
13 |
-> ProofContext.context * theory
|
haftmann@19150
|
14 |
val instance_arity: (xstring * string list) * string
|
haftmann@19136
|
15 |
-> bstring * Attrib.src list -> ((bstring * Attrib.src list) * string) list
|
haftmann@18575
|
16 |
-> theory -> Proof.state
|
haftmann@19150
|
17 |
val instance_arity_i: (string * sort list) * sort
|
haftmann@19136
|
18 |
-> bstring * attribute list -> ((bstring * attribute list) * term) list
|
haftmann@18575
|
19 |
-> theory -> Proof.state
|
haftmann@19150
|
20 |
val prove_instance_arity: tactic -> (string * sort list) * sort
|
haftmann@19136
|
21 |
-> bstring * attribute list -> ((bstring * attribute list) * term) list
|
haftmann@19110
|
22 |
-> theory -> theory
|
haftmann@19150
|
23 |
val instance_sort: string * string -> theory -> Proof.state
|
haftmann@19150
|
24 |
val instance_sort_i: class * sort -> theory -> Proof.state
|
haftmann@19150
|
25 |
val prove_instance_sort: tactic -> class * sort -> theory -> theory
|
haftmann@18168
|
26 |
|
haftmann@19253
|
27 |
val use_cp_instance: bool ref;
|
haftmann@19253
|
28 |
|
haftmann@19110
|
29 |
val intern_class: theory -> xstring -> class
|
haftmann@19110
|
30 |
val intern_sort: theory -> sort -> sort
|
haftmann@19110
|
31 |
val extern_class: theory -> class -> xstring
|
haftmann@19110
|
32 |
val extern_sort: theory -> sort -> sort
|
haftmann@18755
|
33 |
val certify_class: theory -> class -> class
|
haftmann@19110
|
34 |
val certify_sort: theory -> sort -> sort
|
haftmann@19110
|
35 |
val read_sort: theory -> string -> sort
|
haftmann@18884
|
36 |
val operational_sort_of: theory -> sort -> sort
|
haftmann@18702
|
37 |
val the_superclasses: theory -> class -> class list
|
haftmann@18702
|
38 |
val the_consts_sign: theory -> class -> string * (string * typ) list
|
haftmann@18168
|
39 |
val lookup_const_class: theory -> string -> class option
|
haftmann@19213
|
40 |
val the_instances: theory -> class -> (string * ((sort list) * string)) list
|
haftmann@18702
|
41 |
val the_inst_sign: theory -> class * string -> (string * sort) list * (string * typ) list
|
haftmann@19213
|
42 |
val get_classtab: theory -> (string * string) list Symtab.table
|
haftmann@19110
|
43 |
|
haftmann@18702
|
44 |
val print_classes: theory -> unit
|
haftmann@19110
|
45 |
val intro_classes_tac: thm list -> tactic
|
haftmann@19110
|
46 |
val default_intro_classes_tac: thm list -> tactic
|
haftmann@18168
|
47 |
|
haftmann@18168
|
48 |
type sortcontext = (string * sort) list
|
haftmann@18884
|
49 |
datatype classlookup = Instance of (class * string) * classlookup list list
|
haftmann@19253
|
50 |
| Lookup of class list * (string * (int * int))
|
haftmann@18168
|
51 |
val extract_sortctxt: theory -> typ -> sortcontext
|
haftmann@18884
|
52 |
val extract_classlookup: theory -> string * typ -> classlookup list list
|
haftmann@18884
|
53 |
val extract_classlookup_inst: theory -> class * string -> class -> classlookup list list
|
haftmann@19253
|
54 |
val extract_classlookup_member: theory -> typ * typ -> classlookup list list
|
haftmann@18168
|
55 |
end;
|
haftmann@18168
|
56 |
|
haftmann@18168
|
57 |
structure ClassPackage: CLASS_PACKAGE =
|
haftmann@18168
|
58 |
struct
|
haftmann@18168
|
59 |
|
haftmann@18168
|
60 |
|
wenzelm@18708
|
61 |
(* theory data *)
|
haftmann@18168
|
62 |
|
haftmann@19456
|
63 |
datatype class_data = ClassData of {
|
haftmann@18575
|
64 |
name_locale: string,
|
haftmann@18575
|
65 |
name_axclass: string,
|
haftmann@19110
|
66 |
intro: thm option,
|
haftmann@18575
|
67 |
var: string,
|
haftmann@19280
|
68 |
consts: (string * (string * typ)) list
|
haftmann@19280
|
69 |
(*locale parameter ~> toplevel const*)
|
haftmann@18168
|
70 |
};
|
haftmann@18168
|
71 |
|
haftmann@19456
|
72 |
fun rep_classdata (ClassData c) = c;
|
haftmann@19456
|
73 |
fun eq_classdata (ClassData {
|
haftmann@19456
|
74 |
name_locale = name_locale1, name_axclass = name_axclass1, intro = intro1,
|
haftmann@19456
|
75 |
var = var1, consts = consts1}, ClassData {
|
haftmann@19456
|
76 |
name_locale = name_locale2, name_axclass = name_axclass2, intro = intro2,
|
haftmann@19456
|
77 |
var = var2, consts = consts2}) =
|
haftmann@19456
|
78 |
name_locale1 = name_locale2 andalso name_axclass1 = name_axclass2
|
haftmann@19456
|
79 |
andalso eq_opt eq_thm (intro1, intro2) andalso var1 = var2
|
haftmann@19456
|
80 |
andalso eq_list (eq_pair (op =) (eq_pair (op =) (Type.eq_type Vartab.empty)))
|
haftmann@19456
|
81 |
(consts1, consts2);
|
haftmann@19456
|
82 |
|
haftmann@18575
|
83 |
structure ClassData = TheoryDataFun (
|
haftmann@18168
|
84 |
struct
|
haftmann@18168
|
85 |
val name = "Pure/classes";
|
haftmann@19213
|
86 |
type T = (class_data Graph.T
|
haftmann@19213
|
87 |
* (string * (sort list * string)) list Symtab.table)
|
haftmann@19456
|
88 |
(*class ~> tyco ~> (arity, thyname)*)
|
haftmann@19213
|
89 |
* class Symtab.table;
|
haftmann@19213
|
90 |
val empty = ((Graph.empty, Symtab.empty), Symtab.empty);
|
haftmann@18168
|
91 |
val copy = I;
|
haftmann@18168
|
92 |
val extend = I;
|
haftmann@19456
|
93 |
fun merge _ (((g1, c1), f1) : T, ((g2, c2), f2)) =
|
haftmann@19456
|
94 |
((Graph.merge eq_classdata (g1, g2), Symtab.join (fn _ => AList.merge (op =) (op =)) (c1, c2)),
|
haftmann@19213
|
95 |
Symtab.merge (op =) (f1, f2));
|
haftmann@19213
|
96 |
fun print thy ((gr, _), _) =
|
haftmann@18575
|
97 |
let
|
haftmann@19456
|
98 |
fun pretty_class gr (name, ClassData {name_locale, name_axclass, intro, var, consts}) =
|
haftmann@18575
|
99 |
(Pretty.block o Pretty.fbreaks) [
|
haftmann@18575
|
100 |
Pretty.str ("class " ^ name ^ ":"),
|
haftmann@18575
|
101 |
(Pretty.block o Pretty.fbreaks) (
|
haftmann@18575
|
102 |
Pretty.str "superclasses: "
|
haftmann@19110
|
103 |
:: (map Pretty.str o Graph.imm_succs gr) name
|
haftmann@18575
|
104 |
),
|
haftmann@18575
|
105 |
Pretty.str ("locale: " ^ name_locale),
|
haftmann@18575
|
106 |
Pretty.str ("axclass: " ^ name_axclass),
|
haftmann@18575
|
107 |
Pretty.str ("class variable: " ^ var),
|
haftmann@18575
|
108 |
(Pretty.block o Pretty.fbreaks) (
|
haftmann@18575
|
109 |
Pretty.str "constants: "
|
haftmann@19280
|
110 |
:: map (fn (_, (c, ty)) => Pretty.str (c ^ " :: " ^ Sign.string_of_typ thy ty)) consts
|
haftmann@18575
|
111 |
)
|
haftmann@18575
|
112 |
]
|
haftmann@18575
|
113 |
in
|
haftmann@19110
|
114 |
(Pretty.writeln o Pretty.chunks o map (pretty_class gr)
|
haftmann@19110
|
115 |
o AList.make (Graph.get_node gr) o Library.flat o Graph.strong_conn) gr
|
haftmann@18575
|
116 |
end;
|
haftmann@18168
|
117 |
end
|
haftmann@18168
|
118 |
);
|
haftmann@18168
|
119 |
|
wenzelm@18708
|
120 |
val _ = Context.add_setup ClassData.init;
|
haftmann@18575
|
121 |
val print_classes = ClassData.print;
|
haftmann@18575
|
122 |
|
haftmann@19038
|
123 |
|
haftmann@19038
|
124 |
(* queries *)
|
haftmann@19038
|
125 |
|
haftmann@19456
|
126 |
val lookup_class_data = Option.map rep_classdata oo try o Graph.get_node o fst o fst o ClassData.get;
|
haftmann@19213
|
127 |
val the_instances = these oo Symtab.lookup o snd o fst o ClassData.get;
|
haftmann@19213
|
128 |
val lookup_const_class = Symtab.lookup o snd o ClassData.get;
|
haftmann@18168
|
129 |
|
haftmann@19038
|
130 |
fun the_class_data thy class =
|
haftmann@18168
|
131 |
case lookup_class_data thy class
|
haftmann@18755
|
132 |
of NONE => error ("undeclared operational class " ^ quote class)
|
haftmann@18168
|
133 |
| SOME data => data;
|
haftmann@18168
|
134 |
|
haftmann@19280
|
135 |
val is_class = is_some oo lookup_class_data;
|
haftmann@19280
|
136 |
|
haftmann@19280
|
137 |
fun is_operational_class thy cls =
|
haftmann@18702
|
138 |
lookup_class_data thy cls
|
haftmann@18702
|
139 |
|> Option.map (not o null o #consts)
|
haftmann@18702
|
140 |
|> the_default false;
|
haftmann@18168
|
141 |
|
haftmann@18884
|
142 |
fun operational_sort_of thy sort =
|
haftmann@18360
|
143 |
let
|
haftmann@19110
|
144 |
fun get_sort class =
|
haftmann@19280
|
145 |
if is_operational_class thy class
|
haftmann@19110
|
146 |
then [class]
|
wenzelm@19412
|
147 |
else operational_sort_of thy (Sign.super_classes thy class);
|
haftmann@18360
|
148 |
in
|
haftmann@18360
|
149 |
map get_sort sort
|
haftmann@18360
|
150 |
|> Library.flat
|
wenzelm@19412
|
151 |
|> Sign.certify_sort thy
|
haftmann@18360
|
152 |
end;
|
haftmann@18168
|
153 |
|
haftmann@18702
|
154 |
fun the_superclasses thy class =
|
haftmann@18515
|
155 |
if is_class thy class
|
haftmann@18515
|
156 |
then
|
wenzelm@19412
|
157 |
Sign.super_classes thy class
|
haftmann@18884
|
158 |
|> operational_sort_of thy
|
haftmann@18515
|
159 |
else
|
haftmann@19280
|
160 |
error ("no class: " ^ class);
|
haftmann@18168
|
161 |
|
haftmann@19110
|
162 |
fun get_superclass_derivation thy (subclass, superclass) =
|
haftmann@19110
|
163 |
if subclass = superclass
|
haftmann@19110
|
164 |
then SOME [subclass]
|
haftmann@19213
|
165 |
else case Graph.find_paths ((fst o fst o ClassData.get) thy) (subclass, superclass)
|
haftmann@19110
|
166 |
of [] => NONE
|
haftmann@19280
|
167 |
| (p::_) => (SOME o filter (is_operational_class thy)) p;
|
haftmann@19110
|
168 |
|
haftmann@19038
|
169 |
fun the_ancestry thy classes =
|
haftmann@19038
|
170 |
let
|
haftmann@19038
|
171 |
fun ancestry class anc =
|
haftmann@19038
|
172 |
anc
|
haftmann@19038
|
173 |
|> cons class
|
haftmann@19038
|
174 |
|> fold ancestry (the_superclasses thy class);
|
haftmann@19038
|
175 |
in fold ancestry classes [] end;
|
haftmann@19038
|
176 |
|
haftmann@19110
|
177 |
fun the_intros thy =
|
haftmann@19110
|
178 |
let
|
haftmann@19213
|
179 |
val gr = (fst o fst o ClassData.get) thy;
|
haftmann@19456
|
180 |
in (List.mapPartial (#intro o rep_classdata o Graph.get_node gr) o Graph.keys) gr end;
|
haftmann@19110
|
181 |
|
haftmann@19038
|
182 |
fun subst_clsvar v ty_subst =
|
haftmann@19038
|
183 |
map_type_tfree (fn u as (w, _) =>
|
haftmann@19038
|
184 |
if w = v then ty_subst else TFree u);
|
haftmann@19038
|
185 |
|
haftmann@19280
|
186 |
fun the_parm_map thy class =
|
haftmann@19280
|
187 |
let
|
haftmann@19280
|
188 |
val data = the_class_data thy class
|
haftmann@19280
|
189 |
in (#consts data) end;
|
haftmann@19280
|
190 |
|
haftmann@18702
|
191 |
fun the_consts_sign thy class =
|
haftmann@18702
|
192 |
let
|
haftmann@19038
|
193 |
val data = the_class_data thy class
|
haftmann@19280
|
194 |
in (#var data, (map snd o #consts) data) end;
|
haftmann@18168
|
195 |
|
wenzelm@19292
|
196 |
fun mg_domain thy tyco class =
|
wenzelm@19292
|
197 |
Sorts.mg_domain (Sign.classes_of thy, Sign.arities_of thy) tyco [class];
|
wenzelm@19292
|
198 |
|
haftmann@18702
|
199 |
fun the_inst_sign thy (class, tyco) =
|
haftmann@18168
|
200 |
let
|
haftmann@19280
|
201 |
val _ = if is_operational_class thy class then () else error ("no operational class: " ^ class);
|
wenzelm@19292
|
202 |
val arity = mg_domain thy tyco class;
|
haftmann@19038
|
203 |
val clsvar = (#var o the_class_data thy) class;
|
haftmann@18702
|
204 |
val const_sign = (snd o the_consts_sign thy) class;
|
haftmann@18702
|
205 |
fun add_var sort used =
|
haftmann@18702
|
206 |
let
|
haftmann@18702
|
207 |
val v = hd (Term.invent_names used "'a" 1)
|
haftmann@18702
|
208 |
in ((v, sort), v::used) end;
|
haftmann@18702
|
209 |
val (vsorts, _) =
|
haftmann@19213
|
210 |
[clsvar]
|
haftmann@18702
|
211 |
|> fold (fn (_, ty) => curry (gen_union (op =))
|
haftmann@18702
|
212 |
((map (fst o fst) o typ_tvars) ty @ (map fst o typ_tfrees) ty)) const_sign
|
haftmann@18702
|
213 |
|> fold_map add_var arity;
|
haftmann@18702
|
214 |
val ty_inst = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vsorts);
|
haftmann@18702
|
215 |
val inst_signs = map (apsnd (subst_clsvar clsvar ty_inst)) const_sign;
|
haftmann@18702
|
216 |
in (vsorts, inst_signs) end;
|
haftmann@18168
|
217 |
|
haftmann@18168
|
218 |
fun get_classtab thy =
|
haftmann@19213
|
219 |
(Symtab.map o map)
|
haftmann@19213
|
220 |
(fn (tyco, (_, thyname)) => (tyco, thyname)) ((snd o fst o ClassData.get) thy);
|
haftmann@18168
|
221 |
|
haftmann@18168
|
222 |
|
haftmann@19038
|
223 |
(* updaters *)
|
haftmann@19038
|
224 |
|
haftmann@19110
|
225 |
fun add_class_data (class, (superclasses, name_locale, name_axclass, intro, var, consts)) =
|
haftmann@19213
|
226 |
ClassData.map (fn ((gr, tab), consttab) => ((
|
haftmann@19213
|
227 |
gr
|
haftmann@19456
|
228 |
|> Graph.new_node (class, ClassData {
|
haftmann@19038
|
229 |
name_locale = name_locale,
|
haftmann@19038
|
230 |
name_axclass = name_axclass,
|
haftmann@19110
|
231 |
intro = intro,
|
haftmann@19110
|
232 |
var = var,
|
haftmann@19213
|
233 |
consts = consts
|
haftmann@19110
|
234 |
})
|
haftmann@19110
|
235 |
|> fold (curry Graph.add_edge_acyclic class) superclasses,
|
haftmann@19213
|
236 |
tab
|
haftmann@19213
|
237 |
|> Symtab.update (class, [])),
|
haftmann@19213
|
238 |
consttab
|
haftmann@19280
|
239 |
|> fold (fn (_, (c, _)) => Symtab.update (c, class)) consts
|
haftmann@19038
|
240 |
));
|
haftmann@19038
|
241 |
|
haftmann@19038
|
242 |
fun add_inst_data (class, inst) =
|
haftmann@19213
|
243 |
ClassData.map (fn ((gr, tab), consttab) =>
|
haftmann@19280
|
244 |
let
|
haftmann@19280
|
245 |
val undef_supclasses = class :: (filter (Symtab.defined tab) (Graph.all_succs gr [class]));
|
haftmann@19280
|
246 |
in
|
haftmann@19280
|
247 |
((gr, tab |> fold (fn class => Symtab.map_entry class (AList.update (op =) inst)) undef_supclasses), consttab)
|
haftmann@19280
|
248 |
end);
|
haftmann@19038
|
249 |
|
haftmann@19038
|
250 |
|
haftmann@19038
|
251 |
(* name handling *)
|
haftmann@19038
|
252 |
|
haftmann@19038
|
253 |
fun certify_class thy class =
|
haftmann@19110
|
254 |
(fn class => (the_class_data thy class; class)) (Sign.certify_class thy class);
|
haftmann@19038
|
255 |
|
haftmann@19110
|
256 |
fun certify_sort thy sort =
|
haftmann@19110
|
257 |
map (fn class => (the_class_data thy class; class)) (Sign.certify_sort thy sort);
|
haftmann@19038
|
258 |
|
haftmann@19110
|
259 |
fun intern_class thy =
|
haftmann@19280
|
260 |
certify_class thy o Sign.intern_class thy;
|
haftmann@19110
|
261 |
|
haftmann@19110
|
262 |
fun intern_sort thy =
|
haftmann@19110
|
263 |
certify_sort thy o Sign.intern_sort thy;
|
haftmann@19110
|
264 |
|
haftmann@19110
|
265 |
fun extern_class thy =
|
haftmann@19110
|
266 |
Sign.extern_class thy o certify_class thy;
|
haftmann@19110
|
267 |
|
haftmann@19110
|
268 |
fun extern_sort thy =
|
haftmann@19110
|
269 |
Sign.extern_sort thy o certify_sort thy;
|
haftmann@19110
|
270 |
|
haftmann@19110
|
271 |
fun read_sort thy =
|
haftmann@19110
|
272 |
certify_sort thy o Sign.read_sort thy;
|
haftmann@19110
|
273 |
|
haftmann@19110
|
274 |
|
haftmann@19110
|
275 |
(* tactics and methods *)
|
haftmann@19110
|
276 |
|
wenzelm@19123
|
277 |
fun class_intros thy =
|
wenzelm@19123
|
278 |
AxClass.class_intros thy @ the_intros thy;
|
haftmann@19110
|
279 |
|
haftmann@19110
|
280 |
fun intro_classes_tac facts st =
|
haftmann@19110
|
281 |
(ALLGOALS (Method.insert_tac facts THEN'
|
wenzelm@19123
|
282 |
REPEAT_ALL_NEW (resolve_tac (class_intros (Thm.theory_of_thm st))))
|
haftmann@19110
|
283 |
THEN Tactic.distinct_subgoals_tac) st;
|
haftmann@19110
|
284 |
|
haftmann@19110
|
285 |
fun default_intro_classes_tac [] = intro_classes_tac []
|
haftmann@19110
|
286 |
| default_intro_classes_tac _ = Tactical.no_tac; (*no error message!*)
|
haftmann@19110
|
287 |
|
haftmann@19110
|
288 |
fun default_tac rules ctxt facts =
|
haftmann@19110
|
289 |
HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
|
haftmann@19110
|
290 |
default_intro_classes_tac facts;
|
haftmann@19038
|
291 |
|
haftmann@19038
|
292 |
|
wenzelm@19246
|
293 |
(* axclass instances *)
|
wenzelm@19246
|
294 |
|
wenzelm@19246
|
295 |
local
|
wenzelm@19246
|
296 |
|
wenzelm@19412
|
297 |
fun gen_instance mk_prop add_thm after_qed inst thy =
|
wenzelm@19246
|
298 |
thy
|
wenzelm@19246
|
299 |
|> ProofContext.init
|
wenzelm@19412
|
300 |
|> Proof.theorem_i PureThy.internalK NONE (after_qed oo (fold o fold) add_thm) NONE ("", [])
|
wenzelm@19246
|
301 |
(map (fn t => (("", []), [(t, ([], []))])) (mk_prop thy inst));
|
wenzelm@19246
|
302 |
|
wenzelm@19246
|
303 |
in
|
wenzelm@19246
|
304 |
|
wenzelm@19246
|
305 |
val axclass_instance_subclass =
|
wenzelm@19412
|
306 |
gen_instance (single oo (Logic.mk_classrel oo AxClass.read_classrel)) AxClass.add_classrel I;
|
wenzelm@19246
|
307 |
val axclass_instance_arity =
|
wenzelm@19412
|
308 |
gen_instance (Logic.mk_arities oo Sign.read_arity) AxClass.add_arity;
|
wenzelm@19246
|
309 |
val axclass_instance_arity_i =
|
wenzelm@19412
|
310 |
gen_instance (Logic.mk_arities oo Sign.cert_arity) AxClass.add_arity;
|
wenzelm@19246
|
311 |
|
wenzelm@19246
|
312 |
end;
|
wenzelm@19246
|
313 |
|
wenzelm@19246
|
314 |
|
haftmann@19038
|
315 |
(* classes and instances *)
|
haftmann@19038
|
316 |
|
haftmann@19038
|
317 |
local
|
haftmann@19038
|
318 |
|
haftmann@19110
|
319 |
fun intro_incr thy name expr =
|
haftmann@19110
|
320 |
let
|
haftmann@19110
|
321 |
fun fish_thm basename =
|
haftmann@19110
|
322 |
try (PureThy.get_thm thy) ((Name o NameSpace.append basename) "intro");
|
haftmann@19110
|
323 |
in if expr = Locale.empty
|
haftmann@19110
|
324 |
then fish_thm name
|
haftmann@19110
|
325 |
else fish_thm (name ^ "_axioms")
|
haftmann@19110
|
326 |
end;
|
haftmann@19038
|
327 |
|
haftmann@19110
|
328 |
fun add_locale opn name expr body thy =
|
haftmann@19110
|
329 |
thy
|
haftmann@19110
|
330 |
|> Locale.add_locale opn name expr body
|
haftmann@19110
|
331 |
||>> `(fn thy => intro_incr thy name expr)
|
haftmann@19340
|
332 |
|-> (fn ((name, ctxt), intro) => pair ((name, intro), ctxt));
|
haftmann@19110
|
333 |
|
haftmann@19110
|
334 |
fun add_locale_i opn name expr body thy =
|
haftmann@19110
|
335 |
thy
|
haftmann@19110
|
336 |
|> Locale.add_locale_i opn name expr body
|
haftmann@19110
|
337 |
||>> `(fn thy => intro_incr thy name expr)
|
haftmann@19340
|
338 |
|-> (fn ((name, ctxt), intro) => pair ((name, intro), ctxt));
|
haftmann@19110
|
339 |
|
haftmann@19110
|
340 |
fun add_axclass_i (name, supsort) axs thy =
|
haftmann@19038
|
341 |
let
|
wenzelm@19395
|
342 |
val (c, thy') = thy
|
wenzelm@19434
|
343 |
|> AxClass.add_axclass_i (name, supsort) [] axs;
|
wenzelm@19395
|
344 |
val {intro, axioms, ...} = AxClass.get_info thy' c;
|
wenzelm@19395
|
345 |
in ((c, (intro, axioms)), thy') end;
|
haftmann@19110
|
346 |
|
haftmann@19110
|
347 |
fun prove_interpretation_i (prfx, atts) expr insts tac thy =
|
haftmann@19110
|
348 |
let
|
haftmann@19110
|
349 |
fun ad_hoc_term NONE = NONE
|
haftmann@19110
|
350 |
| ad_hoc_term (SOME (Const (c, ty))) =
|
haftmann@19110
|
351 |
let
|
haftmann@19110
|
352 |
val p = setmp show_types true (setmp show_sorts true (setmp print_mode [] (Sign.pretty_typ thy))) ty;
|
haftmann@19110
|
353 |
val s = c ^ "::" ^ Pretty.output p;
|
haftmann@19110
|
354 |
val _ = writeln s;
|
haftmann@19110
|
355 |
in SOME s end
|
haftmann@19110
|
356 |
| ad_hoc_term (SOME t) =
|
haftmann@19110
|
357 |
let
|
haftmann@19110
|
358 |
val p = setmp show_types true (setmp show_sorts true (setmp print_mode [] (Sign.pretty_term thy))) t;
|
haftmann@19110
|
359 |
val s = Pretty.output p;
|
haftmann@19110
|
360 |
val _ = writeln s;
|
haftmann@19110
|
361 |
in SOME s end;
|
haftmann@19110
|
362 |
in
|
haftmann@19110
|
363 |
thy
|
haftmann@19110
|
364 |
|> Locale.interpretation (prfx, atts) expr (map ad_hoc_term insts)
|
haftmann@19110
|
365 |
|> Proof.global_terminal_proof (Method.Basic (fn _ => Method.SIMPLE_METHOD tac), NONE)
|
haftmann@19110
|
366 |
|-> (fn _ => I)
|
haftmann@19110
|
367 |
end;
|
haftmann@19110
|
368 |
|
haftmann@19150
|
369 |
fun gen_class add_locale prep_class bname raw_supclasses raw_elems thy =
|
haftmann@19110
|
370 |
let
|
haftmann@19110
|
371 |
val supclasses = map (prep_class thy) raw_supclasses;
|
haftmann@19038
|
372 |
val supsort =
|
haftmann@19038
|
373 |
supclasses
|
haftmann@19038
|
374 |
|> map (#name_axclass o the_class_data thy)
|
haftmann@19038
|
375 |
|> Sorts.certify_sort (Sign.classes_of thy)
|
haftmann@19038
|
376 |
|> null ? K (Sign.defaultS thy);
|
haftmann@19110
|
377 |
val expr = if null supclasses
|
haftmann@19110
|
378 |
then Locale.empty
|
haftmann@19110
|
379 |
else
|
haftmann@19110
|
380 |
(Locale.Merge o map (Locale.Locale o #name_locale o the_class_data thy)) supclasses;
|
haftmann@19280
|
381 |
val mapp_sup = AList.make
|
haftmann@19280
|
382 |
(the o AList.lookup (op =) ((Library.flat o map (the_parm_map thy) o the_ancestry thy) supclasses))
|
haftmann@19280
|
383 |
((map (fst o fst) o Locale.parameters_of_expr thy) expr);
|
haftmann@19038
|
384 |
fun extract_tyvar_consts thy name_locale =
|
haftmann@19038
|
385 |
let
|
haftmann@19038
|
386 |
fun extract_tyvar_name thy tys =
|
haftmann@19038
|
387 |
fold (curry add_typ_tfrees) tys []
|
haftmann@19038
|
388 |
|> (fn [(v, sort)] =>
|
haftmann@19280
|
389 |
if Sorts.sort_le (Sign.classes_of thy) (swap (sort, supsort))
|
haftmann@19038
|
390 |
then v
|
haftmann@19038
|
391 |
else error ("illegal sort constraint on class type variable: " ^ Sign.string_of_sort thy sort)
|
haftmann@19038
|
392 |
| [] => error ("no class type variable")
|
haftmann@19038
|
393 |
| vs => error ("more than one type variable: " ^ (commas o map (Sign.string_of_typ thy o TFree)) vs))
|
haftmann@19110
|
394 |
val consts1 =
|
haftmann@19038
|
395 |
Locale.parameters_of thy name_locale
|
haftmann@19038
|
396 |
|> map (apsnd Syntax.unlocalize_mixfix)
|
haftmann@19110
|
397 |
val v = (extract_tyvar_name thy o map (snd o fst)) consts1;
|
haftmann@19110
|
398 |
val consts2 = map ((apfst o apsnd) (subst_clsvar v (TFree (v, [])))) consts1;
|
haftmann@19280
|
399 |
in (v, chop (length mapp_sup) consts2) end;
|
haftmann@19110
|
400 |
fun add_consts v raw_cs_sup raw_cs_this thy =
|
haftmann@19110
|
401 |
let
|
haftmann@19110
|
402 |
fun add_global_const ((c, ty), syn) thy =
|
haftmann@19110
|
403 |
thy
|
haftmann@19110
|
404 |
|> Sign.add_consts_i [(c, ty |> subst_clsvar v (TFree (v, Sign.defaultS thy)), syn)]
|
haftmann@19110
|
405 |
|> `(fn thy => (c, (Sign.intern_const thy c, ty)))
|
haftmann@19110
|
406 |
in
|
haftmann@19110
|
407 |
thy
|
haftmann@19110
|
408 |
|> fold_map add_global_const raw_cs_this
|
haftmann@19110
|
409 |
end;
|
haftmann@19110
|
410 |
fun extract_assumes thy name_locale cs_mapp =
|
haftmann@19110
|
411 |
let
|
haftmann@19110
|
412 |
val subst_assume =
|
haftmann@19110
|
413 |
map_aterms (fn Free (c, ty) => Const ((fst o the o AList.lookup (op =) cs_mapp) c, ty)
|
haftmann@19110
|
414 |
| t => t)
|
haftmann@19110
|
415 |
fun prep_asm ((name, atts), ts) =
|
haftmann@19110
|
416 |
((name, map (Attrib.attribute thy) atts), map subst_assume ts)
|
haftmann@19110
|
417 |
in
|
haftmann@19110
|
418 |
(map prep_asm o Locale.local_asms_of thy) name_locale
|
haftmann@19110
|
419 |
end;
|
haftmann@19280
|
420 |
fun add_global_constraint v class (_, (c, ty)) thy =
|
haftmann@19038
|
421 |
thy
|
haftmann@19136
|
422 |
|> Sign.add_const_constraint_i (c, SOME (subst_clsvar v (TFree (v, [class])) ty));
|
haftmann@19110
|
423 |
fun mk_const thy class v (c, ty) =
|
haftmann@19110
|
424 |
Const (c, subst_clsvar v (TFree (v, [class])) ty);
|
haftmann@19038
|
425 |
in
|
haftmann@19038
|
426 |
thy
|
haftmann@19110
|
427 |
|> add_locale bname expr raw_elems
|
haftmann@19110
|
428 |
|-> (fn ((name_locale, intro), ctxt) =>
|
haftmann@19038
|
429 |
`(fn thy => extract_tyvar_consts thy name_locale)
|
haftmann@19110
|
430 |
#-> (fn (v, (raw_cs_sup, raw_cs_this)) =>
|
haftmann@19110
|
431 |
add_consts v raw_cs_sup raw_cs_this
|
haftmann@19280
|
432 |
#-> (fn mapp_this =>
|
haftmann@19280
|
433 |
`(fn thy => extract_assumes thy name_locale (mapp_sup @ mapp_this))
|
haftmann@19110
|
434 |
#-> (fn loc_axioms =>
|
wenzelm@19434
|
435 |
add_axclass_i (bname, supsort) (map (apfst (apfst (K ""))) loc_axioms)
|
haftmann@19110
|
436 |
#-> (fn (name_axclass, (_, ax_axioms)) =>
|
haftmann@19280
|
437 |
fold (add_global_constraint v name_axclass) mapp_this
|
haftmann@19280
|
438 |
#> add_class_data (name_locale, (supclasses, name_locale, name_axclass, intro, v, mapp_this))
|
haftmann@19110
|
439 |
#> prove_interpretation_i (NameSpace.base name_locale, [])
|
haftmann@19280
|
440 |
(Locale.Locale name_locale) (map (SOME o mk_const thy name_axclass v) (map snd (mapp_sup @ mapp_this)))
|
haftmann@19110
|
441 |
((ALLGOALS o resolve_tac) ax_axioms)
|
haftmann@19110
|
442 |
#> pair ctxt
|
haftmann@19110
|
443 |
)))))
|
haftmann@19038
|
444 |
end;
|
haftmann@19038
|
445 |
|
haftmann@19038
|
446 |
in
|
haftmann@19038
|
447 |
|
haftmann@19150
|
448 |
val class = gen_class (add_locale true) intern_class;
|
haftmann@19150
|
449 |
val class_i = gen_class (add_locale_i true) certify_class;
|
haftmann@19038
|
450 |
|
haftmann@19038
|
451 |
end; (* local *)
|
haftmann@19038
|
452 |
|
haftmann@19110
|
453 |
local
|
haftmann@19110
|
454 |
|
haftmann@19110
|
455 |
fun gen_add_defs_overloaded prep_att tap_def add_defs tyco raw_defs thy =
|
haftmann@19038
|
456 |
let
|
haftmann@19110
|
457 |
fun invent_name raw_t =
|
haftmann@19110
|
458 |
let
|
haftmann@19110
|
459 |
val t = tap_def thy raw_t;
|
haftmann@19110
|
460 |
val c = (fst o dest_Const o fst o strip_comb o fst o Logic.dest_equals) t;
|
haftmann@19110
|
461 |
in
|
haftmann@19110
|
462 |
Thm.def_name (NameSpace.base c ^ "_" ^ NameSpace.base tyco)
|
haftmann@19110
|
463 |
end;
|
haftmann@19110
|
464 |
fun prep_def (_, (("", a), t)) =
|
haftmann@19110
|
465 |
let
|
haftmann@19110
|
466 |
val n = invent_name t
|
haftmann@19110
|
467 |
in ((n, t), map (prep_att thy) a) end
|
haftmann@19110
|
468 |
| prep_def (_, ((n, a), t)) =
|
haftmann@19110
|
469 |
((n, t), map (prep_att thy) a);
|
haftmann@19110
|
470 |
in
|
haftmann@19110
|
471 |
thy
|
haftmann@19110
|
472 |
|> add_defs true (map prep_def raw_defs)
|
haftmann@19110
|
473 |
end;
|
haftmann@19110
|
474 |
|
haftmann@19110
|
475 |
val add_defs_overloaded = gen_add_defs_overloaded Attrib.attribute Sign.read_term PureThy.add_defs;
|
haftmann@19110
|
476 |
val add_defs_overloaded_i = gen_add_defs_overloaded (K I) (K I) PureThy.add_defs_i;
|
haftmann@19110
|
477 |
|
haftmann@19136
|
478 |
fun gen_instance_arity prep_arity prep_att add_defs tap_def do_proof raw_arity (raw_name, raw_atts) raw_defs theory =
|
haftmann@19110
|
479 |
let
|
haftmann@19110
|
480 |
val pp = Sign.pp theory;
|
haftmann@19110
|
481 |
val arity as (tyco, asorts, sort) = prep_arity theory ((fn ((x, y), z) => (x, y, z)) raw_arity);
|
haftmann@19038
|
482 |
val ty_inst = Type (tyco, map2 (curry TVar o rpair 0) (Term.invent_names [] "'a" (length asorts)) asorts)
|
haftmann@19136
|
483 |
val name = case raw_name
|
haftmann@19136
|
484 |
of "" => Thm.def_name ((space_implode "_" o map NameSpace.base) sort ^ "_" ^ NameSpace.base tyco)
|
haftmann@19136
|
485 |
| _ => raw_name;
|
haftmann@19136
|
486 |
val atts = map (prep_att theory) raw_atts;
|
haftmann@19110
|
487 |
fun get_classes thy tyco sort =
|
haftmann@19038
|
488 |
let
|
haftmann@19110
|
489 |
fun get class classes =
|
haftmann@19213
|
490 |
if AList.defined (op =) ((the_instances thy) class) tyco
|
haftmann@19110
|
491 |
then classes
|
haftmann@19110
|
492 |
else classes
|
haftmann@19110
|
493 |
|> cons class
|
haftmann@19110
|
494 |
|> fold get (the_superclasses thy class)
|
haftmann@19110
|
495 |
in fold get sort [] end;
|
haftmann@19110
|
496 |
val classes = get_classes theory tyco sort;
|
haftmann@19110
|
497 |
val _ = if null classes then error ("already instantiated") else ();
|
haftmann@19110
|
498 |
fun get_consts class =
|
haftmann@19110
|
499 |
let
|
haftmann@19110
|
500 |
val data = the_class_data theory class;
|
haftmann@19038
|
501 |
val subst_ty = map_type_tfree (fn (var as (v, _)) =>
|
haftmann@19038
|
502 |
if #var data = v then ty_inst else TFree var)
|
haftmann@19280
|
503 |
in (map (apsnd subst_ty o snd) o #consts) data end;
|
haftmann@19110
|
504 |
val cs = (Library.flat o map get_consts) classes;
|
haftmann@19110
|
505 |
fun get_remove_contraint c thy =
|
haftmann@19110
|
506 |
let
|
haftmann@19110
|
507 |
val ty = Sign.the_const_constraint thy c;
|
haftmann@19110
|
508 |
in
|
haftmann@19110
|
509 |
thy
|
haftmann@19110
|
510 |
|> Sign.add_const_constraint_i (c, NONE)
|
haftmann@19136
|
511 |
|> pair (c, Type.unvarifyT ty)
|
haftmann@19110
|
512 |
end;
|
haftmann@19253
|
513 |
fun check_defs0 thy raw_defs c_req =
|
haftmann@19038
|
514 |
let
|
haftmann@19038
|
515 |
fun get_c raw_def =
|
haftmann@19253
|
516 |
(fst o Sign.cert_def pp o tap_def thy o snd) raw_def;
|
haftmann@19038
|
517 |
val c_given = map get_c raw_defs;
|
haftmann@19340
|
518 |
fun eq_c ((c1 : string, ty1), (c2, ty2)) =
|
haftmann@19038
|
519 |
let
|
haftmann@19038
|
520 |
val ty1' = Type.varifyT ty1;
|
haftmann@19038
|
521 |
val ty2' = Type.varifyT ty2;
|
haftmann@19038
|
522 |
in
|
haftmann@19038
|
523 |
c1 = c2
|
haftmann@19253
|
524 |
andalso Sign.typ_instance thy (ty1', ty2')
|
haftmann@19253
|
525 |
andalso Sign.typ_instance thy (ty2', ty1')
|
haftmann@19038
|
526 |
end;
|
wenzelm@19300
|
527 |
val _ = case subtract eq_c c_req c_given
|
haftmann@19038
|
528 |
of [] => ()
|
haftmann@19038
|
529 |
| cs => error ("superfluous definition(s) given for "
|
haftmann@19253
|
530 |
^ (commas o map (fn (c, ty) => quote (c ^ "::" ^ Sign.string_of_typ thy ty))) cs);
|
haftmann@19340
|
531 |
(*val _ = case subtract eq_c c_given c_req
|
haftmann@19110
|
532 |
of [] => ()
|
haftmann@19038
|
533 |
| cs => error ("no definition(s) given for "
|
haftmann@19340
|
534 |
^ (commas o map (fn (c, ty) => quote (c ^ "::" ^ Sign.string_of_typ thy ty))) cs);*)
|
haftmann@19253
|
535 |
in () end;
|
haftmann@19253
|
536 |
fun check_defs1 raw_defs c_req thy =
|
haftmann@19253
|
537 |
let
|
haftmann@19253
|
538 |
val thy' = (Sign.add_arities_i [(tyco, asorts, sort)] o Theory.copy) thy
|
haftmann@19253
|
539 |
in (check_defs0 thy' raw_defs c_req; thy) end;
|
haftmann@19110
|
540 |
fun mangle_alldef_name tyco sort =
|
haftmann@19110
|
541 |
Thm.def_name ((space_implode "_" o map NameSpace.base) sort ^ "_" ^ NameSpace.base tyco);
|
haftmann@19110
|
542 |
fun note_all tyco sort thms thy =
|
haftmann@19110
|
543 |
thy
|
haftmann@19136
|
544 |
|> PureThy.note_thmss_i PureThy.internalK [((name, atts), [(thms, [])])]
|
haftmann@19110
|
545 |
|> snd;
|
haftmann@19110
|
546 |
fun after_qed cs thy =
|
haftmann@19110
|
547 |
thy
|
haftmann@19253
|
548 |
|> fold (fn class =>
|
haftmann@19253
|
549 |
add_inst_data (class, (tyco,
|
wenzelm@19412
|
550 |
(map (operational_sort_of thy) asorts, Context.theory_name thy)))) sort
|
wenzelm@19412
|
551 |
|> fold Sign.add_const_constraint_i (map (apsnd SOME) cs);
|
haftmann@19038
|
552 |
in
|
haftmann@19110
|
553 |
theory
|
haftmann@19253
|
554 |
|> check_defs1 raw_defs cs
|
haftmann@19110
|
555 |
|> fold_map get_remove_contraint (map fst cs)
|
haftmann@19110
|
556 |
||>> add_defs tyco (map (pair NONE) raw_defs)
|
haftmann@19110
|
557 |
|-> (fn (cs, defnames) => note_all tyco sort defnames #> pair cs)
|
haftmann@19110
|
558 |
|-> (fn cs => do_proof (after_qed cs) arity)
|
haftmann@19038
|
559 |
end;
|
haftmann@19038
|
560 |
|
wenzelm@19246
|
561 |
fun instance_arity' do_proof = gen_instance_arity Sign.read_arity Attrib.attribute add_defs_overloaded
|
haftmann@19110
|
562 |
(fn thy => fn t => (snd o read_axm thy) ("", t)) do_proof;
|
wenzelm@19246
|
563 |
fun instance_arity_i' do_proof = gen_instance_arity Sign.cert_arity (K I) add_defs_overloaded_i
|
haftmann@19110
|
564 |
(K I) do_proof;
|
wenzelm@19246
|
565 |
val setup_proof = axclass_instance_arity_i;
|
wenzelm@19246
|
566 |
fun tactic_proof tac after_qed arity = AxClass.prove_arity arity tac #> after_qed;
|
haftmann@19038
|
567 |
|
haftmann@19110
|
568 |
in
|
haftmann@19110
|
569 |
|
haftmann@19150
|
570 |
val instance_arity = instance_arity' setup_proof;
|
haftmann@19150
|
571 |
val instance_arity_i = instance_arity_i' setup_proof;
|
haftmann@19150
|
572 |
val prove_instance_arity = instance_arity_i' o tactic_proof;
|
haftmann@19110
|
573 |
|
haftmann@19110
|
574 |
end; (* local *)
|
haftmann@19110
|
575 |
|
haftmann@19110
|
576 |
local
|
haftmann@19110
|
577 |
|
haftmann@19136
|
578 |
fun fish_thms (name, expr) after_qed thy =
|
haftmann@19136
|
579 |
let
|
haftmann@19136
|
580 |
val _ = writeln ("sub " ^ name)
|
haftmann@19136
|
581 |
val suplocales = (fn Locale.Merge es => map (fn Locale.Locale n => n) es) expr;
|
haftmann@19136
|
582 |
val _ = writeln ("super " ^ commas suplocales)
|
haftmann@19280
|
583 |
fun get_c name =
|
haftmann@19136
|
584 |
(map (NameSpace.base o fst o fst) o Locale.parameters_of thy) name;
|
haftmann@19136
|
585 |
fun get_a name =
|
haftmann@19136
|
586 |
(map (NameSpace.base o fst o fst) o Locale.local_asms_of thy) name;
|
haftmann@19136
|
587 |
fun get_t supname =
|
haftmann@19136
|
588 |
map (NameSpace.append (NameSpace.append name ((space_implode "_" o get_c) supname)) o NameSpace.base)
|
haftmann@19136
|
589 |
(get_a name);
|
haftmann@19136
|
590 |
val names = map get_t suplocales;
|
haftmann@19136
|
591 |
val _ = writeln ("fishing for " ^ (commas o map commas) names);
|
haftmann@19136
|
592 |
in
|
haftmann@19136
|
593 |
thy
|
haftmann@19136
|
594 |
|> after_qed ((map o map) (Drule.standard o get_thm thy o Name) names)
|
haftmann@19136
|
595 |
end;
|
haftmann@19136
|
596 |
|
haftmann@19136
|
597 |
fun add_interpretation_in (after_qed : thm list list -> theory -> theory) (name, expr) thy =
|
haftmann@19136
|
598 |
thy
|
haftmann@19136
|
599 |
|> Locale.interpretation_in_locale (name, expr);
|
haftmann@19136
|
600 |
|
haftmann@19136
|
601 |
fun prove_interpretation_in tac (after_qed : thm list list -> theory -> theory) (name, expr) thy =
|
haftmann@19136
|
602 |
thy
|
haftmann@19136
|
603 |
|> Locale.interpretation_in_locale (name, expr)
|
haftmann@19136
|
604 |
|> Proof.global_terminal_proof (Method.Basic (fn _ => Method.SIMPLE_METHOD tac), NONE)
|
haftmann@19136
|
605 |
|-> (fn _ => I);
|
haftmann@19110
|
606 |
|
haftmann@19150
|
607 |
fun gen_instance_sort prep_class prep_sort do_proof (raw_class, raw_sort) theory =
|
haftmann@19110
|
608 |
let
|
haftmann@19110
|
609 |
val class = prep_class theory raw_class;
|
haftmann@19110
|
610 |
val sort = prep_sort theory raw_sort;
|
haftmann@19136
|
611 |
val loc_name = (#name_locale o the_class_data theory) class;
|
haftmann@19136
|
612 |
val loc_expr = if null sort
|
haftmann@19136
|
613 |
then Locale.empty
|
haftmann@19136
|
614 |
else
|
haftmann@19136
|
615 |
(Locale.Merge o map (Locale.Locale o #name_locale o the_class_data theory)) sort;
|
haftmann@19136
|
616 |
fun after_qed thmss thy =
|
haftmann@19136
|
617 |
(writeln "---"; (Pretty.writeln o Display.pretty_thms o Library.flat) thmss; writeln "---"; fold (fn supclass =>
|
wenzelm@19412
|
618 |
AxClass.prove_classrel (class, supclass)
|
haftmann@19136
|
619 |
(ALLGOALS (K (intro_classes_tac [])) THEN
|
haftmann@19136
|
620 |
(ALLGOALS o resolve_tac o Library.flat) thmss)
|
haftmann@19136
|
621 |
) sort thy)
|
haftmann@19110
|
622 |
in
|
haftmann@19110
|
623 |
theory
|
haftmann@19136
|
624 |
|> do_proof after_qed (loc_name, loc_expr)
|
haftmann@19110
|
625 |
end;
|
haftmann@19110
|
626 |
|
haftmann@19150
|
627 |
fun instance_sort' do_proof = gen_instance_sort intern_class read_sort do_proof;
|
haftmann@19150
|
628 |
fun instance_sort_i' do_proof = gen_instance_sort certify_class certify_sort do_proof;
|
haftmann@19136
|
629 |
val setup_proof = add_interpretation_in;
|
haftmann@19136
|
630 |
val tactic_proof = prove_interpretation_in;
|
haftmann@19110
|
631 |
|
haftmann@19110
|
632 |
in
|
haftmann@19110
|
633 |
|
haftmann@19150
|
634 |
val instance_sort = instance_sort' setup_proof;
|
haftmann@19150
|
635 |
val instance_sort_i = instance_sort_i' setup_proof;
|
haftmann@19150
|
636 |
val prove_instance_sort = instance_sort_i' o tactic_proof;
|
haftmann@19110
|
637 |
|
haftmann@19110
|
638 |
end; (* local *)
|
haftmann@19038
|
639 |
|
haftmann@18168
|
640 |
(* extracting dictionary obligations from types *)
|
haftmann@18168
|
641 |
|
haftmann@18168
|
642 |
type sortcontext = (string * sort) list;
|
haftmann@18168
|
643 |
|
haftmann@18335
|
644 |
fun extract_sortctxt thy ty =
|
haftmann@18702
|
645 |
(typ_tfrees o fst o Type.freeze_thaw_type) ty
|
haftmann@18884
|
646 |
|> map (apsnd (operational_sort_of thy))
|
haftmann@18168
|
647 |
|> filter (not o null o snd);
|
haftmann@18168
|
648 |
|
haftmann@18884
|
649 |
datatype classlookup = Instance of (class * string) * classlookup list list
|
haftmann@19253
|
650 |
| Lookup of class list * (string * (int * int))
|
haftmann@19213
|
651 |
|
haftmann@19213
|
652 |
fun pretty_lookup' (Instance ((class, tyco), lss)) =
|
haftmann@19213
|
653 |
(Pretty.block o Pretty.breaks) (
|
haftmann@19213
|
654 |
Pretty.enum "," "{" "}" [Pretty.str class, Pretty.str tyco]
|
haftmann@19213
|
655 |
:: map pretty_lookup lss
|
haftmann@19213
|
656 |
)
|
haftmann@19253
|
657 |
| pretty_lookup' (Lookup (classes, (v, (i, j)))) =
|
haftmann@19253
|
658 |
Pretty.enum " <" "[" "]" (map Pretty.str classes @ [Pretty.str (v ^ "!" ^ string_of_int i ^ "/" ^ string_of_int j)])
|
haftmann@19213
|
659 |
and pretty_lookup ls = (Pretty.enum "," "(" ")" o map pretty_lookup') ls;
|
haftmann@18168
|
660 |
|
haftmann@18864
|
661 |
fun extract_lookup thy sortctxt raw_typ_def raw_typ_use =
|
haftmann@18168
|
662 |
let
|
haftmann@18168
|
663 |
val typ_def = Type.varifyT raw_typ_def;
|
haftmann@18168
|
664 |
val typ_use = Type.varifyT raw_typ_use;
|
haftmann@18168
|
665 |
val match_tab = Sign.typ_match thy (typ_def, typ_use) Vartab.empty;
|
haftmann@18168
|
666 |
fun tab_lookup vname = (the o Vartab.lookup match_tab) (vname, 0);
|
haftmann@19110
|
667 |
fun mk_class_deriv thy subclasses superclass =
|
haftmann@18884
|
668 |
let
|
haftmann@19233
|
669 |
val (i, (subclass::deriv)) = (the oo get_index) (fn subclass =>
|
haftmann@19110
|
670 |
get_superclass_derivation thy (subclass, superclass)
|
haftmann@19110
|
671 |
) subclasses;
|
haftmann@19253
|
672 |
in (rev deriv, (i, length subclasses)) end;
|
haftmann@19213
|
673 |
fun mk_lookup (sort_def, (Type (tyco, tys))) =
|
haftmann@19213
|
674 |
map (fn class => Instance ((class, tyco),
|
haftmann@19213
|
675 |
map2 (curry mk_lookup)
|
wenzelm@19292
|
676 |
(map (operational_sort_of thy) (mg_domain thy tyco class))
|
haftmann@19213
|
677 |
tys)
|
haftmann@19213
|
678 |
) sort_def
|
haftmann@18168
|
679 |
| mk_lookup (sort_def, TVar ((vname, _), sort_use)) =
|
haftmann@18168
|
680 |
let
|
haftmann@18168
|
681 |
fun mk_look class =
|
haftmann@18884
|
682 |
let val (deriv, classindex) = mk_class_deriv thy (operational_sort_of thy sort_use) class
|
haftmann@18168
|
683 |
in Lookup (deriv, (vname, classindex)) end;
|
haftmann@18168
|
684 |
in map mk_look sort_def end;
|
haftmann@18864
|
685 |
in
|
haftmann@19280
|
686 |
sortctxt
|
haftmann@18864
|
687 |
|> map (tab_lookup o fst)
|
haftmann@18884
|
688 |
|> map (apfst (operational_sort_of thy))
|
haftmann@18864
|
689 |
|> filter (not o null o fst)
|
haftmann@18864
|
690 |
|> map mk_lookup
|
haftmann@18864
|
691 |
end;
|
haftmann@18864
|
692 |
|
haftmann@18884
|
693 |
fun extract_classlookup thy (c, raw_typ_use) =
|
haftmann@18864
|
694 |
let
|
haftmann@18864
|
695 |
val raw_typ_def = Sign.the_const_constraint thy c;
|
haftmann@18864
|
696 |
val typ_def = Type.varifyT raw_typ_def;
|
haftmann@18702
|
697 |
fun reorder_sortctxt ctxt =
|
haftmann@18702
|
698 |
case lookup_const_class thy c
|
haftmann@18702
|
699 |
of NONE => ctxt
|
haftmann@18702
|
700 |
| SOME class =>
|
haftmann@18702
|
701 |
let
|
haftmann@19038
|
702 |
val data = the_class_data thy class;
|
haftmann@19280
|
703 |
val sign = (Type.varifyT o the o AList.lookup (op =) ((map snd o #consts) data)) c;
|
haftmann@18702
|
704 |
val match_tab = Sign.typ_match thy (sign, typ_def) Vartab.empty;
|
haftmann@18702
|
705 |
val v : string = case Vartab.lookup match_tab (#var data, 0)
|
haftmann@18702
|
706 |
of SOME (_, TVar ((v, _), _)) => v;
|
haftmann@18702
|
707 |
in
|
haftmann@18702
|
708 |
(v, (the o AList.lookup (op =) ctxt) v) :: AList.delete (op =) v ctxt
|
haftmann@18702
|
709 |
end;
|
haftmann@18168
|
710 |
in
|
haftmann@18864
|
711 |
extract_lookup thy
|
haftmann@18864
|
712 |
(reorder_sortctxt (extract_sortctxt thy ((fst o Type.freeze_thaw_type) raw_typ_def)))
|
haftmann@18864
|
713 |
raw_typ_def raw_typ_use
|
haftmann@18168
|
714 |
end;
|
haftmann@18168
|
715 |
|
haftmann@18884
|
716 |
fun extract_classlookup_inst thy (class, tyco) supclass =
|
haftmann@18864
|
717 |
let
|
haftmann@18864
|
718 |
fun mk_typ class = Type (tyco, (map TFree o fst o the_inst_sign thy) (class, tyco))
|
haftmann@19136
|
719 |
val typ_def = mk_typ supclass;
|
haftmann@19136
|
720 |
val typ_use = mk_typ class;
|
haftmann@18864
|
721 |
in
|
haftmann@18864
|
722 |
extract_lookup thy (extract_sortctxt thy typ_def) typ_def typ_use
|
haftmann@18864
|
723 |
end;
|
haftmann@18168
|
724 |
|
haftmann@19253
|
725 |
fun extract_classlookup_member thy (ty_decl, ty_use) =
|
haftmann@19253
|
726 |
extract_lookup thy (extract_sortctxt thy ty_decl) ty_decl ty_use;
|
haftmann@18884
|
727 |
|
haftmann@18515
|
728 |
(* toplevel interface *)
|
haftmann@18515
|
729 |
|
haftmann@18515
|
730 |
local
|
haftmann@18515
|
731 |
|
haftmann@18515
|
732 |
structure P = OuterParse
|
haftmann@18515
|
733 |
and K = OuterKeyword
|
haftmann@18515
|
734 |
|
haftmann@18515
|
735 |
in
|
haftmann@18515
|
736 |
|
haftmann@18849
|
737 |
val (classK, instanceK) = ("class", "instance")
|
haftmann@18515
|
738 |
|
haftmann@19253
|
739 |
val use_cp_instance = ref false;
|
haftmann@19253
|
740 |
|
haftmann@19136
|
741 |
fun wrap_add_instance_subclass (class, sort) thy =
|
haftmann@19136
|
742 |
case Sign.read_sort thy sort
|
haftmann@19136
|
743 |
of [class'] =>
|
haftmann@19253
|
744 |
if ! use_cp_instance
|
haftmann@19253
|
745 |
andalso (is_some o lookup_class_data thy o Sign.intern_class thy) class
|
haftmann@19136
|
746 |
andalso (is_some o lookup_class_data thy o Sign.intern_class thy) class'
|
haftmann@19136
|
747 |
then
|
haftmann@19150
|
748 |
instance_sort (class, sort) thy
|
haftmann@19136
|
749 |
else
|
wenzelm@19246
|
750 |
axclass_instance_subclass (class, sort) thy
|
haftmann@19150
|
751 |
| _ => instance_sort (class, sort) thy;
|
haftmann@19136
|
752 |
|
haftmann@18911
|
753 |
val parse_inst =
|
haftmann@19136
|
754 |
(Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 P.sort --| P.$$$ ")")) [] -- P.xname --| P.$$$ "::" -- P.sort)
|
haftmann@19136
|
755 |
>> (fn ((asorts, tyco), sort) => ((tyco, asorts), sort))
|
haftmann@19136
|
756 |
|| (P.xname --| P.$$$ "::" -- P.!!! P.arity)
|
haftmann@19136
|
757 |
>> (fn (tyco, (asorts, sort)) => ((tyco, asorts), sort));
|
haftmann@18911
|
758 |
|
haftmann@19038
|
759 |
val locale_val =
|
haftmann@19038
|
760 |
(P.locale_expr --
|
haftmann@19038
|
761 |
Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 P.context_element)) [] ||
|
haftmann@19038
|
762 |
Scan.repeat1 P.context_element >> pair Locale.empty);
|
haftmann@19038
|
763 |
|
haftmann@19280
|
764 |
val class_subP = P.name -- Scan.repeat (P.$$$ "+" |-- P.name) >> (op ::);
|
haftmann@19280
|
765 |
val class_bodyP = P.!!! (Scan.repeat1 P.context_element);
|
haftmann@19280
|
766 |
|
haftmann@18515
|
767 |
val classP =
|
haftmann@18849
|
768 |
OuterSyntax.command classK "operational type classes" K.thy_decl (
|
haftmann@18849
|
769 |
P.name --| P.$$$ "="
|
haftmann@19280
|
770 |
-- (
|
haftmann@19280
|
771 |
class_subP --| P.$$$ "+" -- class_bodyP
|
haftmann@19280
|
772 |
|| class_subP >> rpair []
|
haftmann@19280
|
773 |
|| class_bodyP >> pair []
|
haftmann@19280
|
774 |
) >> (Toplevel.theory_context
|
haftmann@19280
|
775 |
o (fn (bname, (supclasses, elems)) => class bname supclasses elems)));
|
haftmann@18515
|
776 |
|
haftmann@18575
|
777 |
val instanceP =
|
haftmann@18849
|
778 |
OuterSyntax.command instanceK "prove type arity or subclass relation" K.thy_goal ((
|
haftmann@19136
|
779 |
P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> wrap_add_instance_subclass
|
haftmann@19136
|
780 |
|| P.opt_thm_name ":" -- (parse_inst -- Scan.repeat (P.opt_thm_name ":" -- P.prop))
|
wenzelm@19246
|
781 |
>> (fn (("", []), (((tyco, asorts), sort), [])) => axclass_instance_arity I (tyco, asorts, sort)
|
haftmann@19150
|
782 |
| (natts, (inst, defs)) => instance_arity inst natts defs)
|
haftmann@18849
|
783 |
) >> (Toplevel.print oo Toplevel.theory_to_proof));
|
haftmann@18575
|
784 |
|
haftmann@19110
|
785 |
val _ = OuterSyntax.add_parsers [classP, instanceP];
|
haftmann@19110
|
786 |
|
haftmann@19110
|
787 |
val _ = Context.add_setup (Method.add_methods
|
haftmann@19110
|
788 |
[("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
|
haftmann@19110
|
789 |
"back-chain introduction rules of classes"),
|
haftmann@19110
|
790 |
("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), "apply some intro/elim rule")]);
|
haftmann@18515
|
791 |
|
haftmann@18515
|
792 |
end; (* local *)
|
haftmann@18515
|
793 |
|
haftmann@18168
|
794 |
end; (* struct *)
|