[ fix #1887 ] Parse _ <- as DoBind instead of DoBinPat

Author: gallais

src/Idris/Parser.idr

@@ -843,13 +843,13 @@ mutual
 
   validPatternVar : Name -> EmptyRule ()
   validPatternVar (UN n)
-      = if lowerFirst n then pure ()
-                        else fail "Not a pattern variable"
+      = unless (lowerFirst n || n == "_") $
+          fail "Not a pattern variable"
   validPatternVar _ = fail "Not a pattern variable"
 
   doAct : OriginDesc -> IndentInfo -> Rule (List PDo)
   doAct fname indents
-      = do b <- bounds (do n <- bounds name
+      = do b <- bounds (do n <- bounds (name <|> UN "_" <$ symbol "_")
                            -- If the name doesn't begin with a lower case letter, we should
                            -- treat this as a pattern, so fail
                            validPatternVar n.val

src/Libraries/Text/Parser.idr

@@ -226,3 +226,8 @@ public export
 when : Bool -> Lazy (Grammar state token False ()) -> Grammar state token False ()
 when True y = y
 when False y = pure ()
+
+public export
+%inline
+unless : Bool -> Lazy (Grammar state token False ()) -> Grammar state token False ()
+unless = when . not

tests/Main.idr

@@ -41,6 +41,7 @@ idrisTestsBasic = MkTestPool "Fundamental language features" [] Nothing
        "basic046", "basic047",             "basic049", "basic050",
        "basic051", "basic052", "basic053", "basic054", "basic055",
        "basic056", "basic057", "basic058", "basic059", "basic060",
+       "basic061",
        "interpolation001", "interpolation002"]
 
 idrisTestsCoverage : TestPool

tests/idris2/basic061/IgnoreDo.idr

@@ -0,0 +1,16 @@
+module IgnoreDo
+
+bound : Maybe () -> Maybe b -> Maybe b
+bound m n = do
+  x <- m
+  n
+
+ignored : Maybe () -> Maybe b -> Maybe b
+ignored m n = do
+  _ <- m
+  n
+
+seqd : Maybe () -> Maybe b -> Maybe b
+seqd m n = do
+  m
+  n

tests/idris2/basic061/expected

@@ -0,0 +1,8 @@
+1/1: Building IgnoreDo (IgnoreDo.idr)
+IgnoreDo> IgnoreDo.bound : Maybe () -> Maybe b -> Maybe b
+bound m n = m >>= (\x => n)
+IgnoreDo> IgnoreDo.ignored : Maybe () -> Maybe b -> Maybe b
+ignored m n = m >>= (\_ => n)
+IgnoreDo> IgnoreDo.seqd : Maybe () -> Maybe b -> Maybe b
+seqd m n = m >> Delay n
+IgnoreDo> Bye for now!

tests/idris2/basic061/input

@@ -0,0 +1,4 @@
+:printdef bound
+:printdef ignored
+:printdef seqd
+:q

tests/idris2/basic061/run

@@ -0,0 +1,3 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner IgnoreDo.idr < input