def scalar

stelliferous@0.0.2.0 · proofs/traversal_lanes_refinement.bend:154

import Base
import stelliferous@0.0.2.0/traversal_array.bend as Traversal
import stelliferous@0.0.2.0/traversal_loop.bend as Loop
import stelliferous@0.0.2.0/proofs/traversal_batch_refinement.bend as Batch
import stelliferous@0.0.2.0/proofs/traversal_array_refinement.bend as ArrayLaws
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

154def scalar(~Context: Data,~map: Context -> F32 -> F32,+count: Nat,+position: U32,+context: Context,+values: Tree.Tree<F32>) ->
155  {Traversal.map_in_place(~F32,~Context,~map,count,position,context,Tree.pack(F32,values)) ==
156    Tree.pack(F32,MapReadback.run(~F32,~Context,~map,count,position,context,values)) : Array<F32>}:
157  +initial = {Traversal.State{Unit{},values,position,context} : Batch.ModelState(~F32,~Context)}
158  %Equal.sym(Traversal.State<&2,&1,Unit,Array<F32>,Context>,
159    Loop.run(~Traversal.State<&2,&1,Unit,Array<F32>,Context>,~Traversal.map_step(~F32,~Context,~map),count,Traversal.State{Unit{},Tree.pack(F32,values),position,context}),
160    ArrayLaws.represent_map(~F32,~Context,Loop.run(~Batch.ModelState(~F32,~Context),~ArrayLaws.model_map_step(~F32,~Context,~ArrayLaws.unindexed(~F32,~Context,~map)),count,initial)),
161    ArrayLaws.map_loop_refines_model(~F32,~Context,~map,count,initial)) :
162    {Traversal.mapped_output(~F32,~Context,_) == Tree.pack(F32,MapReadback.run(~F32,~Context,~map,count,position,context,values)) : Array<F32>}
163  output(~Context,Loop.run(~Batch.ModelState(~F32,~Context),~ArrayLaws.model_map_step(~F32,~Context,~ArrayLaws.unindexed(~F32,~Context,~map)),count,initial))