"""
Forward Semantics
=================
Lyra's internal forward semantics of statements.
:Authors: Caterina Urban
"""
from lyra.core.expressions import BinarySequenceOperation, ListDisplay
from lyra.core.types import ListLyraType
from lyra.semantics.semantics import Semantics, DefaultSemantics
from lyra.abstract_domains.state import State
from lyra.core.statements import Assignment, Call
[docs]class ForwardSemantics(Semantics):
"""Forward semantics of statements."""
[docs] def append_call_semantics(self, stmt: Call, state: State) -> State:
assert len(stmt.arguments) == 2
targets = self.semantics(stmt.arguments[0], state).result
op = BinarySequenceOperation.Operator.Concat
values = self.semantics(stmt.arguments[1], state).result
rhs = set()
for target in targets:
for value in values:
display = ListDisplay(ListLyraType(value.typ), [value])
rhs.add(BinarySequenceOperation(target.typ, target, op, display))
return state.assign(targets, rhs)
[docs]class UserDefinedCallSemantics(ForwardSemantics):
"""Forward semantics of user-defined function/method calls."""
# noinspection PyUnusedLocal
[docs] def user_defined_call_semantics(self, stmt: Call, state: State):
"""Forward semantics of a user-defined function/method call.
:param stmt: call statement to be executed
:param state: state before executing the call statement
:return: state modified by the call statement
"""
error = f"Forward semantics for call statement {stmt} not yet implemented!"
raise NotImplementedError(error)
[docs]class AssignmentSemantics(ForwardSemantics):
"""Forward semantics of assignments."""
[docs] def assignment_semantics(self, stmt: Assignment, state: State) -> State:
"""Forward semantics of an assignment.
:param stmt: assignment statement to be executed
:param state: state before executing the assignment
:return: state modified by the assignment
"""
lhs = self.semantics(stmt.left, state).result # lhs evaluation
rhs = self.semantics(stmt.right, state).result # rhs evaluation
return state.assign(lhs, rhs)
# noinspection PyAbstractClass
[docs]class DefaultForwardSemantics(DefaultSemantics, UserDefinedCallSemantics, AssignmentSemantics):
"""Default forward semantics of statements."""
pass