--- a/src/Pure/axclass.ML Mon Apr 24 16:37:52 2006 +0200
+++ b/src/Pure/axclass.ML Tue Apr 25 22:22:58 2006 +0200
@@ -2,19 +2,20 @@
ID: $Id$
Author: Markus Wenzel, TU Muenchen
-Axiomatic type classes.
+Axiomatic type classes: managing predicates and parameter collections.
*)
signature AX_CLASS =
sig
val print_axclasses: theory -> unit
- val get_info: theory -> class -> {super: sort, def: thm, intro: thm, axioms: thm list}
+ val get_info: theory -> class -> {def: thm, intro: thm, axioms: thm list}
val get_instances: theory ->
{classes: unit Graph.T,
classrel: ((class * class) * thm) list,
arities: ((string * sort list * class) * thm) list}
val class_intros: theory -> thm list
- val params_of_sort: theory -> sort -> string list
+ val params_of: theory -> class -> string list
+ val all_params_of: theory -> sort -> string list
val cert_classrel: theory -> class * class -> class * class
val read_classrel: theory -> xstring * xstring -> class * class
val add_classrel: thm -> theory -> theory
@@ -30,6 +31,7 @@
structure AxClass: AX_CLASS =
struct
+
(** theory data **)
(* class parameters (canonical order) *)
@@ -54,15 +56,14 @@
val axiomsN = "axioms";
datatype axclass = AxClass of
- {super: sort,
- def: thm,
+ {def: thm,
intro: thm,
axioms: thm list};
-fun make_axclass (super, def, intro, axioms) =
- AxClass {super = super, def = def, intro = intro, axioms = axioms};
+type axclasses = axclass Symtab.table * param list;
-type axclasses = axclass Symtab.table * param list;
+fun make_axclass (def, intro, axioms) =
+ AxClass {def = def, intro = intro, axioms = axioms};
fun merge_axclasses pp ((tab1, params1), (tab2, params2)) : axclasses =
(Symtab.merge (K true) (tab1, tab2), merge_params pp (params1, params2));
@@ -99,39 +100,15 @@
val empty : T = ((Symtab.empty, []), make_instances (Graph.empty, [], []));
val copy = I;
val extend = I;
-
fun merge pp ((axclasses1, instances1), (axclasses2, instances2)) =
(merge_axclasses pp (axclasses1, axclasses2), merge_instances (instances1, instances2));
-
- fun print thy ((axclasses, params), _) =
- let
- val ctxt = ProofContext.init thy;
- val prt_cls = ProofContext.pretty_sort ctxt o single;
-
- fun pretty_class c [] = prt_cls c
- | pretty_class c cs = Pretty.block
- (prt_cls c :: Pretty.str " <" :: Pretty.brk 1 :: Pretty.commas (map prt_cls cs));
-
- fun pretty_axclass (class, AxClass {super, def, intro, axioms}) =
- Pretty.block (Pretty.fbreaks
- [pretty_class class super,
- Pretty.strs ("parameters:" ::
- fold (fn (x, c) => if c = class then cons x else I) params []),
- ProofContext.pretty_fact ctxt ("def", [def]),
- ProofContext.pretty_fact ctxt (introN, [intro]),
- ProofContext.pretty_fact ctxt (axiomsN, axioms)]);
- in
- Pretty.writeln (Pretty.chunks (map pretty_axclass (Symtab.dest axclasses)))
- end;
+ fun print _ _ = ();
end);
val _ = Context.add_setup AxClassData.init;
-val print_axclasses = AxClassData.print;
-
-val get_instances = AxClassData.get #> (fn (_, Instances insts) => insts);
-(* lookup *)
+(* lookup classes *)
val lookup_info = Symtab.lookup o #1 o #1 o AxClassData.get;
@@ -148,16 +125,38 @@
in map (Thm.class_triv thy) classes @ fold add_intro classes [] end;
+(* lookup parameters *)
+
+fun get_params thy pred =
+ let val params = #2 (#1 (AxClassData.get thy))
+ in fold (fn (x, c) => if pred c then cons x else I) params [] end;
+
+fun params_of thy c = get_params thy (fn c' => c' = c);
+fun all_params_of thy S = get_params thy (fn c => Sign.subsort thy (S, [c]));
+
+
+(* print_axclasses *)
+
+fun print_axclasses thy =
+ let
+ val axclasses = #1 (#1 (AxClassData.get thy));
+ val ctxt = ProofContext.init thy;
+
+ fun pretty_axclass (class, AxClass {def, intro, axioms}) =
+ Pretty.block (Pretty.fbreaks
+ [Pretty.block
+ [Pretty.str "axclass ", ProofContext.pretty_sort ctxt [class], Pretty.str ":"],
+ Pretty.strs ("parameters:" :: params_of thy class),
+ ProofContext.pretty_fact ctxt ("def", [def]),
+ ProofContext.pretty_fact ctxt (introN, [intro]),
+ ProofContext.pretty_fact ctxt (axiomsN, axioms)]);
+ in Pretty.writeln (Pretty.chunks (map pretty_axclass (Symtab.dest axclasses))) end;
+
+
(** instances **)
-(* parameters *)
-
-fun params_of_sort thy S =
- let
- val range = Graph.all_succs (Sign.classes_of thy) (Sign.certify_sort thy S);
- val params = #2 (#1 (AxClassData.get thy));
- in fold (fn (x, c) => if member (op =) range c then cons x else I) params [] end;
+val get_instances = AxClassData.get #> (fn (_, Instances insts) => insts);
(* class relations *)
@@ -167,7 +166,7 @@
val (c1, c2) = pairself (Sign.certify_class thy) raw_rel;
val _ = Type.add_classrel (Sign.pp thy) [(c1, c2)] (Sign.tsig_of thy);
val _ =
- (case subtract (op =) (params_of_sort thy [c1]) (params_of_sort thy [c2]) of
+ (case subtract (op =) (all_params_of thy [c1]) (all_params_of thy [c2]) of
[] => ()
| xs => raise TYPE ("Class " ^ Sign.string_of_sort thy [c1] ^ " lacks parameter(s) " ^
commas_quote xs ^ " of " ^ Sign.string_of_sort thy [c2], [], []));
@@ -299,7 +298,7 @@
|> PureThy.note_thmss_i "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) |> snd
|> Sign.restore_naming facts_thy
|> AxClassData.map (apfst (fn (is, ps) =>
- (Symtab.update (class, make_axclass (super, def, intro, axioms)) is,
+ (Symtab.update (class, make_axclass (def, intro, axioms)) is,
fold (fn x => add_param pp (x, class)) params ps)));
in (class, result_thy) end;