simplification/standardization of some theory data;
authorwenzelm
Thu Aug 26 16:34:10 2010 +0200 (2010-08-26)
changeset 3875937a9092de102
parent 38758 f2cfb2cc03e8
child 38760 6f285436e3d6
simplification/standardization of some theory data;
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML
src/HOL/Tools/Quotient/quotient_info.ML
src/Tools/Code/code_simp.ML
src/Tools/quickcheck.ML
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Aug 26 16:25:25 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Aug 26 16:34:10 2010 +0200
     1.3 @@ -730,9 +730,7 @@
     1.4    type T = (mode * (compilation_funs -> typ -> term)) list Symtab.table;
     1.5    val empty = Symtab.empty;
     1.6    val extend = I;
     1.7 -  val merge = Symtab.merge ((K true)
     1.8 -    : ((mode * (compilation_funs -> typ -> term)) list *
     1.9 -      (mode * (compilation_funs -> typ -> term)) list -> bool));
    1.10 +  fun merge data : T = Symtab.merge (K true) data;
    1.11  );
    1.12  
    1.13  fun alternative_compilation_of_global thy pred_name mode =
     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Thu Aug 26 16:25:25 2010 +0200
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Thu Aug 26 16:34:10 2010 +0200
     2.3 @@ -18,8 +18,7 @@
     2.4  structure Specialisations = Theory_Data
     2.5  (
     2.6    type T = (term * term) Item_Net.T;
     2.7 -  val empty = Item_Net.init ((op aconv o pairself fst) : (term * term) * (term * term) -> bool)
     2.8 -    (single o fst);
     2.9 +  val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst);
    2.10    val extend = I;
    2.11    val merge = Item_Net.merge;
    2.12  )
     3.1 --- a/src/HOL/Tools/Quotient/quotient_info.ML	Thu Aug 26 16:25:25 2010 +0200
     3.2 +++ b/src/HOL/Tools/Quotient/quotient_info.ML	Thu Aug 26 16:34:10 2010 +0200
     3.3 @@ -56,10 +56,12 @@
     3.4  type maps_info = {mapfun: string, relmap: string}
     3.5  
     3.6  structure MapsData = Theory_Data
     3.7 -  (type T = maps_info Symtab.table
     3.8 -   val empty = Symtab.empty
     3.9 -   val extend = I
    3.10 -   fun merge data = Symtab.merge (K true) data)
    3.11 +(
    3.12 +  type T = maps_info Symtab.table
    3.13 +  val empty = Symtab.empty
    3.14 +  val extend = I
    3.15 +  fun merge data = Symtab.merge (K true) data
    3.16 +)
    3.17  
    3.18  fun maps_defined thy s =
    3.19    Symtab.defined (MapsData.get thy) s
    3.20 @@ -120,10 +122,12 @@
    3.21  type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
    3.22  
    3.23  structure QuotData = Theory_Data
    3.24 -  (type T = quotdata_info Symtab.table
    3.25 -   val empty = Symtab.empty
    3.26 -   val extend = I
    3.27 -   fun merge data = Symtab.merge (K true) data)
    3.28 +(
    3.29 +  type T = quotdata_info Symtab.table
    3.30 +  val empty = Symtab.empty
    3.31 +  val extend = I
    3.32 +  fun merge data = Symtab.merge (K true) data
    3.33 +)
    3.34  
    3.35  fun transform_quotdata phi {qtyp, rtyp, equiv_rel, equiv_thm} =
    3.36    {qtyp = Morphism.typ phi qtyp,
    3.37 @@ -174,10 +178,12 @@
    3.38     for example given "nat fset" we need to find "'a fset";
    3.39     but overloaded constants share the same name *)
    3.40  structure QConstsData = Theory_Data
    3.41 -  (type T = (qconsts_info list) Symtab.table
    3.42 -   val empty = Symtab.empty
    3.43 -   val extend = I
    3.44 -   val merge = Symtab.merge_list qconsts_info_eq)
    3.45 +(
    3.46 +  type T = qconsts_info list Symtab.table
    3.47 +  val empty = Symtab.empty
    3.48 +  val extend = I
    3.49 +  val merge = Symtab.merge_list qconsts_info_eq
    3.50 +)
    3.51  
    3.52  fun transform_qconsts phi {qconst, rconst, def} =
    3.53    {qconst = Morphism.term phi qconst,
     4.1 --- a/src/Tools/Code/code_simp.ML	Thu Aug 26 16:25:25 2010 +0200
     4.2 +++ b/src/Tools/Code/code_simp.ML	Thu Aug 26 16:34:10 2010 +0200
     4.3 @@ -37,7 +37,8 @@
     4.4  
     4.5  (* dedicated simpset *)
     4.6  
     4.7 -structure Simpset = Theory_Data (
     4.8 +structure Simpset = Theory_Data
     4.9 +(
    4.10    type T = simpset;
    4.11    val empty = empty_ss;
    4.12    fun extend ss = MetaSimplifier.inherit_context empty_ss ss;
     5.1 --- a/src/Tools/quickcheck.ML	Thu Aug 26 16:25:25 2010 +0200
     5.2 +++ b/src/Tools/quickcheck.ML	Thu Aug 26 16:34:10 2010 +0200
     5.3 @@ -78,27 +78,32 @@
     5.4  
     5.5  datatype test_params = Test_Params of
     5.6    { size: int, iterations: int, default_type: typ list, no_assms: bool,
     5.7 -  expect : expectation, report: bool, quiet : bool};
     5.8 +    expect : expectation, report: bool, quiet : bool};
     5.9  
    5.10  fun dest_test_params (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet }) =
    5.11    ((size, iterations), ((default_type, no_assms), ((expect, report), quiet)));
    5.12 +
    5.13  fun make_test_params ((size, iterations), ((default_type, no_assms), ((expect, report), quiet))) =
    5.14    Test_Params { size = size, iterations = iterations, default_type = default_type,
    5.15 -                no_assms = no_assms, expect = expect, report = report, quiet = quiet };
    5.16 +    no_assms = no_assms, expect = expect, report = report, quiet = quiet };
    5.17 +
    5.18  fun map_test_params f (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet }) =
    5.19    make_test_params (f ((size, iterations), ((default_type, no_assms), ((expect, report), quiet))));
    5.20 -fun merge_test_params (Test_Params { size = size1, iterations = iterations1, default_type = default_type1,
    5.21 -                                     no_assms = no_assms1, expect = expect1, report = report1, quiet = quiet1 },
    5.22 +
    5.23 +fun merge_test_params
    5.24 + (Test_Params { size = size1, iterations = iterations1, default_type = default_type1,
    5.25 +    no_assms = no_assms1, expect = expect1, report = report1, quiet = quiet1 },
    5.26    Test_Params { size = size2, iterations = iterations2, default_type = default_type2,
    5.27 -                no_assms = no_assms2, expect = expect2, report = report2, quiet = quiet2 }) =
    5.28 +    no_assms = no_assms2, expect = expect2, report = report2, quiet = quiet2 }) =
    5.29    make_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)),
    5.30      ((merge (op =) (default_type1, default_type2), no_assms1 orelse no_assms2),
    5.31      ((merge_expectation (expect1, expect2), report1 orelse report2), quiet1 orelse quiet2)));
    5.32  
    5.33  structure Data = Theory_Data
    5.34  (
    5.35 -  type T = (string * (Proof.context -> bool -> term -> int -> term list option * (bool list * bool))) list
    5.36 -    * test_params;
    5.37 +  type T =
    5.38 +    (string * (Proof.context -> bool -> term -> int -> term list option * (bool list * bool))) list
    5.39 +      * test_params;
    5.40    val empty = ([], Test_Params
    5.41      { size = 10, iterations = 100, default_type = [], no_assms = false,
    5.42        expect = No_Expectation, report = false, quiet = false});