1.1 --- a/src/CCL/Wfd.thy Sun May 06 21:50:17 2007 +0200
1.2 +++ b/src/CCL/Wfd.thy Mon May 07 00:49:59 2007 +0200
1.3 @@ -500,12 +500,10 @@
1.4
1.5 structure Data = GenericDataFun
1.6 (
1.7 - val name = "CCL/eval";
1.8 type T = thm list;
1.9 val empty = [];
1.10 val extend = I;
1.11 fun merge _ = Drule.merge_rules;
1.12 - fun print _ _ = ();
1.13 );
1.14
1.15 in
1.16 @@ -518,7 +516,6 @@
1.17 DEPTH_SOLVE_1 (resolve_tac (ths @ prems @ Data.get (Context.Proof ctxt)) 1)) 1;
1.18
1.19 val eval_setup =
1.20 - Data.init #>
1.21 Attrib.add_attributes
1.22 [("eval", Attrib.add_del_args eval_add eval_del, "declaration of evaluation rule")] #>
1.23 Method.add_methods [("eval", Method.thms_ctxt_args (fn ths => fn ctxt =>
2.1 --- a/src/HOL/Algebra/ringsimp.ML Sun May 06 21:50:17 2007 +0200
2.2 +++ b/src/HOL/Algebra/ringsimp.ML Mon May 07 00:49:59 2007 +0200
2.3 @@ -20,9 +20,8 @@
2.4 fun struct_eq ((s1: string, ts1), (s2, ts2)) =
2.5 (s1 = s2) andalso eq_list (op aconv) (ts1, ts2);
2.6
2.7 -structure AlgebraData = GenericDataFun
2.8 -(struct
2.9 - val name = "Algebra/algebra";
2.10 +structure Data = GenericDataFun
2.11 +(
2.12 type T = ((string * term list) * thm list) list;
2.13 (* Algebraic structures:
2.14 identifier of the structure, list of operations and simp rules,
2.15 @@ -30,20 +29,16 @@
2.16 val empty = [];
2.17 val extend = I;
2.18 fun merge _ = AList.join struct_eq (K (Library.merge Thm.eq_thm_prop));
2.19 - fun print generic structs =
2.20 - let
2.21 - val ctxt = Context.proof_of generic;
2.22 - val pretty_term = Pretty.quote o ProofContext.pretty_term ctxt;
2.23 - fun pretty_struct ((s, ts), _) = Pretty.block
2.24 - [Pretty.str s, Pretty.str ":", Pretty.brk 1,
2.25 - Pretty.enclose "(" ")" (Pretty.breaks (map pretty_term ts))];
2.26 - in
2.27 - Pretty.big_list "Algebraic structures:" (map pretty_struct structs) |>
2.28 - Pretty.writeln
2.29 - end
2.30 -end);
2.31 +);
2.32
2.33 -val print_structures = AlgebraData.print o Context.Proof;
2.34 +fun print_structures ctxt =
2.35 + let
2.36 + val structs = Data.get (Context.Proof ctxt);
2.37 + val pretty_term = Pretty.quote o ProofContext.pretty_term ctxt;
2.38 + fun pretty_struct ((s, ts), _) = Pretty.block
2.39 + [Pretty.str s, Pretty.str ":", Pretty.brk 1,
2.40 + Pretty.enclose "(" ")" (Pretty.breaks (map pretty_term ts))];
2.41 + in Pretty.writeln (Pretty.big_list "Algebraic structures:" (map pretty_struct structs)) end;
2.42
2.43
2.44 (** Method **)
2.45 @@ -57,17 +52,17 @@
2.46 in asm_full_simp_tac (HOL_ss settermless less addsimps simps) end;
2.47
2.48 fun algebra_tac ctxt =
2.49 - EVERY' (map (fn s => TRY o struct_tac s) (AlgebraData.get (Context.Proof ctxt)));
2.50 + EVERY' (map (fn s => TRY o struct_tac s) (Data.get (Context.Proof ctxt)));
2.51
2.52
2.53 (** Attribute **)
2.54
2.55 fun add_struct_thm s =
2.56 Thm.declaration_attribute
2.57 - (fn thm => AlgebraData.map (AList.map_default struct_eq (s, []) (insert Thm.eq_thm_prop thm)));
2.58 + (fn thm => Data.map (AList.map_default struct_eq (s, []) (insert Thm.eq_thm_prop thm)));
2.59 fun del_struct s =
2.60 Thm.declaration_attribute
2.61 - (fn _ => AlgebraData.map (AList.delete struct_eq s));
2.62 + (fn _ => Data.map (AList.delete struct_eq s));
2.63
2.64 val attribute = Attrib.syntax
2.65 (Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon ||
2.66 @@ -79,7 +74,6 @@
2.67 (** Setup **)
2.68
2.69 val setup =
2.70 - AlgebraData.init #>
2.71 Method.add_methods [("algebra", Method.ctxt_args (Method.SIMPLE_METHOD' o algebra_tac),
2.72 "normalisation of algebraic structure")] #>
2.73 Attrib.add_attributes [("algebra", attribute, "theorems controlling algebra method")];
3.1 --- a/src/HOL/Hyperreal/transfer.ML Sun May 06 21:50:17 2007 +0200
3.2 +++ b/src/HOL/Hyperreal/transfer.ML Mon May 07 00:49:59 2007 +0200
3.3 @@ -16,8 +16,7 @@
3.4 struct
3.5
3.6 structure TransferData = GenericDataFun
3.7 -(struct
3.8 - val name = "HOL/transfer";
3.9 +(
3.10 type T = {
3.11 intros: thm list,
3.12 unfolds: thm list,
3.13 @@ -35,8 +34,7 @@
3.14 unfolds = Drule.merge_rules (unfolds1, unfolds2),
3.15 refolds = Drule.merge_rules (refolds1, refolds2),
3.16 consts = Library.merge (op =) (consts1, consts2)} : T;
3.17 - fun print _ _ = ();
3.18 -end);
3.19 +);
3.20
3.21 val transfer_start = thm "transfer_start"
3.22
3.23 @@ -109,7 +107,6 @@
3.24 {intros=intros, unfolds=unfolds, refolds=refolds, consts=c::consts}))
3.25
3.26 val setup =
3.27 - TransferData.init #>
3.28 Attrib.add_attributes
3.29 [("transfer_intro", Attrib.add_del_args intro_add intro_del,
3.30 "declaration of transfer introduction rule"),
4.1 --- a/src/HOL/Import/hol4rews.ML Sun May 06 21:50:17 2007 +0200
4.2 +++ b/src/HOL/Import/hol4rews.ML Mon May 07 00:49:59 2007 +0200
4.3 @@ -12,102 +12,70 @@
4.4 | Generating of string
4.5 | Replaying of string
4.6
4.7 -structure HOL4DefThyArgs: THEORY_DATA_ARGS =
4.8 -struct
4.9 -val name = "HOL4/import_status"
4.10 -type T = ImportStatus
4.11 -val empty = NoImport
4.12 -val copy = I
4.13 -val extend = I
4.14 -fun merge _ (NoImport,NoImport) = NoImport
4.15 - | merge _ _ = (warning "Import status set during merge"; NoImport)
4.16 -fun print _ import_status =
4.17 - Pretty.writeln (Pretty.str (case import_status of NoImport => "No current import" | Generating thyname => ("Generating " ^ thyname) | Replaying thyname => ("Replaying " ^ thyname)))
4.18 -end;
4.19 +structure HOL4DefThy = TheoryDataFun
4.20 +(
4.21 + type T = ImportStatus
4.22 + val empty = NoImport
4.23 + val copy = I
4.24 + val extend = I
4.25 + fun merge _ (NoImport,NoImport) = NoImport
4.26 + | merge _ _ = (warning "Import status set during merge"; NoImport)
4.27 +)
4.28
4.29 -structure HOL4DefThy = TheoryDataFun(HOL4DefThyArgs);
4.30 -
4.31 -structure ImportSegmentArgs: THEORY_DATA_ARGS =
4.32 -struct
4.33 -val name = "HOL4/import_segment"
4.34 -type T = string
4.35 -val empty = ""
4.36 -val copy = I
4.37 -val extend = I
4.38 -fun merge _ ("",arg) = arg
4.39 - | merge _ (arg,"") = arg
4.40 - | merge _ (s1,s2) =
4.41 - if s1 = s2
4.42 - then s1
4.43 - else error "Trying to merge two different import segments"
4.44 -fun print _ import_segment =
4.45 - Pretty.writeln (Pretty.str ("Import segment: " ^ import_segment))
4.46 -end;
4.47 -
4.48 -structure ImportSegment = TheoryDataFun(ImportSegmentArgs);
4.49 +structure ImportSegment = TheoryDataFun
4.50 +(
4.51 + type T = string
4.52 + val empty = ""
4.53 + val copy = I
4.54 + val extend = I
4.55 + fun merge _ ("",arg) = arg
4.56 + | merge _ (arg,"") = arg
4.57 + | merge _ (s1,s2) =
4.58 + if s1 = s2
4.59 + then s1
4.60 + else error "Trying to merge two different import segments"
4.61 +)
4.62
4.63 val get_import_segment = ImportSegment.get
4.64 val set_import_segment = ImportSegment.put
4.65
4.66 -structure HOL4UNamesArgs: THEORY_DATA_ARGS =
4.67 -struct
4.68 -val name = "HOL4/used_names"
4.69 -type T = string list
4.70 -val empty = []
4.71 -val copy = I
4.72 -val extend = I
4.73 -fun merge _ ([],[]) = []
4.74 - | merge _ _ = error "Used names not empty during merge"
4.75 -fun print _ used_names =
4.76 - Pretty.writeln (Pretty.str "Printing of HOL4/used_names Not implemented")
4.77 -end;
4.78 +structure HOL4UNames = TheoryDataFun
4.79 +(
4.80 + type T = string list
4.81 + val empty = []
4.82 + val copy = I
4.83 + val extend = I
4.84 + fun merge _ ([],[]) = []
4.85 + | merge _ _ = error "Used names not empty during merge"
4.86 +)
4.87
4.88 -structure HOL4UNames = TheoryDataFun(HOL4UNamesArgs);
4.89 +structure HOL4Dump = TheoryDataFun
4.90 +(
4.91 + type T = string * string * string list
4.92 + val empty = ("","",[])
4.93 + val copy = I
4.94 + val extend = I
4.95 + fun merge _ (("","",[]),("","",[])) = ("","",[])
4.96 + | merge _ _ = error "Dump data not empty during merge"
4.97 +)
4.98
4.99 -structure HOL4DumpArgs: THEORY_DATA_ARGS =
4.100 -struct
4.101 -val name = "HOL4/dump_data"
4.102 -type T = string * string * string list
4.103 -val empty = ("","",[])
4.104 -val copy = I
4.105 -val extend = I
4.106 -fun merge _ (("","",[]),("","",[])) = ("","",[])
4.107 - | merge _ _ = error "Dump data not empty during merge"
4.108 -fun print _ dump_data =
4.109 - Pretty.writeln (Pretty.str "Printing of HOL4/dump_data Not implemented")
4.110 -end;
4.111 +structure HOL4Moves = TheoryDataFun
4.112 +(
4.113 + type T = string Symtab.table
4.114 + val empty = Symtab.empty
4.115 + val copy = I
4.116 + val extend = I
4.117 + fun merge _ : T * T -> T = Symtab.merge (K true)
4.118 +)
4.119
4.120 -structure HOL4Dump = TheoryDataFun(HOL4DumpArgs);
4.121 -
4.122 -structure HOL4MovesArgs: THEORY_DATA_ARGS =
4.123 -struct
4.124 -val name = "HOL4/moves"
4.125 -type T = string Symtab.table
4.126 -val empty = Symtab.empty
4.127 -val copy = I
4.128 -val extend = I
4.129 -fun merge _ : T * T -> T = Symtab.merge (K true)
4.130 -fun print _ tab =
4.131 - Pretty.writeln (Pretty.big_list "HOL4 moves:"
4.132 - (Symtab.fold (fn (bef, aft) => fn xl => (Pretty.str (bef ^ " --> " ^ aft) :: xl)) tab []))
4.133 -end;
4.134 -
4.135 -structure HOL4Moves = TheoryDataFun(HOL4MovesArgs);
4.136 -
4.137 -structure HOL4ImportsArgs: THEORY_DATA_ARGS =
4.138 -struct
4.139 -val name = "HOL4/imports"
4.140 -type T = string Symtab.table
4.141 -val empty = Symtab.empty
4.142 -val copy = I
4.143 -val extend = I
4.144 -fun merge _ : T * T -> T = Symtab.merge (K true)
4.145 -fun print _ tab =
4.146 - Pretty.writeln (Pretty.big_list "HOL4 imports:"
4.147 - (Symtab.fold (fn (thyname, segname) => fn xl => (Pretty.str (thyname ^ " imported from segment " ^ segname) :: xl)) tab []))
4.148 -end;
4.149 -
4.150 -structure HOL4Imports = TheoryDataFun(HOL4ImportsArgs);
4.151 +structure HOL4Imports = TheoryDataFun
4.152 +(
4.153 + type T = string Symtab.table
4.154 + val empty = Symtab.empty
4.155 + val copy = I
4.156 + val extend = I
4.157 + fun merge _ : T * T -> T = Symtab.merge (K true)
4.158 +)
4.159
4.160 fun get_segment2 thyname thy =
4.161 Symtab.lookup (HOL4Imports.get thy) thyname
4.162 @@ -120,143 +88,86 @@
4.163 HOL4Imports.put imps' thy
4.164 end
4.165
4.166 -structure HOL4CMovesArgs: THEORY_DATA_ARGS =
4.167 -struct
4.168 -val name = "HOL4/constant_moves"
4.169 -type T = string Symtab.table
4.170 -val empty = Symtab.empty
4.171 -val copy = I
4.172 -val extend = I
4.173 -fun merge _ : T * T -> T = Symtab.merge (K true)
4.174 -fun print _ tab =
4.175 - Pretty.writeln (Pretty.big_list "HOL4 constant moves:"
4.176 - (Symtab.fold (fn (bef, aft) => fn xl => (Pretty.str (bef ^ " --> " ^ aft) :: xl)) tab []))
4.177 -end;
4.178 +structure HOL4CMoves = TheoryDataFun
4.179 +(
4.180 + type T = string Symtab.table
4.181 + val empty = Symtab.empty
4.182 + val copy = I
4.183 + val extend = I
4.184 + fun merge _ : T * T -> T = Symtab.merge (K true)
4.185 +)
4.186
4.187 -structure HOL4CMoves = TheoryDataFun(HOL4CMovesArgs);
4.188 +structure HOL4Maps = TheoryDataFun
4.189 +(
4.190 + type T = (string option) StringPair.table
4.191 + val empty = StringPair.empty
4.192 + val copy = I
4.193 + val extend = I
4.194 + fun merge _ : T * T -> T = StringPair.merge (K true)
4.195 +)
4.196
4.197 -structure HOL4MapsArgs: THEORY_DATA_ARGS =
4.198 -struct
4.199 -val name = "HOL4/mappings"
4.200 -type T = (string option) StringPair.table
4.201 -val empty = StringPair.empty
4.202 -val copy = I
4.203 -val extend = I
4.204 -fun merge _ : T * T -> T = StringPair.merge (K true)
4.205 -fun print _ tab =
4.206 - Pretty.writeln (Pretty.big_list "HOL4 mappings:"
4.207 - (StringPair.fold (fn ((bthy, bthm), isathm) => fn xl =>
4.208 - (Pretty.str (bthy ^ "." ^ bthm ^ (case isathm of SOME th => " --> " ^ th | NONE => "IGNORED")) :: xl)) tab []))
4.209 -end;
4.210 +structure HOL4Thms = TheoryDataFun
4.211 +(
4.212 + type T = holthm StringPair.table
4.213 + val empty = StringPair.empty
4.214 + val copy = I
4.215 + val extend = I
4.216 + fun merge _ : T * T -> T = StringPair.merge (K true)
4.217 +)
4.218
4.219 -structure HOL4Maps = TheoryDataFun(HOL4MapsArgs);
4.220 +structure HOL4ConstMaps = TheoryDataFun
4.221 +(
4.222 + type T = (bool * string * typ option) StringPair.table
4.223 + val empty = StringPair.empty
4.224 + val copy = I
4.225 + val extend = I
4.226 + fun merge _ : T * T -> T = StringPair.merge (K true)
4.227 +)
4.228
4.229 -structure HOL4ThmsArgs: THEORY_DATA_ARGS =
4.230 -struct
4.231 -val name = "HOL4/theorems"
4.232 -type T = holthm StringPair.table
4.233 -val empty = StringPair.empty
4.234 -val copy = I
4.235 -val extend = I
4.236 -fun merge _ : T * T -> T = StringPair.merge (K true)
4.237 -fun print _ tab =
4.238 - Pretty.writeln (Pretty.big_list "HOL4 mappings:"
4.239 - (StringPair.fold (fn ((bthy, bthm), (_, thm)) => fn xl => (Pretty.str (bthy ^ "." ^ bthm ^ ":") :: Display.pretty_thm thm :: xl)) tab []))
4.240 -end;
4.241 +structure HOL4Rename = TheoryDataFun
4.242 +(
4.243 + type T = string StringPair.table
4.244 + val empty = StringPair.empty
4.245 + val copy = I
4.246 + val extend = I
4.247 + fun merge _ : T * T -> T = StringPair.merge (K true)
4.248 +)
4.249
4.250 -structure HOL4Thms = TheoryDataFun(HOL4ThmsArgs);
4.251 +structure HOL4DefMaps = TheoryDataFun
4.252 +(
4.253 + type T = string StringPair.table
4.254 + val empty = StringPair.empty
4.255 + val copy = I
4.256 + val extend = I
4.257 + fun merge _ : T * T -> T = StringPair.merge (K true)
4.258 +)
4.259
4.260 -structure HOL4ConstMapsArgs: THEORY_DATA_ARGS =
4.261 -struct
4.262 -val name = "HOL4/constmappings"
4.263 -type T = (bool * string * typ option) StringPair.table
4.264 -val empty = StringPair.empty
4.265 -val copy = I
4.266 -val extend = I
4.267 -fun merge _ : T * T -> T = StringPair.merge (K true)
4.268 -fun print _ tab =
4.269 - Pretty.writeln (Pretty.big_list "HOL4 constant mappings:"
4.270 - (StringPair.fold (fn ((bthy, bconst), (internal, isaconst, _)) => fn xl =>
4.271 - (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ isaconst ^ (if internal then " (*)" else "")) :: xl)) tab []))
4.272 -end;
4.273 +structure HOL4TypeMaps = TheoryDataFun
4.274 +(
4.275 + type T = (bool * string) StringPair.table
4.276 + val empty = StringPair.empty
4.277 + val copy = I
4.278 + val extend = I
4.279 + fun merge _ : T * T -> T = StringPair.merge (K true)
4.280 +)
4.281
4.282 -structure HOL4ConstMaps = TheoryDataFun(HOL4ConstMapsArgs);
4.283 +structure HOL4Pending = TheoryDataFun
4.284 +(
4.285 + type T = ((term * term) list * thm) StringPair.table
4.286 + val empty = StringPair.empty
4.287 + val copy = I
4.288 + val extend = I
4.289 + fun merge _ : T * T -> T = StringPair.merge (K true)
4.290 +)
4.291
4.292 -structure HOL4RenameArgs: THEORY_DATA_ARGS =
4.293 -struct
4.294 -val name = "HOL4/renamings"
4.295 -type T = string StringPair.table
4.296 -val empty = StringPair.empty
4.297 -val copy = I
4.298 -val extend = I
4.299 -fun merge _ : T * T -> T = StringPair.merge (K true)
4.300 -fun print _ tab =
4.301 - Pretty.writeln (Pretty.big_list "HOL4 constant renamings:"
4.302 - (StringPair.fold (fn ((bthy,bconst),newname) => fn xl => (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ newname)::xl)) tab []))
4.303 -end;
4.304 -
4.305 -structure HOL4Rename = TheoryDataFun(HOL4RenameArgs);
4.306 -
4.307 -structure HOL4DefMapsArgs: THEORY_DATA_ARGS =
4.308 -struct
4.309 -val name = "HOL4/def_maps"
4.310 -type T = string StringPair.table
4.311 -val empty = StringPair.empty
4.312 -val copy = I
4.313 -val extend = I
4.314 -fun merge _ : T * T -> T = StringPair.merge (K true)
4.315 -fun print _ tab =
4.316 - Pretty.writeln (Pretty.big_list "HOL4 constant definitions:"
4.317 - (StringPair.fold (fn ((bthy,bconst),newname) => fn xl => (Pretty.str (bthy ^ "." ^ bconst ^ ": " ^ newname)::xl)) tab []))
4.318 -end;
4.319 -
4.320 -structure HOL4DefMaps = TheoryDataFun(HOL4DefMapsArgs);
4.321 -
4.322 -structure HOL4TypeMapsArgs: THEORY_DATA_ARGS =
4.323 -struct
4.324 -val name = "HOL4/typemappings"
4.325 -type T = (bool * string) StringPair.table
4.326 -val empty = StringPair.empty
4.327 -val copy = I
4.328 -val extend = I
4.329 -fun merge _ : T * T -> T = StringPair.merge (K true)
4.330 -fun print _ tab =
4.331 - Pretty.writeln (Pretty.big_list "HOL4 type mappings:"
4.332 - (StringPair.fold (fn ((bthy, bconst), (internal, isaconst)) => fn xl =>
4.333 - (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ isaconst ^ (if internal then " (*)" else "")) :: xl)) tab []))
4.334 -end;
4.335 -
4.336 -structure HOL4TypeMaps = TheoryDataFun(HOL4TypeMapsArgs);
4.337 -
4.338 -structure HOL4PendingArgs: THEORY_DATA_ARGS =
4.339 -struct
4.340 -val name = "HOL4/pending"
4.341 -type T = ((term * term) list * thm) StringPair.table
4.342 -val empty = StringPair.empty
4.343 -val copy = I
4.344 -val extend = I
4.345 -fun merge _ : T * T -> T = StringPair.merge (K true)
4.346 -fun print _ tab =
4.347 - Pretty.writeln (Pretty.big_list "HOL4 pending theorems:"
4.348 - (StringPair.fold (fn ((bthy,bthm),(_,th)) => fn xl => (Pretty.chunks [Pretty.str (bthy ^ "." ^ bthm ^ ":"),Display.pretty_thm th]::xl)) tab []))
4.349 -end;
4.350 -
4.351 -structure HOL4Pending = TheoryDataFun(HOL4PendingArgs);
4.352 -
4.353 -structure HOL4RewritesArgs: THEORY_DATA_ARGS =
4.354 -struct
4.355 -val name = "HOL4/rewrites"
4.356 -type T = thm list
4.357 -val empty = []
4.358 -val copy = I
4.359 -val extend = I
4.360 -fun merge _ = Library.gen_union Thm.eq_thm
4.361 -fun print _ thms =
4.362 - Pretty.writeln (Pretty.big_list "HOL4 rewrite rules:"
4.363 - (map Display.pretty_thm thms))
4.364 -end;
4.365 -
4.366 -structure HOL4Rewrites = TheoryDataFun(HOL4RewritesArgs);
4.367 +structure HOL4Rewrites = TheoryDataFun
4.368 +(
4.369 + type T = thm list
4.370 + val empty = []
4.371 + val copy = I
4.372 + val extend = I
4.373 + fun merge _ = Library.gen_union Thm.eq_thm
4.374 +)
4.375
4.376 val hol4_debug = ref false
4.377 fun message s = if !hol4_debug then writeln s else ()
4.378 @@ -677,7 +588,7 @@
4.379 | _ => error "hol4rews.set_used_names called on initialized data!"
4.380 end
4.381
4.382 -val clear_used_names = HOL4UNames.put HOL4UNamesArgs.empty
4.383 +val clear_used_names = HOL4UNames.put [];
4.384
4.385 fun get_defmap thyname const thy =
4.386 let
4.387 @@ -737,21 +648,6 @@
4.388 |> add_hol4_const_mapping "min" "@" false "Hilbert_Choice.Eps"
4.389 in
4.390 val hol4_setup =
4.391 - HOL4Rewrites.init #>
4.392 - HOL4Maps.init #>
4.393 - HOL4UNames.init #>
4.394 - HOL4DefMaps.init #>
4.395 - HOL4Moves.init #>
4.396 - HOL4CMoves.init #>
4.397 - HOL4ConstMaps.init #>
4.398 - HOL4Rename.init #>
4.399 - HOL4TypeMaps.init #>
4.400 - HOL4Pending.init #>
4.401 - HOL4Thms.init #>
4.402 - HOL4Dump.init #>
4.403 - HOL4DefThy.init #>
4.404 - HOL4Imports.init #>
4.405 - ImportSegment.init #>
4.406 initial_maps #>
4.407 Attrib.add_attributes
4.408 [("hol4rew", Attrib.no_args add_hol4_rewrite, "HOL4 rewrite rule")]
5.1 --- a/src/HOL/Import/import_package.ML Sun May 06 21:50:17 2007 +0200
5.2 +++ b/src/HOL/Import/import_package.ML Mon May 07 00:49:59 2007 +0200
5.3 @@ -10,18 +10,14 @@
5.4 val debug : bool ref
5.5 end
5.6
5.7 -structure ImportDataArgs: THEORY_DATA_ARGS =
5.8 -struct
5.9 -val name = "HOL4/import_data"
5.10 -type T = ProofKernel.thm option array option
5.11 -val empty = NONE
5.12 -val copy = I
5.13 -val extend = I
5.14 -fun merge _ _ = NONE
5.15 -fun print _ _ = ()
5.16 -end
5.17 -
5.18 -structure ImportData = TheoryDataFun(ImportDataArgs)
5.19 +structure ImportData = TheoryDataFun
5.20 +(
5.21 + type T = ProofKernel.thm option array option
5.22 + val empty = NONE
5.23 + val copy = I
5.24 + val extend = I
5.25 + fun merge _ _ = NONE
5.26 +)
5.27
5.28 structure ImportPackage :> IMPORT_PACKAGE =
5.29 struct
5.30 @@ -80,6 +76,6 @@
5.31 Method.SIMPLE_METHOD (import_tac arg thy)
5.32 end)
5.33
5.34 -val setup = Method.add_method("import",import_meth,"Import HOL4 theorem") #> ImportData.init
5.35 +val setup = Method.add_method("import",import_meth,"Import HOL4 theorem")
5.36 end
5.37
6.1 --- a/src/HOL/Import/shuffler.ML Sun May 06 21:50:17 2007 +0200
6.2 +++ b/src/HOL/Import/shuffler.ML Mon May 07 00:49:59 2007 +0200
6.3 @@ -75,20 +75,18 @@
6.4 | _ => raise THM("Not an equality",0,[th]))
6.5 handle _ => raise THM("Couldn't make object equality",0,[th])
6.6
6.7 -structure ShuffleDataArgs: THEORY_DATA_ARGS =
6.8 -struct
6.9 -val name = "HOL/shuffles"
6.10 -type T = thm list
6.11 -val empty = []
6.12 -val copy = I
6.13 -val extend = I
6.14 -fun merge _ = Library.gen_union Thm.eq_thm
6.15 -fun print _ thms =
6.16 - Pretty.writeln (Pretty.big_list "Shuffle theorems:"
6.17 - (map Display.pretty_thm thms))
6.18 -end
6.19 +structure ShuffleData = TheoryDataFun
6.20 +(
6.21 + type T = thm list
6.22 + val empty = []
6.23 + val copy = I
6.24 + val extend = I
6.25 + fun merge _ = Library.gen_union Thm.eq_thm
6.26 +)
6.27
6.28 -structure ShuffleData = TheoryDataFun(ShuffleDataArgs)
6.29 +fun print_shuffles thy =
6.30 + Pretty.writeln (Pretty.big_list "Shuffle theorems:"
6.31 + (map Display.pretty_thm (ShuffleData.get thy)))
6.32
6.33 val weaken =
6.34 let
6.35 @@ -667,8 +665,6 @@
6.36 Method.SIMPLE_METHOD' (gen_shuffle_tac thy true (map (pair "premise") prems))
6.37 end
6.38
6.39 -val print_shuffles = ShuffleData.print
6.40 -
6.41 fun add_shuffle_rule thm thy =
6.42 let
6.43 val shuffles = ShuffleData.get thy
6.44 @@ -682,9 +678,10 @@
6.45 val shuffle_attr = Thm.declaration_attribute (fn th => Context.mapping (add_shuffle_rule th) I);
6.46
6.47 val setup =
6.48 - Method.add_method ("shuffle_tac",Method.thms_ctxt_args shuffle_meth,"solve goal by shuffling terms around") #>
6.49 - Method.add_method ("search_tac",Method.ctxt_args search_meth,"search for suitable theorems") #>
6.50 - ShuffleData.init #>
6.51 + Method.add_method ("shuffle_tac",
6.52 + Method.thms_ctxt_args shuffle_meth,"solve goal by shuffling terms around") #>
6.53 + Method.add_method ("search_tac",
6.54 + Method.ctxt_args search_meth,"search for suitable theorems") #>
6.55 add_shuffle_rule weaken #>
6.56 add_shuffle_rule equiv_comm #>
6.57 add_shuffle_rule imp_comm #>
7.1 --- a/src/HOL/Inductive.thy Sun May 06 21:50:17 2007 +0200
7.2 +++ b/src/HOL/Inductive.thy Mon May 07 00:49:59 2007 +0200
7.3 @@ -118,7 +118,6 @@
7.4 use "Tools/datatype_realizer.ML"
7.5
7.6 use "Tools/datatype_hooks.ML"
7.7 -setup DatatypeHooks.setup
7.8
7.9 use "Tools/datatype_package.ML"
7.10 setup DatatypePackage.setup
8.1 --- a/src/HOL/Nominal/Nominal.thy Sun May 06 21:50:17 2007 +0200
8.2 +++ b/src/HOL/Nominal/Nominal.thy Mon May 07 00:49:59 2007 +0200
8.3 @@ -3226,7 +3226,6 @@
8.4 (* setup for the individial atom-kinds *)
8.5 (* and nominal datatypes *)
8.6 use "nominal_atoms.ML"
8.7 -setup "NominalAtoms.setup"
8.8
8.9 (************************************************************)
8.10 (* various tactics for analysing permutations, supports etc *)
8.11 @@ -3288,7 +3287,6 @@
8.12 (************************************************)
8.13 (* main file for constructing nominal datatypes *)
8.14 use "nominal_package.ML"
8.15 -setup "NominalPackage.setup"
8.16
8.17 (******************************************************)
8.18 (* primitive recursive functions on nominal datatypes *)
9.1 --- a/src/HOL/Nominal/nominal_atoms.ML Sun May 06 21:50:17 2007 +0200
9.2 +++ b/src/HOL/Nominal/nominal_atoms.ML Mon May 07 00:49:59 2007 +0200
9.3 @@ -13,7 +13,6 @@
9.4 val get_atom_info : theory -> string -> atom_info option
9.5 val atoms_of : theory -> string list
9.6 val mk_permT : typ -> typ
9.7 - val setup : theory -> theory
9.8 end
9.9
9.10 structure NominalAtoms : NOMINAL_ATOMS =
9.11 @@ -23,27 +22,21 @@
9.12 val Collect_const = thm "Collect_const";
9.13
9.14
9.15 -(* data kind 'HOL/nominal' *)
9.16 +(* theory data *)
9.17
9.18 type atom_info =
9.19 {pt_class : string,
9.20 fs_class : string,
9.21 cp_classes : (string * string) list};
9.22
9.23 -structure NominalArgs =
9.24 -struct
9.25 - val name = "HOL/nominal";
9.26 +structure NominalData = TheoryDataFun
9.27 +(
9.28 type T = atom_info Symtab.table;
9.29 -
9.30 val empty = Symtab.empty;
9.31 val copy = I;
9.32 val extend = I;
9.33 fun merge _ x = Symtab.merge (K true) x;
9.34 -
9.35 - fun print sg tab = ();
9.36 -end;
9.37 -
9.38 -structure NominalData = TheoryDataFun(NominalArgs);
9.39 +);
9.40
9.41 fun make_atom_info ((pt_class, fs_class), cp_classes) =
9.42 {pt_class = pt_class,
9.43 @@ -889,6 +882,4 @@
9.44
9.45 val _ = OuterSyntax.add_parsers [atom_declP];
9.46
9.47 -val setup = NominalData.init;
9.48 -
9.49 end;
10.1 --- a/src/HOL/Nominal/nominal_package.ML Sun May 06 21:50:17 2007 +0200
10.2 +++ b/src/HOL/Nominal/nominal_package.ML Mon May 07 00:49:59 2007 +0200
10.3 @@ -17,7 +17,6 @@
10.4 val perm_of_pair: term * term -> term
10.5 val mk_not_sym: thm list -> thm list
10.6 val perm_simproc: simproc
10.7 - val setup: theory -> theory
10.8 end
10.9
10.10 structure NominalPackage : NOMINAL_PACKAGE =
10.11 @@ -68,7 +67,7 @@
10.12
10.13 end;
10.14
10.15 -(* data kind 'HOL/nominal_datatypes' *)
10.16 +(* theory data *)
10.17
10.18 type descr = (int * (string * dtyp list * (string * (dtyp list * dtyp) list) list)) list;
10.19
10.20 @@ -83,25 +82,19 @@
10.21 inject : thm list};
10.22
10.23 structure NominalDatatypesData = TheoryDataFun
10.24 -(struct
10.25 - val name = "HOL/nominal_datatypes";
10.26 +(
10.27 type T = nominal_datatype_info Symtab.table;
10.28 -
10.29 val empty = Symtab.empty;
10.30 val copy = I;
10.31 val extend = I;
10.32 fun merge _ tabs : T = Symtab.merge (K true) tabs;
10.33 -
10.34 - fun print sg tab =
10.35 - Pretty.writeln (Pretty.strs ("nominal datatypes:" ::
10.36 - map #1 (NameSpace.extern_table (Sign.type_space sg, tab))));
10.37 -end);
10.38 +);
10.39
10.40 val get_nominal_datatypes = NominalDatatypesData.get;
10.41 val put_nominal_datatypes = NominalDatatypesData.put;
10.42 val map_nominal_datatypes = NominalDatatypesData.map;
10.43 val get_nominal_datatype = Symtab.lookup o get_nominal_datatypes;
10.44 -val setup = NominalDatatypesData.init;
10.45 +
10.46
10.47 (**** make datatype info ****)
10.48
11.1 --- a/src/HOL/Nominal/nominal_thmdecls.ML Sun May 06 21:50:17 2007 +0200
11.2 +++ b/src/HOL/Nominal/nominal_thmdecls.ML Mon May 07 00:49:59 2007 +0200
11.3 @@ -1,13 +1,13 @@
11.4 (* ID: "$Id$"
11.5 Authors: Julien Narboux and Christian Urban
11.6
11.7 - This file introduces the infrastructure for the lemma
11.8 + This file introduces the infrastructure for the lemma
11.9 declaration "eqvts" "bijs" and "freshs".
11.10
11.11 - By attaching [eqvt] [bij] or [fresh] to a lemma, the lemma gets stored
11.12 + By attaching [eqvt] [bij] or [fresh] to a lemma, the lemma gets stored
11.13 in a data-slot in the theory context. Possible modifiers
11.14 are [attribute add] and [attribute del] for adding and deleting,
11.15 - respectively the lemma from the data-slot.
11.16 + respectively the lemma from the data-slot.
11.17 *)
11.18
11.19 signature NOMINAL_THMDECLS =
11.20 @@ -21,7 +21,7 @@
11.21 val get_eqvt_thms: theory -> thm list
11.22 val get_fresh_thms: theory -> thm list
11.23 val get_bij_thms: theory -> thm list
11.24 -
11.25 +
11.26
11.27 val NOMINAL_EQVT_DEBUG : bool ref
11.28 end;
11.29 @@ -31,24 +31,12 @@
11.30
11.31 structure Data = GenericDataFun
11.32 (
11.33 - val name = "HOL/Nominal/eqvt";
11.34 type T = {eqvts:thm list, freshs:thm list, bijs:thm list};
11.35 val empty = ({eqvts=[], freshs=[], bijs=[]}:T);
11.36 val extend = I;
11.37 - fun merge _ (r1:T,r2:T) = {eqvts = Drule.merge_rules (#eqvts r1, #eqvts r2),
11.38 - freshs = Drule.merge_rules (#freshs r1, #freshs r2),
11.39 + fun merge _ (r1:T,r2:T) = {eqvts = Drule.merge_rules (#eqvts r1, #eqvts r2),
11.40 + freshs = Drule.merge_rules (#freshs r1, #freshs r2),
11.41 bijs = Drule.merge_rules (#bijs r1, #bijs r2)}
11.42 - fun print context (data:T) =
11.43 - let
11.44 - fun print_aux msg thms =
11.45 - Pretty.writeln (Pretty.big_list msg
11.46 - (map (ProofContext.pretty_thm (Context.proof_of context)) thms))
11.47 - in
11.48 - (print_aux "Equivariance lemmas: " (#eqvts data);
11.49 - print_aux "Freshness lemmas: " (#freshs data);
11.50 - print_aux "Bijection lemmas: " (#bijs data))
11.51 - end;
11.52 -
11.53 );
11.54
11.55 (* Exception for when a theorem does not conform with form of an equivariance lemma. *)
11.56 @@ -62,7 +50,19 @@
11.57 (* eqality-lemma can be derived. *)
11.58 exception EQVT_FORM of string;
11.59
11.60 -val print_data = Data.print o Context.Proof;
11.61 +fun print_data ctxt =
11.62 + let
11.63 + val data = Data.get (Context.Proof ctxt);
11.64 + fun pretty_thms msg thms =
11.65 + Pretty.big_list msg (map (ProofContext.pretty_thm ctxt) thms);
11.66 + in
11.67 + Pretty.writeln (Pretty.chunks
11.68 + [pretty_thms "Equivariance lemmas:" (#eqvts data),
11.69 + pretty_thms "Freshness lemmas:" (#freshs data),
11.70 + pretty_thms "Bijection lemmas:" (#bijs data)])
11.71 + end;
11.72 +
11.73 +
11.74 val get_eqvt_thms = Context.Theory #> Data.get #> #eqvts;
11.75 val get_fresh_thms = Context.Theory #> Data.get #> #freshs;
11.76 val get_bij_thms = Context.Theory #> Data.get #> #bijs;
11.77 @@ -75,56 +75,56 @@
11.78
11.79 val NOMINAL_EQVT_DEBUG = ref false;
11.80
11.81 -fun tactic (msg,tac) =
11.82 - if !NOMINAL_EQVT_DEBUG
11.83 +fun tactic (msg,tac) =
11.84 + if !NOMINAL_EQVT_DEBUG
11.85 then (EVERY [tac, print_tac ("after "^msg)])
11.86 - else tac
11.87 + else tac
11.88
11.89 fun dynamic_thms thy name = PureThy.get_thms thy (Name name)
11.90
11.91 -fun tactic_eqvt ctx orig_thm pi typi =
11.92 - let
11.93 +fun tactic_eqvt ctx orig_thm pi typi =
11.94 + let
11.95 val mypi = Thm.cterm_of ctx (Var (pi,typi))
11.96 val mypifree = Thm.cterm_of ctx (Const ("List.rev",typi --> typi) $ Free (fst pi,typi))
11.97 val perm_pi_simp = dynamic_thms ctx "perm_pi_simp"
11.98 in
11.99 - EVERY [tactic ("iffI applied",rtac iffI 1),
11.100 - tactic ("simplifies with orig_thm and perm_bool",
11.101 - asm_full_simp_tac (HOL_basic_ss addsimps [perm_bool,orig_thm]) 1),
11.102 + EVERY [tactic ("iffI applied",rtac iffI 1),
11.103 + tactic ("simplifies with orig_thm and perm_bool",
11.104 + asm_full_simp_tac (HOL_basic_ss addsimps [perm_bool,orig_thm]) 1),
11.105 tactic ("applies orig_thm instantiated with rev pi",
11.106 - dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm) 1),
11.107 + dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm) 1),
11.108 tactic ("getting rid of all remaining perms",
11.109 - full_simp_tac (HOL_basic_ss addsimps (perm_bool::perm_pi_simp)) 1)]
11.110 + full_simp_tac (HOL_basic_ss addsimps (perm_bool::perm_pi_simp)) 1)]
11.111 end;
11.112
11.113 fun get_derived_thm thy hyp concl orig_thm pi typi =
11.114 - let
11.115 + let
11.116 val lhs = (Const("Nominal.perm", typi --> HOLogic.boolT --> HOLogic.boolT) $ Var(pi,typi) $ hyp)
11.117 - val goal_term = Logic.unvarify (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,concl)))
11.118 - val _ = Display.print_cterm (cterm_of thy goal_term)
11.119 + val goal_term = Logic.unvarify (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,concl)))
11.120 + val _ = Display.print_cterm (cterm_of thy goal_term)
11.121 in
11.122 - Goal.prove_global thy [] [] goal_term (fn _ => (tactic_eqvt thy orig_thm pi typi))
11.123 + Goal.prove_global thy [] [] goal_term (fn _ => (tactic_eqvt thy orig_thm pi typi))
11.124 end
11.125
11.126 (* FIXME: something naughty here, but as long as there is no infrastructure to expose *)
11.127 (* the eqvt_thm_list to the user, we have to manually update the context and the *)
11.128 (* thm-list eqvt *)
11.129 fun update_context flag thms context =
11.130 - let
11.131 - val context' = fold (fn thm => Data.map (flag thm)) thms context
11.132 - in
11.133 + let
11.134 + val context' = fold (fn thm => Data.map (flag thm)) thms context
11.135 + in
11.136 Context.mapping (snd o PureThy.add_thmss [(("eqvts",(#eqvts (Data.get context'))),[])]) I context'
11.137 end;
11.138
11.139 -(* replaces every variable x in t with pi o x *)
11.140 +(* replaces every variable x in t with pi o x *)
11.141 fun apply_pi trm (pi,typi) =
11.142 - let
11.143 + let
11.144 fun only_vars t =
11.145 (case t of
11.146 Var (n,ty) => (Const ("Nominal.perm",typi --> ty --> ty) $ (Var (pi,typi)) $ (Var (n,ty)))
11.147 | _ => t)
11.148 - in
11.149 - map_aterms only_vars trm
11.150 + in
11.151 + map_aterms only_vars trm
11.152 end;
11.153
11.154 (* returns *the* pi which is in front of all variables, provided there *)
11.155 @@ -132,69 +132,69 @@
11.156 fun get_pi t thy =
11.157 let fun get_pi_aux s =
11.158 (case s of
11.159 - (Const ("Nominal.perm",typrm) $
11.160 - (Var (pi,typi as Type("List.list",[Type ("*",[Type (tyatm,[]),_])]))) $
11.161 - (Var (n,ty))) =>
11.162 + (Const ("Nominal.perm",typrm) $
11.163 + (Var (pi,typi as Type("List.list",[Type ("*",[Type (tyatm,[]),_])]))) $
11.164 + (Var (n,ty))) =>
11.165 let
11.166 (* FIXME: this should be an operation the library *)
11.167 - val class_name = (NameSpace.map_base (fn s => "pt_"^s) tyatm)
11.168 - in
11.169 - if (Type.of_sort (Sign.tsig_of thy) (ty,[class_name]))
11.170 - then [(pi,typi)]
11.171 - else raise
11.172 - EQVT_FORM ("Could not find any permutation or an argument is not an instance of "^class_name)
11.173 - end
11.174 + val class_name = (NameSpace.map_base (fn s => "pt_"^s) tyatm)
11.175 + in
11.176 + if (Type.of_sort (Sign.tsig_of thy) (ty,[class_name]))
11.177 + then [(pi,typi)]
11.178 + else raise
11.179 + EQVT_FORM ("Could not find any permutation or an argument is not an instance of "^class_name)
11.180 + end
11.181 | Abs (_,_,t1) => get_pi_aux t1
11.182 | (t1 $ t2) => get_pi_aux t1 @ get_pi_aux t2
11.183 - | _ => [])
11.184 - in
11.185 + | _ => [])
11.186 + in
11.187 (* collect first all pi's in front of variables in t and then use distinct *)
11.188 (* to ensure that all pi's must have been the same, i.e. distinct returns *)
11.189 (* a singleton-list *)
11.190 - (case (distinct (op =) (get_pi_aux t)) of
11.191 + (case (distinct (op =) (get_pi_aux t)) of
11.192 [(pi,typi)] => (pi,typi)
11.193 | _ => raise EQVT_FORM "All permutation should be the same")
11.194 end;
11.195
11.196 (* Either adds a theorem (orig_thm) to or deletes one from the equivaraince *)
11.197 (* lemma list depending on flag. To be added the lemma has to satisfy a *)
11.198 -(* certain form. *)
11.199 +(* certain form. *)
11.200 fun eqvt_add_del_aux flag orig_thm context =
11.201 - let
11.202 + let
11.203 val thy = Context.theory_of context
11.204 val thms_to_be_added = (case (prop_of orig_thm) of
11.205 - (* case: eqvt-lemma is of the implicational form *)
11.206 + (* case: eqvt-lemma is of the implicational form *)
11.207 (Const("==>", _) $ (Const ("Trueprop",_) $ hyp) $ (Const ("Trueprop",_) $ concl)) =>
11.208 - let
11.209 + let
11.210 val (pi,typi) = get_pi concl thy
11.211 in
11.212 if (apply_pi hyp (pi,typi) = concl)
11.213 - then
11.214 + then
11.215 (warning ("equivariance lemma of the relational form");
11.216 [orig_thm, get_derived_thm thy hyp concl orig_thm pi typi])
11.217 else raise EQVT_FORM "Type Implication"
11.218 end
11.219 - (* case: eqvt-lemma is of the equational form *)
11.220 - | (Const ("Trueprop", _) $ (Const ("op =", _) $
11.221 + (* case: eqvt-lemma is of the equational form *)
11.222 + | (Const ("Trueprop", _) $ (Const ("op =", _) $
11.223 (Const ("Nominal.perm",typrm) $ Var (pi,typi) $ lhs) $ rhs)) =>
11.224 - (if (apply_pi lhs (pi,typi)) = rhs
11.225 + (if (apply_pi lhs (pi,typi)) = rhs
11.226 then [orig_thm]
11.227 else raise EQVT_FORM "Type Equality")
11.228 | _ => raise EQVT_FORM "Type unknown")
11.229 - in
11.230 + in
11.231 update_context flag thms_to_be_added context
11.232 end
11.233 - handle EQVT_FORM s =>
11.234 + handle EQVT_FORM s =>
11.235 error (string_of_thm orig_thm ^ " does not comply with the form of an equivariance lemma ("^s^").")
11.236
11.237 (* in cases of bij- and freshness, we just add the lemmas to the *)
11.238 -(* data-slot *)
11.239 +(* data-slot *)
11.240
11.241 -fun simple_add_del_aux record_access name flag th context =
11.242 - let
11.243 +fun simple_add_del_aux record_access name flag th context =
11.244 + let
11.245 val context' = Data.map (flag th) context
11.246 in
11.247 - Context.mapping (snd o PureThy.add_thmss [((name,(record_access (Data.get context'))),[])]) I context'
11.248 + Context.mapping (snd o PureThy.add_thmss [((name,(record_access (Data.get context'))),[])]) I context'
11.249 end
11.250
11.251 fun bij_add_del_aux f = simple_add_del_aux #bijs "bijs" f
11.252 @@ -205,21 +205,20 @@
11.253 fun fresh_map f th (r:Data.T) = {eqvts = #eqvts r, freshs = (f th (#freshs r)), bijs = #bijs r};
11.254 fun bij_map f th (r:Data.T) = {eqvts = #eqvts r, freshs = #freshs r, bijs = (f th (#bijs r))};
11.255
11.256 -val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.add_rule));
11.257 -val eqvt_del = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.del_rule));
11.258 -val eqvt_force_add = Thm.declaration_attribute (eqvt_force_add_del_aux (eqvt_map Drule.add_rule));
11.259 -val eqvt_force_del = Thm.declaration_attribute (eqvt_force_add_del_aux (eqvt_map Drule.del_rule));
11.260 +val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.add_rule));
11.261 +val eqvt_del = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.del_rule));
11.262 +val eqvt_force_add = Thm.declaration_attribute (eqvt_force_add_del_aux (eqvt_map Drule.add_rule));
11.263 +val eqvt_force_del = Thm.declaration_attribute (eqvt_force_add_del_aux (eqvt_map Drule.del_rule));
11.264
11.265 -val bij_add = Thm.declaration_attribute (bij_add_del_aux (bij_map Drule.add_rule));
11.266 +val bij_add = Thm.declaration_attribute (bij_add_del_aux (bij_map Drule.add_rule));
11.267 val bij_del = Thm.declaration_attribute (bij_add_del_aux (bij_map Drule.del_rule));
11.268 -val fresh_add = Thm.declaration_attribute (fresh_add_del_aux (fresh_map Drule.add_rule));
11.269 +val fresh_add = Thm.declaration_attribute (fresh_add_del_aux (fresh_map Drule.add_rule));
11.270 val fresh_del = Thm.declaration_attribute (fresh_add_del_aux (fresh_map Drule.del_rule));
11.271
11.272
11.273
11.274 val setup =
11.275 - Data.init #>
11.276 - Attrib.add_attributes
11.277 + Attrib.add_attributes
11.278 [("eqvt", Attrib.add_del_args eqvt_add eqvt_del, "equivariance theorem declaration"),
11.279 ("eqvt_force", Attrib.add_del_args eqvt_force_add eqvt_force_del,
11.280 "equivariance theorem declaration (without checking the form of the lemma)"),
11.281 @@ -227,11 +226,3 @@
11.282 ("bij", Attrib.add_del_args bij_add bij_del, "bijection theorem declaration")];
11.283
11.284 end;
11.285 -
11.286 -(* Thm.declaration_attribute has type (thm -> Context.generic -> Context.generic) -> attribute *)
11.287 -
11.288 -(* Drule.add_rule has type thm -> thm list -> thm list *)
11.289 -
11.290 -(* Data.map has type thm list -> thm list -> Context.generic -> Context.generic *)
11.291 -
11.292 -(* add_del_args is of type attribute -> attribute -> src -> attribute *)
11.293 \ No newline at end of file
12.1 --- a/src/HOL/Predicate.thy Sun May 06 21:50:17 2007 +0200
12.2 +++ b/src/HOL/Predicate.thy Mon May 07 00:49:59 2007 +0200
12.3 @@ -152,14 +152,12 @@
12.4 val rules2 = [split_set, mk_meta_eq mem_Collect_eq, mem_Collect2_eq];
12.5
12.6 structure PredSetConvData = GenericDataFun
12.7 -(struct
12.8 - val name = "HOL/pred_set_conv";
12.9 +(
12.10 type T = thm list;
12.11 val empty = [];
12.12 val extend = I;
12.13 fun merge _ = Drule.merge_rules;
12.14 - fun print _ _ = ()
12.15 -end)
12.16 +);
12.17
12.18 fun mk_attr ths1 ths2 f = Attrib.syntax (Attrib.thms >> (fn ths =>
12.19 Thm.rule_attribute (fn ctxt => rew ths1 (map (f o Simpdata.mk_eq)
12.20 @@ -170,7 +168,7 @@
12.21
12.22 in
12.23
12.24 -val _ = ML_Context.>> (PredSetConvData.init #>
12.25 +val _ = ML_Context.>> (
12.26 Attrib.add_attributes
12.27 [("pred_set_conv", pred_set_conv_att,
12.28 "declare rules for converting between predicate and set notation"),
13.1 --- a/src/HOL/Tools/datatype_hooks.ML Sun May 06 21:50:17 2007 +0200
13.2 +++ b/src/HOL/Tools/datatype_hooks.ML Mon May 07 00:49:59 2007 +0200
13.3 @@ -7,49 +7,29 @@
13.4
13.5 signature DATATYPE_HOOKS =
13.6 sig
13.7 - type hook = string list -> theory -> theory;
13.8 - val add: hook -> theory -> theory;
13.9 - val all: hook;
13.10 - val setup: theory -> theory;
13.11 + type hook = string list -> theory -> theory
13.12 + val add: hook -> theory -> theory
13.13 + val all: hook
13.14 end;
13.15
13.16 structure DatatypeHooks : DATATYPE_HOOKS =
13.17 struct
13.18
13.19 -
13.20 -(* theory data *)
13.21 -
13.22 type hook = string list -> theory -> theory;
13.23 -datatype T = T of (serial * hook) list;
13.24 -
13.25 -fun map_T f (T hooks) = T (f hooks);
13.26 -fun merge_T pp (T hooks1, T hooks2) =
13.27 - T (AList.merge (op =) (K true) (hooks1, hooks2));
13.28
13.29 structure DatatypeHooksData = TheoryDataFun
13.30 -(struct
13.31 - val name = "HOL/datatype_hooks";
13.32 - type T = T;
13.33 - val empty = T [];
13.34 +(
13.35 + type T = (serial * hook) list;
13.36 + val empty = [];
13.37 val copy = I;
13.38 val extend = I;
13.39 - val merge = merge_T;
13.40 - fun print _ _ = ();
13.41 -end);
13.42 -
13.43 -
13.44 -(* interface *)
13.45 + fun merge _ hooks : T = AList.merge (op =) (K true) hooks;
13.46 +);
13.47
13.48 fun add hook =
13.49 - DatatypeHooksData.map (map_T (cons (serial (), hook)));
13.50 + DatatypeHooksData.map (cons (serial (), hook));
13.51
13.52 fun all dtcos thy =
13.53 - fold (fn (_, f) => f dtcos) ((fn T hooks => hooks) (DatatypeHooksData.get thy)) thy;
13.54 -
13.55 -
13.56 -(* theory setup *)
13.57 -
13.58 -val setup = DatatypeHooksData.init;
13.59 + fold (fn (_, f) => f dtcos) (DatatypeHooksData.get thy) thy;
13.60
13.61 end;
13.62 -
14.1 --- a/src/HOL/Tools/datatype_package.ML Sun May 06 21:50:17 2007 +0200
14.2 +++ b/src/HOL/Tools/datatype_package.ML Mon May 07 00:49:59 2007 +0200
14.3 @@ -85,11 +85,10 @@
14.4 val quiet_mode = quiet_mode;
14.5
14.6
14.7 -(* data kind 'HOL/datatypes' *)
14.8 +(* theory data *)
14.9
14.10 structure DatatypesData = TheoryDataFun
14.11 -(struct
14.12 - val name = "HOL/datatypes";
14.13 +(
14.14 type T =
14.15 {types: datatype_info Symtab.table,
14.16 constrs: datatype_info Symtab.table,
14.17 @@ -105,15 +104,14 @@
14.18 {types = Symtab.merge (K true) (types1, types2),
14.19 constrs = Symtab.merge (K true) (constrs1, constrs2),
14.20 cases = Symtab.merge (K true) (cases1, cases2)};
14.21 -
14.22 - fun print sg ({types, ...} : T) =
14.23 - Pretty.writeln (Pretty.strs ("datatypes:" ::
14.24 - map #1 (NameSpace.extern_table (Sign.type_space sg, types))));
14.25 -end);
14.26 +);
14.27
14.28 val get_datatypes = #types o DatatypesData.get;
14.29 val map_datatypes = DatatypesData.map;
14.30 -val print_datatypes = DatatypesData.print;
14.31 +
14.32 +fun print_datatypes thy =
14.33 + Pretty.writeln (Pretty.strs ("datatypes:" ::
14.34 + map #1 (NameSpace.extern_table (Sign.type_space thy, get_datatypes thy))));
14.35
14.36
14.37 (** theory information about datatypes **)
14.38 @@ -933,7 +931,7 @@
14.39 (* setup theory *)
14.40
14.41 val setup =
14.42 - DatatypesData.init #> Method.add_methods tactic_emulations #> simproc_setup #> trfun_setup;
14.43 + Method.add_methods tactic_emulations #> simproc_setup #> trfun_setup;
14.44
14.45
14.46 (* outer syntax *)
15.1 --- a/src/HOL/Tools/function_package/fundef_common.ML Sun May 06 21:50:17 2007 +0200
15.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML Mon May 07 00:49:59 2007 +0200
15.3 @@ -78,30 +78,24 @@
15.4 end
15.5
15.6 structure FundefData = GenericDataFun
15.7 -(struct
15.8 - val name = "HOL/function_def/data";
15.9 - type T = (term * fundef_context_data) NetRules.T
15.10 -
15.11 +(
15.12 + type T = (term * fundef_context_data) NetRules.T;
15.13 val empty = NetRules.init
15.14 (op aconv o pairself fst : (term * fundef_context_data) * (term * fundef_context_data) -> bool)
15.15 fst;
15.16 val copy = I;
15.17 val extend = I;
15.18 fun merge _ (tab1, tab2) = NetRules.merge (tab1, tab2)
15.19 -
15.20 - fun print _ _ = ();
15.21 -end);
15.22 +);
15.23
15.24
15.25 structure FundefCongs = GenericDataFun
15.26 -(struct
15.27 - val name = "HOL/function_def/congs"
15.28 - type T = thm list
15.29 - val empty = []
15.30 - val extend = I
15.31 - fun merge _ = Drule.merge_rules
15.32 - fun print _ _ = ()
15.33 -end);
15.34 +(
15.35 + type T = thm list
15.36 + val empty = []
15.37 + val extend = I
15.38 + fun merge _ = Drule.merge_rules
15.39 +);
15.40
15.41
15.42 (* Generally useful?? *)
15.43 @@ -143,14 +137,12 @@
15.44
15.45
15.46 structure TerminationRule = GenericDataFun
15.47 -(struct
15.48 - val name = "HOL/function_def/termination"
15.49 - type T = thm list
15.50 - val empty = []
15.51 - val extend = I
15.52 - fun merge _ = Drule.merge_rules
15.53 - fun print _ _ = ()
15.54 -end);
15.55 +(
15.56 + type T = thm list
15.57 + val empty = []
15.58 + val extend = I
15.59 + fun merge _ = Drule.merge_rules
15.60 +);
15.61
15.62 val get_termination_rules = TerminationRule.get
15.63 val store_termination_rule = TerminationRule.map o cons
16.1 --- a/src/HOL/Tools/function_package/fundef_package.ML Sun May 06 21:50:17 2007 +0200
16.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML Mon May 07 00:49:59 2007 +0200
16.3 @@ -208,13 +208,11 @@
16.4 (* setup *)
16.5
16.6 val setup =
16.7 - FundefData.init
16.8 - #> FundefCongs.init
16.9 - #> TerminationRule.init
16.10 - #> Attrib.add_attributes
16.11 - [("fundef_cong", Attrib.add_del_args cong_add cong_del, "declaration of congruence rule for function definitions")]
16.12 - #> setup_case_cong_hook
16.13 - #> FundefRelation.setup
16.14 + Attrib.add_attributes
16.15 + [("fundef_cong", Attrib.add_del_args cong_add cong_del,
16.16 + "declaration of congruence rule for function definitions")]
16.17 + #> setup_case_cong_hook
16.18 + #> FundefRelation.setup
16.19
16.20 val get_congs = FundefCommon.get_fundef_congs o Context.Theory
16.21
17.1 --- a/src/HOL/Tools/inductive_codegen.ML Sun May 06 21:50:17 2007 +0200
17.2 +++ b/src/HOL/Tools/inductive_codegen.ML Mon May 07 00:49:59 2007 +0200
17.3 @@ -22,8 +22,7 @@
17.4 Symtab.join (fn _ => AList.merge (Thm.eq_thm_prop) (K true)) tabs;
17.5
17.6 structure CodegenData = TheoryDataFun
17.7 -(struct
17.8 - val name = "HOL/inductive_codegen";
17.9 +(
17.10 type T =
17.11 {intros : (thm * (string * int)) list Symtab.table,
17.12 graph : unit Graph.T,
17.13 @@ -37,8 +36,7 @@
17.14 {intros = merge_rules (intros1, intros2),
17.15 graph = Graph.merge (K true) (graph1, graph2),
17.16 eqns = merge_rules (eqns1, eqns2)};
17.17 - fun print _ _ = ();
17.18 -end);
17.19 +);
17.20
17.21
17.22 fun warn thm = warning ("InductiveCodegen: Not a proper clause:\n" ^
17.23 @@ -653,7 +651,6 @@
17.24
17.25 val setup =
17.26 add_codegen "inductive" inductive_codegen #>
17.27 - CodegenData.init #>
17.28 add_attribute "ind" (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) --
17.29 Scan.option (Args.$$$ "params" |-- Args.colon |-- Args.nat) >> uncurry add);
17.30
18.1 --- a/src/HOL/Tools/inductive_package.ML Sun May 06 21:50:17 2007 +0200
18.2 +++ b/src/HOL/Tools/inductive_package.ML Mon May 07 00:49:59 2007 +0200
18.3 @@ -86,7 +86,7 @@
18.4
18.5
18.6
18.7 -(** theory data **)
18.8 +(** context data **)
18.9
18.10 type inductive_result =
18.11 {preds: term list, defs: thm list, elims: thm list, raw_induct: thm,
18.12 @@ -106,28 +106,25 @@
18.13 {names: string list, coind: bool} * inductive_result;
18.14
18.15 structure InductiveData = GenericDataFun
18.16 -(struct
18.17 - val name = "HOL/inductive";
18.18 +(
18.19 type T = inductive_info Symtab.table * thm list;
18.20 -
18.21 val empty = (Symtab.empty, []);
18.22 val extend = I;
18.23 fun merge _ ((tab1, monos1), (tab2, monos2)) =
18.24 (Symtab.merge (K true) (tab1, tab2), Drule.merge_rules (monos1, monos2));
18.25 -
18.26 - fun print context (tab, monos) =
18.27 - let
18.28 - val ctxt = Context.proof_of context;
18.29 - val space = Consts.space_of (ProofContext.consts_of ctxt);
18.30 - in
18.31 - [Pretty.strs ("(co)inductives:" :: map #1 (NameSpace.extern_table (space, tab))),
18.32 - Pretty.big_list "monotonicity rules:" (map (ProofContext.pretty_thm ctxt) monos)]
18.33 - |> Pretty.chunks |> Pretty.writeln
18.34 - end;
18.35 -end);
18.36 +);
18.37
18.38 val get_inductives = InductiveData.get o Context.Proof;
18.39 -val print_inductives = InductiveData.print o Context.Proof;
18.40 +
18.41 +fun print_inductives ctxt =
18.42 + let
18.43 + val (tab, monos) = get_inductives ctxt;
18.44 + val space = Consts.space_of (ProofContext.consts_of ctxt);
18.45 + in
18.46 + [Pretty.strs ("(co)inductives:" :: map #1 (NameSpace.extern_table (space, tab))),
18.47 + Pretty.big_list "monotonicity rules:" (map (ProofContext.pretty_thm ctxt) monos)]
18.48 + |> Pretty.chunks |> Pretty.writeln
18.49 + end;
18.50
18.51
18.52 (* get and put data *)
18.53 @@ -156,7 +153,7 @@
18.54 (_ $ (_ $ (Const ("Not", _) $ _) $ _)) => []
18.55 | _ => [thm' RS (thm' RS eq_to_mono2)]);
18.56 fun dest_less_concl thm = dest_less_concl (thm RS le_funD)
18.57 - handle THM _ => thm RS le_boolD
18.58 + handle THM _ => thm RS le_boolD
18.59 in
18.60 case concl of
18.61 Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq)
18.62 @@ -892,7 +889,6 @@
18.63 (* setup theory *)
18.64
18.65 val setup =
18.66 - InductiveData.init #>
18.67 Method.add_methods [("ind_cases2", ind_cases, (* FIXME "ind_cases" (?) *)
18.68 "dynamic case analysis on predicates")] #>
18.69 Attrib.add_attributes [("mono2", Attrib.add_del_args mono_add mono_del, (* FIXME "mono" *)
19.1 --- a/src/HOL/Tools/old_inductive_package.ML Sun May 06 21:50:17 2007 +0200
19.2 +++ b/src/HOL/Tools/old_inductive_package.ML Mon May 07 00:49:59 2007 +0200
19.3 @@ -37,7 +37,6 @@
19.4 {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
19.5 intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}) option
19.6 val the_mk_cases: theory -> string -> string -> thm
19.7 - val print_inductives: theory -> unit
19.8 val mono_add: attribute
19.9 val mono_del: attribute
19.10 val get_monos: theory -> thm list
19.11 @@ -88,27 +87,14 @@
19.12 induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm};
19.13
19.14 structure InductiveData = TheoryDataFun
19.15 -(struct
19.16 - val name = "HOL/inductive";
19.17 +(
19.18 type T = inductive_info Symtab.table * thm list;
19.19 -
19.20 val empty = (Symtab.empty, []);
19.21 val copy = I;
19.22 val extend = I;
19.23 fun merge _ ((tab1, monos1), (tab2, monos2)) =
19.24 (Symtab.merge (K true) (tab1, tab2), Drule.merge_rules (monos1, monos2));
19.25 -
19.26 - fun print thy (tab, monos) =
19.27 - [Pretty.strs ("(co)inductives:" ::
19.28 - map #1 (NameSpace.extern_table (Sign.const_space thy, tab))),
19.29 - Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_sg thy) monos)]
19.30 - |> Pretty.chunks |> Pretty.writeln;
19.31 -end);
19.32 -
19.33 -val print_inductives = InductiveData.print;
19.34 -
19.35 -
19.36 -(* get and put data *)
19.37 +);
19.38
19.39 val get_inductive = Symtab.lookup o #1 o InductiveData.get;
19.40
19.41 @@ -871,7 +857,6 @@
19.42 (* setup theory *)
19.43
19.44 val setup =
19.45 - InductiveData.init #>
19.46 Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args,
19.47 "dynamic case analysis on sets")] #>
19.48 Attrib.add_attributes [("mono", Attrib.add_del_args mono_add mono_del,
20.1 --- a/src/HOL/Tools/recdef_package.ML Sun May 06 21:50:17 2007 +0200
20.2 +++ b/src/HOL/Tools/recdef_package.ML Mon May 07 00:49:59 2007 +0200
20.3 @@ -8,7 +8,6 @@
20.4 signature RECDEF_PACKAGE =
20.5 sig
20.6 val quiet_mode: bool ref
20.7 - val print_recdefs: theory -> unit
20.8 val get_recdef: theory -> string
20.9 -> {simps: thm list, rules: thm list list, induct: thm, tcs: term list} option
20.10 val get_hints: Proof.context -> {simps: thm list, congs: (string * thm) list, wfs: thm list}
20.11 @@ -97,10 +96,8 @@
20.12 type recdef_info = {simps: thm list, rules: thm list list, induct: thm, tcs: term list};
20.13
20.14 structure GlobalRecdefData = TheoryDataFun
20.15 -(struct
20.16 - val name = "HOL/recdef";
20.17 +(
20.18 type T = recdef_info Symtab.table * hints;
20.19 -
20.20 val empty = (Symtab.empty, mk_hints ([], [], [])): T;
20.21 val copy = I;
20.22 val extend = I;
20.23 @@ -111,14 +108,7 @@
20.24 mk_hints (Drule.merge_rules (simps1, simps2),
20.25 AList.merge (op =) Thm.eq_thm (congs1, congs2),
20.26 Drule.merge_rules (wfs1, wfs2)));
20.27 -
20.28 - fun print thy (tab, hints) =
20.29 - (Pretty.strs ("recdefs:" :: map #1 (NameSpace.extern_table (Sign.const_space thy, tab))) ::
20.30 - pretty_hints hints) |> Pretty.chunks |> Pretty.writeln;
20.31 -end);
20.32 -
20.33 -val print_recdefs = GlobalRecdefData.print;
20.34 -
20.35 +);
20.36
20.37 val get_recdef = Symtab.lookup o #1 o GlobalRecdefData.get;
20.38
20.39 @@ -135,12 +125,10 @@
20.40 (* proof data *)
20.41
20.42 structure LocalRecdefData = ProofDataFun
20.43 -(struct
20.44 - val name = "HOL/recdef";
20.45 +(
20.46 type T = hints;
20.47 val init = get_global_hints;
20.48 - fun print _ hints = pretty_hints hints |> Pretty.chunks |> Pretty.writeln;
20.49 -end);
20.50 +);
20.51
20.52 val get_hints = LocalRecdefData.get;
20.53 fun map_hints f = Context.mapping (GlobalRecdefData.map (apsnd f)) (LocalRecdefData.map f);
20.54 @@ -297,8 +285,6 @@
20.55 (* setup theory *)
20.56
20.57 val setup =
20.58 - GlobalRecdefData.init #>
20.59 - LocalRecdefData.init #>
20.60 Attrib.add_attributes
20.61 [(recdef_simpN, Attrib.add_del_args simp_add simp_del, "declaration of recdef simp rule"),
20.62 (recdef_congN, Attrib.add_del_args cong_add cong_del, "declaration of recdef cong rule"),
21.1 --- a/src/HOL/Tools/recfun_codegen.ML Sun May 06 21:50:17 2007 +0200
21.2 +++ b/src/HOL/Tools/recfun_codegen.ML Mon May 07 00:49:59 2007 +0200
21.3 @@ -18,15 +18,13 @@
21.4 open Codegen;
21.5
21.6 structure RecCodegenData = TheoryDataFun
21.7 -(struct
21.8 - val name = "HOL/recfun_codegen";
21.9 +(
21.10 type T = (thm * string option) list Symtab.table;
21.11 val empty = Symtab.empty;
21.12 val copy = I;
21.13 val extend = I;
21.14 fun merge _ = Symtab.merge_list (Thm.eq_thm_prop o pairself fst);
21.15 - fun print _ _ = ();
21.16 -end);
21.17 +);
21.18
21.19
21.20 val dest_eqn = HOLogic.dest_eq o HOLogic.dest_Trueprop;
21.21 @@ -172,7 +170,6 @@
21.22
21.23
21.24 val setup =
21.25 - RecCodegenData.init #>
21.26 add_codegen "recfun" recfun_codegen #>
21.27 add_attribute ""
21.28 (Args.del |-- Scan.succeed del
22.1 --- a/src/HOL/Tools/record_package.ML Sun May 06 21:50:17 2007 +0200
22.2 +++ b/src/HOL/Tools/record_package.ML Mon May 07 00:49:59 2007 +0200
22.3 @@ -243,7 +243,8 @@
22.4 fun make_parent_info name fields extension induct =
22.5 {name = name, fields = fields, extension = extension, induct = induct}: parent_info;
22.6
22.7 -(* data kind 'HOL/record' *)
22.8 +
22.9 +(* theory data *)
22.10
22.11 type record_data =
22.12 {records: record_info Symtab.table,
22.13 @@ -266,10 +267,8 @@
22.14 extfields = extfields, fieldext = fieldext }: record_data;
22.15
22.16 structure RecordsData = TheoryDataFun
22.17 -(struct
22.18 - val name = "HOL/record";
22.19 +(
22.20 type T = record_data;
22.21 -
22.22 val empty =
22.23 make_record_data Symtab.empty
22.24 {selectors = Symtab.empty, updates = Symtab.empty, simpset = HOL_basic_ss}
22.25 @@ -308,27 +307,26 @@
22.26 (splits1, splits2))
22.27 (Symtab.merge (K true) (extfields1,extfields2))
22.28 (Symtab.merge (K true) (fieldext1,fieldext2));
22.29 +);
22.30
22.31 - fun print thy ({records = recs, ...}: record_data) =
22.32 - let
22.33 - val prt_typ = Sign.pretty_typ thy;
22.34 +fun print_records thy =
22.35 + let
22.36 + val {records = recs, ...} = RecordsData.get thy;
22.37 + val prt_typ = Sign.pretty_typ thy;
22.38
22.39 - fun pretty_parent NONE = []
22.40 - | pretty_parent (SOME (Ts, name)) =
22.41 - [Pretty.block [prt_typ (Type (name, Ts)), Pretty.str " +"]];
22.42 + fun pretty_parent NONE = []
22.43 + | pretty_parent (SOME (Ts, name)) =
22.44 + [Pretty.block [prt_typ (Type (name, Ts)), Pretty.str " +"]];
22.45
22.46 - fun pretty_field (c, T) = Pretty.block
22.47 - [Pretty.str (Sign.extern_const thy c), Pretty.str " ::",
22.48 - Pretty.brk 1, Pretty.quote (prt_typ T)];
22.49 + fun pretty_field (c, T) = Pretty.block
22.50 + [Pretty.str (Sign.extern_const thy c), Pretty.str " ::",
22.51 + Pretty.brk 1, Pretty.quote (prt_typ T)];
22.52
22.53 - fun pretty_record (name, {args, parent, fields, ...}: record_info) =
22.54 - Pretty.block (Pretty.fbreaks (Pretty.block
22.55 - [prt_typ (Type (name, map TFree args)), Pretty.str " = "] ::
22.56 - pretty_parent parent @ map pretty_field fields));
22.57 - in map pretty_record (Symtab.dest recs) |> Pretty.chunks |> Pretty.writeln end;
22.58 -end);
22.59 -
22.60 -val print_records = RecordsData.print;
22.61 + fun pretty_record (name, {args, parent, fields, ...}: record_info) =
22.62 + Pretty.block (Pretty.fbreaks (Pretty.block
22.63 + [prt_typ (Type (name, map TFree args)), Pretty.str " = "] ::
22.64 + pretty_parent parent @ map pretty_field fields));
22.65 + in map pretty_record (Symtab.dest recs) |> Pretty.chunks |> Pretty.writeln end;
22.66
22.67
22.68 (* access 'records' *)
22.69 @@ -343,6 +341,7 @@
22.70 sel_upd equalities extinjects extsplit splits extfields fieldext;
22.71 in RecordsData.put data thy end;
22.72
22.73 +
22.74 (* access 'sel_upd' *)
22.75
22.76 val get_sel_upd = #sel_upd o RecordsData.get;
22.77 @@ -365,6 +364,7 @@
22.78 equalities extinjects extsplit splits extfields fieldext;
22.79 in RecordsData.put data thy end;
22.80
22.81 +
22.82 (* access 'equalities' *)
22.83
22.84 fun add_record_equalities name thm thy =
22.85 @@ -378,18 +378,21 @@
22.86
22.87 val get_equalities =Symtab.lookup o #equalities o RecordsData.get;
22.88
22.89 +
22.90 (* access 'extinjects' *)
22.91
22.92 fun add_extinjects thm thy =
22.93 let
22.94 val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} =
22.95 RecordsData.get thy;
22.96 - val data = make_record_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects) extsplit
22.97 - splits extfields fieldext;
22.98 + val data =
22.99 + make_record_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects) extsplit
22.100 + splits extfields fieldext;
22.101 in RecordsData.put data thy end;
22.102
22.103 val get_extinjects = rev o #extinjects o RecordsData.get;
22.104
22.105 +
22.106 (* access 'extsplit' *)
22.107
22.108 fun add_extsplit name thm thy =
22.109 @@ -2263,7 +2266,6 @@
22.110 (* setup theory *)
22.111
22.112 val setup =
22.113 - RecordsData.init #>
22.114 Theory.add_trfuns ([], parse_translation, [], []) #>
22.115 Theory.add_advanced_trfuns ([], adv_parse_translation, [], []) #>
22.116 (fn thy => (Simplifier.change_simpset_of thy
23.1 --- a/src/HOL/Tools/refute.ML Sun May 06 21:50:17 2007 +0200
23.2 +++ b/src/HOL/Tools/refute.ML Mon May 07 00:49:59 2007 +0200
23.3 @@ -186,9 +186,8 @@
23.4 };
23.5
23.6
23.7 - structure RefuteDataArgs =
23.8 - struct
23.9 - val name = "HOL/refute";
23.10 + structure RefuteData = TheoryDataFun
23.11 + (
23.12 type T =
23.13 {interpreters: (string * (theory -> model -> arguments -> Term.term ->
23.14 (interpretation * model * arguments) option)) list,
23.15 @@ -204,15 +203,7 @@
23.16 {interpreters = AList.merge (op =) (K true) (in1, in2),
23.17 printers = AList.merge (op =) (K true) (pr1, pr2),
23.18 parameters = Symtab.merge (op=) (pa1, pa2)};
23.19 - fun print sg {interpreters, printers, parameters} =
23.20 - Pretty.writeln (Pretty.chunks
23.21 - [Pretty.strs ("default parameters:" :: List.concat (map
23.22 - (fn (name, value) => [name, "=", value]) (Symtab.dest parameters))),
23.23 - Pretty.strs ("interpreters:" :: map fst interpreters),
23.24 - Pretty.strs ("printers:" :: map fst printers)]);
23.25 - end;
23.26 -
23.27 - structure RefuteData = TheoryDataFun(RefuteDataArgs);
23.28 + );
23.29
23.30
23.31 (* ------------------------------------------------------------------------- *)
23.32 @@ -3210,7 +3201,6 @@
23.33 (* (theory -> theory) list *)
23.34
23.35 val setup =
23.36 - RefuteData.init #>
23.37 add_interpreter "stlc" stlc_interpreter #>
23.38 add_interpreter "Pure" Pure_interpreter #>
23.39 add_interpreter "HOLogic" HOLogic_interpreter #>
24.1 --- a/src/HOL/Tools/res_atpset.ML Sun May 06 21:50:17 2007 +0200
24.2 +++ b/src/HOL/Tools/res_atpset.ML Mon May 07 00:49:59 2007 +0200
24.3 @@ -18,24 +18,22 @@
24.4
24.5 structure Data = GenericDataFun
24.6 (
24.7 - val name = "HOL/atpset";
24.8 type T = thm list;
24.9 val empty = [];
24.10 val extend = I;
24.11 fun merge _ = Drule.merge_rules;
24.12 - fun print context rules =
24.13 - Pretty.writeln (Pretty.big_list "ATP rules:"
24.14 - (map (ProofContext.pretty_thm (Context.proof_of context)) rules));
24.15 );
24.16
24.17 -val print_atpset = Data.print o Context.Proof;
24.18 val get_atpset = Data.get o Context.Proof;
24.19
24.20 +fun print_atpset ctxt =
24.21 + Pretty.writeln (Pretty.big_list "ATP rules:"
24.22 + (map (ProofContext.pretty_thm ctxt) (get_atpset ctxt)));
24.23 +
24.24 val atp_add = Thm.declaration_attribute (Data.map o Drule.add_rule);
24.25 val atp_del = Thm.declaration_attribute (Data.map o Drule.del_rule);
24.26
24.27 val setup =
24.28 - Data.init #>
24.29 Attrib.add_attributes [("atp", Attrib.add_del_args atp_add atp_del, "declaration of ATP rules")];
24.30
24.31 end;
25.1 --- a/src/HOL/Tools/res_axioms.ML Sun May 06 21:50:17 2007 +0200
25.2 +++ b/src/HOL/Tools/res_axioms.ML Mon May 07 00:49:59 2007 +0200
25.3 @@ -481,15 +481,13 @@
25.4 (SOME (to_nnf th, fake_name th) handle THM _ => NONE);
25.5
25.6 structure ThmCache = TheoryDataFun
25.7 -(struct
25.8 - val name = "ATP/thm_cache";
25.9 +(
25.10 type T = (thm list) Thmtab.table ref;
25.11 val empty : T = ref Thmtab.empty;
25.12 fun copy (ref tab) : T = ref tab;
25.13 val extend = copy;
25.14 fun merge _ (ref tab1, ref tab2) : T = ref (Thmtab.merge (K true) (tab1, tab2));
25.15 - fun print _ _ = ();
25.16 -end);
25.17 +);
25.18
25.19 (*The cache prevents repeated clausification of a theorem, and also repeated declaration of
25.20 Skolem functions. The global one holds theorems proved prior to this point. Theory data
26.1 --- a/src/HOL/Tools/typecopy_package.ML Sun May 06 21:50:17 2007 +0200
26.2 +++ b/src/HOL/Tools/typecopy_package.ML Mon May 07 00:49:59 2007 +0200
26.3 @@ -23,7 +23,7 @@
26.4 val add_hook: hook -> theory -> theory
26.5 val get_spec: theory -> string -> (string * sort) list * (string * typ list) list
26.6 val get_eq: theory -> string -> thm
26.7 - val print: theory -> unit
26.8 + val print_typecopies: theory -> unit
26.9 val setup: theory -> theory
26.10 end;
26.11
26.12 @@ -44,33 +44,30 @@
26.13 type hook = string * info -> theory -> theory;
26.14
26.15 structure TypecopyData = TheoryDataFun
26.16 -(struct
26.17 - val name = "HOL/typecopy_package";
26.18 +(
26.19 type T = info Symtab.table * (serial * hook) list;
26.20 val empty = (Symtab.empty, []);
26.21 val copy = I;
26.22 val extend = I;
26.23 fun merge _ ((tab1, hooks1), (tab2, hooks2) : T) =
26.24 (Symtab.merge (K true) (tab1, tab2), AList.merge (op =) (K true) (hooks1, hooks2));
26.25 - fun print thy (tab, _) =
26.26 - let
26.27 - fun mk (tyco, { vs, constr, typ, proj = (proj, _), ... } : info) =
26.28 - (Pretty.block o Pretty.breaks) [
26.29 - Sign.pretty_typ thy (Type (tyco, map TFree vs)),
26.30 - Pretty.str "=",
26.31 - (Pretty.str o Sign.extern_const thy) constr,
26.32 - Sign.pretty_typ thy typ,
26.33 - Pretty.block [Pretty.str "(", (Pretty.str o Sign.extern_const thy) proj, Pretty.str ")"]
26.34 - ];
26.35 +);
26.36 +
26.37 +fun print_typecopies thy =
26.38 + let
26.39 + val (tab, _) = TypecopyData.get thy;
26.40 + fun mk (tyco, { vs, constr, typ, proj = (proj, _), ... } : info) =
26.41 + (Pretty.block o Pretty.breaks) [
26.42 + Sign.pretty_typ thy (Type (tyco, map TFree vs)),
26.43 + Pretty.str "=",
26.44 + (Pretty.str o Sign.extern_const thy) constr,
26.45 + Sign.pretty_typ thy typ,
26.46 + Pretty.block [Pretty.str "(", (Pretty.str o Sign.extern_const thy) proj, Pretty.str ")"]];
26.47 in
26.48 - (Pretty.writeln o Pretty.block o Pretty.fbreaks) (
26.49 - Pretty.str "type copies:"
26.50 - :: map mk (Symtab.dest tab)
26.51 - )
26.52 + (Pretty.writeln o Pretty.block o Pretty.fbreaks)
26.53 + (Pretty.str "type copies:" :: map mk (Symtab.dest tab))
26.54 end;
26.55 -end);
26.56
26.57 -val print = TypecopyData.print;
26.58 val get_typecopies = Symtab.keys o fst o TypecopyData.get;
26.59 val get_typecopy_info = Symtab.lookup o fst o TypecopyData.get;
26.60
26.61 @@ -128,7 +125,7 @@
26.62
26.63 val add_typecopy = gen_add_typecopy Sign.certify_typ;
26.64
26.65 -end; (*local*)
26.66 +end;
26.67
26.68
26.69 (* equality function equation and datatype specification *)
26.70 @@ -147,8 +144,6 @@
26.71 fun add_project (_ , {proj_def, ...} : info) =
26.72 CodegenData.add_func true proj_def;
26.73
26.74 -val setup =
26.75 - TypecopyData.init
26.76 - #> add_hook add_project;
26.77 +val setup = add_hook add_project;
26.78
26.79 -end; (*struct*)
26.80 +end;
27.1 --- a/src/HOL/Tools/typedef_package.ML Sun May 06 21:50:17 2007 +0200
27.2 +++ b/src/HOL/Tools/typedef_package.ML Mon May 07 00:49:59 2007 +0200
27.3 @@ -24,7 +24,6 @@
27.4 * (string * string) option -> theory -> Proof.state
27.5 val typedef_i: (bool * string) * (bstring * string list * mixfix) * term
27.6 * (string * string) option -> theory -> Proof.state
27.7 - val setup: theory -> theory
27.8 end;
27.9
27.10 structure TypedefPackage: TYPEDEF_PACKAGE =
27.11 @@ -77,15 +76,13 @@
27.12 Abs_cases: thm, Rep_induct: thm, Abs_induct: thm};
27.13
27.14 structure TypedefData = TheoryDataFun
27.15 -(struct
27.16 - val name = "HOL/typedef";
27.17 +(
27.18 type T = info Symtab.table;
27.19 val empty = Symtab.empty;
27.20 val copy = I;
27.21 val extend = I;
27.22 fun merge _ tabs : T = Symtab.merge (K true) tabs;
27.23 - fun print _ _ = ();
27.24 -end);
27.25 +);
27.26
27.27 val get_info = Symtab.lookup o TypedefData.get;
27.28 fun put_info name info = TypedefData.map (Symtab.update (name, info));
27.29 @@ -270,8 +267,6 @@
27.30
27.31 end;
27.32
27.33 -val setup = TypedefData.init;
27.34 -
27.35
27.36
27.37 (** outer syntax **)
28.1 --- a/src/HOL/Typedef.thy Sun May 06 21:50:17 2007 +0200
28.2 +++ b/src/HOL/Typedef.thy Mon May 07 00:49:59 2007 +0200
28.3 @@ -90,8 +90,7 @@
28.4 use "Tools/typedef_codegen.ML"
28.5
28.6 setup {*
28.7 - TypedefPackage.setup
28.8 - #> TypecopyPackage.setup
28.9 + TypecopyPackage.setup
28.10 #> TypedefCodegen.setup
28.11 *}
28.12
29.1 --- a/src/HOL/arith_data.ML Sun May 06 21:50:17 2007 +0200
29.2 +++ b/src/HOL/arith_data.ML Mon May 07 00:49:59 2007 +0200
29.3 @@ -206,8 +206,7 @@
29.4 fun eq_arith_tactic (ArithTactic {id = id1, ...}, ArithTactic {id = id2, ...}) = (id1 = id2);
29.5
29.6 structure ArithTheoryData = TheoryDataFun
29.7 -(struct
29.8 - val name = "HOL/arith";
29.9 +(
29.10 type T = {splits: thm list,
29.11 inj_consts: (string * typ) list,
29.12 discrete: string list,
29.13 @@ -221,8 +220,7 @@
29.14 inj_consts = Library.merge (op =) (inj_consts1, inj_consts2),
29.15 discrete = Library.merge (op =) (discrete1, discrete2),
29.16 tactics = Library.merge eq_arith_tactic (tactics1, tactics2)};
29.17 - fun print _ _ = ();
29.18 -end);
29.19 +);
29.20
29.21 val arith_split_add = Thm.declaration_attribute (fn thm =>
29.22 Context.mapping (ArithTheoryData.map (fn {splits,inj_consts,discrete,tactics} =>
29.23 @@ -922,7 +920,6 @@
29.24 Most of the work is done by the cancel tactics. *)
29.25
29.26 val init_lin_arith_data =
29.27 - Fast_Arith.setup #>
29.28 Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} =>
29.29 {add_mono_thms = add_mono_thms @
29.30 @{thms add_mono_thms_ordered_semiring} @ @{thms add_mono_thms_ordered_field},
29.31 @@ -940,7 +937,6 @@
29.32 addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]
29.33 (*abel_cancel helps it work in abstract algebraic domains*)
29.34 addsimprocs nat_cancel_sums_add}) #>
29.35 - ArithTheoryData.init #>
29.36 arith_discrete "nat";
29.37
29.38 val fast_nat_arith_simproc =
30.1 --- a/src/Provers/Arith/fast_lin_arith.ML Sun May 06 21:50:17 2007 +0200
30.2 +++ b/src/Provers/Arith/fast_lin_arith.ML Mon May 07 00:49:59 2007 +0200
30.3 @@ -86,7 +86,6 @@
30.4
30.5 signature FAST_LIN_ARITH =
30.6 sig
30.7 - val setup: theory -> theory
30.8 val map_data: ({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
30.9 lessD: thm list, neqE: thm list, simpset: Simplifier.simpset}
30.10 -> {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
30.11 @@ -99,18 +98,15 @@
30.12 val cut_lin_arith_tac: simpset -> int -> tactic
30.13 end;
30.14
30.15 -functor Fast_Lin_Arith(structure LA_Logic:LIN_ARITH_LOGIC
30.16 +functor Fast_Lin_Arith(structure LA_Logic:LIN_ARITH_LOGIC
30.17 and LA_Data:LIN_ARITH_DATA) : FAST_LIN_ARITH =
30.18 struct
30.19
30.20
30.21 (** theory data **)
30.22
30.23 -(* data kind 'Provers/fast_lin_arith' *)
30.24 -
30.25 structure Data = TheoryDataFun
30.26 -(struct
30.27 - val name = "Provers/fast_lin_arith";
30.28 +(
30.29 type T = {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
30.30 lessD: thm list, neqE: thm list, simpset: Simplifier.simpset};
30.31
30.32 @@ -130,12 +126,9 @@
30.33 lessD = Drule.merge_rules (lessD1, lessD2),
30.34 neqE = Drule.merge_rules (neqE1, neqE2),
30.35 simpset = Simplifier.merge_ss (simpset1, simpset2)};
30.36 -
30.37 - fun print _ _ = ();
30.38 -end);
30.39 +);
30.40
30.41 val map_data = Data.map;
30.42 -val setup = Data.init;
30.43
30.44
30.45
30.46 @@ -424,7 +417,7 @@
30.47 local
30.48 exception FalseE of thm
30.49 in
30.50 -fun mkthm (sg:theory, ss:simpset) (asms:thm list) (just:injust) : thm =
30.51 +fun mkthm (sg:theory, ss) (asms:thm list) (just:injust) : thm =
30.52 let val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset, ...} =
30.53 Data.get sg;
30.54 val simpset' = Simplifier.inherit_context ss simpset;
30.55 @@ -503,7 +496,7 @@
30.56 fun integ(rlhs,r,rel,rrhs,s,d) =
30.57 let val (rn,rd) = Rat.quotient_of_rat r and (sn,sd) = Rat.quotient_of_rat s
30.58 val m = lcms(map (abs o snd o Rat.quotient_of_rat) (r :: s :: map snd rlhs @ map snd rrhs))
30.59 - fun mult(t,r) =
30.60 + fun mult(t,r) =
30.61 let val (i,j) = Rat.quotient_of_rat r
30.62 in (t,i * (m div j)) end
30.63 in (m,(map mult rlhs, rn*(m div rd), rel, map mult rrhs, sn*(m div sd), d)) end
30.64 @@ -527,7 +520,7 @@
30.65 else lineq(c,Lt,diff,just)
30.66 | "~<" => lineq(~c,Le,map (op~) diff,NotLessD(just))
30.67 | "=" => lineq(c,Eq,diff,just)
30.68 - | _ => sys_error("mklineq" ^ rel)
30.69 + | _ => sys_error("mklineq" ^ rel)
30.70 end;
30.71
30.72 (* ------------------------------------------------------------------------- *)
30.73 @@ -590,15 +583,9 @@
30.74 (* failure as soon as a case could not be refuted; i.e. delay further *)
30.75 (* splitting until after a refutation for other cases has been found. *)
30.76
30.77 -fun split_items sg (do_pre : bool) (Ts : typ list, terms : term list) :
30.78 +fun split_items sg (do_pre : bool) (Ts, terms) :
30.79 (typ list * (LA_Data.decompT * int) list) list =
30.80 let
30.81 -(*
30.82 - val _ = if !trace then
30.83 - trace_msg ("split_items: Ts = " ^ string_of_list (Sign.string_of_typ sg) Ts ^ "\n" ^
30.84 - " terms = " ^ string_of_list (Sign.string_of_term sg) terms)
30.85 - else ()
30.86 -*)
30.87 (* splits inequalities '~=' into '<' and '>'; this corresponds to *)
30.88 (* 'REPEAT_DETERM (eresolve_tac neqE i)' at the theorem/tactic *)
30.89 (* level *)
30.90 @@ -634,38 +621,14 @@
30.91
30.92 val result = (Ts, terms)
30.93 |> (* user-defined preprocessing of the subgoal *)
30.94 - (* (typ list * term list) list *)
30.95 (if do_pre then LA_Data.pre_decomp sg else Library.single)
30.96 - |> (* compute the internal encoding of (in-)equalities *)
30.97 - (* (typ list * (LA_Data.decompT option * bool) list) list *)
30.98 + |> (* produce the internal encoding of (in-)equalities *)
30.99 map (apsnd (map (fn t => (LA_Data.decomp sg t, LA_Data.domain_is_nat t))))
30.100 |> (* splitting of inequalities *)
30.101 - (* (typ list * (LA_Data.decompT option * bool) list list) list *)
30.102 map (apsnd elim_neq)
30.103 - |> (* combine the list of lists of subgoals into a single list *)
30.104 - map (fn (Ts, subgoals) => map (pair Ts o map fst) subgoals)
30.105 - |> List.concat
30.106 + |> maps (fn (Ts, subgoals) => map (pair Ts o map fst) subgoals)
30.107 |> (* numbering of hypotheses, ignoring irrelevant ones *)
30.108 map (apsnd (number_hyps 0))
30.109 -(*
30.110 - val _ = if !trace then
30.111 - trace_msg ("split_items: result has " ^ Int.toString (length result) ^
30.112 - " subgoal(s)" ^ "\n" ^ (cat_lines o fst) (fold_map (fn (Ts, items) => fn n =>
30.113 - (" " ^ Int.toString n ^ ". Ts = " ^
30.114 - string_of_list (Sign.string_of_typ sg) Ts ^ "\n" ^
30.115 - " items = " ^ string_of_list (string_of_pair
30.116 - (fn (l, i, rel, r, j, d) => enclose "(" ")" (commas
30.117 - [string_of_list
30.118 - (string_of_pair (Sign.string_of_term sg) Rat.string_of_rat) l,
30.119 - Rat.string_of_rat i,
30.120 - rel,
30.121 - string_of_list
30.122 - (string_of_pair (Sign.string_of_term sg) Rat.string_of_rat) r,
30.123 - Rat.string_of_rat j,
30.124 - Bool.toString d]))
30.125 - Int.toString) items, n+1)) result 1))
30.126 - else ()
30.127 -*)
30.128 in result end;
30.129
30.130 fun add_atoms (ats : term list, ((lhs,_,_,rhs,_,_) : LA_Data.decompT, _)) : term list =
30.131 @@ -742,7 +705,7 @@
30.132 refute sg params show_ex do_pre Hs'
30.133 end;
30.134
30.135 -fun refute_tac (ss : simpset) (i : int, justs : injust list) : tactic =
30.136 +fun refute_tac ss (i, justs) =
30.137 fn state =>
30.138 let val _ = trace_thm ("refute_tac (on subgoal " ^ Int.toString i ^ ", with " ^
30.139 Int.toString (length justs) ^ " justification(s)):") state
31.1 --- a/src/Provers/classical.ML Sun May 06 21:50:17 2007 +0200
31.2 +++ b/src/Provers/classical.ML Mon May 07 00:49:59 2007 +0200
31.3 @@ -140,9 +140,9 @@
31.4 val add_context_unsafe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory
31.5 val del_context_unsafe_wrapper: string -> theory -> theory
31.6 val get_claset: theory -> claset
31.7 - val print_local_claset: Proof.context -> unit
31.8 val get_local_claset: Proof.context -> claset
31.9 val put_local_claset: claset -> Proof.context -> Proof.context
31.10 + val print_local_claset: Proof.context -> unit
31.11 val safe_dest: int option -> attribute
31.12 val safe_elim: int option -> attribute
31.13 val safe_intro: int option -> attribute
31.14 @@ -857,19 +857,16 @@
31.15 (* global claset *)
31.16
31.17 structure GlobalClaset = TheoryDataFun
31.18 -(struct
31.19 - val name = "Provers/claset";
31.20 +(
31.21 type T = claset ref * context_cs;
31.22 -
31.23 val empty = (ref empty_cs, empty_context_cs);
31.24 fun copy (ref cs, ctxt_cs) = (ref cs, ctxt_cs): T;
31.25 val extend = copy;
31.26 fun merge _ ((ref cs1, ctxt_cs1), (ref cs2, ctxt_cs2)) =
31.27 (ref (merge_cs (cs1, cs2)), merge_context_cs (ctxt_cs1, ctxt_cs2));
31.28 - fun print _ (ref cs, _) = print_cs cs;
31.29 -end);
31.30 +);
31.31
31.32 -val print_claset = GlobalClaset.print;
31.33 +val print_claset = print_cs o ! o #1 o GlobalClaset.get;
31.34 val get_claset = ! o #1 o GlobalClaset.get;
31.35
31.36 val get_context_cs = #2 o GlobalClaset.get o ProofContext.theory_of;
31.37 @@ -912,20 +909,19 @@
31.38 (* local claset *)
31.39
31.40 structure LocalClaset = ProofDataFun
31.41 -(struct
31.42 - val name = "Provers/claset";
31.43 +(
31.44 type T = claset;
31.45 val init = get_claset;
31.46 - fun print ctxt cs = print_cs (context_cs ctxt cs (get_context_cs ctxt));
31.47 -end);
31.48 +);
31.49
31.50 -val print_local_claset = LocalClaset.print;
31.51 val get_local_claset = LocalClaset.get;
31.52 val put_local_claset = LocalClaset.put;
31.53
31.54 fun local_claset_of ctxt =
31.55 context_cs ctxt (get_local_claset ctxt) (get_context_cs ctxt);
31.56
31.57 +val print_local_claset = print_cs o local_claset_of;
31.58 +
31.59
31.60 (* attributes *)
31.61
31.62 @@ -1061,7 +1057,7 @@
31.63
31.64 (** theory setup **)
31.65
31.66 -val setup = GlobalClaset.init #> LocalClaset.init #> setup_attrs #> setup_methods;
31.67 +val setup = GlobalClaset.init #> setup_attrs #> setup_methods;
31.68
31.69
31.70
32.1 --- a/src/Pure/Isar/attrib.ML Sun May 06 21:50:17 2007 +0200
32.2 +++ b/src/Pure/Isar/attrib.ML Mon May 07 00:49:59 2007 +0200
32.3 @@ -49,29 +49,24 @@
32.4 (* theory data *)
32.5
32.6 structure AttributesData = TheoryDataFun
32.7 -(struct
32.8 - val name = "Isar/attributes";
32.9 +(
32.10 type T = (((src -> attribute) * string) * stamp) NameSpace.table;
32.11 -
32.12 val empty = NameSpace.empty_table;
32.13 val copy = I;
32.14 val extend = I;
32.15 -
32.16 fun merge _ tables = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUPS dups =>
32.17 error ("Attempt to merge different versions of attribute(s) " ^ commas_quote dups);
32.18 +);
32.19
32.20 - fun print _ attribs =
32.21 - let
32.22 - fun prt_attr (name, ((_, comment), _)) = Pretty.block
32.23 - [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
32.24 - in
32.25 - [Pretty.big_list "attributes:" (map prt_attr (NameSpace.extern_table attribs))]
32.26 - |> Pretty.chunks |> Pretty.writeln
32.27 - end;
32.28 -end);
32.29 -
32.30 -val _ = Context.add_setup AttributesData.init;
32.31 -val print_attributes = AttributesData.print;
32.32 +fun print_attributes thy =
32.33 + let
32.34 + val attribs = AttributesData.get thy;
32.35 + fun prt_attr (name, ((_, comment), _)) = Pretty.block
32.36 + [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
32.37 + in
32.38 + [Pretty.big_list "attributes:" (map prt_attr (NameSpace.extern_table attribs))]
32.39 + |> Pretty.chunks |> Pretty.writeln
32.40 + end;
32.41
32.42
32.43 (* name space *)
33.1 --- a/src/Pure/Isar/calculation.ML Sun May 06 21:50:17 2007 +0200
33.2 +++ b/src/Pure/Isar/calculation.ML Mon May 07 00:49:59 2007 +0200
33.3 @@ -30,25 +30,21 @@
33.4
33.5 structure CalculationData = GenericDataFun
33.6 (
33.7 - val name = "Isar/calculation";
33.8 type T = (thm NetRules.T * thm list) * (thm list * int) option;
33.9 val empty = ((NetRules.elim, []), NONE);
33.10 val extend = I;
33.11
33.12 fun merge _ (((trans1, sym1), _), ((trans2, sym2), _)) =
33.13 ((NetRules.merge (trans1, trans2), Drule.merge_rules (sym1, sym2)), NONE);
33.14 -
33.15 - fun print generic ((trans, sym), _) =
33.16 - let val ctxt = Context.proof_of generic in
33.17 - [Pretty.big_list "transitivity rules:"
33.18 - (map (ProofContext.pretty_thm ctxt) (NetRules.rules trans)),
33.19 - Pretty.big_list "symmetry rules:" (map (ProofContext.pretty_thm ctxt) sym)]
33.20 - |> Pretty.chunks |> Pretty.writeln
33.21 - end;
33.22 );
33.23
33.24 -val _ = Context.add_setup CalculationData.init;
33.25 -val print_rules = CalculationData.print o Context.Proof;
33.26 +fun print_rules ctxt =
33.27 + let val ((trans, sym), _) = CalculationData.get (Context.Proof ctxt) in
33.28 + [Pretty.big_list "transitivity rules:"
33.29 + (map (ProofContext.pretty_thm ctxt) (NetRules.rules trans)),
33.30 + Pretty.big_list "symmetry rules:" (map (ProofContext.pretty_thm ctxt) sym)]
33.31 + |> Pretty.chunks |> Pretty.writeln
33.32 + end;
33.33
33.34
33.35 (* access calculation *)
34.1 --- a/src/Pure/Isar/context_rules.ML Sun May 06 21:50:17 2007 +0200
34.2 +++ b/src/Pure/Isar/context_rules.ML Mon May 07 00:49:59 2007 +0200
34.3 @@ -94,9 +94,7 @@
34.4
34.5 structure Rules = GenericDataFun
34.6 (
34.7 - val name = "Pure/rules";
34.8 type T = T;
34.9 -
34.10 val empty = make_rules ~1 [] empty_netpairs ([], []);
34.11 val extend = I;
34.12
34.13 @@ -112,20 +110,17 @@
34.14 nth_map i (curry insert_tagged_brl ((w, n), (b, th))))
34.15 (next upto ~1 ~~ rules) empty_netpairs;
34.16 in make_rules (next - 1) rules netpairs wrappers end
34.17 -
34.18 - fun print generic (Rules {rules, ...}) =
34.19 - let
34.20 - val ctxt = Context.proof_of generic;
34.21 - fun prt_kind (i, b) =
34.22 - Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":")
34.23 - (map_filter (fn (_, (k, th)) =>
34.24 - if k = (i, b) then SOME (ProofContext.pretty_thm ctxt th) else NONE)
34.25 - (sort (int_ord o pairself fst) rules));
34.26 - in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
34.27 );
34.28
34.29 -val _ = Context.add_setup Rules.init;
34.30 -val print_rules = Rules.print o Context.Proof;
34.31 +fun print_rules ctxt =
34.32 + let
34.33 + val Rules {rules, ...} = Rules.get (Context.Proof ctxt);
34.34 + fun prt_kind (i, b) =
34.35 + Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":")
34.36 + (map_filter (fn (_, (k, th)) =>
34.37 + if k = (i, b) then SOME (ProofContext.pretty_thm ctxt th) else NONE)
34.38 + (sort (int_ord o pairself fst) rules));
34.39 + in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
34.40
34.41
34.42 (* access data *)
35.1 --- a/src/Pure/Isar/induct_attrib.ML Sun May 06 21:50:17 2007 +0200
35.2 +++ b/src/Pure/Isar/induct_attrib.ML Mon May 07 00:49:59 2007 +0200
35.3 @@ -94,49 +94,43 @@
35.4
35.5 (* context data *)
35.6
35.7 -fun dest ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) =
35.8 - {type_cases = NetRules.rules casesT,
35.9 - set_cases = NetRules.rules casesS,
35.10 - type_induct = NetRules.rules inductT,
35.11 - set_induct = NetRules.rules inductS,
35.12 - type_coinduct = NetRules.rules coinductT,
35.13 - set_coinduct = NetRules.rules coinductS};
35.14 -
35.15 structure Induct = GenericDataFun
35.16 (
35.17 - val name = "Isar/induct";
35.18 type T = (rules * rules) * (rules * rules) * (rules * rules);
35.19 -
35.20 val empty =
35.21 ((init_rules (left_var_prem o #2), init_rules (Thm.major_prem_of o #2)),
35.22 (init_rules (right_var_concl o #2), init_rules (Thm.major_prem_of o #2)),
35.23 (init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2)));
35.24 -
35.25 val extend = I;
35.26 -
35.27 fun merge _ (((casesT1, casesS1), (inductT1, inductS1), (coinductT1, coinductS1)),
35.28 ((casesT2, casesS2), (inductT2, inductS2), (coinductT2, coinductS2))) =
35.29 ((NetRules.merge (casesT1, casesT2), NetRules.merge (casesS1, casesS2)),
35.30 (NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2)),
35.31 (NetRules.merge (coinductT1, coinductT2), NetRules.merge (coinductS1, coinductS2)));
35.32 -
35.33 - fun print generic ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) =
35.34 - let val ctxt = Context.proof_of generic in
35.35 - [pretty_rules ctxt "coinduct type:" coinductT,
35.36 - pretty_rules ctxt "coinduct set:" coinductS,
35.37 - pretty_rules ctxt "induct type:" inductT,
35.38 - pretty_rules ctxt "induct set:" inductS,
35.39 - pretty_rules ctxt "cases type:" casesT,
35.40 - pretty_rules ctxt "cases set:" casesS]
35.41 - |> Pretty.chunks |> Pretty.writeln
35.42 - end
35.43 );
35.44
35.45 -val _ = Context.add_setup Induct.init;
35.46 -val print_rules = Induct.print o Context.Proof;
35.47 -val dest_rules = dest o Induct.get o Context.Proof;
35.48 +val get_local = Induct.get o Context.Proof;
35.49
35.50 -val get_local = Induct.get o Context.Proof;
35.51 +fun dest_rules ctxt =
35.52 + let val ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) = get_local ctxt in
35.53 + {type_cases = NetRules.rules casesT,
35.54 + set_cases = NetRules.rules casesS,
35.55 + type_induct = NetRules.rules inductT,
35.56 + set_induct = NetRules.rules inductS,
35.57 + type_coinduct = NetRules.rules coinductT,
35.58 + set_coinduct = NetRules.rules coinductS}
35.59 + end;
35.60 +
35.61 +fun print_rules ctxt =
35.62 + let val ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) = get_local ctxt in
35.63 + [pretty_rules ctxt "coinduct type:" coinductT,
35.64 + pretty_rules ctxt "coinduct set:" coinductS,
35.65 + pretty_rules ctxt "induct type:" inductT,
35.66 + pretty_rules ctxt "induct set:" inductS,
35.67 + pretty_rules ctxt "cases type:" casesT,
35.68 + pretty_rules ctxt "cases set:" casesS]
35.69 + |> Pretty.chunks |> Pretty.writeln
35.70 + end;
35.71
35.72
35.73 (* access rules *)
36.1 --- a/src/Pure/Isar/local_defs.ML Sun May 06 21:50:17 2007 +0200
36.2 +++ b/src/Pure/Isar/local_defs.ML Mon May 07 00:49:59 2007 +0200
36.3 @@ -147,19 +147,15 @@
36.4
36.5 structure Rules = GenericDataFun
36.6 (
36.7 - val name = "Pure/derived_defs";
36.8 type T = thm list;
36.9 val empty = []
36.10 val extend = I;
36.11 fun merge _ = Drule.merge_rules;
36.12 - fun print context rules =
36.13 - Pretty.writeln (Pretty.big_list "definitional transformations:"
36.14 - (map (ProofContext.pretty_thm (Context.proof_of context)) rules));
36.15 );
36.16
36.17 -val _ = Context.add_setup Rules.init;
36.18 -
36.19 -val print_rules = Rules.print o Context.Proof;
36.20 +fun print_rules ctxt =
36.21 + Pretty.writeln (Pretty.big_list "definitional transformations:"
36.22 + (map (ProofContext.pretty_thm ctxt) (Rules.get (Context.Proof ctxt))));
36.23
36.24 val defn_add = Thm.declaration_attribute (Rules.map o Drule.add_rule);
36.25 val defn_del = Thm.declaration_attribute (Rules.map o Drule.del_rule);
37.1 --- a/src/Pure/Isar/local_theory.ML Sun May 06 21:50:17 2007 +0200
37.2 +++ b/src/Pure/Isar/local_theory.ML Mon May 07 00:49:59 2007 +0200
37.3 @@ -88,12 +88,9 @@
37.4
37.5 structure Data = ProofDataFun
37.6 (
37.7 - val name = "Pure/local_theory";
37.8 type T = lthy option;
37.9 fun init _ = NONE;
37.10 - fun print _ _ = ();
37.11 );
37.12 -val _ = Context.add_setup Data.init;
37.13
37.14 fun get_lthy lthy =
37.15 (case Data.get lthy of
38.1 --- a/src/Pure/Isar/locale.ML Sun May 06 21:50:17 2007 +0200
38.2 +++ b/src/Pure/Isar/locale.ML Mon May 07 00:49:59 2007 +0200
38.3 @@ -305,8 +305,7 @@
38.4 (** theory data **)
38.5
38.6 structure GlobalLocalesData = TheoryDataFun
38.7 -(struct
38.8 - val name = "Isar/locales";
38.9 +(
38.10 type T = NameSpace.T * locale Symtab.table * Registrations.T Symtab.table;
38.11 (* 1st entry: locale namespace,
38.12 2nd entry: locales of the theory,
38.13 @@ -332,33 +331,26 @@
38.14 fun merge _ ((space1, locs1, regs1), (space2, locs2, regs2)) =
38.15 (NameSpace.merge (space1, space2), Symtab.join join_locales (locs1, locs2),
38.16 Symtab.join (K Registrations.join) (regs1, regs2));
38.17 -
38.18 - fun print _ (space, locs, _) =
38.19 +);
38.20 +
38.21 +
38.22 +
38.23 +(** context data **)
38.24 +
38.25 +structure LocalLocalesData = ProofDataFun
38.26 +(
38.27 + type T = Registrations.T Symtab.table; (*registrations, indexed by locale name*)
38.28 + fun init _ = Symtab.empty;
38.29 +);
38.30 +
38.31 +
38.32 +(* access locales *)
38.33 +
38.34 +fun print_locales thy =
38.35 + let val (space, locs, _) = GlobalLocalesData.get thy in
38.36 Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs)))
38.37 - |> Pretty.writeln;
38.38 -end);
38.39 -
38.40 -val _ = Context.add_setup GlobalLocalesData.init;
38.41 -
38.42 -
38.43 -
38.44 -(** context data **)
38.45 -
38.46 -structure LocalLocalesData = ProofDataFun
38.47 -(struct
38.48 - val name = "Isar/locales";
38.49 - type T = Registrations.T Symtab.table;
38.50 - (* registrations, indexed by locale name *)
38.51 - fun init _ = Symtab.empty;
38.52 - fun print _ _ = ();
38.53 -end);
38.54 -
38.55 -val _ = Context.add_setup LocalLocalesData.init;
38.56 -
38.57 -
38.58 -(* access locales *)
38.59 -
38.60 -val print_locales = GlobalLocalesData.print;
38.61 + |> Pretty.writeln
38.62 + end;
38.63
38.64 val intern = NameSpace.intern o #1 o GlobalLocalesData.get;
38.65 val extern = NameSpace.extern o #1 o GlobalLocalesData.get;
39.1 --- a/src/Pure/Isar/method.ML Sun May 06 21:50:17 2007 +0200
39.2 +++ b/src/Pure/Isar/method.ML Mon May 07 00:49:59 2007 +0200
39.3 @@ -378,28 +378,24 @@
39.4 (* method definitions *)
39.5
39.6 structure MethodsData = TheoryDataFun
39.7 -(struct
39.8 - val name = "Isar/methods";
39.9 +(
39.10 type T = (((src -> Proof.context -> method) * string) * stamp) NameSpace.table;
39.11 -
39.12 val empty = NameSpace.empty_table;
39.13 val copy = I;
39.14 val extend = I;
39.15 fun merge _ tables = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUPS dups =>
39.16 error ("Attempt to merge different versions of method(s) " ^ commas_quote dups);
39.17 +);
39.18
39.19 - fun print _ meths =
39.20 - let
39.21 - fun prt_meth (name, ((_, comment), _)) = Pretty.block
39.22 - [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
39.23 - in
39.24 - [Pretty.big_list "methods:" (map prt_meth (NameSpace.extern_table meths))]
39.25 - |> Pretty.chunks |> Pretty.writeln
39.26 - end;
39.27 -end);
39.28 -
39.29 -val _ = Context.add_setup MethodsData.init;
39.30 -val print_methods = MethodsData.print;
39.31 +fun print_methods thy =
39.32 + let
39.33 + val meths = MethodsData.get thy;
39.34 + fun prt_meth (name, ((_, comment), _)) = Pretty.block
39.35 + [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
39.36 + in
39.37 + [Pretty.big_list "methods:" (map prt_meth (NameSpace.extern_table meths))]
39.38 + |> Pretty.chunks |> Pretty.writeln
39.39 + end;
39.40
39.41
39.42 (* get methods *)
40.1 --- a/src/Pure/Isar/object_logic.ML Sun May 06 21:50:17 2007 +0200
40.2 +++ b/src/Pure/Isar/object_logic.ML Mon May 07 00:49:59 2007 +0200
40.3 @@ -38,11 +38,9 @@
40.4 (** theory data **)
40.5
40.6 structure ObjectLogicData = TheoryDataFun
40.7 -(struct
40.8 - val name = "Pure/object_logic";
40.9 +(
40.10 type T = string option * (thm list * thm list);
40.11 -
40.12 - val empty = (NONE, ([], [Drule.norm_hhf_eq]));
40.13 + val empty = (NONE, ([], []));
40.14 val copy = I;
40.15 val extend = I;
40.16
40.17 @@ -53,11 +51,7 @@
40.18 fun merge _ ((judgment1, (atomize1, rulify1)), (judgment2, (atomize2, rulify2))) =
40.19 (merge_judgment (judgment1, judgment2),
40.20 (Drule.merge_rules (atomize1, atomize2), Drule.merge_rules (rulify1, rulify2)));
40.21 -
40.22 - fun print _ _ = ();
40.23 -end);
40.24 -
40.25 -val _ = Context.add_setup ObjectLogicData.init;
40.26 +);
40.27
40.28
40.29
40.30 @@ -136,11 +130,13 @@
40.31 val get_atomize = #1 o #2 o ObjectLogicData.get;
40.32 val get_rulify = #2 o #2 o ObjectLogicData.get;
40.33
40.34 -val declare_atomize = Thm.declaration_attribute (fn th =>
40.35 - Context.mapping (ObjectLogicData.map (apsnd (apfst (Drule.add_rule th)))) I);
40.36 +val add_atomize = ObjectLogicData.map o apsnd o apfst o Drule.add_rule;
40.37 +val add_rulify = ObjectLogicData.map o apsnd o apsnd o Drule.add_rule;
40.38
40.39 -val declare_rulify = Thm.declaration_attribute (fn th =>
40.40 - Context.mapping (ObjectLogicData.map (apsnd (apsnd (Drule.add_rule th)))) I);
40.41 +val declare_atomize = Thm.declaration_attribute (fn th => Context.mapping (add_atomize th) I);
40.42 +val declare_rulify = Thm.declaration_attribute (fn th => Context.mapping (add_rulify th) I);
40.43 +
40.44 +val _ = Context.add_setup (add_rulify Drule.norm_hhf_eq);
40.45
40.46
40.47 (* atomize *)
41.1 --- a/src/Pure/Isar/proof_context.ML Sun May 06 21:50:17 2007 +0200
41.2 +++ b/src/Pure/Isar/proof_context.ML Mon May 07 00:49:59 2007 +0200
41.3 @@ -198,17 +198,13 @@
41.4
41.5 structure ContextData = ProofDataFun
41.6 (
41.7 - val name = "Isar/context";
41.8 type T = ctxt;
41.9 fun init thy =
41.10 make_ctxt (false, local_naming, LocalSyntax.init thy,
41.11 (Sign.consts_of thy, Sign.consts_of thy),
41.12 (NameSpace.empty_table, FactIndex.empty), []);
41.13 - fun print _ _ = ();
41.14 );
41.15
41.16 -val _ = Context.add_setup ContextData.init;
41.17 -
41.18 fun rep_context ctxt = ContextData.get ctxt |> (fn Ctxt args => args);
41.19
41.20 fun map_context f =
42.1 --- a/src/Pure/Isar/theory_target.ML Sun May 06 21:50:17 2007 +0200
42.2 +++ b/src/Pure/Isar/theory_target.ML Mon May 07 00:49:59 2007 +0200
42.3 @@ -22,13 +22,10 @@
42.4
42.5 structure Data = ProofDataFun
42.6 (
42.7 - val name = "Isar/theory_target";
42.8 type T = string option;
42.9 fun init _ = NONE;
42.10 - fun print _ _ = ();
42.11 );
42.12
42.13 -val _ = Context.add_setup Data.init;
42.14 val peek = Data.get;
42.15
42.16
43.1 --- a/src/Pure/Proof/extraction.ML Sun May 06 21:50:17 2007 +0200
43.2 +++ b/src/Pure/Proof/extraction.ML Mon May 07 00:49:59 2007 +0200
43.3 @@ -171,11 +171,10 @@
43.4
43.5 (**** theory data ****)
43.6
43.7 -(* data kind 'Pure/extraction' *)
43.8 +(* theory data *)
43.9
43.10 structure ExtractionData = TheoryDataFun
43.11 -(struct
43.12 - val name = "Pure/extraction";
43.13 +(
43.14 type T =
43.15 {realizes_eqns : rules,
43.16 typeof_eqns : rules,
43.17 @@ -209,11 +208,7 @@
43.18 defs = Library.merge Thm.eq_thm (defs1, defs2),
43.19 expand = Library.merge (op =) (expand1, expand2),
43.20 prep = (case prep1 of NONE => prep2 | _ => prep1)};
43.21 -
43.22 - fun print _ _ = ();
43.23 -end);
43.24 -
43.25 -val _ = Context.add_setup ExtractionData.init;
43.26 +);
43.27
43.28 fun read_condeq thy =
43.29 let val thy' = add_syntax thy
44.1 --- a/src/Pure/Thy/present.ML Sun May 06 21:50:17 2007 +0200
44.2 +++ b/src/Pure/Thy/present.ML Mon May 07 00:49:59 2007 +0200
44.3 @@ -75,17 +75,13 @@
44.4 (** additional theory data **)
44.5
44.6 structure BrowserInfoData = TheoryDataFun
44.7 -(struct
44.8 - val name = "Pure/browser_info";
44.9 +(
44.10 type T = {name: string, session: string list, is_local: bool};
44.11 val empty = {name = "", session = [], is_local = false}: T;
44.12 val copy = I;
44.13 fun extend _ = empty;
44.14 fun merge _ _ = empty;
44.15 - fun print _ _ = ();
44.16 -end);
44.17 -
44.18 -val _ = Context.add_setup BrowserInfoData.init;
44.19 +);
44.20
44.21 fun get_info thy =
44.22 if member (op =) [Context.ProtoPureN, Context.PureN, Context.CPureN] (Context.theory_name thy)
45.1 --- a/src/Pure/Thy/term_style.ML Sun May 06 21:50:17 2007 +0200
45.2 +++ b/src/Pure/Thy/term_style.ML Mon May 07 00:49:59 2007 +0200
45.3 @@ -22,19 +22,17 @@
45.4 error ("Duplicate declaration of antiquote style(s): " ^ commas_quote names);
45.5
45.6 structure StyleData = TheoryDataFun
45.7 -(struct
45.8 - val name = "Isar/antiquote_style";
45.9 +(
45.10 type T = ((Proof.context -> term -> term) * stamp) Symtab.table;
45.11 val empty = Symtab.empty;
45.12 val copy = I;
45.13 val extend = I;
45.14 fun merge _ tabs = Symtab.merge (eq_snd (op =)) tabs
45.15 handle Symtab.DUPS dups => err_dup_styles dups;
45.16 - fun print _ tab = Pretty.writeln (Pretty.strs ("antiquote styles:" :: Symtab.keys tab));
45.17 -end);
45.18 +);
45.19
45.20 -val _ = Context.add_setup StyleData.init;
45.21 -val print_styles = StyleData.print;
45.22 +fun print_styles thy =
45.23 + Pretty.writeln (Pretty.strs ("antiquote styles:" :: Symtab.keys (StyleData.get thy)));
45.24
45.25
45.26 (* accessors *)
46.1 --- a/src/Pure/Tools/class_package.ML Sun May 06 21:50:17 2007 +0200
46.2 +++ b/src/Pure/Tools/class_package.ML Mon May 07 00:49:59 2007 +0200
46.3 @@ -237,20 +237,15 @@
46.4
46.5 fun merge_pair f1 f2 ((x1, y1), (x2, y2)) = (f1 (x1, x2), f2 (y1, y2));
46.6
46.7 -structure ClassData = TheoryDataFun (
46.8 - struct
46.9 - val name = "Pure/classes";
46.10 - type T = class_data Graph.T * class Symtab.table (*locale name ~> class name*);
46.11 - val empty = (Graph.empty, Symtab.empty);
46.12 - val copy = I;
46.13 - val extend = I;
46.14 - fun merge _ = merge_pair (Graph.merge (K true)) (Symtab.merge (K true));
46.15 - fun print _ _ = ();
46.16 - end
46.17 +structure ClassData = TheoryDataFun
46.18 +(
46.19 + type T = class_data Graph.T * class Symtab.table (*locale name ~> class name*);
46.20 + val empty = (Graph.empty, Symtab.empty);
46.21 + val copy = I;
46.22 + val extend = I;
46.23 + fun merge _ = merge_pair (Graph.merge (K true)) (Symtab.merge (K true));
46.24 );
46.25
46.26 -val _ = Context.add_setup ClassData.init;
46.27 -
46.28
46.29 (* queries *)
46.30
47.1 --- a/src/Pure/Tools/codegen_data.ML Sun May 06 21:50:17 2007 +0200
47.2 +++ b/src/Pure/Tools/codegen_data.ML Mon May 07 00:49:59 2007 +0200
47.3 @@ -312,8 +312,7 @@
47.4 type data = Object.T Datatab.table;
47.5
47.6 structure CodeData = TheoryDataFun
47.7 -(struct
47.8 - val name = "Pure/codegen_data";
47.9 +(
47.10 type T = exec * data ref;
47.11 val empty = (empty_exec, ref Datatab.empty : data ref);
47.12 fun copy (exec, data) = (exec, ref (! data));
47.13 @@ -325,67 +324,67 @@
47.14 val data2' = Datatab.map' (invoke_purge NONE touched) (! data2);
47.15 val data = Datatab.join (invoke_merge pp) (data1', data2');
47.16 in (exec, ref data) end;
47.17 - fun print thy (exec, _) =
47.18 - let
47.19 - val ctxt = ProofContext.init thy;
47.20 - fun pretty_func (s, lthms) =
47.21 - (Pretty.block o Pretty.fbreaks) (
47.22 - Pretty.str s :: pretty_sdthms ctxt lthms
47.23 - );
47.24 - fun pretty_dtyp (s, []) =
47.25 +);
47.26 +
47.27 +fun print_codesetup thy =
47.28 + let
47.29 + val ctxt = ProofContext.init thy;
47.30 + val (exec, _) = CodeData.get thy;
47.31 + fun pretty_func (s, lthms) =
47.32 + (Pretty.block o Pretty.fbreaks) (
47.33 + Pretty.str s :: pretty_sdthms ctxt lthms
47.34 + );
47.35 + fun pretty_dtyp (s, []) =
47.36 + Pretty.str s
47.37 + | pretty_dtyp (s, cos) =
47.38 + (Pretty.block o Pretty.breaks) (
47.39 Pretty.str s
47.40 - | pretty_dtyp (s, cos) =
47.41 - (Pretty.block o Pretty.breaks) (
47.42 - Pretty.str s
47.43 - :: Pretty.str "="
47.44 - :: separate (Pretty.str "|") (map (fn (c, []) => Pretty.str c
47.45 - | (c, tys) =>
47.46 - (Pretty.block o Pretty.breaks)
47.47 - (Pretty.str c :: Pretty.str "of" :: map (Pretty.quote o Sign.pretty_typ thy) tys)) cos)
47.48 - );
47.49 - val inlines = (#inlines o the_preproc) exec;
47.50 - val inline_procs = (map fst o #inline_procs o the_preproc) exec;
47.51 - val preprocs = (map fst o #preprocs o the_preproc) exec;
47.52 - val funs = the_funcs exec
47.53 - |> Consttab.dest
47.54 - |> (map o apfst) (CodegenConsts.string_of_const thy)
47.55 - |> sort (string_ord o pairself fst);
47.56 - val dtyps = the_dtyps exec
47.57 - |> Symtab.dest
47.58 - |> map (fn (dtco, (vs, cos)) => (Sign.string_of_typ thy (Type (dtco, map TFree vs)), cos))
47.59 - |> sort (string_ord o pairself fst)
47.60 - in
47.61 - (Pretty.writeln o Pretty.chunks) [
47.62 - Pretty.block (
47.63 - Pretty.str "defining equations:"
47.64 - :: Pretty.fbrk
47.65 - :: (Pretty.fbreaks o map pretty_func) funs
47.66 - ),
47.67 - Pretty.block (
47.68 - Pretty.str "inlining theorems:"
47.69 - :: Pretty.fbrk
47.70 - :: (Pretty.fbreaks o map (ProofContext.pretty_thm ctxt)) inlines
47.71 - ),
47.72 - Pretty.block (
47.73 - Pretty.str "inlining procedures:"
47.74 - :: Pretty.fbrk
47.75 - :: (Pretty.fbreaks o map Pretty.str) inline_procs
47.76 - ),
47.77 - Pretty.block (
47.78 - Pretty.str "preprocessors:"
47.79 - :: Pretty.fbrk
47.80 - :: (Pretty.fbreaks o map Pretty.str) preprocs
47.81 - ),
47.82 - Pretty.block (
47.83 - Pretty.str "datatypes:"
47.84 - :: Pretty.fbrk
47.85 - :: (Pretty.fbreaks o map pretty_dtyp) dtyps
47.86 - )
47.87 - ]
47.88 - end;
47.89 -end);
47.90 -
47.91 -val print_codesetup = CodeData.print;
47.92 + :: Pretty.str "="
47.93 + :: separate (Pretty.str "|") (map (fn (c, []) => Pretty.str c
47.94 + | (c, tys) =>
47.95 + (Pretty.block o Pretty.breaks)
47.96 + (Pretty.str c :: Pretty.str "of" :: map (Pretty.quote o Sign.pretty_typ thy) tys)) cos)
47.97 + );
47.98 + val inlines = (#inlines o the_preproc) exec;
47.99 + val inline_procs = (map fst o #inline_procs o the_preproc) exec;
47.100 + val preprocs = (map fst o #preprocs o the_preproc) exec;
47.101 + val funs = the_funcs exec
47.102 + |> Consttab.dest
47.103 + |> (map o apfst) (CodegenConsts.string_of_const thy)
47.104 + |> sort (string_ord o pairself fst);
47.105 + val dtyps = the_dtyps exec
47.106 + |> Symtab.dest
47.107 + |> map (fn (dtco, (vs, cos)) => (Sign.string_of_typ thy (Type (dtco, map TFree vs)), cos))
47.108 + |> sort (string_ord o pairself fst)
47.109 + in
47.110 + (Pretty.writeln o Pretty.chunks) [
47.111 + Pretty.block (
47.112 + Pretty.str "defining equations:"
47.113 + :: Pretty.fbrk
47.114 + :: (Pretty.fbreaks o map pretty_func) funs
47.115 + ),
47.116 + Pretty.block (
47.117 + Pretty.str "inlining theorems:"
47.118 + :: Pretty.fbrk
47.119 + :: (Pretty.fbreaks o map (ProofContext.pretty_thm ctxt)) inlines
47.120 + ),
47.121 + Pretty.block (
47.122 + Pretty.str "inlining procedures:"
47.123 + :: Pretty.fbrk
47.124 + :: (Pretty.fbreaks o map Pretty.str) inline_procs
47.125 + ),
47.126 + Pretty.block (
47.127 + Pretty.str "preprocessors:"
47.128 + :: Pretty.fbrk
47.129 + :: (Pretty.fbreaks o map Pretty.str) preprocs
47.130 + ),
47.131 + Pretty.block (
47.132 + Pretty.str "datatypes:"
47.133 + :: Pretty.fbrk
47.134 + :: (Pretty.fbreaks o map pretty_dtyp) dtyps
47.135 + )
47.136 + ]
47.137 + end;
47.138
47.139 fun init k = CodeData.map
47.140 (fn (exec, data) => (exec, ref (Datatab.update (k, invoke_empty k) (! data))));
48.1 --- a/src/Pure/Tools/codegen_names.ML Sun May 06 21:50:17 2007 +0200
48.2 +++ b/src/Pure/Tools/codegen_names.ML Mon May 07 00:49:59 2007 +0200
48.3 @@ -292,18 +292,16 @@
48.4 end; (*local*)
48.5
48.6 structure CodeName = TheoryDataFun
48.7 -(struct
48.8 - val name = "Pure/codegen_names";
48.9 +(
48.10 type T = names ref;
48.11 val empty = ref empty_names;
48.12 fun copy (ref names) = ref names;
48.13 val extend = copy;
48.14 fun merge _ (ref names1, ref names2) = ref (merge_names (names1, names2));
48.15 - fun print _ _ = ();
48.16 -end);
48.17 +);
48.18
48.19 structure ConstName = CodeDataFun
48.20 -(struct
48.21 +(
48.22 val name = "Pure/codegen_names";
48.23 type T = const Consttab.table * (string * string option) Symtab.table;
48.24 val empty = (Consttab.empty, Symtab.empty);
48.25 @@ -313,7 +311,7 @@
48.26 fun purge _ NONE _ = empty
48.27 | purge _ (SOME cs) (const, constrev) = (fold Consttab.delete_safe cs const,
48.28 fold Symtab.delete (map_filter (Consttab.lookup const) cs) constrev);
48.29 -end);
48.30 +);
48.31
48.32 val _ = Context.add_setup (CodeName.init #> ConstName.init);
48.33
49.1 --- a/src/Pure/Tools/codegen_package.ML Sun May 06 21:50:17 2007 +0200
49.2 +++ b/src/Pure/Tools/codegen_package.ML Mon May 07 00:49:59 2007 +0200
49.3 @@ -51,18 +51,17 @@
49.4 Consttab.merge CodegenConsts.eq_const (consts1, consts2));
49.5
49.6 structure CodegenPackageData = TheoryDataFun
49.7 -(struct
49.8 - val name = "Pure/codegen_package_setup";
49.9 +(
49.10 type T = appgens * abstypes;
49.11 val empty = (Symtab.empty, (Symtab.empty, Consttab.empty));
49.12 val copy = I;
49.13 val extend = I;
49.14 fun merge _ ((appgens1, abstypes1), (appgens2, abstypes2)) =
49.15 (merge_appgens (appgens1, appgens2), merge_abstypes (abstypes1, abstypes2));
49.16 - fun print _ _ = ();
49.17 -end);
49.18 +);
49.19
49.20 -structure Funcgr = CodegenFuncgrRetrieval (
49.21 +structure Funcgr = CodegenFuncgrRetrieval
49.22 +(
49.23 val name = "Pure/codegen_package_thms";
49.24 fun rewrites thy = [];
49.25 );
49.26 @@ -94,7 +93,7 @@
49.27 in Present.display_graph prgr end;
49.28
49.29 structure Code = CodeDataFun
49.30 -(struct
49.31 +(
49.32 val name = "Pure/codegen_package_code";
49.33 type T = CodegenThingol.code;
49.34 val empty = CodegenThingol.empty_code;
49.35 @@ -110,9 +109,9 @@
49.36 o filter (member CodegenConsts.eq_const cs_exisiting)
49.37 ) cs;
49.38 in Graph.del_nodes dels code end;
49.39 -end);
49.40 +);
49.41
49.42 -val _ = Context.add_setup (CodegenPackageData.init #> Funcgr.init #> Code.init);
49.43 +val _ = Context.add_setup (Funcgr.init #> Code.init);
49.44
49.45
49.46 (* preparing defining equations *)
50.1 --- a/src/Pure/Tools/codegen_serializer.ML Sun May 06 21:50:17 2007 +0200
50.2 +++ b/src/Pure/Tools/codegen_serializer.ML Mon May 07 00:49:59 2007 +0200
50.3 @@ -1539,15 +1539,13 @@
50.4 error ("Incompatible serializers: " ^ quote target);
50.5
50.6 structure CodegenSerializerData = TheoryDataFun
50.7 -(struct
50.8 - val name = "Pure/codegen_serializer";
50.9 +(
50.10 type T = target Symtab.table;
50.11 val empty = Symtab.empty;
50.12 val copy = I;
50.13 val extend = I;
50.14 fun merge _ = Symtab.join merge_target;
50.15 - fun print _ _ = ();
50.16 -end);
50.17 +);
50.18
50.19 fun the_serializer (Target { serializer, ... }) = serializer;
50.20 fun the_reserved (Target { reserved, ... }) = reserved;
50.21 @@ -1587,8 +1585,7 @@
50.22 val target_diag = "diag";
50.23
50.24 val _ = Context.add_setup (
50.25 - CodegenSerializerData.init
50.26 - #> add_serializer (target_SML, isar_seri_sml)
50.27 + add_serializer (target_SML, isar_seri_sml)
50.28 #> add_serializer (target_OCaml, isar_seri_ocaml)
50.29 #> add_serializer (target_Haskell, isar_seri_haskell)
50.30 #> add_serializer (target_diag, (fn _ => fn _ => fn _ => seri_diagnosis))
51.1 --- a/src/Pure/Tools/nbe.ML Sun May 06 21:50:17 2007 +0200
51.2 +++ b/src/Pure/Tools/nbe.ML Mon May 07 00:49:59 2007 +0200
51.3 @@ -26,19 +26,14 @@
51.4 (* preproc and postproc attributes *)
51.5
51.6 structure NBE_Rewrite = TheoryDataFun
51.7 -(struct
51.8 - val name = "Pure/nbe";
51.9 +(
51.10 type T = thm list * thm list
51.11 -
51.12 - val empty = ([],[])
51.13 + val empty = ([], []);
51.14 val copy = I;
51.15 val extend = I;
51.16 -
51.17 fun merge _ ((pres1,posts1), (pres2,posts2)) =
51.18 (Library.merge Thm.eq_thm (pres1,pres2), Library.merge Thm.eq_thm (posts1,posts2))
51.19 -
51.20 - fun print _ _ = ()
51.21 -end);
51.22 +);
51.23
51.24 val _ =
51.25 let
51.26 @@ -51,8 +46,7 @@
51.27 || Args.$$$ "post" >> K attr_post));
51.28 in
51.29 Context.add_setup (
51.30 - NBE_Rewrite.init
51.31 - #> Attrib.add_attributes
51.32 + Attrib.add_attributes
51.33 [("normal", attr, "declare rewrite theorems for normalization")]
51.34 )
51.35 end;
52.1 --- a/src/Pure/assumption.ML Sun May 06 21:50:17 2007 +0200
52.2 +++ b/src/Pure/assumption.ML Mon May 07 00:49:59 2007 +0200
52.3 @@ -62,14 +62,10 @@
52.4
52.5 structure Data = ProofDataFun
52.6 (
52.7 - val name = "Pure/assumption";
52.8 type T = data;
52.9 fun init _ = make_data ([], []);
52.10 - fun print _ _ = ();
52.11 );
52.12
52.13 -val _ = Context.add_setup Data.init;
52.14 -
52.15 fun map_data f = Data.map (fn Data {assms, prems} => make_data (f (assms, prems)));
52.16 fun rep_data ctxt = Data.get ctxt |> (fn Data args => args);
52.17
53.1 --- a/src/Pure/axclass.ML Sun May 06 21:50:17 2007 +0200
53.2 +++ b/src/Pure/axclass.ML Mon May 07 00:49:59 2007 +0200
53.3 @@ -95,18 +95,14 @@
53.4 (* setup data *)
53.5
53.6 structure AxClassData = TheoryDataFun
53.7 -(struct
53.8 - val name = "Pure/axclass";
53.9 +(
53.10 type T = axclasses * instances;
53.11 - val empty : T = ((Symtab.empty, []), ([], Symtab.empty));
53.12 + val empty = ((Symtab.empty, []), ([], Symtab.empty));
53.13 val copy = I;
53.14 val extend = I;
53.15 fun merge pp ((axclasses1, instances1), (axclasses2, instances2)) =
53.16 (merge_axclasses pp (axclasses1, axclasses2), (merge_instances (instances1, instances2)));
53.17 - fun print _ _ = ();
53.18 -end);
53.19 -
53.20 -val _ = Context.add_setup AxClassData.init;
53.21 +);
53.22
53.23
53.24 (* maintain axclasses *)
54.1 --- a/src/Pure/codegen.ML Sun May 06 21:50:17 2007 +0200
54.2 +++ b/src/Pure/codegen.ML Mon May 07 00:49:59 2007 +0200
54.3 @@ -199,13 +199,13 @@
54.4 {size = size, iterations = iterations,
54.5 default_type = SOME (Sign.read_typ thy s)};
54.6
54.7 -(* data kind 'Pure/codegen' *)
54.8 +
54.9 +(* theory data *)
54.10
54.11 structure CodeData = CodegenData;
54.12
54.13 structure CodegenData = TheoryDataFun
54.14 -(struct
54.15 - val name = "Pure/codegen";
54.16 +(
54.17 type T =
54.18 {codegens : (string * term codegen) list,
54.19 tycodegens : (string * typ codegen) list,
54.20 @@ -237,15 +237,15 @@
54.21 preprocs = AList.merge (op =) (K true) (preprocs1, preprocs2),
54.22 modules = Symtab.merge (K true) (modules1, modules2),
54.23 test_params = merge_test_params test_params1 test_params2};
54.24 +);
54.25
54.26 - fun print _ ({codegens, tycodegens, ...} : T) =
54.27 +fun print_codegens thy =
54.28 + let val {codegens, tycodegens, ...} = CodegenData.get thy in
54.29 Pretty.writeln (Pretty.chunks
54.30 [Pretty.strs ("term code generators:" :: map fst codegens),
54.31 - Pretty.strs ("type code generators:" :: map fst tycodegens)]);
54.32 -end);
54.33 + Pretty.strs ("type code generators:" :: map fst tycodegens)])
54.34 + end;
54.35
54.36 -val _ = Context.add_setup CodegenData.init;
54.37 -val print_codegens = CodegenData.print;
54.38
54.39
54.40 (**** access parameters for random testing ****)
55.1 --- a/src/Pure/compress.ML Sun May 06 21:50:17 2007 +0200
55.2 +++ b/src/Pure/compress.ML Mon May 07 00:49:59 2007 +0200
55.3 @@ -21,8 +21,7 @@
55.4 (* theory data *)
55.5
55.6 structure CompressData = TheoryDataFun
55.7 -(struct
55.8 - val name = "Pure/compress";
55.9 +(
55.10 type T = typ Typtab.table ref * term Termtab.table ref;
55.11 val empty : T = (ref Typtab.empty, ref Termtab.empty);
55.12 fun copy (ref typs, ref terms) : T = (ref typs, ref terms);
55.13 @@ -30,8 +29,7 @@
55.14 fun merge _ ((ref typs1, ref terms1), (ref typs2, ref terms2)) : T =
55.15 (ref (Typtab.merge (K true) (typs1, typs2)),
55.16 ref (Termtab.merge (K true) (terms1, terms2)));
55.17 - fun print _ _ = ();
55.18 -end);
55.19 +);
55.20
55.21 val init_data = CompressData.init;
55.22
56.1 --- a/src/Pure/display.ML Sun May 06 21:50:17 2007 +0200
56.2 +++ b/src/Pure/display.ML Mon May 07 00:49:59 2007 +0200
56.3 @@ -234,9 +234,6 @@
56.4 val rests = restricts |> map (apfst (apfst extern_const)) |> sort_wrt (#1 o #1);
56.5 in
56.6 [Pretty.strs ("names:" :: Context.names_of thy)] @
56.7 - (if verbose then
56.8 - [Pretty.strs ("theory data:" :: Context.theory_data_of thy),
56.9 - Pretty.strs ("proof data:" :: Context.proof_data_of thy)] else []) @
56.10 [Pretty.strs ["name prefix:", NameSpace.path_of naming],
56.11 Pretty.big_list "classes:" (map pretty_classrel clsses),
56.12 pretty_default default,
57.1 --- a/src/Pure/proofterm.ML Sun May 06 21:50:17 2007 +0200
57.2 +++ b/src/Pure/proofterm.ML Mon May 07 00:49:59 2007 +0200
57.3 @@ -110,8 +110,6 @@
57.4 (string * (typ list -> proof -> proof option)) list -> proof -> proof
57.5 val rewrite_proof_notypes : (proof * proof) list *
57.6 (string * (typ list -> proof -> proof option)) list -> proof -> proof
57.7 - val init_data: theory -> theory
57.8 -
57.9 end
57.10
57.11 structure Proofterm : PROOFTERM =
57.12 @@ -1178,10 +1176,8 @@
57.13 (**** theory data ****)
57.14
57.15 structure ProofData = TheoryDataFun
57.16 -(struct
57.17 - val name = "Pure/proof";
57.18 - type T = ((proof * proof) list *
57.19 - (string * (typ list -> proof -> proof option)) list);
57.20 +(
57.21 + type T = (proof * proof) list * (string * (typ list -> proof -> proof option)) list;
57.22
57.23 val empty = ([], []);
57.24 val copy = I;
57.25 @@ -1189,10 +1185,7 @@
57.26 fun merge _ ((rules1, procs1) : T, (rules2, procs2)) =
57.27 (Library.merge (op =) (rules1, rules2),
57.28 AList.merge (op =) (K true) (procs1, procs2));
57.29 - fun print _ _ = ();
57.30 -end);
57.31 -
57.32 -val init_data = ProofData.init;
57.33 +);
57.34
57.35 fun add_prf_rrule r = (ProofData.map o apfst) (insert (op =) r);
57.36
58.1 --- a/src/Pure/pure_thy.ML Sun May 06 21:50:17 2007 +0200
58.2 +++ b/src/Pure/pure_thy.ML Mon May 07 00:49:59 2007 +0200
58.3 @@ -152,7 +152,6 @@
58.4
58.5 structure TheoremsData = TheoryDataFun
58.6 (struct
58.7 - val name = "Pure/theorems";
58.8 type T =
58.9 {theorems: thm list NameSpace.table,
58.10 index: FactIndex.T} ref;
58.11 @@ -505,9 +504,6 @@
58.12 val proto_pure =
58.13 Context.pre_pure_thy
58.14 |> Compress.init_data
58.15 - |> Sign.init_data
58.16 - |> Theory.init_data
58.17 - |> Proofterm.init_data
58.18 |> TheoremsData.init
58.19 |> Sign.add_types
58.20 [("fun", 2, NoSyn),
59.1 --- a/src/Pure/sign.ML Sun May 06 21:50:17 2007 +0200
59.2 +++ b/src/Pure/sign.ML Mon May 07 00:49:59 2007 +0200
59.3 @@ -60,7 +60,6 @@
59.4
59.5 signature SIGN =
59.6 sig
59.7 - val init_data: theory -> theory
59.8 val rep_sg: theory ->
59.9 {naming: NameSpace.naming,
59.10 syn: Syntax.syntax,
59.11 @@ -203,8 +202,7 @@
59.12 Sign {naming = naming, syn = syn, tsig = tsig, consts = consts};
59.13
59.14 structure SignData = TheoryDataFun
59.15 -(struct
59.16 - val name = "Pure/sign";
59.17 +(
59.18 type T = sign;
59.19 val copy = I;
59.20 fun extend (Sign {syn, tsig, consts, ...}) =
59.21 @@ -223,11 +221,7 @@
59.22 val tsig = Type.merge_tsigs pp (tsig1, tsig2);
59.23 val consts = Consts.merge (consts1, consts2);
59.24 in make_sign (naming, syn, tsig, consts) end;
59.25 -
59.26 - fun print _ _ = ();
59.27 -end);
59.28 -
59.29 -val init_data = SignData.init;
59.30 +);
59.31
59.32 fun rep_sg thy = SignData.get thy |> (fn Sign args => args);
59.33
60.1 --- a/src/Pure/simplifier.ML Sun May 06 21:50:17 2007 +0200
60.2 +++ b/src/Pure/simplifier.ML Mon May 07 00:49:59 2007 +0200
60.3 @@ -97,19 +97,16 @@
60.4 (* global simpsets *)
60.5
60.6 structure GlobalSimpset = TheoryDataFun
60.7 -(struct
60.8 - val name = "Pure/simpset";
60.9 +(
60.10 type T = simpset ref;
60.11 -
60.12 val empty = ref empty_ss;
60.13 - fun copy (ref ss) = ref ss: T; (*create new reference!*)
60.14 + fun copy (ref ss) = ref ss: T;
60.15 fun extend (ref ss) = ref (MetaSimplifier.inherit_context empty_ss ss);
60.16 fun merge _ (ref ss1, ref ss2) = ref (merge_ss (ss1, ss2));
60.17 - fun print _ (ref ss) = print_ss ss;
60.18 -end);
60.19 +);
60.20
60.21 val _ = Context.add_setup GlobalSimpset.init;
60.22 -val print_simpset = GlobalSimpset.print;
60.23 +fun print_simpset thy = print_ss (! (GlobalSimpset.get thy));
60.24 val get_simpset = ! o GlobalSimpset.get;
60.25
60.26 val change_simpset_of = change o GlobalSimpset.get;
60.27 @@ -133,15 +130,12 @@
60.28 (* local simpsets *)
60.29
60.30 structure LocalSimpset = ProofDataFun
60.31 -(struct
60.32 - val name = "Pure/simpset";
60.33 +(
60.34 type T = simpset;
60.35 val init = get_simpset;
60.36 - fun print _ ss = print_ss ss;
60.37 -end);
60.38 +);
60.39
60.40 -val _ = Context.add_setup LocalSimpset.init;
60.41 -val print_local_simpset = LocalSimpset.print;
60.42 +val print_local_simpset = print_ss o LocalSimpset.get;
60.43 val get_local_simpset = LocalSimpset.get;
60.44 val put_local_simpset = LocalSimpset.put;
60.45
60.46 @@ -181,15 +175,12 @@
60.47
60.48 structure Simprocs = GenericDataFun
60.49 (
60.50 - val name = "Pure/simprocs";
60.51 type T = simproc NameSpace.table;
60.52 val empty = NameSpace.empty_table;
60.53 val extend = I;
60.54 fun merge _ simprocs = NameSpace.merge_tables eq_simproc simprocs
60.55 handle Symtab.DUPS ds => err_dup_simprocs ds;
60.56 - fun print _ _ = ();
60.57 );
60.58 -val _ = Context.add_setup Simprocs.init;
60.59
60.60
60.61 (* get simprocs *)
61.1 --- a/src/Pure/theory.ML Sun May 06 21:50:17 2007 +0200
61.2 +++ b/src/Pure/theory.ML Mon May 07 00:49:59 2007 +0200
61.3 @@ -21,7 +21,6 @@
61.4 val end_theory: theory -> theory
61.5 val checkpoint: theory -> theory
61.6 val copy: theory -> theory
61.7 - val init_data: theory -> theory
61.8 val rep_theory: theory ->
61.9 {axioms: term NameSpace.table,
61.10 defs: Defs.T,
61.11 @@ -101,8 +100,7 @@
61.12 fun err_dup_oras dups = error ("Duplicate oracle(s): " ^ commas_quote dups);
61.13
61.14 structure ThyData = TheoryDataFun
61.15 -(struct
61.16 - val name = "Pure/theory";
61.17 +(
61.18 type T = thy;
61.19 val empty = make_thy (NameSpace.empty_table, Defs.empty, NameSpace.empty_table);
61.20 val copy = I;
61.21 @@ -119,11 +117,7 @@
61.22 val oracles = NameSpace.merge_tables (eq_snd (op =)) (oracles1, oracles2)
61.23 handle Symtab.DUPS dups => err_dup_oras dups;
61.24 in make_thy (axioms, defs, oracles) end;
61.25 -
61.26 - fun print _ _ = ();
61.27 -end);
61.28 -
61.29 -val init_data = ThyData.init;
61.30 +);
61.31
61.32 fun rep_theory thy = ThyData.get thy |> (fn Thy args => args);
61.33
62.1 --- a/src/Pure/variable.ML Sun May 06 21:50:17 2007 +0200
62.2 +++ b/src/Pure/variable.ML Mon May 07 00:49:59 2007 +0200
62.3 @@ -79,15 +79,11 @@
62.4
62.5 structure Data = ProofDataFun
62.6 (
62.7 - val name = "Pure/variable";
62.8 type T = data;
62.9 fun init thy =
62.10 make_data (false, Name.context, [], Vartab.empty, Symtab.empty, (Vartab.empty, Vartab.empty));
62.11 - fun print _ _ = ();
62.12 );
62.13
62.14 -val _ = Context.add_setup Data.init;
62.15 -
62.16 fun map_data f =
62.17 Data.map (fn Data {is_body, names, fixes, binds, type_occs, constraints} =>
62.18 make_data (f (is_body, names, fixes, binds, type_occs, constraints)));
63.1 --- a/src/ZF/Tools/ind_cases.ML Sun May 06 21:50:17 2007 +0200
63.2 +++ b/src/ZF/Tools/ind_cases.ML Mon May 07 00:49:59 2007 +0200
63.3 @@ -19,16 +19,13 @@
63.4 (* theory data *)
63.5
63.6 structure IndCasesData = TheoryDataFun
63.7 -(struct
63.8 - val name = "ZF/ind_cases";
63.9 +(
63.10 type T = (simpset -> cterm -> thm) Symtab.table;
63.11 -
63.12 val empty = Symtab.empty;
63.13 val copy = I;
63.14 val extend = I;
63.15 fun merge _ tabs : T = Symtab.merge (K true) tabs;
63.16 - fun print _ _ = ();
63.17 -end);
63.18 +);
63.19
63.20
63.21 fun declare name f = IndCasesData.map (Symtab.update (name, f));
63.22 @@ -72,9 +69,8 @@
63.23 (* package setup *)
63.24
63.25 val setup =
63.26 - (IndCasesData.init #>
63.27 - Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args,
63.28 - "dynamic case analysis on sets")]);
63.29 + Method.add_methods
63.30 + [("ind_cases", mk_cases_meth oo mk_cases_args, "dynamic case analysis on sets")];
63.31
63.32
63.33 (* outer syntax *)
64.1 --- a/src/ZF/Tools/induct_tacs.ML Sun May 06 21:50:17 2007 +0200
64.2 +++ b/src/ZF/Tools/induct_tacs.ML Mon May 07 00:49:59 2007 +0200
64.3 @@ -31,19 +31,14 @@
64.4 exhaustion : thm};
64.5
64.6 structure DatatypesData = TheoryDataFun
64.7 -(struct
64.8 - val name = "ZF/datatypes";
64.9 +(
64.10 type T = datatype_info Symtab.table;
64.11 -
64.12 val empty = Symtab.empty;
64.13 val copy = I;
64.14 val extend = I;
64.15 fun merge _ tabs : T = Symtab.merge (K true) tabs;
64.16 +);
64.17
64.18 - fun print thy tab =
64.19 - Pretty.writeln (Pretty.strs ("datatypes:" ::
64.20 - map #1 (NameSpace.extern_table (Sign.type_space thy, tab))));
64.21 -end);
64.22
64.23
64.24 (** Constructor information: needed to map constructors to datatypes **)
64.25 @@ -56,15 +51,13 @@
64.26
64.27
64.28 structure ConstructorsData = TheoryDataFun
64.29 -(struct
64.30 - val name = "ZF/constructors"
64.31 +(
64.32 type T = constructor_info Symtab.table
64.33 val empty = Symtab.empty
64.34 val copy = I;
64.35 val extend = I
64.36 fun merge _ tabs: T = Symtab.merge (K true) tabs;
64.37 - fun print _ _= ();
64.38 -end);
64.39 +);
64.40
64.41 structure DatatypeTactics : DATATYPE_TACTICS =
64.42 struct
64.43 @@ -185,13 +178,11 @@
64.44 (* theory setup *)
64.45
64.46 val setup =
64.47 - (DatatypesData.init #>
64.48 - ConstructorsData.init #>
64.49 Method.add_methods
64.50 [("induct_tac", Method.goal_args Args.name induct_tac,
64.51 "induct_tac emulation (dynamic instantiation!)"),
64.52 ("case_tac", Method.goal_args Args.name exhaust_tac,
64.53 - "datatype case_tac emulation (dynamic instantiation!)")]);
64.54 + "datatype case_tac emulation (dynamic instantiation!)")];
64.55
64.56
64.57 (* outer syntax *)
65.1 --- a/src/ZF/Tools/typechk.ML Sun May 06 21:50:17 2007 +0200
65.2 +++ b/src/ZF/Tools/typechk.ML Mon May 07 00:49:59 2007 +0200
65.3 @@ -44,7 +44,6 @@
65.4
65.5 structure Data = GenericDataFun
65.6 (
65.7 - val name = "ZF/type-checking";
65.8 type T = tcset
65.9 val empty = TC {rules = [], net = Net.empty};
65.10 val extend = I;
65.11 @@ -52,19 +51,19 @@
65.12 fun merge _ (TC {rules, net}, TC {rules = rules', net = net'}) =
65.13 TC {rules = Drule.merge_rules (rules, rules'),
65.14 net = Net.merge Thm.eq_thm_prop (net, net')};
65.15 -
65.16 - fun print context (TC {rules, ...}) =
65.17 - Pretty.writeln (Pretty.big_list "type-checking rules:"
65.18 - (map (ProofContext.pretty_thm (Context.proof_of context)) rules));
65.19 );
65.20
65.21 -val print_tcset = Data.print o Context.Proof;
65.22 -
65.23 val TC_add = Thm.declaration_attribute (Data.map o add_rule);
65.24 val TC_del = Thm.declaration_attribute (Data.map o del_rule);
65.25
65.26 val tcset_of = Data.get o Context.Proof;
65.27
65.28 +fun print_tcset ctxt =
65.29 + let val TC {rules, ...} = tcset_of ctxt in
65.30 + Pretty.writeln (Pretty.big_list "type-checking rules:"
65.31 + (map (ProofContext.pretty_thm ctxt) rules))
65.32 + end;
65.33 +
65.34
65.35 (* tactics *)
65.36
65.37 @@ -128,7 +127,6 @@
65.38 (* theory setup *)
65.39
65.40 val setup =
65.41 - Data.init #>
65.42 Attrib.add_attributes [("TC", TC_att, "declaration of type-checking rule")] #>
65.43 Method.add_methods [("typecheck", typecheck_meth, "ZF type-checking")] #>
65.44 (fn thy => (change_simpset_of thy (fn ss => ss setSolver type_solver); thy));