wneuper/isa: libisabelle-protocol/libisabelle/protocol/Codec

     1 theory Codec_Test

     2 imports Common "~~/src/Tools/Spec_Check/Spec_Check"

     3 begin

     5 ML\<open>

     6 fun check_for str =

     7   let

     8     val prop1 =

     9       "ALL x. (let val c = (" ^ str ^ ") in Codec.decode c (Codec.encode c x) = Codec.Success x end)"

    10     val prop2 =

    11       "ALL x. (let val c = (" ^ str ^ ") in Codec.decode c (YXML.parse (YXML.string_of (Codec.encode c x))) = Codec.Success x end)"

    12   in

    13     check_property prop1;

    14     check_property prop2

    15   end

    17 fun gen_unit r =

    18   ((), r)

    19 \<close>

    21 ML_command\<open>

    22   check_for "Codec.unit";

    23   check_for "Codec.int";

    24   check_for "Codec.bool";

    25   check_for "Codec.string";

    26   check_for "Codec.tuple Codec.int Codec.int";

    27   check_for "Codec.tuple Codec.string Codec.unit";

    28   check_for "Codec.list Codec.unit";

    29   check_for "Codec.list Codec.int";

    30   check_for "Codec.list Codec.string";

    31   check_for "Codec.list (Codec.list Codec.string)";

    32   check_for "Codec.list (Codec.tuple Codec.int Codec.int)";

    33   check_for "Codec.tuple Codec.int (Codec.list Codec.int)";

    34   check_for "Codec.option Codec.int";

    35   check_for "Codec.option (Codec.list Codec.int)";

    36   check_for "Codec.list (Codec.option (Codec.int))";

    37   check_for "Codec.term";

    38   check_for "Codec.typ";

    39 \<close>

    41 end

author	Walther Neuper <wneuper@ist.tugraz.at>
	Tue, 04 Sep 2018 14:50:30 +0200
changeset 59469	5c56f14bea53
parent 59340	097347b8910e
permissions	-rw-r--r--