@@ -40,6 +40,7 @@ parseProg :: String -> Idris [PDecl]
4040parseProg fname = do file <- lift $ readFile fname
4141 i <- get
4242 case (runParser (do ps <- many1 pDecl
43+ eof
4344 i' <- getState
4445 return (ps, i')) i fname file) of
4546 Left err -> fail (show err)
@@ -59,6 +60,7 @@ pDecl' = try pFixity
5960 <|> try (do n <- pfName; ty <- pTSig
6061 return (PTy n ty))
6162 <|> try pData
63+ <|> try pPattern
6264
6365-------- Fixity --------
6466
@@ -98,6 +100,11 @@ pSimpleExpr =
98100 <|> try (do lchar '('; e <- pExpr; lchar ')'; return e)
99101 <|> try (do reserved "Set"; return PSet)
100102
103+pHSimpleExpr = try pSimpleExpr
104+ <|> do lchar '.'
105+ e <- pSimpleExpr
106+ return $ PHidden e
107+
101108pApp = do f <- pSimpleExpr
102109 args <- many1 pSimpleExpr
103110 return (PApp f [] args)
@@ -168,3 +175,16 @@ pSimpleCon = do cn <- pfName
168175
169176--------- Pattern match clauses ---------
170177
178+pPattern :: IParser PDecl
179+pPattern = try (do n <- pfName
180+ args <- many pHSimpleExpr
181+ lchar '='
182+ rhs <- pExpr
183+ return $ PClause (PApp (PRef n) [] args) rhs)
184+ <|> do l <- pSimpleExpr
185+ op <- operator
186+ r <- pSimpleExpr
187+ lchar '='
188+ rhs <- pExpr
189+ return $ PClause (PApp (PRef (UN [op])) [] [l,r]) rhs
190+