def reflect_packed

stelliferous@0.0.2.0 · proofs/storage_refinement.bend:11

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

11# The tree model covers every native Array owner, including capacities larger
12# than its logical sequence. These equalities allocate no runtime conversion.
13def reflect_packed(-Element: Data,+tree: Tree.Tree<Element>) ->
14  {Tree.reflect(Element,Tree.pack(Element,tree)) == tree : Tree.Tree<Element>}:
15  match tree:
16    case Tree.Leaf{value}: {==}
17    case Tree.Node{+left,+right}:
18      %Equal.sym(Tree.Tree<Element>,Tree.reflect(Element,Tree.pack(Element,left)),left,reflect_packed(Element,left)) :
19        {Tree.Node{_,Tree.reflect(Element,Tree.pack(Element,right))} == Tree.Node{left,right} : Tree.Tree<Element>}
20      %Equal.sym(Tree.Tree<Element>,Tree.reflect(Element,Tree.pack(Element,right)),right,reflect_packed(Element,right)) :
21        {Tree.Node{left,_} == Tree.Node{left,right} : Tree.Tree<Element>}
22      {==}