empty class specifcations observe default sort
authorhaftmann
Wed Apr 28 13:29:39 2010 +0200 (2010-04-28 ago)
changeset 36460c643b23e8592
parent 36446 06081e4921d6
child 36461 e741ba542b61
empty class specifcations observe default sort
NEWS
src/Pure/Isar/class.ML
     1.1 --- a/NEWS	Wed Apr 28 08:25:02 2010 +0200
     1.2 +++ b/NEWS	Wed Apr 28 13:29:39 2010 +0200
     1.3 @@ -84,6 +84,8 @@
     1.4  
     1.5  *** Pure ***
     1.6  
     1.7 +* Empty class specifications observe default sort.  INCOMPATIBILITY.
     1.8 +
     1.9  * Old 'axclass' has been discontinued.  Use 'class' instead.  INCOMPATIBILITY.
    1.10  
    1.11  * Code generator: simple concept for abstract datatypes obeying invariants.
     2.1 --- a/src/Pure/Isar/class.ML	Wed Apr 28 08:25:02 2010 +0200
     2.2 +++ b/src/Pure/Isar/class.ML	Wed Apr 28 13:29:39 2010 +0200
     2.3 @@ -100,10 +100,14 @@
     2.4  
     2.5  (* reading and processing class specifications *)
     2.6  
     2.7 -fun prep_class_elems prep_decl thy sups proto_base_sort raw_elems =
     2.8 +fun prep_class_elems prep_decl thy sups raw_elems =
     2.9    let
    2.10  
    2.11      (* user space type system: only permits 'a type variable, improves towards 'a *)
    2.12 +    val algebra = Sign.classes_of thy;
    2.13 +    val inter_sort = curry (Sorts.inter_sort algebra);
    2.14 +    val proto_base_sort = if null sups then Sign.defaultS thy
    2.15 +      else fold inter_sort (map (base_sort thy) sups) [];
    2.16      val base_constraints = (map o apsnd)
    2.17        (map_type_tfree (K (TVar ((Name.aT, 0), proto_base_sort))) o fst o snd)
    2.18          (these_operations thy sups);
    2.19 @@ -111,17 +115,17 @@
    2.20            if v = Name.aT then T
    2.21            else error ("No type variable other than " ^ Name.aT ^ " allowed in class specification")
    2.22        | T => T);
    2.23 -    fun singleton_fixate thy algebra Ts =
    2.24 +    fun singleton_fixate Ts =
    2.25        let
    2.26          fun extract f = (fold o fold_atyps) f Ts [];
    2.27          val tfrees = extract
    2.28            (fn TFree (v, sort) => insert (op =) (v, sort) | _ => I);
    2.29          val inferred_sort = extract
    2.30 -          (fn TVar (_, sort) => curry (Sorts.inter_sort algebra) sort | _ => I);
    2.31 +          (fn TVar (_, sort) => inter_sort sort | _ => I);
    2.32          val fixate_sort = if null tfrees then inferred_sort
    2.33            else case tfrees
    2.34             of [(_, a_sort)] => if Sorts.sort_le algebra (a_sort, inferred_sort)
    2.35 -                then Sorts.inter_sort algebra (a_sort, inferred_sort)
    2.36 +                then inter_sort a_sort inferred_sort
    2.37                  else error ("Type inference imposes additional sort constraint "
    2.38                    ^ Syntax.string_of_sort_global thy inferred_sort
    2.39                    ^ " of type parameter " ^ Name.aT ^ " of sort "
    2.40 @@ -136,7 +140,7 @@
    2.41      val init_class_body = fold (ProofContext.add_const_constraint o apsnd SOME) base_constraints
    2.42        #> redeclare_operations thy sups
    2.43        #> add_typ_check 10 "reject_bcd_etc" reject_bcd_etc
    2.44 -      #> add_typ_check ~10 "singleton_fixate" (singleton_fixate thy (Sign.classes_of thy));
    2.45 +      #> add_typ_check ~10 "singleton_fixate" singleton_fixate;
    2.46      val raw_supexpr = (map (fn sup => (sup, (("", false),
    2.47        Expression.Positional []))) sups, []);
    2.48      val ((raw_supparams, _, inferred_elems), _) = ProofContext.init thy
    2.49 @@ -183,11 +187,10 @@
    2.50        then error ("Duplicate parameter(s) in superclasses: "
    2.51          ^ (commas o map quote o duplicates (op =)) raw_supparam_names)
    2.52        else ();
    2.53 -    val given_basesort = fold inter_sort (map (base_sort thy) sups) [];
    2.54  
    2.55      (* infer types and base sort *)
    2.56      val (base_sort, supparam_names, supexpr, inferred_elems) =
    2.57 -      prep_class_elems thy sups given_basesort raw_elems;
    2.58 +      prep_class_elems thy sups raw_elems;
    2.59      val sup_sort = inter_sort base_sort sups;
    2.60  
    2.61      (* process elements as class specification *)