<d1b2>
<Olivier Galibert> Is there a standard method for (type) testing of parameters. E.g. I require fs and fe to be non-zero positive integers and fe <= fs, how do I test that and bitch if needed in an amaranth-module sanctioned way? (there are a lot of possibilities, I'm interested to know if there's a pattern to reproduce)
<d1b2>
<Olivier Galibert> Perfect, I'll use exactly that
<d1b2>
<Olivier Galibert> Bad amaranth, bad!\
<d1b2>
<Olivier Galibert> with m.Switch(Cat(self.state, self.substate)): with m.Case(Cat(ST.IDLE, 0)): m.d.sync += [self.o_sclk.eq(1), self.o_data.eq(1)]
<d1b2>
<Olivier Galibert> amaranth.hdl.dsl.SyntaxError: Case pattern must be an integer, a string, or an enumeration, not (cat (const 4'd0) (const 1'd0))
<d1b2>
<Olivier Galibert> pouts
<whitequark>
there's no concept of a const expression in Amaranth at the moment
<whitequark>
before I start talking about the concerns I have about this RFC, I'd like to hear your opinions on it
<d1b2>
<Olivier Galibert> Doesn't that hide a little too much?
<jfng[m]>
what happens in op_a = Op.Add(42) ? is it a lowered to a const, or a Signal with 42 as reset ?
<d1b2>
<Olivier Galibert> I mean I can see that there's probably 16 lines fo rthe value and one for the op, but I have no certainty there right?
<whitequark>
jfng: that's a very good question
<whitequark>
I imagine it would be a const
<whitequark>
it's unfortunate that the RFC's "detailed design" section does not include any actual detailed design
<whitequark>
my concerns about the RFC are:
<jfng[m]>
the feature itself could be useful, e.g. one could encode a CPU instruction with a struct
<jfng[m]>
sometimes, the fields would be hardcoded constants, sometimes, their value would be controlled by logic, e.g. an FSM
<jfng[m]>
while reusing the same definition
<whitequark>
- no detailed design; unclear how the functionality would actually work
<whitequark>
- no side-by-side comparison with the same code that can be written today without this RFC
<whitequark>
- no motivation for adding the `|` operator instead of using existing `m.Case(Op.Mul, Op.Add):` functionality
<d1b2>
<Olivier Galibert> I suspect the code generation is not trivial. I mean, it's not hard to generate code that will work, but will it be good? There are times where you'll want the bits physically shared, and other times not, and amaranth probably can't know without becoming a fully-fledged compiler
<d1b2>
<Olivier Galibert> the motivation I think is the presence of the "as"
<Chips4MakersakaS>
Don't understand name of IfLet, does not seem a conditional to me but a cast.
<whitequark>
- no explanation for what happens in the `m.Case(Op.Mul, Op.Add) as x:` case if `Op.Mul` and `Op.Add` have different values
<d1b2>
<Olivier Galibert> but it's exactly as problematic in practice
<whitequark>
i.e. what is the type of x there?
<whitequark>
Olivier: I agree re: code generation, codegen for matches is non-trivial, though there has been much academic research
<d1b2>
<Olivier Galibert> @Chips4Makers if the type matches the run the block with let thing=value
<d1b2>
<Olivier Galibert> (remove one the)
<whitequark>
- may not integrate well with the Python type system we you use `Add: unsigned(16)` annotation that is shown
<whitequark>
s/you//
<d1b2>
<Olivier Galibert> It's trying to port a very useful Rust construct, but does it blend?
<whitequark>
* - may not integrate well with the Python type system if we use `Add: unsigned(16)` annotation that is shown
<whitequark>
Chips4Makers (aka Staf Verhaegen): `m.IfLet` is a shortcut for `m.Match` with one `m.Case`
<whitequark>
you are right however, m.Match/m.Case with as here are a cast
<d1b2>
<Olivier Galibert> The problem is that tagged values in software make a lot of sense, while tagged ports in hardware make a lot less
<d1b2>
<Olivier Galibert> (and signals are more ports than values)
<mwk>
Chips4MakersakaS: the IfLet construct (and Match as well) are analogous to Rust constructs of the same name
<whitequark>
they make some sense
<whitequark>
for example, in AXI4 streams, you have data and valid. you could think of this as an enum of None or Some(data)
<jfng[m]>
assuming Op.Add(42) lowered to a const, and #751 was implemented, would m.Match() be redundant with m.Switch() ?
<whitequark>
this is better than just having data/valid because it unambiguously states that when valid is low, the value of data would be irrelevant
<whitequark>
jfng: I think there's no `m.Match`/`m.Case(Op.Add(42))` functionality presented in the RFC
<d1b2>
<Olivier Galibert> isn't that implicit through saying that equality comparison is possible?
<jfng[m]>
ah right, i misread
<whitequark>
- Match in Rust is useful because it lets you descend into nested structures, but the functionality in the RFC does not seem to allow that (you can't bind variables)
<whitequark>
Olivier: right now, m.Case is not equivalent to equality comparison
<d1b2>
<Olivier Galibert> @whitequark Thanks for the issue 🙂
<d1b2>
<Olivier Galibert> isn't the point of the "as" being binding the variable?
<whitequark>
I mean in the nested structure
<whitequark>
in Rust, you can do something like `match x { Foo { bar: A(x), baz: B(y) } => ... }`
<whitequark>
here, you would have to deconstruct this into a tree of... three matches, I think?
<whitequark>
if Foo, A, and B are all enums, three.
<vup>
as far as I can tell the RFC mainly introduces `Match` and `IfLet` to be able to bind the value of the value "contained" by the union.
<vup>
It is not clear to me why this ability should be limited to this special kind of tagged union. One could for example also want use a similar functionality with Struct's, where one maybe has a case that matches on a specific value of the first field of the struct, and wants to use the second field in the struct in the statements that are gated by the case.
<vup>
<whitequark>
vup: yeah, I agree; it's not limited to tagged unions in Rust either
<vup>
Using this more general pattern matching and destructuring ability the tagged union would then basically just be a special case of a Struct containing a int and a Union
<d1b2>
<Olivier Galibert> isn't the main problem that the concept just doesn't exist in python?
<d1b2>
<Olivier Galibert> so there's no usual syntax to go with it?
<vup>
python 3.10 has `match`
<whitequark>
vup: there is a benefit to not being able to access the "wrong" union members (the ones that are related to the tags that are not used)
<whitequark>
unfortunately 3.10 match isn't useful at all for this functionality, I've evaluated it a while ago
<whitequark>
lt lets you bind variables in the interior of objects, yes, but it's not programmable
<d1b2>
<Olivier Galibert> plus 3.10 match is C's switch/case, nothing more, afaict
<whitequark>
there's no way to make case [x]: mean something different for Amaranth. and there isn't really a way to simulate this either since x isn't a value like it usually is in expressions, it's a hole
<d1b2>
<Olivier Galibert> there no type matching and local name binding
<vup>
whitequark: that is true, but it could be possible to prevent accessing wrong union members using library functions instead of features added to the core language.
<whitequark>
vup: having this invariant in the core language has the benefit that everyone using the language can rely on the invariant, and not only the subset of consumers that use the library
<whitequark>
it's not clear however how much "make illegal states unrepresentable" applies to Amaranth. right now we don't have a type system for signals, so you can always set an enum to a "wrong" (not included in the definition) value. and someone external can always give us an enum like that
<whitequark>
so while there is a benefit in principle, it may not apply to Amaranth
<vup>
The folding of the tag value into the union like rust does for Option<NonNull> could be nice
<whitequark>
I think that's only really useful in software? there aren't too many cases in hardware where you pass around pointers
crzwdjk has joined #amaranth-lang
<vup>
I was more thinking of things packet lengths, where a zero length packet might not be valid
<whitequark>
besides, we aren't free to change representation arbitrarily, we don't have the equivalent of #[repr]
<whitequark>
* besides, we aren't free to change representation arbitrarily, we don't have the equivalent of #[repr(C)] and our implied contract for the default representation says it's stable
<Chips4MakersakaS>
To me big difference between Switch and Match is that Switch consider 'run time' value in a script; Match works on defined type in Amaranth. Don
<mwk>
whitequark: it could be useful for nested enums
<Chips4MakersakaS>
't see direct use case for latter.
<whitequark>
Chips4Makers (aka Staf Verhaegen): I'm not entirely sure what you mean here?
<Chips4MakersakaS>
script -> circuit
<crzwdjk>
It's not about pointers per se, it's about types where some values are really "invalid value"
<whitequark>
vup: ah, so folding valid into length? I think that requires something like full dependent types to express in the general case
<whitequark>
I don't think that's viable
<vup>
whitequark: yeah folding valid into length, for example to preventing zero length packets from being able to be generated at the amaranth level.
<Chips4MakersakaS>
The value for a Switch signal can be different due to input to the circuit; Match is depending on how a value is defined in python. Don't know if the latter is needed for Amaranth. Unless for making generics in metaprogramming or something like that ?
<d1b2>
<Olivier Galibert> crzwdjk: that's where are say half of the values in amaranth aren't values, they're ports you connect to, and sometimes also persistent state. But they don't really behave like values in a software sense
<whitequark>
Chips4Makers (aka Staf Verhaegen): I don't think that's true? in the example there's `m.Match(op_a)`, which works the same as `m.Switch(op_a)`; what changes is what `m.Case` means
<d1b2>
<Olivier Galibert> when you pass them around you're hauling off wiring 😉
<vup>
whitequark: A tagged union will be a dependent type anyways, right? Where does the additional complexity come in?
<whitequark>
vup: a tagged union is a special case that you can hardcode into the language. Rust doesn't have general dependent types (I think?) but they do have two special cases, enums and closures
<whitequark>
this lets you have an easier time because you don't have to go full Agda on it
<Chips4MakersakaS>
I guess my question is what the use cases are where you would use m.Match(op_a).
<whitequark>
Chips4Makers (aka Staf Verhaegen): so with this RFC, `Op` is internally a struct with two members, `tag` and `u`, and `u` is a union with two members, `add` and `mul`
<whitequark>
when you do m.Match(op_a): and then m.Case(Op.Add) as x, what you're doing is internally m.Switch(op_a.tag): then m.Case(Op.Add): x = op_a.u.add; ...
<whitequark>
does this make sense?
<Chips4MakersakaS>
and op_a.tag is a Signal ?
<whitequark>
op_a in this case would be backed by a single Signal as it happens in lib.data, yes
<whitequark>
so op_a.tag would be something like sig[0] where sig is the underlying signal
<Chips4MakersakaS>
OK understood, so size of tag is determined by the number of enum values in the Enum.
<whitequark>
yes, as it happens normally with Enums
<whitequark>
okay, we've had this meeting run for a hour; let me summarize the result and check if we all agree on it
<whitequark>
primary concerns:
<whitequark>
resolution: close; RFC has major unresolved concerns
<whitequark>
1. no detailed design
<whitequark>
2. lack of ability to perform nested matches greatly limits usefulness compared to e.g. Rust's `match`
<whitequark>
3. not clear that the language should treat tagged unions specially considering that there are other common patterns expressing dependencies between fields (e.g. the length field being 0 meaning the data field is invalid)
<whitequark>
any comments on this summary?
<vup>
I would see value in a followup RFC that considers a more general pattern matching construct, that can be used with Struct and allows for variable binding
<vup>
whitequark: is this something that you think is actually reasonably doable in a python DSL
<mwk>
as for 3, I'd argue it's a tagged union with a funny representation
<mwk>
involving a field with a niche (as the Rust folks call it)
<mwk>
I think there'd be value in having a way to create tagged unions with tightly-controlled representation details, to match existing protocols into higher-level constructs?
<mwk>
the other missing part of the puzzle here would be a type of "integer, with range restricted to 1-65535" which... unfortunately would involve a range check on creation, which is a thing that's hard to do in a satisfying way when you cannot just `panic!`
<mwk>
(that or a pinky promise)
<whitequark>
oh, I forgot another concern:
<whitequark>
4. unclear what `Op.Add(42)` should return. it is a Const? is it an integer? is it a Signal with a reset value?
<whitequark>
vup: I would say no, but people are welcome to try
<whitequark>
mwk: I'm not sure if Amaranth is the right place for that kind of representation invariants, to be honest
<whitequark>
we can't enforce them in any way other than $assert/$assume
<mwk>
yeah, that's the unfortunate part
<whitequark>
it would be useful for simulations, but the tooling support for that is so poor
<mwk>
also, as a data point, SystemVerilog has packed tagged unions which behave pretty much like what's proposed here (except with nicer matching syntax)
<mwk>
freely castable to/from plain bitvec
<mwk>
no representation control, but exact bit representation is well-defined by the standard
<whitequark>
vup: what is your github @?
<vup>
whitequark: rroohhh
daveberkeley has quit [Quit: Client closed]
<whitequark>
ohhh, I never realized that those are the handles of the same person
<_whitenotifier-9>
[amaranth-lang/amaranth-lang.github.io] whitequark 77c209a - Deploying to main from @ amaranth-lang/amaranth@e2f05197741bbf36d01c3baf03ae48931ede2c19 🚀
<byteit101>
Should I be concerned by a number of overlaping cases in the generated verilog?
<whitequark>
can you show an example?
<byteit101>
seems to mostly be one-hot encoding, and most of them are identical anyway, but a few arent.
<byteit101>
casez ({ \$3 , \$1 })
<byteit101>
2'b?1: \do_ack$next = 1'h0;
<byteit101>
2'b1?: \do_ack$next = 1'h0;
<whitequark>
if/else are translated to this pattern
<whitequark>
it's a way to encode a priority mux
<byteit101>
ah, good, so I can ignore the 65 errors of this kind then?