adds tracing for quantification

language-reference-manual/lrm.trlc

@@ -1519,8 +1519,8 @@ section "Quantification" {
   Grammar Quantified_Expression {
     bnf = '''
       quantified_expression ::=
-        quantifier IDENTIFIER_name 'in' IDENTIFIER_component_name '=>'
-        expression_PREDICATE
+        '(' quantifier IDENTIFIER_name 'in' IDENTIFIER_component_name '=>'
+        expression_PREDICATE ')'
 
       quantifier ::= 'forall' | 'exists'
     '''
@@ -1546,14 +1546,6 @@ section "Quantification" {
               quantified expression is Boolean.'''
   }
 
-  Dynamic_Semantics Quantification_Evaluation {
-    text = '''During evaluation of the quantified expression, each element
-              of the array is evaluated in sequence and its
-              value is bound to the declared name. The
-              predicated is then evaluated with this
-              binding.'''
-  }
-
   Dynamic_Semantics Universal_Quantification_Semantics {
     text = '''For universal *(forall)* quantification the final value is
               true iff all predicates evaluate to
@@ -1569,6 +1561,14 @@ section "Quantification" {
               vacuously false.)*'''
   }
 
+  Note Quantification_Evaluation {
+    text = '''During evaluation of the quantified expression, each element
+              of the array is evaluated in sequence and its
+              value is bound to the declared name. The
+              predicated is then evaluated with this
+              binding.'''
+  }
+
   Recommendation Quantification_Short_Circuit_Evaluation {
     text = '''In general Quantification is equivalent to a chain of `and`
               or `or` expressions, however it is left
@@ -1580,6 +1580,7 @@ section "Quantification" {
                '''For static analysis or linting, use non-short-circuit
                   semantics, as using a quantifier as a
                   complex guard is not reasonable.''']
+    untraced_reason = "Non-normative text"
   }
 
 }

tests-system/rbt-existential-quantification-semantics/foo.rsl

@@ -0,0 +1,9 @@
+package Foo
+
+type T {
+    a Integer[0..*]
+}
+
+checks T {
+    (exists item in a => item == 7), warning "there is no 7 in a"
+}

tests-system/rbt-existential-quantification-semantics/foo.trlc

@@ -0,0 +1,9 @@
+package Foo
+
+T Bar {
+    a = [7]
+}
+
+T Kitten {
+    a = []
+}

tests-system/rbt-existential-quantification-semantics/output

@@ -0,0 +1,3 @@
+T Kitten {
+  ^^^^^^ rbt-existential-quantification-semantics/foo.trlc:7: check warning: there is no 7 in a
+Processed 1 model and 1 requirement file and found 1 warning

tests-system/rbt-existential-quantification-semantics/output.brief

@@ -0,0 +1 @@
+rbt-existential-quantification-semantics/foo.trlc:7:3: trlc check warning: there is no 7 in a

tests-system/rbt-existential-quantification-semantics/output.json

@@ -0,0 +1,13 @@
+T Kitten {
+  ^^^^^^ rbt-existential-quantification-semantics/foo.trlc:7: check warning: there is no 7 in a
+{
+  "Bar": {
+    "a": [
+      7
+    ]
+  },
+  "Kitten": {
+    "a": []
+  }
+}
+Processed 1 model and 1 requirement file and found 1 warning

tests-system/rbt-existential-quantification-semantics/output.smtlib

@@ -0,0 +1,3 @@
+T Kitten {
+  ^^^^^^ rbt-existential-quantification-semantics/foo.trlc:7: check warning: there is no 7 in a
+Processed 1 model and 1 requirement file and found 1 warning

tests-system/rbt-quantification-naming-scope/foo.rsl

@@ -0,0 +1,11 @@
+package Foo
+
+type T {
+    a Integer[1..10]
+}
+
+checks T {
+    (forall item in a => item > 0), warning "All items must be positive"
+    (forall item in a => item < 10), warning "All items must be less than 10"
+    (forall a in a => a != 7), warning "No sevens allowed"
+}

tests-system/rbt-quantification-naming-scope/output

@@ -0,0 +1,3 @@
+(forall a in a => a != 7), warning "No sevens allowed"
+        ^ rbt-quantification-naming-scope/foo.rsl:10: error: shadows Composite_Component a from foo.rsl:4
+Processed 1 model and 0 requirement files and found 1 error

tests-system/rbt-quantification-naming-scope/output.brief

@@ -0,0 +1 @@
+rbt-quantification-naming-scope/foo.rsl:10:13: trlc error: shadows Composite_Component a from foo.rsl:4

tests-system/rbt-quantification-naming-scope/output.json

@@ -0,0 +1,3 @@
+(forall a in a => a != 7), warning "No sevens allowed"
+        ^ rbt-quantification-naming-scope/foo.rsl:10: error: shadows Composite_Component a from foo.rsl:4
+Processed 1 model and 0 requirement files and found 1 error

tests-system/rbt-quantification-naming-scope/output.smtlib

@@ -0,0 +1,3 @@
+(forall a in a => a != 7), warning "No sevens allowed"
+        ^ rbt-quantification-naming-scope/foo.rsl:10: error: shadows Composite_Component a from foo.rsl:4
+Processed 1 model and 0 requirement files and found 1 error

tests-system/rbt-quantification-object-1/foo.rsl

@@ -0,0 +1,9 @@
+package Foo
+
+type Potato {
+    a String
+}
+
+checks Potato {
+    (forall char in a => char != "a"), warning "a should not contain the letter a"
+}

tests-system/rbt-quantification-object-1/output

@@ -0,0 +1,3 @@
+(forall char in a => char != "a"), warning "a should not contain the letter a"
+                ^ rbt-quantification-object-1/foo.rsl:8: error: you can only quantify over arrays
+Processed 1 model and 0 requirement files and found 1 error

tests-system/rbt-quantification-object-1/output.brief

@@ -0,0 +1 @@
+rbt-quantification-object-1/foo.rsl:8:21: trlc error: you can only quantify over arrays

tests-system/rbt-quantification-object-1/output.json

@@ -0,0 +1,3 @@
+(forall char in a => char != "a"), warning "a should not contain the letter a"
+                ^ rbt-quantification-object-1/foo.rsl:8: error: you can only quantify over arrays
+Processed 1 model and 0 requirement files and found 1 error

tests-system/rbt-quantification-object-1/output.smtlib

@@ -0,0 +1,3 @@
+(forall char in a => char != "a"), warning "a should not contain the letter a"
+                ^ rbt-quantification-object-1/foo.rsl:8: error: you can only quantify over arrays
+Processed 1 model and 0 requirement files and found 1 error

tests-system/rbt-quantification-object-2/foo.rsl

@@ -0,0 +1,9 @@
+package Foo
+
+type Potato {
+    a String
+}
+
+checks Potato {
+    (forall char in b => char != "a"), warning "b should not contain the letter a"
+}

tests-system/rbt-quantification-object-2/output

@@ -0,0 +1,3 @@
+(forall char in b => char != "a"), warning "b should not contain the letter a"
+                ^ rbt-quantification-object-2/foo.rsl:8: error: unknown symbol b
+Processed 1 model and 0 requirement files and found 1 error

tests-system/rbt-quantification-object-2/output.brief

@@ -0,0 +1 @@
+rbt-quantification-object-2/foo.rsl:8:21: trlc error: unknown symbol b

tests-system/rbt-quantification-object-2/output.json

@@ -0,0 +1,3 @@
+(forall char in b => char != "a"), warning "b should not contain the letter a"
+                ^ rbt-quantification-object-2/foo.rsl:8: error: unknown symbol b
+Processed 1 model and 0 requirement files and found 1 error

tests-system/rbt-quantification-object-2/output.smtlib

@@ -0,0 +1,3 @@
+(forall char in b => char != "a"), warning "b should not contain the letter a"
+                ^ rbt-quantification-object-2/foo.rsl:8: error: unknown symbol b
+Processed 1 model and 0 requirement files and found 1 error

tests-system/rbt-quantified-expression/foo.rsl

@@ -0,0 +1,11 @@
+package Foo
+
+type T {
+    a Integer[1..*]
+}
+
+checks T {
+    (forall item in a => item > 0), warning "All items must be positive", a
+    (exists item in a => item == 7), warning "7 is a lucky number", a
+    (forall item in a => 42), warning "All items must be positive", a
+}

tests-system/rbt-quantified-expression/foo.trlc

@@ -0,0 +1,5 @@
+package Foo
+
+T Bar {
+    a = [1, 2, 3, 7]
+}

tests-system/rbt-quantified-expression/output

@@ -0,0 +1,3 @@
+(forall item in a => 42), warning "All items must be positive", a
+                     ^^ rbt-quantified-expression/foo.rsl:10: error: expected expression of type Builtin_Boolean, got Builtin_Integer instead
+Processed 1 model and 1 requirement file and found 1 error

tests-system/rbt-quantified-expression/output.brief

@@ -0,0 +1 @@
+rbt-quantified-expression/foo.rsl:10:26: trlc error: expected expression of type Builtin_Boolean, got Builtin_Integer instead

tests-system/rbt-quantified-expression/output.json

@@ -0,0 +1,3 @@
+(forall item in a => 42), warning "All items must be positive", a
+                     ^^ rbt-quantified-expression/foo.rsl:10: error: expected expression of type Builtin_Boolean, got Builtin_Integer instead
+Processed 1 model and 1 requirement file and found 1 error

tests-system/rbt-quantified-expression/output.smtlib

@@ -0,0 +1,3 @@
+(forall item in a => 42), warning "All items must be positive", a
+                     ^^ rbt-quantified-expression/foo.rsl:10: error: expected expression of type Builtin_Boolean, got Builtin_Integer instead
+Processed 1 model and 1 requirement file and found 1 error

tests-system/rbt-quantified-expression/tracing

@@ -0,0 +1 @@
+LRM.Quantification_Type

tests-system/rbt-universal-quantification-semantics/foo.rsl

@@ -0,0 +1,9 @@
+package Foo
+
+type T {
+    a Integer[0..*]
+}
+
+checks T {
+    (forall item in a => item > 0), warning "All items must be positive"
+}

tests-system/rbt-universal-quantification-semantics/foo.trlc

@@ -0,0 +1,13 @@
+package Foo
+
+T Bar {
+    a = [-1]
+}
+
+T Kitten {
+    a = []
+}
+
+T Potato {
+    a = [-1, 1]
+}

tests-system/rbt-universal-quantification-semantics/output

@@ -0,0 +1,5 @@
+T Bar {
+  ^^^ rbt-universal-quantification-semantics/foo.trlc:3: check warning: All items must be positive
+T Potato {
+  ^^^^^^ rbt-universal-quantification-semantics/foo.trlc:11: check warning: All items must be positive
+Processed 1 model and 1 requirement file and found 2 warnings

tests-system/rbt-universal-quantification-semantics/output.brief

@@ -0,0 +1,2 @@
+rbt-universal-quantification-semantics/foo.trlc:3:3: trlc check warning: All items must be positive
+rbt-universal-quantification-semantics/foo.trlc:11:3: trlc check warning: All items must be positive

tests-system/rbt-universal-quantification-semantics/output.json

@@ -0,0 +1,21 @@
+T Bar {
+  ^^^ rbt-universal-quantification-semantics/foo.trlc:3: check warning: All items must be positive
+T Potato {
+  ^^^^^^ rbt-universal-quantification-semantics/foo.trlc:11: check warning: All items must be positive
+{
+  "Bar": {
+    "a": [
+      -1
+    ]
+  },
+  "Kitten": {
+    "a": []
+  },
+  "Potato": {
+    "a": [
+      -1,
+      1
+    ]
+  }
+}
+Processed 1 model and 1 requirement file and found 2 warnings

tests-system/rbt-universal-quantification-semantics/output.smtlib

@@ -0,0 +1,5 @@
+T Bar {
+  ^^^ rbt-universal-quantification-semantics/foo.trlc:3: check warning: All items must be positive
+T Potato {
+  ^^^^^^ rbt-universal-quantification-semantics/foo.trlc:11: check warning: All items must be positive
+Processed 1 model and 1 requirement file and found 2 warnings

trlc/ast.py

@@ -2046,6 +2046,8 @@ def __init__(self, mh, location,
                  n_variable,
                  n_source,
                  n_expr):
+        # lobster-trace: LRM.Quantified_Expression
+        # lobster-trace: LRM.Quantification_Type
         super().__init__(location, typ)
         assert isinstance(typ, Builtin_Boolean)
         assert isinstance(universal, bool)
@@ -2077,6 +2079,8 @@ def to_string(self):
 
     def evaluate(self, mh, context):
         # lobster-trace: LRM.Null_Is_Invalid
+        # lobster-trace: LRM.Universal_Quantification_Semantics
+        # lobster-trace: LRM.Existential_Quantification_Semantics
         assert isinstance(mh, Message_Handler)
         assert context is None or isinstance(context, dict)
 

trlc/parser.py

@@ -1064,6 +1064,7 @@ def parse_primary(self, scope):
             return self.parse_name(scope)
 
     def parse_quantified_expression(self, scope):
+        # lobster-trace: LRM.Quantified_Expression
         assert isinstance(scope, ast.Scope)
 
         if self.peek_kw("forall"):
@@ -1078,6 +1079,7 @@ def parse_quantified_expression(self, scope):
         self.match("IDENTIFIER")
         t_qv = self.ct
         if scope.contains(t_qv.value):
+            # lobster-trace: LRM.Quantification_Naming_Scope
             pdef = scope.lookup(self.mh, t_qv)
             self.mh.error(t_qv.location,
                           "shadows %s %s from %s" %
@@ -1092,6 +1094,7 @@ def parse_quantified_expression(self, scope):
                                       field)
         n_source.set_ast_link(self.ct)
         if not isinstance(field.n_typ, ast.Array_Type):
+            # lobster-trace: LRM.Quantification_Object
             self.mh.error(self.ct.location,
                           "you can only quantify over arrays")
         n_var = ast.Quantified_Variable(t_qv.value,