src/shape/construct_proofs.bend
bendtorch-core@0.1.0.0 · 79 lines · 10 definitions
1import Base
2import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
3import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
4import bendtorch-core@0.1.0.0/src/shape/LAWS.bend as Laws
5
6def within(-dims: List<&2, Nat>, capacity: Shape.Capacity<dims>) -> Bool:
7 match capacity:
8 case Shape.Within{size, exact, bound}:
9 True{}
10 case Shape.Beyond{}:
11 False{}
12
13def bound_within(-dims: List<&2, Nat>, -size: Nat, -exact: {size == Shape.numel(dims) : Nat}, +decision: Shape.BoolCase<Nat.is_le(size, 1048576n)>, fits: {True{} == Nat.is_le(size, 1048576n) : Bool}) -> {True{} == within(dims, Shape.capacity.bound(dims, size, exact, decision)) : Bool}:
14 match decision:
15 case Shape.BFalse{equal}:
16 Empty.absurd({True{} == False{} : Bool}, Nats.contradiction(Nat.is_le(size, 1048576n), fits, equal))
17 case Shape.BTrue{equal}:
18 {==}
19
20def scale_within(+head: Nat, -tail: List<&2, Nat>, +size: Nat, -exact: {size == Shape.numel(tail) : Nat}, +small: Shape.BoolCase<Bool.or(Nat.is_eq(size, 0n), Nat.is_le(head, 1048576n))>, fits_small: {True{} == Bool.or(Nat.is_eq(size, 0n), Nat.is_le(head, 1048576n)) : Bool}, fits_product: {True{} == Nat.is_le(Nat.mul(head, size), 1048576n) : Bool}) -> {True{} == within(head <> tail, Shape.capacity.scale(head, tail, size, exact, small)) : Bool}:
21 match small:
22 case Shape.BFalse{equal}:
23 Empty.absurd({True{} == False{} : Bool}, Nats.contradiction(Bool.or(Nat.is_eq(size, 0n), Nat.is_le(head, 1048576n)), fits_small, equal))
24 case Shape.BTrue{equal}:
25 bound_within(head <> tail, Nat.mul(head, size), Equal.cong(Nat, Nat, value => Nat.mul(head, value), size, Shape.numel(tail), exact), Shape.bool_case(Nat.is_le(Nat.mul(head, size), 1048576n)), fits_product)
26
27def scale_fits(+p: Nat, +size: Nat, bound: Shape.LE(Nat.mul(1n+p, size), 1048576n)) -> {True{} == Bool.or(Nat.is_eq(size, 0n), Nat.is_le(1n+p, 1048576n)) : Bool}:
28 match size:
29 case 0n:
30 {==}
31 case 1n+q:
32 Nats.le_true(1n+p, 1048576n, Nats.le_add_left(1n+p, Nat.mul(1n+p, q), 1048576n, Nats.le_rewrite(Nat.add(1n+p, Nat.mul(1n+p, q)), Nat.mul(1n+p, 1n+q), 1048576n, Nats.mul_succ_right(1n+p, q), bound)))
33
34def zero_small(+size: Nat) -> {True{} == Bool.or(Nat.is_eq(size, 0n), Nat.is_le(0n, 1048576n)) : Bool}:
35 match size:
36 case 0n:
37 {==}
38 case 1n+q:
39 {==}
40
41def zero_within(-tail: List<&2, Nat>, +rest: Shape.Capacity<tail>) -> {True{} == within(0n <> tail, Shape.capacity.step(0n, tail, rest)) : Bool}:
42 match rest:
43 case Shape.Beyond{}:
44 {==}
45 case Shape.Within{+size, exact, bound}:
46 scale_within(0n, tail, size, exact, Shape.bool_case(Bool.or(Nat.is_eq(size, 0n), Nat.is_le(0n, 1048576n))), zero_small(size), {==})
47
48def step_within(+p: Nat, +tail: List<&2, Nat>, +rest: Shape.Capacity<tail>, ih: {True{} == within(tail, rest) : Bool}, bound: Shape.LE(Nat.mul(1n+p, Shape.numel(tail)), 1048576n)) -> {True{} == within((1n+p) <> tail, Shape.capacity.step(1n+p, tail, rest)) : Bool}:
49 match rest:
50 case Shape.Beyond{}:
51 Empty.absurd({True{} == within((1n+p) <> tail, Shape.capacity.step(1n+p, tail, Shape.Beyond{})) : Bool}, Shape.clash(ih))
52 case Shape.Within{+size, +exact, fits}:
53 +scaled = Nats.le_rewrite(Nat.mul(1n+p, size), Nat.mul(1n+p, Shape.numel(tail)), 1048576n, Equal.cong(Nat, Nat, value => Nat.mul(1n+p, value), Shape.numel(tail), size, Equal.sym(Nat, size, Shape.numel(tail), exact)), bound)
54 scale_within(1n+p, tail, size, exact, Shape.bool_case(Bool.or(Nat.is_eq(size, 0n), Nat.is_le(1n+p, 1048576n))), scale_fits(p, size, scaled), Nats.le_true(Nat.mul(1n+p, size), 1048576n, scaled))
55
56def capacity_complete(+dims: List<&2, Nat>, +bound: Shape.LE(Shape.numel(dims), 1048576n)) -> {True{} == within(dims, Shape.capacity(dims)) : Bool}:
57 match dims:
58 case Nil{}:
59 {==}
60 case +head <> +tail:
61 match head:
62 case 0n:
63 zero_within(tail, Shape.capacity(tail))
64 case 1n+p:
65 step_within(p, tail, Shape.capacity(tail), capacity_complete(tail, Nats.le_add_left(Shape.numel(tail), Nat.mul(p, Shape.numel(tail)), 1048576n, bound)), bound)
66
67def capacity_built(+input: List<&2, U32>, rank_bound: Shape.LE(Shape.rank_dimensions(input), 4n), +capacity: Shape.Capacity<Shape.naturals(input)>, fits: {True{} == within(Shape.naturals(input), capacity) : Bool}) -> {Laws.built(input, Shape.construct.capacity(input, rank_bound, capacity)) == Some{input} : Maybe<&2, List<&2, U32>>}:
68 match capacity:
69 case Shape.Beyond{}:
70 Empty.absurd({Laws.built(input, Shape.construct.capacity(input, rank_bound, Shape.Beyond{})) == Some{input} : Maybe<&2, List<&2, U32>>}, Shape.clash(fits))
71 case Shape.Within{size, exact, bound}:
72 {==}
73
74def construction_complete(+input: List<&2, U32>, +decision: Shape.BoolCase<Nat.is_le(Shape.rank_dimensions(input), 4n)>, rank_fits: {True{} == Nat.is_le(Shape.rank_dimensions(input), 4n) : Bool}, capacity_bound: Shape.LE(Shape.logical_numel(input), 1048576n)) -> {Laws.built(input, Shape.construct.ranked(input, decision)) == Some{input} : Maybe<&2, List<&2, U32>>}:
75 match decision:
76 case Shape.BFalse{equal}:
77 Empty.absurd({Laws.built(input, Shape.construct.ranked(input, Shape.BFalse{equal})) == Some{input} : Maybe<&2, List<&2, U32>>}, Nats.contradiction(Nat.is_le(Shape.rank_dimensions(input), 4n), rank_fits, equal))
78 case Shape.BTrue{equal}:
79 capacity_built(input, Shape.LE.from(Shape.rank_dimensions(input), 4n, equal), Shape.capacity(Shape.naturals(input)), capacity_complete(Shape.naturals(input), capacity_bound))