def store_node

stelliferous@0.0.2.0 · proofs/storage_shape.bend:41

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

41def store_node(-Element: Data,+depth: Nat,+left: Tree.Tree<Element>,+right: Tree.Tree<Element>,
42  +half: U32,+index: U32,+value: Element,+choose_left: Bool,
43  left_balanced: Balanced(Element,depth,left),right_balanced: Balanced(Element,depth,right),
44  left_stored: Balanced(Element,depth,Tree.store(Element,left,half,index,value)),
45  right_stored: Balanced(Element,depth,Tree.store(Element,right,half,(index - half : U32),value))) ->
46  Balanced(Element,1n+depth,Bool.pick(Tree.Tree<Element>,choose_left,
47    Tree.Node{Tree.store(Element,left,half,index,value),right},
48    Tree.Node{left,Tree.store(Element,right,half,(index - half : U32),value)})):
49  match choose_left:
50    case True{}: Both{left_stored,right_balanced}
51    case False{}: Both{left_balanced,right_stored}