src/HOL/Tools/record_package.ML
author wenzelm
Thu Jun 18 18:35:07 1998 +0200 (1998-06-18)
changeset 5052 bbe3584b515b
parent 5006 cdc86a914e63
child 5060 7b86df67cc1a
permissions -rw-r--r--
fixed comment;
     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 (* data kind 'HOL/records' *)
   260 
   261 structure RecordsArgs =
   262 struct
   263   val name = "HOL/records";
   264   type T = record_info Symtab.table;
   265 
   266   val empty = Symtab.empty;
   267   val prep_ext = I;
   268   val merge: T * T -> T = Symtab.merge (K true);
   269 
   270   fun print sg tab =
   271     let
   272       val prt_typ = Sign.pretty_typ sg;
   273       val ext_const = Sign.cond_extern sg Sign.constK;
   274 
   275       fun pretty_parent None = []
   276         | pretty_parent (Some (Ts, name)) =
   277             [Pretty.block [prt_typ (Type (name, Ts)), Pretty.str " +"]];
   278 
   279       fun pretty_field (c, T) = Pretty.block
   280         [Pretty.str (ext_const c), Pretty.str " ::", Pretty.brk 1, Pretty.quote (prt_typ T)];
   281 
   282       fun pretty_record (name, {args, parent, fields, simps = _}) = Pretty.block (Pretty.fbreaks
   283         (Pretty.block [prt_typ (Type (name, map TFree args)), Pretty.str " = "] ::
   284           pretty_parent parent @ map pretty_field fields));
   285     in
   286       seq (Pretty.writeln o pretty_record) (Symtab.dest tab)
   287     end;
   288 end;
   289 
   290 structure RecordsData = TheoryDataFun(RecordsArgs);
   291 val print_records = RecordsData.print;
   292 
   293 
   294 (* get and put records *)
   295 
   296 fun get_record thy name = Symtab.lookup (RecordsData.get thy, name);
   297 
   298 fun put_record name info thy =
   299   RecordsData.put (Symtab.update ((name, info), RecordsData.get thy)) thy;
   300 
   301 
   302 (* parent records *)
   303 
   304 fun inst_record thy (types, name) =
   305   let
   306     val sign = Theory.sign_of thy;
   307     fun err msg = error (msg ^ " parent record " ^ quote name);
   308 
   309     val {args, parent, fields, simps} =
   310       (case get_record thy name of Some info => info | None => err "Unknown");
   311     val _ = if length types <> length args then err "Bad number of arguments for" else ();
   312 
   313     fun bad_inst ((x, S), T) =
   314       if Sign.of_sort sign (T, S) then None else Some x
   315     val bads = mapfilter bad_inst (args ~~ types);
   316 
   317     val inst = map fst args ~~ types;
   318     val subst = Term.map_type_tfree (fn (x, _) => the (assoc (inst, x)));
   319   in
   320     if not (null bads) then
   321       err ("Ill-sorted instantiation of " ^ commas bads ^ " in")
   322     else (apsome (apfst (map subst)) parent, map (apsnd subst) fields, simps)
   323   end;
   324 
   325 fun add_parents thy (None, parents) = parents
   326   | add_parents thy (Some (types, name), parents) =
   327       let val (pparent, pfields, psimps) = inst_record thy (types, name)
   328       in add_parents thy (pparent, {name = name, fields = pfields, simps = psimps} :: parents) end;
   329 
   330 
   331 
   332 (** internal theory extenders **)
   333 
   334 (* field_definitions *)
   335 
   336 (*theorems from Prod.thy*)
   337 val prod_convs = map Attribute.tthm_of [fst_conv, snd_conv];
   338 
   339 
   340 fun field_definitions fields names zeta moreT more vars named_vars thy =
   341   let
   342     val base = Sign.base_name;
   343 
   344 
   345     (* prepare declarations and definitions *)
   346 
   347     (*field types*)
   348     fun mk_fieldT_spec c =
   349       (suffix field_typeN c, ["'a", zeta],
   350         HOLogic.mk_prodT (TFree ("'a", HOLogic.termS), moreT), Syntax.NoSyn);
   351     val fieldT_specs = map (mk_fieldT_spec o base) names;
   352 
   353     (*field declarations*)
   354     val field_decls = map (mk_fieldC moreT) fields;
   355     val dest_decls = map (mk_fstC moreT) fields @ map (mk_sndC moreT) fields;
   356 
   357     (*field constructors*)
   358     fun mk_field_spec (c, v) =
   359       mk_field ((c, v), more) :== HOLogic.mk_prod (v, more);
   360     val field_specs = map mk_field_spec named_vars;
   361 
   362     (*field destructors*)
   363     fun mk_dest_spec dest dest' (c, T) =
   364       let
   365         val p = Free ("p", mk_fieldT ((c, T), moreT));
   366         val p' = Free ("p", HOLogic.mk_prodT (T, moreT));
   367           (*note: field types are just abbreviations*)
   368       in dest p :== dest' p' end;
   369     val dest_specs =
   370       map (mk_dest_spec mk_fst HOLogic.mk_fst) fields @
   371       map (mk_dest_spec mk_snd HOLogic.mk_snd) fields;
   372 
   373 
   374     (* prepare theorems *)
   375 
   376     fun mk_dest_prop dest dest' (c, v) =
   377       dest (mk_field ((c, v), more)) === dest' (v, more);
   378     val dest_props =
   379       map (mk_dest_prop mk_fst fst) named_vars @
   380       map (mk_dest_prop mk_snd snd) named_vars;
   381 
   382 
   383     (* 1st stage: defs_thy *)
   384 
   385     val defs_thy =
   386       thy
   387       |> Theory.add_tyabbrs_i fieldT_specs
   388       |> (Theory.add_consts_i o map (Syntax.no_syn o apfst base))
   389         (field_decls @ dest_decls)
   390       |> (PureThy.add_defs_i o map Attribute.none)
   391         (field_specs @ dest_specs);
   392 
   393     val field_defs = get_defs defs_thy field_specs;
   394     val dest_defs = get_defs defs_thy dest_specs;
   395 
   396 
   397     (* 2nd stage: thms_thy *)
   398 
   399     val dest_convs =
   400       map (prove_simp defs_thy (field_defs @ dest_defs @ prod_convs)) dest_props;
   401 
   402     val thms_thy =
   403       defs_thy
   404       |> (PureThy.add_tthmss o map Attribute.none)
   405         [("field_defs", field_defs),
   406           ("dest_defs", dest_defs),
   407           ("dest_convs", dest_convs)];
   408 
   409   in (thms_thy, dest_convs) end;
   410 
   411 
   412 (* record_definition *)
   413 
   414 fun record_definition (args, bname) parent (parents: parent_info list) bfields thy =
   415   let
   416     val sign = Theory.sign_of thy;
   417     val full = Sign.full_name_path sign bname;
   418     val base = Sign.base_name;
   419 
   420 
   421     (* basic components *)
   422 
   423     val alphas = map fst args;
   424     val name = Sign.full_name sign bname;	(*not made part of record name space!*)
   425 
   426     val parent_fields = flat (map #fields parents);
   427     val parent_names = map fst parent_fields;
   428     val parent_types = map snd parent_fields;
   429     val parent_len = length parent_fields;
   430     val parent_xs = variantlist (map (base o fst) parent_fields, [moreN]);
   431     val parent_vars = ListPair.map Free (parent_xs, parent_types);
   432     val parent_named_vars = parent_names ~~ parent_vars;
   433 
   434     val fields = map (apfst full) bfields;
   435     val names = map fst fields;
   436     val types = map snd fields;
   437     val len = length fields;
   438     val xs = variantlist (map fst bfields, moreN :: parent_xs);
   439     val vars = ListPair.map Free (xs, types);
   440     val named_vars = names ~~ vars;
   441 
   442     val all_fields = parent_fields @ fields;
   443     val all_names = parent_names @ names;
   444     val all_types = parent_types @ types;
   445     val all_len = parent_len + len;
   446     val all_xs = parent_xs @ xs;
   447     val all_vars = parent_vars @ vars;
   448     val all_named_vars = parent_named_vars @ named_vars;
   449 
   450     val zeta = variant alphas "'z";
   451     val moreT = TFree (zeta, moreS);
   452     val more = Free (moreN, moreT);
   453     fun more_part t = mk_more t (full moreN);
   454 
   455     val parent_more = funpow parent_len mk_snd;
   456     val idxs = 0 upto (len - 1);
   457 
   458     val rec_schemeT = mk_recordT (all_fields, moreT);
   459     val rec_scheme = mk_record (all_named_vars, more);
   460     val r = Free ("r", rec_schemeT);
   461     val recT = mk_recordT (all_fields, HOLogic.unitT);
   462 
   463 
   464     (* prepare print translation functions *)
   465 
   466     val field_tr'_names =
   467       distinct (flat (map (NameSpace.accesses o suffix fieldN) names)) \\
   468         #3 (Syntax.trfun_names (Theory.syn_of thy));
   469     val field_trfuns = ([], [], field_tr'_names ~~ map field_tr' field_tr'_names, []);
   470 
   471 
   472     (* prepare declarations *)
   473 
   474     val sel_decls = map (mk_selC rec_schemeT) bfields @ [mk_moreC rec_schemeT (moreN, moreT)];
   475     val update_decls = map (mk_updateC rec_schemeT) bfields;
   476     val make_decls =
   477       [(mk_makeC rec_schemeT (make_schemeN, all_types @ [moreT])),
   478        (mk_makeC recT (makeN, all_types))];
   479 
   480 
   481     (* prepare definitions *)
   482 
   483     (*record (scheme) type abbreviation*)
   484     val recordT_specs =
   485       [(suffix schemeN bname, alphas @ [zeta], rec_schemeT, Syntax.NoSyn),
   486         (bname, alphas, recT, Syntax.NoSyn)];
   487 
   488     (*selectors*)
   489     fun mk_sel_spec (i, c) =
   490       mk_sel r c :== mk_fst (funpow i mk_snd (parent_more r));
   491     val sel_specs =
   492       ListPair.map mk_sel_spec (idxs, names) @
   493         [more_part r :== funpow len mk_snd (parent_more r)];
   494 
   495     (*updates*)
   496     val all_sels = all_names ~~ map (mk_sel r) all_names;
   497     fun mk_upd_spec (i, (c, x)) =
   498       mk_update r (c, x) :==
   499         mk_record (nth_update (c, x) (parent_len + i, all_sels), more_part r)
   500     val update_specs = ListPair.map mk_upd_spec (idxs, named_vars);
   501 
   502     (*makes*)
   503     val make_scheme = Const (mk_makeC rec_schemeT (full make_schemeN, all_types @ [moreT]));
   504     val make = Const (mk_makeC recT (full makeN, all_types));
   505     val make_specs =
   506       [list_comb (make_scheme, all_vars) $ more :== rec_scheme,
   507         list_comb (make, all_vars) :== mk_record (all_named_vars, HOLogic.unit)];
   508 
   509 
   510     (* prepare propositions *)
   511 
   512     (*selectors*)
   513     val sel_props =
   514       map (fn (c, x) => mk_sel rec_scheme c === x) named_vars @
   515         [more_part rec_scheme === more];
   516 
   517     (*updates*)
   518     fun mk_upd_prop (i, (c, T)) =
   519       let val x' = Free (variant all_xs (base c ^ "'"), T) in
   520         mk_update rec_scheme (c, x') ===
   521           mk_record (nth_update (c, x') (parent_len + i, all_named_vars), more)
   522       end;
   523     val update_props = ListPair.map mk_upd_prop (idxs, fields);
   524 
   525 
   526     (* 1st stage: fields_thy *)
   527 
   528     val (fields_thy, field_simps) =
   529       thy
   530       |> Theory.add_path bname
   531       |> field_definitions fields names zeta moreT more vars named_vars;
   532 
   533 
   534     (* 2nd stage: defs_thy *)
   535 
   536     val defs_thy =
   537       fields_thy
   538       |> Theory.parent_path
   539       |> Theory.add_tyabbrs_i recordT_specs	(*not made part of record name space!*)
   540       |> Theory.add_path bname
   541       |> Theory.add_trfuns field_trfuns
   542       |> (Theory.add_consts_i o map Syntax.no_syn)
   543         (sel_decls @ update_decls @ make_decls)
   544       |> (PureThy.add_defs_i o map Attribute.none)
   545         (sel_specs @ update_specs @ make_specs);
   546 
   547     val sel_defs = get_defs defs_thy sel_specs;
   548     val update_defs = get_defs defs_thy update_specs;
   549     val make_defs = get_defs defs_thy make_specs;
   550 
   551 
   552     (* 3rd stage: thms_thy *)
   553 
   554     val parent_simps = flat (map #simps parents);
   555     val prove = prove_simp defs_thy;
   556 
   557     val sel_convs = map (prove (parent_simps @ sel_defs @ field_simps)) sel_props;
   558     val update_convs = map (prove (parent_simps @ update_defs @ sel_convs)) update_props;
   559 
   560     val simps = field_simps @ sel_convs @ update_convs @ make_defs;
   561 
   562     val thms_thy =
   563       defs_thy
   564       |> (PureThy.add_tthmss o map Attribute.none)
   565         [("select_defs", sel_defs),
   566           ("update_defs", update_defs),
   567           ("make_defs", make_defs),
   568           ("select_convs", sel_convs),
   569           ("update_convs", update_convs)]
   570       |> PureThy.add_tthmss [(("simps", simps), [Simplifier.simp_add_global])];
   571 
   572 
   573     (* 4th stage: final_thy *)
   574 
   575     val final_thy =
   576       thms_thy
   577       |> put_record name {args = args, parent = parent, fields = fields, simps = simps}
   578       |> Theory.parent_path;
   579 
   580   in final_thy end;
   581 
   582 
   583 
   584 (** theory extender interface **)
   585 
   586 (* prepare arguments *)
   587 
   588 (*note: read_raw_typ avoids expanding type abbreviations*)
   589 fun read_raw_parent sign s =
   590   (case Sign.read_raw_typ (sign, K None) s handle TYPE (msg, _, _) => error msg of
   591     Type (name, Ts) => (Ts, name)
   592   | _ => error ("Bad parent record specification: " ^ quote s));
   593 
   594 fun read_typ sign (env, s) =
   595   let
   596     fun def_type (x, ~1) = assoc (env, x)
   597       | def_type _ = None;
   598     val T = Type.no_tvars (Sign.read_typ (sign, def_type) s) handle TYPE (msg, _, _) => error msg;
   599   in (Term.add_typ_tfrees (T, env), T) end;
   600 
   601 fun cert_typ sign (env, raw_T) =
   602   let val T = Type.no_tvars (Sign.certify_typ sign raw_T) handle TYPE (msg, _, _) => error msg
   603   in (Term.add_typ_tfrees (T, env), T) end;
   604 
   605 
   606 (* add_record *)
   607 
   608 (*we do all preparations and error checks here, deferring the real
   609   work to record_definition*)
   610 
   611 fun gen_add_record prep_typ prep_raw_parent (params, bname) raw_parent raw_fields thy =
   612   let
   613     val _ = Theory.requires thy "Record" "record definitions";
   614     val sign = Theory.sign_of thy;
   615     val _ = writeln ("Defining record " ^ quote bname ^ " ...");
   616 
   617 
   618     (* parents *)
   619 
   620     fun prep_inst T = snd (cert_typ sign ([], T));
   621 
   622     val parent = apsome (apfst (map prep_inst) o prep_raw_parent sign) raw_parent
   623       handle ERROR => error ("The error(s) above in parent record specification");
   624     val parents = add_parents thy (parent, []);
   625 
   626     val init_env =
   627       (case parent of
   628         None => []
   629       | Some (types, _) => foldr Term.add_typ_tfrees (types, []));
   630 
   631 
   632     (* fields *)
   633 
   634     fun prep_field (env, (c, raw_T)) =
   635       let val (env', T) = prep_typ sign (env, raw_T) handle ERROR =>
   636         error ("The error(s) above occured in field " ^ quote c)
   637       in (env', (c, T)) end;
   638 
   639     val (envir, bfields) = foldl_map prep_field (init_env, raw_fields);
   640     val envir_names = map fst envir;
   641 
   642 
   643     (* args *)
   644 
   645     val defaultS = Sign.defaultS sign;
   646     val args = map (fn x => (x, if_none (assoc (envir, x)) defaultS)) params;
   647 
   648 
   649     (* errors *)
   650 
   651     val name = Sign.full_name sign bname;
   652     val err_dup_record =
   653       if is_none (get_record thy name) then []
   654       else ["Duplicate definition of record " ^ quote name];
   655 
   656     val err_dup_parms =
   657       (case duplicates params of
   658         [] => []
   659       | dups => ["Duplicate parameter(s) " ^ commas dups]);
   660 
   661     val err_extra_frees =
   662       (case gen_rems (op =) (envir_names, params) of
   663         [] => []
   664       | extras => ["Extra free type variable(s) " ^ commas extras]);
   665 
   666     val err_no_fields = if null bfields then ["No fields present"] else [];
   667 
   668     val err_dup_fields =
   669       (case duplicates (map fst bfields) of
   670         [] => []
   671       | dups => ["Duplicate field(s) " ^ commas_quote dups]);
   672 
   673     val err_bad_fields =
   674       if forall (not_equal moreN o fst) bfields then []
   675       else ["Illegal field name " ^ quote moreN];
   676 
   677     val err_dup_sorts =
   678       (case duplicates envir_names of
   679         [] => []
   680       | dups => ["Inconsistent sort constraints for " ^ commas dups]);
   681 
   682     val errs =
   683       err_dup_record @ err_dup_parms @ err_extra_frees @ err_no_fields @
   684       err_dup_fields @ err_bad_fields @ err_dup_sorts;
   685   in
   686     if null errs then () else error (cat_lines errs);
   687     thy |> record_definition (args, bname) parent parents bfields
   688   end
   689   handle ERROR => error ("Failed to define record " ^ quote bname);
   690 
   691 val add_record = gen_add_record read_typ read_raw_parent;
   692 val add_record_i = gen_add_record cert_typ (K I);
   693 
   694 
   695 
   696 (** setup theory **)
   697 
   698 val setup =
   699  [RecordsData.init,
   700   Theory.add_trfuns
   701     ([], [("_record", record_tr), ("_record_scheme", record_scheme_tr)], [], [])];
   702 
   703 
   704 end;