author  haftmann 
Wed, 31 Jan 2007 16:05:16 +0100  
changeset 22222  bb07dd6cb1b9 
parent 22209  86b688409dde 
child 22302  bf5bdb7f7607 
permissions  rwrr 
18168  1 
(* Title: Pure/Tools/class_package.ML 
2 
ID: $Id$ 

3 
Author: Florian Haftmann, TU Muenchen 

4 

19468  5 
Type classes derived from primitive axclasses and locales. 
18168  6 
*) 
7 

8 
signature CLASS_PACKAGE = 

9 
sig 

21954  10 
val class: bstring > class list > Element.context_i Locale.element list > theory > 
20964  11 
string * Proof.context 
21954  12 
val instance_arity: ((bstring * sort list) * sort) list 
21924  13 
> ((bstring * attribute list) * term) list 
18575  14 
> theory > Proof.state 
21924  15 
val prove_instance_arity: tactic > ((string * sort list) * sort) list 
16 
> ((bstring * attribute list) * term) list 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

17 
> theory > theory 
21954  18 
val instance_sort: class * sort > theory > Proof.state 
19150  19 
val prove_instance_sort: tactic > class * sort > theory > theory 
18168  20 

20175  21 
val assume_arities_of_sort: theory > ((string * sort list) * sort) list > typ * sort > bool 
22 
val assume_arities_thy: theory > ((string * sort list) * sort) list > (theory > 'a) > 'a 

23 
(*'a must not keep any reference to theory*) 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

24 

21954  25 
(* experimental class target *) 
21553  26 
val add_def: class * thm > theory > theory 
27 
val export_typ: theory > class > typ > typ 

28 
val export_def: theory > class > term > term 

29 
val export_thm: theory > class > thm > thm 

30 

18702  31 
val print_classes: theory > unit 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

32 
val intro_classes_tac: thm list > tactic 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

33 
val default_intro_classes_tac: thm list > tactic 
18168  34 
end; 
35 

20182
79c9ff40d760
tactic for prove_instance_arity now gets definition theorems as arguments
haftmann
parents:
20175
diff
changeset

36 
structure ClassPackage : CLASS_PACKAGE = 
18168  37 
struct 
38 

21954  39 
(** axclasses with implicit parameter handling **) 
18168  40 

21954  41 
(* axclass instances *) 
18168  42 

21954  43 
local 
19456  44 

21954  45 
fun gen_instance mk_prop add_thm after_qed insts thy = 
46 
let 

47 
fun after_qed' results = 

48 
ProofContext.theory ((fold o fold) add_thm results #> after_qed); 

49 
in 

50 
thy 

51 
> ProofContext.init 

52 
> Proof.theorem_i NONE after_qed' ((map (fn t => [(t, [])]) o maps (mk_prop thy)) insts) 

53 
end; 

18168  54 

21954  55 
in 
56 

57 
val axclass_instance_arity = 

58 
gen_instance (Logic.mk_arities oo Sign.cert_arity) AxClass.add_arity; 

59 
val axclass_instance_sort = 

60 
gen_instance (single oo (Logic.mk_classrel oo AxClass.cert_classrel)) 

61 
AxClass.add_classrel I o single; 

62 

63 
end; (* local *) 

18575  64 

19038  65 

21954  66 
(* introducing axclasses with implicit parameter handling *) 
19038  67 

21954  68 
fun axclass_params (name, raw_superclasses) raw_consts raw_dep_axioms thy = 
21924  69 
let 
21954  70 
val superclasses = map (Sign.certify_class thy) raw_superclasses; 
71 
val consts = (map o apfst o apsnd) (Sign.certify_typ thy) raw_consts; 

72 
fun add_const ((c, ty), syn) = 

73 
Sign.add_consts_authentic [(c, ty, syn)] #> pair (Sign.full_name thy c, ty); 

74 
fun mk_axioms cs thy = 

75 
raw_dep_axioms thy cs 

76 
> (map o apsnd o map) (Sign.cert_prop thy) 

77 
> rpair thy; 

78 
fun add_constraint class (c, ty) = 

79 
Sign.add_const_constraint_i (c, SOME (Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty)); 

21924  80 
in 
21954  81 
thy 
82 
> fold_map add_const consts 

83 
> (fn cs => mk_axioms cs 

84 
#> (fn axioms => AxClass.define_class_i (name, superclasses) (map fst cs) axioms 

85 
#> (fn class => `(fn thy => AxClass.get_definition thy class) 

86 
#> (fn {intro, axioms, ...} => fold (add_constraint class) cs 

87 
#> pair (class, ((intro, axioms), cs)))))) 

21924  88 
end; 
89 

18168  90 

21954  91 
(* contexts with arity assumptions *) 
20175  92 

93 
fun assume_arities_of_sort thy arities ty_sort = 

94 
let 

95 
val pp = Sign.pp thy; 

96 
val algebra = Sign.classes_of thy 

97 
> fold (fn ((tyco, asorts), sort) => 

98 
Sorts.add_arities pp (tyco, map (fn class => (class, asorts)) sort)) arities; 

99 
in Sorts.of_sort algebra ty_sort end; 

100 

101 
fun assume_arities_thy thy arities f = 

102 
let 

103 
val thy_read = (fold (fn ((tyco, asorts), sort) 

104 
=> Sign.primitive_arity (tyco, asorts, sort)) arities o Theory.copy) thy 

105 
in f thy_read end; 

106 

20455  107 

21954  108 
(* instances with implicit parameter handling *) 
19038  109 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

110 
local 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

111 

20175  112 
fun gen_read_def thy prep_att read_def ((raw_name, raw_atts), raw_t) = 
19038  113 
let 
19957  114 
val (_, t) = read_def thy (raw_name, raw_t); 
115 
val ((c, ty), _) = Sign.cert_def (Sign.pp thy) t; 

116 
val atts = map (prep_att thy) raw_atts; 

20175  117 
val insts = (Consts.typargs (Sign.consts_of thy) (c, ty)) 
19957  118 
val name = case raw_name 
20385  119 
of "" => NONE 
120 
 _ => SOME raw_name; 

20175  121 
in (c, (insts, ((name, t), atts))) end; 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

122 

21954  123 
fun read_def_e thy = gen_read_def thy Attrib.attribute read_axm; 
124 
fun read_def thy = gen_read_def thy (K I) (K I); 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

125 

21924  126 
fun gen_instance_arity prep_arity prep_att read_def do_proof raw_arities raw_defs theory = 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

127 
let 
20175  128 
fun prep_arity' ((tyco, asorts), sort) = prep_arity theory (tyco, asorts, sort); 
129 
val arities = map prep_arity' raw_arities; 

130 
val arities_pair = map (fn (tyco, asorts, sort) => ((tyco, asorts), sort)) arities; 

131 
val _ = if null arities then error "at least one arity must be given" else (); 

132 
val _ = case (duplicates (op =) o map #1) arities 

133 
of [] => () 

134 
 dupl_tycos => error ("type constructors occur more than once in arities: " 

135 
^ (commas o map quote) dupl_tycos); 

21954  136 
val super_sort = (Graph.all_succs o #classes o Sorts.rep_algebra o Sign.classes_of) theory 
20175  137 
fun get_consts_class tyco ty class = 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

138 
let 
21954  139 
val cs = (these o Option.map snd o try (AxClass.params_of_class theory)) class; 
21463
42dd50268c8b
completed class parameter handling in axclass.ML
haftmann
parents:
21444
diff
changeset

140 
val subst_ty = map_type_tfree (K ty); 
19957  141 
in 
21894  142 
map (fn (c, ty) => (c, ((tyco, class), subst_ty ty))) cs 
19957  143 
end; 
20175  144 
fun get_consts_sort (tyco, asorts, sort) = 
19957  145 
let 
20192
956cd30ef3be
renamed Name.give_names to Name.names and moved Name.alphanum to Symbol.alphanum
haftmann
parents:
20191
diff
changeset

146 
val ty = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) (Name.names Name.context "'a" asorts)) 
21954  147 
in maps (get_consts_class tyco ty) (super_sort sort) end; 
20175  148 
val cs = maps get_consts_sort arities; 
20385  149 
fun mk_typnorm thy (ty, ty_sc) = 
150 
case try (Sign.typ_match thy (Logic.varifyT ty_sc, ty)) Vartab.empty 

151 
of SOME env => SOME (Logic.varifyT #> Envir.typ_subst_TVars env #> Logic.unvarifyT) 

152 
 NONE => NONE; 

20175  153 
fun read_defs defs cs thy_read = 
154 
let 

19957  155 
fun read raw_def cs = 
156 
let 

20385  157 
val (c, (inst, ((name_opt, t), atts))) = read_def thy_read raw_def; 
158 
val ty = Consts.instance (Sign.consts_of thy_read) (c, inst); 

20175  159 
val ((tyco, class), ty') = case AList.lookup (op =) cs c 
19957  160 
of NONE => error ("superfluous definition for constant " ^ quote c) 
19966  161 
 SOME class_ty => class_ty; 
20385  162 
val name = case name_opt 
20628  163 
of NONE => Thm.def_name (Logic.name_arity (tyco, [], c)) 
20385  164 
 SOME name => name; 
165 
val t' = case mk_typnorm thy_read (ty', ty) 

19966  166 
of NONE => error ("superfluous definition for constant " ^ 
167 
quote c ^ "::" ^ Sign.string_of_typ thy_read ty) 

20548
8ef25fe585a8
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
wenzelm
parents:
20465
diff
changeset

168 
 SOME norm => map_types norm t 
20175  169 
in (((class, tyco), ((name, t'), atts)), AList.delete (op =) c cs) end; 
19957  170 
in fold_map read defs cs end; 
20175  171 
val (defs, _) = assume_arities_thy theory arities_pair (read_defs raw_defs cs); 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

172 
fun get_remove_contraint c thy = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

173 
let 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

174 
val ty = Sign.the_const_constraint thy c; 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

175 
in 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

176 
thy 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

177 
> Sign.add_const_constraint_i (c, NONE) 
20385  178 
> pair (c, Logic.unvarifyT ty) 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

179 
end; 
19966  180 
fun add_defs defs thy = 
181 
thy 

182 
> PureThy.add_defs_i true (map snd defs) 

183 
> (fn thms => pair (map fst defs ~~ thms)); 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

184 
fun after_qed cs thy = 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

185 
thy 
19412  186 
> fold Sign.add_const_constraint_i (map (apsnd SOME) cs); 
19038  187 
in 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

188 
theory 
20385  189 
> fold_map get_remove_contraint (map fst cs > distinct (op =)) 
19966  190 
>> add_defs defs 
21954  191 
> (fn (cs, _) => do_proof (after_qed cs) arities) 
19038  192 
end; 
193 

21954  194 
fun instance_arity_e' do_proof = gen_instance_arity Sign.read_arity Attrib.attribute 
195 
read_def_e do_proof; 

196 
fun instance_arity' do_proof = gen_instance_arity Sign.cert_arity (K I) 

19957  197 
read_def do_proof; 
21924  198 
fun tactic_proof tac after_qed arities = 
199 
fold (fn arity => AxClass.prove_arity arity tac) arities 

20175  200 
#> after_qed; 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

201 

4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

202 
in 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

203 

21954  204 
val instance_arity_e = instance_arity_e' axclass_instance_arity; 
205 
val instance_arity = instance_arity' axclass_instance_arity; 

206 
val prove_instance_arity = instance_arity' o tactic_proof; 

207 

208 
end; (* local *) 

209 

210 

211 

212 
(** combining locales and axclasses **) 

213 

214 
(* theory data *) 

215 

216 
datatype class_data = ClassData of { 

217 
locale: string, 

218 
consts: (string * string) list 

219 
(*locale parameter ~> toplevel theory constant*), 

220 
propnames: string list, 

22182  221 
(*for adhoc instance in*) 
21954  222 
defs: thm list 
223 
(*for experimental class target*) 

224 
}; 

225 

226 
fun rep_classdata (ClassData c) = c; 

227 

228 
structure ClassData = TheoryDataFun ( 

229 
struct 

230 
val name = "Pure/classes"; 

231 
type T = class_data Graph.T; 

232 
val empty = Graph.empty; 

233 
val copy = I; 

234 
val extend = I; 

235 
fun merge _ = Graph.merge (K true); 

236 
fun print _ _ = (); 

237 
end 

238 
); 

239 

240 
val _ = Context.add_setup ClassData.init; 

241 

242 

243 
(* queries *) 

244 

245 
val lookup_class_data = Option.map rep_classdata oo try o Graph.get_node o ClassData.get; 

246 
val is_class = can o Graph.get_node o ClassData.get; 

247 
fun the_class_data thy class = 

248 
case lookup_class_data thy class 

249 
of NONE => error ("undeclared class " ^ quote class) 

250 
 SOME data => data; 

251 

252 
fun the_ancestry thy = Graph.all_succs (ClassData.get thy); 

253 

254 
fun the_parm_map thy class = 

255 
let 

256 
val const_typs = (#params o AxClass.get_definition thy) class; 

257 
val const_names = (#consts o the_class_data thy) class; 

258 
in 

259 
map (apsnd (fn c => (c, (the o AList.lookup (op =) const_typs) c))) const_names 

260 
end; 

261 

262 
val the_propnames = #propnames oo the_class_data; 

263 

264 
fun print_classes thy = 

265 
let 

266 
val algebra = Sign.classes_of thy; 

267 
val arities = 

268 
Symtab.empty 

269 
> Symtab.fold (fn (tyco, arities) => fold (fn (class, _) => 

270 
Symtab.map_default (class, []) (insert (op =) tyco)) arities) 

271 
((#arities o Sorts.rep_algebra) algebra); 

272 
val the_arities = these o Symtab.lookup arities; 

273 
fun mk_arity class tyco = 

274 
let 

275 
val Ss = Sorts.mg_domain algebra tyco [class]; 

276 
in Sign.pretty_arity thy (tyco, Ss, [class]) end; 

277 
fun mk_param (c, ty) = Pretty.str (Sign.extern_const thy c ^ " :: " 

278 
^ setmp show_sorts false (Sign.string_of_typ thy o Type.strip_sorts) ty); 

279 
fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [ 

280 
(SOME o Pretty.str) ("class " ^ class ^ ":"), 

281 
(SOME o Pretty.block) [Pretty.str "supersort: ", 

282 
(Sign.pretty_sort thy o Sign.certify_sort thy o Sign.super_classes thy) class], 

283 
Option.map (Pretty.str o prefix "locale: " o #locale) (lookup_class_data thy class), 

284 
((fn [] => NONE  ps => (SOME o Pretty.block o Pretty.fbreaks) (Pretty.str "parameters:" :: ps)) o map mk_param 

285 
o these o Option.map #params o try (AxClass.get_definition thy)) class, 

286 
(SOME o Pretty.block o Pretty.breaks) [ 

287 
Pretty.str "instances:", 

288 
Pretty.list "" "" (map (mk_arity class) (the_arities class)) 

289 
] 

290 
] 

291 
in 

292 
(Pretty.writeln o Pretty.chunks o separate (Pretty.str "") o map mk_entry o Sorts.all_classes) 

293 
algebra 

294 
end; 

295 

296 

297 
(* updaters *) 

298 

299 
fun add_class_data ((class, superclasses), (locale, consts, propnames)) = 

300 
ClassData.map ( 

301 
Graph.new_node (class, ClassData { 

302 
locale = locale, 

303 
consts = consts, 

304 
propnames = propnames, 

305 
defs = []}) 

306 
#> fold (curry Graph.add_edge class) superclasses 

307 
); 

308 

309 
fun add_def (class, thm) = 

310 
(ClassData.map o Graph.map_node class) 

22182  311 
(fn ClassData { locale, consts, propnames, defs } => ClassData { locale = locale, 
21954  312 
consts = consts, propnames = propnames, defs = thm :: defs }); 
313 

314 

315 
(* tactics and methods *) 

316 

317 
fun intro_classes_tac facts st = 

22182  318 
let 
319 
val thy = Thm.theory_of_thm st; 

320 
val ctxt = ProofContext.init thy; 

321 
val intro_classes_tac = ALLGOALS 

322 
(Method.insert_tac facts THEN' REPEAT_ALL_NEW (resolve_tac (AxClass.class_intros thy))) 

323 
THEN Tactic.distinct_subgoals_tac; 

324 
val intro_locales_tac = Locale.intro_locales_tac true ctxt facts; 

325 
in 

326 
(intro_classes_tac THEN TRY intro_locales_tac) st 

327 
end; 

21954  328 

329 
fun default_intro_classes_tac [] = intro_classes_tac [] 

330 
 default_intro_classes_tac _ = Tactical.no_tac; (*no error message!*) 

331 

332 
fun default_tac rules ctxt facts = 

333 
HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE 

334 
default_intro_classes_tac facts; 

335 

336 
val _ = Context.add_setup (Method.add_methods 

337 
[("intro_classes", Method.no_args (Method.METHOD intro_classes_tac), 

338 
"backchain introduction rules of classes"), 

339 
("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), 

340 
"apply some intro/elim rule")]); 

341 

342 

22069  343 
(* FIXME workarounds for locale package *) 
21954  344 

345 
fun prove_interpretation (prfx, atts) expr insts tac thy = 

346 
let 

347 
fun ad_hoc_term (Const (c, ty)) = 

348 
let 

349 
val p = setmp show_types true (setmp show_sorts true (setmp print_mode [] (Sign.pretty_typ thy))) ty; 

350 
val s = c ^ "::" ^ Pretty.output p; 

351 
in s end 

352 
 ad_hoc_term t = 

353 
let 

354 
val p = setmp show_types true (setmp show_sorts true (setmp print_mode [] (Sign.pretty_term thy))) t; 

355 
val s = Pretty.output p; 

356 
in s end; 

357 
in 

358 
thy 

359 
> Locale.interpretation I (prfx, atts) expr (map (Option.map ad_hoc_term) insts) 

360 
> Proof.global_terminal_proof (Method.Basic (fn _ => Method.SIMPLE_METHOD tac), NONE) 

361 
> ProofContext.theory_of 

362 
end; 

363 

22069  364 
fun prove_interpretation_in tac after_qed (name, expr) thy = 
365 
thy 

366 
> Locale.interpretation_in_locale (ProofContext.theory after_qed) (name, expr) 

367 
> Proof.global_terminal_proof (Method.Basic (fn _ => Method.SIMPLE_METHOD tac), NONE) 

368 
> ProofContext.theory_of; 

369 

370 
fun instance_sort' do_proof (class, sort) theory = 

371 
let 

372 
val loc_name = (#locale o the_class_data theory) class; 

373 
val loc_expr = 

374 
(Locale.Merge o map (Locale.Locale o #locale o the_class_data theory)) sort; 

375 
val const_names = (map (NameSpace.base o snd) 

376 
o maps (#consts o the_class_data theory) 

377 
o the_ancestry theory) [class]; 

378 
fun get_thms thy = 

379 
the_ancestry thy sort 

380 
> AList.make (the_propnames thy) 

381 
> map (apsnd (map (NameSpace.append (Logic.const_of_class loc_name)))) 

382 
> map_filter (fn (superclass, thm_names) => 

383 
case map_filter (try (PureThy.get_thm thy o Name)) thm_names 

384 
of [] => NONE 

385 
 thms => SOME (superclass, thms)); 

386 
fun after_qed thy = 

387 
thy 

388 
> `get_thms 

389 
> fold (fn (supclass, thms) => I 

390 
AxClass.prove_classrel (class, supclass) 

391 
(ALLGOALS (K (intro_classes_tac [])) THEN 

392 
(ALLGOALS o ProofContext.fact_tac) thms)) 

393 
in 

394 
theory 

395 
> do_proof after_qed (loc_name, loc_expr) 

396 
end; 

397 

22074  398 
val prove_instance_sort = instance_sort' o prove_interpretation_in; 
399 

22069  400 

401 
(* classes and instances *) 

402 

403 
local 

404 

405 
fun add_axclass (name, supsort) params axs thy = 

406 
let 

407 
val (c, thy') = thy 

408 
> AxClass.define_class_i (name, supsort) params axs; 

409 
val {intro, axioms, ...} = AxClass.get_definition thy' c; 

410 
in ((c, (intro, axioms)), thy') end; 

411 

412 
fun certify_class thy class = 

413 
tap (the_class_data thy) (Sign.certify_class thy class); 

414 

415 
fun read_class thy = 

416 
certify_class thy o Sign.intern_class thy; 

417 

21954  418 
fun gen_class add_locale prep_class bname raw_supclasses raw_elems thy = 
419 
let 

420 
val elems = fold_rev (fn Locale.Elem e => cons e  _ => I) raw_elems []; 

421 
val supclasses = map (prep_class thy) raw_supclasses; 

422 
val supsort = 

423 
supclasses 

424 
> Sign.certify_sort thy 

425 
> (fn [] => Sign.defaultS thy  S => S); (* FIXME Why syntax defaultS? *) 

426 
val supexpr = Locale.Merge (map (Locale.Locale o #locale o the_class_data thy) supclasses); 

427 
val supconsts = AList.make 

428 
(the o AList.lookup (op =) ((maps (the_parm_map thy) o the_ancestry thy) supclasses)) 

429 
((map (fst o fst) o Locale.parameters_of_expr thy) supexpr); 

430 
fun check_locale thy name_locale = 

431 
let 

432 
val tfrees = 

433 
[] 

434 
> fold (fold Term.add_tfrees o snd) (Locale.global_asms_of thy name_locale) 

435 
> fold (Term.add_tfreesT o snd o fst) (Locale.parameters_of thy name_locale); 

436 
in case tfrees 

437 
of [(_, _)] => () 

438 
(* [(_, sort)] => error ("Additional sort constraint on class variable: " 

439 
^ Sign.string_of_sort thy sort) FIXME what to do about this?*) 

440 
 [] => error ("No type variable in class specification") 

441 
 tfrees => error ("More than one type variable in class specification: " ^ 

442 
(commas o map fst) tfrees) 

443 
end; 

444 
fun extract_params thy name_locale = 

445 
Locale.parameters_of thy name_locale 

446 
> (map o apfst o apsnd o Term.map_type_tfree) (K (TFree (AxClass.param_tyvarname, []))) 

447 
> (map o apsnd) (TheoryTarget.fork_mixfix false true #> fst) 

448 
> chop (length supconsts) 

449 
> snd; 

450 
fun extract_assumes name_locale params thy cs = 

451 
let 

452 
val consts = supconsts @ (map (fst o fst) params ~~ cs); 

453 
(*FIXME is this type handling correct?*) 

454 
fun subst (Free (c, ty)) = 

22048  455 
Const ((fst o the o AList.lookup (op =) consts) c, ty) 
456 
 subst t = t; 

21954  457 
fun prep_asm ((name, atts), ts) = 
458 
(*FIXME*) 

459 
((NameSpace.base name, map (Attrib.attribute thy) atts), (map o map_aterms) subst ts); 

460 
in 

22182  461 
Locale.global_asms_of thy name_locale 
21954  462 
> map prep_asm 
463 
end; 

22048  464 
fun extract_axiom_names thy name_locale = 
465 
name_locale 

22182  466 
> Locale.global_asms_of thy 
22048  467 
> map (NameSpace.base o fst o fst) (*FIXME*) 
21954  468 
fun mk_const thy class (c, ty) = 
469 
Const (c, Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty); 

470 
in 

471 
thy 

472 
> add_locale bname supexpr elems 

473 
> (fn name_locale => ProofContext.theory_result ( 

474 
tap (fn thy => check_locale thy name_locale) 

475 
#> `(fn thy => extract_params thy name_locale) 

476 
#> (fn params => 

477 
axclass_params (bname, supsort) params (extract_assumes name_locale params) 

478 
#> (fn (name_axclass, ((_, ax_axioms), consts)) => 

22048  479 
`(fn thy => extract_axiom_names thy name_locale) 
480 
#> (fn axiom_names => 

481 
add_class_data ((name_axclass, supclasses), 

482 
(name_locale, map (fst o fst) params ~~ map fst consts, axiom_names)) 

21954  483 
#> prove_interpretation (Logic.const_of_class bname, []) 
22182  484 
(Locale.Locale name_locale) (map (SOME o mk_const thy name_axclass) (map snd supconsts @ consts)) 
21954  485 
((ALLGOALS o ProofContext.fact_tac) ax_axioms) 
486 
#> pair name_axclass 

22048  487 
))))) 
21954  488 
end; 
489 

490 
in 

491 

22182  492 
val class_e = gen_class (Locale.add_locale true) read_class; 
493 
val class = gen_class (Locale.add_locale_i true) certify_class; 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

494 

20455  495 
end; (*local*) 
19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

496 

4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

497 
local 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

498 

21954  499 
fun gen_instance_sort prep_class prep_sort (raw_class, raw_sort) theory = 
500 
let 

501 
val class = prep_class theory raw_class; 

502 
val sort = prep_sort theory raw_sort; 

503 
in if is_class theory class andalso forall (is_class theory) sort then 

504 
theory 

505 
> instance_sort' (Locale.interpretation_in_locale o ProofContext.theory) (class, sort) 

506 
else case sort 

507 
of [class'] => 

508 
theory 

509 
> axclass_instance_sort (class, class') 

510 
 _ => error ("Exactly one class expected: " ^ Sign.string_of_sort theory sort) 

511 
end; 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

512 

4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

513 
in 
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

514 

21954  515 
val instance_sort_e = gen_instance_sort Sign.read_class Sign.read_sort; 
516 
val instance_sort = gen_instance_sort Sign.certify_class Sign.certify_sort; 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

517 

4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

518 
end; (* local *) 
19038  519 

19957  520 

21954  521 
(** experimental class target **) 
522 

523 
fun export_typ thy loc = 

524 
let 

525 
val class = loc (*FIXME*); 

526 
val (v, _) = AxClass.params_of_class thy class; 

527 
in 

528 
Term.map_type_tfree (fn var as (w, sort) => 

529 
if w = v then TFree (w, Sorts.inter_sort (Sign.classes_of thy) 

530 
(sort, [class])) else TFree var) 

531 
end; 

532 

533 
fun export_def thy loc = 

534 
let 

535 
val class = loc (*FIXME*); 

536 
val consts = the_parm_map thy class; 

537 
val subst_typ = Term.map_type_tfree (fn var as (w, sort) => 

538 
if w = AxClass.param_tyvarname then TFree (w, Sorts.inter_sort (Sign.classes_of thy) 

539 
(sort, [class])) else TFree var) 

540 
fun subst (t as Free (v, _)) = (case AList.lookup (op =) consts v 

541 
of SOME c_ty => Const c_ty 

542 
 NONE => t) 

543 
 subst t = t; 

544 
in 

545 
Term.map_aterms subst #> map_types subst_typ 

546 
end; 

547 

548 
fun export_thm thy loc = 

549 
let 

550 
val class = loc (*FIXME*); 

551 
val thms = (#defs o the_class_data thy) class; 

552 
in 

553 
MetaSimplifier.rewrite_rule thms 

554 
end; 

555 

556 

557 

20455  558 
(** toplevel interface **) 
18515  559 

560 
local 

561 

562 
structure P = OuterParse 

563 
and K = OuterKeyword 

564 

565 
in 

566 

20385  567 
val (classK, instanceK, print_classesK) = ("class", "instance", "print_classes") 
18515  568 

20385  569 
val class_subP = P.name  Scan.repeat (P.$$$ "+"  P.name) >> (op ::); 
22101  570 
val class_bodyP = P.!!! (Scan.repeat1 SpecParse.locale_element); 
20385  571 

20601  572 
val parse_arity = 
573 
(P.xname  P.$$$ "::"  P.!!! P.arity) 

19136  574 
>> (fn (tyco, (asorts, sort)) => ((tyco, asorts), sort)); 
18911  575 

18515  576 
val classP = 
22222  577 
OuterSyntax.command classK "define type class" K.thy_decl ( 
18849
05a16861d3a5
added three times overloaded Isar instance command
haftmann
parents:
18829
diff
changeset

578 
P.name  P.$$$ "=" 
19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

579 
 ( 
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

580 
class_subP  P.$$$ "+"  class_bodyP 
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
19253
diff
changeset

581 
 class_subP >> rpair [] 
20964  582 
 class_bodyP >> pair []) 
583 
 P.opt_begin 

584 
>> (fn ((bname, (supclasses, elems)), begin) => 

21805  585 
Toplevel.begin_local_theory begin 
21954  586 
(class_e bname supclasses elems #> TheoryTarget.begin true))); 
18515  587 

18575  588 
val instanceP = 
18849
05a16861d3a5
added three times overloaded Isar instance command
haftmann
parents:
18829
diff
changeset

589 
OuterSyntax.command instanceK "prove type arity or subclass relation" K.thy_goal (( 
21954  590 
P.xname  ((P.$$$ "\\<subseteq>"  P.$$$ "<")  P.!!! P.xname) 
591 
>> instance_sort_e 

22101  592 
 P.and_list1 parse_arity  Scan.repeat (SpecParse.opt_thm_name ":"  P.prop) 
21954  593 
>> (fn (arities, defs) => instance_arity_e arities defs) 
18849
05a16861d3a5
added three times overloaded Isar instance command
haftmann
parents:
18829
diff
changeset

594 
) >> (Toplevel.print oo Toplevel.theory_to_proof)); 
18575  595 

20385  596 
val print_classesP = 
597 
OuterSyntax.improper_command print_classesK "print classes of this theory" K.diag 

598 
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory 

599 
o Toplevel.keep (print_classes o Toplevel.theory_of))); 

600 

601 
val _ = OuterSyntax.add_parsers [classP, instanceP, print_classesP]; 

19110
4bda27adcd2e
moved intro_classes from AxClass to ClassPackage
haftmann
parents:
19102
diff
changeset

602 

20455  603 
end; (*local*) 
18515  604 

20455  605 
end; 