1.1 --- a/src/HOL/record.ML Wed Apr 29 11:38:52 1998 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,430 +0,0 @@
1.4 -(* Title: HOL/record.ML
1.5 - ID: $Id$
1.6 - Author: Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
1.7 -
1.8 -Internal interface for records.
1.9 -*)
1.10 -
1.11 -
1.12 -signature RECORD =
1.13 -sig
1.14 - val add_record:
1.15 - (string list * bstring) -> string option ->
1.16 - (bstring * string) list -> theory -> theory
1.17 - val add_record_i:
1.18 - (string list * bstring) -> (typ list * string) option ->
1.19 - (bstring * typ) list -> theory -> theory
1.20 -end;
1.21 -
1.22 -structure Record: RECORD =
1.23 -struct
1.24 -
1.25 -val base = Sign.base_name;
1.26 -
1.27 -(* FIXME move to Pure/library.ML *)
1.28 -fun set_minus xs [] = xs
1.29 - | set_minus xs (y::ys) = set_minus (xs \ y) ys;
1.30 -(* FIXME *)
1.31 -
1.32 -(* FIXME move to Pure/sign.ML *)
1.33 -fun of_sort sg =
1.34 - Sorts.of_sort
1.35 - (#classrel (Type.rep_tsig (#tsig (Sign.rep_sg sg))))
1.36 - (#arities (Type.rep_tsig (#tsig (Sign.rep_sg sg))));
1.37 -(* FIXME *)
1.38 -
1.39 -
1.40 -
1.41 -(** record info **)
1.42 -
1.43 -fun get_record thy name =
1.44 - let val table = ThyData.get_records thy
1.45 - in
1.46 - Symtab.lookup (table, name)
1.47 - end;
1.48 -
1.49 -fun put_record thy name info =
1.50 - let val table = ThyData.get_records thy
1.51 - in
1.52 - ThyData.put_records (Symtab.update ((name, info), table))
1.53 - end;
1.54 -
1.55 -local
1.56 - fun record_infos thy None = []
1.57 - | record_infos thy (Some info) =
1.58 - case #parent info of
1.59 - None => [info]
1.60 - | Some (_, parent) => record_infos thy (get_record thy parent) @ [info];
1.61 - fun record_parass thy info =
1.62 - (map (map (fn (str, _) => (str, 0)) o #args) (record_infos thy (Some info)))
1.63 - : indexname list list;
1.64 - fun record_argss thy info =
1.65 - map (fst o the) (tl (map #parent (record_infos thy (Some info)))) @
1.66 - [map TFree (#args info)];
1.67 -in
1.68 - fun record_field_names thy info =
1.69 - flat (map (map fst o #fields) (record_infos thy (Some info)));
1.70 - fun record_field_types thy info =
1.71 - let
1.72 - val paras_args = map (op ~~) (record_parass thy info ~~ record_argss thy info);
1.73 - val raw_substs = map typ_subst_TVars paras_args;
1.74 - fun make_substs [] = []
1.75 - | make_substs (x::xs) = (foldr1 (op o) (rev (x::xs))) :: make_substs xs;
1.76 - val free_TFree = map (map (map_type_tfree (fn (str, s) => TVar((str, 0), s))));
1.77 - val raw_record_field_types = map (map snd o #fields) (record_infos thy (Some info))
1.78 - in
1.79 - flat (ListPair.map (fn (s, ts) => map s ts)
1.80 - (make_substs raw_substs, free_TFree raw_record_field_types))
1.81 - end;
1.82 -end;
1.83 -
1.84 -
1.85 -
1.86 -(** abstract syntax **)
1.87 -
1.88 -(* tuples *)
1.89 -
1.90 -val unitT = Type ("unit",[]);
1.91 -val unit = Const ("()",unitT);
1.92 -fun mk_prodT (T1, T2) = Type ("*", [T1,T2]);
1.93 -fun mk_Pair (t1, t2) =
1.94 - let val T1 = fastype_of t1
1.95 - and T2 = fastype_of t2
1.96 - in Const ("Pair", [T1, T2] ---> mk_prodT (T1,T2)) $ t1 $ t2 end;
1.97 -
1.98 -val mk_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq;
1.99 -
1.100 -fun dest_prodT (Type ("*", [T1, T2])) = (T1, T2)
1.101 - | dest_prodT T = raise TYPE ("dest_prodT: product type expected", [T], []);
1.102 -
1.103 -fun mk_fst pT = Const ("fst", pT --> fst (dest_prodT pT));
1.104 -fun mk_snd pT = Const ("snd", pT --> snd (dest_prodT pT));
1.105 -
1.106 -fun ap_fst t = mk_fst (fastype_of t) $ t;
1.107 -fun ap_snd t = mk_snd (fastype_of t) $ t;
1.108 -
1.109 -
1.110 -(* records *)
1.111 -
1.112 -fun selT T recT = recT --> T;
1.113 -fun updateT T recT = T --> recT --> recT;
1.114 -val base_free = Free o apfst base;
1.115 -val make_scheme_name = "make_scheme";
1.116 -val make_name = "make";
1.117 -fun def_suffix s = s ^ "_def";
1.118 -fun update_suffix s = s ^ "_update";
1.119 -fun make_schemeC full make_schemeT = Const (full make_scheme_name, make_schemeT);
1.120 -fun makeC full makeT = Const (full make_name, makeT);
1.121 -fun make_args_scheme full make_schemeT base_frees z =
1.122 - list_comb (make_schemeC full make_schemeT, base_frees) $ z;
1.123 -fun make_args full makeT base_frees =
1.124 - list_comb (makeC full makeT, base_frees);
1.125 -fun selC s T recT = Const (s, selT T recT);
1.126 -fun updateC s T recT = Const (update_suffix s, updateT T recT);
1.127 -fun frees xs = foldr add_typ_tfree_names (xs, []);
1.128 -
1.129 -
1.130 -
1.131 -(** constants, definitions, axioms **)
1.132 -
1.133 -(* constant declarations for make, selectors and update *)
1.134 -
1.135 -fun decls make_schemeT makeT selT updateT recT current_fields =
1.136 - let val make_scheme_decl = (make_scheme_name, make_schemeT, NoSyn);
1.137 - val make_decl = (make_name, makeT, NoSyn);
1.138 - val sel_decls = map (fn (c, T) => (c, selT T recT, NoSyn)) current_fields;
1.139 - val update_decls =
1.140 - map (fn (c, T) => (update_suffix c, updateT T recT, NoSyn)) current_fields
1.141 - in
1.142 - make_scheme_decl :: make_decl :: sel_decls @ update_decls
1.143 - end;
1.144 -
1.145 -
1.146 -(* definitions for make, selectors and update *)
1.147 -
1.148 -(*make*)
1.149 -fun make_defs make_schemeT makeT base_frees z thy =
1.150 - let
1.151 - val sign = sign_of thy;
1.152 - val full = Sign.full_name sign;
1.153 - val make_scheme_def =
1.154 - mk_defpair (make_args_scheme full make_schemeT base_frees z,
1.155 - foldr mk_Pair (base_frees, z));
1.156 - val make_def =
1.157 - mk_defpair (make_args full makeT base_frees,
1.158 - foldr mk_Pair (base_frees, unit))
1.159 - in
1.160 - make_scheme_def :: [make_def]
1.161 - end;
1.162 -
1.163 -(*selectors*)
1.164 -fun sel_defs recT r all_fields current_fullfields =
1.165 - let
1.166 - val prefix_len = length all_fields - length current_fullfields;
1.167 - val sel_terms =
1.168 - map (fn k => ap_fst o funpow k ap_snd)
1.169 - (prefix_len upto length all_fields - 1)
1.170 - in
1.171 - ListPair.map
1.172 - (fn ((s, T), t) => mk_defpair (selC s T recT $ r, t r))
1.173 - (current_fullfields, sel_terms)
1.174 - end;
1.175 -
1.176 -(*update*)
1.177 -fun update_defs recT r all_fields current_fullfields thy =
1.178 - let
1.179 - val len_all_fields = length all_fields;
1.180 - fun sel_last r = funpow len_all_fields ap_snd r;
1.181 - fun update_def_s (s, T) =
1.182 - let val updates = map (fn (s', T') =>
1.183 - if s = s' then base_free (s, T) else selC s' T' recT $ r)
1.184 - all_fields
1.185 - in
1.186 - mk_defpair (updateC s T recT $ base_free (s, T) $ r,
1.187 - foldr mk_Pair (updates, sel_last r))
1.188 - end;
1.189 - in
1.190 - map update_def_s current_fullfields
1.191 - end
1.192 -
1.193 -
1.194 -(* theorems for make, selectors and update *)
1.195 -
1.196 -(*preparations*)
1.197 -fun get_all_selector_defs all_fields full thy =
1.198 - map (fn (s, T) => get_axiom thy (def_suffix s)) all_fields;
1.199 -fun get_all_update_defs all_fields full thy =
1.200 - map (fn (s, T) => get_axiom thy (def_suffix (update_suffix s))) all_fields;
1.201 -fun get_make_scheme_def full thy = get_axiom thy (full (def_suffix make_scheme_name));
1.202 -fun get_make_def full thy = get_axiom thy (full (def_suffix make_name));
1.203 -fun all_rec_defs all_fields full thy =
1.204 - get_make_scheme_def full thy :: get_make_def full thy ::
1.205 - get_all_selector_defs all_fields full thy @ get_all_update_defs all_fields full thy;
1.206 -fun prove_goal_s goal_s all_fields full thy =
1.207 - map (fn (s,T) =>
1.208 - (prove_goalw_cterm (all_rec_defs all_fields full thy)
1.209 - (cterm_of (sign_of thy) (mk_eq (goal_s (s,T))))
1.210 - (K [simp_tac (HOL_basic_ss addsimps [fst_conv,snd_conv]) 1])))
1.211 - all_fields;
1.212 -
1.213 -(*si (make(_scheme) x1 ... xi ... xn) = xi*)
1.214 -fun sel_make_scheme_thms recT make_schemeT base_frees z all_fields full thy =
1.215 - let
1.216 - fun sel_make_scheme_s (s, T) =
1.217 - (selC s T recT $ make_args_scheme full make_schemeT base_frees z, base_free(s,T))
1.218 - in
1.219 - prove_goal_s sel_make_scheme_s all_fields full thy
1.220 - end;
1.221 -
1.222 -fun sel_make_thms recT_unitT makeT base_frees all_fields full thy =
1.223 - let
1.224 - fun sel_make_s (s, T) =
1.225 - (selC s T recT_unitT $ make_args full makeT base_frees, Free(base s,T))
1.226 - in
1.227 - prove_goal_s sel_make_s all_fields full thy
1.228 - end;
1.229 -
1.230 -(*si_update xia (make(_scheme) x1 ... xi ... xn) = (make x1 ... xia ... xn)*)
1.231 -fun update_make_scheme_thms recT make_schemeT base_frees z all_fields full thy =
1.232 - let
1.233 - fun update_make_scheme_s (s, T) =
1.234 - (updateC s T recT $ base_free(s ^ "'", T) $
1.235 - make_args_scheme full make_schemeT base_frees z,
1.236 - make_args_scheme full make_schemeT
1.237 - (map (fn t => if t = base_free(s, T) then base_free(s ^ "'", T) else t) base_frees) z)
1.238 - in
1.239 - prove_goal_s update_make_scheme_s all_fields full thy
1.240 - end;
1.241 -
1.242 -fun update_make_thms recT_unitT makeT base_frees all_fields full thy =
1.243 - let
1.244 - fun update_make_s (s, T) =
1.245 - (updateC s T recT_unitT $ base_free(s ^ "'", T) $
1.246 - make_args full makeT base_frees,
1.247 - make_args full makeT
1.248 - (map (fn t => if t = base_free(s, T) then base_free(s ^ "'", T) else t) base_frees))
1.249 - in
1.250 - prove_goal_s update_make_s all_fields full thy
1.251 - end;
1.252 -
1.253 -
1.254 -
1.255 -(** errors **)
1.256 -
1.257 -fun check_duplicate_fields all_field_names =
1.258 - let val has_dupl = findrep all_field_names
1.259 - in
1.260 - if null has_dupl then []
1.261 - else ["Duplicate field declaration: " ^ quote (hd has_dupl) ^
1.262 - " (Double might be in ancestor)"]
1.263 - end;
1.264 -
1.265 -fun check_parent None name thy = []
1.266 - | check_parent (Some (args, parent)) name thy =
1.267 - let
1.268 - val opt_info = get_record thy parent;
1.269 - val sign = sign_of thy;
1.270 - fun check_sorts [] [] = []
1.271 - | check_sorts ((str, sort)::xs) (y::ys) =
1.272 - if of_sort sign (y, sort)
1.273 - then check_sorts xs ys
1.274 - else ["Sort of " ^
1.275 - quote (Pretty.string_of (Sign.pretty_typ sign y)) ^
1.276 - " does not match parent declaration"]
1.277 - in
1.278 - case opt_info of
1.279 - None => ["Parent " ^ quote parent ^" not defined"]
1.280 - | Some {args = pargs, parent = pparent, fields = pfields} =>
1.281 - if (length args = length pargs)
1.282 - then check_sorts pargs args
1.283 - else ["Mismatching arities for parent " ^ quote (base parent)]
1.284 - end;
1.285 -
1.286 -fun check_duplicate_records thy full_name =
1.287 - if is_none (get_record thy full_name) then []
1.288 - else ["Duplicate record declaration"];
1.289 -
1.290 -fun check_duplicate_args raw_args =
1.291 - let val has_dupl = findrep raw_args
1.292 - in
1.293 - if null has_dupl then []
1.294 - else ["Duplicate parameter: " ^ quote (hd has_dupl)]
1.295 - end;
1.296 -
1.297 -fun check_raw_args raw_args free_vars thy =
1.298 - let
1.299 - val free_vars_names = map fst free_vars;
1.300 - val diff_set = set_minus free_vars_names raw_args;
1.301 - val default_sort = Type.defaultS ((#tsig o Sign.rep_sg) (sign_of thy));
1.302 - val assign_sorts =
1.303 - map (fn x => case assoc (free_vars, x) of
1.304 - None => (x, default_sort)
1.305 - | Some sort => (x, sort)) raw_args
1.306 - in
1.307 - if free_vars_names subset raw_args
1.308 - then ([], assign_sorts)
1.309 - else (["Free type variable(s): " ^
1.310 - (foldr1 (fn (s, s') => s ^ ", " ^ s') (map quote diff_set))],
1.311 - [])
1.312 - end;
1.313 -
1.314 -
1.315 -
1.316 -(** ext_record **)
1.317 -
1.318 -fun ext_record (args, name) opt_parent current_fields thy =
1.319 - let
1.320 - val full_name = Sign.full_name (sign_of thy) name;
1.321 - val thy = thy |> Theory.add_path name;
1.322 - val sign = sign_of thy;
1.323 - val full = Sign.full_name sign;
1.324 -
1.325 - val current_fullfields = map (apfst full) current_fields;
1.326 - val info = {args = args, fields = current_fullfields, parent = opt_parent};
1.327 - val thy = thy |> put_record thy full_name info;
1.328 - val all_types = record_field_types thy info;
1.329 - val all_fields = record_field_names thy info ~~ all_types;
1.330 - val base_frees = map base_free all_fields;
1.331 -
1.332 - val tfrees = frees all_types;
1.333 - val zeta = variant tfrees "'z";
1.334 - val zetaT = TFree (zeta, HOLogic.termS);
1.335 - val z = base_free ("z", zetaT);
1.336 - val recT = foldr mk_prodT (all_types, zetaT);
1.337 - val recT_unitT = foldr mk_prodT (all_types, unitT);
1.338 - val make_schemeT = (all_types @ [zetaT]) ---> recT;
1.339 - val makeT = all_types ---> recT_unitT;
1.340 - val r = base_free ("r", recT);
1.341 -
1.342 - val errors = check_duplicate_fields (map base (record_field_names thy info))
1.343 - in
1.344 - if not (null errors)
1.345 - then error (cat_lines errors) else
1.346 - let val thy =
1.347 - thy |> Theory.add_path ".."
1.348 - |> Theory.add_tyabbrs_i [(name ^ "_scheme", tfrees @ [zeta], recT, NoSyn)]
1.349 - |> Theory.add_tyabbrs_i [(name, tfrees, recT_unitT, NoSyn)]
1.350 - |> Theory.add_path name
1.351 - |> Theory.add_consts_i (decls make_schemeT makeT selT updateT recT current_fields)
1.352 - |> Theory.add_defs_i
1.353 - ((make_defs make_schemeT makeT base_frees z thy) @
1.354 - (sel_defs recT r all_fields current_fullfields) @
1.355 - (update_defs recT r all_fields current_fullfields thy))
1.356 - in
1.357 - thy |> PureThy.store_thmss
1.358 - [("record_simps",
1.359 - sel_make_scheme_thms recT make_schemeT base_frees z all_fields full thy @
1.360 - sel_make_thms recT_unitT makeT base_frees all_fields full thy @
1.361 - update_make_scheme_thms recT make_schemeT base_frees z all_fields full thy @
1.362 - update_make_thms recT_unitT makeT base_frees all_fields full thy )]
1.363 - |> Theory.add_path ".."
1.364 - end
1.365 -
1.366 -(* @ update_make_thms @
1.367 - update_update_thms @ sel_update_thms)] *)
1.368 -
1.369 - end;
1.370 -
1.371 -
1.372 -
1.373 -(** external interfaces **)
1.374 -
1.375 -(* add_record *)
1.376 -
1.377 -fun add_record_aux prep_typ prep_parent (raw_args, name) raw_parent raw_fields thy =
1.378 - let
1.379 - val _ = require_thy thy "Prod" "record definitions";
1.380 - val sign = sign_of thy;
1.381 - val full_name = Sign.full_name sign name;
1.382 - val make_assocs = map (fn (a, b) => ((a, ~1), b));
1.383 -
1.384 - val parent = apsome (prep_parent sign) raw_parent;
1.385 - val parent_args = if_none (apsome fst parent) [];
1.386 - val parent_assoc = make_assocs (foldr (op union) ((map typ_tfrees parent_args), []));
1.387 -
1.388 - fun prepare_fields ass [] = []
1.389 - | prepare_fields ass ((name, str)::xs) =
1.390 - let val type_of_name = prep_typ sign ass str
1.391 - in (name, type_of_name)::
1.392 - (prepare_fields (ass union (make_assocs (typ_tfrees type_of_name))) xs)
1.393 - end;
1.394 - val fields = prepare_fields (parent_assoc) raw_fields;
1.395 - val fields_types = map snd fields;
1.396 - val free_vars = foldr (op union) ((map typ_tfrees fields_types), []);
1.397 -
1.398 - val check_args = check_raw_args raw_args free_vars thy;
1.399 - val args = snd check_args;
1.400 -
1.401 - val errors = (check_parent parent name thy) @
1.402 - (check_duplicate_records thy full_name) @
1.403 - (check_duplicate_args raw_args) @
1.404 - (fst check_args)
1.405 - in
1.406 - if not (null errors)
1.407 - then error (cat_lines errors)
1.408 - else ext_record (args, name) parent fields thy
1.409 - end
1.410 - handle ERROR =>
1.411 - error ("The error(s) above occurred in record declaration " ^ quote name);
1.412 -
1.413 -
1.414 -(* internalization methods *)
1.415 -
1.416 -fun read_parent sign name =
1.417 - (case Sign.read_raw_typ (sign, K None) name of
1.418 - Type (name, Ts) => (Ts, name)
1.419 - | _ => error ("Malformed parent specification: " ^ name));
1.420 -
1.421 -fun read_typ sign ass name =
1.422 - Sign.read_typ (sign, curry assoc ass) name handle TYPE (msg, _, _) => error msg;
1.423 -
1.424 -fun cert_typ sign ass T =
1.425 - Sign.certify_typ sign T handle TYPE (msg, _, _) => error msg;
1.426 -
1.427 -
1.428 -(* add_record(_i) *)
1.429 -
1.430 -val add_record = add_record_aux read_typ read_parent;
1.431 -val add_record_i = add_record_aux cert_typ (K I);
1.432 -
1.433 -end;