Idris2-boot icon indicating copy to clipboard operation
Idris2-boot copied to clipboard

Whitespace-sensitive parsing of let binding without ascription

Open ohad opened this issue 6 years ago • 1 comments

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

ohad avatar Oct 05 '19 05:10 ohad

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.

edwinb avatar Feb 22 '20 18:02 edwinb