wneuper/isa: test/Tools/isac/kestore.sml@73dc85c025ab

     1 (* Title: tests for KEStore.thy

     2    Author: Walther Neuper

     3    Use is subject to license terms.

     4 *)

     6 "-----------------------------------------------------------------------------";

     7 "-----------------------------------------------------------------------------";

     8 "table of contents -----------------------------------------------------------";

     9 "-----------------------------------------------------------------------------";

    10 "-------- fun check_kestore_rls ----------------------------------------------";

    11 "-------- fun Test_KEStore_Elems.add_rlss overwrites earlier data ------------";

    12 "-----------------------------------------------------------------------------";

    13 "-----------------------------------------------------------------------------";

    15 "-------- fun check_kestore_rls ----------------------------------------------";

    16 "-------- fun check_kestore_rls ----------------------------------------------";

    17 "-------- fun check_kestore_rls ----------------------------------------------";

    18 if check_kestore_rls ("e_rls", ("KEStore", e_rls)) =

    19   "(e_rls, (KEStore, Rls {#calc = 0, #rules = 0, ...))"

    20 then () else error "check_kestore_rls changed"

    21 ;

    22 Test_KEStore_Elems.get_rlss @{theory Isac}

    23   |> map check_kestore_rls

    24   |> enumerate_strings

    25   |> sort string_ord

    26 (*|> map writeln*)

    27 ;

    29 "-------- fun Test_KEStore_Elems.add_rlss overwrites earlier data -----------------";

    30 "-------- fun Test_KEStore_Elems.add_rlss overwrites earlier data -----------------";

    31 "-------- fun Test_KEStore_Elems.add_rlss overwrites earlier data -----------------";

    32   fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;

    33   fun rls_eq ((id1, (thyID1, _)), (id2, (thyID2, _))) = id1 = id2 (*andalso thyID1 = thyID2*)

    35 val data1 = [("test", ("theory-1", Erls)),

    36   ("test_rls", ("theory-1",

    37     append_rls "test_rls" e_rls [Thm ("refl", @{thm refl}), Thm ("subst", @{thm subst})]))]

    38 val data2 =

    39   [("test_rls", ("theory-2",

    40     append_rls "test_rls" e_rls [Thm ("not_def", @{thm not_def})]))]

    41 val data_3a = union rls_eq data1 data2

    42 val data_3b = union_overwrite rls_eq data1 data2

    44 val SOME (_, Rls {rules, ...}) = AList.lookup op = data_3a "test_rls";

    45 case rules of

    46   [Thm ("not_def", _)] => ()

    47 | _ => error "union rls_eq changed: 1st argument is NOT overwritten anymore"

    48 ;

    49 val SOME (_, Rls {rules, ...}) = AList.lookup op = data_3b "test_rls";

    50 case rules of

    51   [Thm ("refl", _), Thm ("subst", _)] => ()

    52 | _ => error "union_overwrite rls_eq changed: 2nd argument is NOT overwritten anymore"

    54 (* add_rlss will take union_overwrite due to argument sequence *)

author	Mathias Lehnfeld <s1210629013@students.fh-hagenberg.at>
	Mon, 27 Jan 2014 21:49:27 +0100
changeset 55359	73dc85c025ab
parent 52139	511fc271f783
child 55397	71f7fd375e7d
permissions	-rw-r--r--