def from_shape

stelliferous@0.0.2.0 · proofs/storage_witness.bend:35

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

35def from_shape(-Element: Data,+depth: Nat,+tree: Tree.Tree<Element>,balanced: Shape.Balanced(Element,depth,tree)) ->
36  Witness(Element,depth,Tree.pack(Element,tree)):
37  match depth tree:
38    case 0n Tree.Leaf{value}: Leaf{value,{==}}
39    case 0n Tree.Node{left,right}: match balanced:
40    case 1n+rest Tree.Leaf{value}: match balanced:
41    case 1n+ +rest Tree.Node{+left,+right}:
42      Shape.Both{left_balanced,right_balanced} = balanced
43      Node{Tree.pack(Element,left),Tree.pack(Element,right),{==},from_shape(Element,rest,left,left_balanced),from_shape(Element,rest,right,right_balanced)}