metaborg / nabl

Spoofax' Name Binding Language
Apache License 2.0
7 stars 12 forks source link

Bugfix/nested completeness #50

Closed AZWN closed 3 years ago

AZWN commented 3 years ago

Fixes the issue that this test exposes:

resolve {s_data1 s_data2 res}
  new s_data1,
  new s_data2,
  s_data2 -INHERIT-> s_data1,
  lub(s_data1, s_data2) == res

signature
  name-resolution
    labels
      INHERIT

rules
  lub : scope * scope -> list((path * scope))
  lub(s1, s2) = paths :-
    query ()
      filter INHERIT* and { s_super :-
        query ()
          filter INHERIT* and { s_data :- s_data == s_super }
          in s2 |-> [_|_]
      }
    in s1 |-> paths.

Basically, the issue was that entailment contexts as instantiated by the name resolution algorithm would always consider all critical edges closed, which made nested query in data{wf,leq} invalid. This changes ensures that the isComplete predicate from the parent solver is passed to the solver that evaluates the data{wf,leq} conditions.

AZWN commented 3 years ago

@hendrikvanantwerpen This is a bugfix for the issue Ivo showed. See the description for my analysis of the rout cause. These adaptions should ensure that the subsolver for the data{wf,leq} constraints is now instantiated in the same way as the one for the try. Since this is the first time for me to touch this code, would you be as kind as to reflect whether this approach/solution is right?

Also, the history shows two approaches (passing completeness or params::isComplete from the parent solver.). I think the last one is most clean, but would be curious to what you think.