metaborg/dynsem

RTCO does not propagate accumulated components

Opened this issue · 0 comments

Elimination of recursive tail calls may change the semantics of rules which accumulate results in semantic components:

  install-aliases(_, _) :: Als [] --> U() :: Als [].

  install-aliases(name, clos) :: Als [a@AliasL(_, ID(x)) | Als] --> u :: Als [a | Als']
  where
    name != x;
    install-aliases(name, clos) :: Als --> u :: Als'.

  ...

The second rule accumulates results in the Als read-write component. The rule is determined by the RTCO transformation as being tail recursive but the accumulated changes are dropped after the last call. At the end of the call chain the value of the semantic component Als is [] regardless of whether the list should or should not be empty.