6dc5ea2 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix name shadowing in where

commit6dc5ea2f4cef0dedc758498ff5ad241f57217f69 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 27 Aug 2013, 13:15 (13 years ago) parent0aca9f2

4 files changed+13−5

compare with master

unifiedsplit

CHANGELOG+4 src/Idris/AbsSyntax.hs+3−3 src/Idris/Chaser.hs+4−1 src/Idris/REPL.hs+2−1

CHANGELOG+4

@@ -7,6 +7,10 @@ New in 0.9.10:

77 in the scope e

88* At the REPL, "it" now refers to the previous expression

10+Internal changes

11+

12+* New module/dependency tree checking

13+

1014New in 0.9.9:

1115-------------

1216

src/Idris/AbsSyntax.hs+3−3

@@ -609,17 +609,17 @@ expandParams dec ps ns infs tm = en tm

609609 mkShadow (NS x s) = NS (mkShadow x) s

610610

611611 en (PLam n t s)

612− | n `elem` map fst ps

612+ | n `elem` (map fst ps ++ ns)

613613 = let n' = mkShadow n in

614614 PLam n' (en t) (en (shadow n n' s))

615615 | otherwise = PLam n (en t) (en s)

616616 en (PPi p n t s)

617− | n `elem` map fst ps

617+ | n `elem` (map fst ps ++ ns)

618618 = let n' = mkShadow n in

619619 PPi p n' (en t) (en (shadow n n' s))

620620 | otherwise = PPi p n (en t) (en s)

621621 en (PLet n ty v s)

622− | n `elem` map fst ps

622+ | n `elem` (map fst ps ++ ns)

623623 = let n' = mkShadow n in

624624 PLet n' (en ty) (en v) (en (shadow n n' s))

625625 | otherwise = PLet n (en ty) (en v) (en s)

src/Idris/Chaser.hs+4−1

@@ -70,7 +70,10 @@ getIModTime (LIDR i) = getModificationTime i

7070

7171buildTree :: [FilePath] -> -- already guaranteed built

7272 FilePath -> Idris [ModuleTree]

73−buildTree built fp = btree [] fp where

73+buildTree built fp = idrisCatch (btree [] fp)

74+ (\e -> do now <- liftIO $ getCurrentTime

75+ return [MTree (IDR fp) True now []])

76+ where

7477 btree done f =

7578 do i <- getIState

7679 let file = takeWhile (/= ' ') f

src/Idris/REPL.hs+2−1

@@ -672,7 +672,8 @@ loadInputs inputs

672672 iLOG ("MODULE TREE : " ++ show modTree)

673673 iLOG ("RELOAD: " ++ show ifiles)

674674 when (not (all ibc ifiles) || loadCode) $ tryLoad ifiles

675− return ifiles)

675+ -- return the files that need rechecking

676+ return (if (all ibc ifiles) then ifiles else []))

676677 ninputs

677678 inew <- getIState

678679 -- to check everything worked consistently (in particular, will catch