def facts_3

bendtorch-core@0.1.0.0 · src/tensor/axis_algebra.bend:2159

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/tensor/axis_spec.bend as Axis

2159def facts_3(+axes: List<&2, Nat>, accepted: {True{} == Axis.valid(3n, axes) : Bool}) -> Facts<3n, axes>:
2160  match axes:
2161    case Nil{}:
2162      Empty.absurd(Facts<3n, Nil{}>, Shape.clash(accepted))
2163    case +a0 <> Nil{}:
2164      Empty.absurd(Facts<3n, a0 <> Nil{}>, Shape.clash(accepted))
2165    case +a0 <> +a1 <> Nil{}:
2166      Empty.absurd(Facts<3n, a0 <> a1 <> Nil{}>, Shape.clash(accepted))
2167    case 0n <> 0n <> 0n <> Nil{}:
2168      Empty.absurd(Facts<3n, [0n, 0n, 0n]>, Shape.clash(accepted))
2169    case 0n <> 0n <> 1n <> Nil{}:
2170      Empty.absurd(Facts<3n, [0n, 0n, 1n]>, Shape.clash(accepted))
2171    case 0n <> 0n <> 2n <> Nil{}:
2172      Empty.absurd(Facts<3n, [0n, 0n, 2n]>, Shape.clash(accepted))
2173    case 0n <> 0n <> (3n+p) <> Nil{}:
2174      Empty.absurd(Facts<3n, 0n <> 0n <> (3n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(3n+p, 3n), Axis.bounded(Nil{}, 3n), Arith.and_left(Axis.bounded(0n <> 0n <> (3n+p) <> Nil{}, 3n), Axis.unique(0n <> 0n <> (3n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(3n, 0n <> 0n <> (3n+p) <> Nil{}), accepted)))))
2175    case 0n <> 1n <> 0n <> Nil{}:
2176      Empty.absurd(Facts<3n, [0n, 1n, 0n]>, Shape.clash(accepted))
2177    case 0n <> 1n <> 1n <> Nil{}:
2178      Empty.absurd(Facts<3n, [0n, 1n, 1n]>, Shape.clash(accepted))
2179    case 0n <> 1n <> 2n <> Nil{}:
2180      Certified{{==}, {==}, {==}, A => items => length => lists_012(A, items, length),
2181        dims => length => product_012(dims, length), dims => coords => dl => cl => fit_012(dims, coords, dl, cl)}
2182    case 0n <> 1n <> (3n+p) <> Nil{}:
2183      Empty.absurd(Facts<3n, 0n <> 1n <> (3n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(3n+p, 3n), Axis.bounded(Nil{}, 3n), Arith.and_left(Axis.bounded(0n <> 1n <> (3n+p) <> Nil{}, 3n), Axis.unique(0n <> 1n <> (3n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(3n, 0n <> 1n <> (3n+p) <> Nil{}), accepted)))))
2184    case 0n <> 2n <> 0n <> Nil{}:
2185      Empty.absurd(Facts<3n, [0n, 2n, 0n]>, Shape.clash(accepted))
2186    case 0n <> 2n <> 1n <> Nil{}:
2187      Certified{{==}, {==}, {==}, A => items => length => lists_021(A, items, length),
2188        dims => length => product_021(dims, length), dims => coords => dl => cl => fit_021(dims, coords, dl, cl)}
2189    case 0n <> 2n <> 2n <> Nil{}:
2190      Empty.absurd(Facts<3n, [0n, 2n, 2n]>, Shape.clash(accepted))
2191    case 0n <> 2n <> (3n+p) <> Nil{}:
2192      Empty.absurd(Facts<3n, 0n <> 2n <> (3n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(3n+p, 3n), Axis.bounded(Nil{}, 3n), Arith.and_left(Axis.bounded(0n <> 2n <> (3n+p) <> Nil{}, 3n), Axis.unique(0n <> 2n <> (3n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(3n, 0n <> 2n <> (3n+p) <> Nil{}), accepted)))))
2193    case 0n <> (3n+p) <> a0 <> Nil{}:
2194      Empty.absurd(Facts<3n, 0n <> (3n+p) <> a0 <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(3n+p, 3n), Axis.bounded(a0 <> Nil{}, 3n), Arith.and_left(Axis.bounded(0n <> (3n+p) <> a0 <> Nil{}, 3n), Axis.unique(0n <> (3n+p) <> a0 <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(3n, 0n <> (3n+p) <> a0 <> Nil{}), accepted)))))
2195    case 1n <> 0n <> 0n <> Nil{}:
2196      Empty.absurd(Facts<3n, [1n, 0n, 0n]>, Shape.clash(accepted))
2197    case 1n <> 0n <> 1n <> Nil{}:
2198      Empty.absurd(Facts<3n, [1n, 0n, 1n]>, Shape.clash(accepted))
2199    case 1n <> 0n <> 2n <> Nil{}:
2200      Certified{{==}, {==}, {==}, A => items => length => lists_102(A, items, length),
2201        dims => length => product_102(dims, length), dims => coords => dl => cl => fit_102(dims, coords, dl, cl)}
2202    case 1n <> 0n <> (3n+p) <> Nil{}:
2203      Empty.absurd(Facts<3n, 1n <> 0n <> (3n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(3n+p, 3n), Axis.bounded(Nil{}, 3n), Arith.and_left(Axis.bounded(1n <> 0n <> (3n+p) <> Nil{}, 3n), Axis.unique(1n <> 0n <> (3n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(3n, 1n <> 0n <> (3n+p) <> Nil{}), accepted)))))
2204    case 1n <> 1n <> 0n <> Nil{}:
2205      Empty.absurd(Facts<3n, [1n, 1n, 0n]>, Shape.clash(accepted))
2206    case 1n <> 1n <> 1n <> Nil{}:
2207      Empty.absurd(Facts<3n, [1n, 1n, 1n]>, Shape.clash(accepted))
2208    case 1n <> 1n <> 2n <> Nil{}:
2209      Empty.absurd(Facts<3n, [1n, 1n, 2n]>, Shape.clash(accepted))
2210    case 1n <> 1n <> (3n+p) <> Nil{}:
2211      Empty.absurd(Facts<3n, 1n <> 1n <> (3n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(3n+p, 3n), Axis.bounded(Nil{}, 3n), Arith.and_left(Axis.bounded(1n <> 1n <> (3n+p) <> Nil{}, 3n), Axis.unique(1n <> 1n <> (3n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(3n, 1n <> 1n <> (3n+p) <> Nil{}), accepted)))))
2212    case 1n <> 2n <> 0n <> Nil{}:
2213      Certified{{==}, {==}, {==}, A => items => length => lists_120(A, items, length),
2214        dims => length => product_120(dims, length), dims => coords => dl => cl => fit_120(dims, coords, dl, cl)}
2215    case 1n <> 2n <> 1n <> Nil{}:
2216      Empty.absurd(Facts<3n, [1n, 2n, 1n]>, Shape.clash(accepted))
2217    case 1n <> 2n <> 2n <> Nil{}:
2218      Empty.absurd(Facts<3n, [1n, 2n, 2n]>, Shape.clash(accepted))
2219    case 1n <> 2n <> (3n+p) <> Nil{}:
2220      Empty.absurd(Facts<3n, 1n <> 2n <> (3n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(3n+p, 3n), Axis.bounded(Nil{}, 3n), Arith.and_left(Axis.bounded(1n <> 2n <> (3n+p) <> Nil{}, 3n), Axis.unique(1n <> 2n <> (3n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(3n, 1n <> 2n <> (3n+p) <> Nil{}), accepted)))))
2221    case 1n <> (3n+p) <> a0 <> Nil{}:
2222      Empty.absurd(Facts<3n, 1n <> (3n+p) <> a0 <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(3n+p, 3n), Axis.bounded(a0 <> Nil{}, 3n), Arith.and_left(Axis.bounded(1n <> (3n+p) <> a0 <> Nil{}, 3n), Axis.unique(1n <> (3n+p) <> a0 <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(3n, 1n <> (3n+p) <> a0 <> Nil{}), accepted)))))
2223    case 2n <> 0n <> 0n <> Nil{}:
2224      Empty.absurd(Facts<3n, [2n, 0n, 0n]>, Shape.clash(accepted))
2225    case 2n <> 0n <> 1n <> Nil{}:
2226      Certified{{==}, {==}, {==}, A => items => length => lists_201(A, items, length),
2227        dims => length => product_201(dims, length), dims => coords => dl => cl => fit_201(dims, coords, dl, cl)}
2228    case 2n <> 0n <> 2n <> Nil{}:
2229      Empty.absurd(Facts<3n, [2n, 0n, 2n]>, Shape.clash(accepted))
2230    case 2n <> 0n <> (3n+p) <> Nil{}:
2231      Empty.absurd(Facts<3n, 2n <> 0n <> (3n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(3n+p, 3n), Axis.bounded(Nil{}, 3n), Arith.and_left(Axis.bounded(2n <> 0n <> (3n+p) <> Nil{}, 3n), Axis.unique(2n <> 0n <> (3n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(3n, 2n <> 0n <> (3n+p) <> Nil{}), accepted)))))
2232    case 2n <> 1n <> 0n <> Nil{}:
2233      Certified{{==}, {==}, {==}, A => items => length => lists_210(A, items, length),
2234        dims => length => product_210(dims, length), dims => coords => dl => cl => fit_210(dims, coords, dl, cl)}
2235    case 2n <> 1n <> 1n <> Nil{}:
2236      Empty.absurd(Facts<3n, [2n, 1n, 1n]>, Shape.clash(accepted))
2237    case 2n <> 1n <> 2n <> Nil{}:
2238      Empty.absurd(Facts<3n, [2n, 1n, 2n]>, Shape.clash(accepted))
2239    case 2n <> 1n <> (3n+p) <> Nil{}:
2240      Empty.absurd(Facts<3n, 2n <> 1n <> (3n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(3n+p, 3n), Axis.bounded(Nil{}, 3n), Arith.and_left(Axis.bounded(2n <> 1n <> (3n+p) <> Nil{}, 3n), Axis.unique(2n <> 1n <> (3n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(3n, 2n <> 1n <> (3n+p) <> Nil{}), accepted)))))
2241    case 2n <> 2n <> 0n <> Nil{}:
2242      Empty.absurd(Facts<3n, [2n, 2n, 0n]>, Shape.clash(accepted))
2243    case 2n <> 2n <> 1n <> Nil{}:
2244      Empty.absurd(Facts<3n, [2n, 2n, 1n]>, Shape.clash(accepted))
2245    case 2n <> 2n <> 2n <> Nil{}:
2246      Empty.absurd(Facts<3n, [2n, 2n, 2n]>, Shape.clash(accepted))
2247    case 2n <> 2n <> (3n+p) <> Nil{}:
2248      Empty.absurd(Facts<3n, 2n <> 2n <> (3n+p) <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(3n+p, 3n), Axis.bounded(Nil{}, 3n), Arith.and_left(Axis.bounded(2n <> 2n <> (3n+p) <> Nil{}, 3n), Axis.unique(2n <> 2n <> (3n+p) <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(3n, 2n <> 2n <> (3n+p) <> Nil{}), accepted)))))
2249    case 2n <> (3n+p) <> a0 <> Nil{}:
2250      Empty.absurd(Facts<3n, 2n <> (3n+p) <> a0 <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(3n+p, 3n), Axis.bounded(a0 <> Nil{}, 3n), Arith.and_left(Axis.bounded(2n <> (3n+p) <> a0 <> Nil{}, 3n), Axis.unique(2n <> (3n+p) <> a0 <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(3n, 2n <> (3n+p) <> a0 <> Nil{}), accepted)))))
2251    case (3n+p) <> a0 <> a1 <> Nil{}:
2252      Empty.absurd(Facts<3n, (3n+p) <> a0 <> a1 <> Nil{}>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(3n+p, 3n), Axis.bounded(a0 <> a1 <> Nil{}, 3n), Arith.and_left(Axis.bounded((3n+p) <> a0 <> a1 <> Nil{}, 3n), Axis.unique((3n+p) <> a0 <> a1 <> Nil{}), Equal.sym(Bool, True{}, Axis.valid(3n, (3n+p) <> a0 <> a1 <> Nil{}), accepted)))))
2253    case +a0 <> +a1 <> +a2 <> +a3 <> +tail:
2254      Empty.absurd(Facts<3n, a0 <> a1 <> a2 <> a3 <> tail>, Shape.clash(accepted))