Unsupported branches above are excluded by nativePointwiseProgram's erased
admission proof. Inputs name existing slots; every other node materializes a
fresh temporary. Explicit assignments then make their result visible to the
next expression, using the same dependency order as the SM86 realization.
281def nativePointwiseExpression =
282 (lambda unrestricted slots : Nat .
283 (lambda unrestricted base : Nat .
284 (lambda unrestricted scratch : Nat .
285 (lambda unrestricted expression : (family PointwiseExpression StdU64 slots) .
286 (pointwiseFold
287 StdU64
288 (pi unrestricted next : Nat . (family NativePointwiseFragment))
289 slots
290 (lambda unrestricted operation : (family PointwiseUnary) .
291 (lambda unrestricted operand : (pi unrestricted next : Nat . (family NativePointwiseFragment)) .
292 (lambda unrestricted next : Nat .
293 (let unrestricted child =
294 (operand next)
295 in
296 (constructor
297 NativePointwiseFragment
298 NativePointwiseFragmentOf
299 (lambda unrestricted tail : (family NativePhysicalCommands) .
300 (nativePointwiseCode
301 child
302 (nativePointwiseUnary
303 scratch
304 operation
305 (nativePointwiseEnd child)
306 (nativePointwiseResult child)
307 tail)))
308 (nativePointwiseEnd child)
309 (nativePointwiseAt (nativePointwiseEnd child) 1))))))
310 (lambda unrestricted operation : (family PointwiseBinary) .
311 (lambda unrestricted left : (pi unrestricted next : Nat . (family NativePointwiseFragment)) .
312 (lambda unrestricted right : (pi unrestricted next : Nat . (family NativePointwiseFragment)) .
313 (lambda unrestricted next : Nat .
314 (let unrestricted l =
315 (left next)
316 in
317 (let unrestricted r =
318 (right (nativePointwiseEnd l))
319 in
320 (constructor
321 NativePointwiseFragment
322 NativePointwiseFragmentOf
323 (lambda unrestricted tail : (family NativePhysicalCommands) .
324 (nativePointwiseCode
325 l
326 (nativePointwiseCode
327 r
328 (nativePointwiseBinary
329 scratch
330 operation
331 (nativePointwiseEnd r)
332 (nativePointwiseResult l)
333 (nativePointwiseResult r)
334 tail))))
335 (nativePointwiseEnd r)
336 (nativePointwiseAt (nativePointwiseEnd r) 1))))))))
337 (lambda unrestricted bits : StdU64 .
338 (lambda unrestricted next : Nat .
339 (constructor
340 NativePointwiseFragment
341 NativePointwiseFragmentOf
342 (nativeMemoryStoreWord64
343 b"pointwise-literal"
344 next
345 (nativeLaunchRecipeImmediate (modelWord64Natural bits)))
346 next
347 (nativePointwiseAt next 1))))
348 expression
349 (lambda unrestricted index : (family StdFin slots) .
350 (lambda unrestricted next : Nat .
351 (constructor
352 NativePointwiseFragment
353 NativePointwiseFragmentOf
354 (lambda unrestricted tail : (family NativePhysicalCommands) . tail)
355 (nativePointwiseAt base (stdFinToNatural slots index))
356 next))))))))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.