bendtorch-core

Releases (1)

• 0.1.0.0 indexed

Definitions (5,204)

src/autograd/reduce_parallel_proof.bend

• def visited_ofThe offsets the walk of cell `position` reads.
• type CellAtWhat target cell `position` holds: below `count`, the total of the words its walk saw, from +0.0; at or above it, +0.0.
• def CellSpec
• def CellIs
• def Cells
• def cell_ofThe reduce cell function of `Parallel.build`, from the contribution array.
• def keep_equal
• def run_of
• def cell_keepsEvery cell hands the contribution array back.
• def cell_specWhat the cell function computes is what CellSpec names.
• def halves_equalA split hands each half the contribution array.
• def build_cellsWhatever the split, every cell of the parallel build holds what CellIs names: the generic law of `Parallel.build`, with the reduce cell.
• def ReadsThe words a walk saw are the contribution's words at the offsets it read.
• def obs_gather
• def cell_valueA cell of the parallel build holds `ReduceLaws.fiber`: the words its walk saw add up, from +0.0, to the masked fold over the contribution.

src/autograd/reduce_replayed_proof.bend

• def PlanMap
• def rfoldThe replayed words at a list of offsets, added in order.
• def map_word
• def cell_word
• def writes
• def writes_value
• def lt_not_eq
• def write_skipA write at an index below `index` leaves the word at `index`.
• def writes_zeroAt or above the count, the writes leave the +0.0 fill.
• def lt_zero_false
• def lt_self_succ
• def lt_succ_right
• def above_falsek < b gives b < 1 + k false.
• def lt_asym
• def below_true1 + b <= k gives b < k.
• def lt_add_right
• def le_add_cong
• def le_trans
• def position_step
• def add_zero_right
• def output_positionA word index below the storage length is the offset of its own route.
• def out_leaf
• def out_spec
• def out_balanced
• def new_spec
• def aboveA subtree whose positions all lie above k is the same for k and 1 + k.
• def belowA subtree whose positions all lie below k is the same for k and 1 + k.
• def write_specWriting cell k at the path whose position is k turns the spec for k into the spec for 1 + k.
• def chainThe family history, replayed on the owned storage that `created` makes, is the owned storage that holds the output spec.
• def below_front
• def below_back
• def rfold_append
• def leaf_eq
• def next_eq
• def fiber_eq
• def etaThe facts of `ReduceParallel.fast_fiber`, stated for the replayed arrays `Api.arr`, which a proof can name as often as it needs: a read of `Api.arr(h, d, f)` hands back that array, next to the word it read.
• def got
• def single_arr
• def word_atThe word a strided read of `Api.arr(h, d, f)` gets.
• def step_arr
• def run_arr
• def strided_arr
• def fiber_keptA fiber of `Api.arr(h, d, f)` hands that array back.
• def fast_arr
• type FactsWhat the cells of the build need from the plan: the target is the plan's left shape, with `count` cells, and the contribution is its right shape.
• def walk_belowEvery offset the walk of a cell below `count` reads lies inside the contribution.
• def TreeEq
• def cell_eq
• def tree_join_eq
• def tree_node_eq
• def pair_join_eqThe depth-1 tree: the leaf of cell `base` and the leaf of the cell after it, which reads the state the first hands back.
• def pair_eq
• def tree_eq
• def tree_first
• def fork_eq
• def build_eqWhatever the split, the parallel build over the copy returns the spec.
• def length_snocAs in reduce_fold_PROOF.bend: below the count, the listed words are the replayed words.
• def words_length
• def word_at_front
• def word_at_last
• def words_step
• def words_at
• def parallel_splits
• def output_eqThe writes of every cell, replayed on the owned storage `created` makes for the target, give the owned storage the parallel build fills.
• def FinalThe parallel reduce over a replayed contribution, in transport form: P holds for the result if it holds for the contribution replayed with any history that keeps its words, next to the target replayed with any history whose cells hold the cell words.
• def room_of
• def inside_count
• def indexed_lift
• def rfold_gather
• def word_fiber

src/autograd/reduce_to_fold_PROOF.bend

• def planned_shapes
• def shapes_construct
• def shapes_align
• def shapes_checked
• def first
• def second
• def plan_shapes
• def plan_left
• def plan_right
• def target_index
• def source_index
• def target_belowContribution position `position` lands on a target cell below the target's count.
• def source_below
• def some_injective
• def indices_found