def update_sample

stelliferous@0.0.2.0 · proofs/traversal_witness.bend:105

import Base
import stelliferous@0.0.2.0/traversal_array.bend as Traversal
import stelliferous@0.0.2.0/proofs/storage_witness.bend as Witness

105def update_sample(~Reader: Type,~Element: Data,~Value: Data,~Context: Data,
106  ~combine: Element -> Value -> Element,~destination: Context -> U32 -> U32,
107  +depth: Nat,-reader: Reader,+position: U32,+context: Context,-output: Array<Element>,-current: Element,
108  -result: Reader & Value,output_evidence: Witness.Witness(Element,depth,output),
109  sample: Sample<Reader,Value,reader,result>) ->
110  StateEvidence<Reader,Element,Context,reader,depth,
111    Traversal.update_sample(~Reader,~Element,~Value,~Context,~combine,~destination,position,context,output,current,result)>:
112  match sample:
113    case Sample{value,equation}:
114      %Equal.sym(Reader & Value,result,(reader,value),equation) :
115        StateEvidence<Reader,Element,Context,reader,depth,
116          Traversal.update_sample(~Reader,~Element,~Value,~Context,~combine,~destination,position,context,output,current,_)>
117      StateEvidence{Array.set(Element,output,destination(context,position),combine(current,value)),(position + 1 : U32),context,{==},
118        Witness.write(Element,depth,output,destination(context,position),combine(current,value),output_evidence)}