src/Pure/Isar/class.ML
changeset 36460 c643b23e8592
parent 35845 e5980f0ad025
child 36464 b789c1731fb7
     1.1 --- a/src/Pure/Isar/class.ML	Wed Apr 28 08:25:02 2010 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Wed Apr 28 13:29:39 2010 +0200
     1.3 @@ -100,10 +100,14 @@
     1.4  
     1.5  (* reading and processing class specifications *)
     1.6  
     1.7 -fun prep_class_elems prep_decl thy sups proto_base_sort raw_elems =
     1.8 +fun prep_class_elems prep_decl thy sups raw_elems =
     1.9    let
    1.10  
    1.11      (* user space type system: only permits 'a type variable, improves towards 'a *)
    1.12 +    val algebra = Sign.classes_of thy;
    1.13 +    val inter_sort = curry (Sorts.inter_sort algebra);
    1.14 +    val proto_base_sort = if null sups then Sign.defaultS thy
    1.15 +      else fold inter_sort (map (base_sort thy) sups) [];
    1.16      val base_constraints = (map o apsnd)
    1.17        (map_type_tfree (K (TVar ((Name.aT, 0), proto_base_sort))) o fst o snd)
    1.18          (these_operations thy sups);
    1.19 @@ -111,17 +115,17 @@
    1.20            if v = Name.aT then T
    1.21            else error ("No type variable other than " ^ Name.aT ^ " allowed in class specification")
    1.22        | T => T);
    1.23 -    fun singleton_fixate thy algebra Ts =
    1.24 +    fun singleton_fixate Ts =
    1.25        let
    1.26          fun extract f = (fold o fold_atyps) f Ts [];
    1.27          val tfrees = extract
    1.28            (fn TFree (v, sort) => insert (op =) (v, sort) | _ => I);
    1.29          val inferred_sort = extract
    1.30 -          (fn TVar (_, sort) => curry (Sorts.inter_sort algebra) sort | _ => I);
    1.31 +          (fn TVar (_, sort) => inter_sort sort | _ => I);
    1.32          val fixate_sort = if null tfrees then inferred_sort
    1.33            else case tfrees
    1.34             of [(_, a_sort)] => if Sorts.sort_le algebra (a_sort, inferred_sort)
    1.35 -                then Sorts.inter_sort algebra (a_sort, inferred_sort)
    1.36 +                then inter_sort a_sort inferred_sort
    1.37                  else error ("Type inference imposes additional sort constraint "
    1.38                    ^ Syntax.string_of_sort_global thy inferred_sort
    1.39                    ^ " of type parameter " ^ Name.aT ^ " of sort "
    1.40 @@ -136,7 +140,7 @@
    1.41      val init_class_body = fold (ProofContext.add_const_constraint o apsnd SOME) base_constraints
    1.42        #> redeclare_operations thy sups
    1.43        #> add_typ_check 10 "reject_bcd_etc" reject_bcd_etc
    1.44 -      #> add_typ_check ~10 "singleton_fixate" (singleton_fixate thy (Sign.classes_of thy));
    1.45 +      #> add_typ_check ~10 "singleton_fixate" singleton_fixate;
    1.46      val raw_supexpr = (map (fn sup => (sup, (("", false),
    1.47        Expression.Positional []))) sups, []);
    1.48      val ((raw_supparams, _, inferred_elems), _) = ProofContext.init thy
    1.49 @@ -183,11 +187,10 @@
    1.50        then error ("Duplicate parameter(s) in superclasses: "
    1.51          ^ (commas o map quote o duplicates (op =)) raw_supparam_names)
    1.52        else ();
    1.53 -    val given_basesort = fold inter_sort (map (base_sort thy) sups) [];
    1.54  
    1.55      (* infer types and base sort *)
    1.56      val (base_sort, supparam_names, supexpr, inferred_elems) =
    1.57 -      prep_class_elems thy sups given_basesort raw_elems;
    1.58 +      prep_class_elems thy sups raw_elems;
    1.59      val sup_sort = inter_sort base_sort sups;
    1.60  
    1.61      (* process elements as class specification *)