AdaCore / RecordFlux

Formal specification and generation of verifiable binary parsers, message generators and protocol state machines
Apache License 2.0
106 stars 7 forks source link

Processing/iterating a sequence in a session #1302

Open NickFoubert opened 1 month ago

NickFoubert commented 1 month ago

I'm trying to sort out how I might process the elements of a sequence in the context of a session. I've tried a couple things but I'm stumped:

  1. I tried "iterating" through a sequence using list comprehensions and 'Head but since copying sequences isn't yet supported there doesn't seem to be a way to store the Tail of a list to process the remaining elements.
  2. It appears that sequences can't be used as a function parameter, either directly or as a component of a message type.

The examples in the repo seem to only ever use the 'Head of a sequence to select the first element or some specific element using a list comprehension.

I'd like to be able to call an external function on each element of a sequence.

I suppose a workaround is to write the sequence to a channel and then have the external code re-parse the sequence?

treiher commented 1 month ago

The operations on sequences are indeed limited at the moment:

I'd like to be able to call an external function on each element of a sequence.

What is the return type of the external function? Would adding support for function calls in list comprehensions solve your issue?

NickFoubert commented 1 month ago

In my current case the return type would be an enumeration, so I believe allowing function calls in a list comprehension would indeed solve my current issue. The protocol requires that for each element of the sequence I return a 1:1 list of "return codes", so a map function is what I'd need.

Return_Codes := [for E in Some_Sequence => Map(E)]

While playing around with this I believe I found a bug: the RecordFlux documentation indicates that the "if" portion of a list comprehension is optional, but the validator/generator generated a Python exception.

X := [for E in Some_Sequence => E]

causes an exception

X := [for E in Some_Sequence if True => E]

also causes an exception, but the documentation implies that 'True' is a valid boolean expression.

X := [for E in Some_Sequence if True = True => E]

succeeds, though I'm not sure it is correct since the documentation implies that the output needs to be a selector expression (though I haven't tried to compile the generated code).

I'm using 0.23.0

treiher commented 1 month ago

In my current case the return type would be an enumeration, so I believe allowing function calls in a list comprehension would indeed solve my current issue. The protocol requires that for each element of the sequence I return a 1:1 list of "return codes", so a map function is what I'd need.

Support for function calls in list comprehensions would be a useful improvement. We have created an internal ticket for this feature request. Unfortunately, we cannot yet estimate when this feature will be available.

While playing around with this I believe I found a bug: [...]

Thank you for reporting this! All three examples (without condition, with True and with True = True) should be accepted. A fix for this bug is currently under review and should be available soon.