Skip to content

Commit

Permalink
enhances tracing
Browse files Browse the repository at this point in the history
  • Loading branch information
christophkloeffel committed Oct 23, 2023
1 parent 9096ff1 commit 7d6d26e
Show file tree
Hide file tree
Showing 10 changed files with 24 additions and 9 deletions.
1 change: 0 additions & 1 deletion language-reference-manual/lrm.trlc
Original file line number Diff line number Diff line change
Expand Up @@ -1070,7 +1070,6 @@ section "Expressions" {
is recommended that a linter warns whenever a
unary minus is encountered that has a
non-trivial `term` or `factor` as its operand.'''
untraced_reason = "Non-normative recommendation"
}

Example Expression_Examples {
Expand Down
File renamed without changes.
3 changes: 3 additions & 0 deletions tests-system/rbt-unary-minus-parsing/output
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
-a * b > 0, "potato"
^ rbt-unary-minus-parsing/example.rsl:9: issue: expression means -(a * b), place explicit brackets to clarify intent [unary_minus_precedence]
Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found 1 warning(s)
File renamed without changes.
File renamed without changes.
3 changes: 3 additions & 0 deletions tests-system/rbt-unary-minus-parsing/output.smtlib
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
-a * b > 0, "potato"
^ rbt-unary-minus-parsing/example.rsl:9: issue: expression means -(a * b), place explicit brackets to clarify intent [unary_minus_precedence]
Processed 1 model(s), 0 check(s) and 0 requirement file(s) and found 1 warning(s)
3 changes: 0 additions & 3 deletions tests-system/unary-ops-1/output

This file was deleted.

3 changes: 0 additions & 3 deletions tests-system/unary-ops-1/output.smtlib

This file was deleted.

16 changes: 14 additions & 2 deletions trlc/ast.py
Original file line number Diff line number Diff line change
Expand Up @@ -591,6 +591,7 @@ def to_python_object(self):


class Null_Literal(Literal):
# lobster-trace: LRM.Primary
"""The null literal
This can appear in check expressions::
Expand All @@ -603,14 +604,12 @@ class Null_Literal(Literal):
"""
def __init__(self, token):
# lobster-exclude: Constructor only declares variables
assert isinstance(token, Token)
assert token.kind == "KEYWORD"
assert token.value == "null"
super().__init__(token.location, None)

def dump(self, indent=0): # pragma: no cover
# lobster-exclude: Debugging feature
self.write_indent(indent, "Null Literal")

def to_string(self):
Expand All @@ -630,6 +629,7 @@ def can_be_null(self):

class Integer_Literal(Literal):
# lobster-trace: LRM.Integer_Values
# lobster-trace: LRM.Primary
"""Integer literals
Note that these are always positive. A negative integer is
Expand Down Expand Up @@ -676,6 +676,7 @@ def can_be_null(self):

class Decimal_Literal(Literal):
# lobster-trace: LRM.Decimal_Values
# lobster-trace: LRM.Primary
"""Decimal literals
Note that these are always positive. A negative decimal is
Expand Down Expand Up @@ -723,6 +724,7 @@ def can_be_null(self):
class String_Literal(Literal):
# lobster-trace: LRM.String_Values
# lobster-trace: LRM.Markup_String_Values
# lobster-trace: LRM.Primary
"""String literals
Note the value of the string does not include the quotation marks,
Expand Down Expand Up @@ -778,6 +780,7 @@ def can_be_null(self):

class Boolean_Literal(Literal):
# lobster-trace: LRM.Boolean_Values
# lobster-trace: LRM.Primary
"""Boolean values
:attribute value: the boolean value
Expand Down Expand Up @@ -1166,6 +1169,9 @@ class Unary_Expression(Expression):
"""
def __init__(self, mh, location, typ, operator, n_operand):
# lobster-trace: LRM.Simple_Expression
# lobster-trace: LRM.Relation
# lobster-trace: LRM.Factor
super().__init__(location, typ)
assert isinstance(mh, Message_Handler)
assert isinstance(operator, Unary_Operator)
Expand Down Expand Up @@ -1329,6 +1335,11 @@ class Binary_Expression(Expression):
"""
def __init__(self, mh, location, typ, operator, n_lhs, n_rhs):
# lobster-trace: LRM.Expression
# lobster-trace: LRM.Relation
# lobster-trace: LRM.Simple_Expression
# lobster-trace: LRM.Term
# lobster-trace: LRM.Factor
super().__init__(location, typ)
assert isinstance(mh, Message_Handler)
assert isinstance(operator, Binary_Operator)
Expand Down Expand Up @@ -1731,6 +1742,7 @@ class Range_Test(Expression):
"""
def __init__(self, mh, location, typ, n_lhs, n_lower, n_upper):
# lobster-trace: LRM.Relation
super().__init__(location, typ)
assert isinstance(mh, Message_Handler)
assert isinstance(n_lhs, Expression)
Expand Down
4 changes: 4 additions & 0 deletions trlc/parser.py
Original file line number Diff line number Diff line change
Expand Up @@ -675,6 +675,7 @@ def parse_expression(self, scope):

def parse_relation(self, scope):
# lobster-trace: LRM.Relation
# lobster-trace: LRM.Operators
assert isinstance(scope, ast.Scope)
relop_mapping = {"==" : ast.Binary_Operator.COMP_EQ,
"!=" : ast.Binary_Operator.COMP_NEQ,
Expand Down Expand Up @@ -760,6 +761,8 @@ def parse_relation(self, scope):

def parse_simple_expression(self, scope):
# lobster-trace: LRM.Simple_Expression
# lobster-trace: LRM.Operators
# lobster-trace: LRM.Unary_Minus_Parsing
assert isinstance(scope, ast.Scope)
un_add_map = {"+" : ast.Unary_Operator.PLUS,
"-" : ast.Unary_Operator.MINUS}
Expand Down Expand Up @@ -816,6 +819,7 @@ def parse_simple_expression(self, scope):

def parse_term(self, scope):
# lobster-trace: LRM.Term
# lobster-trace: LRM.Operators
assert isinstance(scope, ast.Scope)
mul_map = {"*" : ast.Binary_Operator.TIMES,
"/" : ast.Binary_Operator.DIVIDE,
Expand Down

0 comments on commit 7d6d26e

Please sign in to comment.