explicit completions of arities
authorhaftmann
Fri Jul 11 09:02:30 2008 +0200 (2008-07-11 ago)
changeset 2754713199740ced6
parent 27546 726e8fa3e404
child 27548 8178db4b25f3
explicit completions of arities
src/Pure/axclass.ML
     1.1 --- a/src/Pure/axclass.ML	Fri Jul 11 09:02:29 2008 +0200
     1.2 +++ b/src/Pure/axclass.ML	Fri Jul 11 09:02:30 2008 +0200
     1.3 @@ -182,15 +182,51 @@
     1.4        Syntax.string_of_arity (ProofContext.init thy) (a, Ss, [c])));
     1.5  
     1.6  fun arity_property thy (c, a) x =
     1.7 -  these (Symtab.lookup (snd (get_instances thy)) a)
     1.8 +  Symtab.lookup_list (snd (get_instances thy)) a
     1.9    |> map_filter (fn ((c', _), th) => if c = c'
    1.10 -        then AList.lookup (op =) (Thm.get_tags th) x else NONE)
    1.11 +      then AList.lookup (op =) (Thm.get_tags th) x else NONE)
    1.12    |> rev;
    1.13  
    1.14 -fun put_arity ((t, Ss, c), th) = map_instances (fn (classrel, arities) =>
    1.15 -  (classrel, arities |> Symtab.insert_list (eq_fst op =) (t, ((c, Ss), th))));
    1.16 +fun insert_arity_completions thy (t, ((c, Ss), th)) arities =
    1.17 +  let
    1.18 +    val algebra = Sign.classes_of thy;
    1.19 +    val super_class_completions = Sign.super_classes thy c
    1.20 +      |> filter_out (fn c1 => exists (fn ((c2, Ss2), _) => c1 = c2
    1.21 +          andalso Sorts.sorts_le algebra (Ss2, Ss)) (Symtab.lookup_list arities t))
    1.22 +    val tags = Thm.get_tags th;
    1.23 +    val completions = map (fn c1 => (Sorts.weaken ((#classes o Sorts.rep_algebra) algebra)
    1.24 +      (fn (th, c2) => fn c3 => th RS the_classrel thy (c2, c3)) (th, c) c1
    1.25 +        |> Thm.map_tags (K tags) |> Thm.close_derivation, c1)) super_class_completions;
    1.26 +    val arities' = fold (fn (th1, c1) => Symtab.cons_list (t, ((c1, Ss), th1)))
    1.27 +      completions arities;
    1.28 +  in (completions, arities') end;
    1.29  
    1.30 +fun put_arity ((t, Ss, c), th) thy =
    1.31 +  let
    1.32 +    val th' = (Thm.map_tags o AList.default (op =))
    1.33 +      (Markup.theory_nameN, Context.theory_name thy) th;
    1.34 +    val arity' = (t, ((c, Ss), th'));
    1.35 +  in
    1.36 +    thy
    1.37 +    |> map_instances (fn (classrel, arities) => (classrel,
    1.38 +      arities
    1.39 +      |> Symtab.insert_list (eq_fst op =) arity'
    1.40 +      |> insert_arity_completions thy arity'
    1.41 +      |> snd))
    1.42 +  end;
    1.43  
    1.44 +fun complete_arities thy = 
    1.45 +  let
    1.46 +    val arities = snd (get_instances thy);
    1.47 +    val (completions, arities') = arities
    1.48 +      |> fold_map (insert_arity_completions thy) (Symtab.dest_list arities)
    1.49 +      |>> flat;
    1.50 +  in if null completions
    1.51 +    then NONE
    1.52 +    else SOME (thy |> map_instances (fn (classrel, _) => (classrel, arities')))
    1.53 +  end;
    1.54 +
    1.55 +val _ = Context.>> (Context.map_theory (Theory.at_begin complete_arities));
    1.56  
    1.57  
    1.58  (* maintain instance parameters *)
    1.59 @@ -272,10 +308,7 @@
    1.60       of [] => ()
    1.61        | cs => Output.legacy_feature
    1.62            ("Missing specifications for overloaded parameters " ^ commas_quote cs)
    1.63 -    val th' = th
    1.64 -      |> Drule.unconstrainTs
    1.65 -      |> (Thm.map_tags o AList.default (op =))
    1.66 -          (Markup.theory_nameN, Context.theory_name thy)
    1.67 +    val th' = Drule.unconstrainTs th;
    1.68    in
    1.69      thy
    1.70      |> Sign.primitive_arity (t, Ss, [c])