src/HOL/record.ML
author narasche
Wed Jan 14 11:10:19 1998 +0100 (1998-01-14)
changeset 4574 b922012cc142
parent 4564 dc45cf21dbd2
permissions -rw-r--r--
error with instantiantion of sub-records removed
narasche@4454
     1
(*  Title:      HOL/record.ML
narasche@4454
     2
    ID:         $Id$
narasche@4454
     3
    Author:     Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
narasche@4454
     4
narasche@4454
     5
Internal interface for records.
narasche@4454
     6
*)
narasche@4454
     7
narasche@4454
     8
narasche@4454
     9
signature RECORD =
narasche@4454
    10
sig
narasche@4454
    11
  val add_record: 
narasche@4454
    12
    (string list * bstring) -> string option -> 
narasche@4454
    13
      (bstring * string) list -> theory -> theory
narasche@4454
    14
  val add_record_i: 
narasche@4454
    15
    (string list * bstring) -> (typ list * string) option -> 
narasche@4454
    16
      (bstring * typ) list -> theory -> theory
narasche@4454
    17
end;
narasche@4454
    18
narasche@4454
    19
structure Record: RECORD =
narasche@4454
    20
struct
narasche@4454
    21
narasche@4454
    22
val base = Sign.base_name; 
narasche@4454
    23
narasche@4454
    24
(* FIXME move to Pure/library.ML *)
narasche@4454
    25
fun set_minus xs [] = xs
narasche@4454
    26
  | set_minus xs (y::ys) = set_minus (xs \ y) ys;
narasche@4454
    27
(* FIXME *)
narasche@4454
    28
narasche@4454
    29
(* FIXME move to Pure/sign.ML *)
narasche@4454
    30
fun of_sort sg = 
narasche@4454
    31
  Sorts.of_sort 
narasche@4454
    32
    (#classrel (Type.rep_tsig (#tsig (Sign.rep_sg sg))))
narasche@4454
    33
    (#arities (Type.rep_tsig (#tsig (Sign.rep_sg sg))));
narasche@4454
    34
(* FIXME *)
narasche@4454
    35
narasche@4454
    36
narasche@4454
    37
narasche@4454
    38
(** record info **)
narasche@4454
    39
narasche@4454
    40
fun get_record thy name = 
narasche@4454
    41
  let val table = ThyData.get_records thy
narasche@4454
    42
  in
narasche@4454
    43
    Symtab.lookup (table, name)
narasche@4454
    44
  end;
narasche@4454
    45
narasche@4454
    46
fun put_record thy name info = 
narasche@4454
    47
  let val table = ThyData.get_records thy 
narasche@4454
    48
  in
narasche@4454
    49
    ThyData.put_records (Symtab.update ((name, info), table))
narasche@4454
    50
  end;
narasche@4454
    51
narasche@4454
    52
local
narasche@4454
    53
  fun record_infos thy None = []
narasche@4454
    54
    | record_infos thy (Some info) =
narasche@4454
    55
        case #parent info of 
narasche@4454
    56
            None => [info]
narasche@4454
    57
          | Some (_, parent) => record_infos thy (get_record thy parent) @ [info];
narasche@4454
    58
  fun record_parass thy info = 
narasche@4454
    59
    (map (map (fn (str, _) => (str, 0)) o #args) (record_infos thy (Some info))) 
narasche@4454
    60
    : indexname list list; 
narasche@4454
    61
  fun record_argss thy info = 
narasche@4454
    62
    map (fst o the) (tl (map #parent (record_infos thy (Some info)))) @ 
narasche@4454
    63
    [map TFree (#args info)];
narasche@4454
    64
in  
narasche@4454
    65
  fun record_field_names thy info = 
narasche@4454
    66
    flat (map (map fst o #fields) (record_infos thy (Some info)));
narasche@4454
    67
  fun record_field_types thy info = 
narasche@4454
    68
    let 
narasche@4454
    69
      val paras_args = map (op ~~) (record_parass thy info ~~ record_argss thy info);
narasche@4454
    70
      val raw_substs = map typ_subst_TVars paras_args;
narasche@4454
    71
      fun make_substs [] = []
narasche@4574
    72
        | make_substs (x::xs) = (foldr1 (op o) (rev (x::xs))) :: make_substs xs; 
narasche@4454
    73
      val free_TFree = map (map (map_type_tfree (fn (str, s) => TVar((str, 0), s))));
narasche@4454
    74
      val raw_record_field_types = map (map snd o #fields) (record_infos thy (Some info))
narasche@4454
    75
    in 
narasche@4454
    76
      flat (ListPair.map (fn (s, ts) => map s ts) 
narasche@4454
    77
                         (make_substs raw_substs, free_TFree raw_record_field_types))
narasche@4454
    78
    end;
narasche@4454
    79
end;
narasche@4454
    80
narasche@4454
    81
narasche@4454
    82
narasche@4454
    83
(** abstract syntax **)
narasche@4454
    84
narasche@4454
    85
(* tuples *)
narasche@4454
    86
narasche@4454
    87
val unitT = Type ("unit",[]);
narasche@4454
    88
val unit = Const ("()",unitT);
narasche@4454
    89
fun mk_prodT (T1, T2) = Type ("*", [T1,T2]);
narasche@4454
    90
fun mk_Pair (t1, t2) = 
narasche@4454
    91
  let val T1 = fastype_of t1
narasche@4454
    92
      and T2 = fastype_of t2
narasche@4454
    93
  in Const ("Pair", [T1, T2] ---> mk_prodT (T1,T2)) $ t1 $ t2  end;
narasche@4454
    94
narasche@4564
    95
val mk_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq;
narasche@4564
    96
narasche@4454
    97
fun dest_prodT (Type ("*", [T1, T2])) = (T1, T2)
narasche@4454
    98
  | dest_prodT T = raise TYPE ("dest_prodT: product type expected", [T], []);
narasche@4454
    99
narasche@4454
   100
fun mk_fst pT = Const ("fst", pT --> fst (dest_prodT pT));
narasche@4454
   101
fun mk_snd pT = Const ("snd", pT --> snd (dest_prodT pT));
narasche@4454
   102
narasche@4454
   103
fun ap_fst t = mk_fst (fastype_of t) $ t;
narasche@4454
   104
fun ap_snd t = mk_snd (fastype_of t) $ t;
narasche@4454
   105
narasche@4454
   106
narasche@4454
   107
(* records *)
narasche@4454
   108
narasche@4454
   109
fun selT T recT = recT --> T; 
narasche@4454
   110
fun updateT T recT = T --> recT --> recT;
narasche@4454
   111
val base_free = Free o apfst base;
narasche@4454
   112
val make_scheme_name = "make_scheme";
narasche@4454
   113
val make_name = "make";
narasche@4564
   114
fun def_suffix s = s ^ "_def";
narasche@4564
   115
fun update_suffix s = s ^ "_update";
narasche@4454
   116
fun make_schemeC full make_schemeT = Const (full make_scheme_name, make_schemeT);
narasche@4454
   117
fun makeC full makeT = Const (full make_name, makeT);
narasche@4564
   118
fun make_args_scheme full make_schemeT base_frees z = 
narasche@4564
   119
  list_comb (make_schemeC full make_schemeT, base_frees) $ z;
narasche@4564
   120
fun make_args full makeT base_frees = 
narasche@4564
   121
  list_comb (makeC full makeT, base_frees); 
narasche@4454
   122
fun selC s T recT = Const (s, selT T recT);
narasche@4564
   123
fun updateC s T recT = Const (update_suffix s, updateT T recT);
narasche@4454
   124
fun frees xs = foldr add_typ_tfree_names (xs, []);
narasche@4454
   125
narasche@4454
   126
narasche@4454
   127
narasche@4454
   128
(** constants, definitions, axioms **)
narasche@4454
   129
narasche@4454
   130
(* constant declarations for make, selectors and update *)
narasche@4454
   131
narasche@4454
   132
fun decls make_schemeT makeT selT updateT recT current_fields =
narasche@4454
   133
  let val make_scheme_decl = (make_scheme_name, make_schemeT, NoSyn);
narasche@4454
   134
      val make_decl = (make_name, makeT, NoSyn);
narasche@4454
   135
      val sel_decls = map (fn (c, T) => (c, selT T recT, NoSyn)) current_fields;
narasche@4454
   136
      val update_decls = 
narasche@4564
   137
        map (fn (c, T) => (update_suffix c, updateT T recT, NoSyn)) current_fields
narasche@4454
   138
  in 
narasche@4454
   139
    make_scheme_decl :: make_decl :: sel_decls @ update_decls
narasche@4454
   140
  end;
narasche@4454
   141
narasche@4454
   142
narasche@4454
   143
(* definitions for make, selectors and update *)
narasche@4454
   144
 
narasche@4454
   145
(*make*)
narasche@4454
   146
fun make_defs make_schemeT makeT base_frees z thy =
narasche@4454
   147
  let
narasche@4454
   148
    val sign = sign_of thy;
narasche@4454
   149
    val full = Sign.full_name sign;
narasche@4454
   150
    val make_scheme_def = 
narasche@4564
   151
      mk_defpair (make_args_scheme full make_schemeT base_frees z, 
narasche@4564
   152
                  foldr mk_Pair (base_frees, z));
narasche@4454
   153
    val make_def = 
narasche@4564
   154
      mk_defpair (make_args full makeT base_frees, 
narasche@4564
   155
                  foldr mk_Pair (base_frees, unit))
narasche@4454
   156
  in
narasche@4454
   157
    make_scheme_def :: [make_def]
narasche@4454
   158
  end;
narasche@4454
   159
narasche@4454
   160
(*selectors*)
narasche@4454
   161
fun sel_defs recT r all_fields current_fullfields = 
narasche@4454
   162
  let 
narasche@4454
   163
    val prefix_len = length all_fields  - length current_fullfields;
narasche@4454
   164
    val sel_terms = 
narasche@4454
   165
        map (fn k => ap_fst o funpow k ap_snd)
narasche@4454
   166
            (prefix_len upto length all_fields - 1)
narasche@4454
   167
  in
narasche@4454
   168
    ListPair.map 
narasche@4454
   169
      (fn ((s, T), t) => mk_defpair (selC s T recT $ r, t r)) 
narasche@4454
   170
      (current_fullfields, sel_terms)
narasche@4454
   171
  end;
narasche@4454
   172
narasche@4454
   173
(*update*)
narasche@4454
   174
fun update_defs recT r all_fields current_fullfields thy = 
narasche@4454
   175
  let
narasche@4454
   176
    val len_all_fields = length all_fields;
narasche@4454
   177
    fun sel_last r = funpow len_all_fields ap_snd r;
narasche@4454
   178
    fun update_def_s (s, T) = 
narasche@4454
   179
      let val updates = map (fn (s', T') => 
narasche@4454
   180
        if s = s' then base_free (s, T) else selC s' T' recT $ r)
narasche@4454
   181
        all_fields
narasche@4454
   182
      in
narasche@4564
   183
        mk_defpair (updateC s T recT $ base_free (s, T) $ r,
narasche@4454
   184
                    foldr mk_Pair (updates, sel_last r)) 
narasche@4454
   185
      end;
narasche@4454
   186
  in 
narasche@4454
   187
    map update_def_s current_fullfields 
narasche@4454
   188
  end
narasche@4454
   189
narasche@4454
   190
narasche@4564
   191
(* theorems for make, selectors and update *)
narasche@4564
   192
 
narasche@4564
   193
(*preparations*)
narasche@4564
   194
fun get_all_selector_defs all_fields full thy = 
narasche@4564
   195
  map (fn (s, T) => get_axiom thy (def_suffix s)) all_fields; 
narasche@4564
   196
fun get_all_update_defs all_fields full thy = 
narasche@4564
   197
  map (fn (s, T) => get_axiom thy (def_suffix (update_suffix s))) all_fields;
narasche@4564
   198
fun get_make_scheme_def full thy = get_axiom thy (full (def_suffix make_scheme_name));
narasche@4564
   199
fun get_make_def full thy = get_axiom thy (full (def_suffix make_name));
narasche@4564
   200
fun all_rec_defs all_fields full thy = 
narasche@4564
   201
  get_make_scheme_def full thy :: get_make_def full thy :: 
narasche@4564
   202
  get_all_selector_defs all_fields full thy @ get_all_update_defs all_fields full thy; 
narasche@4564
   203
fun prove_goal_s goal_s all_fields full thy = 
narasche@4564
   204
  map (fn (s,T) => 
narasche@4564
   205
         (prove_goalw_cterm (all_rec_defs all_fields full thy) 
narasche@4564
   206
                            (cterm_of (sign_of thy) (mk_eq (goal_s (s,T))))
narasche@4564
   207
                            (K [simp_tac (HOL_basic_ss addsimps [fst_conv,snd_conv]) 1])))
narasche@4564
   208
      all_fields;
narasche@4564
   209
narasche@4564
   210
(*si (make(_scheme) x1 ... xi ... xn) = xi*)
narasche@4564
   211
fun sel_make_scheme_thms recT make_schemeT base_frees z all_fields full thy = 
narasche@4564
   212
  let     
narasche@4564
   213
    fun sel_make_scheme_s (s, T) = 
narasche@4564
   214
        (selC s T recT $ make_args_scheme full make_schemeT base_frees z, base_free(s,T)) 
narasche@4564
   215
  in
narasche@4564
   216
    prove_goal_s sel_make_scheme_s all_fields full thy
narasche@4564
   217
  end;
narasche@4564
   218
narasche@4564
   219
fun sel_make_thms recT_unitT makeT base_frees all_fields full thy = 
narasche@4564
   220
  let     
narasche@4564
   221
    fun sel_make_s (s, T) = 
narasche@4564
   222
        (selC s T recT_unitT $ make_args full makeT base_frees, Free(base s,T)) 
narasche@4564
   223
  in
narasche@4564
   224
    prove_goal_s sel_make_s all_fields full thy
narasche@4564
   225
  end;
narasche@4564
   226
narasche@4564
   227
(*si_update xia (make(_scheme) x1 ... xi ... xn) = (make x1 ... xia ... xn)*)
narasche@4564
   228
fun update_make_scheme_thms recT make_schemeT base_frees z all_fields full thy = 
narasche@4564
   229
  let 
narasche@4564
   230
    fun update_make_scheme_s (s, T) = 
narasche@4564
   231
     (updateC s T recT $ base_free(s ^ "'", T) $ 
narasche@4564
   232
        make_args_scheme full make_schemeT base_frees z, 
narasche@4564
   233
      make_args_scheme full make_schemeT 
narasche@4564
   234
        (map (fn t => if t = base_free(s, T) then base_free(s ^ "'", T) else t) base_frees) z)
narasche@4564
   235
  in 
narasche@4564
   236
    prove_goal_s update_make_scheme_s all_fields full thy
narasche@4564
   237
  end;
narasche@4564
   238
narasche@4564
   239
fun update_make_thms recT_unitT makeT base_frees all_fields full thy = 
narasche@4564
   240
  let 
narasche@4564
   241
    fun update_make_s (s, T) = 
narasche@4564
   242
     (updateC s T recT_unitT $ base_free(s ^ "'", T) $ 
narasche@4564
   243
        make_args full makeT base_frees, 
narasche@4564
   244
      make_args full makeT 
narasche@4564
   245
        (map (fn t => if t = base_free(s, T) then base_free(s ^ "'", T) else t) base_frees))
narasche@4564
   246
  in 
narasche@4564
   247
    prove_goal_s update_make_s all_fields full thy
narasche@4564
   248
  end;
narasche@4564
   249
narasche@4564
   250
narasche@4454
   251
narasche@4454
   252
(** errors **)
narasche@4454
   253
narasche@4454
   254
fun check_duplicate_fields all_field_names =
narasche@4454
   255
  let val has_dupl = findrep all_field_names
narasche@4454
   256
  in
narasche@4454
   257
    if null has_dupl then []
narasche@4454
   258
      else ["Duplicate field declaration: " ^ quote (hd has_dupl) ^
narasche@4454
   259
            " (Double might be in ancestor)"]
narasche@4454
   260
  end;
narasche@4454
   261
narasche@4454
   262
fun check_parent None name thy = []
narasche@4454
   263
  | check_parent (Some (args, parent)) name thy = 
narasche@4454
   264
     let 
narasche@4454
   265
       val opt_info = get_record thy parent;
narasche@4454
   266
       val sign = sign_of thy;
narasche@4454
   267
       fun check_sorts [] [] = []
narasche@4454
   268
         | check_sorts ((str, sort)::xs) (y::ys) = 
narasche@4454
   269
            if of_sort sign (y, sort)
narasche@4454
   270
              then check_sorts xs ys 
narasche@4454
   271
              else ["Sort of " ^ 
narasche@4454
   272
                    quote (Pretty.string_of (Sign.pretty_typ sign y)) ^ 
narasche@4454
   273
                    " does not match parent declaration"] 
narasche@4454
   274
     in 
narasche@4454
   275
       case opt_info of 
narasche@4454
   276
         None => ["Parent " ^ quote parent ^" not defined"]
narasche@4459
   277
       | Some {args = pargs, parent = pparent, fields = pfields} =>
narasche@4454
   278
           if (length args = length pargs) 
narasche@4454
   279
             then check_sorts pargs args
narasche@4454
   280
             else ["Mismatching arities for parent " ^ quote (base parent)] 
narasche@4454
   281
     end;    
narasche@4454
   282
narasche@4454
   283
fun check_duplicate_records thy full_name =
narasche@4454
   284
  if is_none (get_record thy full_name) then [] 
narasche@4454
   285
    else ["Duplicate record declaration"];
narasche@4454
   286
narasche@4454
   287
fun check_duplicate_args raw_args =
narasche@4454
   288
  let val has_dupl = findrep raw_args
narasche@4454
   289
  in
narasche@4454
   290
    if null has_dupl then []
narasche@4454
   291
      else ["Duplicate parameter: " ^ quote (hd has_dupl)]
narasche@4454
   292
  end;
narasche@4454
   293
narasche@4454
   294
fun check_raw_args raw_args free_vars thy = 
narasche@4454
   295
  let
narasche@4454
   296
    val free_vars_names = map fst free_vars;
narasche@4454
   297
    val diff_set = set_minus free_vars_names raw_args;
narasche@4454
   298
    val default_sort =  Type.defaultS ((#tsig o Sign.rep_sg) (sign_of thy));
narasche@4454
   299
    val assign_sorts = 
narasche@4454
   300
      map (fn x => case assoc (free_vars, x) of
narasche@4454
   301
                     None => (x, default_sort)
narasche@4454
   302
                   | Some sort => (x, sort)) raw_args
narasche@4454
   303
  in
narasche@4454
   304
    if free_vars_names subset raw_args 
narasche@4454
   305
      then ([], assign_sorts)
narasche@4454
   306
      else (["Free type variable(s): " ^ 
narasche@4454
   307
               (foldr1 (fn (s, s') => s ^ ", " ^ s') (map quote diff_set))],
narasche@4454
   308
            []) 
narasche@4454
   309
  end;
narasche@4454
   310
narasche@4454
   311
narasche@4454
   312
narasche@4454
   313
(** ext_record **)
narasche@4454
   314
narasche@4454
   315
fun ext_record (args, name) opt_parent current_fields thy =
narasche@4454
   316
  let
narasche@4454
   317
    val full_name = Sign.full_name (sign_of thy) name;
narasche@4454
   318
    val thy = thy |> Theory.add_path name;
narasche@4454
   319
    val sign = sign_of thy;
narasche@4454
   320
    val full = Sign.full_name sign;
narasche@4454
   321
narasche@4454
   322
    val current_fullfields = map (apfst full) current_fields;
narasche@4459
   323
    val info = {args = args, fields = current_fullfields, parent = opt_parent};
narasche@4454
   324
    val thy = thy |> put_record thy full_name info;
narasche@4454
   325
    val all_types = record_field_types thy info; 
narasche@4454
   326
    val all_fields = record_field_names thy info ~~ all_types;
narasche@4454
   327
    val base_frees = map base_free all_fields;
narasche@4454
   328
narasche@4454
   329
    val tfrees = frees all_types;
narasche@4454
   330
    val zeta = variant tfrees "'z";
narasche@4454
   331
    val zetaT = TFree (zeta, HOLogic.termS); 
narasche@4454
   332
    val z = base_free ("z", zetaT);
narasche@4454
   333
    val recT = foldr mk_prodT (all_types, zetaT);
narasche@4454
   334
    val recT_unitT = foldr mk_prodT (all_types, unitT);
narasche@4454
   335
    val make_schemeT = (all_types @ [zetaT]) ---> recT;
narasche@4454
   336
    val makeT = all_types ---> recT_unitT;
narasche@4454
   337
    val r = base_free ("r", recT);
narasche@4454
   338
narasche@4454
   339
    val errors = check_duplicate_fields (map base (record_field_names thy info))
narasche@4454
   340
  in
narasche@4454
   341
    if not (null errors) 
narasche@4454
   342
      then error (cat_lines errors) else 
narasche@4564
   343
      let val thy = 
narasche@4454
   344
        thy |> Theory.add_path ".."
narasche@4564
   345
            |> Theory.add_tyabbrs_i [(name ^ "_scheme", tfrees @ [zeta], recT, NoSyn)]  
narasche@4564
   346
            |> Theory.add_tyabbrs_i [(name, tfrees, recT_unitT, NoSyn)]  
narasche@4454
   347
            |> Theory.add_path name
narasche@4454
   348
            |> Theory.add_consts_i (decls make_schemeT makeT selT updateT recT current_fields)
narasche@4454
   349
            |> Theory.add_defs_i 
narasche@4454
   350
                  ((make_defs make_schemeT makeT base_frees z thy) @ 
narasche@4454
   351
                   (sel_defs recT r all_fields current_fullfields) @
narasche@4574
   352
                   (update_defs recT r all_fields current_fullfields thy)) 
narasche@4564
   353
      in 
narasche@4564
   354
        thy |> PureThy.store_thmss 
narasche@4564
   355
                 [("record_simps", 
narasche@4564
   356
                   sel_make_scheme_thms recT make_schemeT base_frees z all_fields full thy @  
narasche@4564
   357
                   sel_make_thms recT_unitT makeT base_frees all_fields full thy @
narasche@4564
   358
                   update_make_scheme_thms recT make_schemeT base_frees z all_fields full thy @
narasche@4574
   359
                   update_make_thms recT_unitT makeT base_frees all_fields full thy )]
narasche@4454
   360
            |> Theory.add_path ".." 
narasche@4564
   361
      end
narasche@4564
   362
narasche@4564
   363
(* @ update_make_thms @ 
narasche@4564
   364
                     update_update_thms @ sel_update_thms)]  *)
narasche@4564
   365
narasche@4454
   366
  end;
narasche@4454
   367
narasche@4454
   368
narasche@4454
   369
narasche@4454
   370
(** external interfaces **)
narasche@4454
   371
narasche@4454
   372
(* add_record *)
narasche@4454
   373
narasche@4454
   374
fun add_record_aux prep_typ prep_parent (raw_args, name) raw_parent raw_fields thy =
narasche@4454
   375
  let
narasche@4454
   376
    val _ = require_thy thy "Prod" "record definitions";
narasche@4454
   377
    val sign = sign_of thy;
narasche@4454
   378
    val full_name = Sign.full_name sign name;
narasche@4454
   379
    val make_assocs = map (fn (a, b) => ((a, ~1), b));
narasche@4454
   380
narasche@4454
   381
    val parent = apsome (prep_parent sign) raw_parent;
narasche@4454
   382
    val parent_args = if_none (apsome fst parent) [];
narasche@4454
   383
    val parent_assoc = make_assocs (foldr (op union) ((map typ_tfrees parent_args), []));
narasche@4454
   384
 
narasche@4454
   385
    fun prepare_fields ass [] = []
narasche@4454
   386
      | prepare_fields ass ((name, str)::xs) = 
narasche@4454
   387
         let val type_of_name = prep_typ sign ass str
narasche@4454
   388
         in (name, type_of_name)::
narasche@4454
   389
              (prepare_fields (ass union (make_assocs (typ_tfrees type_of_name))) xs)
narasche@4454
   390
         end;
narasche@4454
   391
    val fields = prepare_fields (parent_assoc) raw_fields;
narasche@4454
   392
    val fields_types = map snd fields;
narasche@4454
   393
    val free_vars = foldr (op union) ((map typ_tfrees fields_types), []);
narasche@4454
   394
narasche@4454
   395
    val check_args = check_raw_args raw_args free_vars thy;
narasche@4454
   396
    val args = snd check_args;
narasche@4454
   397
narasche@4454
   398
    val errors = (check_parent parent name thy) @ 
narasche@4454
   399
                 (check_duplicate_records thy full_name) @
narasche@4454
   400
                 (check_duplicate_args raw_args) @
narasche@4454
   401
                 (fst check_args)
narasche@4454
   402
  in 
narasche@4454
   403
    if not (null errors) 
narasche@4454
   404
      then error (cat_lines errors)
narasche@4454
   405
      else ext_record (args, name) parent fields thy 
narasche@4454
   406
  end
narasche@4454
   407
  handle ERROR =>
narasche@4454
   408
    error ("The error(s) above occurred in record declaration " ^ quote name);
narasche@4454
   409
narasche@4454
   410
narasche@4454
   411
(* internalization methods *)
narasche@4454
   412
narasche@4454
   413
fun read_parent sign name =
narasche@4454
   414
  (case Sign.read_raw_typ (sign, K None) name of
narasche@4454
   415
    Type (name, Ts) => (Ts, name)
narasche@4454
   416
  | _ => error ("Malformed parent specification: " ^ name));
narasche@4454
   417
narasche@4454
   418
fun read_typ sign ass name = 
narasche@4454
   419
  Sign.read_typ (sign, curry assoc ass) name handle TYPE (msg, _, _) => error msg;
narasche@4454
   420
 
narasche@4454
   421
fun cert_typ sign ass T =
narasche@4454
   422
  Sign.certify_typ sign T handle TYPE (msg, _, _) => error msg;
narasche@4454
   423
narasche@4454
   424
narasche@4454
   425
(* add_record(_i) *)
narasche@4454
   426
narasche@4454
   427
val add_record = add_record_aux read_typ read_parent;
narasche@4454
   428
val add_record_i = add_record_aux cert_typ (K I);
narasche@4454
   429
narasche@4454
   430
end;