avoid separate typ_check phases, integrate into main term_check 0 instead (cf. its Syntax.check_typs in Type_Infer_Context.prepare);
authorwenzelm
Wed Nov 09 23:16:47 2011 +0100 (2011-11-09)
changeset 454334283f3a57cf5
parent 45432 12cc89f1eb0c
child 45434 f28329338d30
avoid separate typ_check phases, integrate into main term_check 0 instead (cf. its Syntax.check_typs in Type_Infer_Context.prepare);
src/Pure/Isar/class_declaration.ML
     1.1 --- a/src/Pure/Isar/class_declaration.ML	Wed Nov 09 22:43:14 2011 +0100
     1.2 +++ b/src/Pure/Isar/class_declaration.ML	Wed Nov 09 23:16:47 2011 +0100
     1.3 @@ -116,21 +116,18 @@
     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_other =
     1.8 -      (tap o exists o Term.exists_subtype)
     1.9 -        (fn TFree (a, _) =>
    1.10 -          a <> Name.aT andalso
    1.11 -            error ("No type variable other than " ^ Name.aT ^ " allowed in class specification")
    1.12 -        | _ => false);
    1.13 -    fun singleton_fixate Ts =
    1.14 +    fun singleton_fixate tms =
    1.15        let
    1.16 -        val tfrees = fold Term.add_tfreesT Ts [];
    1.17 -        val inferred_sort = (fold o Term.fold_atyps) (fn TVar (_, S) => inter_sort S | _ => I) Ts [];
    1.18 +        val tfrees = fold Term.add_tfrees tms [];
    1.19 +        val inferred_sort =
    1.20 +          (fold o fold_types o fold_atyps) (fn TVar (_, S) => inter_sort S | _ => I) tms [];
    1.21          val fixate_sort =
    1.22            (case tfrees of
    1.23              [] => inferred_sort
    1.24 -          | [(_, S)] =>
    1.25 -              if Sorts.sort_le algebra (S, inferred_sort) then S
    1.26 +          | [(a, S)] =>
    1.27 +              if a <> Name.aT then
    1.28 +                error ("No type variable other than " ^ Name.aT ^ " allowed in class specification")
    1.29 +              else if Sorts.sort_le algebra (S, inferred_sort) then S
    1.30                else
    1.31                  error ("Type inference imposes additional sort constraint " ^
    1.32                    Syntax.string_of_sort_global thy inferred_sort ^
    1.33 @@ -139,19 +136,19 @@
    1.34            | _ => error "Multiple type variables in class specification");
    1.35          val fixateT = TFree (Name.aT, fixate_sort);
    1.36        in
    1.37 -        (map o map_atyps)
    1.38 -          (fn T as TVar (xi, _) => if Type_Infer.is_param xi then fixateT else T | T => T) Ts
    1.39 +        (map o map_types o map_atyps)
    1.40 +          (fn T as TVar (xi, _) => if Type_Infer.is_param xi then fixateT else T | T => T) tms
    1.41        end;
    1.42 -    fun after_infer_fixate Ts =
    1.43 +    fun after_infer_fixate tms =
    1.44        let
    1.45          val fixate_sort =
    1.46 -          (fold o fold_atyps)
    1.47 -            (fn TVar (xi, S) => if Type_Infer.is_param xi then inter_sort S else I | _ => I) Ts [];
    1.48 +          (fold o fold_types o fold_atyps)
    1.49 +            (fn TVar (xi, S) => if Type_Infer.is_param xi then inter_sort S else I | _ => I) tms [];
    1.50        in
    1.51 -        (map o map_atyps)
    1.52 +        (map o map_types o map_atyps)
    1.53            (fn T as TVar (xi, _) =>
    1.54                if Type_Infer.is_param xi then Type_Infer.param 0 (Name.aT, fixate_sort) else T
    1.55 -            | T => T) Ts
    1.56 +            | T => T) tms
    1.57        end;
    1.58  
    1.59      (* preprocessing elements, retrieving base sort from type-checked elements *)
    1.60 @@ -160,11 +157,10 @@
    1.61      val init_class_body =
    1.62        fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints
    1.63        #> Class.redeclare_operations thy sups
    1.64 -      #> Context.proof_map (Syntax_Phases.typ_check 10 "reject_other" (K reject_other))
    1.65 -      #> Context.proof_map (Syntax_Phases.typ_check ~10 "singleton_fixate" (K singleton_fixate));
    1.66 +      #> Context.proof_map (Syntax_Phases.term_check 0 "singleton_fixate" (K singleton_fixate));
    1.67      val ((raw_supparams, _, raw_inferred_elems), _) =
    1.68        Proof_Context.init_global thy
    1.69 -      |> Context.proof_map (Syntax_Phases.typ_check 5 "after_infer_fixate" (K after_infer_fixate))
    1.70 +      |> Context.proof_map (Syntax_Phases.term_check 0 "after_infer_fixate" (K after_infer_fixate))
    1.71        |> prep_decl raw_supexpr init_class_body raw_elems;
    1.72      fun filter_element (Element.Fixes []) = NONE
    1.73        | filter_element (e as Element.Fixes _) = SOME e