Commit | Line | Data |
---|---|---|
7f918cf1 CE |
1 | datatype b = TRUE | FALSE |
2 | ||
3 | datatype nat = Z | S of nat | |
4 | ||
5 | fun lt (Z, S _) = TRUE | |
6 | | lt (S n1, S n2) = lt (n1, n2) | |
7 | | lt _ = FALSE | |
8 | ||
9 | fun ZZZ_f (a, b) = lt (#value a, #value b) | |
10 | ||
11 | fun ZZZ_copyTo (array, record as {value, offset}) = | |
12 | fn S Z => {value = value, offset = S (S (S Z))} | |
13 | | n => array n | |
14 | ||
15 | fun ZZZ_fixTooBig (array, record) = | |
16 | let | |
17 | val left = array (S Z) | |
18 | val right = array (S (S Z)) | |
19 | val small = | |
20 | case ZZZ_f (left, right) of | |
21 | TRUE => left | |
22 | | FALSE => right | |
23 | in | |
24 | case ZZZ_f (record, small) of | |
25 | TRUE => ZZZ_copyTo (array, record) | |
26 | | FALSE => ZZZ_copyTo (array, small) | |
27 | end |