def obs_append

bendtorch-core@0.1.0.0 · src/autograd/reduce_parallel_proof.bend:259

import Base
import bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend as Parallel

259def obs_append(+d: Nat, -A: Array<F32>, +xs: List<&2, Nat>, +vs: List<&2, F32>, -ys: List<&2, Nat>, -ws: List<&2, F32>,
260  -first: Obs(d, A, xs, vs), -second: Obs(d, A, ys, ws)) ->
261  Parallel.Fact<Obs(d, A, List.append(&2, Nat, xs, ys), List.append(&2, F32, vs, ws))>:
262  match xs vs:
263    case Nil{} Nil{}:
264      Parallel.Fact{second}
265    case +p <> +ps +v <> +rest:
266      Parallel.Fact{{\{ObsStep: seen => more =>
267        ObsStep{seen, {\{Parallel.Fact: p => p} : Parallel.Fact<Obs(d, A, List.append(&2, Nat, ps, ys), List.append(&2, F32, rest, ws))> ->
268          Obs(d, A, List.append(&2, Nat, ps, ys), List.append(&2, F32, rest, ws))}(obs_append(d, A, ps, rest, ys, ws, more, second))}} :
269        ObsStep<d, A, p, v, ps, rest> -> ObsStep<d, A, p, v, List.append(&2, Nat, ps, ys), List.append(&2, F32, rest, ws)>}(first)}
270    case Nil{} +v <> +rest:
271      Parallel.Fact{Empty.absurd(Obs(d, A, ys, List.append(&2, F32, v <> rest, ws)), first)}
272    case +p <> +ps Nil{}:
273      Parallel.Fact{Empty.absurd(Obs(d, A, List.append(&2, Nat, p <> ps, ys), ws), first)}