thorin2
thorin2 copied to clipboard
Closure Conversion dependent type rewrites
Fork: neuralcoder3/throin2
Branch: matrix_dialect
Command: ./build/bin/thorin -d matrix lit/matrix/print_const.thorin -d affine -d direct -d clos -o - -VVVV
The type of .con print_int_matrix [mem: %mem.M, k: .Nat, l: .Nat, m: %matrix.Mat (2, (k,l), I32), return : .Cn [%mem.M]];
is rewritten to cc_print_int_matrix_3068959 : [%mem.M, [], .Nat, .Nat, %mem.Ptr («k_3068787; «l_3068793; .Idx 4294967296»», 0), .Cn %mem.M]
.
The dependency is lost resulting in error: cannot pass argument
.
Note: Intermediate solution: Ignore dependencies in the type scheme by writing a wrapper that replaces (k,l)
with (⊤:.Nat,⊤:.Nat)
using bitcasts.
This is a known limitation. See also Typed Closure Conversion for the Calculus of Constructions.
Relabeling as enhancement.