# HG changeset patch # User narasche # Date 878648977 -3600 # Node ID 57c1e7d709601529285bf98f1d0f70f851185e17 # Parent de6e388f3d8692e37e4dba8597b5925797b867c3 data kinds 'datatypes', data kinds 'records' added diff -r de6e388f3d86 -r 57c1e7d70960 src/HOL/thy_data.ML --- a/src/HOL/thy_data.ML Tue Nov 04 13:35:13 1997 +0100 +++ b/src/HOL/thy_data.ML Tue Nov 04 14:09:37 1997 +0100 @@ -17,6 +17,9 @@ 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_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 @@ -46,33 +49,68 @@ 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 *) + + 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; + + fun put_datatypes tab thy = + Theory.put_data (datatypesK, DatatypeInfo tab) thy; end; -(* get and put datatypes *) +(** records **) + +(* data kind 'records' *) + +(* methods *) + +local -fun get_datatypes_sg sg = - (case Sign.get_data sg datatypesK of - DatatypeInfo tab => tab - | _ => sys_error "get_datatypes_sg"); + val recordsK = "records"; + exception Records of + (string * (string * ctyp) list) Symtab.table; + + fun forget_Records (Records t) = t; (* FIXME *) (* not very nice *) -val get_datatypes = get_datatypes_sg o sign_of; + val empty = Records Symtab.null; + + fun prep_ext r = r; + + fun merge (Records rs1, Records rs2) = Records (Symtab.merge (fn (a,b) => true) (rs1, rs2)); -fun put_datatypes tab thy = - Theory.put_data (datatypesK, DatatypeInfo tab) thy; - - + 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; -(** records **) (* FIXME *) + 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 -val recordsK = "records"; + 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); + end; (** hol_data **) val hol_data = - [Simplifier.simpset_thy_data, ClasetThyData.thy_data, datatypes_thy_data]; - + [Simplifier.simpset_thy_data, ClasetThyData.thy_data, datatypes_thy_data, record_thy_data]; end;