def get_checked_hit

bendtorch-core@0.1.0.0 · src/storage/api.bend:22

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
import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as Laws
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith

22def get_checked_hit(+d: Nat, +n: Nat, array: Array<F32>, +i: U32, allowed: Bool,
23  -decision: {allowed == Nat.is_lt(U32.to_nat(i), n) : Bool},
24  -balanced: Model.Balanced(F32, d, array), -valid: {Storage.bounds(d, n) == True{} : Bool},
25  yes: {True{} == allowed : Bool}, +fits: {Storage.bounds(d, n) == True{} : Bool},
26  +inside: {Nat.is_lt(U32.to_nat(i), n) == True{} : Bool}) ->
27  {Laws.outcome(Result<&2, &2, Storage.Error, F32>, Storage.get_checked(d, n, array, i, allowed, decision, balanced, valid)) ==
28    Done{Refinement.second(F32, Array.get(F32, array, i))} : Result<&2, &2, Storage.Error, F32>}:
29  match allowed:
30    case True{}:
31      finish_value(d, n, array, i, Array.get(F32, array, i), {==}, balanced, valid)
32    case False{}:
33      Empty.absurd({Laws.outcome(Result<&2, &2, Storage.Error, F32>, Storage.get_checked(d, n, array, i, False{}, decision, balanced, valid)) ==
34        Done{Refinement.second(F32, Array.get(F32, array, i))} : Result<&2, &2, Storage.Error, F32>}, Arith.clash_true(yes))