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
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
#[test]
pub fn listing0 () { fgi_listing_test![
decls {
/// Lists of natural numbers
type List = (+ Unit + (x Nat x List));
type LazyList = (Thk[0] 0 F (+ Unit + (x Nat x LazyList)));
//uses explicit LazyList type b/c of force bug docced earlier
type Queue = (x (Thk[0] 0 F (+ Unit + (x Nat x LazyList))) x List x LazyList);
type OpNat = (+ Unit + Nat );
type OpQueue = (+ Unit + Queue );
}
let cons_ll:(
Thk[0]
0 Nat ->
0 LazyList ->
0 F LazyList
) = {
ret thunk #h.#l. ret thunk ret roll inj2 (h, l)
}
let cons:(
Thk[0] 0 Nat -> 0 List -> 0 F List
) = {
ret thunk #h.#t. ret roll inj2 (h, t)
}
let lazynil:(
Thk[0] 0 F LazyList
) = {
ret thunk ret thunk ret roll inj1 ()
}
let nil:(
Thk[0] 0 F List
) = {
ret thunk ret roll inj1 ()
}
let empty:(
Thk[0] 0 F Queue
) = {
//ret thunk ret (ret roll inj1 ret thunk (), ret roll inj1 (), ret roll inj1 ret thunk ())
//ret thunk ret (ret thunk ret roll inj1 (), ret roll inj1 (), ret thunk ret roll inj1 ())
let ll = {force lazynil}
let l = {force nil}
ret thunk ret (ll, l, ll) //TODO: what's up with this?
}
let is_empty_lazylist:(
Thk[0]
0 (Thk[0] 0 F (+ Unit + (x Nat x LazyList))) ->
0 F Bool
) = {
ret thunk #ll.
let fl = {force ll}
unroll match fl {
_u => { ret true }
c => { ret false }
}
}
let is_empty:(
Thk[0]
0 Queue ->
0 F Bool
) = {
ret thunk #q.
let (front, back, sched) = q
{{force is_empty_lazylist} front}
}
let peek:(
Thk[0]
0 Queue ->
0 F OpNat
) = {
ret thunk #q.
let (front, back, sched) = q
let ffront = {force front}
unroll match ffront {
_u => {ret inj1 ()}
c => {
let (h, tl) = { ret c }
ret inj2 h
}
}
}
let rec rotate:(
Thk[0]
0 (Thk[0] 0 F (+ Unit + (x Nat x LazyList))) ->
0 List ->
0 LazyList ->
0 F LazyList
) = {
#f.#b.#s.
unroll match b {
_u => { {force lazynil} } //ERROR CASE: SHOULD NOT HAPPEN
c => {
let (y, ys) = { ret c }
let scons = {{force cons_ll} y s}
let ff = { force f }
unroll match ff {
_u => { ret scons } //base case
d => {
let (x, xs) = { ret d }
//TODO: this is stack overflowing
let rtl = {{force rotate} xs ys scons}
{{force cons_ll} x rtl}
}
}
}
}
}
let exec:(
Thk[0]
//f needs to be explicit b/c rotate's first arg is?
0 (Thk[0] 0 F (+ Unit + (x Nat x LazyList))) ->
0 List ->
0 (Thk[0] 0 F (+ Unit + (x Nat x LazyList))) ->
0 F Queue
) = {
ret thunk #f.#b.#s.
let fs = { force s }
unroll match fs {
_u => {
let ln = {force lazynil}
let fr = {{force rotate} f b ln}
let n = {force nil}
ret (fr, n, fr)
}
c => {
let (w, ss) = { ret c }
ret (f, b, ss)
}
}
}
let enqueue:(
Thk[0]
0 Nat ->
0 Queue ->
0 F Queue
) = {
ret thunk #n.#q.
let (front, back, sched) = q
let aback = {{force cons} n back}
{{force exec} front aback sched}
}
//TODO: why does OpQueue version not work?
let dequeue:(
Thk[0]
0 Queue ->
0 F Queue
) = {
ret thunk #q.
let (front, back, sched) = q
let ff = {force front}
unroll match ff {
_u => { {force empty} }
c => {
let (h, tl) = { ret c }
{{force exec} tl back sched}
}
}
}
ret 0
]}