--- a/src/Pure/axclass.ML Mon Apr 10 00:33:49 2006 +0200
+++ b/src/Pure/axclass.ML Mon Apr 10 00:33:51 2006 +0200
@@ -13,12 +13,14 @@
val mk_arities: string * sort list * sort -> term list
val dest_arity: term -> string * sort list * class
val print_axclasses: theory -> unit
- val get_info: theory -> string -> {super_classes: class list, intro: thm, axioms: thm list}
+ val get_info: theory -> class -> {super_classes: class list, intro: thm, axioms: thm list}
+ val get_instances: theory ->
+ {classrel: unit Graph.T, subsorts: ((sort * sort) * thm) list, arities: (arity * thm) list}
val class_intros: theory -> thm list
val add_axclass: bstring * xstring list -> ((bstring * string) * Attrib.src list) list ->
- theory -> {intro: thm, axioms: thm list} * theory
+ theory -> class * theory
val add_axclass_i: bstring * class list -> ((bstring * term) * attribute list) list ->
- theory -> {intro: thm, axioms: thm list} * theory
+ theory -> class * theory
val add_classrel: thm list -> theory -> theory
val add_arity: thm list -> theory -> theory
val prove_subclass: class * class -> tactic -> theory -> theory
@@ -31,23 +33,16 @@
(** abstract syntax operations **)
-fun aT S = TFree ("'a", S);
-
-fun dest_varT (TFree (x, S)) = ((x, ~1), S)
- | dest_varT (TVar a) = a
- | dest_varT T = raise TYPE ("AxClass.dest_varT", [T], []);
-
-
(* subclass propositions *)
-fun mk_classrel (c1, c2) = Logic.mk_inclass (aT [c1], c2);
+fun mk_classrel (c1, c2) = Logic.mk_inclass (Term.aT [c1], c2);
fun dest_classrel tm =
let
fun err () = raise TERM ("AxClass.dest_classrel", [tm]);
val (ty, c2) = Logic.dest_inclass tm handle TERM _ => err ();
- val c1 = (case dest_varT ty of (_, [c]) => c | _ => err ())
+ val c1 = (case dest_TVar ty of (_, [c]) => c | _ => err ())
handle TYPE _ => err ();
in (c1, c2) end;
@@ -68,7 +63,7 @@
val (ty, c) = Logic.dest_inclass tm handle TERM _ => err ();
val (t, tvars) =
(case ty of
- Type (t, tys) => (t, map dest_varT tys handle TYPE _ => err ())
+ Type (t, tys) => (t, map dest_TVar tys handle TYPE _ => err ())
| _ => err ());
val ss =
if has_duplicates (eq_fst (op =)) tvars then err ()
@@ -77,27 +72,59 @@
-(** axclass info **)
+(** theory data **)
+
+(* axclass *)
val introN = "intro";
val axiomsN = "axioms";
-type axclass_info =
- {super_classes: class list,
- intro: thm,
- axioms: thm list};
+datatype axclass = AxClass of
+ {super_classes: class list,
+ intro: thm,
+ axioms: thm list};
+
+fun make_axclass (super_classes, intro, axioms) =
+ AxClass {super_classes = super_classes, intro = intro, axioms = axioms};
+
+
+(* instances *)
+
+datatype instances = Instances of
+ {classrel: unit Graph.T, (*raw relation -- no closure!*)
+ subsorts: ((sort * sort) * thm) list,
+ arities: (arity * thm) list};
+
+fun make_instances (classrel, subsorts, arities) =
+ Instances {classrel = classrel, subsorts = subsorts, arities = arities};
-structure AxclassesData = TheoryDataFun
+fun map_instances f (Instances {classrel, subsorts, arities}) =
+ make_instances (f (classrel, subsorts, arities));
+
+fun merge_instances
+ (Instances {classrel = classrel1, subsorts = subsorts1, arities = arities1},
+ Instances {classrel = classrel2, subsorts = subsorts2, arities = arities2}) =
+ make_instances
+ (Graph.merge (K true) (classrel1, classrel2),
+ merge (eq_fst op =) (subsorts1, subsorts2),
+ merge (eq_fst op =) (arities1, arities2));
+
+
+(* setup data *)
+
+structure AxClassData = TheoryDataFun
(struct
- val name = "Pure/axclasses";
- type T = axclass_info Symtab.table;
+ val name = "Pure/axclass";
+ type T = axclass Symtab.table * instances;
- val empty = Symtab.empty;
+ val empty = (Symtab.empty, make_instances (Graph.empty, [], []));
val copy = I;
val extend = I;
- fun merge _ = Symtab.merge (K true);
- fun print thy tab =
+ fun merge _ ((axclasses1, instances1), (axclasses2, instances2)) =
+ (Symtab.merge (K true) (axclasses1, axclasses2), merge_instances (instances1, instances2));
+
+ fun print thy (axclasses, _) =
let
fun pretty_class c cs = Pretty.block
(Pretty.str (Sign.extern_class thy c) :: Pretty.str " <" :: Pretty.brk 1 ::
@@ -106,31 +133,39 @@
fun pretty_thms name thms = Pretty.big_list (name ^ ":")
(map (Display.pretty_thm_sg thy) thms);
- fun pretty_axclass (name, {super_classes, intro, axioms}) = Pretty.block (Pretty.fbreaks
- [pretty_class name super_classes, pretty_thms introN [intro], pretty_thms axiomsN axioms]);
- in Pretty.writeln (Pretty.chunks (map pretty_axclass (Symtab.dest tab))) end;
+ fun pretty_axclass (name, AxClass {super_classes, intro, axioms}) =
+ Pretty.block (Pretty.fbreaks
+ [pretty_class name super_classes, pretty_thms introN [intro], pretty_thms axiomsN axioms]);
+ in Pretty.writeln (Pretty.chunks (map pretty_axclass (Symtab.dest axclasses))) end;
end);
-val _ = Context.add_setup AxclassesData.init;
-val print_axclasses = AxclassesData.print;
+val _ = Context.add_setup AxClassData.init;
+val print_axclasses = AxClassData.print;
+
+val get_instances = AxClassData.get #> (fn (_, Instances insts) => insts);
-val lookup_info = Symtab.lookup o AxclassesData.get;
+
+(** axclass definitions **)
+
+(* lookup *)
+
+val lookup_info = Symtab.lookup o #1 o AxClassData.get;
fun get_info thy c =
(case lookup_info thy c of
- NONE => error ("Unknown axclass " ^ quote c)
- | SOME info => info);
+ SOME (AxClass info) => info
+ | NONE => error ("Unknown axclass " ^ quote c));
fun class_intros thy =
- let val classes = Sign.classes thy in
- map (Thm.class_triv thy) classes @
- List.mapPartial (Option.map #intro o lookup_info thy) classes
- end;
+ let
+ fun add_intro c =
+ (case lookup_info thy c of SOME (AxClass {intro, ...}) => cons intro | _ => I);
+ val classes = Sign.classes thy;
+ in map (Thm.class_triv thy) classes @ fold add_intro classes [] end;
-
-(** add axiomatic type classes **)
+(* add_axclass(_i) *)
local
@@ -157,8 +192,8 @@
(*prepare abstract axioms*)
fun abs_axm ax =
if null (term_tfrees ax) then
- Logic.mk_implies (Logic.mk_inclass (aT [], class), ax)
- else replace_tfree (aT [class]) ax;
+ Logic.mk_implies (Logic.mk_inclass (Term.aT [], class), ax)
+ else replace_tfree (Term.aT [class]) ax;
val abs_axms = map (abs_axm o snd) axms;
fun axm_sort (name, ax) =
@@ -168,8 +203,8 @@
| _ => err_bad_tfrees name);
val axS = Sign.certify_sort class_thy (List.concat (map axm_sort axms));
- val int_axm = Logic.close_form o replace_tfree (aT axS);
- fun inclass c = Logic.mk_inclass (aT axS, c);
+ val int_axm = Logic.close_form o replace_tfree (Term.aT axS);
+ fun inclass c = Logic.mk_inclass (Term.aT axS, c);
val intro_axm = Logic.list_implies
(map inclass super_classes @ map (int_axm o #2) axms, inclass class);
@@ -180,16 +215,16 @@
|> Theory.add_path (Logic.const_of_class bclass)
|> PureThy.add_axioms_i [Thm.no_attributes (introN, intro_axm)]
||>> PureThy.add_axiomss_i [Thm.no_attributes (axiomsN, abs_axms)];
- val info = {super_classes = super_classes, intro = intro, axioms = axioms};
+ val info = make_axclass (super_classes, intro, axioms);
(*store info*)
val (_, final_thy) =
axms_thy
- |> Theory.add_finals_i false [Const (Logic.const_of_class class, a_itselfT --> propT)]
+ |> Theory.add_finals_i false [Const (Logic.const_of_class class, Term.a_itselfT --> propT)]
|> PureThy.add_thms ((map #1 axms ~~ axioms) ~~ atts)
||> Theory.restore_naming class_thy
- ||> AxclassesData.map (Symtab.update (class, info));
- in ({intro = intro, axioms = axioms}, final_thy) end;
+ ||> AxClassData.map (apfst (Symtab.update (class, info)));
+ in (class, final_thy) end;
in
@@ -200,29 +235,41 @@
-(** proven class instantiation **)
+(** instantiation proofs **)
-(* primitive rules *)
+(* primitives *)
fun add_classrel ths thy =
let
- fun prep_thm th =
+ fun add_rel (c1, c2) =
+ Graph.default_node (c1, ()) #> Graph.default_node (c2, ()) #> Graph.add_edge (c1, c2);
+ val rels = ths |> map (fn th =>
let
val prop = Drule.plain_prop_of (Thm.transfer thy th);
val (c1, c2) = dest_classrel prop handle TERM _ =>
raise THM ("AxClass.add_classrel: not a class relation", 0, [th]);
- in (c1, c2) end;
- in Theory.add_classrel_i (map prep_thm ths) thy end;
+ in (c1, c2) end);
+ in
+ thy
+ |> Theory.add_classrel_i rels
+ |> AxClassData.map (apsnd (map_instances (fn (classrel, subsorts, arities) =>
+ (classrel |> fold add_rel rels, (map (pairself single) rels ~~ ths) @ subsorts, arities))))
+ end;
fun add_arity ths thy =
let
- fun prep_thm th =
+ val ars = ths |> map (fn th =>
let
val prop = Drule.plain_prop_of (Thm.transfer thy th);
val (t, ss, c) = dest_arity prop handle TERM _ =>
raise THM ("AxClass.add_arity: not a type arity", 0, [th]);
- in (t, ss, [c]) end;
- in Theory.add_arities_i (map prep_thm ths) thy end;
+ in (t, ss, [c]) end);
+ in
+ thy
+ |> Theory.add_arities_i ars
+ |> AxClassData.map (apsnd (map_instances (fn (classrel, subsorts, arities) =>
+ (classrel, subsorts, (ars ~~ ths) @ arities))))
+ end;
(* tactical proofs *)
@@ -245,4 +292,5 @@
quote (Sign.string_of_arity thy arity));
in add_arity ths thy end;
+
end;