RecordFlux icon indicating copy to clipboard operation
RecordFlux copied to clipboard

Implement the `not` operator

Open rami3l opened this issue 2 years ago • 1 comments

There are times when the negation of a complex boolean expression is more expressive.

For example, when specifying a RecordFlux message, rather than manually applying the De Morgan's law:

First_Field : Some_Type
   then Second_Field
      if Foo = 1 and Bar = 2 and Baz = 3
   then null
      if Foo /= 1 or Bar /= 2 or Baz /= 3;

... sometimes it seems more intuitive to write:

First_Field : Some_Type
   then Second_Field
      if Foo = 1 and Bar = 2 and Baz = 3
   then null
      if not (Foo = 1 and Bar = 2 and Baz = 3);
Real-World Example

When implementing the ASN.1 BER serialization scheme, all 3 fields in the tag should be matched against:

with Prelude;

package Test is

   type BOOLEAN_ is
      message
         Tag_Class : Prelude::Asn_Tag_Class;
         Tag_Form : Prelude::Asn_Tag_Form;
         Tag_Num : Prelude::Asn_Tag_Num
            then null
               if Tag_Num /= 1
                   or Tag_Class /= 0
                   or Tag_Form /= 0
            then Untagged_Length
               if Tag_Num = 1
                  and Tag_Class = 0
                  and Tag_Form = 0;
         Untagged_Length : Prelude::Asn_Length
            then null
               if Untagged_Length'Size /= Prelude::Asn_Raw_BOOLEAN'Size
            then Untagged_Value
               if Untagged_Length'Size = Prelude::Asn_Raw_BOOLEAN'Size;
         Untagged_Value : Prelude::Asn_Raw_BOOLEAN;
      end message;

end Test;

From a code generator's point of view, it's easier to specify the first predicate as follows:

if not (Tag_Num = 1
    and Tag_Class = 0
    and Tag_Form = 0)

... and as a bonus, it will be interesting to accept something like:

First_Field : Some_Type
   then Second_Field
      if Foo = 1 and Bar = 2 and Baz = 3
   then null
      otherwise;

Implementation progress

  • Backend support: #1049
  • Frontend support: https://github.com/Componolit/RecordFlux-parser/pull/59
  • Finalize the integration: (no PR yet)

rami3l avatar May 18 '22 15:05 rami3l

@rami3l Here are some pointers for implementing this feature:

The RecordFlux parser needs to be extended. There is already a Not token, but the expression and extended_expression grammar rules do not support using it:

https://github.com/Componolit/RecordFlux-parser/blob/d01ed5f308f7b01bd5e8c9bd53694961fe2da4b6/language/parser.py#L158-L170 https://github.com/Componolit/RecordFlux-parser/blob/d01ed5f308f7b01bd5e8c9bd53694961fe2da4b6/language/parser.py#L324-L336

A good first step would be adding test cases to the grammar tests:

https://github.com/Componolit/RecordFlux-parser/blob/d01ed5f308f7b01bd5e8c9bd53694961fe2da4b6/tests/grammar_test.py#L868 https://github.com/Componolit/RecordFlux-parser/blob/d01ed5f308f7b01bd5e8c9bd53694961fe2da4b6/tests/grammar_test.py#L993

Note that the version of the parser must be increased when changing the grammar:

https://github.com/Componolit/RecordFlux-parser/blob/d01ed5f308f7b01bd5e8c9bd53694961fe2da4b6/Makefile#L3

In RecordFlux, the conversion of the AST into expression.Expr objects needs to be extended and tested:

https://github.com/Componolit/RecordFlux/blob/6886e51f22175fa31c54817045e4ed642dcae169/rflx/specification/parser.py#L664-L685 https://github.com/Componolit/RecordFlux/blob/6886e51f22175fa31c54817045e4ed642dcae169/tests/unit/specification/grammar_test.py#L301

I'm not sure yet what exactly has to be done in the model. I would start with adding a test case with a message where Not is used and see what problems occur. The following unit test could be used as a template and the new test could be added to the same unit:

https://github.com/Componolit/RecordFlux/blob/6886e51f22175fa31c54817045e4ed642dcae169/tests/unit/model/message_test.py#L1264-L1285

treiher avatar May 20 '22 08:05 treiher