f3fef7e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Precise tracking of bindings in do blocks

commitf3fef7ec3dd7e87f19e15be21a7e68eb1b956791 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateMon 11 May 2015, 15:57 (11 years ago) parent56b6850

8 files changed+21−19

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+3−3 src/Idris/DSL.hs+2−2 src/Idris/DeepSeq.hs+1−1 src/Idris/ElabQuasiquote.hs+2−2 src/Idris/Error.hs+1−1 src/Idris/IBC.hs+7−5 src/Idris/IdrisDoc.hs+1−1 src/Idris/ParseExpr.hs+4−4

src/Idris/AbsSyntaxTree.hs+3−3

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

957957type PTactic = PTactic' PTerm

958958

959959data PDo' t = DoExp FC t

960− | DoBind FC Name t

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

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

962962 | DoLet FC Name t t

963963 | DoLetP FC t t

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

969969

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

971971 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

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

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

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

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

10591059 (fc:_) -> Just fc

10601060 where

10611061 getDoFC (DoExp fc t) = fc

1062− getDoFC (DoBind fc nm t) = fc

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

10631063 getDoFC (DoBindP fc l r alts) = fc

10641064 getDoFC (DoLet fc nm l r) = fc

10651065 getDoFC (DoLetP fc l r) = fc

src/Idris/DSL.hs+2−2

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

9797 where

9898 block b [DoExp fc tm] = tm

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

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

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

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

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

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

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

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

src/Idris/DeepSeq.hs+1−1

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

316316

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

318318 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` ()

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

321321 rnf (DoLet x1 x2 x3 x4)

322322 = 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)])

5858extractDoUnquotes d (DoExp fc tm)

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

6060 return (DoExp fc tm', ex)

61−extractDoUnquotes d (DoBind fc n tm)

61+extractDoUnquotes d (DoBind fc n nfc tm)

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

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

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

6464extractDoUnquotes d (DoBindP fc t t' alts)

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

6666extractDoUnquotes d (DoLet fc n v b)

src/Idris/Error.hs+1−1

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

121121warnDisamb ist Placeholder = return ()

122122warnDisamb ist (PDoBlock steps) = mapM_ wStep steps

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

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

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

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

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

127127 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

19591959 DoExp x1 x2 -> do putWord8 0

19601960 put x1

19611961 put x2

1962− DoBind x1 x2 x3 -> do putWord8 1

1963− put x1

1964− put x2

1965− put x3

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

1963+ put x1

1964+ put x2

1965+ put x3

1966+ put x4

19661967 DoBindP x1 x2 x3 x4 -> do putWord8 2

19671968 put x1

19681969 put x2

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

19861987 1 -> do x1 <- get

19871988 x2 <- get

19881989 x3 <- get

1989− return (DoBind x1 x2 x3)

1990+ x4 <- get

1991+ return (DoBind x1 x2 x3 x4)

19901992 2 -> do x1 <- get

19911993 x2 <- get

19921994 x3 <- get

src/Idris/IdrisDoc.hs+1−1

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

341341-- | Helper function for extractPTermNames

342342extractPDo :: PDo -> [Name]

343343extractPDo (DoExp _ p) = extract p

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

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

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

346346 ps' = ps1 ++ ps2

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

src/Idris/ParseExpr.hs+4−4

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

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

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

190190 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

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

193193 : upd (dropn n ns) ds

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

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

11551155 fc <- getFC

11561156 sc <- expr syn

11571157 return (DoLetP fc i sc))

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

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

11591159 symbol "<-"

11601160 fc <- getFC

11611161 e <- expr syn;

1162− option (DoBind fc i e)

1162+ option (DoBind fc i ifc e)

11631163 (do lchar '|'

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

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

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

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

11671167 symbol "<-"

11681168 fc <- getFC