def pair

stelliferous@0.0.2.0 · proofs/kernel_tile_witness.bend:6

import Base
import stelliferous@0.0.2.0/kernel_block.bend as Block
import stelliferous@0.0.2.0/proofs/traversal_witness.bend as TraversalWitness

6# Pair composition consumes already established observations. Context and
7# values may be erased, so a cached head need not become a live proof field.
8def pair(~State: Type,~Context: Data,~Element: Data,~read: State -> Context -> Nat -> State & Element,~stride: Nat,
9  -state: State,-context: Context,+index: Nat,
10  first: TraversalWitness.Sample<State,Element,state,read(state,context,index)>,
11  second: TraversalWitness.Sample<State,Element,state,read(state,context,Nat.add(index,stride))>) ->
12  TraversalWitness.Sample<State,Block.Twin<Element>,state,Block.read_pair(~State,~Context,~Element,~read,~stride,state,context,index)>:
13  TraversalWitness.Sample{left,left_equation} = first
14  TraversalWitness.Sample{right,right_equation} = second
15  %Equal.sym(State & Element,read(state,context,index),(state,left),left_equation) :
16    TraversalWitness.Sample<State,Block.Twin<Element>,state,Block.read_second(~State,~Context,~Element,~Nat,~read,_,context,Nat.add(index,stride))>
17  %Equal.sym(State & Element,read(state,context,Nat.add(index,stride)),(state,right),right_equation) :
18    TraversalWitness.Sample<State,Block.Twin<Element>,state,Block.finish_pair(~State,~Element,left,_)>
19  TraversalWitness.Sample{Block.Twin{left,right},{==}}