def decode_fit

bendtorch-core@0.1.0.0 · src/shape/boundary_proofs.bend:48

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend as Coordinates
import bendtorch-core@0.1.0.0/src/shape/LAWS.bend as Laws

48def decode_fit(+dims: List<&2, Nat>, +values: List<&2, Nat>, +fits: Coordinates.Fits(dims, values)) -> {Laws.decode(dims, values) == Some{Coordinates.coordinate_of(dims, values, fits)} : Maybe<&2, Shape.Coordinate(dims)>}:
49  match dims values:
50    case Nil{} Nil{}:
51      {==}
52    case +dh <> +dt +vh <> +vt:
53      Coordinates.FStep{+bound, +tail} = fits
54      %Equal.sym(Maybe<&2, Shape.Coordinate(dt)>, Laws.decode(dt, vt), Some{Coordinates.coordinate_of(dt, vt, tail)}, decode_fit(dt, vt, tail)) : {Laws.decode.step(dh, dt, _, Laws.fin_of(dh, vh)) == Some{Shape.CStep{Coordinates.fin_from(dh, vh, bound), Coordinates.coordinate_of(dt, vt, tail)}} : Maybe<&2, Shape.Coordinate(dh <> dt)>}
55      %Equal.sym(Maybe<&2, Shape.Fin(dh)>, Laws.fin_of(dh, vh), Some{Coordinates.fin_from(dh, vh, bound)}, fin_of_from(dh, vh, bound)) : {Laws.decode.step(dh, dt, Some{Coordinates.coordinate_of(dt, vt, tail)}, _) == Some{Shape.CStep{Coordinates.fin_from(dh, vh, bound), Coordinates.coordinate_of(dt, vt, tail)}} : Maybe<&2, Shape.Coordinate(dh <> dt)>}
56      {==}
57    case Nil{} vh <> vt:
58      match fits:
59    case dh <> dt Nil{}:
60      match fits: