1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
#[test]
pub fn listing0 () { fgi_listing_test![
decls {
/// Optional natural numbers
type OpNat = (+ Unit + Nat );
/// Optional pairs of natural numbers
type Op2Nat = (+ Unit + (x Nat x Nat));
}
// Split an optional pair of natural into a pair of optional naturals
let opnat_split:(
Thk[0] 0 Op2Nat -> 0 F (x OpNat x OpNat)
) = {
ret thunk #xyo. match (xyo) {
_u => {
ret (inj1 (), inj1 ())
}
xy => {
let (x,y) = { ret xy }
ret (inj2 x, inj2 y)
}}
}
// Pair two optional naturals into an optional pair of naturals
let opnat_pair:(
Thk[0] 0 (x OpNat x OpNat) -> 0 F (Op2Nat)
) = {
ret thunk #xoyo. let (xo,yo) = { ret xoyo }
match (xo) {
_u => { ret inj1 () }
x => { match (yo) {
_u => { ret inj1 () }
y => { ret inj2 (x,y) }
}}
}
}
// Filter an optional natural number, using a natural number predicate
let opnat_filter_nat:(
Thk[0] 0 OpNat ->
0 (Thk[0] 0 Nat -> 0 F Bool) ->
0 F OpNat
) = {
ret thunk #opnat.#pred.
match opnat {
_u => {
// no number to filter
ret inj1 ()
}
n => {
// apply user-supplied predicate
if {{force pred} n} {
// keep the number n
ret inj2 n
} else {
// filter out the number n
ret inj1 ()
}
}
}
}
// Compute the maximum optional natural number (among a pair)
let opnat_max:(
Thk[0] 0 OpNat -> 0 OpNat -> 0 F OpNat
) = {
ret thunk #xo.#yo.
match (xo) {
_u => { ret yo }
x => { match (yo) {
_u => { ret yo }
y => {
if { x < y } {ret yo}
else {ret xo}
}
}}
}
}
ret 0
]}