def update_frame

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

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

26def update_frame(-T: Data, +d: Nat, array: Array<T>, +i: Model.Path(d), +j: Model.Path(d), +value: T, valid: Model.Balanced(T, d, array)) ->
27  {Model.observe(T, d, ArrayCore.write_path(T, d, array, i, value), j) == Model.select(T, Model.same(d, i, j), value, Model.observe(T, d, array, j)) : Maybe<&2, T>}:
28  match d array:
29    case 0n ALeaf{old}:
30      {==}
31    case 0n ANode{xs, ys}:
32      match valid:
33    case 1n+p ALeaf{old}:
34      match valid:
35    case 1n++p ANode{xs, ys}:
36      Model.Step{ib, ir} = i
37      match ib:
38        case False{}:
39          Model.Step{jb, jr} = j
40          match jb:
41            case False{}:
42              (ex, ey) = valid
43              update_frame(T, p, xs, ir, jr, value, ex)
44            case True{}:
45              {==}
46        case True{}:
47          Model.Step{jb, jr} = j
48          match jb:
49            case False{}:
50              {==}
51            case True{}:
52              (ex, ey) = valid
53              update_frame(T, p, ys, ir, jr, value, ey)