1.1 --- a/src/Pure/axclass.ML Sun Apr 25 21:18:04 2010 +0200
1.2 +++ b/src/Pure/axclass.ML Sun Apr 25 22:50:47 2010 +0200
1.3 @@ -44,6 +44,18 @@
1.4
1.5 (** theory data **)
1.6
1.7 +(* axclass info *)
1.8 +
1.9 +type info =
1.10 + {def: thm,
1.11 + intro: thm,
1.12 + axioms: thm list,
1.13 + params: (string * typ) list};
1.14 +
1.15 +fun make_axclass (def, intro, axioms, params): info =
1.16 + {def = def, intro = intro, axioms = axioms, params = params};
1.17 +
1.18 +
1.19 (* class parameters (canonical order) *)
1.20
1.21 type param = string * class;
1.22 @@ -55,85 +67,109 @@
1.23 " for " ^ Pretty.string_of_sort pp [c] ^
1.24 (if c = c' then "" else " and " ^ Pretty.string_of_sort pp [c'])));
1.25
1.26 -fun merge_params _ ([], qs) = qs
1.27 - | merge_params pp (ps, qs) =
1.28 - fold_rev (fn q => if member (op =) ps q then I else add_param pp q) qs ps;
1.29 -
1.30 -
1.31 -(* axclass info *)
1.32 -
1.33 -type info =
1.34 - {def: thm,
1.35 - intro: thm,
1.36 - axioms: thm list,
1.37 - params: (string * typ) list};
1.38 -
1.39 -type axclasses = info Symtab.table * param list;
1.40 -
1.41 -fun make_axclass ((def, intro, axioms), params): info =
1.42 - {def = def, intro = intro, axioms = axioms, params = params};
1.43 -
1.44 -fun merge_axclasses pp ((tab1, params1), (tab2, params2)) : axclasses =
1.45 - (Symtab.merge (K true) (tab1, tab2), merge_params pp (params1, params2));
1.46 -
1.47 -
1.48 -(* instances *)
1.49 -
1.50 -val classrel_prefix = "classrel_";
1.51 -val arity_prefix = "arity_";
1.52 -
1.53 -type instances =
1.54 - (thm * proof) Symreltab.table * (*classrel theorems*)
1.55 - ((class * sort list) * ((thm * string) * proof)) list Symtab.table; (*arity theorems with theory name*)
1.56 -
1.57 -(*transitive closure of classrels and arity completion is done in Theory.at_begin hook*)
1.58 -fun merge_instances ((classrel1, arities1): instances, (classrel2, arities2)) =
1.59 - (Symreltab.join (K fst) (classrel1, classrel2),
1.60 - Symtab.join (K (merge (eq_fst op =))) (arities1, arities2));
1.61 -
1.62 -
1.63 -(* instance parameters *)
1.64 -
1.65 -type inst_params =
1.66 - (string * thm) Symtab.table Symtab.table
1.67 - (*constant name ~> type constructor ~> (constant name, equation)*)
1.68 - * (string * string) Symtab.table; (*constant name ~> (constant name, type constructor)*)
1.69 -
1.70 -fun merge_inst_params ((const_param1, param_const1), (const_param2, param_const2)) =
1.71 - (Symtab.join (K (Symtab.merge (K true))) (const_param1, const_param2),
1.72 - Symtab.merge (K true) (param_const1, param_const2));
1.73 -
1.74
1.75 (* setup data *)
1.76
1.77 +datatype data = Data of
1.78 + {axclasses: info Symtab.table,
1.79 + params: param list,
1.80 + proven_classrels: (thm * proof) Symreltab.table,
1.81 + proven_arities: ((class * sort list) * ((thm * string) * proof)) list Symtab.table,
1.82 + (*arity theorems with theory name*)
1.83 + inst_params:
1.84 + (string * thm) Symtab.table Symtab.table *
1.85 + (*constant name ~> type constructor ~> (constant name, equation)*)
1.86 + (string * string) Symtab.table (*constant name ~> (constant name, type constructor)*),
1.87 + diff_merge_classrels: (class * class) list};
1.88 +
1.89 +fun make_data
1.90 + (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) =
1.91 + Data {axclasses = axclasses, params = params, proven_classrels = proven_classrels,
1.92 + proven_arities = proven_arities, inst_params = inst_params,
1.93 + diff_merge_classrels = diff_merge_classrels};
1.94 +
1.95 structure Data = Theory_Data_PP
1.96 (
1.97 - type T = axclasses * ((instances * inst_params) * (class * class) list);
1.98 - val empty = ((Symtab.empty, []), (((Symreltab.empty, Symtab.empty), (Symtab.empty, Symtab.empty)), []));
1.99 + type T = data;
1.100 + val empty =
1.101 + make_data (Symtab.empty, [], Symreltab.empty, Symtab.empty, (Symtab.empty, Symtab.empty), []);
1.102 val extend = I;
1.103 - fun merge pp ((axclasses1, ((instances1, inst_params1), diff_merge_classrels1)),
1.104 - (axclasses2, ((instances2, inst_params2), diff_merge_classrels2))) =
1.105 + fun merge pp
1.106 + (Data {axclasses = axclasses1, params = params1, proven_classrels = proven_classrels1,
1.107 + proven_arities = proven_arities1, inst_params = inst_params1,
1.108 + diff_merge_classrels = diff_merge_classrels1},
1.109 + Data {axclasses = axclasses2, params = params2, proven_classrels = proven_classrels2,
1.110 + proven_arities = proven_arities2, inst_params = inst_params2,
1.111 + diff_merge_classrels = diff_merge_classrels2}) =
1.112 let
1.113 - val (classrels1, classrels2) = pairself (Symreltab.keys o fst) (instances1, instances2);
1.114 - val diff_merge_classrels =
1.115 + val axclasses' = Symtab.merge (K true) (axclasses1, axclasses2);
1.116 + val params' =
1.117 + if null params1 then params2
1.118 + else fold_rev (fn q => if member (op =) params1 q then I else add_param pp q) params2 params1;
1.119 +
1.120 + (*transitive closure of classrels and arity completion is done in Theory.at_begin hook*)
1.121 + val proven_classrels' = Symreltab.join (K #1) (proven_classrels1, proven_classrels2);
1.122 + val proven_arities' =
1.123 + Symtab.join (K (Library.merge (eq_fst op =))) (proven_arities1, proven_arities2);
1.124 +
1.125 + val classrels1 = Symreltab.keys proven_classrels1;
1.126 + val classrels2 = Symreltab.keys proven_classrels2;
1.127 + val diff_merge_classrels' =
1.128 subtract (op =) classrels1 classrels2 @
1.129 subtract (op =) classrels2 classrels1 @
1.130 diff_merge_classrels1 @ diff_merge_classrels2;
1.131 +
1.132 + val inst_params' =
1.133 + (Symtab.join (K (Symtab.merge (K true))) (#1 inst_params1, #1 inst_params2),
1.134 + Symtab.merge (K true) (#2 inst_params1, #2 inst_params2));
1.135 in
1.136 - (merge_axclasses pp (axclasses1, axclasses2),
1.137 - ((merge_instances (instances1, instances2), merge_inst_params (inst_params1, inst_params2)),
1.138 - diff_merge_classrels))
1.139 + make_data (axclasses', params', proven_classrels', proven_arities', inst_params',
1.140 + diff_merge_classrels')
1.141 end;
1.142 );
1.143
1.144 +fun map_data f =
1.145 + Data.map (fn Data {axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels} =>
1.146 + make_data (f (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels)));
1.147 +
1.148 +fun map_axclasses f =
1.149 + map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) =>
1.150 + (f axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels));
1.151 +
1.152 +fun map_params f =
1.153 + map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) =>
1.154 + (axclasses, f params, proven_classrels, proven_arities, inst_params, diff_merge_classrels));
1.155 +
1.156 +fun map_proven_classrels f =
1.157 + map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) =>
1.158 + (axclasses, params, f proven_classrels, proven_arities, inst_params, diff_merge_classrels));
1.159 +
1.160 +fun map_proven_arities f =
1.161 + map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) =>
1.162 + (axclasses, params, proven_classrels, f proven_arities, inst_params, diff_merge_classrels));
1.163 +
1.164 +fun map_inst_params f =
1.165 + map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) =>
1.166 + (axclasses, params, proven_classrels, proven_arities, f inst_params, diff_merge_classrels));
1.167 +
1.168 +val clear_diff_merge_classrels =
1.169 + map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, _) =>
1.170 + (axclasses, params, proven_classrels, proven_arities, inst_params, []));
1.171 +
1.172 +val rep_data = Data.get #> (fn Data args => args);
1.173 +
1.174 +val axclasses_of = #axclasses o rep_data;
1.175 +val params_of = #params o rep_data;
1.176 +val proven_classrels_of = #proven_classrels o rep_data;
1.177 +val proven_arities_of = #proven_arities o rep_data;
1.178 +val inst_params_of = #inst_params o rep_data;
1.179 +val diff_merge_classrels_of = #diff_merge_classrels o rep_data;
1.180 +
1.181
1.182 (* maintain axclasses *)
1.183
1.184 -val get_axclasses = #1 o Data.get;
1.185 -val map_axclasses = Data.map o apfst;
1.186 -
1.187 fun get_info thy c =
1.188 - (case Symtab.lookup (#1 (get_axclasses thy)) c of
1.189 + (case Symtab.lookup (axclasses_of thy) c of
1.190 SOME info => info
1.191 | NONE => error ("No such axclass: " ^ quote c));
1.192
1.193 @@ -143,40 +179,40 @@
1.194 val classes = Sign.all_classes thy;
1.195 in map (Thm.class_triv thy) classes @ fold add_intro classes [] end;
1.196
1.197 +
1.198 +(* maintain params *)
1.199 +
1.200 fun all_params_of thy S =
1.201 - let val params = #2 (get_axclasses thy);
1.202 + let val params = params_of thy;
1.203 in fold (fn (x, c) => if Sign.subsort thy (S, [c]) then cons x else I) params [] end;
1.204
1.205 -fun class_of_param thy = AList.lookup (op =) (#2 (get_axclasses thy));
1.206 +fun class_of_param thy = AList.lookup (op =) (params_of thy);
1.207
1.208
1.209 (* maintain instances *)
1.210
1.211 +val classrel_prefix = "classrel_";
1.212 +val arity_prefix = "arity_";
1.213 +
1.214 fun instance_name (a, c) = Long_Name.base_name c ^ "_" ^ Long_Name.base_name a;
1.215
1.216 -val get_instances = #1 o #1 o #2 o Data.get;
1.217 -val map_instances = Data.map o apsnd o apfst o apfst;
1.218 -
1.219 -val get_diff_merge_classrels = #2 o #2 o Data.get;
1.220 -val clear_diff_merge_classrels = Data.map (apsnd (apsnd (K [])));
1.221 -
1.222
1.223 fun the_classrel thy (c1, c2) =
1.224 - (case Symreltab.lookup (#1 (get_instances thy)) (c1, c2) of
1.225 + (case Symreltab.lookup (proven_classrels_of thy) (c1, c2) of
1.226 SOME classrel => classrel
1.227 | NONE => error ("Unproven class relation " ^
1.228 Syntax.string_of_classrel (ProofContext.init thy) [c1, c2]));
1.229
1.230 -fun the_classrel_thm thy = Thm.transfer thy o fst o the_classrel thy;
1.231 -fun the_classrel_prf thy = snd o the_classrel thy;
1.232 +fun the_classrel_thm thy = Thm.transfer thy o #1 o the_classrel thy;
1.233 +fun the_classrel_prf thy = #2 o the_classrel thy;
1.234
1.235 fun put_trancl_classrel ((c1, c2), th) thy =
1.236 let
1.237 val cert = Thm.cterm_of thy;
1.238 val certT = Thm.ctyp_of thy;
1.239
1.240 - val classrels = fst (get_instances thy);
1.241 val classes = Sorts.classes_of (Sign.classes_of thy);
1.242 + val classrels = proven_classrels_of thy;
1.243
1.244 fun reflcl_classrel (c1', c2') =
1.245 if c1' = c2'
1.246 @@ -187,7 +223,7 @@
1.247 val th' = ((reflcl_classrel (c1_pred, c1) RS th) RS reflcl_classrel (c2, c2_succ))
1.248 |> Drule.instantiate' [SOME (certT (TVar ((Name.aT, 0), [])))] []
1.249 |> Thm.close_derivation;
1.250 - val prf' = th' |> Thm.proof_of;
1.251 + val prf' = Thm.proof_of th';
1.252 in ((c1_pred, c2_succ), (th', prf')) end;
1.253
1.254 val new_classrels =
1.255 @@ -197,38 +233,36 @@
1.256 val needed = not (null new_classrels);
1.257 in
1.258 (needed,
1.259 - if needed then
1.260 - thy |> map_instances (fn (classrels, arities) =>
1.261 - (classrels |> fold Symreltab.update new_classrels, arities))
1.262 - else thy)
1.263 + if needed then map_proven_classrels (fold Symreltab.update new_classrels) thy
1.264 + else thy)
1.265 end;
1.266
1.267 fun complete_classrels thy =
1.268 let
1.269 - val diff_merge_classrels = get_diff_merge_classrels thy;
1.270 - val classrels = fst (get_instances thy);
1.271 + val classrels = proven_classrels_of thy;
1.272 + val diff_merge_classrels = diff_merge_classrels_of thy;
1.273 val (needed, thy') = (false, thy) |>
1.274 fold (fn c12 => fn (needed, thy) =>
1.275 - put_trancl_classrel (c12, Symreltab.lookup classrels c12 |> the |> fst) thy
1.276 + put_trancl_classrel (c12, Symreltab.lookup classrels c12 |> the |> #1) thy
1.277 |>> (fn b => needed orelse b))
1.278 diff_merge_classrels;
1.279 in
1.280 if null diff_merge_classrels then NONE
1.281 - else thy' |> clear_diff_merge_classrels |> SOME
1.282 + else SOME (clear_diff_merge_classrels thy')
1.283 end;
1.284
1.285
1.286 fun the_arity thy a (c, Ss) =
1.287 - (case AList.lookup (op =) (Symtab.lookup_list (#2 (get_instances thy)) a) (c, Ss) of
1.288 + (case AList.lookup (op =) (Symtab.lookup_list (proven_arities_of thy) a) (c, Ss) of
1.289 SOME arity => arity
1.290 | NONE => error ("Unproven type arity " ^
1.291 Syntax.string_of_arity (ProofContext.init thy) (a, Ss, [c])));
1.292
1.293 -fun the_arity_thm thy a c_Ss = the_arity thy a c_Ss |> fst |> fst |> Thm.transfer thy;
1.294 -fun the_arity_prf thy a c_Ss = the_arity thy a c_Ss |> snd;
1.295 +fun the_arity_thm thy a c_Ss = the_arity thy a c_Ss |> #1 |> #1 |> Thm.transfer thy;
1.296 +fun the_arity_prf thy a c_Ss = the_arity thy a c_Ss |> #2;
1.297
1.298 fun thynames_of_arity thy (c, a) =
1.299 - Symtab.lookup_list (#2 (get_instances thy)) a
1.300 + Symtab.lookup_list (proven_arities_of thy) a
1.301 |> map_filter (fn ((c', _), ((_, name),_)) => if c = c' then SOME name else NONE)
1.302 |> rev;
1.303
1.304 @@ -256,34 +290,30 @@
1.305 val arity' = (t, ((c, Ss), ((th, Context.theory_name thy), Thm.proof_of th)));
1.306 in
1.307 thy
1.308 - |> map_instances (fn (classrel, arities) => (classrel,
1.309 - arities
1.310 - |> Symtab.insert_list (eq_fst op =) arity'
1.311 - |> insert_arity_completions thy arity'
1.312 - |> snd))
1.313 + |> map_proven_arities
1.314 + (Symtab.insert_list (eq_fst op =) arity' #>
1.315 + insert_arity_completions thy arity' #> snd)
1.316 end;
1.317
1.318 fun complete_arities thy =
1.319 let
1.320 - val arities = snd (get_instances thy);
1.321 + val arities = proven_arities_of thy;
1.322 val (finished, arities') = arities
1.323 |> fold_map (insert_arity_completions thy) (Symtab.dest_list arities);
1.324 in
1.325 - if forall I finished then NONE
1.326 - else SOME (thy |> map_instances (fn (classrel, _) => (classrel, arities')))
1.327 + if forall I finished
1.328 + then NONE
1.329 + else SOME (map_proven_arities (K arities') thy)
1.330 end;
1.331
1.332 val _ = Context.>> (Context.map_theory
1.333 - (Theory.at_begin complete_classrels #> Theory.at_begin complete_arities))
1.334 + (Theory.at_begin complete_classrels #> Theory.at_begin complete_arities));
1.335
1.336
1.337 (* maintain instance parameters *)
1.338
1.339 -val get_inst_params = #2 o #1 o #2 o Data.get;
1.340 -val map_inst_params = Data.map o apsnd o apfst o apsnd;
1.341 -
1.342 fun get_inst_param thy (c, tyco) =
1.343 - (case Symtab.lookup (the_default Symtab.empty (Symtab.lookup (#1 (get_inst_params thy)) c)) tyco of
1.344 + (case Symtab.lookup (the_default Symtab.empty (Symtab.lookup (#1 (inst_params_of thy)) c)) tyco of
1.345 SOME c' => c'
1.346 | NONE => error ("No instance parameter for constant " ^ quote c ^ " on type " ^ quote tyco));
1.347
1.348 @@ -291,11 +321,11 @@
1.349 (map_inst_params o apfst o Symtab.map_default (c, Symtab.empty)) (Symtab.update_new (tyco, inst))
1.350 #> (map_inst_params o apsnd) (Symtab.update_new (fst inst, (c, tyco)));
1.351
1.352 -val inst_of_param = Symtab.lookup o snd o get_inst_params;
1.353 +val inst_of_param = Symtab.lookup o #2 o inst_params_of;
1.354 val param_of_inst = fst oo get_inst_param;
1.355
1.356 fun inst_thms thy =
1.357 - (Symtab.fold (Symtab.fold (cons o snd o snd) o snd) o fst) (get_inst_params thy) [];
1.358 + Symtab.fold (Symtab.fold (cons o #2 o #2) o #2) (#1 (inst_params_of thy)) [];
1.359
1.360 fun get_inst_tyco consts = try (fst o dest_Type o the_single o Consts.typargs consts);
1.361
1.362 @@ -339,8 +369,6 @@
1.363 cert_classrel thy (pairself (ProofContext.read_class (ProofContext.init thy)) raw_rel)
1.364 handle TYPE (msg, _, _) => error msg;
1.365
1.366 -val shyps_topped = forall null o #shyps o Thm.rep_thm;
1.367 -
1.368
1.369 (* declaration and definition of instances of overloaded constants *)
1.370
1.371 @@ -392,6 +420,8 @@
1.372
1.373 (* primitive rules *)
1.374
1.375 +val shyps_topped = forall null o #shyps o Thm.rep_thm;
1.376 +
1.377 fun add_classrel raw_th thy =
1.378 let
1.379 val th = Thm.strip_shyps (Thm.transfer thy raw_th);
1.380 @@ -562,16 +592,15 @@
1.381
1.382 (* result *)
1.383
1.384 - val axclass = make_axclass ((def, intro, axioms), params);
1.385 + val axclass = make_axclass (def, intro, axioms, params);
1.386 val result_thy =
1.387 facts_thy
1.388 |> fold (snd oo put_trancl_classrel) (map (pair class) super ~~ classrel)
1.389 |> Sign.qualified_path false bconst
1.390 |> PureThy.note_thmss "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) |> snd
1.391 |> Sign.restore_naming facts_thy
1.392 - |> map_axclasses (fn (axclasses, parameters) =>
1.393 - (Symtab.update (class, axclass) axclasses,
1.394 - fold (fn (x, _) => add_param pp (x, class)) params parameters));
1.395 + |> map_axclasses (Symtab.update (class, axclass))
1.396 + |> map_params (fold (fn (x, _) => add_param pp (x, class)) params);
1.397
1.398 in (class, result_thy) end;
1.399