def balanced

stelliferous@0.0.2.0 · proofs/storage_witness.bend:25

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

25def balanced(-Element: Data,depth: Nat,-storage: Array<Element>,witness: Witness(Element,depth,storage)) ->
26  Shape.Balanced(Element,depth,Tree.reflect(Element,storage)):
27  match depth witness:
28    case 0n Leaf{value,owner}:
29      %Equal.sym(Array<Element>,storage,ALeaf{value},owner) : Shape.Balanced(Element,0n,Tree.reflect(Element,_))
30      Unit{}
31    case 1n+ +rest Node{left,right,owner,left_balanced,right_balanced}:
32      %Equal.sym(Array<Element>,storage,ANode{left,right},owner) : Shape.Balanced(Element,1n+rest,Tree.reflect(Element,_))
33      Shape.Both{balanced(Element,rest,left,left_balanced),balanced(Element,rest,right,right_balanced)}