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
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
#[test]
pub fn listing () { fgi_listing_test![
decls {
/// Optional natural numbers:
type OpNat = (+ Unit + Nat );
/// Levels (as numbers), for level trees.
type Lev = ( Nat )
/// Sequences (balanced binary level trees), whose leaves
/// are optional natural numbers:
type Seq = (
rec seq. foralli (X,Y):NmSet.
(+ (+ Unit + Nat)
+ (exists (X1,X2,X3) :NmSet | ((X1%X2%X3)=X:NmSet).
exists (Y1,Y2,Y3,Y4):NmSet | ((Y1%Y2%Y3%Y4)=Y:NmSet).
x Nm[X1] x Lev
x Ref[Y1](seq[X2][Y2])
x Ref[Y3](seq[X3][Y4]))
)
);
/// Pointers written for each name in a structural recursion
/// (-`_SR`) over a sequence:
idxtm Seq_SR = ( #x:Nm.({x,@1})%({x,@2}) );
/// ... prefixed with the current write scope (`WS`-), named
/// `@!` below, as a nameset-level function
idxtm WS_Seq_SR = ( #x:NmSet.{@!}((Seq_SR) x) );
/// ... same, but just the first recursive call
idxtm WS_Seq_SR1 = ( #x:NmSet.[@@](x * {@1}));
//idxtm WS_Seq_SR1 = ( #x:NmSet.{@!}(x * {@1}));
//-- TODO: Add equations to make this work too, e.g., [@@]( i ) == {@!}( i )
/// ... second recursive call
idxtm WS_Seq_SR2 = ( #x:NmSet.[@@](x * {@2}));
//idxtm WS_Seq_SR2 = ( #x:NmSet.{@!}(x * {@2}));
//-- TODO: Make this work too.
/// Filter an optional natural number, using a natural number predicate
fn opnat_filter_nat:(
Thk[0] 0 OpNat ->
0 (Thk[0] 0 Nat -> 0 F Bool) ->
0 F OpNat
) = {
#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 ()
}
}
}
}
fn is_empty:(
Thk[0] foralli (X,Y):NmSet.
0 (Seq[X][Y]) -> { 0; Y } F Bool
) = { unimplemented }
}
// Filter a sequence (of optional natural numbers) using a
// predicate over natural numbers
let filter:(
Thk[0] foralli (X,Y):NmSet.
0 Seq[X][Y] ->
0 (Thk[0] 0 Nat -> 0 F Bool) ->
{ {WS_Seq_SR} X; Y }
F Seq[X][{WS_Seq_SR} X]
) = {
ret thunk fix filter. #seq. #f. unroll match seq {
on => {
let on = {{force opnat_filter_nat} on f}
ret roll inj1 on
}
bin => {
unpack (X1,X2,X3,Y1,Y2,Y3,Y4) bin = bin
let (n,lev,l,r) = {ret bin}
let (rsl, sl) = { memo{n,(@1)}{ {force filter}[X2][Y2]{!l} f } }
let (rsr, sr) = { memo{n,(@2)}{ {force filter}[X3][Y4]{!r} f } }
if {{force is_empty}[X2][({WS_Seq_SR} X2)] sl} {
ret sr
} else {if {{force is_empty}[X3][({WS_Seq_SR} X3)] sr} {
ret sl
} else {
ret roll inj2 pack (
X1, X2, X3,
{WS_Seq_SR1} X1, {WS_Seq_SR} X2,
{WS_Seq_SR2} X1, {WS_Seq_SR} X3
)(n,lev,rsl,rsr)
}}
}
}
}
ret 0
]}