1 import Base 2 import ./core.bend as Shape 3 import ./index_proofs.bend as Index 4 import ./broadcast_proofs.bend as Broadcast 5 import ./nat_proofs.bend as Nats 6 import ./construct_proofs.bend as Construct 7 import ./boundary_proofs.bend as Boundary 8 import ./unique_proofs.bend as Unique 9 import ./plan_proofs.bend as Plan 10 import ./LAWS.bend as Laws 11 12 def Laws.row_major_bounded(dims, coordinate): 13 %Index.flatten_row_major(dims, coordinate) : Shape.LT(_, Shape.numel(dims)) 14 Shape.Fin.bound(Shape.numel(dims), Shape.flatten(dims, coordinate)) 15 16 def Laws.flatten_unflatten(dims, index): 17 Index.flatten_unflatten(dims, index) 18 19 def Laws.unflatten_flatten(dims, coordinate): 20 Index.unflatten_flatten(dims, coordinate) 21 22 def Laws.flatten_row_major(dims, coordinate): 23 Index.flatten_row_major(dims, coordinate) 24 25 def Laws.broadcast_left_projection(left, right, output, alignment, coordinate): 26 Broadcast.project_left(left, right, output, alignment, coordinate) 27 28 def Laws.broadcast_right_projection(left, right, output, alignment, coordinate): 29 Broadcast.project_right(left, right, output, alignment, coordinate) 30 31 def Laws.construction_complete(input, rank_bound, capacity_bound): 32 Construct.construction_complete(input, Shape.bool_case(Nat.is_le(Shape.rank_dimensions(input), 4n)), Nats.le_true(Shape.rank_dimensions(input), 4n, rank_bound), capacity_bound) 33 34 def Laws.flatten_checked_refines(shape, values): 35 Boundary.flatten_checked(shape, values) 36 37 def Laws.unflatten_checked_refines(shape, index): 38 Boundary.unflatten_checked(shape, index) 39 40 def Laws.broadcast_output_unique(left, right, output, other, first, second): 41 Unique.broadcast_unique(left, right, output, other, first, second) 42 43 def Laws.broadcast_checked_plan(left, right): 44 Plan.broadcast_checked_plan(left, right) 45 46 def Laws.broadcast_checked_complete(left, right, output, alignment, rank_bound, capacity_bound): 47 Plan.broadcast_checked_complete(left, right, output, alignment, rank_bound, capacity_bound) 48 49 def Laws.project_left_checked_refines(plan, values): 50 Boundary.project_left_checked(plan, values) 51 52 def Laws.project_right_checked_refines(plan, values): 53 Boundary.project_right_checked(plan, values) 54 55 def Laws.project_left_index_refines(plan, map, index): 56 Boundary.project_left_index(plan, map, index) 57 58 def Laws.project_right_index_refines(plan, map, index): 59 Boundary.project_right_index(plan, map, index) 60 61 def flatten_fits_bounds(+shape: Shape.Shape, +values: List<&2, U32>, verdict: Shape.BoolCase, 62 outside: {Shape.fit_words(Shape.dimensions(shape), values) == False{} : Bool}) -> 63 {Shape.flatten_checked.fits(shape, values, verdict) == Fail{Shape.CoordinateOutOfBounds{}} : Result<&2, &2, Shape.Error, Shape.FlatIndex>}: 64 match verdict: 65 case Shape.BFalse{equal}: 66 {==} 67 case Shape.BTrue{equal}: 68 Empty.absurd({Shape.flatten_checked.fits(shape, values, Shape.BTrue{equal}) == Fail{Shape.CoordinateOutOfBounds{}} : Result<&2, &2, Shape.Error, Shape.FlatIndex>}, 69 Shape.clash(Equal.trans(Bool, True{}, Shape.fit_words(Shape.dimensions(shape), values), False{}, equal, outside))) 70 71 def flatten_ranked_rank(+shape: Shape.Shape, +values: List<&2, U32>, 72 same_rank: Shape.BoolCase, 73 differ: {Shape.rank_dimensions(Shape.dimensions(shape)) != Shape.rank_dimensions(values) : Nat}) -> 74 {Shape.flatten_checked.ranked(shape, values, same_rank) == Fail{Shape.CoordinateRankMismatch{}} : Result<&2, &2, Shape.Error, Shape.FlatIndex>}: 75 match same_rank: 76 case Shape.BFalse{equal}: 77 {==} 78 case Shape.BTrue{equal}: 79 Empty.absurd({Shape.flatten_checked.ranked(shape, values, Shape.BTrue{equal}) == Fail{Shape.CoordinateRankMismatch{}} : Result<&2, &2, Shape.Error, Shape.FlatIndex>}, 80 differ(Shape.equal_decided(Shape.rank_dimensions(Shape.dimensions(shape)), Shape.rank_dimensions(values), equal))) 81 82 def flatten_ranked_bounds(+shape: Shape.Shape, +values: List<&2, U32>, 83 same_rank: Shape.BoolCase, 84 same: {Shape.rank_dimensions(Shape.dimensions(shape)) == Shape.rank_dimensions(values) : Nat}, 85 outside: {Shape.fit_words(Shape.dimensions(shape), values) == False{} : Bool}) -> 86 {Shape.flatten_checked.ranked(shape, values, same_rank) == Fail{Shape.CoordinateOutOfBounds{}} : Result<&2, &2, Shape.Error, Shape.FlatIndex>}: 87 match same_rank: 88 case Shape.BFalse{equal}: 89 Empty.absurd({Shape.flatten_checked.ranked(shape, values, Shape.BFalse{equal}) == Fail{Shape.CoordinateOutOfBounds{}} : Result<&2, &2, Shape.Error, Shape.FlatIndex>}, 90 Shape.clash(Equal.trans(Bool, True{}, Nat.is_eq(Shape.rank_dimensions(Shape.dimensions(shape)), Shape.rank_dimensions(values)), False{}, 91 Plan.eq_true(Shape.rank_dimensions(Shape.dimensions(shape)), Shape.rank_dimensions(values), same), 92 Equal.sym(Bool, False{}, Nat.is_eq(Shape.rank_dimensions(Shape.dimensions(shape)), Shape.rank_dimensions(values)), equal)))) 93 case Shape.BTrue{equal}: 94 flatten_fits_bounds(shape, values, Shape.bool_case(Shape.fit_words(Shape.dimensions(shape), values)), outside) 95 96 def Laws.flatten_rank_error(shape, values, differ): 97 flatten_ranked_rank(shape, values, Shape.bool_case(Nat.is_eq(Shape.rank_dimensions(Shape.dimensions(shape)), Shape.rank_dimensions(values))), differ) 98 99 def Laws.flatten_bounds_error(shape, values, same, outside): 100 flatten_ranked_bounds(shape, values, Shape.bool_case(Nat.is_eq(Shape.rank_dimensions(Shape.dimensions(shape)), Shape.rank_dimensions(values))), same, outside)