tagged arities
authorhaftmann
Mon Jun 30 13:41:31 2008 +0200 (2008-06-30 ago)
changeset 273971d8456c5d53d
parent 27396 77ea650bfc3a
child 27398 768da1da59d6
tagged arities
src/Pure/axclass.ML
     1.1 --- a/src/Pure/axclass.ML	Mon Jun 30 13:41:30 2008 +0200
     1.2 +++ b/src/Pure/axclass.ML	Mon Jun 30 13:41:31 2008 +0200
     1.3 @@ -37,6 +37,7 @@
     1.4    val unoverload_const: theory -> string * typ -> string
     1.5    val param_of_inst: theory -> string * string -> string
     1.6    val inst_of_param: theory -> string -> (string * string) option
     1.7 +  val these_arity_tags: theory -> class * string -> Markup.property list
     1.8    type cache
     1.9    val of_sort: theory -> typ * sort -> cache -> thm list * cache  (*exception Sorts.CLASS_ERROR*)
    1.10    val cache: cache
    1.11 @@ -79,8 +80,8 @@
    1.12  
    1.13  type axclasses = axclass Symtab.table * param list;
    1.14  
    1.15 -fun make_axclass ((def, intro, axioms), params) =
    1.16 -  AxClass {def = def, intro = intro, axioms = axioms, params = params};
    1.17 +fun make_axclass ((def, intro, axioms), params) = AxClass
    1.18 +  {def = def, intro = intro, axioms = axioms, params = params};
    1.19  
    1.20  fun merge_axclasses pp ((tab1, params1), (tab2, params2)) : axclasses =
    1.21    (Symtab.merge (K true) (tab1, tab2), merge_params pp (params1, params2));
    1.22 @@ -180,10 +181,17 @@
    1.23    | NONE => error ("Unproven type arity " ^
    1.24        Syntax.string_of_arity (ProofContext.init thy) (a, Ss, [c])));
    1.25  
    1.26 +fun these_arity_tags thy (c, a) = case find_first (fn ((c', _), _) => c = c')
    1.27 +  (these (Symtab.lookup (snd (get_instances thy)) a)) of
    1.28 +    SOME ((_, _), th) => Thm.get_tags th
    1.29 +  | NONE => [];
    1.30 +
    1.31  fun put_arity ((t, Ss, c), th) = map_instances (fn (classrel, arities) =>
    1.32    (classrel, arities |> Symtab.insert_list (eq_fst op =) (t, ((c, Ss), th))));
    1.33  
    1.34  
    1.35 +
    1.36 +
    1.37  (* maintain instance parameters *)
    1.38  
    1.39  val get_inst_params = #2 o #2 o AxClassData.get;
    1.40 @@ -263,10 +271,14 @@
    1.41       of [] => ()
    1.42        | cs => Output.legacy_feature
    1.43            ("Missing specifications for overloaded parameters " ^ commas_quote cs)
    1.44 +    val th' = th
    1.45 +      |> Drule.unconstrainTs
    1.46 +      |> (Thm.map_tags o AList.default (op =))
    1.47 +          (Markup.theory_nameN, Context.theory_name thy)
    1.48    in
    1.49      thy
    1.50      |> Sign.primitive_arity (t, Ss, [c])
    1.51 -    |> put_arity ((t, Ss, c), Drule.unconstrainTs th)
    1.52 +    |> put_arity ((t, Ss, c), th')
    1.53    end;
    1.54  
    1.55