def primitive_write_read

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

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement

111def primitive_write_read(-T: Data, +d: Nat, array: Array<T>, +i: U32, +value: T, valid: Model.Balanced(T, d, array)) ->
112  {Model.observe(T, d, Array.set(T, array, i, value), Refinement.route(d, i)) == Some{value} : Maybe<&2, T>}:
113  %Equal.sym(Maybe<&2, T>,
114    Model.observe(T, d, Array.set(T, array, i, value), Refinement.route(d, i)),
115    Model.select(T, Model.same(d, Refinement.route(d, i), Refinement.route(d, i)), value,
116      Model.observe(T, d, array, Refinement.route(d, i))),
117    primitive_update_frame(T, d, array, i, Refinement.route(d, i), value, valid)) :
118    {_ == Some{value} : Maybe<&2, T>}
119  %Equal.sym(Bool, Model.same(d, Refinement.route(d, i), Refinement.route(d, i)), True{},
120    path_self_same(d, Refinement.route(d, i))) :
121    {Model.select(T, _, value, Model.observe(T, d, array, Refinement.route(d, i))) == Some{value} : Maybe<&2, T>}
122  {==}