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

Whitespace-sensitive parsing of let binding without ascription #113

Open
ohad opened this issue Oct 5, 2019 · 1 comment
Open

Whitespace-sensitive parsing of let binding without ascription #113

ohad opened this issue Oct 5, 2019 · 1 comment

Comments

@ohad
Copy link

ohad commented Oct 5, 2019

Sorry if this is a feature!

Steps to Reproduce

Type-check the following declarations:

x1 : Nat
x1 = 
  let u = 
     S
     Z
  in
  1

x2 : Nat
x2 = 
  let u = 
   S Z
  in
  1

x3 : Nat
x3 = 
  let u = 
    S Z
  in
  1

x4 : Nat
x4 = 
  let u = S Z
  in
  1

x5 : Nat
x5 = 
  let u = 
     S Z
  in
  1

Expected Behavior

These should all type-check.

Observed Behavior

The following don't type-check, with the below errors:

x1 : Nat
x1 = 
  let u = 
     S
     Z
  in
  1
Parse error: Expected 'case', 'if', 'do', application or operator expression (next tokens: [let, identifier u, symbol =, identifier S, identifier Z, in, literal 1, end of input])

x2 : Nat
x2 = 
  let u = 
   S Z
  in
  1
Parse error: Expected 'case', 'if', 'do', application or operator expression (next tokens: [let, identifier u, symbol =, identifier S, identifier Z, in, literal 1, end of input])

x3 : Nat
x3 = 
  let u = 
    S Z
  in
  1
Foo.idr:21:7--22:7:While processing right hand side of Main.x4 at Foo.idr:20:1--42:1:
No type declaration for Main.u

The following type-check

x4 : Nat
x4 = 
  let u = S Z
  in
  1

x5 : Nat
x5 = 
  let u = 
     S Z
  in
  1
@edwinb
Copy link
Owner

edwinb commented Feb 22, 2020

I don't think they should, because the body of the let should be indented further right than the u. Actually I think x5 should also be rejected but I can see why it isn't, looking at the code for the parser.

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

2 participants