8215c60 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fix zero argument with clauses

8215c60Edwin Brady12 years ago

src/Idris/ElabDecls.hs+3−3

@@ -1826,7 +1826,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1826 do lhs <- updateLHS n wname mvars ns ns' (fullApp tm) w

1827 return $ PWith fc wname lhs ws wval withs'

1828 mkAux wname toplhs ns ns' c

1829− = ifail $ show fc ++ "badly formed with clause"

1829+ = ifail $ show fc ++ ":badly formed with clause"

1830

1831 addArg (PApp fc f args) w = PApp fc f (args ++ [pexp w])

1832 addArg (PRef fc f) w = PApp fc (PRef fc f) [pexp w]

@@ -1837,8 +1837,8 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1837 return $ substMatches mvars $

1838 PApp fc (PRef fc' wname)

1839 (map pexp ns ++ pexp w : (map pexp ns'))

1840− updateLHS n wname mvars ns ns' tm w

1840+ updateLHS n wname mvars ns_in ns_in' tm w

1841− = ifail $ "Not implemented match " ++ show tm

1841+ = updateLHS n wname mvars ns_in ns_in' (PApp fc tm []) w

1842

1843 keepMvar mvs fc v | v `elem` mvs = PRef fc v

1844 | otherwise = Placeholder

src/Idris/ParseHelpers.hs+1−1

@@ -316,7 +316,7 @@ operatorLetter = oneOf opChars

316-- | Parses an operator

317operator :: MonadicParsing m => m String

318operator = do op <- token . some $ operatorLetter

319− when (op `elem` [":", "=>", "->", "<-", "=", "?="]) $

319+ when (op `elem` [":", "=>", "->", "<-", "=", "?=", "|"]) $

320 fail $ op ++ " is not a valid operator"

321 return op

322