adds tracing for conditional expressions

language-reference-manual/lrm.trlc

@@ -1650,7 +1650,7 @@ section "Conditional expressions" {
   }
 
   Dynamic_Semantics Conditional_Expression_Else {
-    text = '''If all condition are evaluated to false, then the else
+    text = '''If all conditions are evaluated to false, then the else
               dependent expression is evaluated and
               returned.'''
   }

tests-system/rbt-conditional-expression-types/foo.rsl

@@ -0,0 +1,11 @@
+package Foo
+
+type T {
+   x Integer
+   y Integer
+   b Boolean
+}
+
+checks T {
+   (if x then x elsif y > x then y else y) <= x, "potato type"
+}

tests-system/rbt-conditional-expression-types/output

@@ -0,0 +1,3 @@
+(if x then x elsif y > x then y else y) <= x, "potato type"
+    ^ rbt-conditional-expression-types/foo.rsl:10: error: expected expression of type Builtin_Boolean, got Builtin_Integer instead
+Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 error(s)

tests-system/rbt-conditional-expression-types/output.brief

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

tests-system/rbt-conditional-expression-types/output.json

@@ -0,0 +1,3 @@
+(if x then x elsif y > x then y else y) <= x, "potato type"
+    ^ rbt-conditional-expression-types/foo.rsl:10: error: expected expression of type Builtin_Boolean, got Builtin_Integer instead
+Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 error(s)

tests-system/rbt-conditional-expression-types/output.smtlib

@@ -0,0 +1,3 @@
+(if x then x elsif y > x then y else y) <= x, "potato type"
+    ^ rbt-conditional-expression-types/foo.rsl:10: error: expected expression of type Builtin_Boolean, got Builtin_Integer instead
+Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 error(s)

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

@@ -0,0 +1,15 @@
+package Foo
+
+type T {
+   x Integer
+   y Integer
+   z Integer
+   b Boolean
+}
+
+checks T {
+   (if b then b else x > 5), "kitten"
+   (if y > x then x elsif x > y then x else y) < x, "foobar evaluation if"
+   (if x > y then x elsif y > x then y else z) <= x, "foobar evaluation elsif"
+   (if x > y then x elsif y == x then y else z) >= x, "potato else"
+}

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

@@ -0,0 +1,8 @@
+package Foo
+
+T test_01 {
+   x = 5
+   y = 10
+   z = 1
+   b = false
+}

tests-system/rbt-conditional-expression/output

@@ -0,0 +1,9 @@
+T test_01 {
+  ^^^^^^^ rbt-conditional-expression/foo.trlc:3: check error: kitten
+T test_01 {
+  ^^^^^^^ rbt-conditional-expression/foo.trlc:3: check error: foobar evaluation if
+T test_01 {
+  ^^^^^^^ rbt-conditional-expression/foo.trlc:3: check error: foobar evaluation elsif
+T test_01 {
+  ^^^^^^^ rbt-conditional-expression/foo.trlc:3: check error: potato else
+Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 4 error(s)

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

@@ -0,0 +1,4 @@
+rbt-conditional-expression/foo.trlc:3:3: trlc check error: kitten
+rbt-conditional-expression/foo.trlc:3:3: trlc check error: foobar evaluation if
+rbt-conditional-expression/foo.trlc:3:3: trlc check error: foobar evaluation elsif
+rbt-conditional-expression/foo.trlc:3:3: trlc check error: potato else

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

@@ -0,0 +1,9 @@
+T test_01 {
+  ^^^^^^^ rbt-conditional-expression/foo.trlc:3: check error: kitten
+T test_01 {
+  ^^^^^^^ rbt-conditional-expression/foo.trlc:3: check error: foobar evaluation if
+T test_01 {
+  ^^^^^^^ rbt-conditional-expression/foo.trlc:3: check error: foobar evaluation elsif
+T test_01 {
+  ^^^^^^^ rbt-conditional-expression/foo.trlc:3: check error: potato else
+Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 4 error(s)

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

@@ -0,0 +1,9 @@
+T test_01 {
+  ^^^^^^^ rbt-conditional-expression/foo.trlc:3: check error: kitten
+T test_01 {
+  ^^^^^^^ rbt-conditional-expression/foo.trlc:3: check error: foobar evaluation if
+T test_01 {
+  ^^^^^^^ rbt-conditional-expression/foo.trlc:3: check error: foobar evaluation elsif
+T test_01 {
+  ^^^^^^^ rbt-conditional-expression/foo.trlc:3: check error: potato else
+Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 4 error(s)

tests-system/rbt-conditional-expression/tracing

@@ -0,0 +1,2 @@
+LRM.Conditional_Expression_Evaluation
+LRM.Conditional_Expression_Else

trlc/ast.py

@@ -480,6 +480,7 @@ def to_string(self):  # pragma: no cover
             self.__class__.__name__
 
     def ensure_type(self, mh, typ):
+        # lobster-trace: LRM.Conditional_Expression_Types
         assert isinstance(typ, (type, Type))
         if self.typ is None:
             mh.error(self.location,
@@ -1817,7 +1818,7 @@ def __init__(self, mh, t_kind, n_condition, n_expression):
         self.kind   = t_kind.value
         self.n_cond = n_condition
         self.n_expr = n_expression
-
+        # lobster-trace: LRM.Conditional_Expression_Types
         self.n_cond.ensure_type(mh, Builtin_Boolean)
 
     def dump(self, indent=0):  # pragma: no cover
@@ -1875,6 +1876,7 @@ def add_elsif(self, mh, n_action):
         self.actions.append(n_action)
 
     def set_else_part(self, mh, n_expr):
+        # lobster-trace: LRM.Conditional_Expression_Else
         assert isinstance(mh, Message_Handler)
         assert isinstance(n_expr, Expression)
 
@@ -1897,6 +1899,7 @@ def to_string(self):
         return rv
 
     def evaluate(self, mh, context):
+        # lobster-trace: LRM.Conditional_Expression_Evaluation
         assert isinstance(mh, Message_Handler)
         assert context is None or isinstance(context, dict)
 

trlc/parser.py

@@ -966,6 +966,7 @@ def parse_quantified_expression(self, scope):
                                          n_expr     = n_expr)
 
     def parse_conditional_expression(self, scope):
+        # lobster-trace: LRM.Conditional_Expression
         assert isinstance(scope, ast.Scope)
 
         self.match_kw("if")