equal
deleted
inserted
replaced
|
1 theory Codec_Test |
|
2 imports Common "~~/src/Tools/Spec_Check/Spec_Check" |
|
3 begin |
|
4 |
|
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 |
|
16 |
|
17 fun gen_unit r = |
|
18 ((), r) |
|
19 \<close> |
|
20 |
|
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> |
|
40 |
|
41 end |