Functional constraint normalization in Template Messages

Bug description When an functional predicate application is used in a message template, it is not lifted. This causes an exception when loading a specification.

Versions Spoofax version: Spoofax 2.5.16 Statix setup: Both single-file and multi-file.

Steps to reproduce the behavior Execute the following test:

resolve false | error $[[fmt()]]

rules
  fmt: -> string
  fmt() = "msg".

Observed behavior The transformation fails with an exception:

org.metaborg.core.transform.TransformException: Invoking Stratego strategy editor-evaluate-traditional failed at term:
    Test(
  CFalse(
    Message(
      Error(){TermIndex("bugs.stxtest", 1)}
    , Formatted([Term(COp("fmt"{TermIndex("bugs.stxtest", 2)}, []{TermIndex("bugs.stxtest", 4)}){TermIndex("bugs.stxtest", 5)}){TermIndex("bugs.stxtest", 6)}]{TermIndex("bugs.stxtest", 9)}){TermIndex("bugs.stxtest", 10)}
    , NoOrigin(){TermIndex("bugs.stxtest", 11)}
    ){TermIndex("bugs.stxtest", 12)}
  ){TermIndex("bugs.stxtest", 13)}
, [ Rules(
      [ CDecl(InductiveC(){TermIndex("bugs.stxtest", 14)}, "fmt"{TermIndex("bugs.stxtest", 15)}, FunType([]{TermIndex("bugs.stxtest", 17)}, StringSort(){TermIndex("bugs.stxtest", 18)}){TermIndex("bugs.stxtest", 19)}){TermIndex("bugs.stxtest", 20)}
      , Rule(NoName(){TermIndex("bugs.stxtest", 21)}, F("fmt"{TermIndex("bugs.stxtest", 22)}, []{TermIndex("bugs.stxtest", 24)}, Str("msg"{TermIndex("bugs.stxtest", 25)}){TermIndex("bugs.stxtest", 26)}){TermIndex("bugs.stxtest", 27)}, CTrue(){TermIndex("bugs.stxtest", 28)}){TermIndex("bugs.stxtest", 29), DesugaredAxiomRule()}
      ]{TermIndex("bugs.stxtest", 33)}
    ){TermIndex("bugs.stxtest", 34)}
  ]{TermIndex("bugs.stxtest", 37)}
){TermIndex("bugs.stxtest", 38)}
Stratego trace:
    editor_evaluate_traditional_0_0
    editor_evaluate_traditional_0_0
    with_1_1
    evaluate_traditional_0_0
    evaluate_1_0
    with_1_1 <==
    solve_1_2
    stx__solve_constraint_0_2
    stx__solve_constraint_0_4

Expected behavior We expect the test to execute, and give a .stxresult file containing an error with text "msg".

Additional context

During normalization, functional constraints are translated to predicative constraints. As part of that process, functional constraint instantiations that occur inside other terms are lifted into a separate constraint, and their original position is substituted with a new variable. This lifting is not applied to messages, and hence functional rule application terms remain in the normalized specification, while they should be normalized away.

metaborg / nabl

Functional constraint normalization in Template Messages #54