Update from HH
[hl193./.git] / Ntrie / ntrie_tests.ml
1 (* -*- holl -*- *)
2
3 (* ========================================================================= *)
4 (* Conversions for ntries.                                                   *)
5 (* ========================================================================= *)
6
7 (* ------------------------------------------------------------------------- *)
8 (* NTRIE_IN_CONV                                                             *)
9 (* ------------------------------------------------------------------------- *)
10
11 NTRIE_IN_CONV `2 IN NTRIE NEMPTY`;;
12 NTRIE_IN_CONV `0 IN NTRIE NZERO`;;
13 NTRIE_IN_CONV `0 IN NTRIE (NNODE NZERO NZERO)`;;
14 NTRIE_IN_CONV `0 IN NTRIE (NNODE NZERO NZERO)`;;
15 NTRIE_IN_CONV `1 IN NTRIE NZERO`;;
16 NTRIE_IN_CONV `1 IN NTRIE (NNODE NEMPTY NZERO)`;;
17 NTRIE_IN_CONV `1 IN NTRIE (NNODE NZERO NEMPTY)`;;
18 NTRIE_IN_CONV `1 IN NTRIE (NNODE NZERO NZERO)`;;
19 NTRIE_IN_CONV `2 IN NTRIE (NNODE NZERO NZERO)`;;
20 NTRIE_IN_CONV `3 IN NTRIE (NNODE NZERO NZERO)`;;
21
22 (* ------------------------------------------------------------------------- *)
23 (* NTRIE_EQ_CONV                                                             *)
24 (* ------------------------------------------------------------------------- *)
25
26 NTRIE_EQ_CONV `NTRIE NEMPTY = NTRIE NZERO`;;
27 NTRIE_EQ_CONV `NTRIE NZERO = NTRIE NZERO`;;
28 NTRIE_EQ_CONV `NTRIE (NNODE NZERO NEMPTY) = NTRIE NZERO`;;
29 NTRIE_EQ_CONV `NTRIE (NNODE NEMPTY NZERO) = NTRIE NZERO`;;
30 NTRIE_EQ_CONV `NTRIE (NNODE NZERO NEMPTY) = NTRIE (NNODE NZERO NZERO)`;;
31 NTRIE_EQ_CONV `NTRIE (NNODE NEMPTY NZERO) = NTRIE (NNODE NZERO NZERO)`;;
32 NTRIE_EQ_CONV `NTRIE (NNODE NEMPTY NEMPTY) = NTRIE NEMPTY`;;
33
34 (* ------------------------------------------------------------------------- *)
35 (* NTRIE_SUBSET_CONV                                                         *)
36 (* ------------------------------------------------------------------------- *)
37
38 NTRIE_SUBSET_CONV `NTRIE NZERO SUBSET NTRIE NEMPTY`;;
39 NTRIE_SUBSET_CONV `NTRIE NEMPTY SUBSET NTRIE NZERO`;;
40 NTRIE_SUBSET_CONV
41   `NTRIE (NNODE NZERO NEMPTY) SUBSET NTRIE (NNODE NZERO NZERO)`;;
42 NTRIE_SUBSET_CONV
43   `NTRIE (NNODE NEMPTY NZERO) SUBSET NTRIE (NNODE NZERO NZERO)`;;
44
45 (* ------------------------------------------------------------------------- *)
46 (* NTRIE_DISJOINT_CONV                                                       *)
47 (* ------------------------------------------------------------------------- *)
48
49 NTRIE_DISJOINT_CONV `DISJOINT (NTRIE NEMPTY) (NTRIE NEMPTY)`;;
50 NTRIE_DISJOINT_CONV
51   `DISJOINT (NTRIE (NNODE NEMPTY NZERO)) (NTRIE (NNODE NZERO NEMPTY))`;;
52 NTRIE_DISJOINT_CONV
53   `DISJOINT (NTRIE (NNODE NEMPTY NZERO)) (NTRIE (NNODE NEMPTY NZERO))`;;
54
55 (* ------------------------------------------------------------------------- *)
56 (* NTRIE_SING_CONV                                                           *)
57 (* ------------------------------------------------------------------------- *)
58
59 NTRIE_SING_CONV `{10}`;;
60 NTRIE_SING_CONV `{1000}`;;
61 NTRIE_SING_CONV `{100000}`;;
62
63 (* ------------------------------------------------------------------------- *)
64 (* NTRIE_INSERT_CONV                                                         *)
65 (* ------------------------------------------------------------------------- *)
66
67 NTRIE_INSERT_CONV `2 INSERT NTRIE NEMPTY`;;
68 NTRIE_INSERT_CONV `0 INSERT NTRIE NZERO`;;
69 NTRIE_INSERT_CONV `NUMERAL (BIT1 _0) INSERT NTRIE NZERO`;;
70 NTRIE_INSERT_CONV `NUMERAL (BIT0 _0) INSERT NTRIE (NNODE NZERO NZERO)`;;
71 NTRIE_INSERT_CONV `NUMERAL _0 INSERT NTRIE (NNODE NZERO NZERO)`;;
72 NTRIE_INSERT_CONV `NUMERAL (BIT1 _0) INSERT NTRIE (NNODE NZERO NZERO)`;;
73 NTRIE_INSERT_CONV `NUMERAL (BIT0 _0) INSERT NTRIE NZERO`;;
74 NTRIE_INSERT_CONV `NUMERAL (BIT0 (BIT1 (BIT1 _0))) INSERT NTRIE NZERO`;;
75
76 (* ------------------------------------------------------------------------- *)
77 (* NTRIE_UNION_CONV                                                          *)
78 (* ------------------------------------------------------------------------- *)
79
80 NTRIE_UNION_CONV `NTRIE NEMPTY UNION NTRIE NEMPTY`;;
81 NTRIE_UNION_CONV `NTRIE NEMPTY UNION NTRIE NZERO`;;
82 NTRIE_UNION_CONV `NTRIE (NNODE NZERO NZERO) UNION NTRIE NZERO`;;
83 NTRIE_UNION_CONV `NTRIE (NNODE NEMPTY NZERO) UNION NTRIE NZERO`;;
84 NTRIE_UNION_CONV `NTRIE (NNODE NZERO NEMPTY) UNION NTRIE NZERO`;;
85
86 (* ------------------------------------------------------------------------- *)
87 (* NTRIE_INTER_CONV                                                          *)
88 (* ------------------------------------------------------------------------- *)
89
90 NTRIE_INTER_CONV `NTRIE NEMPTY INTER NTRIE NEMPTY`;;
91 NTRIE_INTER_CONV `NTRIE NEMPTY INTER NTRIE NZERO`;;
92 NTRIE_INTER_CONV `NTRIE (NNODE NZERO NZERO) INTER NTRIE NZERO`;;
93 NTRIE_INTER_CONV `NTRIE (NNODE NEMPTY NZERO) INTER NTRIE NZERO`;;
94 NTRIE_INTER_CONV `NTRIE (NNODE NZERO NEMPTY) INTER NTRIE NZERO`;;
95 NTRIE_INTER_CONV
96   `NTRIE (NNODE NEMPTY NEMPTY) INTER NTRIE (NNODE NEMPTY NEMPTY)`;;
97
98 (* ------------------------------------------------------------------------- *)
99 (* NTRIE_DELETE_CONV                                                         *)
100 (* ------------------------------------------------------------------------- *)
101
102 NTRIE_DELETE_CONV `NTRIE NEMPTY DELETE 0`;;
103 NTRIE_DELETE_CONV `NTRIE NZERO DELETE 0`;;
104 NTRIE_DELETE_CONV `NTRIE (NNODE NZERO NEMPTY) DELETE 0`;;
105 NTRIE_DELETE_CONV `NTRIE (NNODE NEMPTY NZERO) DELETE 0`;;
106 NTRIE_DELETE_CONV `NTRIE (NNODE NEMPTY NZERO) DELETE 1`;;
107 NTRIE_DELETE_CONV `NTRIE (NNODE NZERO NEMPTY) DELETE 1`;;
108
109 (* ------------------------------------------------------------------------- *)
110 (* NTRIE_DIFF_CONV                                                           *)
111 (* ------------------------------------------------------------------------- *)
112
113 NTRIE_DIFF_CONV `NTRIE NEMPTY DIFF NTRIE NZERO`;;
114 NTRIE_DIFF_CONV `NTRIE NZERO DIFF NTRIE NZERO`;;
115 NTRIE_DIFF_CONV `NTRIE (NNODE NZERO NEMPTY) DIFF NTRIE (NNODE NZERO NEMPTY)`;;
116 NTRIE_DIFF_CONV `NTRIE (NNODE NEMPTY NZERO) DIFF NTRIE (NNODE NZERO NEMPTY)`;;
117 NTRIE_DIFF_CONV `NTRIE (NNODE NZERO NZERO) DIFF NTRIE (NNODE NEMPTY NZERO)`;;
118 NTRIE_DIFF_CONV `NTRIE (NNODE NZERO NZERO) DIFF NTRIE (NNODE NZERO NEMPTY)`;;
119
120 (* ------------------------------------------------------------------------- *)
121 (* NTRIE_IMAGE_CONV                                                          *)
122 (* ------------------------------------------------------------------------- *)
123
124 NTRIE_IMAGE_CONV NUM_ADD_CONV `IMAGE ((+) 2) (NTRIE NEMPTY)`;;
125 NTRIE_IMAGE_CONV NUM_ADD_CONV `IMAGE ((+) 2) (NTRIE NZERO)`;;
126 NTRIE_IMAGE_CONV NUM_ADD_CONV `IMAGE ((+) 2) (NTRIE (NNODE NZERO NEMPTY))`;;
127 NTRIE_IMAGE_CONV NUM_ADD_CONV `IMAGE ((+) 2) (NTRIE (NNODE NZERO NZERO))`;;
128 NTRIE_IMAGE_CONV NUM_ADD_CONV `IMAGE ((+) 2) (NTRIE (NNODE NEMPTY NZERO))`;;
129 NTRIE_IMAGE_CONV NUM_ADD_CONV `IMAGE ((+) 2) (NTRIE (NNODE NEMPTY NEMPTY))`;;
130 NTRIE_IMAGE_CONV NUM_ADD_CONV `IMAGE ((+) 2) (NTRIE (NNODE (NNODE NEMPTY NZERO) NEMPTY))`;;
131
132 NTRIE_IMAGE_CONV NUM_ADD_CONV `IMAGE (\n. n + 2) (NTRIE NEMPTY)`;;
133 NTRIE_IMAGE_CONV NUM_ADD_CONV `IMAGE (\n. n + 2) (NTRIE NZERO)`;;
134 NTRIE_IMAGE_CONV NUM_ADD_CONV `IMAGE (\n. n + 2) (NTRIE (NNODE NZERO NEMPTY))`;;
135 NTRIE_IMAGE_CONV NUM_ADD_CONV `IMAGE (\n. n + 2) (NTRIE (NNODE NZERO NZERO))`;;
136 NTRIE_IMAGE_CONV NUM_ADD_CONV `IMAGE (\n. n + 2) (NTRIE (NNODE NEMPTY NZERO))`;;
137 NTRIE_IMAGE_CONV NUM_ADD_CONV `IMAGE (\n. n + 2) (NTRIE (NNODE NEMPTY NEMPTY))`;;
138 NTRIE_IMAGE_CONV NUM_ADD_CONV `IMAGE (\n. n + 2) (NTRIE (NNODE (NNODE NEMPTY NZERO) NEMPTY))`;;
139 NTRIE_IMAGE_CONV NUM_ADD_CONV `IMAGE (\n. n + 2) (NTRIE (NNODE NEMPTY (NNODE NEMPTY NZERO)))`;;
140
141 (* ------------------------------------------------------------------------- *)
142 (* NTRIE_DECODE                                                              *)
143 (* ------------------------------------------------------------------------- *)
144
145 NTRIE_DECODE_CONV `NTRIE NEMPTY`;;
146 NTRIE_DECODE_CONV `NTRIE NZERO`;;
147 NTRIE_DECODE_CONV `NTRIE (NNODE NZERO NEMPTY)`;;
148 NTRIE_DECODE_CONV `NTRIE (NNODE NZERO NZERO)`;;
149 NTRIE_DECODE_CONV `NTRIE (NNODE NEMPTY NZERO)`;;
150 NTRIE_DECODE_CONV `NTRIE (NNODE NEMPTY NEMPTY)`;;
151 NTRIE_DECODE_CONV `NTRIE (NNODE (NNODE NEMPTY NZERO) NEMPTY)`;;
152
153 (* ------------------------------------------------------------------------- *)
154 (* NTRIE_ENCODE                                                              *)
155 (* ------------------------------------------------------------------------- *)
156
157 NTRIE_ENCODE_CONV `{}:num->bool`;;
158 NTRIE_ENCODE_CONV `{1,2,3}`;;
159 ONCE_DEPTH_CONV NTRIE_ENCODE_CONV `{1,2,3} UNION {3,4,5}`;;
160
161 (* ------------------------------------------------------------------------- *)
162 (* Final hack-together.                                                      *)
163 (* ------------------------------------------------------------------------- *)
164
165 NTRIE_COMPUTE NTRIE_REDUCE_CONV `{1,2,3} UNION ({3,4} UNION {6,7} UNION {1,7})`;;
166 NTRIE_COMPUTE NTRIE_REDUCE_CONV `{1,2,3} INTER ({3,4} UNION {6,7} UNION {1,7})`;;
167 NTRIE_COMPUTE NTRIE_REDUCE_CONV `{1,2,3} DIFF ({3,4} UNION {6,7} UNION {1,7})`;;
168 NTRIE_COMPUTE NTRIE_REDUCE_CONV `{1,2,3} DIFF ({3,4} UNION {6,7} INTER {1,7})`;;
169 NTRIE_COMPUTE NTRIE_REDUCE_CONV `3 IN {1,2,3} INTER ({3,4} UNION {6,7} UNION {1,7})`;;
170 NTRIE_COMPUTE NTRIE_REDUCE_CONV `11 IN {1,2,3} INTER ({3,4} UNION {6,7} UNION {1,7})`;;
171 NTRIE_COMPUTE NTRIE_REDUCE_CONV `{5,2,3} = {3,2,5}`;;
172 NTRIE_COMPUTE NTRIE_REDUCE_CONV `{5,2,3,2} = {3,2,5}`;;
173 NTRIE_COMPUTE NTRIE_REDUCE_CONV `{5,2,3,2} = {3,2,1,5}`;;
174 NTRIE_COMPUTE NTRIE_REDUCE_CONV `{5,2,3,2} DELETE 2 = {3,5}`;;
175 NTRIE_COMPUTE NTRIE_REDUCE_CONV `{5,2,3} SUBSET {3,2,5}`;;
176 NTRIE_COMPUTE NTRIE_REDUCE_CONV `{5,2,3,7} SUBSET {3,2,5}`;;
177 NTRIE_COMPUTE NTRIE_REDUCE_CONV `{5,2,3,2} SUBSET {3,2,1,5}`;;
178 NTRIE_COMPUTE NTRIE_REDUCE_CONV `{5,2,3} PSUBSET {3,2,5}`;;
179 NTRIE_COMPUTE NTRIE_REDUCE_CONV `{5,2,3} PSUBSET {3,2,0,5}`;;
180 NTRIE_COMPUTE NTRIE_REDUCE_CONV `DISJOINT {12,3,2,1} {3,2,7,9}`;;
181 NTRIE_COMPUTE NTRIE_REDUCE_CONV `DISJOINT {12,3,1} {2,7,9}`;;