118def planNativePhysicalMemory =
119 (lambda unrestricted state : Nat .
120 (lambda unrestricted slots : Nat .
121 (lambda unrestricted depth : Nat .
122 (eliminate
123 StdBool
124 (lambda unrestricted flag : (family StdBool) .
125 (family
126 StdResult
127 (family NativePhysicalMemoryFailure)
128 (family NativePhysicalMemoryLayout)))
129 (stdBoolFromNatural (naturalNonzero state))
130 (branch
131 StdTrue
132 .
133 (eliminate
134 StdBool
135 (lambda unrestricted flag : (family StdBool) .
136 (family
137 StdResult
138 (family NativePhysicalMemoryFailure)
139 (family NativePhysicalMemoryLayout)))
140 (stdBoolFromNatural (nativePhysicalMemoryAdmitted state slots depth))
141 (branch
142 StdTrue
143 .
144 (let unrestricted slotBytes =
145 (naturalMultiply slots nativePhysicalMemoryWordBytes)
146 in
147 (let unrestricted scratch =
148 (naturalAdd state slotBytes)
149 in
150 (constructor
151 StdResult
152 StdSuccess
153 (family NativePhysicalMemoryFailure)
154 (family NativePhysicalMemoryLayout)
155 (constructor
156 NativePhysicalMemoryLayout
157 NativePhysicalMemoryLayoutOf
158 state
159 slotBytes
160 scratch
161 (naturalAdd scratch (nativePhysicalRepeatScratchBytes depth)))))))
162 (branch
163 StdFalse
164 .
165 (constructor
166 StdResult
167 StdFailure
168 (family NativePhysicalMemoryFailure)
169 (family NativePhysicalMemoryLayout)
170 (constructor NativePhysicalMemoryFailure NativePhysicalMemoryOverflow)))))
171 (branch
172 StdFalse
173 .
174 (constructor
175 StdResult
176 StdFailure
177 (family NativePhysicalMemoryFailure)
178 (family NativePhysicalMemoryLayout)
179 (constructor NativePhysicalMemoryFailure NativePhysicalMemoryEmpty)))))))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.