src/HOL/Tools/record_package.ML
changeset 16458 4c6fd0c01d28
parent 16379 d29d27e0f59f
child 16783 26fccaaf9cb4
     1.1 --- a/src/HOL/Tools/record_package.ML	Fri Jun 17 18:33:42 2005 +0200
     1.2 +++ b/src/HOL/Tools/record_package.ML	Fri Jun 17 18:35:27 2005 +0200
     1.3 @@ -29,16 +29,16 @@
     1.4    val ext_typeN: string
     1.5    val last_extT: typ -> (string * typ list) option
     1.6    val dest_recTs : typ -> (string * typ list) list
     1.7 -  val get_extT_fields:  Sign.sg -> typ -> ((string * typ) list * (string * typ))
     1.8 -  val get_recT_fields:  Sign.sg -> typ -> ((string * typ) list * (string * typ))
     1.9 -  val get_extension: Sign.sg -> Symtab.key -> (string * typ list) option
    1.10 -  val get_extinjects: Sign.sg -> thm list
    1.11 -  val get_simpset: Sign.sg -> simpset
    1.12 +  val get_extT_fields:  theory -> typ -> ((string * typ) list * (string * typ))
    1.13 +  val get_recT_fields:  theory -> typ -> ((string * typ) list * (string * typ))
    1.14 +  val get_extension: theory -> Symtab.key -> (string * typ list) option
    1.15 +  val get_extinjects: theory -> thm list
    1.16 +  val get_simpset: theory -> simpset
    1.17    val print_records: theory -> unit
    1.18 -  val add_record: string list * string -> string option -> (string * string * mixfix) list 
    1.19 -                  -> theory -> theory
    1.20 -  val add_record_i: string list * string -> (typ list * string) option 
    1.21 -                    -> (string * typ * mixfix) list -> theory -> theory
    1.22 +  val add_record: string list * string -> string option -> (string * string * mixfix) list
    1.23 +    -> theory -> theory
    1.24 +  val add_record_i: string list * string -> (typ list * string) option
    1.25 +    -> (string * typ * mixfix) list -> theory -> theory
    1.26    val setup: (theory -> theory) list
    1.27  end;
    1.28  
    1.29 @@ -235,8 +235,8 @@
    1.30    equalities = equalities, extinjects=extinjects, extsplit = extsplit, splits = splits, 
    1.31    extfields = extfields, fieldext = fieldext }: record_data;
    1.32  
    1.33 -structure RecordsArgs =
    1.34 -struct
    1.35 +structure RecordsData = TheoryDataFun
    1.36 +(struct
    1.37    val name = "HOL/records";       
    1.38    type T = record_data;
    1.39  
    1.40 @@ -246,8 +246,8 @@
    1.41         Symtab.empty [] Symtab.empty Symtab.empty Symtab.empty Symtab.empty;
    1.42  
    1.43    val copy = I;
    1.44 -  val prep_ext = I;
    1.45 -  fun merge
    1.46 +  val extend = I;
    1.47 +  fun merge _
    1.48     ({records = recs1,
    1.49       sel_upd = {selectors = sels1, updates = upds1, simpset = ss1},
    1.50       equalities = equalities1,
    1.51 @@ -296,11 +296,11 @@
    1.52            [prt_typ (Type (name, map TFree args)), Pretty.str " = "] ::
    1.53            pretty_parent parent @ map pretty_field fields));
    1.54      in map pretty_record (Symtab.dest recs) |> Pretty.chunks |> Pretty.writeln end;
    1.55 -end;
    1.56 +end);
    1.57  
    1.58 -structure RecordsData = TheoryDataFun(RecordsArgs);
    1.59  val print_records = RecordsData.print;
    1.60  
    1.61 +
    1.62  (* access 'records' *)
    1.63  
    1.64  fun get_record thy name = Symtab.lookup (#records (RecordsData.get thy), name);
    1.65 @@ -315,7 +315,7 @@
    1.66  
    1.67  (* access 'sel_upd' *)
    1.68  
    1.69 -fun get_sel_upd sg = #sel_upd (RecordsData.get_sg sg);
    1.70 +val get_sel_upd = #sel_upd o RecordsData.get;
    1.71  
    1.72  fun get_selectors sg name = Symtab.lookup (#selectors (get_sel_upd sg), name);
    1.73  fun is_selector sg name = 
    1.74 @@ -353,7 +353,7 @@
    1.75    in RecordsData.put data thy end;
    1.76  
    1.77  fun get_equalities sg name =
    1.78 -  Symtab.lookup (#equalities (RecordsData.get_sg sg), name);
    1.79 +  Symtab.lookup (#equalities (RecordsData.get sg), name);
    1.80  
    1.81  (* access 'extinjects' *)
    1.82  
    1.83 @@ -365,7 +365,7 @@
    1.84                   splits extfields fieldext;
    1.85    in RecordsData.put data thy end;
    1.86  
    1.87 -fun get_extinjects sg = #extinjects (RecordsData.get_sg sg);
    1.88 +fun get_extinjects sg = #extinjects (RecordsData.get sg);
    1.89  
    1.90  (* access 'extsplit' *)
    1.91  
    1.92 @@ -379,7 +379,7 @@
    1.93    in RecordsData.put data thy end;
    1.94  
    1.95  fun get_extsplit sg name =
    1.96 -  Symtab.lookup (#extsplit (RecordsData.get_sg sg), name);
    1.97 +  Symtab.lookup (#extsplit (RecordsData.get sg), name);
    1.98  
    1.99  (* access 'splits' *)
   1.100  
   1.101 @@ -393,13 +393,13 @@
   1.102    in RecordsData.put data thy end;
   1.103  
   1.104  fun get_splits sg name =
   1.105 -  Symtab.lookup (#splits (RecordsData.get_sg sg), name);
   1.106 +  Symtab.lookup (#splits (RecordsData.get sg), name);
   1.107  
   1.108  
   1.109  
   1.110  (* extension of a record name *)
   1.111  fun get_extension sg name =
   1.112 - case Symtab.lookup (#records (RecordsData.get_sg sg),name) of
   1.113 + case Symtab.lookup (#records (RecordsData.get sg),name) of
   1.114          SOME s => SOME (#extension s)
   1.115        | NONE => NONE;
   1.116  
   1.117 @@ -415,7 +415,7 @@
   1.118    in RecordsData.put data thy end;
   1.119  
   1.120  fun get_extfields sg name =
   1.121 -  Symtab.lookup (#extfields (RecordsData.get_sg sg), name);
   1.122 +  Symtab.lookup (#extfields (RecordsData.get sg), name);
   1.123  
   1.124  fun get_extT_fields sg T = 
   1.125    let
   1.126 @@ -425,7 +425,7 @@
   1.127      val midx = maxidx_of_typs (moreT::Ts);
   1.128      fun varify (a, S) = TVar ((a, midx), S);
   1.129      val varifyT = map_type_tfree varify;
   1.130 -    val {records,extfields,...} = RecordsData.get_sg sg;
   1.131 +    val {records,extfields,...} = RecordsData.get sg;
   1.132      val (flds,(more,_)) = split_last (Symtab.lookup_multi (extfields,name));
   1.133      val args = map varifyT (snd (#extension (valOf (Symtab.lookup (records,recname)))));
   1.134  
   1.135 @@ -458,7 +458,7 @@
   1.136  
   1.137  
   1.138  fun get_fieldext sg name =
   1.139 -  Symtab.lookup (#fieldext (RecordsData.get_sg sg), name);
   1.140 +  Symtab.lookup (#fieldext (RecordsData.get sg), name);
   1.141  
   1.142  (* parent records *)
   1.143  
   1.144 @@ -841,7 +841,7 @@
   1.145  
   1.146  fun prove_split_simp sg T prop =
   1.147    let 
   1.148 -    val {sel_upd={simpset,...},extsplit,...} = RecordsData.get_sg sg;
   1.149 +    val {sel_upd={simpset,...},extsplit,...} = RecordsData.get sg;
   1.150      val extsplits = 
   1.151              Library.foldl (fn (thms,(n,_)) => (list (Symtab.lookup (extsplit,n)))@thms) 
   1.152                      ([],dest_recTs T);
   1.153 @@ -880,7 +880,7 @@
   1.154            (case get_updates sg u of SOME u_name =>
   1.155              let
   1.156                fun mk_abs_var x t = (x, fastype_of t);
   1.157 -              val {sel_upd={updates,...},extfields,...} = RecordsData.get_sg sg;
   1.158 +              val {sel_upd={updates,...},extfields,...} = RecordsData.get sg;
   1.159                
   1.160                fun mk_eq_terms ((upd as Const (u,Type(_,[updT,_]))) $ k $ r) =
   1.161  		  (case (Symtab.lookup (updates,u)) of
   1.162 @@ -938,7 +938,7 @@
   1.163      (fn sg => fn _ => fn t =>
   1.164        (case t of ((upd as Const (u, Type(_,[_,Type(_,[T,_])]))) $ k $ r) =>
   1.165   	 let datatype ('a,'b) calc = Init of 'b | Inter of 'a  
   1.166 -             val {sel_upd={selectors,updates,...},extfields,...} = RecordsData.get_sg sg;
   1.167 +             val {sel_upd={selectors,updates,...},extfields,...} = RecordsData.get sg;
   1.168               
   1.169  	     fun mk_abs_var x t = (x, fastype_of t);
   1.170               fun sel_name u = NameSpace.base (unsuffix updateN u);
   1.171 @@ -1142,7 +1142,7 @@
   1.172    let
   1.173      val sg = Thm.sign_of_thm st;
   1.174      val {sel_upd={simpset,...},...} 
   1.175 -            = RecordsData.get_sg sg;
   1.176 +            = RecordsData.get sg;
   1.177  
   1.178      val has_rec = exists_Const
   1.179        (fn (s, Type (_, [Type (_, [T, _]), _])) =>