@@ -939,6 +939,11 @@ rewriteTerm syn = do keyword "rewrite"
939 return (PRewrite fc using prf sc giving)
939 return (PRewrite fc using prf sc giving)
940 <?> "term rewrite expression"
940 <?> "term rewrite expression"
942+-- | Parse a constant and its source span
943+rigCount :: Parsing m => m RigCount
944+rigCount = P.option RigW $ do lchar '1'; return Rig1
945+ <|> do lchar '0'; return Rig0
942{- |Parses a let binding
947{- |Parses a let binding
@@ -957,18 +962,19 @@ let_ syn = P.try (do keyword "let"
957 return (buildLets ls sc))
962 return (buildLets ls sc))
958 <?> "let binding"
963 <?> "let binding"
959 where buildLets [] sc = sc
964 where buildLets [] sc = sc
960− buildLets ((fc, PRef nfc _ n, ty, v, []) : ls) sc
965+ buildLets ((fc, rc, PRef nfc _ n, ty, v, []) : ls) sc
961− = PLet fc RigW n nfc ty v (buildLets ls sc)
966+ = PLet fc rc n nfc ty v (buildLets ls sc)
962− buildLets ((fc, pat, ty, v, alts) : ls) sc
967+ buildLets ((fc, _, pat, ty, v, alts) : ls) sc
963 = PCase fc v ((pat, buildLets ls sc) : alts)
968 = PCase fc v ((pat, buildLets ls sc) : alts)
970+let_binding syn = do rc <- rigCount
965−let_binding syn = do (pat, fc) <- withExtent $ expr' (syn { inPattern = True })
971+ (pat, fc) <- withExtent $ expr' (syn { inPattern = True })
966 ty <- P.option Placeholder (do lchar ':'; expr' syn)
972 ty <- P.option Placeholder (do lchar ':'; expr' syn)
967 lchar '='
973 lchar '='
968 v <- expr (syn { withAppAllowed = isVar pat })
974 v <- expr (syn { withAppAllowed = isVar pat })
969 ts <- P.option [] (do lchar '|'
975 ts <- P.option [] (do lchar '|'
970 P.sepBy1 (do_alt syn) (lchar '|'))
976 P.sepBy1 (do_alt syn) (lchar '|'))
971− return (fc,pat,ty,v,ts)
977+ return (fc,rc,pat,ty,v,ts)
972 where isVar (PRef _ _ _) = True
978 where isVar (PRef _ _ _) = True
973 isVar _ = False
979 isVar _ = False
@@ -1169,7 +1175,7 @@ FunctionSignatureList ::=
1171typeDeclList :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
1177typeDeclList :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
1172−typeDeclList syn = P.try (P.sepBy1 (do rig <- P.option RigW rigCount
1178+typeDeclList syn = P.try (P.sepBy1 (do rig <- rigCount
1173 (x, xfc) <- withExtent fnName
1179 (x, xfc) <- withExtent fnName
1174 lchar ':'
1180 lchar ':'
1175 t <- typeExpr (disallowImp syn)
1181 t <- typeExpr (disallowImp syn)
@@ -1180,9 +1186,6 @@ typeDeclList syn = P.try (P.sepBy1 (do rig <- P.option RigW rigCount
1180 t <- typeExpr (disallowImp syn)
1186 t <- typeExpr (disallowImp syn)
1181 return (map (\(x, xfc) -> (RigW, x, xfc, t)) ns)
1187 return (map (\(x, xfc) -> (RigW, x, xfc, t)) ns)
1182 <?> "type declaration list"
1188 <?> "type declaration list"
1184− rigCount = do lchar '1'; return Rig1
1185− <|> do lchar '0'; return Rig0
1187{- | Parses a type declaration list with optional parameters
1190{- | Parses a type declaration list with optional parameters