src/Pure/Isar/class.ML
changeset 26259 d30f4a509361
parent 26247 b6608fbeaae1
child 26329 3e58e4c67a2a
     1.1 --- a/src/Pure/Isar/class.ML	Wed Mar 12 08:45:51 2008 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Wed Mar 12 08:47:35 2008 +0100
     1.3 @@ -40,6 +40,7 @@
     1.4    val instantiation_param: local_theory -> string -> string option
     1.5    val confirm_declaration: string -> local_theory -> local_theory
     1.6    val pretty_instantiation: local_theory -> Pretty.T
     1.7 +  val type_name: string -> string
     1.8  
     1.9    (*old axclass layer*)
    1.10    val axclass_cmd: bstring * xstring list
    1.11 @@ -433,9 +434,9 @@
    1.12    in
    1.13      ctxt
    1.14      |> fold declare_const local_constraints
    1.15 -    |> fold (ProofContext.add_const_constraint o apsnd SOME) local_constraints
    1.16      |> Overloading.map_improvable_syntax (K (((local_constraints, global_constraints),
    1.17          ((improve, subst), unchecks)), false))
    1.18 +    |> Overloading.set_local_constraints
    1.19    end;
    1.20  
    1.21  fun refresh_syntax class ctxt =
    1.22 @@ -661,22 +662,15 @@
    1.23  
    1.24  fun synchronize_inst_syntax ctxt =
    1.25    let
    1.26 -    val Instantiation { arities = (_, _, sorts), params = params } = Instantiation.get ctxt;
    1.27 +    val Instantiation { arities = (_, _, sort), params = params } = Instantiation.get ctxt;
    1.28      val thy = ProofContext.theory_of ctxt;
    1.29 -    val operations = these_operations thy sorts;
    1.30      fun subst_class_typ sort = map_atyps
    1.31        (fn TFree _ => TVar ((Name.aT, 0), sort) | ty' => ty');
    1.32 -    val local_constraints =
    1.33 -      (map o apsnd) (subst_class_typ [] o fst o snd) operations;
    1.34 -    val global_constraints = map_filter (fn (c, (class, (ty, _))) =>
    1.35 +    val operations = these_operations thy sort;
    1.36 +    val global_constraints = (*map_filter (fn (c, (class, (ty, _))) =>
    1.37        if exists (fn ((c', _), _) => c = c') params
    1.38          then SOME (c, subst_class_typ [class] ty)
    1.39 -        else NONE) operations;
    1.40 -    fun improve (c, ty) = case AxClass.inst_tyco_of thy (c, ty)
    1.41 -         of SOME tyco => (case AList.lookup (op =) params (c, tyco)
    1.42 -             of SOME (_, ty') => SOME (ty, ty')
    1.43 -              | NONE => NONE)
    1.44 -          | NONE => NONE;
    1.45 +        else NONE) operations;*)[];
    1.46            (*| NONE => (case map_filter
    1.47                 (fn ((c', _), (_, ty')) => if c' = c then SOME ty' else NONE) params
    1.48               of [ty'] => (case Sign.const_typargs thy (c, ty)
    1.49 @@ -692,9 +686,9 @@
    1.50        map (fn ((c, _), v_ty as (_, ty)) => (Free v_ty, Const (c, ty))) params;
    1.51    in
    1.52      ctxt
    1.53 -    |> fold (ProofContext.add_const_constraint o apsnd SOME) local_constraints
    1.54 -    |> Overloading.map_improvable_syntax (K (((local_constraints, global_constraints),
    1.55 -        ((improve, subst), unchecks)), false))
    1.56 +    |> Overloading.map_improvable_syntax
    1.57 +         (fn (((local_constraints, _), ((improve, _), _)), _) =>
    1.58 +            (((local_constraints, global_constraints), ((improve, subst), unchecks)), false))
    1.59    end;
    1.60  
    1.61  
    1.62 @@ -715,25 +709,37 @@
    1.63      explode #> scan_valids #> implode
    1.64    end;
    1.65  
    1.66 +fun type_name "*" = "prod"
    1.67 +  | type_name "+" = "sum"
    1.68 +  | type_name s = sanatize_name (NameSpace.base s); (*FIXME*)
    1.69 +
    1.70  fun init_instantiation (tycos, vs, sort) thy =
    1.71    let
    1.72      val _ = if null tycos then error "At least one arity must be given" else ();
    1.73 -    val _ = map (the_class_data thy) sort;
    1.74 -    fun type_name "*" = "prod"
    1.75 -      | type_name "+" = "sum"
    1.76 -      | type_name s = sanatize_name (NameSpace.base s); (*FIXME*)
    1.77 +    fun subst_class_typ sort = map_atyps
    1.78 +      (fn TFree _ => TVar ((Name.aT, 0), sort) | ty' => ty');
    1.79      fun get_param tyco (param, (c, ty)) = if can (AxClass.param_of_inst thy) (c, tyco)
    1.80        then NONE else SOME ((c, tyco),
    1.81          (param ^ "_" ^ type_name tyco, map_atyps (K (Type (tyco, map TFree vs))) ty));
    1.82      val params = map_product get_param tycos (these_params thy sort) |> map_filter I;
    1.83 +    val operations = these_operations thy sort;
    1.84 +    val local_constraints = (map o apsnd) (subst_class_typ [] o fst o snd) operations;
    1.85 +    fun improve (c, ty) = case AxClass.inst_tyco_of thy (c, ty)
    1.86 +     of SOME tyco => (case AList.lookup (op =) params (c, tyco)
    1.87 +         of SOME (_, ty') => SOME (ty, ty')
    1.88 +          | NONE => NONE)
    1.89 +      | NONE => NONE;
    1.90    in
    1.91      thy
    1.92      |> ProofContext.init
    1.93      |> Instantiation.put (mk_instantiation ((tycos, vs, sort), params))
    1.94      |> fold (Variable.declare_term o Logic.mk_type o TFree) vs
    1.95      |> fold (Variable.declare_names o Free o snd) params
    1.96 +    |> (Overloading.map_improvable_syntax o apfst)
    1.97 +         (fn ((_, global_constraints), ((_, subst), unchecks)) =>
    1.98 +            ((local_constraints, global_constraints), ((improve, subst), unchecks)))
    1.99 +    |> Overloading.add_improvable_syntax
   1.100      |> synchronize_inst_syntax
   1.101 -    |> Overloading.add_improvable_syntax
   1.102    end;
   1.103  
   1.104  fun confirm_declaration c = (map_instantiation o apsnd)