adapted to new theory data interface;
authorwenzelm
Tue Jun 09 11:37:52 1998 +0200 (1998-06-09)
changeset 5006cdc86a914e63
parent 5005 4486d53a6438
child 5007 0ebd6c91088a
adapted to new theory data interface;
src/HOL/Tools/record_package.ML
src/HOL/thy_data.ML
     1.1 --- a/src/HOL/Tools/record_package.ML	Mon Jun 08 15:58:56 1998 +0200
     1.2 +++ b/src/HOL/Tools/record_package.ML	Tue Jun 09 11:37:52 1998 +0200
     1.3 @@ -256,21 +256,18 @@
     1.4    simps: tthm list};
     1.5  
     1.6  
     1.7 -(* data kind 'records' *)
     1.8 -
     1.9 -local
    1.10 -  val recordsK = Object.kind "HOL/records";
    1.11 -  exception Records of record_info Symtab.table;
    1.12 -
    1.13 +(* data kind '"HOL/records' *)
    1.14  
    1.15 -  val empty = Records Symtab.empty;
    1.16 -
    1.17 -  fun prep_ext (x as Records _) = x;
    1.18 +structure RecordsArgs =
    1.19 +struct
    1.20 +  val name = "HOL/records";
    1.21 +  type T = record_info Symtab.table;
    1.22  
    1.23 -  fun merge (Records tab1, Records tab2) =
    1.24 -    Records (Symtab.merge (K true) (tab1, tab2));
    1.25 +  val empty = Symtab.empty;
    1.26 +  val prep_ext = I;
    1.27 +  val merge: T * T -> T = Symtab.merge (K true);
    1.28  
    1.29 -  fun print sg (Records tab) =
    1.30 +  fun print sg tab =
    1.31      let
    1.32        val prt_typ = Sign.pretty_typ sg;
    1.33        val ext_const = Sign.cond_extern sg Sign.constK;
    1.34 @@ -288,20 +285,18 @@
    1.35      in
    1.36        seq (Pretty.writeln o pretty_record) (Symtab.dest tab)
    1.37      end;
    1.38 -in
    1.39 -  val init_records = Theory.init_data recordsK (empty, prep_ext, merge, print);
    1.40 -  val print_records = Theory.print_data recordsK;
    1.41 -  val get_records = Theory.get_data recordsK (fn Records x => x);
    1.42 -  val put_records = Theory.put_data recordsK Records;
    1.43  end;
    1.44  
    1.45 +structure RecordsData = TheoryDataFun(RecordsArgs);
    1.46 +val print_records = RecordsData.print;
    1.47 +
    1.48  
    1.49  (* get and put records *)
    1.50  
    1.51 -fun get_record thy name = Symtab.lookup (get_records thy, name);
    1.52 +fun get_record thy name = Symtab.lookup (RecordsData.get thy, name);
    1.53  
    1.54  fun put_record name info thy =
    1.55 -  put_records (Symtab.update ((name, info), get_records thy)) thy;
    1.56 +  RecordsData.put (Symtab.update ((name, info), RecordsData.get thy)) thy;
    1.57  
    1.58  
    1.59  (* parent records *)
    1.60 @@ -701,7 +696,7 @@
    1.61  (** setup theory **)
    1.62  
    1.63  val setup =
    1.64 - [init_records,
    1.65 + [RecordsData.init,
    1.66    Theory.add_trfuns
    1.67      ([], [("_record", record_tr), ("_record_scheme", record_scheme_tr)], [], [])];
    1.68  
     2.1 --- a/src/HOL/thy_data.ML	Mon Jun 08 15:58:56 1998 +0200
     2.2 +++ b/src/HOL/thy_data.ML	Tue Jun 09 11:37:52 1998 +0200
     2.3 @@ -28,33 +28,31 @@
     2.4  struct
     2.5  
     2.6  
     2.7 -(* data kind 'datatypes' *)
     2.8 -
     2.9 -local
    2.10 -  val datatypesK = Object.kind "HOL/datatypes";
    2.11 -  exception DatatypeInfo of datatype_info Symtab.table;
    2.12 +(* data kind 'HOL/datatypes' *)
    2.13  
    2.14 -  val empty = DatatypeInfo Symtab.empty;
    2.15 -
    2.16 -  fun prep_ext (x as DatatypeInfo _) = x;
    2.17 +structure DatatypesArgs =
    2.18 +struct
    2.19 +  val name = "HOL/datatypes";
    2.20 +  type T = datatype_info Symtab.table;
    2.21  
    2.22 -  fun merge (DatatypeInfo tab1, DatatypeInfo tab2) =
    2.23 -    DatatypeInfo (Symtab.merge (K true) (tab1, tab2));
    2.24 +  val empty = Symtab.empty;
    2.25 +  val prep_ext = I;
    2.26 +  val merge: T * T -> T = Symtab.merge (K true);
    2.27  
    2.28 -  fun print sg (DatatypeInfo tab) =
    2.29 +  fun print sg tab =
    2.30      Pretty.writeln (Pretty.strs ("datatypes:" ::
    2.31        map (Sign.cond_extern sg Sign.typeK o fst) (Symtab.dest tab)));
    2.32 -in
    2.33 -  val init_datatypes = Theory.init_data datatypesK (empty, prep_ext, merge, print);
    2.34 -  val get_datatypes_sg = Sign.get_data datatypesK (fn DatatypeInfo tab => tab);
    2.35 -  val get_datatypes = get_datatypes_sg o sign_of;
    2.36 -  val put_datatypes = Theory.put_data datatypesK DatatypeInfo;
    2.37  end;
    2.38  
    2.39 +structure DatatypesData = TheoryDataFun(DatatypesArgs);
    2.40 +val get_datatypes_sg = DatatypesData.get_sg;
    2.41 +val get_datatypes = DatatypesData.get;
    2.42 +val put_datatypes = DatatypesData.put;
    2.43 +
    2.44  
    2.45  (* setup *)
    2.46  
    2.47 -val setup = [init_datatypes];
    2.48 +val setup = [DatatypesData.init];
    2.49  
    2.50  
    2.51  end;