f3fef7e · Idris-dev · git.iko.soy

src/Idris/AbsSyntaxTree.hs+3−3

compare with master

unifiedsplit

@@ -957,7 +957,7 @@ instance Sized a => Sized (PTactic' a) where

957type PTactic = PTactic' PTerm

958

959data PDo' t = DoExp FC t

960− | DoBind FC Name t

960+ | DoBind FC Name FC t -- ^ second FC is precise name location

961 | DoBindP FC t t [(t,t)]

962 | DoLet FC Name t t

963 | DoLetP FC t t

@@ -969,7 +969,7 @@ deriving instance NFData PDo'

969

970instance Sized a => Sized (PDo' a) where

971 size (DoExp fc t) = 1 + size fc + size t

972− size (DoBind fc nm t) = 1 + size fc + size nm + size t

972+ size (DoBind fc nm nfc t) = 1 + size fc + size nm + size nfc + size t

973 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts

974 size (DoLet fc nm l r) = 1 + size fc + size nm + size l + size r

975 size (DoLetP fc l r) = 1 + size fc + size l + size r

@@ -1059,7 +1059,7 @@ highestFC (PDoBlock lines) =

1059 (fc:_) -> Just fc

1060 where

1061 getDoFC (DoExp fc t) = fc

1062− getDoFC (DoBind fc nm t) = fc

1062+ getDoFC (DoBind fc nm nfc t) = fc

1063 getDoFC (DoBindP fc l r alts) = fc

1064 getDoFC (DoLet fc nm l r) = fc

1065 getDoFC (DoLetP fc l r) = fc

src/Idris/DSL.hs+2−2

@@ -97,8 +97,8 @@ expandSugar dsl (PDoBlock ds)

97 where

98 block b [DoExp fc tm] = tm

99 block b [a] = PElabError (Msg "Last statement in do block must be an expression")

100− block b (DoBind fc n tm : rest)

100+ block b (DoBind fc n nfc tm : rest)

101− = PApp fc b [pexp tm, pexp (PLam fc n NoFC Placeholder (block b rest))]

101+ = PApp fc b [pexp tm, pexp (PLam fc n nfc Placeholder (block b rest))]

102 block b (DoBindP fc p tm alts : rest)

103 = PApp fc b [pexp tm, pexp (PLam fc (sMN 0 "bpat") NoFC Placeholder

104 (PCase fc (PRef fc (sMN 0 "bpat"))

src/Idris/DeepSeq.hs+1−1

@@ -316,7 +316,7 @@ instance NFData ErrorReportPart where

316

317instance (NFData t) => NFData (PDo' t) where

318 rnf (DoExp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

319− rnf (DoBind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

319+ rnf (DoBind x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

320 rnf (DoBindP x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

321 rnf (DoLet x1 x2 x3 x4)

322 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

src/Idris/ElabQuasiquote.hs+2−2

@@ -58,9 +58,9 @@ extractDoUnquotes :: Int -> PDo -> Elab' aux (PDo, [(Name, PTerm)])

58extractDoUnquotes d (DoExp fc tm)

59 = do (tm', ex) <- extractUnquotes d tm

60 return (DoExp fc tm', ex)

61−extractDoUnquotes d (DoBind fc n tm)

61+extractDoUnquotes d (DoBind fc n nfc tm)

62 = do (tm', ex) <- extractUnquotes d tm

63− return (DoBind fc n tm', ex)

63+ return (DoBind fc n nfc tm', ex)

64extractDoUnquotes d (DoBindP fc t t' alts)

65 = fail "Pattern-matching binds cannot be quasiquoted"

66extractDoUnquotes d (DoLet fc n v b)

src/Idris/Error.hs+1−1

@@ -121,7 +121,7 @@ warnDisamb ist (PConstant _ _) = return ()

121warnDisamb ist Placeholder = return ()

122warnDisamb ist (PDoBlock steps) = mapM_ wStep steps

123 where wStep (DoExp _ x) = warnDisamb ist x

124− wStep (DoBind _ _ x) = warnDisamb ist x

124+ wStep (DoBind _ _ _ x) = warnDisamb ist x

125 wStep (DoBindP _ x y cs) = warnDisamb ist x >> warnDisamb ist y >>

126 mapM_ (\(x,y) -> warnDisamb ist x >> warnDisamb ist y) cs

127 wStep (DoLet _ _ x y) = warnDisamb ist x >> warnDisamb ist y

src/Idris/IBC.hs+7−5

@@ -1959,10 +1959,11 @@ instance (Binary t) => Binary (PDo' t) where

1959 DoExp x1 x2 -> do putWord8 0

1960 put x1

1961 put x2

1962− DoBind x1 x2 x3 -> do putWord8 1

1962+ DoBind x1 x2 x3 x4 -> do putWord8 1

1963− put x1

1963+ put x1

1964− put x2

1964+ put x2

1965− put x3

1965+ put x3

1966+ put x4

1966 DoBindP x1 x2 x3 x4 -> do putWord8 2

1967 DoBindP x1 x2 x3 x4 -> do putWord8 2

1967 put x1

1968 put x1

1968 put x2

1969 put x2

@@ -1986,7 +1987,8 @@ instance (Binary t) => Binary (PDo' t) where

1986 1 -> do x1 <- get

1987 1 -> do x1 <- get

1987 x2 <- get

1988 x2 <- get

1988 x3 <- get

1989 x3 <- get

1990+ x4 <- get

1989− return (DoBind x1 x2 x3)

1991+ return (DoBind x1 x2 x3 x4)

1990 2 -> do x1 <- get

1992 2 -> do x1 <- get

1991 x2 <- get

1993 x2 <- get

1992 x3 <- get

1994 x3 <- get

src/Idris/IdrisDoc.hs+1−1

@@ -341,7 +341,7 @@ extractPArg (PTacImplicit {pname=n, getScript=p1, getTm=p2})

341-- | Helper function for extractPTermNames

342extractPDo :: PDo -> [Name]

343extractPDo (DoExp _ p) = extract p

344−extractPDo (DoBind _ n p) = n : extract p

344+extractPDo (DoBind _ n _ p) = n : extract p

345extractPDo (DoBindP _ p1 p2 ps) = let (ps1, ps2) = unzip ps

346 ps' = ps1 ++ ps2

347 in concatMap extract (p1 : p2 : ps')

src/Idris/ParseExpr.hs+4−4

@@ -188,7 +188,7 @@ extension syn ns rules =

188 update ns (PDoBlock ds) = PDoBlock $ upd ns ds

189 where upd :: [(Name, SynMatch)] -> [PDo] -> [PDo]

190 upd ns (DoExp fc t : ds) = DoExp fc (update ns t) : upd ns ds

191− upd ns (DoBind fc n t : ds) = DoBind fc n (update ns t) : upd (dropn n ns) ds

191+ upd ns (DoBind fc n nfc t : ds) = DoBind fc n nfc (update ns t) : upd (dropn n ns) ds

192 upd ns (DoLet fc n ty t : ds) = DoLet fc n (update ns ty) (update ns t)

193 : upd (dropn n ns) ds

194 upd ns (DoBindP fc i t ts : ds)

@@ -1155,14 +1155,14 @@ do_ syn

1155 fc <- getFC

1156 sc <- expr syn

1157 return (DoLetP fc i sc))

1158− <|> try (do i <- fst <$> name

1158+ <|> try (do (i, ifc) <- name

1159 symbol "<-"

1160 fc <- getFC

1161 e <- expr syn;

1162− option (DoBind fc i e)

1162+ option (DoBind fc i ifc e)

1163 (do lchar '|'

1164 ts <- sepBy1 (do_alt syn) (lchar '|')

1165− return (DoBindP fc (PRef fc i) e ts)))

1165+ return (DoBindP fc (PRef ifc i) e ts)))

1166 <|> try (do i <- expr' syn

1167 symbol "<-"

1168 fc <- getFC