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