src/HOL/Tools/record_package.ML
author paulson
Wed May 27 12:21:39 1998 +0200 (1998-05-27)
changeset 4970 8b65444edbb0
parent 4967 c9c481bc0216
child 5001 9de7fda0a6df
permissions -rw-r--r--
Changed require to requires for MLWorks
     1 (*  Title:      HOL/Tools/record_package.ML
     2     ID:         $Id$
     3     Author:     Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
     4 
     5 Extensible records with structural subtyping in HOL.
     6 
     7 TODO:
     8   - field types: typedef;
     9   - trfuns for record types;
    10   - operations and theorems: split, split_all/ex, ...;
    11   - field constructor: more specific type for snd component;
    12   - update_more operation;
    13   - field syntax: "..." for "... = more", "?..." for "?... = ?more";
    14 *)
    15 
    16 signature RECORD_PACKAGE =
    17 sig
    18   val moreS: sort
    19   val mk_fieldT: (string * typ) * typ -> typ
    20   val dest_fieldT: typ -> (string * typ) * typ
    21   val mk_field: (string * term) * term -> term
    22   val mk_fst: term -> term
    23   val mk_snd: term -> term
    24   val mk_recordT: (string * typ) list * typ -> typ
    25   val dest_recordT: typ -> (string * typ) list * typ
    26   val mk_record: (string * term) list * term -> term
    27   val mk_sel: term -> string -> term
    28   val mk_update: term -> string * term -> term
    29   val print_records: theory -> unit
    30   val add_record: (string list * bstring) -> string option
    31     -> (bstring * string) list -> theory -> theory
    32   val add_record_i: (string list * bstring) -> (typ list * string) option
    33     -> (bstring * typ) list -> theory -> theory
    34   val setup: (theory -> theory) list
    35 end;
    36 
    37 structure RecordPackage: RECORD_PACKAGE =
    38 struct
    39 
    40 
    41 (*** utilities ***)
    42 
    43 (* string suffixes *)
    44 
    45 fun suffix sfx s = s ^ sfx;
    46 
    47 fun unsuffix sfx s =
    48   let
    49     val cs = explode s;
    50     val prfx_len = size s - size sfx;
    51   in
    52     if prfx_len >= 0 andalso implode (drop (prfx_len, cs)) = sfx then
    53       implode (take (prfx_len, cs))
    54     else raise LIST "unsuffix"
    55   end;
    56 
    57 
    58 (* definitions and equations *)
    59 
    60 infix 0 :== === ;
    61 
    62 val (op :==) = Logic.mk_defpair;
    63 val (op ===) = HOLogic.mk_Trueprop o HOLogic.mk_eq;
    64 
    65 fun get_defs thy specs = map (PureThy.get_tthm thy o fst) specs;
    66 
    67 
    68 (* proof by simplification *)
    69 
    70 fun prove_simp thy simps =
    71   let
    72     val sign = Theory.sign_of thy;
    73     val ss = Simplifier.addsimps (HOL_basic_ss, map Attribute.thm_of simps);
    74 
    75     fun prove goal =
    76       Attribute.tthm_of
    77         (Goals.prove_goalw_cterm [] (Thm.cterm_of sign goal)
    78           (K [ALLGOALS (Simplifier.simp_tac ss)])
    79         handle ERROR => error ("The error(s) above occurred while trying to prove "
    80           ^ quote (Sign.string_of_term sign goal)));
    81   in prove end;
    82 
    83 
    84 
    85 (*** syntax operations ***)
    86 
    87 (** name components **)
    88 
    89 val moreN = "more";
    90 val schemeN = "_scheme";
    91 val fieldN = "_field";
    92 val field_typeN = "_field_type";
    93 val fstN = "_fst";
    94 val sndN = "_snd";
    95 val updateN = "_update";
    96 val makeN = "make";
    97 val make_schemeN = "make_scheme";
    98 
    99 
   100 
   101 (** tuple operations **)
   102 
   103 (* more type class *)
   104 
   105 val moreS = ["more"];
   106 
   107 
   108 (* types *)
   109 
   110 fun mk_fieldT ((c, T), U) = Type (suffix field_typeN c, [T, U]);
   111 
   112 fun dest_fieldT (typ as Type (c_field_type, [T, U])) =
   113       (case try (unsuffix field_typeN) c_field_type of
   114         None => raise TYPE ("dest_fieldT", [typ], [])
   115       | Some c => ((c, T), U))
   116   | dest_fieldT typ = raise TYPE ("dest_fieldT", [typ], []);
   117 
   118 
   119 (* constructors *)
   120 
   121 fun mk_fieldC U (c, T) = (suffix fieldN c, T --> U --> mk_fieldT ((c, T), U));
   122 
   123 fun mk_field ((c, t), u) =
   124   let val T = fastype_of t and U = fastype_of u
   125   in Const (suffix fieldN c, [T, U] ---> mk_fieldT ((c, T), U)) $ t $ u end;
   126 
   127 
   128 (* destructors *)
   129 
   130 fun mk_fstC U (c, T) = (suffix fstN c, mk_fieldT ((c, T), U) --> T);
   131 fun mk_sndC U (c, T) = (suffix sndN c, mk_fieldT ((c, T), U) --> U);
   132 
   133 fun dest_field fst_or_snd p =
   134   let
   135     val pT = fastype_of p;
   136     val ((c, T), U) = dest_fieldT pT;
   137     val (destN, destT) = if fst_or_snd then (fstN, T) else (sndN, U);
   138   in Const (suffix destN c, pT --> destT) $ p end;
   139 
   140 val mk_fst = dest_field true;
   141 val mk_snd = dest_field false;
   142 
   143 
   144 
   145 (** record operations **)
   146 
   147 (* types *)
   148 
   149 val mk_recordT = foldr mk_fieldT;
   150 
   151 fun dest_recordT T =
   152   (case try dest_fieldT T of
   153     None => ([], T)
   154   | Some (c_T, U) => apfst (cons c_T) (dest_recordT U));
   155 
   156 fun find_fieldT c rT =
   157   (case assoc (fst (dest_recordT rT), c) of
   158     None => raise TYPE ("find_field: " ^ c, [rT], [])
   159   | Some T => T);
   160 
   161 
   162 (* constructors *)
   163 
   164 val mk_record = foldr mk_field;
   165 
   166 
   167 (* selectors *)
   168 
   169 fun mk_selC rT (c, T) = (c, rT --> T);
   170 
   171 fun mk_sel r c =
   172   let val rT = fastype_of r
   173   in Const (mk_selC rT (c, find_fieldT c rT)) $ r end;
   174 
   175 val mk_moreC = mk_selC;
   176 
   177 fun mk_more r c =
   178   let val rT = fastype_of r
   179   in Const (mk_moreC rT (c, snd (dest_recordT rT))) $ r end;
   180 
   181 
   182 (* updates *)
   183 
   184 fun mk_updateC rT (c, T) = (suffix updateN c, T --> rT --> rT);
   185 
   186 fun mk_update r (c, x) =
   187   let val rT = fastype_of r
   188   in Const (mk_updateC rT (c, find_fieldT c rT)) $ x $ r end;
   189 
   190 
   191 (* make *)
   192 
   193 fun mk_makeC rT (c, Ts) = (c, Ts ---> rT);
   194 
   195 
   196 
   197 (** concrete syntax for records **)
   198 
   199 (* parse translations *)
   200 
   201 fun field_tr (Const ("_field", _) $ Free (name, _) $ arg) =
   202       Syntax.const (suffix fieldN name) $ arg
   203   | field_tr t = raise TERM ("field_tr", [t]);
   204 
   205 fun fields_tr (Const ("_fields", _) $ field $ fields) =
   206       field_tr field :: fields_tr fields
   207   | fields_tr field = [field_tr field];
   208 
   209 fun record_tr (*"_record"*) [fields] =
   210       foldr (op $) (fields_tr fields, HOLogic.unit)
   211   | record_tr (*"_record"*) ts = raise TERM ("record_tr", ts);
   212 
   213 fun record_scheme_tr (*"_record_scheme"*) [fields, more] =
   214       foldr (op $) (fields_tr fields, more)
   215   | record_scheme_tr (*"_record_scheme"*) ts = raise TERM ("record_scheme_tr", ts);
   216 
   217 
   218 (* print translations *)
   219 
   220 fun fields_tr' (tm as Const (name_field, _) $ arg $ more) =
   221       (case try (unsuffix fieldN) name_field of
   222         Some name =>
   223           apfst (cons (Syntax.const "_field" $ Syntax.free name $ arg)) (fields_tr' more)
   224       | None => ([], tm))
   225   | fields_tr' tm = ([], tm);
   226 
   227 fun record_tr' tm =
   228   let
   229     val (fields, more) = fields_tr' tm;
   230     val fields' = foldr1 (fn (f, fs) => Syntax.const "_fields" $ f $ fs) fields;
   231   in
   232     if HOLogic.is_unit more then Syntax.const "_record" $ fields'
   233     else Syntax.const "_record_scheme" $ fields' $ more
   234   end;
   235 
   236 fun field_tr' name [arg, more] = record_tr' (Syntax.const name $ arg $ more)
   237   | field_tr' _ _ = raise Match;
   238 
   239 
   240 
   241 (*** extend theory by record definition ***)
   242 
   243 (** record info **)
   244 
   245 (* type record_info and parent_info *)
   246 
   247 type record_info =
   248  {args: (string * sort) list,
   249   parent: (typ list * string) option,
   250   fields: (string * typ) list,
   251   simps: tthm list};
   252 
   253 type parent_info =
   254  {name: string,
   255   fields: (string * typ) list,
   256   simps: tthm list};
   257 
   258 
   259 (* theory data *)
   260 
   261 val recordsK = "HOL/records";
   262 exception Records of record_info Symtab.table;
   263 
   264 fun print_records thy = Display.print_data thy recordsK;
   265 
   266 local
   267   val empty = Records Symtab.empty;
   268 
   269   fun prep_ext (x as Records _) = x;
   270 
   271   fun merge (Records tab1, Records tab2) =
   272     Records (Symtab.merge (K true) (tab1, tab2));
   273 
   274   fun print sg (Records tab) =
   275     let
   276       val prt_typ = Sign.pretty_typ sg;
   277       val ext_const = Sign.cond_extern sg Sign.constK;
   278 
   279       fun pretty_parent None = []
   280         | pretty_parent (Some (Ts, name)) =
   281             [Pretty.block [prt_typ (Type (name, Ts)), Pretty.str " +"]];
   282 
   283       fun pretty_field (c, T) = Pretty.block
   284         [Pretty.str (ext_const c), Pretty.str " ::", Pretty.brk 1, Pretty.quote (prt_typ T)];
   285 
   286       fun pretty_record (name, {args, parent, fields, simps = _}) = Pretty.block (Pretty.fbreaks
   287         (Pretty.block [prt_typ (Type (name, map TFree args)), Pretty.str " = "] ::
   288           pretty_parent parent @ map pretty_field fields));
   289     in
   290       seq (Pretty.writeln o pretty_record) (Symtab.dest tab)
   291     end;
   292 in
   293   val record_thy_data = (recordsK, (empty, prep_ext, merge, print));
   294 end;
   295 
   296 
   297 (* get and put records *)
   298 
   299 fun get_records thy =
   300   (case Theory.get_data thy recordsK of
   301     Records tab => tab
   302   | _ => type_error recordsK);
   303 
   304 fun get_record thy name = Symtab.lookup (get_records thy, name);
   305 
   306 fun put_records tab thy =
   307   Theory.put_data (recordsK, Records tab) thy;
   308 
   309 fun put_record name info thy =
   310   put_records (Symtab.update ((name, info), get_records thy)) thy;
   311 
   312 
   313 (* parent records *)
   314 
   315 fun inst_record thy (types, name) =
   316   let
   317     val sign = Theory.sign_of thy;
   318     fun err msg = error (msg ^ " parent record " ^ quote name);
   319 
   320     val {args, parent, fields, simps} =
   321       (case get_record thy name of Some info => info | None => err "Unknown");
   322     val _ = if length types <> length args then err "Bad number of arguments for" else ();
   323 
   324     fun bad_inst ((x, S), T) =
   325       if Sign.of_sort sign (T, S) then None else Some x
   326     val bads = mapfilter bad_inst (args ~~ types);
   327 
   328     val inst = map fst args ~~ types;
   329     val subst = Term.map_type_tfree (fn (x, _) => the (assoc (inst, x)));
   330   in
   331     if not (null bads) then
   332       err ("Ill-sorted instantiation of " ^ commas bads ^ " in")
   333     else (apsome (apfst (map subst)) parent, map (apsnd subst) fields, simps)
   334   end;
   335 
   336 fun add_parents thy (None, parents) = parents
   337   | add_parents thy (Some (types, name), parents) =
   338       let val (pparent, pfields, psimps) = inst_record thy (types, name)
   339       in add_parents thy (pparent, {name = name, fields = pfields, simps = psimps} :: parents) end;
   340 
   341 
   342 
   343 (** internal theory extenders **)
   344 
   345 (* field_definitions *)
   346 
   347 (*theorems from Prod.thy*)
   348 val prod_convs = map Attribute.tthm_of [fst_conv, snd_conv];
   349 
   350 
   351 fun field_definitions fields names zeta moreT more vars named_vars thy =
   352   let
   353     val base = Sign.base_name;
   354 
   355 
   356     (* prepare declarations and definitions *)
   357 
   358     (*field types*)
   359     fun mk_fieldT_spec c =
   360       (suffix field_typeN c, ["'a", zeta],
   361         HOLogic.mk_prodT (TFree ("'a", HOLogic.termS), moreT), Syntax.NoSyn);
   362     val fieldT_specs = map (mk_fieldT_spec o base) names;
   363 
   364     (*field declarations*)
   365     val field_decls = map (mk_fieldC moreT) fields;
   366     val dest_decls = map (mk_fstC moreT) fields @ map (mk_sndC moreT) fields;
   367 
   368     (*field constructors*)
   369     fun mk_field_spec (c, v) =
   370       mk_field ((c, v), more) :== HOLogic.mk_prod (v, more);
   371     val field_specs = map mk_field_spec named_vars;
   372 
   373     (*field destructors*)
   374     fun mk_dest_spec dest dest' (c, T) =
   375       let
   376         val p = Free ("p", mk_fieldT ((c, T), moreT));
   377         val p' = Free ("p", HOLogic.mk_prodT (T, moreT));
   378           (*note: field types are just abbreviations*)
   379       in dest p :== dest' p' end;
   380     val dest_specs =
   381       map (mk_dest_spec mk_fst HOLogic.mk_fst) fields @
   382       map (mk_dest_spec mk_snd HOLogic.mk_snd) fields;
   383 
   384 
   385     (* prepare theorems *)
   386 
   387     fun mk_dest_prop dest dest' (c, v) =
   388       dest (mk_field ((c, v), more)) === dest' (v, more);
   389     val dest_props =
   390       map (mk_dest_prop mk_fst fst) named_vars @
   391       map (mk_dest_prop mk_snd snd) named_vars;
   392 
   393 
   394     (* 1st stage: defs_thy *)
   395 
   396     val defs_thy =
   397       thy
   398       |> Theory.add_tyabbrs_i fieldT_specs
   399       |> (Theory.add_consts_i o map (Syntax.no_syn o apfst base))
   400         (field_decls @ dest_decls)
   401       |> (PureThy.add_defs_i o map Attribute.none)
   402         (field_specs @ dest_specs);
   403 
   404     val field_defs = get_defs defs_thy field_specs;
   405     val dest_defs = get_defs defs_thy dest_specs;
   406 
   407 
   408     (* 2nd stage: thms_thy *)
   409 
   410     val dest_convs =
   411       map (prove_simp defs_thy (field_defs @ dest_defs @ prod_convs)) dest_props;
   412 
   413     val thms_thy =
   414       defs_thy
   415       |> (PureThy.add_tthmss o map Attribute.none)
   416         [("field_defs", field_defs),
   417           ("dest_defs", dest_defs),
   418           ("dest_convs", dest_convs)];
   419 
   420   in (thms_thy, dest_convs) end;
   421 
   422 
   423 (* record_definition *)
   424 
   425 fun record_definition (args, bname) parent (parents: parent_info list) bfields thy =
   426   let
   427     val sign = Theory.sign_of thy;
   428     val full = Sign.full_name_path sign bname;
   429     val base = Sign.base_name;
   430 
   431 
   432     (* basic components *)
   433 
   434     val alphas = map fst args;
   435     val name = Sign.full_name sign bname;	(*not made part of record name space!*)
   436 
   437     val parent_fields = flat (map #fields parents);
   438     val parent_names = map fst parent_fields;
   439     val parent_types = map snd parent_fields;
   440     val parent_len = length parent_fields;
   441     val parent_xs = variantlist (map (base o fst) parent_fields, [moreN]);
   442     val parent_vars = ListPair.map Free (parent_xs, parent_types);
   443     val parent_named_vars = parent_names ~~ parent_vars;
   444 
   445     val fields = map (apfst full) bfields;
   446     val names = map fst fields;
   447     val types = map snd fields;
   448     val len = length fields;
   449     val xs = variantlist (map fst bfields, moreN :: parent_xs);
   450     val vars = ListPair.map Free (xs, types);
   451     val named_vars = names ~~ vars;
   452 
   453     val all_fields = parent_fields @ fields;
   454     val all_names = parent_names @ names;
   455     val all_types = parent_types @ types;
   456     val all_len = parent_len + len;
   457     val all_xs = parent_xs @ xs;
   458     val all_vars = parent_vars @ vars;
   459     val all_named_vars = parent_named_vars @ named_vars;
   460 
   461     val zeta = variant alphas "'z";
   462     val moreT = TFree (zeta, moreS);
   463     val more = Free (moreN, moreT);
   464     fun more_part t = mk_more t (full moreN);
   465 
   466     val parent_more = funpow parent_len mk_snd;
   467     val idxs = 0 upto (len - 1);
   468 
   469     val rec_schemeT = mk_recordT (all_fields, moreT);
   470     val rec_scheme = mk_record (all_named_vars, more);
   471     val r = Free ("r", rec_schemeT);
   472     val recT = mk_recordT (all_fields, HOLogic.unitT);
   473 
   474 
   475     (* prepare print translation functions *)
   476 
   477     val field_tr'_names =
   478       distinct (flat (map (NameSpace.accesses o suffix fieldN) names)) \\
   479         #3 (Syntax.trfun_names (Theory.syn_of thy));
   480     val field_trfuns = ([], [], field_tr'_names ~~ map field_tr' field_tr'_names, []);
   481 
   482 
   483     (* prepare declarations *)
   484 
   485     val sel_decls = map (mk_selC rec_schemeT) bfields @ [mk_moreC rec_schemeT (moreN, moreT)];
   486     val update_decls = map (mk_updateC rec_schemeT) bfields;
   487     val make_decls =
   488       [(mk_makeC rec_schemeT (make_schemeN, all_types @ [moreT])),
   489        (mk_makeC recT (makeN, all_types))];
   490 
   491 
   492     (* prepare definitions *)
   493 
   494     (*record (scheme) type abbreviation*)
   495     val recordT_specs =
   496       [(suffix schemeN bname, alphas @ [zeta], rec_schemeT, Syntax.NoSyn),
   497         (bname, alphas, recT, Syntax.NoSyn)];
   498 
   499     (*selectors*)
   500     fun mk_sel_spec (i, c) =
   501       mk_sel r c :== mk_fst (funpow i mk_snd (parent_more r));
   502     val sel_specs =
   503       ListPair.map mk_sel_spec (idxs, names) @
   504         [more_part r :== funpow len mk_snd (parent_more r)];
   505 
   506     (*updates*)
   507     val all_sels = all_names ~~ map (mk_sel r) all_names;
   508     fun mk_upd_spec (i, (c, x)) =
   509       mk_update r (c, x) :==
   510         mk_record (nth_update (c, x) (parent_len + i, all_sels), more_part r)
   511     val update_specs = ListPair.map mk_upd_spec (idxs, named_vars);
   512 
   513     (*makes*)
   514     val make_scheme = Const (mk_makeC rec_schemeT (full make_schemeN, all_types @ [moreT]));
   515     val make = Const (mk_makeC recT (full makeN, all_types));
   516     val make_specs =
   517       [list_comb (make_scheme, all_vars) $ more :== rec_scheme,
   518         list_comb (make, all_vars) :== mk_record (all_named_vars, HOLogic.unit)];
   519 
   520 
   521     (* prepare propositions *)
   522 
   523     (*selectors*)
   524     val sel_props =
   525       map (fn (c, x) => mk_sel rec_scheme c === x) named_vars @
   526         [more_part rec_scheme === more];
   527 
   528     (*updates*)
   529     fun mk_upd_prop (i, (c, T)) =
   530       let val x' = Free (variant all_xs (base c ^ "'"), T) in
   531         mk_update rec_scheme (c, x') ===
   532           mk_record (nth_update (c, x') (parent_len + i, all_named_vars), more)
   533       end;
   534     val update_props = ListPair.map mk_upd_prop (idxs, fields);
   535 
   536 
   537     (* 1st stage: fields_thy *)
   538 
   539     val (fields_thy, field_simps) =
   540       thy
   541       |> Theory.add_path bname
   542       |> field_definitions fields names zeta moreT more vars named_vars;
   543 
   544 
   545     (* 2nd stage: defs_thy *)
   546 
   547     val defs_thy =
   548       fields_thy
   549       |> Theory.parent_path
   550       |> Theory.add_tyabbrs_i recordT_specs	(*not made part of record name space!*)
   551       |> Theory.add_path bname
   552       |> Theory.add_trfuns field_trfuns
   553       |> (Theory.add_consts_i o map Syntax.no_syn)
   554         (sel_decls @ update_decls @ make_decls)
   555       |> (PureThy.add_defs_i o map Attribute.none)
   556         (sel_specs @ update_specs @ make_specs);
   557 
   558     val sel_defs = get_defs defs_thy sel_specs;
   559     val update_defs = get_defs defs_thy update_specs;
   560     val make_defs = get_defs defs_thy make_specs;
   561 
   562 
   563     (* 3rd stage: thms_thy *)
   564 
   565     val parent_simps = flat (map #simps parents);
   566     val prove = prove_simp defs_thy;
   567 
   568     val sel_convs = map (prove (parent_simps @ sel_defs @ field_simps)) sel_props;
   569     val update_convs = map (prove (parent_simps @ update_defs @ sel_convs)) update_props;
   570 
   571     val simps = field_simps @ sel_convs @ update_convs @ make_defs;
   572 
   573     val thms_thy =
   574       defs_thy
   575       |> (PureThy.add_tthmss o map Attribute.none)
   576         [("select_defs", sel_defs),
   577           ("update_defs", update_defs),
   578           ("make_defs", make_defs),
   579           ("select_convs", sel_convs),
   580           ("update_convs", update_convs)]
   581       |> PureThy.add_tthmss [(("simps", simps), [Simplifier.simp_add_global])];
   582 
   583 
   584     (* 4th stage: final_thy *)
   585 
   586     val final_thy =
   587       thms_thy
   588       |> put_record name {args = args, parent = parent, fields = fields, simps = simps}
   589       |> Theory.parent_path;
   590 
   591   in final_thy end;
   592 
   593 
   594 
   595 (** theory extender interface **)
   596 
   597 (* prepare arguments *)
   598 
   599 (*note: read_raw_typ avoids expanding type abbreviations*)
   600 fun read_raw_parent sign s =
   601   (case Sign.read_raw_typ (sign, K None) s handle TYPE (msg, _, _) => error msg of
   602     Type (name, Ts) => (Ts, name)
   603   | _ => error ("Bad parent record specification: " ^ quote s));
   604 
   605 fun read_typ sign (env, s) =
   606   let
   607     fun def_type (x, ~1) = assoc (env, x)
   608       | def_type _ = None;
   609     val T = Type.no_tvars (Sign.read_typ (sign, def_type) s) handle TYPE (msg, _, _) => error msg;
   610   in (Term.add_typ_tfrees (T, env), T) end;
   611 
   612 fun cert_typ sign (env, raw_T) =
   613   let val T = Type.no_tvars (Sign.certify_typ sign raw_T) handle TYPE (msg, _, _) => error msg
   614   in (Term.add_typ_tfrees (T, env), T) end;
   615 
   616 
   617 (* add_record *)
   618 
   619 (*we do all preparations and error checks here, deferring the real
   620   work to record_definition*)
   621 
   622 fun gen_add_record prep_typ prep_raw_parent (params, bname) raw_parent raw_fields thy =
   623   let
   624     val _ = Theory.requires thy "Record" "record definitions";
   625     val sign = Theory.sign_of thy;
   626     val _ = writeln ("Defining record " ^ quote bname ^ " ...");
   627 
   628 
   629     (* parents *)
   630 
   631     fun prep_inst T = snd (cert_typ sign ([], T));
   632 
   633     val parent = apsome (apfst (map prep_inst) o prep_raw_parent sign) raw_parent
   634       handle ERROR => error ("The error(s) above in parent record specification");
   635     val parents = add_parents thy (parent, []);
   636 
   637     val init_env =
   638       (case parent of
   639         None => []
   640       | Some (types, _) => foldr Term.add_typ_tfrees (types, []));
   641 
   642 
   643     (* fields *)
   644 
   645     fun prep_field (env, (c, raw_T)) =
   646       let val (env', T) = prep_typ sign (env, raw_T) handle ERROR =>
   647         error ("The error(s) above occured in field " ^ quote c)
   648       in (env', (c, T)) end;
   649 
   650     val (envir, bfields) = foldl_map prep_field (init_env, raw_fields);
   651     val envir_names = map fst envir;
   652 
   653 
   654     (* args *)
   655 
   656     val defaultS = Sign.defaultS sign;
   657     val args = map (fn x => (x, if_none (assoc (envir, x)) defaultS)) params;
   658 
   659 
   660     (* errors *)
   661 
   662     val name = Sign.full_name sign bname;
   663     val err_dup_record =
   664       if is_none (get_record thy name) then []
   665       else ["Duplicate definition of record " ^ quote name];
   666 
   667     val err_dup_parms =
   668       (case duplicates params of
   669         [] => []
   670       | dups => ["Duplicate parameter(s) " ^ commas dups]);
   671 
   672     val err_extra_frees =
   673       (case gen_rems (op =) (envir_names, params) of
   674         [] => []
   675       | extras => ["Extra free type variable(s) " ^ commas extras]);
   676 
   677     val err_no_fields = if null bfields then ["No fields present"] else [];
   678 
   679     val err_dup_fields =
   680       (case duplicates (map fst bfields) of
   681         [] => []
   682       | dups => ["Duplicate field(s) " ^ commas_quote dups]);
   683 
   684     val err_bad_fields =
   685       if forall (not_equal moreN o fst) bfields then []
   686       else ["Illegal field name " ^ quote moreN];
   687 
   688     val err_dup_sorts =
   689       (case duplicates envir_names of
   690         [] => []
   691       | dups => ["Inconsistent sort constraints for " ^ commas dups]);
   692 
   693     val errs =
   694       err_dup_record @ err_dup_parms @ err_extra_frees @ err_no_fields @
   695       err_dup_fields @ err_bad_fields @ err_dup_sorts;
   696   in
   697     if null errs then () else error (cat_lines errs);
   698     thy |> record_definition (args, bname) parent parents bfields
   699   end
   700   handle ERROR => error ("Failed to define record " ^ quote bname);
   701 
   702 val add_record = gen_add_record read_typ read_raw_parent;
   703 val add_record_i = gen_add_record cert_typ (K I);
   704 
   705 
   706 
   707 (** setup theory **)
   708 
   709 val setup =
   710  [Theory.init_data [record_thy_data],
   711   Theory.add_trfuns
   712     ([], [("_record", record_tr), ("_record_scheme", record_scheme_tr)], [], [])];
   713 
   714 
   715 end;