Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Parser treats indentation sensitive syntax wrongly #10

Open
skingo opened this issue Nov 9, 2019 · 0 comments
Open

Parser treats indentation sensitive syntax wrongly #10

skingo opened this issue Nov 9, 2019 · 0 comments

Comments

@skingo
Copy link
Contributor

skingo commented Nov 9, 2019

The simple_nested.ub example fails after destructorizing Stream, since all "trailing" cocases are always added to the last seen comatch instead of the correct on (i.e. the one with the same indentation).
As a workaround, one can add id functions around local xtors, which has the side effect of surrounding the resulting xmatches by parentheses, thus making them parse correctly.

data Bool where
   True()
   False()

codata Stream where
   s() : Stream
   s2() : Stream

fun id(x0 : Stream) : Stream :=
   x0



gfun Simpl() : Stream :=
   cocase s() => Simpl()
   cocase s2() => id(comatch L2  with
      cocase s() => id(comatch L1  with
         cocase s() => id(comatch L3  with
            cocase s() => Simpl()
            cocase s2() => Simpl())
         cocase s2() => Simpl())
      cocase s2() => Simpl())
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant