def store

stelliferous@0.0.2.0 · proofs/storage_shape.bend:53

import Base
import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree

53def store(-Element: Data,+depth: Nat,+tree: Tree.Tree<Element>,+capacity: U32,+index: U32,+value: Element,
54  balanced: Balanced(Element,depth,tree)) -> Balanced(Element,depth,Tree.store(Element,tree,capacity,index,value)):
55  match depth tree:
56    case 0n Tree.Leaf{previous}: Unit{}
57    case 0n Tree.Node{left,right}: match balanced:
58    case 1n+rest Tree.Leaf{previous}: match balanced:
59    case 1n+ +rest Tree.Node{+left,+right}:
60      Both{+left_balanced,+right_balanced} = balanced
61      store_node(Element,rest,left,right,U32.shr(capacity),index,value,U32.is_lt(index,U32.shr(capacity)),
62        left_balanced,right_balanced,
63        store(Element,rest,left,U32.shr(capacity),index,value,left_balanced),
64        store(Element,rest,right,U32.shr(capacity),(index - U32.shr(capacity) : U32),value,right_balanced))