# HG changeset patch # User wenzelm # Date 1146859183 -7200 # Node ID 7c761751e9986cf10208114fd90dd32bc13d9057 # Parent 340c466c96051a9927c2967b28bbb52f5ac4eea5 of_sort: explicit cache value; simplified internal representation of instances; diff -r 340c466c9605 -r 7c761751e998 src/Pure/axclass.ML --- a/src/Pure/axclass.ML Fri May 05 21:59:41 2006 +0200 +++ b/src/Pure/axclass.ML Fri May 05 21:59:43 2006 +0200 @@ -29,7 +29,9 @@ val axiomatize_classrel_i: (class * class) list -> theory -> theory val axiomatize_arity: xstring * string list * string -> theory -> theory val axiomatize_arity_i: arity -> theory -> theory - val of_sort: theory -> typ * sort -> thm list option + type cache + val cache: cache + val of_sort: theory -> typ * sort -> cache -> thm list * cache (*exception Sorts.CLASS_ERROR*) end; structure AxClass: AX_CLASS = @@ -78,26 +80,13 @@ val classrelN = "classrel"; val arityN = "arity"; -datatype instances = Instances of - {classes: unit Graph.T, (*raw relation -- no closure!*) - classrel: ((class * class) * thm) list, - arities: ((class * sort list) * thm) list Symtab.table, - types: (class * thm) list Typtab.table}; - -fun make_instances (classes, classrel, arities, types) = - Instances {classes = classes, classrel = classrel, arities = arities, types = types}; +type instances = + ((class * class) * thm) list * + ((class * sort list) * thm) list Symtab.table; -fun map_instances f (Instances {classes, classrel, arities, types}) = - make_instances (f (classes, classrel, arities, types)); - -fun merge_instances - (Instances {classes = classes1, classrel = classrel1, arities = arities1, types = types1}, - Instances {classes = classes2, classrel = classrel2, arities = arities2, types = types2}) = - make_instances - (Graph.merge (K true) (classes1, classes2), - merge (eq_fst op =) (classrel1, classrel2), - Symtab.join (K (merge (eq_fst op =))) (arities1, arities2), - Typtab.join (K (merge (eq_fst op =))) (types1, types2)); +fun merge_instances ((classrel1, arities1): instances, (classrel2, arities2)) = + (merge (eq_fst op =) (classrel1, classrel2), + Symtab.join (K (merge (eq_fst op =))) (arities1, arities2)); (* setup data *) @@ -105,22 +94,24 @@ structure AxClassData = TheoryDataFun (struct val name = "Pure/axclass"; - type T = axclasses * instances ref; - val empty : T = - ((Symtab.empty, []), ref (make_instances (Graph.empty, [], Symtab.empty, Typtab.empty))); - fun copy (axclasses, ref instances) : T = (axclasses, ref instances); - val extend = copy; - fun merge pp ((axclasses1, ref instances1), (axclasses2, ref instances2)) = - (merge_axclasses pp (axclasses1, axclasses2), ref (merge_instances (instances1, instances2))); + type T = axclasses * instances; + val empty : T = ((Symtab.empty, []), ([], Symtab.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 _ _ = (); end); val _ = Context.add_setup AxClassData.init; -(* retrieve axclasses *) +(* maintain axclasses *) -val lookup_def = Symtab.lookup o #1 o #1 o AxClassData.get; +val get_axclasses = #1 o AxClassData.get; +fun map_axclasses f = AxClassData.map (apfst f); + +val lookup_def = Symtab.lookup o #1 o get_axclasses; fun get_definition thy c = (case lookup_def thy c of @@ -135,10 +126,8 @@ in map (Thm.class_triv thy) classes @ fold add_intro classes [] end; -(* retrieve parameters *) - fun get_params thy pred = - let val params = #2 (#1 (AxClassData.get thy)) + let val params = #2 (get_axclasses 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); @@ -147,40 +136,33 @@ (* maintain instances *) -val get_instances = AxClassData.get #> (fn (_, ref (Instances insts)) => insts); - -fun lookup_classrel thy = - Option.map (Thm.transfer thy) o AList.lookup (op =) (#classrel (get_instances thy)); - -fun lookup_arity thy = - Option.map (Thm.transfer thy) oo - (AList.lookup (op =) o Symtab.lookup_list (#arities (get_instances thy))); - -val lookup_type = AList.lookup (op =) oo (Typtab.lookup_list o #types o get_instances); +val get_instances = #2 o AxClassData.get; +fun map_instances f = AxClassData.map (apsnd f); -fun store_instance f thy (x, th) = - (change (#2 (AxClassData.get thy)) (map_instances (f (x, th))); th); +fun the_classrel thy (c1, c2) = + (case AList.lookup (op =) (#1 (get_instances thy)) (c1, c2) of + SOME th => Thm.transfer thy th + | NONE => error ("Unproven class relation " ^ Sign.string_of_classrel thy [c1, c2])); + +fun put_classrel arg = map_instances (fn (classrel, arities) => + (insert (eq_fst op =) arg classrel, arities)); -val store_classrel = store_instance (fn ((c1, c2), th) => fn (classes, classrel, arities, types) => - (classes - |> Graph.default_node (c1, ()) - |> Graph.default_node (c2, ()) - |> Graph.add_edge (c1, c2), - insert (eq_fst op =) ((c1, c2), th) classrel, arities, types)); -val store_arity = store_instance (fn ((t, Ss, c), th) => fn (classes, classrel, arities, types) => - (classes, classrel, arities |> Symtab.insert_list (eq_fst op =) (t, ((c, Ss), th)), types)); +fun the_arity thy a (c, Ss) = + (case AList.lookup (op =) (Symtab.lookup_list (#2 (get_instances thy)) a) (c, Ss) of + SOME th => Thm.transfer thy th + | NONE => error ("Unproven type arity " ^ Sign.string_of_arity thy (a, Ss, [c]))); -val store_type = store_instance (fn ((T, c), th) => fn (classes, classrel, arities, types) => - (classes, classrel, arities, types |> Typtab.insert_list (eq_fst op =) (T, (c, th)))); +fun put_arity ((t, Ss, c), th) = map_instances (fn (classrel, arities) => + (classrel, arities |> Symtab.insert_list (eq_fst op =) (t, ((c, Ss), th)))); (* print data *) fun print_axclasses thy = let - val axclasses = #1 (#1 (AxClassData.get thy)); + val axclasses = #1 (get_axclasses thy); val ctxt = ProofContext.init thy; fun pretty_axclass (class, AxClass {def, intro, axioms}) = @@ -223,9 +205,11 @@ val prop = Drule.plain_prop_of (Thm.transfer thy th); val rel = Logic.dest_classrel prop handle TERM _ => err (); val (c1, c2) = cert_classrel thy rel handle TYPE _ => err (); - val thy' = thy |> Sign.primitive_classrel (c1, c2); - val _ = store_classrel thy' ((c1, c2), Drule.unconstrainTs th); - in thy' end; + in + thy + |> Sign.primitive_classrel (c1, c2) + |> put_classrel ((c1, c2), Drule.unconstrainTs th) + end; fun add_arity th thy = let @@ -233,9 +217,11 @@ val prop = Drule.plain_prop_of (Thm.transfer thy th); val (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err (); val _ = if map (Sign.certify_sort thy) Ss = Ss then () else err (); - val thy' = thy |> Sign.primitive_arity (t, Ss, [c]); - val _ = store_arity thy' ((t, Ss, c), Drule.unconstrainTs th); - in thy' end; + in + thy + |> Sign.primitive_arity (t, Ss, [c]) + |> put_arity ((t, Ss, c), Drule.unconstrainTs th) + end; (* tactical proofs *) @@ -325,19 +311,19 @@ [((introN, []), [([Drule.standard raw_intro], [])]), ((superN, []), [(map Drule.standard raw_classrel, [])]), ((axiomsN, []), [(map (fn th => Drule.standard (class_triv RS th)) raw_axioms, [])])]; - val _ = map (store_classrel facts_thy) (map (pair class) super ~~ classrel); (* result *) val result_thy = facts_thy + |> fold put_classrel (map (pair class) super ~~ classrel) |> Sign.add_path bconst |> PureThy.note_thmss_i "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) |> snd |> Sign.restore_naming facts_thy - |> AxClassData.map (apfst (fn (axclasses, parameters) => + |> map_axclasses (fn (axclasses, parameters) => (Symtab.update (class, make_axclass (def, intro, axioms)) axclasses, - fold (fn x => add_param pp (x, class)) params parameters))); + fold (fn x => add_param pp (x, class)) params parameters)); in (class, result_thy) end; @@ -389,27 +375,13 @@ (** explicit derivations -- cached **) +datatype cache = Types of (class * thm) list Typtab.table; +val cache = Types Typtab.empty; + local -fun derive_classrel thy (th, c1) c2 = - let - fun derive [c, c'] = the (lookup_classrel thy (c, c')) - | derive (c :: c' :: cs) = derive [c, c'] RS derive (c' :: cs); - val th' = - (case lookup_classrel thy (c1, c2) of - SOME rule => rule - | NONE => - (case Graph.find_paths (#classes (get_instances thy)) (c1, c2) of - [] => error ("Cannot derive class relation " ^ Sign.string_of_classrel thy [c1, c2]) - | path :: _ => store_classrel thy ((c1, c2), derive path))) - in th RS th' end; - -fun derive_constructor thy a dom c = - let val Ss = map (map snd) dom and ths = maps (map fst) dom in - (case lookup_arity thy a (c, Ss) of - SOME rule => ths MRS rule - | NONE => error ("Cannot derive type arity " ^ Sign.string_of_arity thy (a, Ss, [c]))) - end; +fun lookup_type (Types cache) = AList.lookup (op =) o Typtab.lookup_list cache; +fun insert_type T der (Types cache) = Types (Typtab.insert_list (eq_fst op =) (T, der) cache); fun derive_type _ (_, []) = [] | derive_type thy (typ, sort) = @@ -418,28 +390,35 @@ (fn T as TFree (_, S) => insert (eq_fst op =) (T, S) | T as TVar (_, S) => insert (eq_fst op =) (T, S) | _ => I) typ []; - val hyps = vars |> map (fn (T, S) => (T, Drule.sort_triv thy (T, S) ~~ S)); + val hyps = vars + |> map (fn (T, S) => (T, Drule.sort_triv thy (T, S) ~~ S)); val ths = (typ, sort) |> Sorts.of_sort_derivation (Sign.pp thy) (Sign.classes_of thy, Sign.arities_of thy) - {classrel = derive_classrel thy, - constructor = derive_constructor thy, - variable = the_default [] o AList.lookup (op =) hyps}; - in map (store_type thy) (map (pair typ) sort ~~ ths) end; + {classrel = + fn (th, c1) => fn c2 => th RS the_classrel thy (c1, c2), + constructor = + fn a => fn dom => fn c => + let val Ss = map (map snd) dom and ths = maps (map fst) dom + in ths MRS the_arity thy a (c, Ss) end, + variable = + the_default [] o AList.lookup (op =) hyps}; + in ths end; in -fun of_sort thy (typ, sort) = - if Sign.of_sort thy (typ, sort) then - let - val cert = Thm.cterm_of thy; - fun derive c = - Goal.finish (the (lookup_type thy typ c) RS Goal.init (cert (Logic.mk_inclass (typ, c)))) - |> Thm.adjust_maxidx_thm; - val _ = derive_type thy (typ, filter (is_none o lookup_type thy typ) sort) - handle ERROR msg => cat_error msg ("The error(s) above occurred for sort derivation: " ^ - Sign.string_of_typ thy typ ^ " :: " ^ Sign.string_of_sort thy sort); - in SOME (map derive sort) end - else NONE; +fun of_sort thy (typ, sort) cache = + let + val sort' = filter (is_none o lookup_type cache typ) sort; + val ths' = derive_type thy (typ, sort') + handle ERROR msg => cat_error msg ("The error(s) above occurred for sort derivation: " ^ + Sign.string_of_typ thy typ ^ " :: " ^ Sign.string_of_sort thy sort'); + val cache' = cache |> fold (insert_type typ) (sort' ~~ ths'); + val ths = + sort |> map (fn c => + Goal.finish (the (lookup_type cache' typ c) RS + Goal.init (Thm.cterm_of thy (Logic.mk_inclass (typ, c)))) + |> Thm.adjust_maxidx_thm); + in (ths, cache') end; end;