def write_read

bendtorch-core@0.1.0.0 · src/storage/frame.bend:7

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/storage/array.bend as ArrayCore

7def write_read(-T: Data, +d: Nat, array: Array<T>, +path: Model.Path(d), value: T, valid: Model.Balanced(T, d, array)) ->
8  {Model.observe(T, d, ArrayCore.write_path(T, d, array, path, value), path) == Some{value} : Maybe<&2, T>}:
9  match d array:
10    case 0n ALeaf{old}:
11      {==}
12    case 0n ANode{xs, ys}:
13      match valid:
14    case 1n+p ALeaf{old}:
15      match valid:
16    case 1n++p ANode{xs, ys}:
17      Model.Step{bit, rest} = path
18      match bit:
19        case False{}:
20          (ex, ey) = valid
21          write_read(T, p, xs, rest, value, ex)
22        case True{}:
23          (ex, ey) = valid
24          write_read(T, p, ys, rest, value, ey)