TraversalLanesRefinement.map: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/traversal_lanes_refinement.bend as TraversalLanesRefinement
Lines 293-305 of stelliferous@0.0.2.0/proofs/traversal_lanes_refinement.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/traversal_lanes_refinement.bend&start_line=293&end_line=305

import Base
import stelliferous@0.0.2.0/traversal_lanes.bend as Lanes
import stelliferous@0.0.2.0/traversal_cells.bend as Cells
import stelliferous@0.0.2.0/traversal_array.bend as Traversal
import stelliferous@0.0.2.0/kernel_tile.bend as Tile
import stelliferous@0.0.2.0/proofs/traversal_map_readback.bend as MapReadback
import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree
import stelliferous@0.0.2.0/proofs/storage_refinement.bend as StorageLaws
import stelliferous@0.0.2.0/proofs/storage_shape.bend as Shape
import stelliferous@0.0.2.0/proofs/nat_order.bend as Order
import stelliferous@0.0.2.0/proofs/word_power_of_two.bend as Power

# The whole map from any position, with a fresh scratch array.
def map(~Context: Data,~map: Context -> F32 -> F32,+count: Nat,+start: Nat,+context: Context,+values: Tree.Tree<F32>,+depth: Nat,+balanced: Shape.Balanced(F32,depth,values),
  +limit: {Nat.is_le(depth,30n) == True{} : Bool},+room: {Nat.is_le(Nat.add(start,count),U32.to_nat(U32.shln(1,depth))) == True{} : Bool}) ->
  {Lanes.map(~Context,~map,count,U32.from_nat(start),context,Tree.pack(F32,values)) ==
    Traversal.map_in_place(~F32,~Context,~map,count,U32.from_nat(start),context,Tree.pack(F32,values)) : Array<F32>}:
  +position = U32.from_nat(start)
  %Equal.sym(Array<F32>,Traversal.map_in_place(~F32,~Context,~map,count,position,context,Tree.pack(F32,values)),Tree.pack(F32,MapReadback.run(~F32,~Context,~map,count,position,context,values)),
    scalar(~Context,~map,count,position,context,values)) :
    {Lanes.map(~Context,~map,count,position,context,Tree.pack(F32,values)) == _ : Array<F32>}
  %Equal.sym(Array<Tile.Tile8>,Array.new(Tile.Tile8,6n,Tile.filled(0.0)),Tree.pack(Tile.Tile8,Tree.fresh(Tile.Tile8,6n,Tile.filled(0.0))),StorageLaws.fresh(Tile.Tile8,6n,Tile.filled(0.0))) :
    {Lanes.rounds(~Context,~map,count,Cells.State{Tree.pack(F32,values),_,position,0,context}) == Tree.pack(F32,MapReadback.run(~F32,~Context,~map,count,position,context,values)) : Array<F32>}
  rounds(~Context,~map,count,start,0,context,values,Tree.fresh(Tile.Tile8,6n,Tile.filled(0.0)),depth,U32.shln(1,depth),Shape.capacity(F32,depth,values,balanced),balanced,limit,
    Power.native_power_bound(depth,Order.successor(depth,30n,limit)),room)

Uses (28):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.new
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shln
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_tile.bend&name=Tile8
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_tile.bend&name=filled
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_order.bend&name=successor
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_refinement.bend&name=fresh
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_shape.bend&name=Balanced
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_shape.bend&name=capacity
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=Tree
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=fresh
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=pack
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_lanes_refinement.bend&name=rounds
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_lanes_refinement.bend&name=scalar
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_map_readback.bend&name=run
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_power_of_two.bend&name=native_power_bound
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_array.bend&name=map_in_place
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_cells.bend&name=State
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_lanes.bend&name=map
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_lanes.bend&name=rounds