4 import Prelude hiding (LT)
8 import Cube hiding (i, j, k)
10 import Misc (all_equal, disjoint)
11 import Tetrahedron (b0, b1, b2, b3, c, fv,
12 v0, v1, v2, v3, volume)
17 prop_opposite_octant_tetrahedra_disjoint1 :: Cube -> Bool
18 prop_opposite_octant_tetrahedra_disjoint1 c =
19 disjoint (front_left_top_tetrahedra c) (front_right_down_tetrahedra c)
21 prop_opposite_octant_tetrahedra_disjoint2 :: Cube -> Bool
22 prop_opposite_octant_tetrahedra_disjoint2 c =
23 disjoint (back_left_top_tetrahedra c) (back_right_down_tetrahedra c)
25 prop_opposite_octant_tetrahedra_disjoint3 :: Cube -> Bool
26 prop_opposite_octant_tetrahedra_disjoint3 c =
27 disjoint (front_left_top_tetrahedra c) (back_right_top_tetrahedra c)
29 prop_opposite_octant_tetrahedra_disjoint4 :: Cube -> Bool
30 prop_opposite_octant_tetrahedra_disjoint4 c =
31 disjoint (front_left_down_tetrahedra c) (back_right_down_tetrahedra c)
33 prop_opposite_octant_tetrahedra_disjoint5 :: Cube -> Bool
34 prop_opposite_octant_tetrahedra_disjoint5 c =
35 disjoint (front_left_top_tetrahedra c) (back_left_down_tetrahedra c)
37 prop_opposite_octant_tetrahedra_disjoint6 :: Cube -> Bool
38 prop_opposite_octant_tetrahedra_disjoint6 c =
39 disjoint (front_right_top_tetrahedra c) (back_right_down_tetrahedra c)
42 -- | Since the grid size is necessarily positive, all tetrahedra
43 -- (which comprise cubes of positive volume) must have positive volume
45 prop_all_volumes_positive :: Cube -> Bool
46 prop_all_volumes_positive cube =
47 null nonpositive_volumes
50 volumes = map volume ts
51 nonpositive_volumes = filter (<= 0) volumes
53 -- | In fact, since all of the tetrahedra are identical, we should
54 -- already know their volumes. There's 24 tetrahedra to a cube, so
55 -- we'd expect the volume of each one to be (1/24)*h^3.
56 prop_all_volumes_exact :: Cube -> Bool
57 prop_all_volumes_exact cube =
58 and [volume t ~~= (1/24)*(delta^(3::Int)) | t <- tetrahedra cube]
62 -- | All tetrahedron should have their v0 located at the center of the cube.
63 prop_v0_all_equal :: Cube -> Bool
64 prop_v0_all_equal cube = (v0 t0) == (v0 t1)
66 t0 = head (tetrahedra cube) -- Doesn't matter which two we choose.
67 t1 = head $ tail (tetrahedra cube)
70 -- | Given in Sorokina and Zeilfelder, p. 79, (2.6). Note that the
71 -- third and fourth indices of c-t1 have been switched. This is
72 -- because we store the triangles oriented such that their volume is
73 -- positive. If T and T-tilde share \<v0,v1,v2\> and v3,v3-tilde point
74 -- in opposite directions, one of them has to have negative volume!
75 prop_c0120_identity1 :: Cube -> Bool
76 prop_c0120_identity1 cube =
77 c t0 0 1 2 0 ~= (c t0 0 0 2 1 + c t3 0 0 1 2) / 2
79 t0 = tetrahedron cube 0
80 t3 = tetrahedron cube 3
83 -- | Given in Sorokina and Zeilfelder, p. 79, (2.6). Repeats
84 -- 'prop_c0120_identity1' with tetrahedrons 1 and 2.
85 prop_c0120_identity2 :: Cube -> Bool
86 prop_c0120_identity2 cube =
87 c t1 0 1 2 0 ~= (c t1 0 0 2 1 + c t0 0 0 1 2) / 2
89 t0 = tetrahedron cube 0
90 t1 = tetrahedron cube 1
92 -- | Given in Sorokina and Zeilfelder, p. 79, (2.6). Repeats
93 -- 'prop_c0120_identity1' with tetrahedrons 1 and 2.
94 prop_c0120_identity3 :: Cube -> Bool
95 prop_c0120_identity3 cube =
96 c t2 0 1 2 0 ~= (c t2 0 0 2 1 + c t1 0 0 1 2) / 2
98 t1 = tetrahedron cube 1
99 t2 = tetrahedron cube 2
101 -- | Given in Sorokina and Zeilfelder, p. 79, (2.6). Repeats
102 -- 'prop_c0120_identity1' with tetrahedrons 2 and 3.
103 prop_c0120_identity4 :: Cube -> Bool
104 prop_c0120_identity4 cube =
105 c t3 0 1 2 0 ~= (c t3 0 0 2 1 + c t2 0 0 1 2) / 2
107 t2 = tetrahedron cube 2
108 t3 = tetrahedron cube 3
111 -- | Given in Sorokina and Zeilfelder, p. 79, (2.6). Repeats
112 -- 'prop_c0120_identity1' with tetrahedrons 4 and 5.
113 prop_c0120_identity5 :: Cube -> Bool
114 prop_c0120_identity5 cube =
115 c t5 0 1 2 0 ~= (c t5 0 0 2 1 + c t4 0 0 1 2) / 2
117 t4 = tetrahedron cube 4
118 t5 = tetrahedron cube 5
120 -- -- | Given in Sorokina and Zeilfelder, p. 79, (2.6). Repeats
121 -- -- 'prop_c0120_identity1' with tetrahedrons 5 and 6.
122 prop_c0120_identity6 :: Cube -> Bool
123 prop_c0120_identity6 cube =
124 c t6 0 1 2 0 ~= (c t6 0 0 2 1 + c t5 0 0 1 2) / 2
126 t5 = tetrahedron cube 5
127 t6 = tetrahedron cube 6
130 -- -- | Given in Sorokina and Zeilfelder, p. 79, (2.6). Repeats
131 -- -- 'prop_c0120_identity1' with tetrahedrons 6 and 7.
132 prop_c0120_identity7 :: Cube -> Bool
133 prop_c0120_identity7 cube =
134 c t7 0 1 2 0 ~= (c t7 0 0 2 1 + c t6 0 0 1 2) / 2
136 t6 = tetrahedron cube 6
137 t7 = tetrahedron cube 7
140 -- | Given in Sorokina and Zeilfelder, p. 79, (2.6). See
141 -- 'prop_c0120_identity1'.
142 prop_c0210_identity1 :: Cube -> Bool
143 prop_c0210_identity1 cube =
144 c t0 0 2 1 0 ~= (c t0 0 1 1 1 + c t3 0 1 1 1) / 2
146 t0 = tetrahedron cube 0
147 t3 = tetrahedron cube 3
150 -- | Given in Sorokina and Zeilfelder, p. 79, (2.6). See
151 -- 'prop_c0120_identity1'.
152 prop_c0300_identity1 :: Cube -> Bool
153 prop_c0300_identity1 cube =
154 c t0 0 3 0 0 ~= (c t0 0 2 0 1 + c t3 0 2 1 0) / 2
156 t0 = tetrahedron cube 0
157 t3 = tetrahedron cube 3
160 -- | Given in Sorokina and Zeilfelder, p. 79, (2.6). See
161 -- 'prop_c0120_identity1'.
162 prop_c1110_identity :: Cube -> Bool
163 prop_c1110_identity cube =
164 c t0 1 1 1 0 ~= (c t0 1 0 1 1 + c t3 1 0 1 1) / 2
166 t0 = tetrahedron cube 0
167 t3 = tetrahedron cube 3
170 -- | Given in Sorokina and Zeilfelder, p. 79, (2.6). See
171 -- 'prop_c0120_identity1'.
172 prop_c1200_identity1 :: Cube -> Bool
173 prop_c1200_identity1 cube =
174 c t0 1 2 0 0 ~= (c t0 1 1 0 1 + c t3 1 1 1 0) / 2
176 t0 = tetrahedron cube 0
177 t3 = tetrahedron cube 3
180 -- | Given in Sorokina and Zeilfelder, p. 79, (2.6). See
181 -- 'prop_c0120_identity1'.
182 prop_c2100_identity1 :: Cube -> Bool
183 prop_c2100_identity1 cube =
184 c t0 2 1 0 0 ~= (c t0 2 0 0 1 + c t3 2 0 1 0) / 2
186 t0 = tetrahedron cube 0
187 t3 = tetrahedron cube 3
191 -- | Given in Sorokina and Zeilfelder, p. 79, (2.7). Note that the
192 -- third and fourth indices of c-t3 have been switched. This is
193 -- because we store the triangles oriented such that their volume is
194 -- positive. If T and T-tilde share \<v0,v1,v2\> and v3,v3-tilde
195 -- point in opposite directions, one of them has to have negative
197 prop_c0102_identity1 :: Cube -> Bool
198 prop_c0102_identity1 cube =
199 c t0 0 1 0 2 ~= (c t0 0 0 1 2 + c t1 0 0 2 1) / 2
201 t0 = tetrahedron cube 0
202 t1 = tetrahedron cube 1
205 -- | Given in Sorokina and Zeilfelder, p. 79, (2.7). See
206 -- 'prop_c0102_identity1'.
207 prop_c0201_identity1 :: Cube -> Bool
208 prop_c0201_identity1 cube =
209 c t0 0 2 0 1 ~= (c t0 0 1 1 1 + c t1 0 1 1 1) / 2
211 t0 = tetrahedron cube 0
212 t1 = tetrahedron cube 1
215 -- | Given in Sorokina and Zeilfelder, p. 79, (2.7). See
216 -- 'prop_c0102_identity1'.
217 prop_c0300_identity2 :: Cube -> Bool
218 prop_c0300_identity2 cube =
219 c t0 0 3 0 0 ~= (c t0 0 2 1 0 + c t1 0 2 0 1) / 2
221 t0 = tetrahedron cube 0
222 t1 = tetrahedron cube 1
225 -- | Given in Sorokina and Zeilfelder, p. 79, (2.7). See
226 -- 'prop_c0102_identity1'.
227 prop_c1101_identity :: Cube -> Bool
228 prop_c1101_identity cube =
229 c t0 1 1 0 1 ~= (c t0 1 0 1 1 + c t1 1 0 1 1) / 2
231 t0 = tetrahedron cube 0
232 t1 = tetrahedron cube 1
235 -- | Given in Sorokina and Zeilfelder, p. 79, (2.7). See
236 -- 'prop_c0102_identity1'.
237 prop_c1200_identity2 :: Cube -> Bool
238 prop_c1200_identity2 cube =
239 c t0 1 2 0 0 ~= (c t0 1 1 1 0 + c t1 1 1 0 1) / 2
241 t0 = tetrahedron cube 0
242 t1 = tetrahedron cube 1
245 -- | Given in Sorokina and Zeilfelder, p. 79, (2.7). See
246 -- 'prop_c0102_identity1'.
247 prop_c2100_identity2 :: Cube -> Bool
248 prop_c2100_identity2 cube =
249 c t0 2 1 0 0 ~= (c t0 2 0 1 0 + c t1 2 0 0 1) / 2
251 t0 = tetrahedron cube 0
252 t1 = tetrahedron cube 1
255 -- | Given in Sorokina and Zeilfelder, p. 79, (2.8). The third and
256 -- fourth indices of c-t6 have been switched. This is because we
257 -- store the triangles oriented such that their volume is
258 -- positive. If T and T-tilde share \<v0,v1,v2\> and v3,v3-tilde
259 -- point in opposite directions, one of them has to have negative
261 prop_c3000_identity :: Cube -> Bool
262 prop_c3000_identity cube =
263 c t0 3 0 0 0 ~= c t0 2 1 0 0 + c t6 2 1 0 0
264 - ((c t0 2 0 1 0 + c t0 2 0 0 1)/ 2)
266 t0 = tetrahedron cube 0
267 t6 = tetrahedron cube 6
270 -- | Given in Sorokina and Zeilfelder, p. 79, (2.8). See
271 -- 'prop_c3000_identity'.
272 prop_c2010_identity :: Cube -> Bool
273 prop_c2010_identity cube =
274 c t0 2 0 1 0 ~= c t0 1 1 1 0 + c t6 1 1 0 1
275 - ((c t0 1 0 2 0 + c t0 1 0 1 1)/ 2)
277 t0 = tetrahedron cube 0
278 t6 = tetrahedron cube 6
281 -- | Given in Sorokina and Zeilfelder, p. 79, (2.8). See
282 -- 'prop_c3000_identity'.
283 prop_c2001_identity :: Cube -> Bool
284 prop_c2001_identity cube =
285 c t0 2 0 0 1 ~= c t0 1 1 0 1 + c t6 1 1 1 0
286 - ((c t0 1 0 0 2 + c t0 1 0 1 1)/ 2)
288 t0 = tetrahedron cube 0
289 t6 = tetrahedron cube 6
292 -- | Given in Sorokina and Zeilfelder, p. 79, (2.8). See
293 -- 'prop_c3000_identity'.
294 prop_c1020_identity :: Cube -> Bool
295 prop_c1020_identity cube =
296 c t0 1 0 2 0 ~= c t0 0 1 2 0 + c t6 0 1 0 2
297 - ((c t0 0 0 3 0 + c t0 0 0 2 1)/ 2)
299 t0 = tetrahedron cube 0
300 t6 = tetrahedron cube 6
303 -- | Given in Sorokina and Zeilfelder, p. 79, (2.8). See
304 -- 'prop_c3000_identity'.
305 prop_c1002_identity :: Cube -> Bool
306 prop_c1002_identity cube =
307 c t0 1 0 0 2 ~= c t0 0 1 0 2 + c t6 0 1 2 0
308 - ((c t0 0 0 0 3 + c t0 0 0 1 2)/ 2)
310 t0 = tetrahedron cube 0
311 t6 = tetrahedron cube 6
314 -- | Given in Sorokina and Zeilfelder, p. 79, (2.8). See
315 -- 'prop_c3000_identity'.
316 prop_c1011_identity :: Cube -> Bool
317 prop_c1011_identity cube =
318 c t0 1 0 1 1 ~= c t0 0 1 1 1 + c t6 0 1 1 1 -
319 ((c t0 0 0 1 2 + c t0 0 0 2 1)/ 2)
321 t0 = tetrahedron cube 0
322 t6 = tetrahedron cube 6
326 -- | Given in Sorokina and Zeilfelder, p. 78.
327 prop_cijk1_identity :: Cube -> Bool
328 prop_cijk1_identity cube =
329 and [ c t0 i j k 1 ~=
330 (c t1 (i+1) j k 0) * ((b0 t0) (v3 t1)) +
331 (c t1 i (j+1) k 0) * ((b1 t0) (v3 t1)) +
332 (c t1 i j (k+1) 0) * ((b2 t0) (v3 t1)) +
333 (c t1 i j k 1) * ((b3 t0) (v3 t1)) | i <- [0..2],
338 t0 = tetrahedron cube 0
339 t1 = tetrahedron cube 1
342 -- | The function values at the interior should be the same for all
344 prop_interior_values_all_identical :: Cube -> Bool
345 prop_interior_values_all_identical cube =
346 all_equal [ eval (Tetrahedron.fv tet) I | tet <- tetrahedra cube ]
349 -- | We know what (c t6 2 1 0 0) should be from Sorokina and Zeilfelder, p. 87.
350 -- This test checks the rotation works as expected.
351 prop_c_tilde_2100_rotation_correct :: Cube -> Bool
352 prop_c_tilde_2100_rotation_correct cube =
355 t0 = tetrahedron cube 0
356 t6 = tetrahedron cube 6
358 -- What gets computed for c2100 of t6.
359 expr1 = eval (Tetrahedron.fv t6) $
361 (1/12)*(T + R + L + D) +
362 (1/64)*(FT + FR + FL + FD) +
365 (1/96)*(RT + LD + LT + RD) +
366 (1/192)*(BT + BR + BL + BD)
368 -- What should be computed for c2100 of t6.
369 expr2 = eval (Tetrahedron.fv t0) $
371 (1/12)*(F + R + L + B) +
372 (1/64)*(FT + RT + LT + BT) +
375 (1/96)*(FR + FL + BR + BL) +
376 (1/192)*(FD + RD + LD + BD)
379 -- | We know what (c t6 2 1 0 0) should be from Sorokina and
380 -- Zeilfelder, p. 87. This test checks the actual value based on
381 -- the FunctionValues of the cube.
383 -- If 'prop_c_tilde_2100_rotation_correct' passes, then this test is
385 prop_c_tilde_2100_correct :: Cube -> Bool
386 prop_c_tilde_2100_correct cube =
387 c t6 2 1 0 0 == expected
389 t0 = tetrahedron cube 0
390 t6 = tetrahedron cube 6
391 fvs = Tetrahedron.fv t0
392 expected = eval fvs $
394 (1/12)*(F + R + L + B) +
395 (1/64)*(FT + RT + LT + BT) +
398 (1/96)*(FR + FL + BR + BL) +
399 (1/192)*(FD + RD + LD + BD)
402 -- Tests to check that the correct edges are incidental.
403 prop_t0_shares_edge_with_t1 :: Cube -> Bool
404 prop_t0_shares_edge_with_t1 cube =
405 (v1 t0) == (v1 t1) && (v3 t0) == (v2 t1)
407 t0 = tetrahedron cube 0
408 t1 = tetrahedron cube 1
410 prop_t0_shares_edge_with_t3 :: Cube -> Bool
411 prop_t0_shares_edge_with_t3 cube =
412 (v1 t0) == (v1 t3) && (v2 t0) == (v3 t3)
414 t0 = tetrahedron cube 0
415 t3 = tetrahedron cube 3
417 prop_t0_shares_edge_with_t6 :: Cube -> Bool
418 prop_t0_shares_edge_with_t6 cube =
419 (v2 t0) == (v3 t6) && (v3 t0) == (v2 t6)
421 t0 = tetrahedron cube 0
422 t6 = tetrahedron cube 6
424 prop_t1_shares_edge_with_t2 :: Cube -> Bool
425 prop_t1_shares_edge_with_t2 cube =
426 (v1 t1) == (v1 t2) && (v3 t1) == (v2 t2)
428 t1 = tetrahedron cube 1
429 t2 = tetrahedron cube 2
431 prop_t1_shares_edge_with_t19 :: Cube -> Bool
432 prop_t1_shares_edge_with_t19 cube =
433 (v2 t1) == (v3 t19) && (v3 t1) == (v2 t19)
435 t1 = tetrahedron cube 1
436 t19 = tetrahedron cube 19
438 prop_t2_shares_edge_with_t3 :: Cube -> Bool
439 prop_t2_shares_edge_with_t3 cube =
440 (v1 t1) == (v1 t2) && (v3 t1) == (v2 t2)
442 t1 = tetrahedron cube 1
443 t2 = tetrahedron cube 2
445 prop_t2_shares_edge_with_t12 :: Cube -> Bool
446 prop_t2_shares_edge_with_t12 cube =
447 (v2 t2) == (v3 t12) && (v3 t2) == (v2 t12)
449 t2 = tetrahedron cube 2
450 t12 = tetrahedron cube 12
452 prop_t3_shares_edge_with_t21 :: Cube -> Bool
453 prop_t3_shares_edge_with_t21 cube =
454 (v2 t3) == (v3 t21) && (v3 t3) == (v2 t21)
456 t3 = tetrahedron cube 3
457 t21 = tetrahedron cube 21
459 prop_t4_shares_edge_with_t5 :: Cube -> Bool
460 prop_t4_shares_edge_with_t5 cube =
461 (v1 t4) == (v1 t5) && (v3 t4) == (v2 t5)
463 t4 = tetrahedron cube 4
464 t5 = tetrahedron cube 5
466 prop_t4_shares_edge_with_t7 :: Cube -> Bool
467 prop_t4_shares_edge_with_t7 cube =
468 (v1 t4) == (v1 t7) && (v2 t4) == (v3 t7)
470 t4 = tetrahedron cube 4
471 t7 = tetrahedron cube 7
473 prop_t4_shares_edge_with_t10 :: Cube -> Bool
474 prop_t4_shares_edge_with_t10 cube =
475 (v2 t4) == (v3 t10) && (v3 t4) == (v2 t10)
477 t4 = tetrahedron cube 4
478 t10 = tetrahedron cube 10
480 prop_t5_shares_edge_with_t6 :: Cube -> Bool
481 prop_t5_shares_edge_with_t6 cube =
482 (v1 t5) == (v1 t6) && (v3 t5) == (v2 t6)
484 t5 = tetrahedron cube 5
485 t6 = tetrahedron cube 6
487 prop_t5_shares_edge_with_t16 :: Cube -> Bool
488 prop_t5_shares_edge_with_t16 cube =
489 (v2 t5) == (v3 t16) && (v3 t5) == (v2 t16)
491 t5 = tetrahedron cube 5
492 t16 = tetrahedron cube 16
494 prop_t6_shares_edge_with_t7 :: Cube -> Bool
495 prop_t6_shares_edge_with_t7 cube =
496 (v1 t6) == (v1 t7) && (v3 t6) == (v2 t7)
498 t6 = tetrahedron cube 6
499 t7 = tetrahedron cube 7
501 prop_t7_shares_edge_with_t20 :: Cube -> Bool
502 prop_t7_shares_edge_with_t20 cube =
503 (v2 t7) == (v3 t20) && (v2 t7) == (v3 t20)
505 t7 = tetrahedron cube 7
506 t20 = tetrahedron cube 20