def primitive_frame_cloned

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

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
import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
import bendtorch-core@0.1.0.0/src/storage/clone.bend as Clone

77def primitive_frame_cloned(-T: Data, +d: Nat, -original: Array<T>, +i: U32,
78  +other: Model.Path(d), +value: T, cloned: Clone.Cloned<T, d, original>) ->
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<T>, 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<T>, second, original, first, same_second,
90        Equal.sym(Array<T>, 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)