# HG changeset patch
# User wenzelm
# Date 878658575 -3600
# Node ID e0382d653d6217c21e20b4b5a427de6e2cdd0dc5
# Parent  c41846a38e2034c8241283e8a506c5dcf7d95dc3
tuned 'records' stuff;

diff -r c41846a38e20 -r e0382d653d62 src/HOL/thy_data.ML
--- a/src/HOL/thy_data.ML	Tue Nov 04 16:46:02 1997 +0100
+++ b/src/HOL/thy_data.ML	Tue Nov 04 16:49:35 1997 +0100
@@ -2,9 +2,15 @@
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-HOL theory data.
+HOL theory data: simpset, claset, records, datatypes.
 *)
 
+(*for records*)
+type record_info =
+ {parent: string option,
+  selectors: (string * ctyp) list};
+
+(*for datatypes*)
 type datatype_info =
  {case_const: term,
   case_rewrites: thm list,
@@ -15,15 +21,16 @@
   exhaust_tac: string -> int -> tactic,
   case_cong: thm};
 
+
 signature THY_DATA =
 sig
-  val datatypesK: string;
-  val get_record_data: theory -> ((string * (string * ctyp) list) Symtab.table);
-  val put_record_data: ((string * (string * ctyp) list) Symtab.table) -> theory -> theory;
+  val get_records: theory -> record_info Symtab.table;
+  val put_records: record_info Symtab.table -> theory -> theory;
   val get_datatypes_sg: Sign.sg -> datatype_info Symtab.table
   val get_datatypes: theory -> datatype_info Symtab.table
   val put_datatypes: datatype_info Symtab.table -> theory -> theory
-  val hol_data: (string * (exn * (exn -> exn) * (exn * exn -> exn) * (exn -> unit))) list
+  val hol_data: (string * (object * (object -> object) *
+    (object * object -> object) * (object -> unit))) list
 end;
 
 structure ThyData: THY_DATA =
@@ -49,68 +56,78 @@
     Pretty.writeln (Pretty.strs ("datatypes:" :: map fst (Symtab.dest tab)));
 in
   val datatypes_thy_data = (datatypesK, (empty, prep_ext, merge, print));
-  (* get and put datatypes *)
+end;
+
+
+(* get and put datatypes *)
 
-  fun get_datatypes_sg sg =
-    (case Sign.get_data sg datatypesK of
-      DatatypeInfo tab => tab
-    | _ => sys_error "get_datatypes_sg");
+fun get_datatypes_sg sg =
+  (case Sign.get_data sg datatypesK of
+    DatatypeInfo tab => tab
+  | _ => sys_error "get_datatypes_sg");
 
-  val get_datatypes = get_datatypes_sg o sign_of;
+val get_datatypes = get_datatypes_sg o sign_of;
 
-  fun put_datatypes tab thy =
-    Theory.put_data (datatypesK, DatatypeInfo tab) thy;
-end;
+fun put_datatypes tab thy =
+  Theory.put_data (datatypesK, DatatypeInfo tab) thy;
+
 
 
 (** records **)
 
 (* data kind 'records' *)
 
+val recordsK = "records";
+exception Records of record_info Symtab.table;
+
+
 (* methods *)
 
 local
-
-  val recordsK = "records";
-  exception Records of
-    (string * (string * ctyp) list) Symtab.table;
-
-  fun forget_Records (Records t) = t; (* FIXME *) (* not very nice *)
-
   val empty = Records Symtab.null;
 
-  fun prep_ext r = r;
+  fun prep_ext (x as Records _) = x;
 
-  fun merge (Records rs1, Records rs2) = Records (Symtab.merge (fn (a,b) => true) (rs1, rs2));
+  fun merge (Records tab1, Records tab2) =
+    Records (Symtab.merge (K true) (tab1, tab2));
 
-  fun print_aux (record_name, (parent, (sels_types))) = 
-     let val sel_types_string = 
-             (map (fn (sel,sel_type) => Pretty.block([Pretty.str (sel ^ " :: "), 
-                                                    Pretty.quote (Pretty.str (Display.string_of_ctyp sel_type))])));
-      in
-      Pretty.big_list ("record " ^ record_name ^ " =")
-                      (if parent = "" then (sel_types_string sels_types)
-                                      else (Pretty.str (parent ^ " +")) :: (sel_types_string sels_types))
-      end;
+  fun print (Records tab) =
+    let
+      fun pretty_parent None = []
+        | pretty_parent (Some name) = [Pretty.str (name ^ " +")];
+
+      fun pretty_sel (c, T) = Pretty.block
+        [Pretty.str (c ^ " :: "), Pretty.brk 1, Pretty.quote (Display.pretty_ctyp T)];
 
-  fun print (Records rs) =
-      if (Symtab.is_null rs) then
-        Pretty.writeln (Pretty.str ("no records available")) else
-        let val data = (Symtab.dest rs) in
-           seq Pretty.writeln (map print_aux data)
-        end;
-  in
+      fun pretty_record (name, {parent, selectors}) =
+        Pretty.big_list (name ^ " =") (pretty_parent parent @ map pretty_sel selectors);
+    in
+      seq (Pretty.writeln o pretty_record) (Symtab.dest tab)
+    end;
+in
+  val record_thy_data = (recordsK, (empty, prep_ext, merge, print));
+end;
+
 
-  val record_thy_data = (recordsK, (empty, prep_ext, merge, print));
-  fun get_record_data thy  = forget_Records(Theory.get_data thy recordsK);
-  fun put_record_data rd = Theory.put_data (recordsK, Records rd);
+(* get and put records *)
 
-  end;
+fun get_records thy =
+  (case Theory.get_data thy recordsK of
+    Records tab => tab
+  | _ => sys_error "get_records");
+
+fun put_records tab thy =
+  Theory.put_data (recordsK, Records tab) thy;
+
 
 
 (** hol_data **)
 
 val hol_data =
- [Simplifier.simpset_thy_data, ClasetThyData.thy_data, datatypes_thy_data, record_thy_data];
+ [Simplifier.simpset_thy_data,          (*see Provers/simplifier.ML*)
+  ClasetThyData.thy_data,               (*see Provers/classical.ML*)
+  datatypes_thy_data,
+  record_thy_data];
+
 
 end;