~/bend-docscommunity

proofs/containers/doubly_linked_list/direct.bend source

proofs/containers/doubly_linked_list/direct.bend on the hub · documented module

import Baseimport ../../../src/containers/doubly_linked_list.bend as Dimport ../../../src/containers/internal/dlist_storage.bend as Rimport ../../../src/containers/types/internal_dlist.bend as Iimport ../../../src/containers/types/doubly_linked_list.bend as E# The public list's direct operations: each is the projection of the trace# step on the same operation, for every list and handle.# ---- the verdict's continuations ----def gv(~T: Data, +tag: U32, +depth: Nat, +cap: U32, -gens: Array<U32>, p: R.DList<T> & Result<&2, &2, I.Error, T>) -> {D.get_result(~T, tag, depth, cap, gens, p) == D.project_value(~T, D.value_result(~T, tag, depth, cap, gens, p)) : D.DList<T> & Result<&2, &2, E.Error, T>}:  match p:    case Tuple{raw, res}:      {==}def sv(~T: Data, +tag: U32, +depth: Nat, +cap: U32, -gens: Array<U32>, p: R.DList<T> & Result<&2, &2, I.Error, Unit>) -> {D.set_result(~T, tag, depth, cap, gens, p) == D.project_unit(~T, D.unit_result(~T, tag, depth, cap, gens, p)) : D.DList<T> & Result<&2, &2, E.Error, Unit>}:  match p:    case Tuple{raw, res}:      {==}def get_m(~T: Data, +h: E.Handle, +tag: U32, +depth: Nat, +cap: U32, raw: R.DList<T>, gens: Array<U32>, m: Maybe<&2, E.Error>) -> {D.get_ready(~T, h, (D.DL{tag, depth, cap, raw, gens}, m)) == D.project_value(~T, D.checked(~T, E.Get{h}, (D.DL{tag, depth, cap, raw, gens}, m))) : D.DList<T> & Result<&2, &2, E.Error, T>}:  match m:    case Some{e}:      {==}    case None{}:      gv(~T, tag, depth, cap, gens, R.get(~T, raw, D.old_handle(h)))def get_s(~T: Data, +h: E.Handle, s: D.DList<T>, m: Maybe<&2, E.Error>) -> {D.get_ready(~T, h, (s, m)) == D.project_value(~T, D.checked(~T, E.Get{h}, (s, m))) : D.DList<T> & Result<&2, &2, E.Error, T>}:  match s:    case D.DL{+tag, +depth, +cap, raw, gens}:      get_m(~T, h, tag, depth, cap, raw, gens, m)def get_r(~T: Data, +h: E.Handle, r: D.DList<T> & Maybe<&2, E.Error>) -> {D.get_ready(~T, h, r) == D.project_value(~T, D.checked(~T, E.Get{h}, r)) : D.DList<T> & Result<&2, &2, E.Error, T>}:  match r:    case Tuple{s, m}:      get_s(~T, h, s, m)def set_m(~T: Data, +h: E.Handle, +x: T, +tag: U32, +depth: Nat, +cap: U32, raw: R.DList<T>, gens: Array<U32>, m: Maybe<&2, E.Error>) -> {D.set_ready(~T, h, x, (D.DL{tag, depth, cap, raw, gens}, m)) == D.project_unit(~T, D.checked(~T, E.Set{h, x}, (D.DL{tag, depth, cap, raw, gens}, m))) : D.DList<T> & Result<&2, &2, E.Error, Unit>}:  match m:    case Some{e}:      {==}    case None{}:      sv(~T, tag, depth, cap, gens, R.set(~T, raw, D.old_handle(h), x))def set_s(~T: Data, +h: E.Handle, +x: T, s: D.DList<T>, m: Maybe<&2, E.Error>) -> {D.set_ready(~T, h, x, (s, m)) == D.project_unit(~T, D.checked(~T, E.Set{h, x}, (s, m))) : D.DList<T> & Result<&2, &2, E.Error, Unit>}:  match s:    case D.DL{+tag, +depth, +cap, raw, gens}:      set_m(~T, h, x, tag, depth, cap, raw, gens, m)def set_r(~T: Data, +h: E.Handle, +x: T, r: D.DList<T> & Maybe<&2, E.Error>) -> {D.set_ready(~T, h, x, r) == D.project_unit(~T, D.checked(~T, E.Set{h, x}, r)) : D.DList<T> & Result<&2, &2, E.Error, Unit>}:  match r:    case Tuple{s, m}:      set_s(~T, h, x, s, m)def rm_m(~T: Data, +owner: U32, +id: U32, +g: U32, +tag: U32, +depth: Nat, +cap: U32, raw: R.DList<T>, gens: Array<U32>, m: Maybe<&2, E.Error>) -> {D.remove_ready(~T, E.H{owner, id, g}, (D.DL{tag, depth, cap, raw, gens}, m)) == D.project_value(~T, D.checked(~T, E.Remove{E.H{owner, id, g}}, (D.DL{tag, depth, cap, raw, gens}, m))) : D.DList<T> & Result<&2, &2, E.Error, T>}:  match m:    case Some{e}:      {==}    case None{}:      {==}def rm_s(~T: Data, +owner: U32, +id: U32, +g: U32, s: D.DList<T>, m: Maybe<&2, E.Error>) -> {D.remove_ready(~T, E.H{owner, id, g}, (s, m)) == D.project_value(~T, D.checked(~T, E.Remove{E.H{owner, id, g}}, (s, m))) : D.DList<T> & Result<&2, &2, E.Error, T>}:  match s:    case D.DL{+tag, +depth, +cap, raw, gens}:      rm_m(~T, owner, id, g, tag, depth, cap, raw, gens, m)def rm_r(~T: Data, +h: E.Handle, r: D.DList<T> & Maybe<&2, E.Error>) -> {D.remove_ready(~T, h, r) == D.project_value(~T, D.checked(~T, E.Remove{h}, r)) : D.DList<T> & Result<&2, &2, E.Error, T>}:  match h r:    case E.H{+owner, +id, +g} Tuple{s, m}:      rm_s(~T, owner, id, g, s, m)def nx_m(~T: Data, +h: E.Handle, +tag: U32, +depth: Nat, +cap: U32, raw: R.DList<T>, gens: Array<U32>, m: Maybe<&2, E.Error>) -> {D.next_ready(~T, h, (D.DL{tag, depth, cap, raw, gens}, m)) == D.project_neighbour(~T, D.checked(~T, E.Next{h}, (D.DL{tag, depth, cap, raw, gens}, m))) : D.DList<T> & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>}:  match m:    case Some{e}:      {==}    case None{}:      {==}def nx_s(~T: Data, +h: E.Handle, s: D.DList<T>, m: Maybe<&2, E.Error>) -> {D.next_ready(~T, h, (s, m)) == D.project_neighbour(~T, D.checked(~T, E.Next{h}, (s, m))) : D.DList<T> & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>}:  match s:    case D.DL{+tag, +depth, +cap, raw, gens}:      nx_m(~T, h, tag, depth, cap, raw, gens, m)def nx_r(~T: Data, +h: E.Handle, r: D.DList<T> & Maybe<&2, E.Error>) -> {D.next_ready(~T, h, r) == D.project_neighbour(~T, D.checked(~T, E.Next{h}, r)) : D.DList<T> & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>}:  match r:    case Tuple{s, m}:      nx_s(~T, h, s, m)def pv_m(~T: Data, +h: E.Handle, +tag: U32, +depth: Nat, +cap: U32, raw: R.DList<T>, gens: Array<U32>, m: Maybe<&2, E.Error>) -> {D.prev_ready(~T, h, (D.DL{tag, depth, cap, raw, gens}, m)) == D.project_neighbour(~T, D.checked(~T, E.Prev{h}, (D.DL{tag, depth, cap, raw, gens}, m))) : D.DList<T> & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>}:  match m:    case Some{e}:      {==}    case None{}:      {==}def pv_s(~T: Data, +h: E.Handle, s: D.DList<T>, m: Maybe<&2, E.Error>) -> {D.prev_ready(~T, h, (s, m)) == D.project_neighbour(~T, D.checked(~T, E.Prev{h}, (s, m))) : D.DList<T> & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>}:  match s:    case D.DL{+tag, +depth, +cap, raw, gens}:      pv_m(~T, h, tag, depth, cap, raw, gens, m)def pv_r(~T: Data, +h: E.Handle, r: D.DList<T> & Maybe<&2, E.Error>) -> {D.prev_ready(~T, h, r) == D.project_neighbour(~T, D.checked(~T, E.Prev{h}, r)) : D.DList<T> & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>}:  match r:    case Tuple{s, m}:      pv_s(~T, h, s, m)def ib_m(~T: Data, +h: E.Handle, +x: T, +tag: U32, +depth: Nat, +cap: U32, raw: R.DList<T>, gens: Array<U32>, m: Maybe<&2, E.Error>) -> {D.insert_before_ready(~T, h, x, (D.DL{tag, depth, cap, raw, gens}, m)) == D.project_insert(~T, D.checked(~T, E.InsertBefore{h, x}, (D.DL{tag, depth, cap, raw, gens}, m))) : D.DList<T> & Result<&2, &2, E.Error, E.Handle>}:  match m:    case Some{e}:      {==}    case None{}:      {==}def ib_s(~T: Data, +h: E.Handle, +x: T, s: D.DList<T>, m: Maybe<&2, E.Error>) -> {D.insert_before_ready(~T, h, x, (s, m)) == D.project_insert(~T, D.checked(~T, E.InsertBefore{h, x}, (s, m))) : D.DList<T> & Result<&2, &2, E.Error, E.Handle>}:  match s:    case D.DL{+tag, +depth, +cap, raw, gens}:      ib_m(~T, h, x, tag, depth, cap, raw, gens, m)def ib_r(~T: Data, +h: E.Handle, +x: T, r: D.DList<T> & Maybe<&2, E.Error>) -> {D.insert_before_ready(~T, h, x, r) == D.project_insert(~T, D.checked(~T, E.InsertBefore{h, x}, r)) : D.DList<T> & Result<&2, &2, E.Error, E.Handle>}:  match r:    case Tuple{s, m}:      ib_s(~T, h, x, s, m)def ia_m(~T: Data, +h: E.Handle, +x: T, +tag: U32, +depth: Nat, +cap: U32, raw: R.DList<T>, gens: Array<U32>, m: Maybe<&2, E.Error>) -> {D.insert_after_ready(~T, h, x, (D.DL{tag, depth, cap, raw, gens}, m)) == D.project_insert(~T, D.checked(~T, E.InsertAfter{h, x}, (D.DL{tag, depth, cap, raw, gens}, m))) : D.DList<T> & Result<&2, &2, E.Error, E.Handle>}:  match m:    case Some{e}:      {==}    case None{}:      {==}def ia_s(~T: Data, +h: E.Handle, +x: T, s: D.DList<T>, m: Maybe<&2, E.Error>) -> {D.insert_after_ready(~T, h, x, (s, m)) == D.project_insert(~T, D.checked(~T, E.InsertAfter{h, x}, (s, m))) : D.DList<T> & Result<&2, &2, E.Error, E.Handle>}:  match s:    case D.DL{+tag, +depth, +cap, raw, gens}:      ia_m(~T, h, x, tag, depth, cap, raw, gens, m)def ia_r(~T: Data, +h: E.Handle, +x: T, r: D.DList<T> & Maybe<&2, E.Error>) -> {D.insert_after_ready(~T, h, x, r) == D.project_insert(~T, D.checked(~T, E.InsertAfter{h, x}, r)) : D.DList<T> & Result<&2, &2, E.Error, E.Handle>}:  match r:    case Tuple{s, m}:      ia_s(~T, h, x, s, m)# ---- the direct operations are projected steps ----def get_step(~T: Data, s: D.DList<T>, +h: E.Handle) -> {D.get(~T, s, h) == D.project_value(~T, D.step(~T, s, E.Get{h})) : D.DList<T> & Result<&2, &2, E.Error, T>}:  get_r(~T, h, D.validate(~T, s, h))def set_step(~T: Data, s: D.DList<T>, +h: E.Handle, +x: T) -> {D.set(~T, s, h, x) == D.project_unit(~T, D.step(~T, s, E.Set{h, x})) : D.DList<T> & Result<&2, &2, E.Error, Unit>}:  set_r(~T, h, x, D.validate(~T, s, h))def remove_step(~T: Data, s: D.DList<T>, +h: E.Handle) -> {D.remove(~T, s, h) == D.project_value(~T, D.step(~T, s, E.Remove{h})) : D.DList<T> & Result<&2, &2, E.Error, T>}:  rm_r(~T, h, D.validate(~T, s, h))def next_step(~T: Data, s: D.DList<T>, +h: E.Handle) -> {D.next(~T, s, h) == D.project_neighbour(~T, D.step(~T, s, E.Next{h})) : D.DList<T> & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>}:  nx_r(~T, h, D.validate(~T, s, h))def prev_step(~T: Data, s: D.DList<T>, +h: E.Handle) -> {D.prev(~T, s, h) == D.project_neighbour(~T, D.step(~T, s, E.Prev{h})) : D.DList<T> & Result<&2, &2, E.Error, Maybe<&2, E.Handle>>}:  pv_r(~T, h, D.validate(~T, s, h))def before_step(~T: Data, s: D.DList<T>, +h: E.Handle, +x: T) -> {D.insert_before(~T, s, h, x) == D.project_insert(~T, D.step(~T, s, E.InsertBefore{h, x})) : D.DList<T> & Result<&2, &2, E.Error, E.Handle>}:  ib_r(~T, h, x, D.validate(~T, s, h))def after_step(~T: Data, s: D.DList<T>, +h: E.Handle, +x: T) -> {D.insert_after(~T, s, h, x) == D.project_insert(~T, D.step(~T, s, E.InsertAfter{h, x})) : D.DList<T> & Result<&2, &2, E.Error, E.Handle>}:  ia_r(~T, h, x, D.validate(~T, s, h))