Skip to content

Commit

Permalink
Remove the Predecessor field from Field_Cursor record
Browse files Browse the repository at this point in the history 
This field was not needed anymore

For eng/recordflux/recordflux#1387
  • Loading branch information
@kanigsson
kanigsson committed Sep 20, 2023
1 parent a79b12e commit cefd4fc
Show file tree
Hide file tree
Showing 56 changed files with 833 additions and 2,424 deletions.
4 changes: 4 additions & 0 deletions CHANGELOG.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,10 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0

- Functions `Valid_Next_Internal`, `Field_Size_Internal`, `Field_First_Internal` (eng/recordflux/RecordFlux#1382)

### Changed

- Removed `Predecessor` field from `Field_Cursor` record (eng/recordflux/RecordFlux#1387)

### Removed

- Functions `Valid_Predecessor` and `Path_Condition` (eng/recordflux/RecordFlux#1382)
Expand Down
58 changes: 7 additions & 51 deletions rflx/generator/common.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -403,16 +403,6 @@ def link_property(link: model.Link, unique: bool) -> Expr:
),
size.ada_expr(),
),
Equal(
Selected(
Indexed(
prefixed("Cursors").ada_expr(),
Variable(link.target.affixed_name),
),
"Predecessor",
),
Variable(link.source.affixed_name),
),
Equal(
Selected(
Indexed(
Expand Down Expand Up @@ -585,21 +575,12 @@ def valid_path_to_next_field_condition(
l.condition.substituted(substitution(message, public=True, prefix=prefix))
.simplified()
.ada_expr(),
And(
Equal(
Call(
"Predecessor",
[Variable("Ctx"), Variable(l.target.affixed_name)],
),
Variable(field.affixed_name),
),
Call(
"Valid_Next",
[Variable("Ctx"), Variable(l.target.affixed_name)],
)
if l.target != model.FINAL
else TRUE,
),
Call(
"Valid_Next",
[Variable("Ctx"), Variable(l.target.affixed_name)],
)
if l.target != model.FINAL
else TRUE,
),
],
)
Expand Down Expand Up @@ -719,16 +700,6 @@ def initialize_field_statements(
("First", Variable("First")),
("Last", Variable("Last")),
("Value", Number(0)),
(
"Predecessor",
Selected(
Indexed(
Variable("Ctx.Cursors"),
Variable(field.affixed_name),
),
"Predecessor",
),
),
),
),
Assignment(
Expand All @@ -741,7 +712,6 @@ def initialize_field_statements(
),
NamedAggregate(
("State", Variable("S_Invalid")),
("Predecessor", Variable(field.affixed_name)),
("others", Variable("<>")),
),
),
Expand Down Expand Up @@ -1060,24 +1030,10 @@ def context_cursors_initialization(message: model.Message) -> Expr:
message.fields[0].affixed_name,
NamedAggregate(
("State", Variable("S_Invalid")),
(
"Predecessor",
Variable(model.INITIAL.affixed_name),
),
("others", Variable("<>")),
),
),
(
"others",
NamedAggregate(
("State", Variable("S_Invalid")),
(
"Predecessor",
Variable(model.FINAL.affixed_name),
),
("others", Variable("<>")),
),
),
("others", Variable("<>")),
)


Expand Down
1 change: 0 additions & 1 deletion rflx/generator/generator.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -577,7 +577,6 @@ def _create_message(self, message: Message) -> dict[ID, Unit]: # noqa: PLR0912
scalar_fields,
composite_fields,
),
self._executor.submit(message_generator.create_predecessor_function),
self._executor.submit(
message_generator.create_successor_function,
self._prefix,
Expand Down
112 changes: 2 additions & 110 deletions rflx/generator/message.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -215,11 +215,6 @@ def create_cursor_type() -> UnitPart:
RecordType(
"Field_Cursor",
[
Component(
"Predecessor",
"Virtual_Field",
Variable(FINAL.affixed_name),
),
Component(
"State",
"Cursor_State",
Expand Down Expand Up @@ -432,16 +427,6 @@ def create_valid_predecessors_invariant_function(
)
if l.source != INITIAL
else expr.TRUE,
expr.Equal(
expr.Selected(
expr.Indexed(
expr.Variable("Cursors"),
expr.Variable(f.affixed_name),
),
"Predecessor",
),
expr.Variable(l.source.affixed_name),
),
l.condition.substituted(
common.substitution(
message,
Expand Down Expand Up @@ -508,18 +493,8 @@ def create_valid_next_internal_function(
)

def link_expr(link: Link) -> Expr:
pred_cond = Equal(
Selected(
Indexed(
Variable("Cursors"),
Variable(link.target.affixed_name),
),
"Predecessor",
),
Variable(link.source.affixed_name),
)
if link.source == INITIAL:
return pred_cond
return TRUE
condition = link.condition.substituted(
common.substitution(message, prefix, embedded=True),
).simplified()
Expand All @@ -529,7 +504,6 @@ def link_expr(link: Link) -> Expr:
[Indexed(Variable("Cursors"), Variable(link.source.affixed_name))],
),
condition.ada_expr(),
pred_cond,
)

def valid_next_expr(fld: Field) -> Expr:
Expand Down Expand Up @@ -947,12 +921,7 @@ def create_context_type(message: Message) -> UnitPart:
Component(
"Cursors",
"Field_Cursors",
NamedAggregate(
(
"others",
Variable("<>"),
),
),
NamedAggregate(("others", Variable("<>"))),
),
],
discriminants,
Expand Down Expand Up @@ -2251,50 +2220,6 @@ def condition(field: Field, message: Message) -> Expr:
)


def create_predecessor_function() -> UnitPart:
specification = FunctionSpecification(
"Predecessor",
"Virtual_Field",
[Parameter(["Ctx"], "Context"), Parameter(["Fld"], "Virtual_Field")],
)

return UnitPart(
[
# Eng/RecordFlux/Workarounds#47
Pragma(
"Warnings",
[Variable("Off"), String("postcondition does not mention function result")],
),
SubprogramDeclaration(specification, [Postcondition(TRUE)]),
Pragma(
"Warnings",
[Variable("On"), String("postcondition does not mention function result")],
),
],
private=[
ExpressionFunctionDeclaration(
specification,
Case(
Variable("Fld"),
[
(
Variable(INITIAL.affixed_name),
Variable(INITIAL.affixed_name),
),
(
Variable("others"),
Selected(
Indexed(Variable("Ctx.Cursors"), Variable("Fld")),
"Predecessor",
),
),
],
),
),
],
)


def create_successor_function(prefix: str, message: Message) -> UnitPart:
specification = FunctionSpecification(
"Successor",
Expand Down Expand Up @@ -2880,7 +2805,6 @@ def create_reset_dependent_fields_procedure(prefix: str, message: Message) -> Un
),
NamedAggregate(
("State", Variable("S_Invalid")),
("Predecessor", Variable(FINAL.affixed_name)),
("others", Variable("<>")),
),
),
Expand All @@ -2907,16 +2831,6 @@ def create_reset_dependent_fields_procedure(prefix: str, message: Message) -> Un
),
NamedAggregate(
("State", Variable("S_Invalid")),
(
"Predecessor",
Selected(
Indexed(
Variable("Ctx.Cursors"),
Variable("Fld"),
),
"Predecessor",
),
),
("others", Variable("<>")),
),
),
Expand Down Expand Up @@ -2952,10 +2866,6 @@ def create_reset_dependent_fields_procedure(prefix: str, message: Message) -> Un
*[
Equal(e, Old(e))
for e in [
Selected(
Indexed(Variable("Ctx.Cursors"), Variable("Fld")),
"Predecessor",
),
Call("Has_Buffer", [Variable("Ctx")]),
Call(
"Field_First",
Expand Down Expand Up @@ -3085,13 +2995,6 @@ def specification(field: Field) -> ProcedureSpecification:
*[
Equal(e, Old(e))
for e in [
Call(
"Predecessor",
[
Variable("Ctx"),
Variable(f.affixed_name),
],
),
Call(
"Field_Last",
[
Expand Down Expand Up @@ -3417,7 +3320,6 @@ def take_buffer_arguments(field: Field) -> abc.Sequence[Expr]:
"First",
"Last",
"Value",
"Predecessor",
)
],
),
Expand All @@ -3437,16 +3339,6 @@ def take_buffer_arguments(field: Field) -> abc.Sequence[Expr]:
),
NamedAggregate(
("State", Variable("S_Invalid")),
(
"Predecessor",
Selected(
Indexed(
Variable("Ctx.Cursors"),
Variable(f.affixed_name),
),
"Predecessor",
),
),
("others", Variable("<>")),
),
),
Expand Down
30 changes: 0 additions & 30 deletions rflx/generator/parser.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -361,8 +361,6 @@ def create_verify_procedure(
),
),
NamedAggregate(
("State", Variable("S_Invalid")),
("Predecessor", Variable("Fld")),
("others", Variable("<>")),
),
),
Expand Down Expand Up @@ -466,16 +464,6 @@ def create_verify_procedure(
Variable("Fld"),
),
NamedAggregate(
(
"State",
Variable("S_Invalid"),
),
(
"Predecessor",
Variable(
FINAL.affixed_name,
),
),
("others", Variable("<>")),
),
),
Expand All @@ -492,10 +480,6 @@ def create_verify_procedure(
),
NamedAggregate(
("State", Variable("S_Incomplete")),
(
"Predecessor",
Variable(FINAL.affixed_name),
),
("others", Variable("<>")),
),
),
Expand Down Expand Up @@ -1240,10 +1224,6 @@ def set_context_cursor_scalar() -> Assignment:
("First", Call("Field_First", [Variable("Ctx"), Variable("Fld")])),
("Last", Call("Field_Last", [Variable("Ctx"), Variable("Fld")])),
("Value", Variable("Value")),
(
"Predecessor",
Selected(Indexed(Variable("Ctx.Cursors"), Variable("Fld")), "Predecessor"),
),
),
)

Expand Down Expand Up @@ -1271,15 +1251,5 @@ def set_context_cursor_composite_field(field_name: str) -> Assignment:
),
),
("Value", Variable("Value")),
(
"Predecessor",
Selected(
Indexed(
Variable("Ctx.Cursors"),
Variable(field_name),
),
"Predecessor",
),
),
),
)
Loading

0 comments on commit cefd4fc

Please sign in to comment.