A general program may have no application arena. The capture arena
must not invent an empty resident merely to certify that valid shape.
125def captureArenaResidents =
126 (lambda unrestricted applicationBytes : Nat .
127 (lambda unrestricted ordinaryCapacity : Nat .
128 (lambda unrestricted reservedCapacity : Nat .
129 (aosChoose
130 (family ArenaResidents)
131 (naturalIsZero applicationBytes)
132 (constructor
133 ArenaResidents
134 ArenaResidentsNext
135 (constructor
136 ArenaResident
137 ArenaResidentValue
138 b"capture-control"
139 (captureControlAt applicationBytes)
140 captureControlBytes
141 captureWordBytes)
142 (constructor
143 ArenaResidents
144 ArenaResidentsNext
145 (constructor
146 ArenaResident
147 ArenaResidentValue
148 b"capture-queue"
149 (captureQueueAt applicationBytes)
150 (captureQueueBytes ordinaryCapacity reservedCapacity)
151 captureWordBytes)
152 (constructor
153 ArenaResidents
154 ArenaResidentsNext
155 (constructor
156 ArenaResident
157 ArenaResidentValue
158 b"capture-values"
159 (captureValuesScratchAt applicationBytes ordinaryCapacity reservedCapacity)
160 captureValuesBytes
161 captureWordBytes)
162 (constructor ArenaResidents ArenaResidentsEnd))))
163 (constructor
164 ArenaResidents
165 ArenaResidentsNext
166 (constructor ArenaResident ArenaResidentValue b"application" 0 applicationBytes 1)
167 (constructor
168 ArenaResidents
169 ArenaResidentsNext
170 (constructor
171 ArenaResident
172 ArenaResidentValue
173 b"capture-control"
174 (captureControlAt applicationBytes)
175 captureControlBytes
176 captureWordBytes)
177 (constructor
178 ArenaResidents
179 ArenaResidentsNext
180 (constructor
181 ArenaResident
182 ArenaResidentValue
183 b"capture-queue"
184 (captureQueueAt applicationBytes)
185 (captureQueueBytes ordinaryCapacity reservedCapacity)
186 captureWordBytes)
187 (constructor
188 ArenaResidents
189 ArenaResidentsNext
190 (constructor
191 ArenaResident
192 ArenaResidentValue
193 b"capture-values"
194 (captureValuesScratchAt applicationBytes ordinaryCapacity reservedCapacity)
195 captureValuesBytes
196 captureWordBytes)
197 (constructor ArenaResidents ArenaResidentsEnd)))))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.