src/Pure/Isar/class.ML
changeset 26518 3db6a46d8460
parent 26470 e44d24620515
child 26596 07d7d0a6d5fd
     1.1 --- a/src/Pure/Isar/class.ML	Wed Apr 02 15:58:40 2008 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Wed Apr 02 15:58:41 2008 +0200
     1.3 @@ -9,9 +9,9 @@
     1.4  sig
     1.5    (*classes*)
     1.6    val class: bstring -> class list -> Element.context_i list
     1.7 -    -> string list -> theory -> string * Proof.context
     1.8 +    -> theory -> string * Proof.context
     1.9    val class_cmd: bstring -> xstring list -> Element.context list
    1.10 -    -> xstring list -> theory -> string * Proof.context
    1.11 +    -> theory -> string * Proof.context
    1.12  
    1.13    val init: class -> theory -> Proof.context
    1.14    val declare: string -> Markup.property list
    1.15 @@ -26,7 +26,7 @@
    1.16  
    1.17    val class_prefix: string -> string
    1.18    val is_class: theory -> class -> bool
    1.19 -  val these_params: theory -> sort -> (string * (string * typ)) list
    1.20 +  val these_params: theory -> sort -> (string * (class * (string * typ))) list
    1.21    val print_classes: theory -> unit
    1.22  
    1.23    (*instances*)
    1.24 @@ -184,7 +184,8 @@
    1.25          val const_typs = (#params o AxClass.get_info thy) class;
    1.26          val const_names = (#consts o the_class_data thy) class;
    1.27        in
    1.28 -        (map o apsnd) (fn c => (c, (the o AList.lookup (op =) const_typs) c)) const_names
    1.29 +        (map o apsnd)
    1.30 +          (fn c => (class, (c, (the o AList.lookup (op =) const_typs) c))) const_names
    1.31        end;
    1.32    in maps params o ancestry thy end;
    1.33  
    1.34 @@ -252,8 +253,8 @@
    1.35  fun register_operation class (c, (t, some_def)) thy =
    1.36    let
    1.37      val base_sort = (#base_sort o the_class_data thy) class;
    1.38 -    val prep_typ = map_atyps
    1.39 -      (fn TVar (vi as (v, _), sort) => if Name.aT = v
    1.40 +    val prep_typ = map_type_tvar
    1.41 +      (fn (vi as (v, _), sort) => if Name.aT = v
    1.42          then TFree (v, base_sort) else TVar (vi, sort));
    1.43      val t' = map_types prep_typ t;
    1.44      val ty' = Term.fastype_of t';
    1.45 @@ -273,9 +274,8 @@
    1.46  fun calculate sups base_sort assm_axiom param_map class thy =
    1.47    let
    1.48      (*static parts of morphism*)
    1.49 -    val subst_typ = map_atyps (fn TFree (v, sort) =>
    1.50 -          if v = Name.aT then TVar ((v, 0), [class]) else TVar ((v, 0), sort)
    1.51 -      | ty => ty);
    1.52 +    val subst_typ = map_type_tfree (fn (v, sort) =>
    1.53 +          if v = Name.aT then TVar ((v, 0), [class]) else TVar ((v, 0), sort));
    1.54      fun subst_aterm (t as Free (v, ty)) = (case AList.lookup (op =) param_map v
    1.55           of SOME (c, _) => Const (c, ty)
    1.56            | NONE => t)
    1.57 @@ -347,10 +347,9 @@
    1.58  
    1.59  fun class_interpretation class facts defs thy =
    1.60    let
    1.61 -    val params = these_params thy [class];
    1.62 -    val consts = map (fst o snd) params;
    1.63 -    val constraints = map (fn c => map_atyps (K (TFree (Name.aT,
    1.64 -      [the (AxClass.class_of_param thy c)]))) (Sign.the_const_type thy c)) consts;
    1.65 +    val consts = map (apsnd fst o snd) (these_params thy [class]);
    1.66 +    val constraints = map (fn (class, c) => map_atyps (K (TFree (Name.aT,
    1.67 +      [class]))) (Sign.the_const_type thy c)) consts;
    1.68      val no_constraints = map (map_atyps (K (TFree (Name.aT, [])))) constraints;
    1.69      fun add_constraint c T = Sign.add_const_constraint (c, SOME T);
    1.70      val inst = (#inst o the_class_data thy) class;
    1.71 @@ -358,10 +357,10 @@
    1.72      val prfx = class_prefix class;
    1.73    in
    1.74      thy
    1.75 -    |> fold2 add_constraint consts no_constraints
    1.76 +    |> fold2 add_constraint (map snd consts) no_constraints
    1.77      |> prove_interpretation tac ((false, prfx), []) (Locale.Locale class)
    1.78            (inst, map (fn def => (("", []), def)) defs)
    1.79 -    |> fold2 add_constraint consts constraints
    1.80 +    |> fold2 add_constraint (map snd consts) constraints
    1.81    end;
    1.82  
    1.83  fun prove_subclass (sub, sup) thm thy =
    1.84 @@ -412,17 +411,16 @@
    1.85  fun synchronize_class_syntax sups base_sort ctxt =
    1.86    let
    1.87      val thy = ProofContext.theory_of ctxt;
    1.88 -    fun subst_class_typ sort = map_atyps
    1.89 -      (fn TFree _ => TVar ((Name.aT, 0), sort) | ty' => ty');
    1.90      val operations = these_operations thy sups;
    1.91 -    val local_constraints =
    1.92 +    fun subst_class_typ sort = map_type_tfree (K (TVar ((Name.aT, 0), sort)));
    1.93 +    val primary_constraints =
    1.94        (map o apsnd) (subst_class_typ base_sort o fst o snd) operations;
    1.95 -    val global_constraints =
    1.96 +    val secondary_constraints =
    1.97        (map o apsnd) (fn (class, (ty, _)) => subst_class_typ [class] ty) operations;
    1.98      fun declare_const (c, _) =
    1.99        let val b = Sign.base_name c
   1.100        in Sign.intern_const thy b = c ? Variable.declare_const (b, c) end;
   1.101 -    fun improve (c, ty) = (case AList.lookup (op =) local_constraints c
   1.102 +    fun improve (c, ty) = (case AList.lookup (op =) primary_constraints c
   1.103       of SOME ty' => (case try (Type.raw_match (ty', ty)) Vartab.empty
   1.104           of SOME tyenv => (case Vartab.lookup tyenv (Name.aT, 0)
   1.105               of SOME (_, ty' as TVar (tvar as (vi, _))) =>
   1.106 @@ -436,10 +434,10 @@
   1.107      val unchecks = map (fn (c, (_, (ty, t))) => (t, Const (c, ty))) operations;
   1.108    in
   1.109      ctxt
   1.110 -    |> fold declare_const local_constraints
   1.111 -    |> Overloading.map_improvable_syntax (K (((local_constraints, global_constraints),
   1.112 +    |> fold declare_const primary_constraints
   1.113 +    |> Overloading.map_improvable_syntax (K (((primary_constraints, secondary_constraints),
   1.114          ((improve, subst), unchecks)), false))
   1.115 -    |> Overloading.set_local_constraints
   1.116 +    |> Overloading.set_primary_constraints
   1.117    end;
   1.118  
   1.119  fun refresh_syntax class ctxt =
   1.120 @@ -500,10 +498,10 @@
   1.121  val read_class_spec = gen_class_spec Sign.intern_class Locale.read_expr;
   1.122  val check_class_spec = gen_class_spec (K I) Locale.cert_expr;
   1.123  
   1.124 -fun adjungate_axclass bname class base_sort sups supsort supparams global_syntax other_consts thy =
   1.125 +fun adjungate_axclass bname class base_sort sups supsort supparams global_syntax thy =
   1.126    let
   1.127      val supconsts = map fst supparams
   1.128 -      |> AList.make (the o AList.lookup (op =) (these_params thy sups))
   1.129 +      |> AList.make (snd o the o AList.lookup (op =) (these_params thy sups))
   1.130        |> (map o apsnd o apsnd o map_atyps o K o TFree) (Name.aT, [class]);
   1.131      val all_params = map fst (Locale.parameters_of thy class);
   1.132      fun add_const (v, raw_ty) thy =
   1.133 @@ -538,7 +536,7 @@
   1.134      thy
   1.135      |> add_consts ((snd o chop (length supparams)) all_params)
   1.136      |-> (fn (param_map, params) => AxClass.define_class (bname, supsort)
   1.137 -          (map (fst o snd) params @ other_consts)
   1.138 +          (map (fst o snd) params)
   1.139            [((bname ^ "_" ^ AxClass.axiomsN, []), map (globalize param_map) raw_pred)]
   1.140      #> snd
   1.141      #> `get_axiom
   1.142 @@ -546,19 +544,17 @@
   1.143      #> pair (param_map, params, assm_axiom)))
   1.144    end;
   1.145  
   1.146 -fun gen_class prep_spec prep_param bname
   1.147 -    raw_supclasses raw_elems raw_other_consts thy =
   1.148 +fun gen_class prep_spec bname raw_supclasses raw_elems thy =
   1.149    let
   1.150      val class = Sign.full_name thy bname;
   1.151      val (((sups, supparams), (supsort, base_sort, mergeexpr)), (elems, global_syntax)) =
   1.152        prep_spec thy raw_supclasses raw_elems;
   1.153 -    val other_consts = map (tap (Sign.the_const_type thy) o prep_param thy) raw_other_consts;
   1.154    in
   1.155      thy
   1.156      |> Locale.add_locale_i (SOME "") bname mergeexpr elems
   1.157      |> snd
   1.158      |> ProofContext.theory_of
   1.159 -    |> adjungate_axclass bname class base_sort sups supsort supparams global_syntax other_consts
   1.160 +    |> adjungate_axclass bname class base_sort sups supsort supparams global_syntax
   1.161      |-> (fn (param_map, params, assm_axiom) =>
   1.162          calculate sups base_sort assm_axiom param_map class
   1.163      #-> (fn (morphism, axiom, assm_intro, of_class) =>
   1.164 @@ -569,12 +565,10 @@
   1.165      |> pair class
   1.166    end;
   1.167  
   1.168 -fun read_const thy = #1 o Term.dest_Const o ProofContext.read_const (ProofContext.init thy);
   1.169 -
   1.170  in
   1.171  
   1.172 -val class_cmd = gen_class read_class_spec read_const;
   1.173 -val class = gen_class check_class_spec (K I);
   1.174 +val class_cmd = gen_class read_class_spec;
   1.175 +val class = gen_class check_class_spec;
   1.176  
   1.177  end; (*local*)
   1.178  
   1.179 @@ -667,8 +661,6 @@
   1.180    let
   1.181      val Instantiation { arities = (_, _, sort), params = params } = Instantiation.get ctxt;
   1.182      val thy = ProofContext.theory_of ctxt;
   1.183 -    fun subst_class_typ sort = map_atyps
   1.184 -      (fn TFree _ => TVar ((Name.aT, 0), sort) | ty' => ty');
   1.185      fun subst (c, ty) = case AxClass.inst_tyco_of thy (c, ty)
   1.186           of SOME tyco => (case AList.lookup (op =) params (c, tyco)
   1.187               of SOME (v_ty as (_, ty)) => SOME (ty, Free v_ty)
   1.188 @@ -679,8 +671,8 @@
   1.189    in
   1.190      ctxt
   1.191      |> Overloading.map_improvable_syntax
   1.192 -         (fn (((local_constraints, _), ((improve, _), _)), _) =>
   1.193 -            (((local_constraints, []), ((improve, subst), unchecks)), false))
   1.194 +         (fn (((primary_constraints, _), ((improve, _), _)), _) =>
   1.195 +            (((primary_constraints, []), ((improve, subst), unchecks)), false))
   1.196    end;
   1.197  
   1.198  
   1.199 @@ -705,43 +697,43 @@
   1.200    | type_name "+" = "sum"
   1.201    | type_name s = sanatize_name (NameSpace.base s); (*FIXME*)
   1.202  
   1.203 +fun resort_terms pp algebra consts constraints ts =
   1.204 +  let
   1.205 +    fun matchings (Const (c_ty as (c, _))) = (case constraints c
   1.206 +         of NONE => I
   1.207 +          | SOME sorts => fold2 (curry (Sorts.meet_sort algebra))
   1.208 +              (Consts.typargs consts c_ty) sorts)
   1.209 +      | matchings _ = I
   1.210 +    val tvartab = (fold o fold_aterms) matchings ts Vartab.empty
   1.211 +      handle Sorts.CLASS_ERROR e => Sorts.class_error pp e;
   1.212 +    val inst = map_type_tvar (fn (vi, _) => TVar (vi, the (Vartab.lookup tvartab vi)));
   1.213 +  in if Vartab.is_empty tvartab then NONE else SOME ((map o map_types) inst ts) end;
   1.214 +
   1.215  fun init_instantiation (tycos, vs, sort) thy =
   1.216    let
   1.217      val _ = if null tycos then error "At least one arity must be given" else ();
   1.218 -    fun subst_class_typ sort = map_atyps
   1.219 -      (fn TFree _ => TVar ((Name.aT, 0), sort) | ty' => ty');
   1.220 -    fun get_param tyco (param, (c, ty)) = if can (AxClass.param_of_inst thy) (c, tyco)
   1.221 +    val params = these_params thy sort;
   1.222 +    fun get_param tyco (param, (_, (c, ty))) = if can (AxClass.param_of_inst thy) (c, tyco)
   1.223        then NONE else SOME ((c, tyco),
   1.224          (param ^ "_" ^ type_name tyco, map_atyps (K (Type (tyco, map TFree vs))) ty));
   1.225 -    val class_of = fst o the o AList.lookup (op =) (these_operations thy sort);
   1.226 -    val params = these_params thy sort;
   1.227 -    val inst_params = map_product get_param tycos (these_params thy sort) |> map_filter I;
   1.228 -    val local_constraints = map (apsnd (subst_class_typ []) o snd) params;
   1.229 -    val pseudo_constraints = map (fn (_, (c, _)) => (c, class_of c)) params;
   1.230 -    val typ_of_sort = Type.typ_of_sort (Sign.classes_of thy);
   1.231 -    val typargs = Sign.const_typargs thy;
   1.232 +    val inst_params = map_product get_param tycos params |> map_filter I;
   1.233 +    val primary_constraints = map (apsnd
   1.234 +      (map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) params;
   1.235      val pp = Sign.pp thy;
   1.236 -    fun constrain_typ tys sorts ty =
   1.237 -      let
   1.238 -        val tyenv = fold2 typ_of_sort tys sorts Vartab.empty
   1.239 -          handle Sorts.CLASS_ERROR e => Sorts.class_error pp e;
   1.240 -      in
   1.241 -        map_atyps (fn TVar (vi, _) => TVar (vi, the (Vartab.lookup tyenv vi))
   1.242 -          | ty => ty) ty
   1.243 -      end;
   1.244 -    fun constrain_class (c, ty) class =
   1.245 -      constrain_typ (typargs (c, ty)) [[class]] ty;
   1.246 -    fun improve_param (c, ty) = case AxClass.inst_tyco_of thy (c, ty)
   1.247 +    val algebra = Sign.classes_of thy
   1.248 +      |> fold (fn tyco => Sorts.add_arities pp
   1.249 +            (tyco, map (fn class => (class, map snd vs)) sort)) tycos;
   1.250 +    val consts = Sign.consts_of thy;
   1.251 +    val improve_constraints = AList.lookup (op =)
   1.252 +      (map (fn (_, (class, (c, _))) => (c, [[class]])) params);
   1.253 +    fun resort_check ts ctxt = case resort_terms pp algebra consts improve_constraints ts
   1.254 +     of NONE => NONE
   1.255 +      | SOME ts' => SOME (ts', ctxt);
   1.256 +    fun improve (c, ty) = case AxClass.inst_tyco_of thy (c, ty)
   1.257       of SOME tyco => (case AList.lookup (op =) inst_params (c, tyco)
   1.258 -         of SOME (_, ty') => SOME (ty, ty')
   1.259 +         of SOME (_, ty') => if Type.raw_instance (ty', ty) then SOME (ty, ty') else NONE
   1.260            | NONE => NONE)
   1.261        | NONE => NONE;
   1.262 -    fun improve (c, ty) = case improve_param (c, ty)
   1.263 -     of SOME ty_ty' => SOME ty_ty'
   1.264 -      | NONE => (case AList.lookup (op =) pseudo_constraints c
   1.265 -         of SOME class =>
   1.266 -              SOME (ty, constrain_class (c, ty) class)
   1.267 -          | NONE => NONE);
   1.268    in
   1.269      thy
   1.270      |> ProofContext.init
   1.271 @@ -750,8 +742,9 @@
   1.272      |> fold (Variable.declare_names o Free o snd) inst_params
   1.273      |> (Overloading.map_improvable_syntax o apfst)
   1.274           (fn ((_, _), ((_, subst), unchecks)) =>
   1.275 -            ((local_constraints, []), ((improve, K NONE), [])))
   1.276 +            ((primary_constraints, []), ((improve, K NONE), [])))
   1.277      |> Overloading.add_improvable_syntax
   1.278 +    |> Context.proof_map (Syntax.add_term_check 0 "resorting" resort_check)
   1.279      |> synchronize_inst_syntax
   1.280    end;
   1.281  
   1.282 @@ -787,11 +780,6 @@
   1.283          (Type (tyco, map TFree vs), sort)
   1.284        then () else error ("Missing instance proof for type " ^ quote (Sign.extern_type thy tyco)))
   1.285          tycos;
   1.286 -    (*this checkpoint should move to AxClass as soon as "attach" has disappeared*)
   1.287 -    val _ = case map (fst o snd) params
   1.288 -     of [] => ()
   1.289 -      | cs => Output.legacy_feature
   1.290 -          ("Missing specifications for overloaded parameters " ^ commas_quote cs)
   1.291    in lthy end;
   1.292  
   1.293  fun pretty_instantiation lthy =