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

git.iko.soy/Idris-dev

Fix zero argument with clauses

Fixes #1245

commit8215c600eb42c8f99d175e596f10cc3dd7cf32bd authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 20 May 2014, 22:40 (12 years ago) parent9acf2c4

2 files changed+4−4

unifiedsplit

src/Idris/ElabDecls.hs+3−3

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

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

18271827 return $ PWith fc wname lhs ws wval withs'

18281828 mkAux wname toplhs ns ns' c

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

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

18301830

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

18321832 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)

18371837 return $ substMatches mvars $

18381838 PApp fc (PRef fc' wname)

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

1840− updateLHS n wname mvars ns ns' tm w

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

1840+ updateLHS n wname mvars ns_in ns_in' tm w

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

18421842

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

18441844 | otherwise = Placeholder

src/Idris/ParseHelpers.hs+1−1

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

316316-- | Parses an operator

317317operator :: MonadicParsing m => m String

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

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

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

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

321321 return op

322322