git.iko.soy/Idris-dev
on master help sign in
Fix name shadowing in where
6dc5ea2Edwin Brady
CHANGELOG+4
compare with master
unifiedsplit
@@ -7,6 +7,10 @@ New in 0.9.10:
7 in the scope e
7 in the scope e
8* At the REPL, "it" now refers to the previous expression
8* At the REPL, "it" now refers to the previous expression
9
9
10+Internal changes
11+
12+* New module/dependency tree checking
13+
10New in 0.9.9:
14New in 0.9.9:
11-------------
15-------------
12
16
src/Idris/AbsSyntax.hs+3−3
@@ -609,17 +609,17 @@ expandParams dec ps ns infs tm = en tm
609 mkShadow (NS x s) = NS (mkShadow x) s
609 mkShadow (NS x s) = NS (mkShadow x) s
610
610
611 en (PLam n t s)
611 en (PLam n t s)
612− | n `elem` map fst ps
612+ | n `elem` (map fst ps ++ ns)
613 = let n' = mkShadow n in
613 = let n' = mkShadow n in
614 PLam n' (en t) (en (shadow n n' s))
614 PLam n' (en t) (en (shadow n n' s))
615 | otherwise = PLam n (en t) (en s)
615 | otherwise = PLam n (en t) (en s)
616 en (PPi p n t s)
616 en (PPi p n t s)
617− | n `elem` map fst ps
617+ | n `elem` (map fst ps ++ ns)
618 = let n' = mkShadow n in
618 = let n' = mkShadow n in
619 PPi p n' (en t) (en (shadow n n' s))
619 PPi p n' (en t) (en (shadow n n' s))
620 | otherwise = PPi p n (en t) (en s)
620 | otherwise = PPi p n (en t) (en s)
621 en (PLet n ty v s)
621 en (PLet n ty v s)
622− | n `elem` map fst ps
622+ | n `elem` (map fst ps ++ ns)
623 = let n' = mkShadow n in
623 = let n' = mkShadow n in
624 PLet n' (en ty) (en v) (en (shadow n n' s))
624 PLet n' (en ty) (en v) (en (shadow n n' s))
625 | otherwise = PLet n (en ty) (en v) (en s)
625 | otherwise = PLet n (en ty) (en v) (en s)
src/Idris/Chaser.hs+4−1
@@ -70,7 +70,10 @@ getIModTime (LIDR i) = getModificationTime i
70
70
71buildTree :: [FilePath] -> -- already guaranteed built
71buildTree :: [FilePath] -> -- already guaranteed built
72 FilePath -> Idris [ModuleTree]
72 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
74 btree done f =
77 btree done f =
75 do i <- getIState
78 do i <- getIState
76 let file = takeWhile (/= ' ') f
79 let file = takeWhile (/= ' ') f
src/Idris/REPL.hs+2−1
@@ -672,7 +672,8 @@ loadInputs inputs
672 iLOG ("MODULE TREE : " ++ show modTree)
672 iLOG ("MODULE TREE : " ++ show modTree)
673 iLOG ("RELOAD: " ++ show ifiles)
673 iLOG ("RELOAD: " ++ show ifiles)
674 when (not (all ibc ifiles) || loadCode) $ tryLoad ifiles
674 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 []))
676 ninputs
677 ninputs
677 inew <- getIState
678 inew <- getIState
678 -- to check everything worked consistently (in particular, will catch
679 -- to check everything worked consistently (in particular, will catch