src/Pure/Isar/class_declaration.ML
changeset 45432 12cc89f1eb0c
parent 45431 924c2f6dcd05
child 45433 4283f3a57cf5
equal deleted inserted replaced
45431:924c2f6dcd05 45432:12cc89f1eb0c
   114       if null sups then Sign.defaultS thy
   114       if null sups then Sign.defaultS thy
   115       else fold inter_sort (map (Class.base_sort thy) sups) [];
   115       else fold inter_sort (map (Class.base_sort thy) sups) [];
   116     val base_constraints = (map o apsnd)
   116     val base_constraints = (map o apsnd)
   117       (map_type_tfree (K (TVar ((Name.aT, 0), proto_base_sort))) o fst o snd)
   117       (map_type_tfree (K (TVar ((Name.aT, 0), proto_base_sort))) o fst o snd)
   118         (Class.these_operations thy sups);
   118         (Class.these_operations thy sups);
   119     val reject_bcd_etc = (map o map_atyps) (fn T as TFree (a, _) =>
   119     val reject_other =
   120           if a = Name.aT then T
   120       (tap o exists o Term.exists_subtype)
   121           else error ("No type variable other than " ^ Name.aT ^ " allowed in class specification")
   121         (fn TFree (a, _) =>
   122       | T => T);
   122           a <> Name.aT andalso
       
   123             error ("No type variable other than " ^ Name.aT ^ " allowed in class specification")
       
   124         | _ => false);
   123     fun singleton_fixate Ts =
   125     fun singleton_fixate Ts =
   124       let
   126       let
   125         fun extract f = (fold o fold_atyps) f Ts [];
   127         val tfrees = fold Term.add_tfreesT Ts [];
   126         val tfrees = extract (fn TFree (v, sort) => insert (op =) (v, sort) | _ => I);
   128         val inferred_sort = (fold o Term.fold_atyps) (fn TVar (_, S) => inter_sort S | _ => I) Ts [];
   127         val inferred_sort = extract (fn TVar (_, sort) => inter_sort sort | _ => I);
       
   128         val fixate_sort =
   129         val fixate_sort =
   129           if null tfrees then inferred_sort
   130           (case tfrees of
   130           else
   131             [] => inferred_sort
   131             (case tfrees of
   132           | [(_, S)] =>
   132               [(_, a_sort)] =>
   133               if Sorts.sort_le algebra (S, inferred_sort) then S
   133                 if Sorts.sort_le algebra (a_sort, inferred_sort) then
   134               else
   134                   inter_sort a_sort inferred_sort
   135                 error ("Type inference imposes additional sort constraint " ^
   135                 else
   136                   Syntax.string_of_sort_global thy inferred_sort ^
   136                   error ("Type inference imposes additional sort constraint " ^
   137                   " of type parameter " ^ Name.aT ^ " of sort " ^
   137                     Syntax.string_of_sort_global thy inferred_sort ^
   138                   Syntax.string_of_sort_global thy S)
   138                     " of type parameter " ^ Name.aT ^ " of sort " ^
   139           | _ => error "Multiple type variables in class specification");
   139                     Syntax.string_of_sort_global thy a_sort)
   140         val fixateT = TFree (Name.aT, fixate_sort);
   140             | _ => error "Multiple type variables in class specification");
   141       in
   141       in (map o map_atyps) (K (TFree (Name.aT, fixate_sort))) Ts end;
   142         (map o map_atyps)
       
   143           (fn T as TVar (xi, _) => if Type_Infer.is_param xi then fixateT else T | T => T) Ts
       
   144       end;
   142     fun after_infer_fixate Ts =
   145     fun after_infer_fixate Ts =
   143       let
   146       let
   144         val S' =
   147         val fixate_sort =
   145           (fold o fold_atyps)
   148           (fold o fold_atyps)
   146             (fn TVar (xi, S) => if Type_Infer.is_param xi then inter_sort S else I | _ => I) Ts [];
   149             (fn TVar (xi, S) => if Type_Infer.is_param xi then inter_sort S else I | _ => I) Ts [];
   147       in
   150       in
   148         (map o map_atyps)
   151         (map o map_atyps)
   149           (fn T as TVar (xi, _) =>
   152           (fn T as TVar (xi, _) =>
   150               if Type_Infer.is_param xi then Type_Infer.param 0 (Name.aT, S') else T
   153               if Type_Infer.is_param xi then Type_Infer.param 0 (Name.aT, fixate_sort) else T
   151             | T => T) Ts
   154             | T => T) Ts
   152       end;
   155       end;
   153 
   156 
   154     (* preprocessing elements, retrieving base sort from type-checked elements *)
   157     (* preprocessing elements, retrieving base sort from type-checked elements *)
   155     val raw_supexpr =
   158     val raw_supexpr =
   156       (map (fn sup => (sup, (("", false), Expression.Positional []))) sups, []);
   159       (map (fn sup => (sup, (("", false), Expression.Positional []))) sups, []);
   157     val init_class_body =
   160     val init_class_body =
   158       fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints
   161       fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints
   159       #> Class.redeclare_operations thy sups
   162       #> Class.redeclare_operations thy sups
   160       #> Context.proof_map (Syntax_Phases.typ_check 10 "reject_bcd_etc" (K reject_bcd_etc))
   163       #> Context.proof_map (Syntax_Phases.typ_check 10 "reject_other" (K reject_other))
   161       #> Context.proof_map (Syntax_Phases.typ_check ~10 "singleton_fixate" (K singleton_fixate));
   164       #> Context.proof_map (Syntax_Phases.typ_check ~10 "singleton_fixate" (K singleton_fixate));
   162     val ((raw_supparams, _, raw_inferred_elems), _) =
   165     val ((raw_supparams, _, raw_inferred_elems), _) =
   163       Proof_Context.init_global thy
   166       Proof_Context.init_global thy
   164       |> Context.proof_map (Syntax_Phases.typ_check 5 "after_infer_fixate" (K after_infer_fixate))
   167       |> Context.proof_map (Syntax_Phases.typ_check 5 "after_infer_fixate" (K after_infer_fixate))
   165       |> prep_decl raw_supexpr init_class_body raw_elems;
   168       |> prep_decl raw_supexpr init_class_body raw_elems;