include info in more .out files; fix parsing of as-patterns

2 files changed, 18 insertions, 13 deletions

diff --git a/src/LambdaCube/Compiler/Lexer.hs b/src/LambdaCube/Compiler/Lexer.hs
index c47ba1ce..fe3015a6 100644
--- a/src/LambdaCube/Compiler/Lexer.hs
+++ b/src/LambdaCube/Compiler/Lexer.hs
@@ -141,7 +141,16 @@ lexemeWithoutSpace p = do
 
 -- TODO?: eliminate; when eliminated, the SPos in parser state can be eliminated too
 appRange :: Parse r w (SI -> a) -> Parse r w a
-appRange p = (\fi p1 a p2 -> a $ RangeSI $ Range fi p1 p2) <$> asks fileInfo <*> getSPos <*> p <*> get
+appRange p = (\fi p1 a p2 -> a $ RangeSI $ Range fi p1 p2) <$> asks fileInfo <*> getSPos <*> p <*> getLexemeEnd
+
+getLexemeEnd = get
+
+noSpaceBefore p = try $ do
+    pos <- getLexemeEnd
+    x <- p
+    guard $ case sourceInfo x of
+        RangeSI (Range _ pos' _) -> pos == pos'
+    return x
 
 lexeme_ p = lexemeWithoutSpace p <* whiteSpace
 
@@ -224,9 +233,9 @@ upperLower      = lowerCase <|> upperCase_ <|> parens symbols
 
 ----------------------------------------------------------- operators and identifiers
 
-reservedOp name = lexeme $ try $ string name *> notFollowedBy opLetter
+reservedOp name = fst <$> lexeme_ (try $ string name *> notFollowedBy opLetter)
 
-reserved name = lexeme $ try $ string name *> notFollowedBy identLetter
+reserved name = fst <$> lexeme_ (try $ string name *> notFollowedBy identLetter)
 
 expect msg p i = i >>= \n -> if p n then unexpected (msg ++ " " ++ show n) else return n
 
diff --git a/src/LambdaCube/Compiler/Parser.hs b/src/LambdaCube/Compiler/Parser.hs
index 1d5139b8..79975251 100644
--- a/src/LambdaCube/Compiler/Parser.hs
+++ b/src/LambdaCube/Compiler/Parser.hs
@@ -172,8 +172,7 @@ parseTermLam =
      <|> mkIf <$ reserved "if"   <*> setR parseTermLam
               <* reserved "then" <*> setR parseTermLam
               <* reserved "else" <*> setR parseTermLam
-     <|> do reserved "forall"
-            (fe, ts) <- telescope $ Just $ Wildcard SType
+     <|> do (fe, ts) <- reserved "forall" *> telescope (Just $ Wildcard SType)
             f <- SPi . const Hidden <$ reservedOp "." <|> SPi . const Visible <$ reservedOp "->"
             t' <- deBruijnify fe <$> setR parseTermLam
             return $ foldr (uncurry f) t' ts
@@ -329,7 +328,7 @@ parsePatApp =
          PConSimp <$> addConsInfo upperCase_ <*> many (setR parsePatAt)
      <|> parsePatAt
 
-parsePatAt = concatParPats <$> sepBy1 (setR parsePatAtom) (reservedOp "@")
+parsePatAt = concatParPats <$> sepBy1 (setR parsePatAtom) (noSpaceBefore $ reservedOp "@")
   where
     concatParPats ps = ParPat $ concat [p | ParPat p <- ps]
 
@@ -373,7 +372,7 @@ parsePatAtom =
 longPattern = setR parsePatAnn <&> (reverse . getPVars &&& id)
 
 telescopePat = do
-    (a, b) <- fmap (reverse . foldMap (getPVars . snd) &&& id) $ many $ uncurry f <$> hiddenTerm (setR parsePatAtom) (setR parsePatAtom)
+    (a, b) <- fmap (reverse . foldMap (getPVars . snd) &&& id) $ many $ uncurry f <$> hiddenTerm (setR parsePatAt) (setR parsePatAt)
     checkPattern a
     return (a, b)
   where
@@ -468,8 +467,7 @@ parseRHS :: String -> BodyParser GuardTrees
 parseRHS tok = do
     mkGuards <$> some (reservedOp "|" *> guard) <*> option [] (reserved "where" *> parseDefs)
   <|> do
-    reservedOp tok
-    rhs <- setR parseTermLam
+    rhs <- reservedOp tok *> setR parseTermLam
     f <- option id $ mkLets <$ reserved "where" <*> parseDefs
     noGuards <$> trackSI (pure $ f rhs)
   where
@@ -493,8 +491,7 @@ funAltDef parseOpName parseName = do
           Just opName -> try_ "operator definition" $ do
             (e', a1) <- longPattern
             n <- opName
-            (e'', a2) <- longPattern
-            lookAhead $ reservedOp "=" <|> reservedOp "|"
+            (e'', a2) <- longPattern <* lookAhead (reservedOp "=" <|> reservedOp "|")
             let fee = e'' <> e'
             checkPattern fee
             return (n, (fee, (,) (Visible, Wildcard SType) <$> [a1, deBruijnify e' a2]))
@@ -539,8 +536,7 @@ parseModule = do
     whiteSpace
     header <- optional $ do
         modn <- reserved "module" *> moduleName
-        exps <- optional (parens $ commaSep parseExport)
-        reserved "where"
+        exps <- optional (parens $ commaSep parseExport) <* reserved "where"
         return (modn, exps)
     let mkIDef _ n i h _ = (n, f i h)
           where