src/Pure/Isar/class.ML
changeset 25002 c3d9cb390471
parent 24981 4ec3f95190bf
child 25010 8bc74ba1423d
     1.1 --- a/src/Pure/Isar/class.ML	Fri Oct 12 14:42:29 2007 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Fri Oct 12 14:42:30 2007 +0200
     1.3 @@ -14,22 +14,23 @@
     1.4      -> theory -> class * theory
     1.5    val classrel_cmd: xstring * xstring -> theory -> Proof.state
     1.6  
     1.7 -  val class: bool -> bstring -> class list -> Element.context_i Locale.element list
     1.8 +  val class: bstring -> class list -> Element.context_i Locale.element list
     1.9      -> string list -> theory -> string * Proof.context
    1.10 -  val class_cmd: bool -> bstring -> xstring list -> Element.context Locale.element list
    1.11 +  val class_cmd: bstring -> xstring list -> Element.context Locale.element list
    1.12      -> xstring list -> theory -> string * Proof.context
    1.13    val init: class -> Proof.context -> Proof.context;
    1.14    val add_const_in_class: string -> (string * term) * Syntax.mixfix
    1.15      -> theory -> string * theory
    1.16    val add_abbrev_in_class: string -> Syntax.mode -> (string * term) * mixfix
    1.17      -> theory -> string * theory
    1.18 -  val remove_constraint: sort -> string -> Proof.context -> Proof.context
    1.19 +  val remove_constraint: class -> string -> Proof.context -> Proof.context
    1.20 +  val class_of_locale: theory -> string -> class option
    1.21 +  val locale_of_class: theory -> class -> string
    1.22 +  val these_params: theory -> sort -> (string * (string * typ)) list
    1.23    val intro_classes_tac: thm list -> tactic
    1.24    val default_intro_classes_tac: thm list -> tactic
    1.25 -  val class_of_locale: theory -> string -> class option
    1.26 -  val locale_of_class: theory -> class -> string
    1.27 -  val local_syntax: theory -> class -> bool
    1.28    val print_classes: theory -> unit
    1.29 +  val uncheck: bool ref
    1.30  
    1.31    val instance_arity: (theory -> theory) -> arity list -> theory -> Proof.state
    1.32    val instance: arity list -> ((bstring * Attrib.src list) * term) list
    1.33 @@ -47,7 +48,6 @@
    1.34    val unoverload_const: theory -> string * typ -> string
    1.35    val inst_const: theory -> string * string -> string
    1.36    val param_const: theory -> string -> (string * string) option
    1.37 -  val params_of_sort: theory -> sort -> (string * (string * typ)) list
    1.38  end;
    1.39  
    1.40  structure Class : CLASS =
    1.41 @@ -63,8 +63,8 @@
    1.42      val mx_local = if is_loc then mx else NoSyn;
    1.43    in (mx_global, mx_local) end;
    1.44  
    1.45 -fun prove_interpretation tac prfx_atts expr insts =
    1.46 -  Locale.interpretation_i I prfx_atts expr insts
    1.47 +fun prove_interpretation tac prfx_atts expr inst =
    1.48 +  Locale.interpretation_i I prfx_atts expr inst
    1.49    #> Proof.global_terminal_proof
    1.50        (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
    1.51    #> ProofContext.theory_of;
    1.52 @@ -323,32 +323,32 @@
    1.53    inst: typ Symtab.table * term Symtab.table
    1.54      (*canonical interpretation*),
    1.55    intro: thm,
    1.56 -  local_syntax: bool,
    1.57    defs: thm list,
    1.58 -  operations: (string * (term * int) option) list,
    1.59 -    (*constant name ~> (locale term, instantiaton index of class typ)*)
    1.60 -  constraints: (string * typ) list
    1.61 +  operations: (string * (term * (typ * int))) list
    1.62 +    (*constant name ~> (locale term, (constant constraint, instantiaton index of class typ))*),
    1.63 +  operations_rev: (string * string) list
    1.64 +    (*locale operation ~> constant name*)
    1.65  };
    1.66  
    1.67  fun rep_class_data (ClassData d) = d;
    1.68 -fun mk_class_data ((locale, consts, local_sort, inst, intro, local_syntax),
    1.69 -    (defs, (operations, constraints))) =
    1.70 +fun mk_class_data ((locale, consts, local_sort, inst, intro),
    1.71 +    (defs, operations, operations_rev)) =
    1.72    ClassData { locale = locale, consts = consts, local_sort = local_sort, inst = inst,
    1.73 -    intro = intro, local_syntax = local_syntax, defs = defs, operations = operations,
    1.74 -    constraints = constraints };
    1.75 +    intro = intro, defs = defs, operations = operations,
    1.76 +    operations_rev = operations_rev };
    1.77  fun map_class_data f (ClassData { locale, consts, local_sort, inst, intro,
    1.78 -    local_syntax, defs, operations, constraints }) =
    1.79 -  mk_class_data (f ((locale, consts, local_sort, inst, intro, local_syntax),
    1.80 -    (defs, (operations, constraints))));
    1.81 +    defs, operations, operations_rev }) =
    1.82 +  mk_class_data (f ((locale, consts, local_sort, inst, intro),
    1.83 +    (defs, operations, operations_rev)));
    1.84  fun merge_class_data _ (ClassData { locale = locale, consts = consts,
    1.85 -    local_sort = local_sort, inst = inst, intro = intro, local_syntax = local_syntax,
    1.86 -    defs = defs1, operations = operations1, constraints = constraints1 },
    1.87 -  ClassData { locale = _, consts = _, local_sort = _, inst = _, intro = _, local_syntax = _,
    1.88 -    defs = defs2, operations = operations2, constraints = constraints2 }) =
    1.89 -  mk_class_data ((locale, consts, local_sort, inst, intro, local_syntax),
    1.90 +    local_sort = local_sort, inst = inst, intro = intro,
    1.91 +    defs = defs1, operations = operations1, operations_rev = operations_rev1 },
    1.92 +  ClassData { locale = _, consts = _, local_sort = _, inst = _, intro = _,
    1.93 +    defs = defs2, operations = operations2, operations_rev = operations_rev2 }) =
    1.94 +  mk_class_data ((locale, consts, local_sort, inst, intro),
    1.95      (Thm.merge_thms (defs1, defs2),
    1.96 -      (AList.merge (op =) (K true) (operations1, operations2),
    1.97 -      AList.merge (op =) (K true) (constraints1, constraints2))));
    1.98 +      AList.merge (op =) (K true) (operations1, operations2),
    1.99 +      AList.merge (op =) (K true) (operations_rev1, operations_rev2)));
   1.100  
   1.101  fun merge_pair f1 f2 ((x1, y1), (x2, y2)) = (f1 (x1, x2), f2 (y1, y2));
   1.102  
   1.103 @@ -377,7 +377,7 @@
   1.104  
   1.105  val ancestry = Graph.all_succs o fst o ClassData.get;
   1.106  
   1.107 -fun params_of_sort thy =
   1.108 +fun these_params thy =
   1.109    let
   1.110      fun params class =
   1.111        let
   1.112 @@ -397,10 +397,12 @@
   1.113  fun these_operations thy =
   1.114    maps (#operations o the_class_data thy) o ancestry thy;
   1.115  
   1.116 -fun these_constraints thy =
   1.117 -  maps (#constraints o the_class_data thy) o ancestry thy;
   1.118 +fun these_operations_rev thy =
   1.119 +  maps (#operations_rev o the_class_data thy) o ancestry thy;
   1.120  
   1.121 -fun local_operation thy = Option.join oo AList.lookup (op =) o these_operations thy;
   1.122 +fun local_operation thy = AList.lookup (op =) o these_operations thy;
   1.123 +
   1.124 +fun global_operation thy = AList.lookup (op =) o these_operations_rev thy;
   1.125  
   1.126  fun sups_local_sort thy sort =
   1.127    let
   1.128 @@ -411,8 +413,6 @@
   1.129        | [] => sort;
   1.130    in (sups, local_sort) end;
   1.131  
   1.132 -fun local_syntax thy = #local_syntax o the_class_data thy;
   1.133 -
   1.134  fun print_classes thy =
   1.135    let
   1.136      val ctxt = ProofContext.init thy;
   1.137 @@ -450,25 +450,24 @@
   1.138  
   1.139  (* updaters *)
   1.140  
   1.141 -fun add_class_data ((class, superclasses), (locale, consts, local_sort, inst, intro, local_syntax)) =
   1.142 -  ClassData.map (fn (gr, tab) => (
   1.143 -    gr
   1.144 -    |> Graph.new_node (class, mk_class_data ((locale, (map o pairself) fst consts,
   1.145 -        local_sort, inst, intro, local_syntax),
   1.146 -          ([], (map (apfst fst o apsnd (SOME o rpair 0 o Free) o swap) consts, map snd consts))))
   1.147 -    |> fold (curry Graph.add_edge class) superclasses,
   1.148 -    tab
   1.149 -    |> Symtab.update (locale, class)
   1.150 -  ));
   1.151 +fun add_class_data ((class, superclasses), (locale, cs, local_sort, inst, intro)) =
   1.152 +  let
   1.153 +    val operations = map (fn (v_ty, (c, ty)) => (c, (Free v_ty, (ty, 0)))) cs;
   1.154 +    val cs = (map o pairself) fst cs;
   1.155 +    val add_class = Graph.new_node (class, mk_class_data ((locale,
   1.156 +          cs, local_sort, inst, intro),
   1.157 +            ([], operations, [])))
   1.158 +      #> fold (curry Graph.add_edge class) superclasses;
   1.159 +    val add_locale = Symtab.update (locale, class);
   1.160 +  in
   1.161 +    ClassData.map (fn (gr, tab) => (add_class gr, add_locale tab))
   1.162 +  end;
   1.163  
   1.164 -fun register_const class (entry, def) =
   1.165 +fun register_operation class (entry, some_def) =
   1.166    (ClassData.map o apfst o Graph.map_node class o map_class_data o apsnd)
   1.167 -    (fn (defs, (operations, constraints)) =>
   1.168 -      (def :: defs, (apsnd (SOME o snd) entry :: operations, apsnd fst entry :: constraints)));
   1.169 -
   1.170 -fun register_abbrev class (abbrev, ty) =
   1.171 -  (ClassData.map o apfst o Graph.map_node class o map_class_data o apsnd o apsnd)
   1.172 -    (fn (operations, constraints) => ((abbrev, NONE) :: operations, (abbrev, ty) :: constraints));
   1.173 +    (fn (defs, operations, operations_rev) =>
   1.174 +      (case some_def of NONE => defs | SOME def => def :: defs,
   1.175 +        entry :: operations, (*FIXME*)operations_rev));
   1.176  
   1.177  
   1.178  (** rule calculation, tactics and methods **)
   1.179 @@ -559,23 +558,30 @@
   1.180  
   1.181  (** classes and class target **)
   1.182  
   1.183 -(* class context initialization *)
   1.184 +(* class context syntax *)
   1.185  
   1.186 -fun remove_constraint local_sort c ctxt =
   1.187 +fun internal_remove_constraint local_sort (c, (_, (ty, typidx))) ctxt =
   1.188    let
   1.189 -    val ty = ProofContext.the_const_constraint ctxt c;
   1.190 -    val ty' = map_atyps (fn ty as TFree (v, _) => if v = Name.aT
   1.191 -      then TFree (v, local_sort) else ty | ty => ty) ty;
   1.192 +    val consts = ProofContext.consts_of ctxt;
   1.193 +    val typargs = Consts.typargs consts (c, ty);
   1.194 +    val typargs' = nth_map typidx (K (TVar ((Name.aT, 0), local_sort))) typargs;
   1.195 +    val ty' = Consts.instance consts (c, typargs');
   1.196 +  in ProofContext.add_const_constraint (c, SOME ty') ctxt end;
   1.197 +
   1.198 +fun remove_constraint class c ctxt =
   1.199 +  let
   1.200 +    val thy = ProofContext.theory_of ctxt;
   1.201 +    val SOME entry = local_operation thy [class] c;
   1.202    in
   1.203 -    ctxt
   1.204 -    |> ProofContext.add_const_constraint (c, SOME ty')
   1.205 +    internal_remove_constraint
   1.206 +      ((#local_sort o the_class_data thy) class) (c, entry) ctxt
   1.207    end;
   1.208  
   1.209  fun sort_term_check sups local_sort ts ctxt =
   1.210    let
   1.211      val thy = ProofContext.theory_of ctxt;
   1.212      val local_operation = local_operation thy sups;
   1.213 -    val constraints = these_constraints thy sups;
   1.214 +    val constraints = these_operations thy sups |> (map o apsnd) (fst o snd);
   1.215      val consts = ProofContext.consts_of ctxt;
   1.216      fun check_typ (c, ty) (t', idx) = case nth (Consts.typargs consts (c, ty)) idx
   1.217       of TFree (v, _) => if v = Name.aT
   1.218 @@ -585,7 +591,7 @@
   1.219              #> apsnd (insert (op =) vi) else I
   1.220        | _ => I;
   1.221      fun add_const (Const (c, ty)) = (case local_operation c
   1.222 -         of SOME (t', idx) => check_typ (c, ty) (t', idx)
   1.223 +         of SOME (t', (_, idx)) => check_typ (c, ty) (t', idx)
   1.224            | NONE => I)
   1.225        | add_const _ = I;
   1.226      val (cs, typarams) = (fold o fold_aterms) add_const ts ([], []);
   1.227 @@ -596,6 +602,23 @@
   1.228      val ctxt' = fold (ProofContext.add_const_constraint o apsnd SOME) constraints ctxt;
   1.229    in (ts', ctxt') end;
   1.230  
   1.231 +val uncheck = ref false;
   1.232 +
   1.233 +fun sort_term_uncheck sups ts ctxt =
   1.234 +  let
   1.235 +    val thy = ProofContext.theory_of ctxt;
   1.236 +    val global_param = AList.lookup (op =) (these_params thy sups) #> Option.map fst;
   1.237 +    val global_operation = global_operation thy sups;
   1.238 +    fun globalize (t as Free (v, ty)) = (case global_param v
   1.239 +         of SOME c => Const (c, ty)
   1.240 +          | NONE => t)
   1.241 +      | globalize (t as Const (c, ty)) = (case global_operation c
   1.242 +         of SOME c => Const (c, ty)
   1.243 +          | NONE => t)
   1.244 +      | globalize t = t;
   1.245 +    val ts' = if ! uncheck then (map o map_aterms) globalize ts else ts;
   1.246 +  in (ts', ctxt) end;
   1.247 +
   1.248  fun init_class_ctxt sups local_sort ctxt =
   1.249    let
   1.250      val operations = these_operations (ProofContext.theory_of ctxt) sups;
   1.251 @@ -603,9 +626,11 @@
   1.252      ctxt
   1.253      |> Variable.declare_term
   1.254          (Logic.mk_type (TFree (Name.aT, local_sort)))
   1.255 -    |> fold (remove_constraint local_sort o fst) operations
   1.256 +    |> fold (internal_remove_constraint local_sort) operations
   1.257      |> Context.proof_map (Syntax.add_term_check 50 "class"
   1.258 -        (sort_term_check sups local_sort))
   1.259 +        (sort_term_check sups local_sort)
   1.260 +        #> Syntax.add_term_uncheck 50 "class"
   1.261 +          (sort_term_uncheck sups))
   1.262    end;
   1.263  
   1.264  fun init class ctxt =
   1.265 @@ -627,7 +652,7 @@
   1.266        | Locale.Expr i => apsnd (cons (prep_expr thy i))) raw_includes_elems ([], []);
   1.267      val supexpr = Locale.Merge suplocales;
   1.268      val supparams = (map fst o Locale.parameters_of_expr thy) supexpr;
   1.269 -    val supconsts = AList.make (the o AList.lookup (op =) (params_of_sort thy sups))
   1.270 +    val supconsts = AList.make (the o AList.lookup (op =) (these_params thy sups))
   1.271        (map fst supparams);
   1.272      val mergeexpr = Locale.Merge (suplocales @ includes);
   1.273      val constrain = Element.Constrains ((map o apsnd o map_atyps)
   1.274 @@ -646,7 +671,6 @@
   1.275  val read_class_spec = gen_class_spec Sign.intern_class Locale.intern_expr Locale.read_expr;
   1.276  val check_class_spec = gen_class_spec (K I) (K I) Locale.cert_expr;
   1.277  
   1.278 -
   1.279  fun define_class_params (name, raw_superclasses) raw_consts raw_dep_axioms other_consts thy =
   1.280    let
   1.281      val superclasses = map (Sign.certify_class thy) raw_superclasses;
   1.282 @@ -656,9 +680,8 @@
   1.283        raw_dep_axioms thy cs
   1.284        |> (map o apsnd o map) (Sign.cert_prop thy)
   1.285        |> rpair thy;
   1.286 -    fun add_constraint class (c, ty) =
   1.287 -      Sign.add_const_constraint (c, SOME
   1.288 -        (Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty));
   1.289 +    fun constrain_typs class = (map o apsnd o Term.map_type_tfree)
   1.290 +      (fn (v, _) => TFree (v, [class]))
   1.291    in
   1.292      thy
   1.293      |> Sign.add_path (Logic.const_of_class name)
   1.294 @@ -667,12 +690,13 @@
   1.295      |-> (fn cs => mk_axioms cs
   1.296      #-> (fn axioms_prop => AxClass.define_class (name, superclasses)
   1.297             (map fst cs @ other_consts) axioms_prop
   1.298 -    #-> (fn class => `(fn thy => AxClass.get_info thy class)
   1.299 -    #-> (fn {axioms, ...} => fold (add_constraint class) cs
   1.300 -    #> pair (class, (cs, axioms))))))
   1.301 +    #-> (fn class => `(fn _ => constrain_typs class cs)
   1.302 +    #-> (fn cs' => `(fn thy => AxClass.get_info thy class)
   1.303 +    #-> (fn {axioms, ...} => fold (Sign.add_const_constraint o apsnd SOME) cs'
   1.304 +    #> pair (class, (cs', axioms)))))))
   1.305    end;
   1.306  
   1.307 -fun gen_class prep_spec prep_param local_syntax bname
   1.308 +fun gen_class prep_spec prep_param bname
   1.309      raw_supclasses raw_includes_elems raw_other_consts thy =
   1.310    let
   1.311      val (((sups, supconsts), (supsort, local_sort, mergeexpr)), elems) =
   1.312 @@ -729,7 +753,7 @@
   1.313          add_class_data ((name_axclass, sups),
   1.314            (name_locale, map fst params ~~ consts, local_sort,
   1.315              (mk_instT name_axclass, mk_inst name_axclass (map fst globals)
   1.316 -              (map snd supconsts @ consts)), class_intro, local_syntax))
   1.317 +              (map snd supconsts @ consts)), class_intro))
   1.318        #> note_intro name_axclass class_intro
   1.319        #> class_interpretation name_axclass axioms []
   1.320        #> pair name_axclass
   1.321 @@ -748,8 +772,8 @@
   1.322  
   1.323  fun export_fixes thy class =
   1.324    let
   1.325 -    val consts = params_of_sort thy [class];
   1.326 -    fun subst_aterm (t as Free (v, ty)) = (case AList.lookup (op =) consts v
   1.327 +    val cs = these_params thy [class];
   1.328 +    fun subst_aterm (t as Free (v, ty)) = (case AList.lookup (op =) cs v
   1.329           of SOME (c, _) => Const (c, ty)
   1.330            | NONE => t)
   1.331        | subst_aterm t = t;
   1.332 @@ -757,10 +781,10 @@
   1.333  
   1.334  fun mk_operation_entry thy (c, rhs) =
   1.335    let
   1.336 -    val ty = fastype_of rhs;
   1.337 +    val ty = Logic.unvarifyT (Sign.the_const_constraint thy c);
   1.338      val typargs = Sign.const_typargs thy (c, ty);
   1.339      val typidx = find_index (fn TFree (w, _) => Name.aT = w | _ => false) typargs;
   1.340 -  in (c, (ty, (rhs, typidx))) end;
   1.341 +  in (c, (rhs, (ty, typidx))) end;
   1.342  
   1.343  fun add_const_in_class class ((c, rhs), syn) thy =
   1.344    let
   1.345 @@ -771,10 +795,9 @@
   1.346          val n2 = NameSpace.qualifier n1;
   1.347          val n3 = NameSpace.base n1;
   1.348        in NameSpace.implode [n2, prfx, n3] end;
   1.349 -    val constrain_sort = curry (Sorts.inter_sort (Sign.classes_of thy)) [class];
   1.350      val rhs' = export_fixes thy class rhs;
   1.351      val subst_typ = Term.map_type_tfree (fn var as (w, sort) =>
   1.352 -      if w = Name.aT then TFree (w, constrain_sort sort) else TFree var);
   1.353 +      if w = Name.aT then TFree (w, [class]) else TFree var);
   1.354      val ty' = Term.fastype_of rhs';
   1.355      val ty'' = subst_typ ty';
   1.356      val c' = mk_name c;
   1.357 @@ -783,12 +806,13 @@
   1.358      fun interpret def thy =
   1.359        let
   1.360          val def' = symmetric def;
   1.361 -        val def_eq = Thm.prop_of def';
   1.362 -        val entry = mk_operation_entry thy (c', rhs);
   1.363 +        val def_eq = (map_types Logic.unvarifyT o Thm.prop_of) def';
   1.364        in
   1.365          thy
   1.366          |> class_interpretation class [def'] [def_eq]
   1.367 -        |> register_const class (entry, def')
   1.368 +        |> Sign.add_const_constraint (c', SOME ty'')
   1.369 +        |> `(fn thy => mk_operation_entry thy (c', rhs))
   1.370 +        |-> (fn entry => register_operation class (entry, SOME def'))
   1.371        end;
   1.372    in
   1.373      thy
   1.374 @@ -798,7 +822,6 @@
   1.375      |> Sign.sticky_prefix prfx
   1.376      |> PureThy.add_defs_i false [(def, [])]
   1.377      |-> (fn [def] => interpret def)
   1.378 -    |> Sign.add_const_constraint (c', SOME ty'')
   1.379      |> Sign.restore_naming thy
   1.380      |> pair c'
   1.381    end;
   1.382 @@ -818,10 +841,11 @@
   1.383      val c' = mk_name c;
   1.384      val rhs' = export_fixes thy class rhs;
   1.385      val ty' = fastype_of rhs';
   1.386 +    val entry = mk_operation_entry thy (c', rhs);
   1.387    in
   1.388      thy
   1.389      |> Sign.notation true prmode [(Const (c', ty'), syn)]
   1.390 -    |> register_abbrev class (c', ty')
   1.391 +    |> register_operation class (entry, NONE)
   1.392      |> pair c'
   1.393    end;
   1.394