# HG changeset patch # User wenzelm # Date 1144622031 -7200 # Node ID a631cd2117a8a54744e8962773847315c1cde75a # Parent 4812d28c90a63f20f8bcd885e67cc4321ec2e9c4 add_axclass(_i): return class name only; subclass/arity statements: require actual TVars, store raw data; tuned; diff -r 4812d28c90a6 -r a631cd2117a8 src/Pure/axclass.ML --- 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;