Pretty-printer fails on some ambiguous programs
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> his 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-V-listto the amb-node. This fails because
pp-*-listexpects a list and not an amb-node.
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-allstrategy 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]) -> hyields 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: ) (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"]) )
Log in to post comments