src/Pure/Isar/class.ML
changeset 26329 3e58e4c67a2a
parent 26259 d30f4a509361
child 26353 537ff6997149
     1.1 --- a/src/Pure/Isar/class.ML	Wed Mar 19 07:20:32 2008 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Wed Mar 19 07:20:33 2008 +0100
     1.3 @@ -666,17 +666,6 @@
     1.4      val thy = ProofContext.theory_of ctxt;
     1.5      fun subst_class_typ sort = map_atyps
     1.6        (fn TFree _ => TVar ((Name.aT, 0), sort) | ty' => ty');
     1.7 -    val operations = these_operations thy sort;
     1.8 -    val global_constraints = (*map_filter (fn (c, (class, (ty, _))) =>
     1.9 -      if exists (fn ((c', _), _) => c = c') params
    1.10 -        then SOME (c, subst_class_typ [class] ty)
    1.11 -        else NONE) operations;*)[];
    1.12 -          (*| NONE => (case map_filter
    1.13 -               (fn ((c', _), (_, ty')) => if c' = c then SOME ty' else NONE) params
    1.14 -             of [ty'] => (case Sign.const_typargs thy (c, ty)
    1.15 -                 of [TVar (vi, _)] => if TypeInfer.is_param vi then SOME (ty, ty') else NONE
    1.16 -                  | _ => NONE)
    1.17 -              | _ => NONE*);
    1.18      fun subst (c, ty) = case AxClass.inst_tyco_of thy (c, ty)
    1.19           of SOME tyco => (case AList.lookup (op =) params (c, tyco)
    1.20               of SOME (v_ty as (_, ty)) => SOME (ty, Free v_ty)
    1.21 @@ -688,7 +677,7 @@
    1.22      ctxt
    1.23      |> Overloading.map_improvable_syntax
    1.24           (fn (((local_constraints, _), ((improve, _), _)), _) =>
    1.25 -            (((local_constraints, global_constraints), ((improve, subst), unchecks)), false))
    1.26 +            (((local_constraints, []), ((improve, subst), unchecks)), false))
    1.27    end;
    1.28  
    1.29  
    1.30 @@ -721,23 +710,43 @@
    1.31      fun get_param tyco (param, (c, ty)) = if can (AxClass.param_of_inst thy) (c, tyco)
    1.32        then NONE else SOME ((c, tyco),
    1.33          (param ^ "_" ^ type_name tyco, map_atyps (K (Type (tyco, map TFree vs))) ty));
    1.34 -    val params = map_product get_param tycos (these_params thy sort) |> map_filter I;
    1.35 -    val operations = these_operations thy sort;
    1.36 -    val local_constraints = (map o apsnd) (subst_class_typ [] o fst o snd) operations;
    1.37 -    fun improve (c, ty) = case AxClass.inst_tyco_of thy (c, ty)
    1.38 -     of SOME tyco => (case AList.lookup (op =) params (c, tyco)
    1.39 +    val class_of = fst o the o AList.lookup (op =) (these_operations thy sort);
    1.40 +    val params = these_params thy sort;
    1.41 +    val inst_params = map_product get_param tycos (these_params thy sort) |> map_filter I;
    1.42 +    val local_constraints = map (apsnd (subst_class_typ []) o snd) params;
    1.43 +    val pseudo_constraints = map (fn (_, (c, _)) => (c, class_of c)) params;
    1.44 +    val typ_of_sort = Type.typ_of_sort (Sign.classes_of thy);
    1.45 +    val typarg = the_single o Sign.const_typargs thy;
    1.46 +    val pp = Sign.pp thy;
    1.47 +    fun constrain_class (c, ty) class =
    1.48 +      let
    1.49 +        val ty' = typarg (c, ty);
    1.50 +        val tyenv = typ_of_sort ty' [class] Vartab.empty
    1.51 +          handle Sorts.CLASS_ERROR e => Sorts.class_error pp e;
    1.52 +      in
    1.53 +        map_atyps (fn TVar (vi, _) => TVar (vi, the (Vartab.lookup tyenv vi))
    1.54 +          | ty => ty) ty
    1.55 +      end;
    1.56 +    fun improve_param (c, ty) = case AxClass.inst_tyco_of thy (c, ty)
    1.57 +     of SOME tyco => (case AList.lookup (op =) inst_params (c, tyco)
    1.58           of SOME (_, ty') => SOME (ty, ty')
    1.59            | NONE => NONE)
    1.60        | NONE => NONE;
    1.61 +    fun improve (c, ty) = case improve_param (c, ty)
    1.62 +     of SOME ty_ty' => SOME ty_ty'
    1.63 +      | NONE => (case AList.lookup (op =) pseudo_constraints c
    1.64 +         of SOME class =>
    1.65 +              SOME (ty, constrain_class (c, ty) class)
    1.66 +          | NONE => NONE);
    1.67    in
    1.68      thy
    1.69      |> ProofContext.init
    1.70 -    |> Instantiation.put (mk_instantiation ((tycos, vs, sort), params))
    1.71 +    |> Instantiation.put (mk_instantiation ((tycos, vs, sort), inst_params))
    1.72      |> fold (Variable.declare_term o Logic.mk_type o TFree) vs
    1.73 -    |> fold (Variable.declare_names o Free o snd) params
    1.74 +    |> fold (Variable.declare_names o Free o snd) inst_params
    1.75      |> (Overloading.map_improvable_syntax o apfst)
    1.76 -         (fn ((_, global_constraints), ((_, subst), unchecks)) =>
    1.77 -            ((local_constraints, global_constraints), ((improve, subst), unchecks)))
    1.78 +         (fn ((_, _), ((_, subst), unchecks)) =>
    1.79 +            ((local_constraints, []), ((improve, K NONE), [])))
    1.80      |> Overloading.add_improvable_syntax
    1.81      |> synchronize_inst_syntax
    1.82    end;