def emb_cp

bendtorch@1.3.0.0 · main.bend:2003

import Base

2003# row i of the output (d numbers) copied from row ids[i] of the table, for the first n ids
2004def emb_cp(left: Nat, ids: List<&2, Nat>, +i: U32, +d: Nat, st: A2) -> A2:
2005  match left ids st:
2006    case 1n+q Con{+id, t} A2{e, o}:
2007      emb_cp(q, t, (i + 1 : U32), d, copy_n(Nat.sub(d, 1n), (U32.from_nat(id) * U32.from_nat(d) : U32), (i * U32.from_nat(d) : U32), o, Array.get(F32, e, (U32.from_nat(id) * U32.from_nat(d) : U32))))
2008    case _ _ st:
2009      st