thorin2 icon indicating copy to clipboard operation
thorin2 copied to clipboard

Closure Conversion dependent type rewrites

Open NeuralCoder3 opened this issue 2 years ago • 1 comments

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.

NeuralCoder3 avatar Jan 09 '23 14:01 NeuralCoder3

This is a known limitation. See also Typed Closure Conversion for the Calculus of Constructions.

Relabeling as enhancement.

leissa avatar Jan 09 '23 19:01 leissa