--- a/src/CCL/Wfd.thy Sun May 06 21:50:17 2007 +0200
+++ b/src/CCL/Wfd.thy Mon May 07 00:49:59 2007 +0200
@@ -500,12 +500,10 @@
structure Data = GenericDataFun
(
- val name = "CCL/eval";
type T = thm list;
val empty = [];
val extend = I;
fun merge _ = Drule.merge_rules;
- fun print _ _ = ();
);
in
@@ -518,7 +516,6 @@
DEPTH_SOLVE_1 (resolve_tac (ths @ prems @ Data.get (Context.Proof ctxt)) 1)) 1;
val eval_setup =
- Data.init #>
Attrib.add_attributes
[("eval", Attrib.add_del_args eval_add eval_del, "declaration of evaluation rule")] #>
Method.add_methods [("eval", Method.thms_ctxt_args (fn ths => fn ctxt =>
--- a/src/HOL/Algebra/ringsimp.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Algebra/ringsimp.ML Mon May 07 00:49:59 2007 +0200
@@ -20,9 +20,8 @@
fun struct_eq ((s1: string, ts1), (s2, ts2)) =
(s1 = s2) andalso eq_list (op aconv) (ts1, ts2);
-structure AlgebraData = GenericDataFun
-(struct
- val name = "Algebra/algebra";
+structure Data = GenericDataFun
+(
type T = ((string * term list) * thm list) list;
(* Algebraic structures:
identifier of the structure, list of operations and simp rules,
@@ -30,20 +29,16 @@
val empty = [];
val extend = I;
fun merge _ = AList.join struct_eq (K (Library.merge Thm.eq_thm_prop));
- fun print generic structs =
- let
- val ctxt = Context.proof_of generic;
- val pretty_term = Pretty.quote o ProofContext.pretty_term ctxt;
- fun pretty_struct ((s, ts), _) = Pretty.block
- [Pretty.str s, Pretty.str ":", Pretty.brk 1,
- Pretty.enclose "(" ")" (Pretty.breaks (map pretty_term ts))];
- in
- Pretty.big_list "Algebraic structures:" (map pretty_struct structs) |>
- Pretty.writeln
- end
-end);
+);
-val print_structures = AlgebraData.print o Context.Proof;
+fun print_structures ctxt =
+ let
+ val structs = Data.get (Context.Proof ctxt);
+ val pretty_term = Pretty.quote o ProofContext.pretty_term ctxt;
+ fun pretty_struct ((s, ts), _) = Pretty.block
+ [Pretty.str s, Pretty.str ":", Pretty.brk 1,
+ Pretty.enclose "(" ")" (Pretty.breaks (map pretty_term ts))];
+ in Pretty.writeln (Pretty.big_list "Algebraic structures:" (map pretty_struct structs)) end;
(** Method **)
@@ -57,17 +52,17 @@
in asm_full_simp_tac (HOL_ss settermless less addsimps simps) end;
fun algebra_tac ctxt =
- EVERY' (map (fn s => TRY o struct_tac s) (AlgebraData.get (Context.Proof ctxt)));
+ EVERY' (map (fn s => TRY o struct_tac s) (Data.get (Context.Proof ctxt)));
(** Attribute **)
fun add_struct_thm s =
Thm.declaration_attribute
- (fn thm => AlgebraData.map (AList.map_default struct_eq (s, []) (insert Thm.eq_thm_prop thm)));
+ (fn thm => Data.map (AList.map_default struct_eq (s, []) (insert Thm.eq_thm_prop thm)));
fun del_struct s =
Thm.declaration_attribute
- (fn _ => AlgebraData.map (AList.delete struct_eq s));
+ (fn _ => Data.map (AList.delete struct_eq s));
val attribute = Attrib.syntax
(Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon ||
@@ -79,7 +74,6 @@
(** Setup **)
val setup =
- AlgebraData.init #>
Method.add_methods [("algebra", Method.ctxt_args (Method.SIMPLE_METHOD' o algebra_tac),
"normalisation of algebraic structure")] #>
Attrib.add_attributes [("algebra", attribute, "theorems controlling algebra method")];
--- a/src/HOL/Hyperreal/transfer.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Hyperreal/transfer.ML Mon May 07 00:49:59 2007 +0200
@@ -16,8 +16,7 @@
struct
structure TransferData = GenericDataFun
-(struct
- val name = "HOL/transfer";
+(
type T = {
intros: thm list,
unfolds: thm list,
@@ -35,8 +34,7 @@
unfolds = Drule.merge_rules (unfolds1, unfolds2),
refolds = Drule.merge_rules (refolds1, refolds2),
consts = Library.merge (op =) (consts1, consts2)} : T;
- fun print _ _ = ();
-end);
+);
val transfer_start = thm "transfer_start"
@@ -109,7 +107,6 @@
{intros=intros, unfolds=unfolds, refolds=refolds, consts=c::consts}))
val setup =
- TransferData.init #>
Attrib.add_attributes
[("transfer_intro", Attrib.add_del_args intro_add intro_del,
"declaration of transfer introduction rule"),
--- a/src/HOL/Import/hol4rews.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Import/hol4rews.ML Mon May 07 00:49:59 2007 +0200
@@ -12,102 +12,70 @@
| Generating of string
| Replaying of string
-structure HOL4DefThyArgs: THEORY_DATA_ARGS =
-struct
-val name = "HOL4/import_status"
-type T = ImportStatus
-val empty = NoImport
-val copy = I
-val extend = I
-fun merge _ (NoImport,NoImport) = NoImport
- | merge _ _ = (warning "Import status set during merge"; NoImport)
-fun print _ import_status =
- Pretty.writeln (Pretty.str (case import_status of NoImport => "No current import" | Generating thyname => ("Generating " ^ thyname) | Replaying thyname => ("Replaying " ^ thyname)))
-end;
-
-structure HOL4DefThy = TheoryDataFun(HOL4DefThyArgs);
+structure HOL4DefThy = TheoryDataFun
+(
+ type T = ImportStatus
+ val empty = NoImport
+ val copy = I
+ val extend = I
+ fun merge _ (NoImport,NoImport) = NoImport
+ | merge _ _ = (warning "Import status set during merge"; NoImport)
+)
-structure ImportSegmentArgs: THEORY_DATA_ARGS =
-struct
-val name = "HOL4/import_segment"
-type T = string
-val empty = ""
-val copy = I
-val extend = I
-fun merge _ ("",arg) = arg
- | merge _ (arg,"") = arg
- | merge _ (s1,s2) =
- if s1 = s2
- then s1
- else error "Trying to merge two different import segments"
-fun print _ import_segment =
- Pretty.writeln (Pretty.str ("Import segment: " ^ import_segment))
-end;
-
-structure ImportSegment = TheoryDataFun(ImportSegmentArgs);
+structure ImportSegment = TheoryDataFun
+(
+ type T = string
+ val empty = ""
+ val copy = I
+ val extend = I
+ fun merge _ ("",arg) = arg
+ | merge _ (arg,"") = arg
+ | merge _ (s1,s2) =
+ if s1 = s2
+ then s1
+ else error "Trying to merge two different import segments"
+)
val get_import_segment = ImportSegment.get
val set_import_segment = ImportSegment.put
-structure HOL4UNamesArgs: THEORY_DATA_ARGS =
-struct
-val name = "HOL4/used_names"
-type T = string list
-val empty = []
-val copy = I
-val extend = I
-fun merge _ ([],[]) = []
- | merge _ _ = error "Used names not empty during merge"
-fun print _ used_names =
- Pretty.writeln (Pretty.str "Printing of HOL4/used_names Not implemented")
-end;
-
-structure HOL4UNames = TheoryDataFun(HOL4UNamesArgs);
-
-structure HOL4DumpArgs: THEORY_DATA_ARGS =
-struct
-val name = "HOL4/dump_data"
-type T = string * string * string list
-val empty = ("","",[])
-val copy = I
-val extend = I
-fun merge _ (("","",[]),("","",[])) = ("","",[])
- | merge _ _ = error "Dump data not empty during merge"
-fun print _ dump_data =
- Pretty.writeln (Pretty.str "Printing of HOL4/dump_data Not implemented")
-end;
-
-structure HOL4Dump = TheoryDataFun(HOL4DumpArgs);
+structure HOL4UNames = TheoryDataFun
+(
+ type T = string list
+ val empty = []
+ val copy = I
+ val extend = I
+ fun merge _ ([],[]) = []
+ | merge _ _ = error "Used names not empty during merge"
+)
-structure HOL4MovesArgs: THEORY_DATA_ARGS =
-struct
-val name = "HOL4/moves"
-type T = string Symtab.table
-val empty = Symtab.empty
-val copy = I
-val extend = I
-fun merge _ : T * T -> T = Symtab.merge (K true)
-fun print _ tab =
- Pretty.writeln (Pretty.big_list "HOL4 moves:"
- (Symtab.fold (fn (bef, aft) => fn xl => (Pretty.str (bef ^ " --> " ^ aft) :: xl)) tab []))
-end;
-
-structure HOL4Moves = TheoryDataFun(HOL4MovesArgs);
+structure HOL4Dump = TheoryDataFun
+(
+ type T = string * string * string list
+ val empty = ("","",[])
+ val copy = I
+ val extend = I
+ fun merge _ (("","",[]),("","",[])) = ("","",[])
+ | merge _ _ = error "Dump data not empty during merge"
+)
-structure HOL4ImportsArgs: THEORY_DATA_ARGS =
-struct
-val name = "HOL4/imports"
-type T = string Symtab.table
-val empty = Symtab.empty
-val copy = I
-val extend = I
-fun merge _ : T * T -> T = Symtab.merge (K true)
-fun print _ tab =
- Pretty.writeln (Pretty.big_list "HOL4 imports:"
- (Symtab.fold (fn (thyname, segname) => fn xl => (Pretty.str (thyname ^ " imported from segment " ^ segname) :: xl)) tab []))
-end;
+structure HOL4Moves = TheoryDataFun
+(
+ type T = string Symtab.table
+ val empty = Symtab.empty
+ val copy = I
+ val extend = I
+ fun merge _ : T * T -> T = Symtab.merge (K true)
+)
-structure HOL4Imports = TheoryDataFun(HOL4ImportsArgs);
+structure HOL4Imports = TheoryDataFun
+(
+ type T = string Symtab.table
+ val empty = Symtab.empty
+ val copy = I
+ val extend = I
+ fun merge _ : T * T -> T = Symtab.merge (K true)
+)
fun get_segment2 thyname thy =
Symtab.lookup (HOL4Imports.get thy) thyname
@@ -120,143 +88,86 @@
HOL4Imports.put imps' thy
end
-structure HOL4CMovesArgs: THEORY_DATA_ARGS =
-struct
-val name = "HOL4/constant_moves"
-type T = string Symtab.table
-val empty = Symtab.empty
-val copy = I
-val extend = I
-fun merge _ : T * T -> T = Symtab.merge (K true)
-fun print _ tab =
- Pretty.writeln (Pretty.big_list "HOL4 constant moves:"
- (Symtab.fold (fn (bef, aft) => fn xl => (Pretty.str (bef ^ " --> " ^ aft) :: xl)) tab []))
-end;
-
-structure HOL4CMoves = TheoryDataFun(HOL4CMovesArgs);
+structure HOL4CMoves = TheoryDataFun
+(
+ type T = string Symtab.table
+ val empty = Symtab.empty
+ val copy = I
+ val extend = I
+ fun merge _ : T * T -> T = Symtab.merge (K true)
+)
-structure HOL4MapsArgs: THEORY_DATA_ARGS =
-struct
-val name = "HOL4/mappings"
-type T = (string option) StringPair.table
-val empty = StringPair.empty
-val copy = I
-val extend = I
-fun merge _ : T * T -> T = StringPair.merge (K true)
-fun print _ tab =
- Pretty.writeln (Pretty.big_list "HOL4 mappings:"
- (StringPair.fold (fn ((bthy, bthm), isathm) => fn xl =>
- (Pretty.str (bthy ^ "." ^ bthm ^ (case isathm of SOME th => " --> " ^ th | NONE => "IGNORED")) :: xl)) tab []))
-end;
-
-structure HOL4Maps = TheoryDataFun(HOL4MapsArgs);
+structure HOL4Maps = TheoryDataFun
+(
+ type T = (string option) StringPair.table
+ val empty = StringPair.empty
+ val copy = I
+ val extend = I
+ fun merge _ : T * T -> T = StringPair.merge (K true)
+)
-structure HOL4ThmsArgs: THEORY_DATA_ARGS =
-struct
-val name = "HOL4/theorems"
-type T = holthm StringPair.table
-val empty = StringPair.empty
-val copy = I
-val extend = I
-fun merge _ : T * T -> T = StringPair.merge (K true)
-fun print _ tab =
- Pretty.writeln (Pretty.big_list "HOL4 mappings:"
- (StringPair.fold (fn ((bthy, bthm), (_, thm)) => fn xl => (Pretty.str (bthy ^ "." ^ bthm ^ ":") :: Display.pretty_thm thm :: xl)) tab []))
-end;
-
-structure HOL4Thms = TheoryDataFun(HOL4ThmsArgs);
+structure HOL4Thms = TheoryDataFun
+(
+ type T = holthm StringPair.table
+ val empty = StringPair.empty
+ val copy = I
+ val extend = I
+ fun merge _ : T * T -> T = StringPair.merge (K true)
+)
-structure HOL4ConstMapsArgs: THEORY_DATA_ARGS =
-struct
-val name = "HOL4/constmappings"
-type T = (bool * string * typ option) StringPair.table
-val empty = StringPair.empty
-val copy = I
-val extend = I
-fun merge _ : T * T -> T = StringPair.merge (K true)
-fun print _ tab =
- Pretty.writeln (Pretty.big_list "HOL4 constant mappings:"
- (StringPair.fold (fn ((bthy, bconst), (internal, isaconst, _)) => fn xl =>
- (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ isaconst ^ (if internal then " (*)" else "")) :: xl)) tab []))
-end;
-
-structure HOL4ConstMaps = TheoryDataFun(HOL4ConstMapsArgs);
+structure HOL4ConstMaps = TheoryDataFun
+(
+ type T = (bool * string * typ option) StringPair.table
+ val empty = StringPair.empty
+ val copy = I
+ val extend = I
+ fun merge _ : T * T -> T = StringPair.merge (K true)
+)
-structure HOL4RenameArgs: THEORY_DATA_ARGS =
-struct
-val name = "HOL4/renamings"
-type T = string StringPair.table
-val empty = StringPair.empty
-val copy = I
-val extend = I
-fun merge _ : T * T -> T = StringPair.merge (K true)
-fun print _ tab =
- Pretty.writeln (Pretty.big_list "HOL4 constant renamings:"
- (StringPair.fold (fn ((bthy,bconst),newname) => fn xl => (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ newname)::xl)) tab []))
-end;
-
-structure HOL4Rename = TheoryDataFun(HOL4RenameArgs);
+structure HOL4Rename = TheoryDataFun
+(
+ type T = string StringPair.table
+ val empty = StringPair.empty
+ val copy = I
+ val extend = I
+ fun merge _ : T * T -> T = StringPair.merge (K true)
+)
-structure HOL4DefMapsArgs: THEORY_DATA_ARGS =
-struct
-val name = "HOL4/def_maps"
-type T = string StringPair.table
-val empty = StringPair.empty
-val copy = I
-val extend = I
-fun merge _ : T * T -> T = StringPair.merge (K true)
-fun print _ tab =
- Pretty.writeln (Pretty.big_list "HOL4 constant definitions:"
- (StringPair.fold (fn ((bthy,bconst),newname) => fn xl => (Pretty.str (bthy ^ "." ^ bconst ^ ": " ^ newname)::xl)) tab []))
-end;
-
-structure HOL4DefMaps = TheoryDataFun(HOL4DefMapsArgs);
+structure HOL4DefMaps = TheoryDataFun
+(
+ type T = string StringPair.table
+ val empty = StringPair.empty
+ val copy = I
+ val extend = I
+ fun merge _ : T * T -> T = StringPair.merge (K true)
+)
-structure HOL4TypeMapsArgs: THEORY_DATA_ARGS =
-struct
-val name = "HOL4/typemappings"
-type T = (bool * string) StringPair.table
-val empty = StringPair.empty
-val copy = I
-val extend = I
-fun merge _ : T * T -> T = StringPair.merge (K true)
-fun print _ tab =
- Pretty.writeln (Pretty.big_list "HOL4 type mappings:"
- (StringPair.fold (fn ((bthy, bconst), (internal, isaconst)) => fn xl =>
- (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ isaconst ^ (if internal then " (*)" else "")) :: xl)) tab []))
-end;
-
-structure HOL4TypeMaps = TheoryDataFun(HOL4TypeMapsArgs);
+structure HOL4TypeMaps = TheoryDataFun
+(
+ type T = (bool * string) StringPair.table
+ val empty = StringPair.empty
+ val copy = I
+ val extend = I
+ fun merge _ : T * T -> T = StringPair.merge (K true)
+)
-structure HOL4PendingArgs: THEORY_DATA_ARGS =
-struct
-val name = "HOL4/pending"
-type T = ((term * term) list * thm) StringPair.table
-val empty = StringPair.empty
-val copy = I
-val extend = I
-fun merge _ : T * T -> T = StringPair.merge (K true)
-fun print _ tab =
- Pretty.writeln (Pretty.big_list "HOL4 pending theorems:"
- (StringPair.fold (fn ((bthy,bthm),(_,th)) => fn xl => (Pretty.chunks [Pretty.str (bthy ^ "." ^ bthm ^ ":"),Display.pretty_thm th]::xl)) tab []))
-end;
-
-structure HOL4Pending = TheoryDataFun(HOL4PendingArgs);
+structure HOL4Pending = TheoryDataFun
+(
+ type T = ((term * term) list * thm) StringPair.table
+ val empty = StringPair.empty
+ val copy = I
+ val extend = I
+ fun merge _ : T * T -> T = StringPair.merge (K true)
+)
-structure HOL4RewritesArgs: THEORY_DATA_ARGS =
-struct
-val name = "HOL4/rewrites"
-type T = thm list
-val empty = []
-val copy = I
-val extend = I
-fun merge _ = Library.gen_union Thm.eq_thm
-fun print _ thms =
- Pretty.writeln (Pretty.big_list "HOL4 rewrite rules:"
- (map Display.pretty_thm thms))
-end;
-
-structure HOL4Rewrites = TheoryDataFun(HOL4RewritesArgs);
+structure HOL4Rewrites = TheoryDataFun
+(
+ type T = thm list
+ val empty = []
+ val copy = I
+ val extend = I
+ fun merge _ = Library.gen_union Thm.eq_thm
+)
val hol4_debug = ref false
fun message s = if !hol4_debug then writeln s else ()
@@ -677,7 +588,7 @@
| _ => error "hol4rews.set_used_names called on initialized data!"
end
-val clear_used_names = HOL4UNames.put HOL4UNamesArgs.empty
+val clear_used_names = HOL4UNames.put [];
fun get_defmap thyname const thy =
let
@@ -737,21 +648,6 @@
|> add_hol4_const_mapping "min" "@" false "Hilbert_Choice.Eps"
in
val hol4_setup =
- HOL4Rewrites.init #>
- HOL4Maps.init #>
- HOL4UNames.init #>
- HOL4DefMaps.init #>
- HOL4Moves.init #>
- HOL4CMoves.init #>
- HOL4ConstMaps.init #>
- HOL4Rename.init #>
- HOL4TypeMaps.init #>
- HOL4Pending.init #>
- HOL4Thms.init #>
- HOL4Dump.init #>
- HOL4DefThy.init #>
- HOL4Imports.init #>
- ImportSegment.init #>
initial_maps #>
Attrib.add_attributes
[("hol4rew", Attrib.no_args add_hol4_rewrite, "HOL4 rewrite rule")]
--- a/src/HOL/Import/import_package.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Import/import_package.ML Mon May 07 00:49:59 2007 +0200
@@ -10,18 +10,14 @@
val debug : bool ref
end
-structure ImportDataArgs: THEORY_DATA_ARGS =
-struct
-val name = "HOL4/import_data"
-type T = ProofKernel.thm option array option
-val empty = NONE
-val copy = I
-val extend = I
-fun merge _ _ = NONE
-fun print _ _ = ()
-end
-
-structure ImportData = TheoryDataFun(ImportDataArgs)
+structure ImportData = TheoryDataFun
+(
+ type T = ProofKernel.thm option array option
+ val empty = NONE
+ val copy = I
+ val extend = I
+ fun merge _ _ = NONE
+)
structure ImportPackage :> IMPORT_PACKAGE =
struct
@@ -80,6 +76,6 @@
Method.SIMPLE_METHOD (import_tac arg thy)
end)
-val setup = Method.add_method("import",import_meth,"Import HOL4 theorem") #> ImportData.init
+val setup = Method.add_method("import",import_meth,"Import HOL4 theorem")
end
--- a/src/HOL/Import/shuffler.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Import/shuffler.ML Mon May 07 00:49:59 2007 +0200
@@ -75,20 +75,18 @@
| _ => raise THM("Not an equality",0,[th]))
handle _ => raise THM("Couldn't make object equality",0,[th])
-structure ShuffleDataArgs: THEORY_DATA_ARGS =
-struct
-val name = "HOL/shuffles"
-type T = thm list
-val empty = []
-val copy = I
-val extend = I
-fun merge _ = Library.gen_union Thm.eq_thm
-fun print _ thms =
- Pretty.writeln (Pretty.big_list "Shuffle theorems:"
- (map Display.pretty_thm thms))
-end
+structure ShuffleData = TheoryDataFun
+(
+ type T = thm list
+ val empty = []
+ val copy = I
+ val extend = I
+ fun merge _ = Library.gen_union Thm.eq_thm
+)
-structure ShuffleData = TheoryDataFun(ShuffleDataArgs)
+fun print_shuffles thy =
+ Pretty.writeln (Pretty.big_list "Shuffle theorems:"
+ (map Display.pretty_thm (ShuffleData.get thy)))
val weaken =
let
@@ -667,8 +665,6 @@
Method.SIMPLE_METHOD' (gen_shuffle_tac thy true (map (pair "premise") prems))
end
-val print_shuffles = ShuffleData.print
-
fun add_shuffle_rule thm thy =
let
val shuffles = ShuffleData.get thy
@@ -682,9 +678,10 @@
val shuffle_attr = Thm.declaration_attribute (fn th => Context.mapping (add_shuffle_rule th) I);
val setup =
- Method.add_method ("shuffle_tac",Method.thms_ctxt_args shuffle_meth,"solve goal by shuffling terms around") #>
- Method.add_method ("search_tac",Method.ctxt_args search_meth,"search for suitable theorems") #>
- ShuffleData.init #>
+ Method.add_method ("shuffle_tac",
+ Method.thms_ctxt_args shuffle_meth,"solve goal by shuffling terms around") #>
+ Method.add_method ("search_tac",
+ Method.ctxt_args search_meth,"search for suitable theorems") #>
add_shuffle_rule weaken #>
add_shuffle_rule equiv_comm #>
add_shuffle_rule imp_comm #>
--- a/src/HOL/Inductive.thy Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Inductive.thy Mon May 07 00:49:59 2007 +0200
@@ -118,7 +118,6 @@
use "Tools/datatype_realizer.ML"
use "Tools/datatype_hooks.ML"
-setup DatatypeHooks.setup
use "Tools/datatype_package.ML"
setup DatatypePackage.setup
--- a/src/HOL/Nominal/Nominal.thy Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Nominal/Nominal.thy Mon May 07 00:49:59 2007 +0200
@@ -3226,7 +3226,6 @@
(* setup for the individial atom-kinds *)
(* and nominal datatypes *)
use "nominal_atoms.ML"
-setup "NominalAtoms.setup"
(************************************************************)
(* various tactics for analysing permutations, supports etc *)
@@ -3288,7 +3287,6 @@
(************************************************)
(* main file for constructing nominal datatypes *)
use "nominal_package.ML"
-setup "NominalPackage.setup"
(******************************************************)
(* primitive recursive functions on nominal datatypes *)
--- a/src/HOL/Nominal/nominal_atoms.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Mon May 07 00:49:59 2007 +0200
@@ -13,7 +13,6 @@
val get_atom_info : theory -> string -> atom_info option
val atoms_of : theory -> string list
val mk_permT : typ -> typ
- val setup : theory -> theory
end
structure NominalAtoms : NOMINAL_ATOMS =
@@ -23,27 +22,21 @@
val Collect_const = thm "Collect_const";
-(* data kind 'HOL/nominal' *)
+(* theory data *)
type atom_info =
{pt_class : string,
fs_class : string,
cp_classes : (string * string) list};
-structure NominalArgs =
-struct
- val name = "HOL/nominal";
+structure NominalData = TheoryDataFun
+(
type T = atom_info Symtab.table;
-
val empty = Symtab.empty;
val copy = I;
val extend = I;
fun merge _ x = Symtab.merge (K true) x;
-
- fun print sg tab = ();
-end;
-
-structure NominalData = TheoryDataFun(NominalArgs);
+);
fun make_atom_info ((pt_class, fs_class), cp_classes) =
{pt_class = pt_class,
@@ -889,6 +882,4 @@
val _ = OuterSyntax.add_parsers [atom_declP];
-val setup = NominalData.init;
-
end;
--- a/src/HOL/Nominal/nominal_package.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Nominal/nominal_package.ML Mon May 07 00:49:59 2007 +0200
@@ -17,7 +17,6 @@
val perm_of_pair: term * term -> term
val mk_not_sym: thm list -> thm list
val perm_simproc: simproc
- val setup: theory -> theory
end
structure NominalPackage : NOMINAL_PACKAGE =
@@ -68,7 +67,7 @@
end;
-(* data kind 'HOL/nominal_datatypes' *)
+(* theory data *)
type descr = (int * (string * dtyp list * (string * (dtyp list * dtyp) list) list)) list;
@@ -83,25 +82,19 @@
inject : thm list};
structure NominalDatatypesData = TheoryDataFun
-(struct
- val name = "HOL/nominal_datatypes";
+(
type T = nominal_datatype_info Symtab.table;
-
val empty = Symtab.empty;
val copy = I;
val extend = I;
fun merge _ tabs : T = Symtab.merge (K true) tabs;
-
- fun print sg tab =
- Pretty.writeln (Pretty.strs ("nominal datatypes:" ::
- map #1 (NameSpace.extern_table (Sign.type_space sg, tab))));
-end);
+);
val get_nominal_datatypes = NominalDatatypesData.get;
val put_nominal_datatypes = NominalDatatypesData.put;
val map_nominal_datatypes = NominalDatatypesData.map;
val get_nominal_datatype = Symtab.lookup o get_nominal_datatypes;
-val setup = NominalDatatypesData.init;
+
(**** make datatype info ****)
--- a/src/HOL/Nominal/nominal_thmdecls.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML Mon May 07 00:49:59 2007 +0200
@@ -1,13 +1,13 @@
(* ID: "$Id$"
Authors: Julien Narboux and Christian Urban
- This file introduces the infrastructure for the lemma
+ This file introduces the infrastructure for the lemma
declaration "eqvts" "bijs" and "freshs".
- By attaching [eqvt] [bij] or [fresh] to a lemma, the lemma gets stored
+ By attaching [eqvt] [bij] or [fresh] to a lemma, the lemma gets stored
in a data-slot in the theory context. Possible modifiers
are [attribute add] and [attribute del] for adding and deleting,
- respectively the lemma from the data-slot.
+ respectively the lemma from the data-slot.
*)
signature NOMINAL_THMDECLS =
@@ -21,7 +21,7 @@
val get_eqvt_thms: theory -> thm list
val get_fresh_thms: theory -> thm list
val get_bij_thms: theory -> thm list
-
+
val NOMINAL_EQVT_DEBUG : bool ref
end;
@@ -31,24 +31,12 @@
structure Data = GenericDataFun
(
- val name = "HOL/Nominal/eqvt";
type T = {eqvts:thm list, freshs:thm list, bijs:thm list};
val empty = ({eqvts=[], freshs=[], bijs=[]}:T);
val extend = I;
- fun merge _ (r1:T,r2:T) = {eqvts = Drule.merge_rules (#eqvts r1, #eqvts r2),
- freshs = Drule.merge_rules (#freshs r1, #freshs r2),
+ fun merge _ (r1:T,r2:T) = {eqvts = Drule.merge_rules (#eqvts r1, #eqvts r2),
+ freshs = Drule.merge_rules (#freshs r1, #freshs r2),
bijs = Drule.merge_rules (#bijs r1, #bijs r2)}
- fun print context (data:T) =
- let
- fun print_aux msg thms =
- Pretty.writeln (Pretty.big_list msg
- (map (ProofContext.pretty_thm (Context.proof_of context)) thms))
- in
- (print_aux "Equivariance lemmas: " (#eqvts data);
- print_aux "Freshness lemmas: " (#freshs data);
- print_aux "Bijection lemmas: " (#bijs data))
- end;
-
);
(* Exception for when a theorem does not conform with form of an equivariance lemma. *)
@@ -62,7 +50,19 @@
(* eqality-lemma can be derived. *)
exception EQVT_FORM of string;
-val print_data = Data.print o Context.Proof;
+fun print_data ctxt =
+ let
+ val data = Data.get (Context.Proof ctxt);
+ fun pretty_thms msg thms =
+ Pretty.big_list msg (map (ProofContext.pretty_thm ctxt) thms);
+ in
+ Pretty.writeln (Pretty.chunks
+ [pretty_thms "Equivariance lemmas:" (#eqvts data),
+ pretty_thms "Freshness lemmas:" (#freshs data),
+ pretty_thms "Bijection lemmas:" (#bijs data)])
+ end;
+
+
val get_eqvt_thms = Context.Theory #> Data.get #> #eqvts;
val get_fresh_thms = Context.Theory #> Data.get #> #freshs;
val get_bij_thms = Context.Theory #> Data.get #> #bijs;
@@ -75,56 +75,56 @@
val NOMINAL_EQVT_DEBUG = ref false;
-fun tactic (msg,tac) =
- if !NOMINAL_EQVT_DEBUG
+fun tactic (msg,tac) =
+ if !NOMINAL_EQVT_DEBUG
then (EVERY [tac, print_tac ("after "^msg)])
- else tac
+ else tac
fun dynamic_thms thy name = PureThy.get_thms thy (Name name)
-fun tactic_eqvt ctx orig_thm pi typi =
- let
+fun tactic_eqvt ctx orig_thm pi typi =
+ let
val mypi = Thm.cterm_of ctx (Var (pi,typi))
val mypifree = Thm.cterm_of ctx (Const ("List.rev",typi --> typi) $ Free (fst pi,typi))
val perm_pi_simp = dynamic_thms ctx "perm_pi_simp"
in
- EVERY [tactic ("iffI applied",rtac iffI 1),
- tactic ("simplifies with orig_thm and perm_bool",
- asm_full_simp_tac (HOL_basic_ss addsimps [perm_bool,orig_thm]) 1),
+ EVERY [tactic ("iffI applied",rtac iffI 1),
+ tactic ("simplifies with orig_thm and perm_bool",
+ asm_full_simp_tac (HOL_basic_ss addsimps [perm_bool,orig_thm]) 1),
tactic ("applies orig_thm instantiated with rev pi",
- dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm) 1),
+ dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm) 1),
tactic ("getting rid of all remaining perms",
- full_simp_tac (HOL_basic_ss addsimps (perm_bool::perm_pi_simp)) 1)]
+ full_simp_tac (HOL_basic_ss addsimps (perm_bool::perm_pi_simp)) 1)]
end;
fun get_derived_thm thy hyp concl orig_thm pi typi =
- let
+ let
val lhs = (Const("Nominal.perm", typi --> HOLogic.boolT --> HOLogic.boolT) $ Var(pi,typi) $ hyp)
- val goal_term = Logic.unvarify (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,concl)))
- val _ = Display.print_cterm (cterm_of thy goal_term)
+ val goal_term = Logic.unvarify (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,concl)))
+ val _ = Display.print_cterm (cterm_of thy goal_term)
in
- Goal.prove_global thy [] [] goal_term (fn _ => (tactic_eqvt thy orig_thm pi typi))
+ Goal.prove_global thy [] [] goal_term (fn _ => (tactic_eqvt thy orig_thm pi typi))
end
(* FIXME: something naughty here, but as long as there is no infrastructure to expose *)
(* the eqvt_thm_list to the user, we have to manually update the context and the *)
(* thm-list eqvt *)
fun update_context flag thms context =
- let
- val context' = fold (fn thm => Data.map (flag thm)) thms context
- in
+ let
+ val context' = fold (fn thm => Data.map (flag thm)) thms context
+ in
Context.mapping (snd o PureThy.add_thmss [(("eqvts",(#eqvts (Data.get context'))),[])]) I context'
end;
-(* replaces every variable x in t with pi o x *)
+(* replaces every variable x in t with pi o x *)
fun apply_pi trm (pi,typi) =
- let
+ let
fun only_vars t =
(case t of
Var (n,ty) => (Const ("Nominal.perm",typi --> ty --> ty) $ (Var (pi,typi)) $ (Var (n,ty)))
| _ => t)
- in
- map_aterms only_vars trm
+ in
+ map_aterms only_vars trm
end;
(* returns *the* pi which is in front of all variables, provided there *)
@@ -132,69 +132,69 @@
fun get_pi t thy =
let fun get_pi_aux s =
(case s of
- (Const ("Nominal.perm",typrm) $
- (Var (pi,typi as Type("List.list",[Type ("*",[Type (tyatm,[]),_])]))) $
- (Var (n,ty))) =>
+ (Const ("Nominal.perm",typrm) $
+ (Var (pi,typi as Type("List.list",[Type ("*",[Type (tyatm,[]),_])]))) $
+ (Var (n,ty))) =>
let
(* FIXME: this should be an operation the library *)
- val class_name = (NameSpace.map_base (fn s => "pt_"^s) tyatm)
- in
- if (Type.of_sort (Sign.tsig_of thy) (ty,[class_name]))
- then [(pi,typi)]
- else raise
- EQVT_FORM ("Could not find any permutation or an argument is not an instance of "^class_name)
- end
+ val class_name = (NameSpace.map_base (fn s => "pt_"^s) tyatm)
+ in
+ if (Type.of_sort (Sign.tsig_of thy) (ty,[class_name]))
+ then [(pi,typi)]
+ else raise
+ EQVT_FORM ("Could not find any permutation or an argument is not an instance of "^class_name)
+ end
| Abs (_,_,t1) => get_pi_aux t1
| (t1 $ t2) => get_pi_aux t1 @ get_pi_aux t2
- | _ => [])
- in
+ | _ => [])
+ in
(* collect first all pi's in front of variables in t and then use distinct *)
(* to ensure that all pi's must have been the same, i.e. distinct returns *)
(* a singleton-list *)
- (case (distinct (op =) (get_pi_aux t)) of
+ (case (distinct (op =) (get_pi_aux t)) of
[(pi,typi)] => (pi,typi)
| _ => raise EQVT_FORM "All permutation should be the same")
end;
(* Either adds a theorem (orig_thm) to or deletes one from the equivaraince *)
(* lemma list depending on flag. To be added the lemma has to satisfy a *)
-(* certain form. *)
+(* certain form. *)
fun eqvt_add_del_aux flag orig_thm context =
- let
+ let
val thy = Context.theory_of context
val thms_to_be_added = (case (prop_of orig_thm) of
- (* case: eqvt-lemma is of the implicational form *)
+ (* case: eqvt-lemma is of the implicational form *)
(Const("==>", _) $ (Const ("Trueprop",_) $ hyp) $ (Const ("Trueprop",_) $ concl)) =>
- let
+ let
val (pi,typi) = get_pi concl thy
in
if (apply_pi hyp (pi,typi) = concl)
- then
+ then
(warning ("equivariance lemma of the relational form");
[orig_thm, get_derived_thm thy hyp concl orig_thm pi typi])
else raise EQVT_FORM "Type Implication"
end
- (* case: eqvt-lemma is of the equational form *)
- | (Const ("Trueprop", _) $ (Const ("op =", _) $
+ (* case: eqvt-lemma is of the equational form *)
+ | (Const ("Trueprop", _) $ (Const ("op =", _) $
(Const ("Nominal.perm",typrm) $ Var (pi,typi) $ lhs) $ rhs)) =>
- (if (apply_pi lhs (pi,typi)) = rhs
+ (if (apply_pi lhs (pi,typi)) = rhs
then [orig_thm]
else raise EQVT_FORM "Type Equality")
| _ => raise EQVT_FORM "Type unknown")
- in
+ in
update_context flag thms_to_be_added context
end
- handle EQVT_FORM s =>
+ handle EQVT_FORM s =>
error (string_of_thm orig_thm ^ " does not comply with the form of an equivariance lemma ("^s^").")
(* in cases of bij- and freshness, we just add the lemmas to the *)
-(* data-slot *)
+(* data-slot *)
-fun simple_add_del_aux record_access name flag th context =
- let
+fun simple_add_del_aux record_access name flag th context =
+ let
val context' = Data.map (flag th) context
in
- Context.mapping (snd o PureThy.add_thmss [((name,(record_access (Data.get context'))),[])]) I context'
+ Context.mapping (snd o PureThy.add_thmss [((name,(record_access (Data.get context'))),[])]) I context'
end
fun bij_add_del_aux f = simple_add_del_aux #bijs "bijs" f
@@ -205,21 +205,20 @@
fun fresh_map f th (r:Data.T) = {eqvts = #eqvts r, freshs = (f th (#freshs r)), bijs = #bijs r};
fun bij_map f th (r:Data.T) = {eqvts = #eqvts r, freshs = #freshs r, bijs = (f th (#bijs r))};
-val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.add_rule));
-val eqvt_del = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.del_rule));
-val eqvt_force_add = Thm.declaration_attribute (eqvt_force_add_del_aux (eqvt_map Drule.add_rule));
-val eqvt_force_del = Thm.declaration_attribute (eqvt_force_add_del_aux (eqvt_map Drule.del_rule));
+val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.add_rule));
+val eqvt_del = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.del_rule));
+val eqvt_force_add = Thm.declaration_attribute (eqvt_force_add_del_aux (eqvt_map Drule.add_rule));
+val eqvt_force_del = Thm.declaration_attribute (eqvt_force_add_del_aux (eqvt_map Drule.del_rule));
-val bij_add = Thm.declaration_attribute (bij_add_del_aux (bij_map Drule.add_rule));
+val bij_add = Thm.declaration_attribute (bij_add_del_aux (bij_map Drule.add_rule));
val bij_del = Thm.declaration_attribute (bij_add_del_aux (bij_map Drule.del_rule));
-val fresh_add = Thm.declaration_attribute (fresh_add_del_aux (fresh_map Drule.add_rule));
+val fresh_add = Thm.declaration_attribute (fresh_add_del_aux (fresh_map Drule.add_rule));
val fresh_del = Thm.declaration_attribute (fresh_add_del_aux (fresh_map Drule.del_rule));
val setup =
- Data.init #>
- Attrib.add_attributes
+ Attrib.add_attributes
[("eqvt", Attrib.add_del_args eqvt_add eqvt_del, "equivariance theorem declaration"),
("eqvt_force", Attrib.add_del_args eqvt_force_add eqvt_force_del,
"equivariance theorem declaration (without checking the form of the lemma)"),
@@ -227,11 +226,3 @@
("bij", Attrib.add_del_args bij_add bij_del, "bijection theorem declaration")];
end;
-
-(* Thm.declaration_attribute has type (thm -> Context.generic -> Context.generic) -> attribute *)
-
-(* Drule.add_rule has type thm -> thm list -> thm list *)
-
-(* Data.map has type thm list -> thm list -> Context.generic -> Context.generic *)
-
-(* add_del_args is of type attribute -> attribute -> src -> attribute *)
\ No newline at end of file
--- a/src/HOL/Predicate.thy Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Predicate.thy Mon May 07 00:49:59 2007 +0200
@@ -152,14 +152,12 @@
val rules2 = [split_set, mk_meta_eq mem_Collect_eq, mem_Collect2_eq];
structure PredSetConvData = GenericDataFun
-(struct
- val name = "HOL/pred_set_conv";
+(
type T = thm list;
val empty = [];
val extend = I;
fun merge _ = Drule.merge_rules;
- fun print _ _ = ()
-end)
+);
fun mk_attr ths1 ths2 f = Attrib.syntax (Attrib.thms >> (fn ths =>
Thm.rule_attribute (fn ctxt => rew ths1 (map (f o Simpdata.mk_eq)
@@ -170,7 +168,7 @@
in
-val _ = ML_Context.>> (PredSetConvData.init #>
+val _ = ML_Context.>> (
Attrib.add_attributes
[("pred_set_conv", pred_set_conv_att,
"declare rules for converting between predicate and set notation"),
--- a/src/HOL/Tools/datatype_hooks.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Tools/datatype_hooks.ML Mon May 07 00:49:59 2007 +0200
@@ -7,49 +7,29 @@
signature DATATYPE_HOOKS =
sig
- type hook = string list -> theory -> theory;
- val add: hook -> theory -> theory;
- val all: hook;
- val setup: theory -> theory;
+ type hook = string list -> theory -> theory
+ val add: hook -> theory -> theory
+ val all: hook
end;
structure DatatypeHooks : DATATYPE_HOOKS =
struct
-
-(* theory data *)
-
type hook = string list -> theory -> theory;
-datatype T = T of (serial * hook) list;
-
-fun map_T f (T hooks) = T (f hooks);
-fun merge_T pp (T hooks1, T hooks2) =
- T (AList.merge (op =) (K true) (hooks1, hooks2));
structure DatatypeHooksData = TheoryDataFun
-(struct
- val name = "HOL/datatype_hooks";
- type T = T;
- val empty = T [];
+(
+ type T = (serial * hook) list;
+ val empty = [];
val copy = I;
val extend = I;
- val merge = merge_T;
- fun print _ _ = ();
-end);
-
-
-(* interface *)
+ fun merge _ hooks : T = AList.merge (op =) (K true) hooks;
+);
fun add hook =
- DatatypeHooksData.map (map_T (cons (serial (), hook)));
+ DatatypeHooksData.map (cons (serial (), hook));
fun all dtcos thy =
- fold (fn (_, f) => f dtcos) ((fn T hooks => hooks) (DatatypeHooksData.get thy)) thy;
-
-
-(* theory setup *)
-
-val setup = DatatypeHooksData.init;
+ fold (fn (_, f) => f dtcos) (DatatypeHooksData.get thy) thy;
end;
-
--- a/src/HOL/Tools/datatype_package.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Tools/datatype_package.ML Mon May 07 00:49:59 2007 +0200
@@ -85,11 +85,10 @@
val quiet_mode = quiet_mode;
-(* data kind 'HOL/datatypes' *)
+(* theory data *)
structure DatatypesData = TheoryDataFun
-(struct
- val name = "HOL/datatypes";
+(
type T =
{types: datatype_info Symtab.table,
constrs: datatype_info Symtab.table,
@@ -105,15 +104,14 @@
{types = Symtab.merge (K true) (types1, types2),
constrs = Symtab.merge (K true) (constrs1, constrs2),
cases = Symtab.merge (K true) (cases1, cases2)};
-
- fun print sg ({types, ...} : T) =
- Pretty.writeln (Pretty.strs ("datatypes:" ::
- map #1 (NameSpace.extern_table (Sign.type_space sg, types))));
-end);
+);
val get_datatypes = #types o DatatypesData.get;
val map_datatypes = DatatypesData.map;
-val print_datatypes = DatatypesData.print;
+
+fun print_datatypes thy =
+ Pretty.writeln (Pretty.strs ("datatypes:" ::
+ map #1 (NameSpace.extern_table (Sign.type_space thy, get_datatypes thy))));
(** theory information about datatypes **)
@@ -933,7 +931,7 @@
(* setup theory *)
val setup =
- DatatypesData.init #> Method.add_methods tactic_emulations #> simproc_setup #> trfun_setup;
+ Method.add_methods tactic_emulations #> simproc_setup #> trfun_setup;
(* outer syntax *)
--- a/src/HOL/Tools/function_package/fundef_common.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML Mon May 07 00:49:59 2007 +0200
@@ -78,30 +78,24 @@
end
structure FundefData = GenericDataFun
-(struct
- val name = "HOL/function_def/data";
- type T = (term * fundef_context_data) NetRules.T
-
+(
+ type T = (term * fundef_context_data) NetRules.T;
val empty = NetRules.init
(op aconv o pairself fst : (term * fundef_context_data) * (term * fundef_context_data) -> bool)
fst;
val copy = I;
val extend = I;
fun merge _ (tab1, tab2) = NetRules.merge (tab1, tab2)
-
- fun print _ _ = ();
-end);
+);
structure FundefCongs = GenericDataFun
-(struct
- val name = "HOL/function_def/congs"
- type T = thm list
- val empty = []
- val extend = I
- fun merge _ = Drule.merge_rules
- fun print _ _ = ()
-end);
+(
+ type T = thm list
+ val empty = []
+ val extend = I
+ fun merge _ = Drule.merge_rules
+);
(* Generally useful?? *)
@@ -143,14 +137,12 @@
structure TerminationRule = GenericDataFun
-(struct
- val name = "HOL/function_def/termination"
- type T = thm list
- val empty = []
- val extend = I
- fun merge _ = Drule.merge_rules
- fun print _ _ = ()
-end);
+(
+ type T = thm list
+ val empty = []
+ val extend = I
+ fun merge _ = Drule.merge_rules
+);
val get_termination_rules = TerminationRule.get
val store_termination_rule = TerminationRule.map o cons
--- a/src/HOL/Tools/function_package/fundef_package.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML Mon May 07 00:49:59 2007 +0200
@@ -208,13 +208,11 @@
(* setup *)
val setup =
- FundefData.init
- #> FundefCongs.init
- #> TerminationRule.init
- #> Attrib.add_attributes
- [("fundef_cong", Attrib.add_del_args cong_add cong_del, "declaration of congruence rule for function definitions")]
- #> setup_case_cong_hook
- #> FundefRelation.setup
+ Attrib.add_attributes
+ [("fundef_cong", Attrib.add_del_args cong_add cong_del,
+ "declaration of congruence rule for function definitions")]
+ #> setup_case_cong_hook
+ #> FundefRelation.setup
val get_congs = FundefCommon.get_fundef_congs o Context.Theory
--- a/src/HOL/Tools/inductive_codegen.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Mon May 07 00:49:59 2007 +0200
@@ -22,8 +22,7 @@
Symtab.join (fn _ => AList.merge (Thm.eq_thm_prop) (K true)) tabs;
structure CodegenData = TheoryDataFun
-(struct
- val name = "HOL/inductive_codegen";
+(
type T =
{intros : (thm * (string * int)) list Symtab.table,
graph : unit Graph.T,
@@ -37,8 +36,7 @@
{intros = merge_rules (intros1, intros2),
graph = Graph.merge (K true) (graph1, graph2),
eqns = merge_rules (eqns1, eqns2)};
- fun print _ _ = ();
-end);
+);
fun warn thm = warning ("InductiveCodegen: Not a proper clause:\n" ^
@@ -653,7 +651,6 @@
val setup =
add_codegen "inductive" inductive_codegen #>
- CodegenData.init #>
add_attribute "ind" (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) --
Scan.option (Args.$$$ "params" |-- Args.colon |-- Args.nat) >> uncurry add);
--- a/src/HOL/Tools/inductive_package.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Tools/inductive_package.ML Mon May 07 00:49:59 2007 +0200
@@ -86,7 +86,7 @@
-(** theory data **)
+(** context data **)
type inductive_result =
{preds: term list, defs: thm list, elims: thm list, raw_induct: thm,
@@ -106,28 +106,25 @@
{names: string list, coind: bool} * inductive_result;
structure InductiveData = GenericDataFun
-(struct
- val name = "HOL/inductive";
+(
type T = inductive_info Symtab.table * thm list;
-
val empty = (Symtab.empty, []);
val extend = I;
fun merge _ ((tab1, monos1), (tab2, monos2)) =
(Symtab.merge (K true) (tab1, tab2), Drule.merge_rules (monos1, monos2));
-
- fun print context (tab, monos) =
- let
- val ctxt = Context.proof_of context;
- val space = Consts.space_of (ProofContext.consts_of ctxt);
- in
- [Pretty.strs ("(co)inductives:" :: map #1 (NameSpace.extern_table (space, tab))),
- Pretty.big_list "monotonicity rules:" (map (ProofContext.pretty_thm ctxt) monos)]
- |> Pretty.chunks |> Pretty.writeln
- end;
-end);
+);
val get_inductives = InductiveData.get o Context.Proof;
-val print_inductives = InductiveData.print o Context.Proof;
+
+fun print_inductives ctxt =
+ let
+ val (tab, monos) = get_inductives ctxt;
+ val space = Consts.space_of (ProofContext.consts_of ctxt);
+ in
+ [Pretty.strs ("(co)inductives:" :: map #1 (NameSpace.extern_table (space, tab))),
+ Pretty.big_list "monotonicity rules:" (map (ProofContext.pretty_thm ctxt) monos)]
+ |> Pretty.chunks |> Pretty.writeln
+ end;
(* get and put data *)
@@ -156,7 +153,7 @@
(_ $ (_ $ (Const ("Not", _) $ _) $ _)) => []
| _ => [thm' RS (thm' RS eq_to_mono2)]);
fun dest_less_concl thm = dest_less_concl (thm RS le_funD)
- handle THM _ => thm RS le_boolD
+ handle THM _ => thm RS le_boolD
in
case concl of
Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq)
@@ -892,7 +889,6 @@
(* setup theory *)
val setup =
- InductiveData.init #>
Method.add_methods [("ind_cases2", ind_cases, (* FIXME "ind_cases" (?) *)
"dynamic case analysis on predicates")] #>
Attrib.add_attributes [("mono2", Attrib.add_del_args mono_add mono_del, (* FIXME "mono" *)
--- a/src/HOL/Tools/old_inductive_package.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Tools/old_inductive_package.ML Mon May 07 00:49:59 2007 +0200
@@ -37,7 +37,6 @@
{defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}) option
val the_mk_cases: theory -> string -> string -> thm
- val print_inductives: theory -> unit
val mono_add: attribute
val mono_del: attribute
val get_monos: theory -> thm list
@@ -88,27 +87,14 @@
induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm};
structure InductiveData = TheoryDataFun
-(struct
- val name = "HOL/inductive";
+(
type T = inductive_info Symtab.table * thm list;
-
val empty = (Symtab.empty, []);
val copy = I;
val extend = I;
fun merge _ ((tab1, monos1), (tab2, monos2)) =
(Symtab.merge (K true) (tab1, tab2), Drule.merge_rules (monos1, monos2));
-
- fun print thy (tab, monos) =
- [Pretty.strs ("(co)inductives:" ::
- map #1 (NameSpace.extern_table (Sign.const_space thy, tab))),
- Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_sg thy) monos)]
- |> Pretty.chunks |> Pretty.writeln;
-end);
-
-val print_inductives = InductiveData.print;
-
-
-(* get and put data *)
+);
val get_inductive = Symtab.lookup o #1 o InductiveData.get;
@@ -871,7 +857,6 @@
(* setup theory *)
val setup =
- InductiveData.init #>
Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args,
"dynamic case analysis on sets")] #>
Attrib.add_attributes [("mono", Attrib.add_del_args mono_add mono_del,
--- a/src/HOL/Tools/recdef_package.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Tools/recdef_package.ML Mon May 07 00:49:59 2007 +0200
@@ -8,7 +8,6 @@
signature RECDEF_PACKAGE =
sig
val quiet_mode: bool ref
- val print_recdefs: theory -> unit
val get_recdef: theory -> string
-> {simps: thm list, rules: thm list list, induct: thm, tcs: term list} option
val get_hints: Proof.context -> {simps: thm list, congs: (string * thm) list, wfs: thm list}
@@ -97,10 +96,8 @@
type recdef_info = {simps: thm list, rules: thm list list, induct: thm, tcs: term list};
structure GlobalRecdefData = TheoryDataFun
-(struct
- val name = "HOL/recdef";
+(
type T = recdef_info Symtab.table * hints;
-
val empty = (Symtab.empty, mk_hints ([], [], [])): T;
val copy = I;
val extend = I;
@@ -111,14 +108,7 @@
mk_hints (Drule.merge_rules (simps1, simps2),
AList.merge (op =) Thm.eq_thm (congs1, congs2),
Drule.merge_rules (wfs1, wfs2)));
-
- fun print thy (tab, hints) =
- (Pretty.strs ("recdefs:" :: map #1 (NameSpace.extern_table (Sign.const_space thy, tab))) ::
- pretty_hints hints) |> Pretty.chunks |> Pretty.writeln;
-end);
-
-val print_recdefs = GlobalRecdefData.print;
-
+);
val get_recdef = Symtab.lookup o #1 o GlobalRecdefData.get;
@@ -135,12 +125,10 @@
(* proof data *)
structure LocalRecdefData = ProofDataFun
-(struct
- val name = "HOL/recdef";
+(
type T = hints;
val init = get_global_hints;
- fun print _ hints = pretty_hints hints |> Pretty.chunks |> Pretty.writeln;
-end);
+);
val get_hints = LocalRecdefData.get;
fun map_hints f = Context.mapping (GlobalRecdefData.map (apsnd f)) (LocalRecdefData.map f);
@@ -297,8 +285,6 @@
(* setup theory *)
val setup =
- GlobalRecdefData.init #>
- LocalRecdefData.init #>
Attrib.add_attributes
[(recdef_simpN, Attrib.add_del_args simp_add simp_del, "declaration of recdef simp rule"),
(recdef_congN, Attrib.add_del_args cong_add cong_del, "declaration of recdef cong rule"),
--- a/src/HOL/Tools/recfun_codegen.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML Mon May 07 00:49:59 2007 +0200
@@ -18,15 +18,13 @@
open Codegen;
structure RecCodegenData = TheoryDataFun
-(struct
- val name = "HOL/recfun_codegen";
+(
type T = (thm * string option) list Symtab.table;
val empty = Symtab.empty;
val copy = I;
val extend = I;
fun merge _ = Symtab.merge_list (Thm.eq_thm_prop o pairself fst);
- fun print _ _ = ();
-end);
+);
val dest_eqn = HOLogic.dest_eq o HOLogic.dest_Trueprop;
@@ -172,7 +170,6 @@
val setup =
- RecCodegenData.init #>
add_codegen "recfun" recfun_codegen #>
add_attribute ""
(Args.del |-- Scan.succeed del
--- a/src/HOL/Tools/record_package.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Tools/record_package.ML Mon May 07 00:49:59 2007 +0200
@@ -243,7 +243,8 @@
fun make_parent_info name fields extension induct =
{name = name, fields = fields, extension = extension, induct = induct}: parent_info;
-(* data kind 'HOL/record' *)
+
+(* theory data *)
type record_data =
{records: record_info Symtab.table,
@@ -266,10 +267,8 @@
extfields = extfields, fieldext = fieldext }: record_data;
structure RecordsData = TheoryDataFun
-(struct
- val name = "HOL/record";
+(
type T = record_data;
-
val empty =
make_record_data Symtab.empty
{selectors = Symtab.empty, updates = Symtab.empty, simpset = HOL_basic_ss}
@@ -308,27 +307,26 @@
(splits1, splits2))
(Symtab.merge (K true) (extfields1,extfields2))
(Symtab.merge (K true) (fieldext1,fieldext2));
+);
- fun print thy ({records = recs, ...}: record_data) =
- let
- val prt_typ = Sign.pretty_typ thy;
-
- fun pretty_parent NONE = []
- | pretty_parent (SOME (Ts, name)) =
- [Pretty.block [prt_typ (Type (name, Ts)), Pretty.str " +"]];
+fun print_records thy =
+ let
+ val {records = recs, ...} = RecordsData.get thy;
+ val prt_typ = Sign.pretty_typ thy;
- fun pretty_field (c, T) = Pretty.block
- [Pretty.str (Sign.extern_const thy c), Pretty.str " ::",
- Pretty.brk 1, Pretty.quote (prt_typ T)];
+ fun pretty_parent NONE = []
+ | pretty_parent (SOME (Ts, name)) =
+ [Pretty.block [prt_typ (Type (name, Ts)), Pretty.str " +"]];
- fun pretty_record (name, {args, parent, fields, ...}: record_info) =
- Pretty.block (Pretty.fbreaks (Pretty.block
- [prt_typ (Type (name, map TFree args)), Pretty.str " = "] ::
- pretty_parent parent @ map pretty_field fields));
- in map pretty_record (Symtab.dest recs) |> Pretty.chunks |> Pretty.writeln end;
-end);
+ fun pretty_field (c, T) = Pretty.block
+ [Pretty.str (Sign.extern_const thy c), Pretty.str " ::",
+ Pretty.brk 1, Pretty.quote (prt_typ T)];
-val print_records = RecordsData.print;
+ fun pretty_record (name, {args, parent, fields, ...}: record_info) =
+ Pretty.block (Pretty.fbreaks (Pretty.block
+ [prt_typ (Type (name, map TFree args)), Pretty.str " = "] ::
+ pretty_parent parent @ map pretty_field fields));
+ in map pretty_record (Symtab.dest recs) |> Pretty.chunks |> Pretty.writeln end;
(* access 'records' *)
@@ -343,6 +341,7 @@
sel_upd equalities extinjects extsplit splits extfields fieldext;
in RecordsData.put data thy end;
+
(* access 'sel_upd' *)
val get_sel_upd = #sel_upd o RecordsData.get;
@@ -365,6 +364,7 @@
equalities extinjects extsplit splits extfields fieldext;
in RecordsData.put data thy end;
+
(* access 'equalities' *)
fun add_record_equalities name thm thy =
@@ -378,18 +378,21 @@
val get_equalities =Symtab.lookup o #equalities o RecordsData.get;
+
(* access 'extinjects' *)
fun add_extinjects thm thy =
let
val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} =
RecordsData.get thy;
- val data = make_record_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects) extsplit
- splits extfields fieldext;
+ val data =
+ make_record_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects) extsplit
+ splits extfields fieldext;
in RecordsData.put data thy end;
val get_extinjects = rev o #extinjects o RecordsData.get;
+
(* access 'extsplit' *)
fun add_extsplit name thm thy =
@@ -2263,7 +2266,6 @@
(* setup theory *)
val setup =
- RecordsData.init #>
Theory.add_trfuns ([], parse_translation, [], []) #>
Theory.add_advanced_trfuns ([], adv_parse_translation, [], []) #>
(fn thy => (Simplifier.change_simpset_of thy
--- a/src/HOL/Tools/refute.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Tools/refute.ML Mon May 07 00:49:59 2007 +0200
@@ -186,9 +186,8 @@
};
- structure RefuteDataArgs =
- struct
- val name = "HOL/refute";
+ structure RefuteData = TheoryDataFun
+ (
type T =
{interpreters: (string * (theory -> model -> arguments -> Term.term ->
(interpretation * model * arguments) option)) list,
@@ -204,15 +203,7 @@
{interpreters = AList.merge (op =) (K true) (in1, in2),
printers = AList.merge (op =) (K true) (pr1, pr2),
parameters = Symtab.merge (op=) (pa1, pa2)};
- fun print sg {interpreters, printers, parameters} =
- Pretty.writeln (Pretty.chunks
- [Pretty.strs ("default parameters:" :: List.concat (map
- (fn (name, value) => [name, "=", value]) (Symtab.dest parameters))),
- Pretty.strs ("interpreters:" :: map fst interpreters),
- Pretty.strs ("printers:" :: map fst printers)]);
- end;
-
- structure RefuteData = TheoryDataFun(RefuteDataArgs);
+ );
(* ------------------------------------------------------------------------- *)
@@ -3210,7 +3201,6 @@
(* (theory -> theory) list *)
val setup =
- RefuteData.init #>
add_interpreter "stlc" stlc_interpreter #>
add_interpreter "Pure" Pure_interpreter #>
add_interpreter "HOLogic" HOLogic_interpreter #>
--- a/src/HOL/Tools/res_atpset.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Tools/res_atpset.ML Mon May 07 00:49:59 2007 +0200
@@ -18,24 +18,22 @@
structure Data = GenericDataFun
(
- val name = "HOL/atpset";
type T = thm list;
val empty = [];
val extend = I;
fun merge _ = Drule.merge_rules;
- fun print context rules =
- Pretty.writeln (Pretty.big_list "ATP rules:"
- (map (ProofContext.pretty_thm (Context.proof_of context)) rules));
);
-val print_atpset = Data.print o Context.Proof;
val get_atpset = Data.get o Context.Proof;
+fun print_atpset ctxt =
+ Pretty.writeln (Pretty.big_list "ATP rules:"
+ (map (ProofContext.pretty_thm ctxt) (get_atpset ctxt)));
+
val atp_add = Thm.declaration_attribute (Data.map o Drule.add_rule);
val atp_del = Thm.declaration_attribute (Data.map o Drule.del_rule);
val setup =
- Data.init #>
Attrib.add_attributes [("atp", Attrib.add_del_args atp_add atp_del, "declaration of ATP rules")];
end;
--- a/src/HOL/Tools/res_axioms.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Tools/res_axioms.ML Mon May 07 00:49:59 2007 +0200
@@ -481,15 +481,13 @@
(SOME (to_nnf th, fake_name th) handle THM _ => NONE);
structure ThmCache = TheoryDataFun
-(struct
- val name = "ATP/thm_cache";
+(
type T = (thm list) Thmtab.table ref;
val empty : T = ref Thmtab.empty;
fun copy (ref tab) : T = ref tab;
val extend = copy;
fun merge _ (ref tab1, ref tab2) : T = ref (Thmtab.merge (K true) (tab1, tab2));
- fun print _ _ = ();
-end);
+);
(*The cache prevents repeated clausification of a theorem, and also repeated declaration of
Skolem functions. The global one holds theorems proved prior to this point. Theory data
--- a/src/HOL/Tools/typecopy_package.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Tools/typecopy_package.ML Mon May 07 00:49:59 2007 +0200
@@ -23,7 +23,7 @@
val add_hook: hook -> theory -> theory
val get_spec: theory -> string -> (string * sort) list * (string * typ list) list
val get_eq: theory -> string -> thm
- val print: theory -> unit
+ val print_typecopies: theory -> unit
val setup: theory -> theory
end;
@@ -44,33 +44,30 @@
type hook = string * info -> theory -> theory;
structure TypecopyData = TheoryDataFun
-(struct
- val name = "HOL/typecopy_package";
+(
type T = info Symtab.table * (serial * hook) list;
val empty = (Symtab.empty, []);
val copy = I;
val extend = I;
fun merge _ ((tab1, hooks1), (tab2, hooks2) : T) =
(Symtab.merge (K true) (tab1, tab2), AList.merge (op =) (K true) (hooks1, hooks2));
- fun print thy (tab, _) =
- let
- fun mk (tyco, { vs, constr, typ, proj = (proj, _), ... } : info) =
- (Pretty.block o Pretty.breaks) [
- Sign.pretty_typ thy (Type (tyco, map TFree vs)),
- Pretty.str "=",
- (Pretty.str o Sign.extern_const thy) constr,
- Sign.pretty_typ thy typ,
- Pretty.block [Pretty.str "(", (Pretty.str o Sign.extern_const thy) proj, Pretty.str ")"]
- ];
+);
+
+fun print_typecopies thy =
+ let
+ val (tab, _) = TypecopyData.get thy;
+ fun mk (tyco, { vs, constr, typ, proj = (proj, _), ... } : info) =
+ (Pretty.block o Pretty.breaks) [
+ Sign.pretty_typ thy (Type (tyco, map TFree vs)),
+ Pretty.str "=",
+ (Pretty.str o Sign.extern_const thy) constr,
+ Sign.pretty_typ thy typ,
+ Pretty.block [Pretty.str "(", (Pretty.str o Sign.extern_const thy) proj, Pretty.str ")"]];
in
- (Pretty.writeln o Pretty.block o Pretty.fbreaks) (
- Pretty.str "type copies:"
- :: map mk (Symtab.dest tab)
- )
+ (Pretty.writeln o Pretty.block o Pretty.fbreaks)
+ (Pretty.str "type copies:" :: map mk (Symtab.dest tab))
end;
-end);
-val print = TypecopyData.print;
val get_typecopies = Symtab.keys o fst o TypecopyData.get;
val get_typecopy_info = Symtab.lookup o fst o TypecopyData.get;
@@ -128,7 +125,7 @@
val add_typecopy = gen_add_typecopy Sign.certify_typ;
-end; (*local*)
+end;
(* equality function equation and datatype specification *)
@@ -147,8 +144,6 @@
fun add_project (_ , {proj_def, ...} : info) =
CodegenData.add_func true proj_def;
-val setup =
- TypecopyData.init
- #> add_hook add_project;
+val setup = add_hook add_project;
-end; (*struct*)
+end;
--- a/src/HOL/Tools/typedef_package.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Tools/typedef_package.ML Mon May 07 00:49:59 2007 +0200
@@ -24,7 +24,6 @@
* (string * string) option -> theory -> Proof.state
val typedef_i: (bool * string) * (bstring * string list * mixfix) * term
* (string * string) option -> theory -> Proof.state
- val setup: theory -> theory
end;
structure TypedefPackage: TYPEDEF_PACKAGE =
@@ -77,15 +76,13 @@
Abs_cases: thm, Rep_induct: thm, Abs_induct: thm};
structure TypedefData = TheoryDataFun
-(struct
- val name = "HOL/typedef";
+(
type T = info Symtab.table;
val empty = Symtab.empty;
val copy = I;
val extend = I;
fun merge _ tabs : T = Symtab.merge (K true) tabs;
- fun print _ _ = ();
-end);
+);
val get_info = Symtab.lookup o TypedefData.get;
fun put_info name info = TypedefData.map (Symtab.update (name, info));
@@ -270,8 +267,6 @@
end;
-val setup = TypedefData.init;
-
(** outer syntax **)
--- a/src/HOL/Typedef.thy Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Typedef.thy Mon May 07 00:49:59 2007 +0200
@@ -90,8 +90,7 @@
use "Tools/typedef_codegen.ML"
setup {*
- TypedefPackage.setup
- #> TypecopyPackage.setup
+ TypecopyPackage.setup
#> TypedefCodegen.setup
*}
--- a/src/HOL/arith_data.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/arith_data.ML Mon May 07 00:49:59 2007 +0200
@@ -206,8 +206,7 @@
fun eq_arith_tactic (ArithTactic {id = id1, ...}, ArithTactic {id = id2, ...}) = (id1 = id2);
structure ArithTheoryData = TheoryDataFun
-(struct
- val name = "HOL/arith";
+(
type T = {splits: thm list,
inj_consts: (string * typ) list,
discrete: string list,
@@ -221,8 +220,7 @@
inj_consts = Library.merge (op =) (inj_consts1, inj_consts2),
discrete = Library.merge (op =) (discrete1, discrete2),
tactics = Library.merge eq_arith_tactic (tactics1, tactics2)};
- fun print _ _ = ();
-end);
+);
val arith_split_add = Thm.declaration_attribute (fn thm =>
Context.mapping (ArithTheoryData.map (fn {splits,inj_consts,discrete,tactics} =>
@@ -922,7 +920,6 @@
Most of the work is done by the cancel tactics. *)
val init_lin_arith_data =
- Fast_Arith.setup #>
Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} =>
{add_mono_thms = add_mono_thms @
@{thms add_mono_thms_ordered_semiring} @ @{thms add_mono_thms_ordered_field},
@@ -940,7 +937,6 @@
addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]
(*abel_cancel helps it work in abstract algebraic domains*)
addsimprocs nat_cancel_sums_add}) #>
- ArithTheoryData.init #>
arith_discrete "nat";
val fast_nat_arith_simproc =
--- a/src/Provers/Arith/fast_lin_arith.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Mon May 07 00:49:59 2007 +0200
@@ -86,7 +86,6 @@
signature FAST_LIN_ARITH =
sig
- val setup: theory -> theory
val map_data: ({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
lessD: thm list, neqE: thm list, simpset: Simplifier.simpset}
-> {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
@@ -99,18 +98,15 @@
val cut_lin_arith_tac: simpset -> int -> tactic
end;
-functor Fast_Lin_Arith(structure LA_Logic:LIN_ARITH_LOGIC
+functor Fast_Lin_Arith(structure LA_Logic:LIN_ARITH_LOGIC
and LA_Data:LIN_ARITH_DATA) : FAST_LIN_ARITH =
struct
(** theory data **)
-(* data kind 'Provers/fast_lin_arith' *)
-
structure Data = TheoryDataFun
-(struct
- val name = "Provers/fast_lin_arith";
+(
type T = {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
lessD: thm list, neqE: thm list, simpset: Simplifier.simpset};
@@ -130,12 +126,9 @@
lessD = Drule.merge_rules (lessD1, lessD2),
neqE = Drule.merge_rules (neqE1, neqE2),
simpset = Simplifier.merge_ss (simpset1, simpset2)};
-
- fun print _ _ = ();
-end);
+);
val map_data = Data.map;
-val setup = Data.init;
@@ -424,7 +417,7 @@
local
exception FalseE of thm
in
-fun mkthm (sg:theory, ss:simpset) (asms:thm list) (just:injust) : thm =
+fun mkthm (sg:theory, ss) (asms:thm list) (just:injust) : thm =
let val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset, ...} =
Data.get sg;
val simpset' = Simplifier.inherit_context ss simpset;
@@ -503,7 +496,7 @@
fun integ(rlhs,r,rel,rrhs,s,d) =
let val (rn,rd) = Rat.quotient_of_rat r and (sn,sd) = Rat.quotient_of_rat s
val m = lcms(map (abs o snd o Rat.quotient_of_rat) (r :: s :: map snd rlhs @ map snd rrhs))
- fun mult(t,r) =
+ fun mult(t,r) =
let val (i,j) = Rat.quotient_of_rat r
in (t,i * (m div j)) end
in (m,(map mult rlhs, rn*(m div rd), rel, map mult rrhs, sn*(m div sd), d)) end
@@ -527,7 +520,7 @@
else lineq(c,Lt,diff,just)
| "~<" => lineq(~c,Le,map (op~) diff,NotLessD(just))
| "=" => lineq(c,Eq,diff,just)
- | _ => sys_error("mklineq" ^ rel)
+ | _ => sys_error("mklineq" ^ rel)
end;
(* ------------------------------------------------------------------------- *)
@@ -590,15 +583,9 @@
(* failure as soon as a case could not be refuted; i.e. delay further *)
(* splitting until after a refutation for other cases has been found. *)
-fun split_items sg (do_pre : bool) (Ts : typ list, terms : term list) :
+fun split_items sg (do_pre : bool) (Ts, terms) :
(typ list * (LA_Data.decompT * int) list) list =
let
-(*
- val _ = if !trace then
- trace_msg ("split_items: Ts = " ^ string_of_list (Sign.string_of_typ sg) Ts ^ "\n" ^
- " terms = " ^ string_of_list (Sign.string_of_term sg) terms)
- else ()
-*)
(* splits inequalities '~=' into '<' and '>'; this corresponds to *)
(* 'REPEAT_DETERM (eresolve_tac neqE i)' at the theorem/tactic *)
(* level *)
@@ -634,38 +621,14 @@
val result = (Ts, terms)
|> (* user-defined preprocessing of the subgoal *)
- (* (typ list * term list) list *)
(if do_pre then LA_Data.pre_decomp sg else Library.single)
- |> (* compute the internal encoding of (in-)equalities *)
- (* (typ list * (LA_Data.decompT option * bool) list) list *)
+ |> (* produce the internal encoding of (in-)equalities *)
map (apsnd (map (fn t => (LA_Data.decomp sg t, LA_Data.domain_is_nat t))))
|> (* splitting of inequalities *)
- (* (typ list * (LA_Data.decompT option * bool) list list) list *)
map (apsnd elim_neq)
- |> (* combine the list of lists of subgoals into a single list *)
- map (fn (Ts, subgoals) => map (pair Ts o map fst) subgoals)
- |> List.concat
+ |> maps (fn (Ts, subgoals) => map (pair Ts o map fst) subgoals)
|> (* numbering of hypotheses, ignoring irrelevant ones *)
map (apsnd (number_hyps 0))
-(*
- val _ = if !trace then
- trace_msg ("split_items: result has " ^ Int.toString (length result) ^
- " subgoal(s)" ^ "\n" ^ (cat_lines o fst) (fold_map (fn (Ts, items) => fn n =>
- (" " ^ Int.toString n ^ ". Ts = " ^
- string_of_list (Sign.string_of_typ sg) Ts ^ "\n" ^
- " items = " ^ string_of_list (string_of_pair
- (fn (l, i, rel, r, j, d) => enclose "(" ")" (commas
- [string_of_list
- (string_of_pair (Sign.string_of_term sg) Rat.string_of_rat) l,
- Rat.string_of_rat i,
- rel,
- string_of_list
- (string_of_pair (Sign.string_of_term sg) Rat.string_of_rat) r,
- Rat.string_of_rat j,
- Bool.toString d]))
- Int.toString) items, n+1)) result 1))
- else ()
-*)
in result end;
fun add_atoms (ats : term list, ((lhs,_,_,rhs,_,_) : LA_Data.decompT, _)) : term list =
@@ -742,7 +705,7 @@
refute sg params show_ex do_pre Hs'
end;
-fun refute_tac (ss : simpset) (i : int, justs : injust list) : tactic =
+fun refute_tac ss (i, justs) =
fn state =>
let val _ = trace_thm ("refute_tac (on subgoal " ^ Int.toString i ^ ", with " ^
Int.toString (length justs) ^ " justification(s)):") state
--- a/src/Provers/classical.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/Provers/classical.ML Mon May 07 00:49:59 2007 +0200
@@ -140,9 +140,9 @@
val add_context_unsafe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory
val del_context_unsafe_wrapper: string -> theory -> theory
val get_claset: theory -> claset
- val print_local_claset: Proof.context -> unit
val get_local_claset: Proof.context -> claset
val put_local_claset: claset -> Proof.context -> Proof.context
+ val print_local_claset: Proof.context -> unit
val safe_dest: int option -> attribute
val safe_elim: int option -> attribute
val safe_intro: int option -> attribute
@@ -857,19 +857,16 @@
(* global claset *)
structure GlobalClaset = TheoryDataFun
-(struct
- val name = "Provers/claset";
+(
type T = claset ref * context_cs;
-
val empty = (ref empty_cs, empty_context_cs);
fun copy (ref cs, ctxt_cs) = (ref cs, ctxt_cs): T;
val extend = copy;
fun merge _ ((ref cs1, ctxt_cs1), (ref cs2, ctxt_cs2)) =
(ref (merge_cs (cs1, cs2)), merge_context_cs (ctxt_cs1, ctxt_cs2));
- fun print _ (ref cs, _) = print_cs cs;
-end);
+);
-val print_claset = GlobalClaset.print;
+val print_claset = print_cs o ! o #1 o GlobalClaset.get;
val get_claset = ! o #1 o GlobalClaset.get;
val get_context_cs = #2 o GlobalClaset.get o ProofContext.theory_of;
@@ -912,20 +909,19 @@
(* local claset *)
structure LocalClaset = ProofDataFun
-(struct
- val name = "Provers/claset";
+(
type T = claset;
val init = get_claset;
- fun print ctxt cs = print_cs (context_cs ctxt cs (get_context_cs ctxt));
-end);
+);
-val print_local_claset = LocalClaset.print;
val get_local_claset = LocalClaset.get;
val put_local_claset = LocalClaset.put;
fun local_claset_of ctxt =
context_cs ctxt (get_local_claset ctxt) (get_context_cs ctxt);
+val print_local_claset = print_cs o local_claset_of;
+
(* attributes *)
@@ -1061,7 +1057,7 @@
(** theory setup **)
-val setup = GlobalClaset.init #> LocalClaset.init #> setup_attrs #> setup_methods;
+val setup = GlobalClaset.init #> setup_attrs #> setup_methods;
--- a/src/Pure/Isar/attrib.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/Isar/attrib.ML Mon May 07 00:49:59 2007 +0200
@@ -49,29 +49,24 @@
(* theory data *)
structure AttributesData = TheoryDataFun
-(struct
- val name = "Isar/attributes";
+(
type T = (((src -> attribute) * string) * stamp) NameSpace.table;
-
val empty = NameSpace.empty_table;
val copy = I;
val extend = I;
-
fun merge _ tables = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUPS dups =>
error ("Attempt to merge different versions of attribute(s) " ^ commas_quote dups);
+);
- fun print _ attribs =
- let
- fun prt_attr (name, ((_, comment), _)) = Pretty.block
- [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
- in
- [Pretty.big_list "attributes:" (map prt_attr (NameSpace.extern_table attribs))]
- |> Pretty.chunks |> Pretty.writeln
- end;
-end);
-
-val _ = Context.add_setup AttributesData.init;
-val print_attributes = AttributesData.print;
+fun print_attributes thy =
+ let
+ val attribs = AttributesData.get thy;
+ fun prt_attr (name, ((_, comment), _)) = Pretty.block
+ [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
+ in
+ [Pretty.big_list "attributes:" (map prt_attr (NameSpace.extern_table attribs))]
+ |> Pretty.chunks |> Pretty.writeln
+ end;
(* name space *)
--- a/src/Pure/Isar/calculation.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/Isar/calculation.ML Mon May 07 00:49:59 2007 +0200
@@ -30,25 +30,21 @@
structure CalculationData = GenericDataFun
(
- val name = "Isar/calculation";
type T = (thm NetRules.T * thm list) * (thm list * int) option;
val empty = ((NetRules.elim, []), NONE);
val extend = I;
fun merge _ (((trans1, sym1), _), ((trans2, sym2), _)) =
((NetRules.merge (trans1, trans2), Drule.merge_rules (sym1, sym2)), NONE);
-
- fun print generic ((trans, sym), _) =
- let val ctxt = Context.proof_of generic in
- [Pretty.big_list "transitivity rules:"
- (map (ProofContext.pretty_thm ctxt) (NetRules.rules trans)),
- Pretty.big_list "symmetry rules:" (map (ProofContext.pretty_thm ctxt) sym)]
- |> Pretty.chunks |> Pretty.writeln
- end;
);
-val _ = Context.add_setup CalculationData.init;
-val print_rules = CalculationData.print o Context.Proof;
+fun print_rules ctxt =
+ let val ((trans, sym), _) = CalculationData.get (Context.Proof ctxt) in
+ [Pretty.big_list "transitivity rules:"
+ (map (ProofContext.pretty_thm ctxt) (NetRules.rules trans)),
+ Pretty.big_list "symmetry rules:" (map (ProofContext.pretty_thm ctxt) sym)]
+ |> Pretty.chunks |> Pretty.writeln
+ end;
(* access calculation *)
--- a/src/Pure/Isar/context_rules.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/Isar/context_rules.ML Mon May 07 00:49:59 2007 +0200
@@ -94,9 +94,7 @@
structure Rules = GenericDataFun
(
- val name = "Pure/rules";
type T = T;
-
val empty = make_rules ~1 [] empty_netpairs ([], []);
val extend = I;
@@ -112,20 +110,17 @@
nth_map i (curry insert_tagged_brl ((w, n), (b, th))))
(next upto ~1 ~~ rules) empty_netpairs;
in make_rules (next - 1) rules netpairs wrappers end
-
- fun print generic (Rules {rules, ...}) =
- let
- val ctxt = Context.proof_of generic;
- fun prt_kind (i, b) =
- Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":")
- (map_filter (fn (_, (k, th)) =>
- if k = (i, b) then SOME (ProofContext.pretty_thm ctxt th) else NONE)
- (sort (int_ord o pairself fst) rules));
- in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
);
-val _ = Context.add_setup Rules.init;
-val print_rules = Rules.print o Context.Proof;
+fun print_rules ctxt =
+ let
+ val Rules {rules, ...} = Rules.get (Context.Proof ctxt);
+ fun prt_kind (i, b) =
+ Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":")
+ (map_filter (fn (_, (k, th)) =>
+ if k = (i, b) then SOME (ProofContext.pretty_thm ctxt th) else NONE)
+ (sort (int_ord o pairself fst) rules));
+ in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
(* access data *)
--- a/src/Pure/Isar/induct_attrib.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/Isar/induct_attrib.ML Mon May 07 00:49:59 2007 +0200
@@ -94,49 +94,43 @@
(* context data *)
-fun dest ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) =
- {type_cases = NetRules.rules casesT,
- set_cases = NetRules.rules casesS,
- type_induct = NetRules.rules inductT,
- set_induct = NetRules.rules inductS,
- type_coinduct = NetRules.rules coinductT,
- set_coinduct = NetRules.rules coinductS};
-
structure Induct = GenericDataFun
(
- val name = "Isar/induct";
type T = (rules * rules) * (rules * rules) * (rules * rules);
-
val empty =
((init_rules (left_var_prem o #2), init_rules (Thm.major_prem_of o #2)),
(init_rules (right_var_concl o #2), init_rules (Thm.major_prem_of o #2)),
(init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2)));
-
val extend = I;
-
fun merge _ (((casesT1, casesS1), (inductT1, inductS1), (coinductT1, coinductS1)),
((casesT2, casesS2), (inductT2, inductS2), (coinductT2, coinductS2))) =
((NetRules.merge (casesT1, casesT2), NetRules.merge (casesS1, casesS2)),
(NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2)),
(NetRules.merge (coinductT1, coinductT2), NetRules.merge (coinductS1, coinductS2)));
-
- fun print generic ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) =
- let val ctxt = Context.proof_of generic in
- [pretty_rules ctxt "coinduct type:" coinductT,
- pretty_rules ctxt "coinduct set:" coinductS,
- pretty_rules ctxt "induct type:" inductT,
- pretty_rules ctxt "induct set:" inductS,
- pretty_rules ctxt "cases type:" casesT,
- pretty_rules ctxt "cases set:" casesS]
- |> Pretty.chunks |> Pretty.writeln
- end
);
-val _ = Context.add_setup Induct.init;
-val print_rules = Induct.print o Context.Proof;
-val dest_rules = dest o Induct.get o Context.Proof;
+val get_local = Induct.get o Context.Proof;
-val get_local = Induct.get o Context.Proof;
+fun dest_rules ctxt =
+ let val ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) = get_local ctxt in
+ {type_cases = NetRules.rules casesT,
+ set_cases = NetRules.rules casesS,
+ type_induct = NetRules.rules inductT,
+ set_induct = NetRules.rules inductS,
+ type_coinduct = NetRules.rules coinductT,
+ set_coinduct = NetRules.rules coinductS}
+ end;
+
+fun print_rules ctxt =
+ let val ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) = get_local ctxt in
+ [pretty_rules ctxt "coinduct type:" coinductT,
+ pretty_rules ctxt "coinduct set:" coinductS,
+ pretty_rules ctxt "induct type:" inductT,
+ pretty_rules ctxt "induct set:" inductS,
+ pretty_rules ctxt "cases type:" casesT,
+ pretty_rules ctxt "cases set:" casesS]
+ |> Pretty.chunks |> Pretty.writeln
+ end;
(* access rules *)
--- a/src/Pure/Isar/local_defs.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/Isar/local_defs.ML Mon May 07 00:49:59 2007 +0200
@@ -147,19 +147,15 @@
structure Rules = GenericDataFun
(
- val name = "Pure/derived_defs";
type T = thm list;
val empty = []
val extend = I;
fun merge _ = Drule.merge_rules;
- fun print context rules =
- Pretty.writeln (Pretty.big_list "definitional transformations:"
- (map (ProofContext.pretty_thm (Context.proof_of context)) rules));
);
-val _ = Context.add_setup Rules.init;
-
-val print_rules = Rules.print o Context.Proof;
+fun print_rules ctxt =
+ Pretty.writeln (Pretty.big_list "definitional transformations:"
+ (map (ProofContext.pretty_thm ctxt) (Rules.get (Context.Proof ctxt))));
val defn_add = Thm.declaration_attribute (Rules.map o Drule.add_rule);
val defn_del = Thm.declaration_attribute (Rules.map o Drule.del_rule);
--- a/src/Pure/Isar/local_theory.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/Isar/local_theory.ML Mon May 07 00:49:59 2007 +0200
@@ -88,12 +88,9 @@
structure Data = ProofDataFun
(
- val name = "Pure/local_theory";
type T = lthy option;
fun init _ = NONE;
- fun print _ _ = ();
);
-val _ = Context.add_setup Data.init;
fun get_lthy lthy =
(case Data.get lthy of
--- a/src/Pure/Isar/locale.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/Isar/locale.ML Mon May 07 00:49:59 2007 +0200
@@ -305,8 +305,7 @@
(** theory data **)
structure GlobalLocalesData = TheoryDataFun
-(struct
- val name = "Isar/locales";
+(
type T = NameSpace.T * locale Symtab.table * Registrations.T Symtab.table;
(* 1st entry: locale namespace,
2nd entry: locales of the theory,
@@ -332,33 +331,26 @@
fun merge _ ((space1, locs1, regs1), (space2, locs2, regs2)) =
(NameSpace.merge (space1, space2), Symtab.join join_locales (locs1, locs2),
Symtab.join (K Registrations.join) (regs1, regs2));
-
- fun print _ (space, locs, _) =
- Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs)))
- |> Pretty.writeln;
-end);
-
-val _ = Context.add_setup GlobalLocalesData.init;
+);
(** context data **)
structure LocalLocalesData = ProofDataFun
-(struct
- val name = "Isar/locales";
- type T = Registrations.T Symtab.table;
- (* registrations, indexed by locale name *)
+(
+ type T = Registrations.T Symtab.table; (*registrations, indexed by locale name*)
fun init _ = Symtab.empty;
- fun print _ _ = ();
-end);
-
-val _ = Context.add_setup LocalLocalesData.init;
+);
(* access locales *)
-val print_locales = GlobalLocalesData.print;
+fun print_locales thy =
+ let val (space, locs, _) = GlobalLocalesData.get thy in
+ Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs)))
+ |> Pretty.writeln
+ end;
val intern = NameSpace.intern o #1 o GlobalLocalesData.get;
val extern = NameSpace.extern o #1 o GlobalLocalesData.get;
--- a/src/Pure/Isar/method.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/Isar/method.ML Mon May 07 00:49:59 2007 +0200
@@ -378,28 +378,24 @@
(* method definitions *)
structure MethodsData = TheoryDataFun
-(struct
- val name = "Isar/methods";
+(
type T = (((src -> Proof.context -> method) * string) * stamp) NameSpace.table;
-
val empty = NameSpace.empty_table;
val copy = I;
val extend = I;
fun merge _ tables = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUPS dups =>
error ("Attempt to merge different versions of method(s) " ^ commas_quote dups);
+);
- fun print _ meths =
- let
- fun prt_meth (name, ((_, comment), _)) = Pretty.block
- [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
- in
- [Pretty.big_list "methods:" (map prt_meth (NameSpace.extern_table meths))]
- |> Pretty.chunks |> Pretty.writeln
- end;
-end);
-
-val _ = Context.add_setup MethodsData.init;
-val print_methods = MethodsData.print;
+fun print_methods thy =
+ let
+ val meths = MethodsData.get thy;
+ fun prt_meth (name, ((_, comment), _)) = Pretty.block
+ [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
+ in
+ [Pretty.big_list "methods:" (map prt_meth (NameSpace.extern_table meths))]
+ |> Pretty.chunks |> Pretty.writeln
+ end;
(* get methods *)
--- a/src/Pure/Isar/object_logic.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/Isar/object_logic.ML Mon May 07 00:49:59 2007 +0200
@@ -38,11 +38,9 @@
(** theory data **)
structure ObjectLogicData = TheoryDataFun
-(struct
- val name = "Pure/object_logic";
+(
type T = string option * (thm list * thm list);
-
- val empty = (NONE, ([], [Drule.norm_hhf_eq]));
+ val empty = (NONE, ([], []));
val copy = I;
val extend = I;
@@ -53,11 +51,7 @@
fun merge _ ((judgment1, (atomize1, rulify1)), (judgment2, (atomize2, rulify2))) =
(merge_judgment (judgment1, judgment2),
(Drule.merge_rules (atomize1, atomize2), Drule.merge_rules (rulify1, rulify2)));
-
- fun print _ _ = ();
-end);
-
-val _ = Context.add_setup ObjectLogicData.init;
+);
@@ -136,11 +130,13 @@
val get_atomize = #1 o #2 o ObjectLogicData.get;
val get_rulify = #2 o #2 o ObjectLogicData.get;
-val declare_atomize = Thm.declaration_attribute (fn th =>
- Context.mapping (ObjectLogicData.map (apsnd (apfst (Drule.add_rule th)))) I);
+val add_atomize = ObjectLogicData.map o apsnd o apfst o Drule.add_rule;
+val add_rulify = ObjectLogicData.map o apsnd o apsnd o Drule.add_rule;
-val declare_rulify = Thm.declaration_attribute (fn th =>
- Context.mapping (ObjectLogicData.map (apsnd (apsnd (Drule.add_rule th)))) I);
+val declare_atomize = Thm.declaration_attribute (fn th => Context.mapping (add_atomize th) I);
+val declare_rulify = Thm.declaration_attribute (fn th => Context.mapping (add_rulify th) I);
+
+val _ = Context.add_setup (add_rulify Drule.norm_hhf_eq);
(* atomize *)
--- a/src/Pure/Isar/proof_context.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/Isar/proof_context.ML Mon May 07 00:49:59 2007 +0200
@@ -198,17 +198,13 @@
structure ContextData = ProofDataFun
(
- val name = "Isar/context";
type T = ctxt;
fun init thy =
make_ctxt (false, local_naming, LocalSyntax.init thy,
(Sign.consts_of thy, Sign.consts_of thy),
(NameSpace.empty_table, FactIndex.empty), []);
- fun print _ _ = ();
);
-val _ = Context.add_setup ContextData.init;
-
fun rep_context ctxt = ContextData.get ctxt |> (fn Ctxt args => args);
fun map_context f =
--- a/src/Pure/Isar/theory_target.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/Isar/theory_target.ML Mon May 07 00:49:59 2007 +0200
@@ -22,13 +22,10 @@
structure Data = ProofDataFun
(
- val name = "Isar/theory_target";
type T = string option;
fun init _ = NONE;
- fun print _ _ = ();
);
-val _ = Context.add_setup Data.init;
val peek = Data.get;
--- a/src/Pure/Proof/extraction.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/Proof/extraction.ML Mon May 07 00:49:59 2007 +0200
@@ -171,11 +171,10 @@
(**** theory data ****)
-(* data kind 'Pure/extraction' *)
+(* theory data *)
structure ExtractionData = TheoryDataFun
-(struct
- val name = "Pure/extraction";
+(
type T =
{realizes_eqns : rules,
typeof_eqns : rules,
@@ -209,11 +208,7 @@
defs = Library.merge Thm.eq_thm (defs1, defs2),
expand = Library.merge (op =) (expand1, expand2),
prep = (case prep1 of NONE => prep2 | _ => prep1)};
-
- fun print _ _ = ();
-end);
-
-val _ = Context.add_setup ExtractionData.init;
+);
fun read_condeq thy =
let val thy' = add_syntax thy
--- a/src/Pure/Thy/present.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/Thy/present.ML Mon May 07 00:49:59 2007 +0200
@@ -75,17 +75,13 @@
(** additional theory data **)
structure BrowserInfoData = TheoryDataFun
-(struct
- val name = "Pure/browser_info";
+(
type T = {name: string, session: string list, is_local: bool};
val empty = {name = "", session = [], is_local = false}: T;
val copy = I;
fun extend _ = empty;
fun merge _ _ = empty;
- fun print _ _ = ();
-end);
-
-val _ = Context.add_setup BrowserInfoData.init;
+);
fun get_info thy =
if member (op =) [Context.ProtoPureN, Context.PureN, Context.CPureN] (Context.theory_name thy)
--- a/src/Pure/Thy/term_style.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/Thy/term_style.ML Mon May 07 00:49:59 2007 +0200
@@ -22,19 +22,17 @@
error ("Duplicate declaration of antiquote style(s): " ^ commas_quote names);
structure StyleData = TheoryDataFun
-(struct
- val name = "Isar/antiquote_style";
+(
type T = ((Proof.context -> term -> term) * stamp) Symtab.table;
val empty = Symtab.empty;
val copy = I;
val extend = I;
fun merge _ tabs = Symtab.merge (eq_snd (op =)) tabs
handle Symtab.DUPS dups => err_dup_styles dups;
- fun print _ tab = Pretty.writeln (Pretty.strs ("antiquote styles:" :: Symtab.keys tab));
-end);
+);
-val _ = Context.add_setup StyleData.init;
-val print_styles = StyleData.print;
+fun print_styles thy =
+ Pretty.writeln (Pretty.strs ("antiquote styles:" :: Symtab.keys (StyleData.get thy)));
(* accessors *)
--- a/src/Pure/Tools/class_package.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/Tools/class_package.ML Mon May 07 00:49:59 2007 +0200
@@ -237,20 +237,15 @@
fun merge_pair f1 f2 ((x1, y1), (x2, y2)) = (f1 (x1, x2), f2 (y1, y2));
-structure ClassData = TheoryDataFun (
- struct
- val name = "Pure/classes";
- type T = class_data Graph.T * class Symtab.table (*locale name ~> class name*);
- val empty = (Graph.empty, Symtab.empty);
- val copy = I;
- val extend = I;
- fun merge _ = merge_pair (Graph.merge (K true)) (Symtab.merge (K true));
- fun print _ _ = ();
- end
+structure ClassData = TheoryDataFun
+(
+ type T = class_data Graph.T * class Symtab.table (*locale name ~> class name*);
+ val empty = (Graph.empty, Symtab.empty);
+ val copy = I;
+ val extend = I;
+ fun merge _ = merge_pair (Graph.merge (K true)) (Symtab.merge (K true));
);
-val _ = Context.add_setup ClassData.init;
-
(* queries *)
--- a/src/Pure/Tools/codegen_data.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/Tools/codegen_data.ML Mon May 07 00:49:59 2007 +0200
@@ -312,8 +312,7 @@
type data = Object.T Datatab.table;
structure CodeData = TheoryDataFun
-(struct
- val name = "Pure/codegen_data";
+(
type T = exec * data ref;
val empty = (empty_exec, ref Datatab.empty : data ref);
fun copy (exec, data) = (exec, ref (! data));
@@ -325,67 +324,67 @@
val data2' = Datatab.map' (invoke_purge NONE touched) (! data2);
val data = Datatab.join (invoke_merge pp) (data1', data2');
in (exec, ref data) end;
- fun print thy (exec, _) =
- let
- val ctxt = ProofContext.init thy;
- fun pretty_func (s, lthms) =
- (Pretty.block o Pretty.fbreaks) (
- Pretty.str s :: pretty_sdthms ctxt lthms
- );
- fun pretty_dtyp (s, []) =
+);
+
+fun print_codesetup thy =
+ let
+ val ctxt = ProofContext.init thy;
+ val (exec, _) = CodeData.get thy;
+ fun pretty_func (s, lthms) =
+ (Pretty.block o Pretty.fbreaks) (
+ Pretty.str s :: pretty_sdthms ctxt lthms
+ );
+ fun pretty_dtyp (s, []) =
+ Pretty.str s
+ | pretty_dtyp (s, cos) =
+ (Pretty.block o Pretty.breaks) (
Pretty.str s
- | pretty_dtyp (s, cos) =
- (Pretty.block o Pretty.breaks) (
- Pretty.str s
- :: Pretty.str "="
- :: separate (Pretty.str "|") (map (fn (c, []) => Pretty.str c
- | (c, tys) =>
- (Pretty.block o Pretty.breaks)
- (Pretty.str c :: Pretty.str "of" :: map (Pretty.quote o Sign.pretty_typ thy) tys)) cos)
- );
- val inlines = (#inlines o the_preproc) exec;
- val inline_procs = (map fst o #inline_procs o the_preproc) exec;
- val preprocs = (map fst o #preprocs o the_preproc) exec;
- val funs = the_funcs exec
- |> Consttab.dest
- |> (map o apfst) (CodegenConsts.string_of_const thy)
- |> sort (string_ord o pairself fst);
- val dtyps = the_dtyps exec
- |> Symtab.dest
- |> map (fn (dtco, (vs, cos)) => (Sign.string_of_typ thy (Type (dtco, map TFree vs)), cos))
- |> sort (string_ord o pairself fst)
- in
- (Pretty.writeln o Pretty.chunks) [
- Pretty.block (
- Pretty.str "defining equations:"
- :: Pretty.fbrk
- :: (Pretty.fbreaks o map pretty_func) funs
- ),
- Pretty.block (
- Pretty.str "inlining theorems:"
- :: Pretty.fbrk
- :: (Pretty.fbreaks o map (ProofContext.pretty_thm ctxt)) inlines
- ),
- Pretty.block (
- Pretty.str "inlining procedures:"
- :: Pretty.fbrk
- :: (Pretty.fbreaks o map Pretty.str) inline_procs
- ),
- Pretty.block (
- Pretty.str "preprocessors:"
- :: Pretty.fbrk
- :: (Pretty.fbreaks o map Pretty.str) preprocs
- ),
- Pretty.block (
- Pretty.str "datatypes:"
- :: Pretty.fbrk
- :: (Pretty.fbreaks o map pretty_dtyp) dtyps
- )
- ]
- end;
-end);
-
-val print_codesetup = CodeData.print;
+ :: Pretty.str "="
+ :: separate (Pretty.str "|") (map (fn (c, []) => Pretty.str c
+ | (c, tys) =>
+ (Pretty.block o Pretty.breaks)
+ (Pretty.str c :: Pretty.str "of" :: map (Pretty.quote o Sign.pretty_typ thy) tys)) cos)
+ );
+ val inlines = (#inlines o the_preproc) exec;
+ val inline_procs = (map fst o #inline_procs o the_preproc) exec;
+ val preprocs = (map fst o #preprocs o the_preproc) exec;
+ val funs = the_funcs exec
+ |> Consttab.dest
+ |> (map o apfst) (CodegenConsts.string_of_const thy)
+ |> sort (string_ord o pairself fst);
+ val dtyps = the_dtyps exec
+ |> Symtab.dest
+ |> map (fn (dtco, (vs, cos)) => (Sign.string_of_typ thy (Type (dtco, map TFree vs)), cos))
+ |> sort (string_ord o pairself fst)
+ in
+ (Pretty.writeln o Pretty.chunks) [
+ Pretty.block (
+ Pretty.str "defining equations:"
+ :: Pretty.fbrk
+ :: (Pretty.fbreaks o map pretty_func) funs
+ ),
+ Pretty.block (
+ Pretty.str "inlining theorems:"
+ :: Pretty.fbrk
+ :: (Pretty.fbreaks o map (ProofContext.pretty_thm ctxt)) inlines
+ ),
+ Pretty.block (
+ Pretty.str "inlining procedures:"
+ :: Pretty.fbrk
+ :: (Pretty.fbreaks o map Pretty.str) inline_procs
+ ),
+ Pretty.block (
+ Pretty.str "preprocessors:"
+ :: Pretty.fbrk
+ :: (Pretty.fbreaks o map Pretty.str) preprocs
+ ),
+ Pretty.block (
+ Pretty.str "datatypes:"
+ :: Pretty.fbrk
+ :: (Pretty.fbreaks o map pretty_dtyp) dtyps
+ )
+ ]
+ end;
fun init k = CodeData.map
(fn (exec, data) => (exec, ref (Datatab.update (k, invoke_empty k) (! data))));
--- a/src/Pure/Tools/codegen_names.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/Tools/codegen_names.ML Mon May 07 00:49:59 2007 +0200
@@ -292,18 +292,16 @@
end; (*local*)
structure CodeName = TheoryDataFun
-(struct
- val name = "Pure/codegen_names";
+(
type T = names ref;
val empty = ref empty_names;
fun copy (ref names) = ref names;
val extend = copy;
fun merge _ (ref names1, ref names2) = ref (merge_names (names1, names2));
- fun print _ _ = ();
-end);
+);
structure ConstName = CodeDataFun
-(struct
+(
val name = "Pure/codegen_names";
type T = const Consttab.table * (string * string option) Symtab.table;
val empty = (Consttab.empty, Symtab.empty);
@@ -313,7 +311,7 @@
fun purge _ NONE _ = empty
| purge _ (SOME cs) (const, constrev) = (fold Consttab.delete_safe cs const,
fold Symtab.delete (map_filter (Consttab.lookup const) cs) constrev);
-end);
+);
val _ = Context.add_setup (CodeName.init #> ConstName.init);
--- a/src/Pure/Tools/codegen_package.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/Tools/codegen_package.ML Mon May 07 00:49:59 2007 +0200
@@ -51,18 +51,17 @@
Consttab.merge CodegenConsts.eq_const (consts1, consts2));
structure CodegenPackageData = TheoryDataFun
-(struct
- val name = "Pure/codegen_package_setup";
+(
type T = appgens * abstypes;
val empty = (Symtab.empty, (Symtab.empty, Consttab.empty));
val copy = I;
val extend = I;
fun merge _ ((appgens1, abstypes1), (appgens2, abstypes2)) =
(merge_appgens (appgens1, appgens2), merge_abstypes (abstypes1, abstypes2));
- fun print _ _ = ();
-end);
+);
-structure Funcgr = CodegenFuncgrRetrieval (
+structure Funcgr = CodegenFuncgrRetrieval
+(
val name = "Pure/codegen_package_thms";
fun rewrites thy = [];
);
@@ -94,7 +93,7 @@
in Present.display_graph prgr end;
structure Code = CodeDataFun
-(struct
+(
val name = "Pure/codegen_package_code";
type T = CodegenThingol.code;
val empty = CodegenThingol.empty_code;
@@ -110,9 +109,9 @@
o filter (member CodegenConsts.eq_const cs_exisiting)
) cs;
in Graph.del_nodes dels code end;
-end);
+);
-val _ = Context.add_setup (CodegenPackageData.init #> Funcgr.init #> Code.init);
+val _ = Context.add_setup (Funcgr.init #> Code.init);
(* preparing defining equations *)
--- a/src/Pure/Tools/codegen_serializer.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/Tools/codegen_serializer.ML Mon May 07 00:49:59 2007 +0200
@@ -1539,15 +1539,13 @@
error ("Incompatible serializers: " ^ quote target);
structure CodegenSerializerData = TheoryDataFun
-(struct
- val name = "Pure/codegen_serializer";
+(
type T = target Symtab.table;
val empty = Symtab.empty;
val copy = I;
val extend = I;
fun merge _ = Symtab.join merge_target;
- fun print _ _ = ();
-end);
+);
fun the_serializer (Target { serializer, ... }) = serializer;
fun the_reserved (Target { reserved, ... }) = reserved;
@@ -1587,8 +1585,7 @@
val target_diag = "diag";
val _ = Context.add_setup (
- CodegenSerializerData.init
- #> add_serializer (target_SML, isar_seri_sml)
+ add_serializer (target_SML, isar_seri_sml)
#> add_serializer (target_OCaml, isar_seri_ocaml)
#> add_serializer (target_Haskell, isar_seri_haskell)
#> add_serializer (target_diag, (fn _ => fn _ => fn _ => seri_diagnosis))
--- a/src/Pure/Tools/nbe.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/Tools/nbe.ML Mon May 07 00:49:59 2007 +0200
@@ -26,19 +26,14 @@
(* preproc and postproc attributes *)
structure NBE_Rewrite = TheoryDataFun
-(struct
- val name = "Pure/nbe";
+(
type T = thm list * thm list
-
- val empty = ([],[])
+ val empty = ([], []);
val copy = I;
val extend = I;
-
fun merge _ ((pres1,posts1), (pres2,posts2)) =
(Library.merge Thm.eq_thm (pres1,pres2), Library.merge Thm.eq_thm (posts1,posts2))
-
- fun print _ _ = ()
-end);
+);
val _ =
let
@@ -51,8 +46,7 @@
|| Args.$$$ "post" >> K attr_post));
in
Context.add_setup (
- NBE_Rewrite.init
- #> Attrib.add_attributes
+ Attrib.add_attributes
[("normal", attr, "declare rewrite theorems for normalization")]
)
end;
--- a/src/Pure/assumption.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/assumption.ML Mon May 07 00:49:59 2007 +0200
@@ -62,14 +62,10 @@
structure Data = ProofDataFun
(
- val name = "Pure/assumption";
type T = data;
fun init _ = make_data ([], []);
- fun print _ _ = ();
);
-val _ = Context.add_setup Data.init;
-
fun map_data f = Data.map (fn Data {assms, prems} => make_data (f (assms, prems)));
fun rep_data ctxt = Data.get ctxt |> (fn Data args => args);
--- a/src/Pure/axclass.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/axclass.ML Mon May 07 00:49:59 2007 +0200
@@ -95,18 +95,14 @@
(* setup data *)
structure AxClassData = TheoryDataFun
-(struct
- val name = "Pure/axclass";
+(
type T = axclasses * instances;
- val empty : T = ((Symtab.empty, []), ([], Symtab.empty));
+ val empty = ((Symtab.empty, []), ([], Symtab.empty));
val copy = I;
val extend = I;
fun merge pp ((axclasses1, instances1), (axclasses2, instances2)) =
(merge_axclasses pp (axclasses1, axclasses2), (merge_instances (instances1, instances2)));
- fun print _ _ = ();
-end);
-
-val _ = Context.add_setup AxClassData.init;
+);
(* maintain axclasses *)
--- a/src/Pure/codegen.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/codegen.ML Mon May 07 00:49:59 2007 +0200
@@ -199,13 +199,13 @@
{size = size, iterations = iterations,
default_type = SOME (Sign.read_typ thy s)};
-(* data kind 'Pure/codegen' *)
+
+(* theory data *)
structure CodeData = CodegenData;
structure CodegenData = TheoryDataFun
-(struct
- val name = "Pure/codegen";
+(
type T =
{codegens : (string * term codegen) list,
tycodegens : (string * typ codegen) list,
@@ -237,15 +237,15 @@
preprocs = AList.merge (op =) (K true) (preprocs1, preprocs2),
modules = Symtab.merge (K true) (modules1, modules2),
test_params = merge_test_params test_params1 test_params2};
+);
- fun print _ ({codegens, tycodegens, ...} : T) =
+fun print_codegens thy =
+ let val {codegens, tycodegens, ...} = CodegenData.get thy in
Pretty.writeln (Pretty.chunks
[Pretty.strs ("term code generators:" :: map fst codegens),
- Pretty.strs ("type code generators:" :: map fst tycodegens)]);
-end);
+ Pretty.strs ("type code generators:" :: map fst tycodegens)])
+ end;
-val _ = Context.add_setup CodegenData.init;
-val print_codegens = CodegenData.print;
(**** access parameters for random testing ****)
--- a/src/Pure/compress.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/compress.ML Mon May 07 00:49:59 2007 +0200
@@ -21,8 +21,7 @@
(* theory data *)
structure CompressData = TheoryDataFun
-(struct
- val name = "Pure/compress";
+(
type T = typ Typtab.table ref * term Termtab.table ref;
val empty : T = (ref Typtab.empty, ref Termtab.empty);
fun copy (ref typs, ref terms) : T = (ref typs, ref terms);
@@ -30,8 +29,7 @@
fun merge _ ((ref typs1, ref terms1), (ref typs2, ref terms2)) : T =
(ref (Typtab.merge (K true) (typs1, typs2)),
ref (Termtab.merge (K true) (terms1, terms2)));
- fun print _ _ = ();
-end);
+);
val init_data = CompressData.init;
--- a/src/Pure/display.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/display.ML Mon May 07 00:49:59 2007 +0200
@@ -234,9 +234,6 @@
val rests = restricts |> map (apfst (apfst extern_const)) |> sort_wrt (#1 o #1);
in
[Pretty.strs ("names:" :: Context.names_of thy)] @
- (if verbose then
- [Pretty.strs ("theory data:" :: Context.theory_data_of thy),
- Pretty.strs ("proof data:" :: Context.proof_data_of thy)] else []) @
[Pretty.strs ["name prefix:", NameSpace.path_of naming],
Pretty.big_list "classes:" (map pretty_classrel clsses),
pretty_default default,
--- a/src/Pure/proofterm.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/proofterm.ML Mon May 07 00:49:59 2007 +0200
@@ -110,8 +110,6 @@
(string * (typ list -> proof -> proof option)) list -> proof -> proof
val rewrite_proof_notypes : (proof * proof) list *
(string * (typ list -> proof -> proof option)) list -> proof -> proof
- val init_data: theory -> theory
-
end
structure Proofterm : PROOFTERM =
@@ -1178,10 +1176,8 @@
(**** theory data ****)
structure ProofData = TheoryDataFun
-(struct
- val name = "Pure/proof";
- type T = ((proof * proof) list *
- (string * (typ list -> proof -> proof option)) list);
+(
+ type T = (proof * proof) list * (string * (typ list -> proof -> proof option)) list;
val empty = ([], []);
val copy = I;
@@ -1189,10 +1185,7 @@
fun merge _ ((rules1, procs1) : T, (rules2, procs2)) =
(Library.merge (op =) (rules1, rules2),
AList.merge (op =) (K true) (procs1, procs2));
- fun print _ _ = ();
-end);
-
-val init_data = ProofData.init;
+);
fun add_prf_rrule r = (ProofData.map o apfst) (insert (op =) r);
--- a/src/Pure/pure_thy.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/pure_thy.ML Mon May 07 00:49:59 2007 +0200
@@ -152,7 +152,6 @@
structure TheoremsData = TheoryDataFun
(struct
- val name = "Pure/theorems";
type T =
{theorems: thm list NameSpace.table,
index: FactIndex.T} ref;
@@ -505,9 +504,6 @@
val proto_pure =
Context.pre_pure_thy
|> Compress.init_data
- |> Sign.init_data
- |> Theory.init_data
- |> Proofterm.init_data
|> TheoremsData.init
|> Sign.add_types
[("fun", 2, NoSyn),
--- a/src/Pure/sign.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/sign.ML Mon May 07 00:49:59 2007 +0200
@@ -60,7 +60,6 @@
signature SIGN =
sig
- val init_data: theory -> theory
val rep_sg: theory ->
{naming: NameSpace.naming,
syn: Syntax.syntax,
@@ -203,8 +202,7 @@
Sign {naming = naming, syn = syn, tsig = tsig, consts = consts};
structure SignData = TheoryDataFun
-(struct
- val name = "Pure/sign";
+(
type T = sign;
val copy = I;
fun extend (Sign {syn, tsig, consts, ...}) =
@@ -223,11 +221,7 @@
val tsig = Type.merge_tsigs pp (tsig1, tsig2);
val consts = Consts.merge (consts1, consts2);
in make_sign (naming, syn, tsig, consts) end;
-
- fun print _ _ = ();
-end);
-
-val init_data = SignData.init;
+);
fun rep_sg thy = SignData.get thy |> (fn Sign args => args);
--- a/src/Pure/simplifier.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/simplifier.ML Mon May 07 00:49:59 2007 +0200
@@ -97,19 +97,16 @@
(* global simpsets *)
structure GlobalSimpset = TheoryDataFun
-(struct
- val name = "Pure/simpset";
+(
type T = simpset ref;
-
val empty = ref empty_ss;
- fun copy (ref ss) = ref ss: T; (*create new reference!*)
+ fun copy (ref ss) = ref ss: T;
fun extend (ref ss) = ref (MetaSimplifier.inherit_context empty_ss ss);
fun merge _ (ref ss1, ref ss2) = ref (merge_ss (ss1, ss2));
- fun print _ (ref ss) = print_ss ss;
-end);
+);
val _ = Context.add_setup GlobalSimpset.init;
-val print_simpset = GlobalSimpset.print;
+fun print_simpset thy = print_ss (! (GlobalSimpset.get thy));
val get_simpset = ! o GlobalSimpset.get;
val change_simpset_of = change o GlobalSimpset.get;
@@ -133,15 +130,12 @@
(* local simpsets *)
structure LocalSimpset = ProofDataFun
-(struct
- val name = "Pure/simpset";
+(
type T = simpset;
val init = get_simpset;
- fun print _ ss = print_ss ss;
-end);
+);
-val _ = Context.add_setup LocalSimpset.init;
-val print_local_simpset = LocalSimpset.print;
+val print_local_simpset = print_ss o LocalSimpset.get;
val get_local_simpset = LocalSimpset.get;
val put_local_simpset = LocalSimpset.put;
@@ -181,15 +175,12 @@
structure Simprocs = GenericDataFun
(
- val name = "Pure/simprocs";
type T = simproc NameSpace.table;
val empty = NameSpace.empty_table;
val extend = I;
fun merge _ simprocs = NameSpace.merge_tables eq_simproc simprocs
handle Symtab.DUPS ds => err_dup_simprocs ds;
- fun print _ _ = ();
);
-val _ = Context.add_setup Simprocs.init;
(* get simprocs *)
--- a/src/Pure/theory.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/theory.ML Mon May 07 00:49:59 2007 +0200
@@ -21,7 +21,6 @@
val end_theory: theory -> theory
val checkpoint: theory -> theory
val copy: theory -> theory
- val init_data: theory -> theory
val rep_theory: theory ->
{axioms: term NameSpace.table,
defs: Defs.T,
@@ -101,8 +100,7 @@
fun err_dup_oras dups = error ("Duplicate oracle(s): " ^ commas_quote dups);
structure ThyData = TheoryDataFun
-(struct
- val name = "Pure/theory";
+(
type T = thy;
val empty = make_thy (NameSpace.empty_table, Defs.empty, NameSpace.empty_table);
val copy = I;
@@ -119,11 +117,7 @@
val oracles = NameSpace.merge_tables (eq_snd (op =)) (oracles1, oracles2)
handle Symtab.DUPS dups => err_dup_oras dups;
in make_thy (axioms, defs, oracles) end;
-
- fun print _ _ = ();
-end);
-
-val init_data = ThyData.init;
+);
fun rep_theory thy = ThyData.get thy |> (fn Thy args => args);
--- a/src/Pure/variable.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/Pure/variable.ML Mon May 07 00:49:59 2007 +0200
@@ -79,15 +79,11 @@
structure Data = ProofDataFun
(
- val name = "Pure/variable";
type T = data;
fun init thy =
make_data (false, Name.context, [], Vartab.empty, Symtab.empty, (Vartab.empty, Vartab.empty));
- fun print _ _ = ();
);
-val _ = Context.add_setup Data.init;
-
fun map_data f =
Data.map (fn Data {is_body, names, fixes, binds, type_occs, constraints} =>
make_data (f (is_body, names, fixes, binds, type_occs, constraints)));
--- a/src/ZF/Tools/ind_cases.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/ZF/Tools/ind_cases.ML Mon May 07 00:49:59 2007 +0200
@@ -19,16 +19,13 @@
(* theory data *)
structure IndCasesData = TheoryDataFun
-(struct
- val name = "ZF/ind_cases";
+(
type T = (simpset -> cterm -> thm) Symtab.table;
-
val empty = Symtab.empty;
val copy = I;
val extend = I;
fun merge _ tabs : T = Symtab.merge (K true) tabs;
- fun print _ _ = ();
-end);
+);
fun declare name f = IndCasesData.map (Symtab.update (name, f));
@@ -72,9 +69,8 @@
(* package setup *)
val setup =
- (IndCasesData.init #>
- Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args,
- "dynamic case analysis on sets")]);
+ Method.add_methods
+ [("ind_cases", mk_cases_meth oo mk_cases_args, "dynamic case analysis on sets")];
(* outer syntax *)
--- a/src/ZF/Tools/induct_tacs.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/ZF/Tools/induct_tacs.ML Mon May 07 00:49:59 2007 +0200
@@ -31,19 +31,14 @@
exhaustion : thm};
structure DatatypesData = TheoryDataFun
-(struct
- val name = "ZF/datatypes";
+(
type T = datatype_info Symtab.table;
-
val empty = Symtab.empty;
val copy = I;
val extend = I;
fun merge _ tabs : T = Symtab.merge (K true) tabs;
+);
- fun print thy tab =
- Pretty.writeln (Pretty.strs ("datatypes:" ::
- map #1 (NameSpace.extern_table (Sign.type_space thy, tab))));
-end);
(** Constructor information: needed to map constructors to datatypes **)
@@ -56,15 +51,13 @@
structure ConstructorsData = TheoryDataFun
-(struct
- val name = "ZF/constructors"
+(
type T = constructor_info Symtab.table
val empty = Symtab.empty
val copy = I;
val extend = I
fun merge _ tabs: T = Symtab.merge (K true) tabs;
- fun print _ _= ();
-end);
+);
structure DatatypeTactics : DATATYPE_TACTICS =
struct
@@ -185,13 +178,11 @@
(* theory setup *)
val setup =
- (DatatypesData.init #>
- ConstructorsData.init #>
Method.add_methods
[("induct_tac", Method.goal_args Args.name induct_tac,
"induct_tac emulation (dynamic instantiation!)"),
("case_tac", Method.goal_args Args.name exhaust_tac,
- "datatype case_tac emulation (dynamic instantiation!)")]);
+ "datatype case_tac emulation (dynamic instantiation!)")];
(* outer syntax *)
--- a/src/ZF/Tools/typechk.ML Sun May 06 21:50:17 2007 +0200
+++ b/src/ZF/Tools/typechk.ML Mon May 07 00:49:59 2007 +0200
@@ -44,7 +44,6 @@
structure Data = GenericDataFun
(
- val name = "ZF/type-checking";
type T = tcset
val empty = TC {rules = [], net = Net.empty};
val extend = I;
@@ -52,19 +51,19 @@
fun merge _ (TC {rules, net}, TC {rules = rules', net = net'}) =
TC {rules = Drule.merge_rules (rules, rules'),
net = Net.merge Thm.eq_thm_prop (net, net')};
-
- fun print context (TC {rules, ...}) =
- Pretty.writeln (Pretty.big_list "type-checking rules:"
- (map (ProofContext.pretty_thm (Context.proof_of context)) rules));
);
-val print_tcset = Data.print o Context.Proof;
-
val TC_add = Thm.declaration_attribute (Data.map o add_rule);
val TC_del = Thm.declaration_attribute (Data.map o del_rule);
val tcset_of = Data.get o Context.Proof;
+fun print_tcset ctxt =
+ let val TC {rules, ...} = tcset_of ctxt in
+ Pretty.writeln (Pretty.big_list "type-checking rules:"
+ (map (ProofContext.pretty_thm ctxt) rules))
+ end;
+
(* tactics *)
@@ -128,7 +127,6 @@
(* theory setup *)
val setup =
- Data.init #>
Attrib.add_attributes [("TC", TC_att, "declaration of type-checking rule")] #>
Method.add_methods [("typecheck", typecheck_meth, "ZF type-checking")] #>
(fn thy => (change_simpset_of thy (fn ss => ss setSolver type_solver); thy));