--- 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;