1 import Base 2 import ./model.bend as Model 3 import ./array.bend as ArrayCore 4 import ./refinement.bend as Refinement 5 import ./clone.bend as Clone 6 7 def write_read(-T: Data, +d: Nat, array: Array, +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) 25 26 def update_frame(-T: Data, +d: Nat, array: Array, +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) 54 55 def observed_correct(-T: Data, -d: Nat, -array: Array, -path: Model.Path(d), 56 read: ArrayCore.Read) -> 57 {ArrayCore.observation(T, d, array, path, read) == Model.observe(T, d, array, path) : Maybe<&2, T>}: 58 match read: 59 case ArrayCore.Read{retained, value, balanced, kept, observed}: 60 observed 61 62 def retained_correct(-T: Data, -d: Nat, -array: Array, -path: Model.Path(d), 63 read: ArrayCore.Read) -> 64 {ArrayCore.retained(T, d, array, path, read) == array : Array}: 65 match read: 66 case ArrayCore.Read{retained, value, balanced, kept, observed}: 67 kept 68 69 def read_refines(-T: Data, +d: Nat, array: Array, +path: Model.Path(d), valid: Model.Balanced(T, d, array)) -> 70 {ArrayCore.observation(T, d, array, path, ArrayCore.read_path(T, d, array, path, valid)) == Model.observe(T, d, array, path) : Maybe<&2, T>}: 71 observed_correct(T, d, array, path, ArrayCore.read_path(T, d, array, path, valid)) 72 73 def read_retains(-T: Data, +d: Nat, array: Array, +path: Model.Path(d), valid: Model.Balanced(T, d, array)) -> 74 {ArrayCore.retained(T, d, array, path, ArrayCore.read_path(T, d, array, path, valid)) == array : Array}: 75 retained_correct(T, d, array, path, ArrayCore.read_path(T, d, array, path, valid)) 76 77 def primitive_frame_cloned(-T: Data, +d: Nat, -original: Array, +i: U32, 78 +other: Model.Path(d), +value: T, cloned: Clone.Cloned) -> 79 {Model.observe(T, d, Array.set(T, original, i, value), other) == Model.select(T, Model.same(d, Refinement.route(d, i), other), value, Model.observe(T, d, original, other)) : Maybe<&2, T>}: 80 match cloned: 81 case Clone.Cloned{first, second, exact, +same_first, +same_second, valid_first, valid_second}: 82 %same_second : 83 {Model.observe(T, d, Array.set(T, original, i, value), other) == Model.select(T, Model.same(d, Refinement.route(d, i), other), value, Model.observe(T, d, _, other)) : Maybe<&2, T>} 84 %same_first : 85 {Model.observe(T, d, Array.set(T, _, i, value), other) == Model.select(T, Model.same(d, Refinement.route(d, i), other), value, Model.observe(T, d, second, other)) : Maybe<&2, T>} 86 %Equal.sym(Array, Array.set(T, first, i, value), ArrayCore.write_path(T, d, first, Refinement.route(d, i), value), 87 Refinement.law_set_refines(T, d, first, i, value, valid_first)) : 88 {Model.observe(T, d, _, other) == Model.select(T, Model.same(d, Refinement.route(d, i), other), value, Model.observe(T, d, second, other)) : Maybe<&2, T>} 89 %Equal.trans(Array, second, original, first, same_second, 90 Equal.sym(Array, first, original, same_first)) : 91 {Model.observe(T, d, ArrayCore.write_path(T, d, _, Refinement.route(d, i), value), other) == Model.select(T, Model.same(d, Refinement.route(d, i), other), value, Model.observe(T, d, second, other)) : Maybe<&2, T>} 92 update_frame(T, d, second, Refinement.route(d, i), other, value, valid_second) 93 94 def primitive_update_frame(-T: Data, +d: Nat, array: Array, +i: U32, +other: Model.Path(d), +value: T, valid: Model.Balanced(T, d, array)) -> 95 {Model.observe(T, d, Array.set(T, array, i, value), other) == Model.select(T, Model.same(d, Refinement.route(d, i), other), value, Model.observe(T, d, array, other)) : Maybe<&2, T>}: 96 primitive_frame_cloned(T, d, array, i, other, value, Clone.certify(T, d, array, valid)) 97 98 def path_self_same(+d: Nat, +path: Model.Path(d)) -> 99 {Model.same(d, path, path) == True{} : Bool}: 100 match d: 101 case 0n: 102 {==} 103 case 1n+p: 104 Model.Step{bit, rest} = path 105 match bit: 106 case False{}: 107 path_self_same(p, rest) 108 case True{}: 109 path_self_same(p, rest) 110 111 def primitive_write_read(-T: Data, +d: Nat, array: Array, +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 {==}