Sign.minimize/complete_sort;
authorwenzelm
Wed Sep 26 20:50:33 2007 +0200 (2007-09-26)
changeset 24731c25aa6ae64ec
parent 24730 a87d8d31abc0
child 24732 08c2dd5378c7
Sign.minimize/complete_sort;
src/Pure/Isar/class.ML
src/Pure/Isar/code.ML
src/Pure/axclass.ML
     1.1 --- a/src/Pure/Isar/class.ML	Wed Sep 26 20:27:58 2007 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Wed Sep 26 20:50:33 2007 +0200
     1.3 @@ -255,8 +255,6 @@
     1.4       of [] => ()
     1.5        | dupl_tycos => error ("type constructors occur more than once in arities: "
     1.6            ^ (commas o map quote) dupl_tycos);
     1.7 -    val super_sort =
     1.8 -      (Graph.all_succs o #classes o Sorts.rep_algebra o Sign.classes_of) theory;
     1.9      fun get_consts_class tyco ty class =
    1.10        let
    1.11          val cs = (these o Option.map snd o try (AxClass.params_of_class theory)) class;
    1.12 @@ -268,7 +266,7 @@
    1.13        let
    1.14          val ty = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort))
    1.15            (Name.names Name.context "'a" asorts))
    1.16 -      in maps (get_consts_class tyco ty) (super_sort sort) end;
    1.17 +      in maps (get_consts_class tyco ty) (Sign.complete_sort theory sort) end;
    1.18      val cs = maps get_consts_sort arities;
    1.19      fun mk_typnorm thy (ty, ty_sc) =
    1.20        case try (Sign.typ_match thy (Logic.varifyT ty_sc, ty)) Vartab.empty
    1.21 @@ -418,7 +416,7 @@
    1.22      fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [
    1.23        (SOME o Pretty.str) ("class " ^ class ^ ":"),
    1.24        (SOME o Pretty.block) [Pretty.str "supersort: ",
    1.25 -        (Sign.pretty_sort thy o Sign.certify_sort thy o Sign.super_classes thy) class],
    1.26 +        (Sign.pretty_sort thy o Sign.minimize_sort thy o Sign.super_classes thy) class],
    1.27        Option.map (Pretty.str o prefix "locale: " o #locale) (lookup_class_data thy class),
    1.28        ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks) (Pretty.str "parameters:" :: ps)) o map mk_param
    1.29          o these o Option.map #params o try (AxClass.get_definition thy)) class,
    1.30 @@ -575,8 +573,8 @@
    1.31        | Locale.Expr i => apsnd (cons i)) raw_elems ([], []);
    1.32      val supclasses = map (prep_class thy) raw_supclasses;
    1.33      val sups = filter (is_some o lookup_class_data thy) supclasses
    1.34 -      |> Sign.certify_sort thy;
    1.35 -    val supsort = Sign.certify_sort thy supclasses;
    1.36 +      |> Sign.minimize_sort thy;
    1.37 +    val supsort = Sign.minimize_sort thy supclasses;
    1.38      val suplocales = map (Locale.Locale o #locale o the_class_data thy) sups;
    1.39      val supexpr = Locale.Merge (suplocales @ includes);
    1.40      val supparams = (map fst o Locale.parameters_of_expr thy)
    1.41 @@ -721,8 +719,7 @@
    1.42      val loc_expr = (Locale.Locale o #locale o the_class_data theory) superclass;
    1.43      fun prove_classrel (class, superclass) thy =
    1.44        let
    1.45 -        val classes = (Graph.all_succs o #classes o Sorts.rep_algebra
    1.46 -              o Sign.classes_of) thy [superclass]
    1.47 +        val classes = Sign.complete_sort thy [superclass]
    1.48            |> filter_out (fn class' => Sign.subsort thy ([class], [class']));
    1.49          fun instance_subclass (class1, class2) thy  =
    1.50            let
    1.51 @@ -731,7 +728,7 @@
    1.52              val intro = #intro (AxClass.get_definition thy class2)
    1.53                |> Drule.instantiate' [SOME (Thm.ctyp_of thy
    1.54                    (TVar ((AxClass.param_tyvarname, 0), [class1])))] [];
    1.55 -            val thm = 
    1.56 +            val thm =
    1.57                intro
    1.58                |> OF_LAST (interp OF ax)
    1.59                |> strip_all_ofclass thy (Sign.super_classes thy class2);
     2.1 --- a/src/Pure/Isar/code.ML	Wed Sep 26 20:27:58 2007 +0200
     2.2 +++ b/src/Pure/Isar/code.ML	Wed Sep 26 20:50:33 2007 +0200
     2.3 @@ -541,7 +541,7 @@
     2.4  
     2.5  fun weakest_constraints thy (class, tyco) =
     2.6    let
     2.7 -    val all_superclasses = class :: Graph.all_succs ((#classes o Sorts.rep_algebra o Sign.classes_of) thy) [class];
     2.8 +    val all_superclasses = Sign.complete_sort thy [class];
     2.9    in case inter_sorts thy (maps (fn class => specific_constraints thy (class, tyco)) all_superclasses)
    2.10     of SOME sorts => sorts
    2.11      | NONE => Sign.arity_sorts thy tyco [class]
    2.12 @@ -555,7 +555,7 @@
    2.13    in case inter_sorts thy (maps (fn class => specific_constraints thy (class, tyco)) inst_subclasses)
    2.14     of SOME sorts => sorts
    2.15      | NONE => replicate
    2.16 -        (Sign.arity_number thy tyco) (Sign.certify_sort thy (Sign.all_classes thy))
    2.17 +        (Sign.arity_number thy tyco) (Sign.minimize_sort thy (Sign.all_classes thy))
    2.18    end;
    2.19  
    2.20  fun gen_classop_typ constr thy class (c, tyco) = 
     3.1 --- a/src/Pure/axclass.ML	Wed Sep 26 20:27:58 2007 +0200
     3.2 +++ b/src/Pure/axclass.ML	Wed Sep 26 20:50:33 2007 +0200
     3.3 @@ -225,7 +225,7 @@
     3.4      fun err () = raise THM ("add_arity: malformed type arity", 0, [th]);
     3.5      val prop = Thm.plain_prop_of (Thm.transfer thy th);
     3.6      val (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
     3.7 -    val _ = if map (Sign.certify_sort thy) Ss = Ss then () else err ();
     3.8 +    val _ = map (Sign.certify_sort thy) Ss = Ss orelse err ();
     3.9    in
    3.10      thy
    3.11      |> Sign.primitive_arity (t, Ss, [c])
    3.12 @@ -291,7 +291,7 @@
    3.13  
    3.14      val bconst = Logic.const_of_class bclass;
    3.15      val class = Sign.full_name thy bclass;
    3.16 -    val super = Sign.certify_sort thy raw_super;
    3.17 +    val super = Sign.minimize_sort thy (Sign.certify_sort thy raw_super);
    3.18  
    3.19      fun prep_axiom t =
    3.20        (case Term.add_tfrees t [] of
    3.21 @@ -420,7 +420,7 @@
    3.22  fun ax_class prep_class prep_classrel (bclass, raw_super) thy =
    3.23    let
    3.24      val class = Sign.full_name thy bclass;
    3.25 -    val super = map (prep_class thy) raw_super |> Sign.certify_sort thy;
    3.26 +    val super = map (prep_class thy) raw_super |> Sign.minimize_sort thy;
    3.27    in
    3.28      thy
    3.29      |> Sign.primitive_class (bclass, super)