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
107
108
109
#[test]
pub fn listing () { fgi_listing_expect![[Expect::Failure]
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]))
)
);
/// Sets (balanced binary hash tries), whose leaves are
/// optional natural numbers:
type Set = (
rec set. 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 Ref[Y1](set[X2][Y2])
x Ref[Y3](set[X3][Y4]))
)
);
/// Structural recursion over a binary tree (output names and pointers):
idxtm Bin = (#x:Nm. {x,@1} % {x,@2} );
idxtm WS_Bin = (#x:NmSet.{@!}( (Bin) x ));
/// Trie_join: Index functions for output names and pointers:
idxtm Join = (#x:NmSet. ( (Bin)((Bin)^* x)));
idxtm WS_Join = (#x:NmSet.{@!}( {Join} x ));
/// Trie_of_seq: Index functions for output names and pointers:
idxtm Trie = (#x:NmSet. ( {Join} x ));
idxtm WS_Trie = (#x:NmSet.{@!}( {Join} x ));
}
let join:(
Thk[0] foralli (X0, X1, X2, Y1, Y2):NmSet.
0 Nm[X0] ->
0 Set[X1][Y1] ->
0 Set[X2][Y2] ->
{
({WS_Bin} X0)
% ({WS_Join} (X1%X2))
;
Y1 % Y2
% ({WS_Bin} X0)
% ({WS_Join} (X1%X2))
}
F Set
[(Join)(X1 % X2)]
[{WS_Join}(X1 % X2)]
) = {
ret thunk fix join. #nm. #set1. #set2. match set1 {
on1 => { match set2 {
on2 => { unimplemented }
bin2 => { unimplemented }
}}
bin1 => { match set2 {
on2 => { unimplemented }
bin2 => {
// XXX
unimplemented
}
}}
}
}
let trie:(
Thk[0] foralli (X,Y):NmSet.
0 Seq[X][Y] ->
{
{WS_Trie} X
;
Y % ( {WS_Trie} X )
}
F Set[X][{WS_Trie} X]
) = {
ret thunk fix trie. #seq. match seq {
on => { ret roll inj1 on }
bin => {
unpack (X1,X2,X3,Y1,Y2,Y3,Y4) bin = bin
let (n,lev,l,r) = {ret bin}
let (rsl, _l) = { memo{n,(@1)}{ {force trie}[X2][Y2]{!l} } }
let (rsr, _r) = { memo{n,(@2)}{ {force trie}[X3][Y4]{!r} } }
let trie = { ws (nmfn [#x:Nm. ~n * x]) {
{force join}
[({Trie}X2)][({Trie}X3)][({WS_Trie}X2)][({WS_Trie}X3)]
{!rsl} {!rsr}
}}
ret trie
}
}
}
ret 0
]}