src/Pure/Isar/class_declaration.ML
changeset 45432 12cc89f1eb0c
parent 45431 924c2f6dcd05
child 45433 4283f3a57cf5
     1.1 --- a/src/Pure/Isar/class_declaration.ML	Wed Nov 09 21:44:06 2011 +0100
     1.2 +++ b/src/Pure/Isar/class_declaration.ML	Wed Nov 09 22:43:14 2011 +0100
     1.3 @@ -116,38 +116,41 @@
     1.4      val base_constraints = (map o apsnd)
     1.5        (map_type_tfree (K (TVar ((Name.aT, 0), proto_base_sort))) o fst o snd)
     1.6          (Class.these_operations thy sups);
     1.7 -    val reject_bcd_etc = (map o map_atyps) (fn T as TFree (a, _) =>
     1.8 -          if a = Name.aT then T
     1.9 -          else error ("No type variable other than " ^ Name.aT ^ " allowed in class specification")
    1.10 -      | T => T);
    1.11 +    val reject_other =
    1.12 +      (tap o exists o Term.exists_subtype)
    1.13 +        (fn TFree (a, _) =>
    1.14 +          a <> Name.aT andalso
    1.15 +            error ("No type variable other than " ^ Name.aT ^ " allowed in class specification")
    1.16 +        | _ => false);
    1.17      fun singleton_fixate Ts =
    1.18        let
    1.19 -        fun extract f = (fold o fold_atyps) f Ts [];
    1.20 -        val tfrees = extract (fn TFree (v, sort) => insert (op =) (v, sort) | _ => I);
    1.21 -        val inferred_sort = extract (fn TVar (_, sort) => inter_sort sort | _ => I);
    1.22 +        val tfrees = fold Term.add_tfreesT Ts [];
    1.23 +        val inferred_sort = (fold o Term.fold_atyps) (fn TVar (_, S) => inter_sort S | _ => I) Ts [];
    1.24          val fixate_sort =
    1.25 -          if null tfrees then inferred_sort
    1.26 -          else
    1.27 -            (case tfrees of
    1.28 -              [(_, a_sort)] =>
    1.29 -                if Sorts.sort_le algebra (a_sort, inferred_sort) then
    1.30 -                  inter_sort a_sort inferred_sort
    1.31 -                else
    1.32 -                  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 -      in (map o map_atyps) (K (TFree (Name.aT, fixate_sort))) Ts end;
    1.38 +          (case tfrees of
    1.39 +            [] => inferred_sort
    1.40 +          | [(_, S)] =>
    1.41 +              if Sorts.sort_le algebra (S, inferred_sort) then S
    1.42 +              else
    1.43 +                error ("Type inference imposes additional sort constraint " ^
    1.44 +                  Syntax.string_of_sort_global thy inferred_sort ^
    1.45 +                  " of type parameter " ^ Name.aT ^ " of sort " ^
    1.46 +                  Syntax.string_of_sort_global thy S)
    1.47 +          | _ => error "Multiple type variables in class specification");
    1.48 +        val fixateT = TFree (Name.aT, fixate_sort);
    1.49 +      in
    1.50 +        (map o map_atyps)
    1.51 +          (fn T as TVar (xi, _) => if Type_Infer.is_param xi then fixateT else T | T => T) Ts
    1.52 +      end;
    1.53      fun after_infer_fixate Ts =
    1.54        let
    1.55 -        val S' =
    1.56 +        val fixate_sort =
    1.57            (fold o fold_atyps)
    1.58              (fn TVar (xi, S) => if Type_Infer.is_param xi then inter_sort S else I | _ => I) Ts [];
    1.59        in
    1.60          (map o map_atyps)
    1.61            (fn T as TVar (xi, _) =>
    1.62 -              if Type_Infer.is_param xi then Type_Infer.param 0 (Name.aT, S') else T
    1.63 +              if Type_Infer.is_param xi then Type_Infer.param 0 (Name.aT, fixate_sort) else T
    1.64              | T => T) Ts
    1.65        end;
    1.66  
    1.67 @@ -157,7 +160,7 @@
    1.68      val init_class_body =
    1.69        fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints
    1.70        #> Class.redeclare_operations thy sups
    1.71 -      #> Context.proof_map (Syntax_Phases.typ_check 10 "reject_bcd_etc" (K reject_bcd_etc))
    1.72 +      #> Context.proof_map (Syntax_Phases.typ_check 10 "reject_other" (K reject_other))
    1.73        #> Context.proof_map (Syntax_Phases.typ_check ~10 "singleton_fixate" (K singleton_fixate));
    1.74      val ((raw_supparams, _, raw_inferred_elems), _) =
    1.75        Proof_Context.init_global thy