7875005 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Change treatment of underscore in lambda

Treat as unnamed variables, rather than as patterns

commit78750058830660b9503bda4468341a1d970205f5 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 1 Aug 2013, 11:45 (13 years ago) parent55dbed5

3 files changed+9−1

unifiedsplit

src/Core/TT.hs+1

@@ -210,6 +210,7 @@ instance Pretty Name where

210210instance Show Name where

211211 show (UN n) = n

212212 show (NS n s) = showSep "." (reverse s) ++ "." ++ show n

213+ show (MN _ "underscore") = "_"

213214 show (MN i s) = "{" ++ s ++ show i ++ "}"

214215 show NErased = "_"

215216

src/Idris/ElabDecls.hs+4

@@ -675,6 +675,10 @@ elabVal info aspat tm_in

675675-- (build i info aspat (MN 0 "val") tm))

676676 tclift (elaborate ctxt (MN 0 "val") infP []

677677 (build i info aspat (MN 0 "val") (infTerm tm)))

678+ def' <- checkDef (FC "(input)" 0) defer

679+ addDeferred def'

680+ mapM_ (elabCaseBlock info) is

681+

678682 logLvl 3 ("Value: " ++ show tm')

679683 recheckC (FC "(input)" 0) [] tm'

680684 let vtm = getInferTerm tm'

src/Idris/Parser.hs+4−1

@@ -1077,11 +1077,14 @@ tyDeclList syn = try (sepBy1 (do x <- pfName

10771077 t <- pTSig (noImp syn)

10781078 return (map (\x -> (x, t)) ns)

10791079

1080−tyOptDeclList syn = sepBy1 (do x <- pfName;

1080+tyOptDeclList syn = sepBy1 (do x <- pNameOrPlaceholder

10811081 t <- option Placeholder (do lchar ':'

10821082 pExpr syn)

10831083 return (x,t))

10841084 (lchar ',')

1085+ where pNameOrPlaceholder = pfName

1086+ <|> do symbol "_"

1087+ return (MN 0 "underscore")

10851088

10861089bindList b [] sc = sc

10871090bindList b ((n, t):bs) sc = b n t (bindList b bs sc)