opencompl
`comb` dialect: `typeSum` and `hList` seem suspicuous
I just had another look at #1112, and noticed the use of typeSum and hList types, which seem suspicuous to me.
At the very least, there don't seem to be any constructors/eliminators of these types, so as the comb dialect currently stands I believe it's not actually possible to write meaningful well-typed programs using the concat or mux operations (i.e., programs that do anything with the result of a mux besides returning it, or that want to concat anything that isn't just an argument to the region).
For comb.mux, @TaoBi22 tells me that the true, false, and return types should all be the same, so there should be no need for a sum type there.
That is, I believe Op.mux ought to take only one width and the signature ought to be | Op.mux w => (Ty.bv w, Ty.bv w, Ty.bool) → Ty.bv w.
For comb.concat, currently it takes only one argument, whose type is an hList. I believe this operation ought to be variadic, i.e, it's signature should be | .concat l => ${l.map Ty.bv} → (Ty.bv l.sum), so that it takes n arguments, each of type .bv l[i].
@alexkeizer FWIW, I recommended typeSum, and was told that we want the ability to model muxes that take different widths. Chat with @luisacicolini about it.
Also, it is possible to write well-typed programs that build a typeSum, but that one does not have an eliminator for typeSum implies that indeed, one cannot inspect the result of a comb.mux.
@alexkeizer For comb.concat, it might once again be useful to chat with @luisacicolini about it. IIRC , at some point, I tried to encode the type as you suggested and failed, because I got lost in the type-tetris game, and would have needed more time than we had at the time to get it through.
happy to eliminate typeSum given what @TaoBi22 said - I stuck with the comb doc which did not mention this afaict.
will also give the comb.concat signature a try and see what happens
happy to eliminate
typeSumgiven what @TaoBi22 said - I stuck with thecombdoc which did not mention this afaict. will also give thecomb.concatsignature a try and see what happens
Yeah I don't think it's mentioned in the autogenned dialect docs but the tablegen definition of the operation requires that the types of the true, false and result values all match
@alexkeizer I'm fixing concat but I don't understand what should be the type of the argument in the definition.
Right now it's def concat {ls : List Nat} (xs : HVector BitVec ls) : BitVec (List.sum ls) := for the variadic op, I'd like to have only a list to make it properly variadic but I don't see how to connect that to ls
refactoring the parser now (#1237) - chatting with @ymherklotz yesterday we decided to temporarlily ignore concat, as it is the only op we can't express as a purely-bitvec operation (read: without hlist or HVector).
@luisacicolini I believe you fixed this in a recent PR, right? please close this issue if so!