src/Pure/Isar/class.ML
changeset 25368 f12613fda79d
parent 25344 00c2179db769
child 25462 dad0291cb76a
     1.1 --- a/src/Pure/Isar/class.ML	Fri Nov 09 23:24:30 2007 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Fri Nov 09 23:24:31 2007 +0100
     1.3 @@ -325,31 +325,27 @@
     1.4      (*partial morphism of canonical interpretation*)
     1.5    intro: thm,
     1.6    defs: thm list,
     1.7 -  operations: (string * (term * (typ * int))) list,
     1.8 -    (*constant name ~> (locale term,
     1.9 -        (constant constraint, instantiaton index of class typ))*)
    1.10 -  unchecks: (term * term) list
    1.11 +  operations: (string * (class * (typ * term))) list
    1.12  };
    1.13  
    1.14  fun rep_class_data (ClassData d) = d;
    1.15  fun mk_class_data ((consts, base_sort, inst, morphism, intro),
    1.16 -    (defs, (operations, unchecks))) =
    1.17 +    (defs, operations)) =
    1.18    ClassData { consts = consts, base_sort = base_sort, inst = inst,
    1.19      morphism = morphism, intro = intro, defs = defs,
    1.20 -    operations = operations, unchecks = unchecks };
    1.21 +    operations = operations };
    1.22  fun map_class_data f (ClassData { consts, base_sort, inst, morphism, intro,
    1.23 -    defs, operations, unchecks }) =
    1.24 +    defs, operations }) =
    1.25    mk_class_data (f ((consts, base_sort, inst, morphism, intro),
    1.26 -    (defs, (operations, unchecks))));
    1.27 +    (defs, operations)));
    1.28  fun merge_class_data _ (ClassData { consts = consts,
    1.29      base_sort = base_sort, inst = inst, morphism = morphism, intro = intro,
    1.30 -    defs = defs1, operations = operations1, unchecks = unchecks1 },
    1.31 +    defs = defs1, operations = operations1 },
    1.32    ClassData { consts = _, base_sort = _, inst = _, morphism = _, intro = _,
    1.33 -    defs = defs2, operations = operations2, unchecks = unchecks2 }) =
    1.34 +    defs = defs2, operations = operations2 }) =
    1.35    mk_class_data ((consts, base_sort, inst, morphism, intro),
    1.36      (Thm.merge_thms (defs1, defs2),
    1.37 -      (AList.merge (op =) (K true) (operations1, operations2),
    1.38 -        Library.merge (op aconv o pairself snd) (unchecks1, unchecks2))));
    1.39 +      AList.merge (op =) (K true) (operations1, operations2)));
    1.40  
    1.41  structure ClassData = TheoryDataFun
    1.42  (
    1.43 @@ -395,9 +391,6 @@
    1.44  fun these_operations thy =
    1.45    maps (#operations o the_class_data thy) o ancestry thy;
    1.46  
    1.47 -fun these_unchecks thy =
    1.48 -  maps (#unchecks o the_class_data thy) o ancestry thy;
    1.49 -
    1.50  fun print_classes thy =
    1.51    let
    1.52      val ctxt = ProofContext.init thy;
    1.53 @@ -438,33 +431,30 @@
    1.54  
    1.55  fun add_class_data ((class, superclasses), (cs, base_sort, inst, phi, intro)) thy =
    1.56    let
    1.57 -    val operations = map (fn (v_ty, (c, ty)) =>
    1.58 -      (c, ((Free v_ty, (Logic.varifyT ty, 0))))) cs;
    1.59 -    val unchecks = map (fn ((v, ty'), (c, _)) =>
    1.60 -      (Free (v, Type.strip_sorts ty'), Const (c, Type.strip_sorts ty'))) cs;
    1.61 +    val operations = map (fn (v_ty as (_, ty), (c, _)) =>
    1.62 +      (c, (class, (ty, Free v_ty)))) cs;
    1.63      val cs = (map o pairself) fst cs;
    1.64      val add_class = Graph.new_node (class,
    1.65 -        mk_class_data ((cs, base_sort, map (SOME o Const) inst, phi, intro), ([], (operations, unchecks))))
    1.66 +        mk_class_data ((cs, base_sort, map (SOME o Const) inst, phi, intro), ([], operations)))
    1.67        #> fold (curry Graph.add_edge class) superclasses;
    1.68    in
    1.69      ClassData.map add_class thy
    1.70    end;
    1.71  
    1.72 -fun register_operation class (c, ((t, t_rev), some_def)) thy =
    1.73 +fun register_operation class (c, (t, some_def)) thy =
    1.74    let
    1.75 -    val ty = Sign.the_const_constraint thy c;
    1.76 -    val typargs = Sign.const_typargs thy (c, ty);
    1.77 -    val typidx = find_index (fn TVar ((v, _), _) => Name.aT = v | _ => false) typargs;
    1.78 +    val base_sort = (#base_sort o the_class_data thy) class;
    1.79      val prep_typ = map_atyps
    1.80 -      (fn TVar (vi as (v, _), _) => if Name.aT = v then TFree (v, []) else TVar (vi, []))
    1.81 -    val t_rev' = map_types prep_typ t_rev;
    1.82 -    val ty' = Term.fastype_of t_rev';
    1.83 +      (fn TVar (vi as (v, _), sort) => if Name.aT = v
    1.84 +        then TFree (v, base_sort) else TVar (vi, sort));
    1.85 +    val t' = map_types prep_typ t;
    1.86 +    val ty' = Term.fastype_of t';
    1.87    in
    1.88      thy
    1.89      |> (ClassData.map o Graph.map_node class o map_class_data o apsnd)
    1.90 -      (fn (defs, (operations, unchecks)) =>
    1.91 +      (fn (defs, operations) =>
    1.92          (fold cons (the_list some_def) defs,
    1.93 -          ((c, (t, (ty, typidx))) :: operations, (t_rev', Const (c, ty')) :: unchecks)))
    1.94 +          (c, (class, (ty', t'))) :: operations))
    1.95    end;
    1.96  
    1.97  
    1.98 @@ -611,57 +601,49 @@
    1.99  
   1.100  structure ClassSyntax = ProofDataFun(
   1.101    type T = {
   1.102 -    constraints: (string * typ) list,
   1.103 +    local_constraints: (string * typ) list,
   1.104 +    global_constraints: (string * typ) list,
   1.105      base_sort: sort,
   1.106 -    local_operation: string * typ -> (typ * term) option,
   1.107 +    operations: (string * (typ * term)) list,
   1.108      unchecks: (term * term) list,
   1.109      passed: bool
   1.110 -  } option;
   1.111 -  fun init _ = NONE;
   1.112 +  };
   1.113 +  fun init _ = {
   1.114 +    local_constraints = [],
   1.115 +    global_constraints = [],
   1.116 +    base_sort = [],
   1.117 +    operations = [],
   1.118 +    unchecks = [],
   1.119 +    passed = true
   1.120 +  };;
   1.121  );
   1.122  
   1.123  fun synchronize_syntax sups base_sort ctxt =
   1.124    let
   1.125      val thy = ProofContext.theory_of ctxt;
   1.126 -
   1.127 -    (* constraints *)
   1.128 +    fun subst_class_typ sort = map_atyps
   1.129 +      (fn TFree _ => TVar ((Name.aT, 0), sort) | ty' => ty');
   1.130      val operations = these_operations thy sups;
   1.131 -    fun local_constraint (c, (_, (ty, _))) =
   1.132 -      let
   1.133 -        val ty' = ty
   1.134 -          |> map_atyps (fn ty as TVar ((v, 0), _) =>
   1.135 -               if v = Name.aT then TVar ((v, 0), base_sort) else ty)
   1.136 -          |> SOME;
   1.137 -      in (c, ty') end
   1.138 -    val constraints = (map o apsnd) (fst o snd) operations;
   1.139 -
   1.140 -    (* check phase *)
   1.141 -    val consts = ProofContext.consts_of ctxt;
   1.142 +    val local_constraints =
   1.143 +      (map o apsnd) (subst_class_typ base_sort o fst o snd) operations;
   1.144 +    val global_constraints =
   1.145 +      (map o apsnd) (fn (class, (ty, _)) => subst_class_typ [class] ty) operations;
   1.146      fun declare_const (c, _) =
   1.147        let val b = Sign.base_name c
   1.148        in Sign.intern_const thy b = c ? Variable.declare_const (b, c) end;
   1.149 -    val typargs = Consts.typargs consts;
   1.150 -    fun check_const (c, ty) (t, (_, typidx)) = ((nth (typargs (c, ty)) typidx), t);
   1.151 -    fun local_operation (c_ty as (c, _)) = AList.lookup (op =) operations c
   1.152 -      |> Option.map (check_const c_ty);
   1.153 -
   1.154 -    (* uncheck phase *)
   1.155 -    val basify =
   1.156 -      map_atyps (fn ty as TFree (v, _) => if Name.aT = v then TFree (v, base_sort)
   1.157 -        else ty | ty => ty);
   1.158 -    val unchecks = these_unchecks thy sups
   1.159 -      |> (map o pairself o map_types) basify;
   1.160 +    val unchecks = map (fn (c, (_, (ty, t))) => (t, Const (c, ty))) operations;
   1.161    in
   1.162      ctxt
   1.163 -(*    |> fold declare_const operations  FIXME *)
   1.164 -    |> fold (ProofContext.add_const_constraint o local_constraint) operations
   1.165 -    |> ClassSyntax.put (SOME {
   1.166 -        constraints = constraints,
   1.167 +    |> fold declare_const local_constraints
   1.168 +    |> fold (ProofContext.add_const_constraint o apsnd SOME) local_constraints
   1.169 +    |> ClassSyntax.put {
   1.170 +        local_constraints = local_constraints,
   1.171 +        global_constraints = global_constraints,
   1.172          base_sort = base_sort,
   1.173 -        local_operation = local_operation,
   1.174 +        operations = (map o apsnd) snd operations,
   1.175          unchecks = unchecks,
   1.176          passed = false
   1.177 -      })
   1.178 +      }
   1.179    end;
   1.180  
   1.181  fun refresh_syntax class ctxt =
   1.182 @@ -670,37 +652,41 @@
   1.183      val base_sort = (#base_sort o the_class_data thy) class;
   1.184    in synchronize_syntax [class] base_sort ctxt end;
   1.185  
   1.186 -val mark_passed = (ClassSyntax.map o Option.map)
   1.187 -  (fn { constraints, base_sort, local_operation, unchecks, passed } =>
   1.188 -    { constraints = constraints, base_sort = base_sort,
   1.189 -      local_operation = local_operation, unchecks = unchecks, passed = true });
   1.190 +val mark_passed = ClassSyntax.map
   1.191 +  (fn { local_constraints, global_constraints, base_sort, operations, unchecks, passed } =>
   1.192 +    { local_constraints = local_constraints, global_constraints = global_constraints,
   1.193 +      base_sort = base_sort, operations = operations, unchecks = unchecks, passed = true });
   1.194  
   1.195  fun sort_term_check ts ctxt =
   1.196    let
   1.197 -    val { constraints, base_sort, local_operation, passed, ... } =
   1.198 -      the (ClassSyntax.get ctxt);
   1.199 -    fun check_typ (c, ty) (TFree (v, _), t) = if v = Name.aT
   1.200 -          then apfst (AList.update (op =) ((c, ty), t)) else I
   1.201 -      | check_typ (c, ty) (TVar (vi, _), t) = if TypeInfer.is_param vi
   1.202 -          then apfst (AList.update (op =) ((c, ty), t))
   1.203 -            #> apsnd (insert (op =) vi) else I
   1.204 -      | check_typ _ _ = I;
   1.205 -    fun add_const (Const c_ty) = Option.map (check_typ c_ty) (local_operation c_ty)
   1.206 -          |> the_default I
   1.207 -      | add_const _ = I;
   1.208 -    val (cs, typarams) = (fold o fold_aterms) add_const ts ([], []);
   1.209 -    val subst_typ = map_type_tvar (fn var as (vi, _) =>
   1.210 -      if member (op =) typarams vi then TFree (Name.aT, base_sort) else TVar var);
   1.211 -    val subst_term = map_aterms
   1.212 -        (fn t as Const (c, ty) => the_default t (AList.lookup (op =) cs (c, ty)) | t => t)
   1.213 -          #> map_types subst_typ;
   1.214 -    val ts' = map subst_term ts;
   1.215 -  in if eq_list (op aconv) (ts, ts') andalso passed then NONE
   1.216 +    val { local_constraints, global_constraints, base_sort, operations, passed, ... } =
   1.217 +      ClassSyntax.get ctxt;
   1.218 +    fun check_improve (Const (c, ty)) = (case AList.lookup (op =) local_constraints c
   1.219 +         of SOME ty0 => (case try (Type.raw_match (ty0, ty)) Vartab.empty
   1.220 +             of SOME tyenv => (case Vartab.lookup tyenv (Name.aT, 0)
   1.221 +                 of SOME (_, TVar (tvar as (vi, _))) =>
   1.222 +                      if TypeInfer.is_param vi then cons tvar else I
   1.223 +                  | _ => I)
   1.224 +              | NONE => I)
   1.225 +          | NONE => I)
   1.226 +      | check_improve _ = I;
   1.227 +    val improvements = (fold o fold_aterms) check_improve ts [];
   1.228 +    val ts' = (map o map_types o map_atyps) (fn ty as TVar tvar =>
   1.229 +        if member (op =) improvements tvar
   1.230 +          then TFree (Name.aT, base_sort) else ty | ty => ty) ts;
   1.231 +    fun check t0 = Envir.expand_term (fn Const (c, ty) => (case AList.lookup (op =) operations c
   1.232 +         of SOME (ty0, t) =>
   1.233 +              if Type.typ_instance (ProofContext.tsig_of ctxt) (ty, ty0)
   1.234 +              then SOME (ty0, check t) else NONE
   1.235 +          | NONE => NONE)
   1.236 +      | _ => NONE) t0;
   1.237 +    val ts'' = map check ts';
   1.238 +  in if eq_list (op aconv) (ts, ts'') andalso passed then NONE
   1.239    else
   1.240      ctxt
   1.241 -    |> fold (ProofContext.add_const_constraint o apsnd SOME) constraints
   1.242 +    |> fold (ProofContext.add_const_constraint o apsnd SOME) global_constraints
   1.243      |> mark_passed
   1.244 -    |> pair ts'
   1.245 +    |> pair ts''
   1.246      |> SOME
   1.247    end;
   1.248  
   1.249 @@ -709,7 +695,7 @@
   1.250  fun sort_term_uncheck ts ctxt =
   1.251    let
   1.252      val thy = ProofContext.theory_of ctxt;
   1.253 -    val unchecks = (#unchecks o the o ClassSyntax.get) ctxt;
   1.254 +    val unchecks = (#unchecks o ClassSyntax.get) ctxt;
   1.255      val ts' = if ! uncheck
   1.256        then map (Pattern.rewrite_term thy unchecks []) ts else ts;
   1.257    in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt) end;
   1.258 @@ -883,7 +869,7 @@
   1.259      |> Thm.add_def false (c, def_eq)    (* FIXME PureThy.add_defs_i *)
   1.260      |>> Thm.symmetric
   1.261      |-> (fn def => class_interpretation class [def] [Thm.prop_of def]
   1.262 -          #> register_operation class (c', ((dict, dict'), SOME (Thm.varifyT def))))
   1.263 +          #> register_operation class (c', (dict', SOME (Thm.varifyT def))))
   1.264      |> Sign.restore_naming thy
   1.265      |> Sign.add_const_constraint (c', SOME ty')
   1.266    end;
   1.267 @@ -906,7 +892,7 @@
   1.268      |> Sign.add_abbrev (#1 prmode) pos (c, map_types Type.strip_sorts rhs') |> snd
   1.269      |> Sign.add_const_constraint (c', SOME ty')
   1.270      |> Sign.notation true prmode [(Const (c', ty'), mx)]
   1.271 -    |> register_operation class (c', ((rhs, rhs'), NONE))
   1.272 +    |> register_operation class (c', (rhs', NONE))
   1.273      |> Sign.restore_naming thy
   1.274    end;
   1.275