Skip to content

Commit

Permalink
adds tracing for conditional expressions (#40)
Browse files Browse the repository at this point in the history
adds tracing for chapter 15
  • Loading branch information
christophkloeffel authored Oct 24, 2023
1 parent a1f208c commit 91a4f33
Show file tree
Hide file tree
Showing 22 changed files with 88 additions and 37 deletions.
2 changes: 1 addition & 1 deletion language-reference-manual/lrm.trlc
Original file line number Diff line number Diff line change
Expand Up @@ -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.'''
}
Expand Down
6 changes: 0 additions & 6 deletions tests-system/if_expressions/foo.check

This file was deleted.

7 changes: 0 additions & 7 deletions tests-system/if_expressions/foo.rsl

This file was deleted.

7 changes: 0 additions & 7 deletions tests-system/if_expressions/output

This file was deleted.

2 changes: 0 additions & 2 deletions tests-system/if_expressions/output.brief

This file was deleted.

5 changes: 0 additions & 5 deletions tests-system/if_expressions/output.json

This file was deleted.

7 changes: 0 additions & 7 deletions tests-system/if_expressions/output.smtlib

This file was deleted.

11 changes: 11 additions & 0 deletions tests-system/rbt-conditional-expression-types/foo.rsl
Original file line number Diff line number Diff line change
@@ -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"
}
File renamed without changes.
3 changes: 3 additions & 0 deletions tests-system/rbt-conditional-expression-types/output
Original file line number Diff line number Diff line change
@@ -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)
1 change: 1 addition & 0 deletions tests-system/rbt-conditional-expression-types/output.brief
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
rbt-conditional-expression-types/foo.rsl:10:8: trlc error: expected expression of type Builtin_Boolean, got Builtin_Integer instead
3 changes: 3 additions & 0 deletions tests-system/rbt-conditional-expression-types/output.json
Original file line number Diff line number Diff line change
@@ -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)
3 changes: 3 additions & 0 deletions tests-system/rbt-conditional-expression-types/output.smtlib
Original file line number Diff line number Diff line change
@@ -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)
15 changes: 15 additions & 0 deletions tests-system/rbt-conditional-expression/foo.rsl
Original file line number Diff line number Diff line change
@@ -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"
}
8 changes: 8 additions & 0 deletions tests-system/rbt-conditional-expression/foo.trlc
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
package Foo

T test_01 {
x = 5
y = 10
z = 1
b = false
}
9 changes: 9 additions & 0 deletions tests-system/rbt-conditional-expression/output
Original file line number Diff line number Diff line change
@@ -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)
4 changes: 4 additions & 0 deletions tests-system/rbt-conditional-expression/output.brief
Original file line number Diff line number Diff line change
@@ -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
9 changes: 9 additions & 0 deletions tests-system/rbt-conditional-expression/output.json
Original file line number Diff line number Diff line change
@@ -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)
9 changes: 9 additions & 0 deletions tests-system/rbt-conditional-expression/output.smtlib
Original file line number Diff line number Diff line change
@@ -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)
2 changes: 2 additions & 0 deletions tests-system/rbt-conditional-expression/tracing
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
LRM.Conditional_Expression_Evaluation
LRM.Conditional_Expression_Else
11 changes: 9 additions & 2 deletions trlc/ast.py
Original file line number Diff line number Diff line change
Expand Up @@ -1814,6 +1814,7 @@ class Action(Node):
"""
def __init__(self, mh, t_kind, n_condition, n_expression):
# lobster-trace: LRM.Conditional_Expression
assert isinstance(mh, Message_Handler)
assert isinstance(t_kind, Token)
assert t_kind.kind == "KEYWORD"
Expand All @@ -1824,7 +1825,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
Expand Down Expand Up @@ -1866,14 +1867,16 @@ class Conditional_Expression(Expression):
"""
def __init__(self, location, if_action):
# lobster-exclude: Constructor only declares variables
# lobster-trace: LRM.Conditional_Expression
assert isinstance(if_action, Action)
assert if_action.kind == "if"
super().__init__(location, if_action.n_expr.typ)
self.actions = [if_action]
self.else_expr = None

def add_elsif(self, mh, n_action):
# lobster-trace: LRM.Conditional_Expression
# lobster-trace; LRM.Conditional_Expression_Types
assert isinstance(mh, Message_Handler)
assert isinstance(n_action, Action)
assert n_action.kind == "elsif"
Expand All @@ -1882,6 +1885,8 @@ 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
# lobster-trace; LRM.Conditional_Expression_Types
assert isinstance(mh, Message_Handler)
assert isinstance(n_expr, Expression)

Expand All @@ -1904,6 +1909,8 @@ def to_string(self):
return rv

def evaluate(self, mh, context):
# lobster-trace: LRM.Conditional_Expression_Else
# lobster-trace: LRM.Conditional_Expression_Evaluation
assert isinstance(mh, Message_Handler)
assert context is None or isinstance(context, dict)

Expand Down
1 change: 1 addition & 0 deletions trlc/parser.py
Original file line number Diff line number Diff line change
Expand Up @@ -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")
Expand Down

0 comments on commit 91a4f33

Please sign in to comment.