src/Pure/Isar/class_declaration.ML
changeset 45421 2bef6da4a6a6
parent 42494 eef1a23c9077
child 45429 fd58cbf8cae3
     1.1 --- a/src/Pure/Isar/class_declaration.ML	Wed Nov 09 11:35:09 2011 +0100
     1.2 +++ b/src/Pure/Isar/class_declaration.ML	Wed Nov 09 14:15:44 2011 +0100
     1.3 @@ -104,7 +104,8 @@
     1.4      (* user space type system: only permits 'a type variable, improves towards 'a *)
     1.5      val algebra = Sign.classes_of thy;
     1.6      val inter_sort = curry (Sorts.inter_sort algebra);
     1.7 -    val proto_base_sort = if null sups then Sign.defaultS thy
     1.8 +    val proto_base_sort =
     1.9 +      if null sups then Sign.defaultS thy
    1.10        else fold inter_sort (map (Class.base_sort thy) sups) [];
    1.11      val base_constraints = (map o apsnd)
    1.12        (map_type_tfree (K (TVar ((Name.aT, 0), proto_base_sort))) o fst o snd)
    1.13 @@ -116,19 +117,19 @@
    1.14      fun singleton_fixate Ts =
    1.15        let
    1.16          fun extract f = (fold o fold_atyps) f Ts [];
    1.17 -        val tfrees = extract
    1.18 -          (fn TFree (v, sort) => insert (op =) (v, sort) | _ => I);
    1.19 -        val inferred_sort = extract
    1.20 -          (fn TVar (_, sort) => inter_sort sort | _ => I);
    1.21 -        val fixate_sort = if null tfrees then inferred_sort
    1.22 -          else case tfrees
    1.23 -           of [(_, a_sort)] => if Sorts.sort_le algebra (a_sort, inferred_sort)
    1.24 +        val tfrees = extract (fn TFree (v, sort) => insert (op =) (v, sort) | _ => I);
    1.25 +        val inferred_sort = extract (fn TVar (_, sort) => inter_sort sort | _ => I);
    1.26 +        val fixate_sort =
    1.27 +          if null tfrees then inferred_sort
    1.28 +          else
    1.29 +            (case tfrees of
    1.30 +              [(_, a_sort)] => if Sorts.sort_le algebra (a_sort, inferred_sort)
    1.31                  then inter_sort a_sort inferred_sort
    1.32                  else error ("Type inference imposes additional sort constraint "
    1.33                    ^ Syntax.string_of_sort_global thy inferred_sort
    1.34                    ^ " of type parameter " ^ Name.aT ^ " of sort "
    1.35                    ^ Syntax.string_of_sort_global thy a_sort)
    1.36 -            | _ => error "Multiple type variables in class specification";
    1.37 +            | _ => error "Multiple type variables in class specification");
    1.38        in (map o map_atyps) (K (TFree (Name.aT, fixate_sort))) Ts end;
    1.39      fun after_infer_fixate Ts =
    1.40        let
    1.41 @@ -158,18 +159,22 @@
    1.42        | filter_element (e as Element.Constrains _) = SOME e
    1.43        | filter_element (Element.Assumes []) = NONE
    1.44        | filter_element (e as Element.Assumes _) = SOME e
    1.45 -      | filter_element (Element.Defines _) = error ("\"defines\" element not allowed in class specification.")
    1.46 -      | filter_element (Element.Notes _) = error ("\"notes\" element not allowed in class specification.");
    1.47 +      | filter_element (Element.Defines _) =
    1.48 +          error ("\"defines\" element not allowed in class specification.")
    1.49 +      | filter_element (Element.Notes _) =
    1.50 +          error ("\"notes\" element not allowed in class specification.");
    1.51      val inferred_elems = map_filter filter_element raw_inferred_elems;
    1.52      fun fold_element_types f (Element.Fixes fxs) = fold (fn (_, SOME T, _) => f T) fxs
    1.53        | fold_element_types f (Element.Constrains cnstrs) = fold (f o snd) cnstrs
    1.54        | fold_element_types f (Element.Assumes assms) = fold (fold (fn (t, ts) =>
    1.55            fold_types f t #> (fold o fold_types) f ts) o snd) assms;
    1.56 -    val base_sort = if null inferred_elems then proto_base_sort else
    1.57 -      case (fold o fold_element_types) Term.add_tfreesT inferred_elems []
    1.58 -       of [] => error "No type variable in class specification"
    1.59 +    val base_sort =
    1.60 +      if null inferred_elems then proto_base_sort
    1.61 +      else
    1.62 +        (case (fold o fold_element_types) Term.add_tfreesT inferred_elems [] of
    1.63 +          [] => error "No type variable in class specification"
    1.64          | [(_, sort)] => sort
    1.65 -        | _ => error "Multiple type variables in class specification";
    1.66 +        | _ => error "Multiple type variables in class specification");
    1.67      val supparams = map (fn ((c, T), _) =>
    1.68        (c, map_atyps (K (TFree (Name.aT, base_sort))) T)) raw_supparams;
    1.69      val supparam_names = map fst supparams;
    1.70 @@ -317,6 +322,7 @@
    1.71  end; (*local*)
    1.72  
    1.73  
    1.74 +
    1.75  (** subclass relations **)
    1.76  
    1.77  local