Problem

The Spoofax-generated pretty-printer contains rewrite rules to allow pretty-printing of ambiguous sentences. Specifically, for every sort S, a strategy prettyprint-L-S: amb([h|hs]) -> <prettyprint-L-S> h is created to map the amb-term to the first alternative.

This approach works fine when the amb-node takes the position of a constructor application. However, when the amb-node is in the position of a list, the pretty-printer applies pp-H-list or pp-V-list to the amb-node. This fails because pp-*-list expects a list and not an amb-node.

Proposed Solution

Option 1: Define the following strategies in libspoofax/pp (and similar for pp-Z-list, pp-HZ-list, etc):

  pp-H-list(pp):
    amb([h|t]) -> <pp-H-list(pp)> h

  pp-H-list(pp|sep):
    amb([h|t]) -> <pp-H-list(pp|sep)> h

Option 2. Create a disambiguate-all strategy that is called before pretty-printing the term:

disambiguate-all = topdown(repeat(disambiguate))
disambiguate: amb([h|t]) -> h

Option 2 introduces an extra traversal, so option 1 is preferred.

Submitted by Martijn on 4 December 2017 at 16:03

On top of that, with the current imploder it may not always be the case that amb([h|t]) -> h yields a well-formed term. For example, in metaborg-coq we have the signature:

Binds : List(Name) * Term -> Binder
      : Ident -> Name
      : String -> Ident

parsing the following program:

CoFixpoint
B _ (_k5lU A: [18]) (a: x) := x : x.

yields the following AST:

Binds(
  [amb([["_k5lU"], [WldName(), "k5lU"]]), "A"]
, List(["18"])
)

if we replace the amb-node by either of its alternatives we are left with a nested list, i.e. an ill-formed term. Either the disambiguation logic needs to take care of flattening these lists (i.e. amb-node whose children are lists and that is placed within a list itself needs to be handled differently, except when the amb-node is placed within another amb-node) or the imploder should have constructed a more general term:

Binds(
  amb([["_k5lU", "A"], [WldName(), "k5lU", "A"]])
, List(["18"])
)