author  wenzelm 
Fri, 19 Jan 2007 22:08:08 +0100  
changeset 22101  6d13239d5f52 
parent 22074  de3586cb0ebd 
child 22182  05ed4080cbd7 
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, 

221 
defs: thm list 

222 
(*for experimental class target*) 

223 
}; 

224 

225 
fun rep_classdata (ClassData c) = c; 

226 

227 
structure ClassData = TheoryDataFun ( 

228 
struct 

229 
val name = "Pure/classes"; 

230 
type T = class_data Graph.T; 

231 
val empty = Graph.empty; 

232 
val copy = I; 

233 
val extend = I; 

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

235 
fun print _ _ = (); 

236 
end 

237 
); 

238 

239 
val _ = Context.add_setup ClassData.init; 

240 

241 

242 
(* queries *) 

243 

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

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

246 
fun the_class_data thy class = 

247 
case lookup_class_data thy class 

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

249 
 SOME data => data; 

250 

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

252 

253 
fun the_parm_map thy class = 

254 
let 

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

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

257 
in 

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

259 
end; 

260 

261 
val the_propnames = #propnames oo the_class_data; 

262 

263 
fun print_classes thy = 

264 
let 

265 
val algebra = Sign.classes_of thy; 

266 
val arities = 

267 
Symtab.empty 

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

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

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

271 
val the_arities = these o Symtab.lookup arities; 

272 
fun mk_arity class tyco = 

273 
let 

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

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

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

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

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

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

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

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

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

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

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

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

286 
Pretty.str "instances:", 

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

288 
] 

289 
] 

290 
in 

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

292 
algebra 

293 
end; 

294 

295 

296 
(* updaters *) 

297 

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

299 
ClassData.map ( 

300 
Graph.new_node (class, ClassData { 

301 
locale = locale, 

302 
consts = consts, 

303 
propnames = propnames, 

304 
defs = []}) 

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

306 
); 

307 

308 
fun add_def (class, thm) = 

309 
(ClassData.map o Graph.map_node class) 

310 
(fn ClassData { locale, 

311 
consts, propnames, defs } => ClassData { locale = locale, 

312 
consts = consts, propnames = propnames, defs = thm :: defs }); 

313 

314 

315 
(* tactics and methods *) 

316 

317 
fun intro_classes_tac facts st = 

318 
(ALLGOALS (Method.insert_tac facts THEN' 

319 
REPEAT_ALL_NEW (resolve_tac (AxClass.class_intros (Thm.theory_of_thm st)))) 

320 
THEN Tactic.distinct_subgoals_tac) st; 

321 

322 
fun default_intro_classes_tac [] = intro_classes_tac [] 

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

324 

325 
fun default_tac rules ctxt facts = 

326 
HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE 

327 
default_intro_classes_tac facts; 

328 

329 
val _ = Context.add_setup (Method.add_methods 

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

331 
"backchain introduction rules of classes"), 

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

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

334 

335 

22069  336 
(* FIXME workarounds for locale package *) 
21954  337 

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

339 
let 

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

341 
let 

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

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

344 
in s end 

345 
 ad_hoc_term t = 

346 
let 

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

348 
val s = Pretty.output p; 

349 
in s end; 

350 
in 

351 
thy 

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

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

354 
> ProofContext.theory_of 

355 
end; 

356 

22069  357 
fun prove_interpretation_in tac after_qed (name, expr) thy = 
358 
thy 

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

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

361 
> ProofContext.theory_of; 

362 

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

364 
let 

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

366 
val loc_expr = 

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

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

369 
o maps (#consts o the_class_data theory) 

370 
o the_ancestry theory) [class]; 

371 
fun get_thms thy = 

372 
the_ancestry thy sort 

373 
> AList.make (the_propnames thy) 

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

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

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

377 
of [] => NONE 

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

379 
fun after_qed thy = 

380 
thy 

381 
> `get_thms 

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

383 
AxClass.prove_classrel (class, supclass) 

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

385 
(ALLGOALS o ProofContext.fact_tac) thms)) 

386 
in 

387 
theory 

388 
> do_proof after_qed (loc_name, loc_expr) 

389 
end; 

390 

22074  391 
val prove_instance_sort = instance_sort' o prove_interpretation_in; 
392 

22069  393 

394 
(* classes and instances *) 

395 

396 
local 

397 

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

399 
let 

400 
val (c, thy') = thy 

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

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

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

404 

405 
fun certify_class thy class = 

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

407 

408 
fun read_class thy = 

409 
certify_class thy o Sign.intern_class thy; 

410 

21954  411 
fun gen_class add_locale prep_class bname raw_supclasses raw_elems thy = 
412 
let 

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

414 
val supclasses = map (prep_class thy) raw_supclasses; 

415 
val supsort = 

416 
supclasses 

417 
> Sign.certify_sort thy 

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

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

420 
val supconsts = AList.make 

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

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

423 
fun check_locale thy name_locale = 

424 
let 

425 
val tfrees = 

426 
[] 

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

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

429 
in case tfrees 

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

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

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

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

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

435 
(commas o map fst) tfrees) 

436 
end; 

437 
fun extract_params thy name_locale = 

438 
Locale.parameters_of thy name_locale 

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

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

441 
> chop (length supconsts) 

442 
> snd; 

443 
fun extract_assumes name_locale params thy cs = 

444 
let 

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

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

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

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

21954  450 
fun prep_asm ((name, atts), ts) = 
451 
(*FIXME*) 

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

453 
in 

454 
Locale.local_asms_of thy name_locale 

455 
> map prep_asm 

456 
end; 

22048  457 
fun extract_axiom_names thy name_locale = 
458 
name_locale 

459 
> Locale.local_asms_of thy 

460 
> map (NameSpace.base o fst o fst) (*FIXME*) 

21954  461 
fun mk_const thy class (c, ty) = 
462 
Const (c, Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty); 

463 
in 

464 
thy 

465 
> add_locale bname supexpr elems 

466 
> (fn name_locale => ProofContext.theory_result ( 

467 
tap (fn thy => check_locale thy name_locale) 

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

469 
#> (fn params => 

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

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

22048  472 
`(fn thy => extract_axiom_names thy name_locale) 
473 
#> (fn axiom_names => 

474 
add_class_data ((name_axclass, supclasses), 

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

21954  476 
#> prove_interpretation (Logic.const_of_class bname, []) 
477 
(Locale.Locale name_locale) (map (SOME o mk_const thy name_axclass) (map snd supconsts @ consts)) 

478 
((ALLGOALS o ProofContext.fact_tac) ax_axioms) 

479 
#> pair name_axclass 

22048  480 
))))) 
21954  481 
end; 
482 

483 
in 

484 

485 
val class_e = gen_class (Locale.add_locale false) read_class; 

486 
val class = gen_class (Locale.add_locale_i false) certify_class; 

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

487 

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

489 

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

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

491 

21954  492 
fun gen_instance_sort prep_class prep_sort (raw_class, raw_sort) theory = 
493 
let 

494 
val class = prep_class theory raw_class; 

495 
val sort = prep_sort theory raw_sort; 

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

497 
theory 

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

499 
else case sort 

500 
of [class'] => 

501 
theory 

502 
> axclass_instance_sort (class, class') 

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

504 
end; 

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

505 

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

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

507 

21954  508 
val instance_sort_e = gen_instance_sort Sign.read_class Sign.read_sort; 
509 
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

510 

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

511 
end; (* local *) 
19038  512 

19957  513 

21954  514 
(** experimental class target **) 
515 

516 
fun export_typ thy loc = 

517 
let 

518 
val class = loc (*FIXME*); 

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

520 
in 

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

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

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

524 
end; 

525 

526 
fun export_def thy loc = 

527 
let 

528 
val class = loc (*FIXME*); 

529 
val consts = the_parm_map thy class; 

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

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

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

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

534 
of SOME c_ty => Const c_ty 

535 
 NONE => t) 

536 
 subst t = t; 

537 
in 

538 
Term.map_aterms subst #> map_types subst_typ 

539 
end; 

540 

541 
fun export_thm thy loc = 

542 
let 

543 
val class = loc (*FIXME*); 

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

545 
in 

546 
MetaSimplifier.rewrite_rule thms 

547 
end; 

548 

549 

550 

20455  551 
(** toplevel interface **) 
18515  552 

553 
local 

554 

555 
structure P = OuterParse 

556 
and K = OuterKeyword 

557 

558 
in 

559 

20385  560 
val (classK, instanceK, print_classesK) = ("class", "instance", "print_classes") 
18515  561 

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

20601  565 
val parse_arity = 
566 
(P.xname  P.$$$ "::"  P.!!! P.arity) 

19136  567 
>> (fn (tyco, (asorts, sort)) => ((tyco, asorts), sort)); 
18911  568 

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

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

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

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

574 
 class_subP >> rpair [] 
20964  575 
 class_bodyP >> pair []) 
576 
 P.opt_begin 

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

21805  578 
Toplevel.begin_local_theory begin 
21954  579 
(class_e bname supclasses elems #> TheoryTarget.begin true))); 
18515  580 

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

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

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

587 
) >> (Toplevel.print oo Toplevel.theory_to_proof)); 
18575  588 

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

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

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

593 

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

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

595 

20455  596 
end; (*local*) 
18515  597 

20455  598 
end; 