b74ad4e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Report names in accessibility check.

commitb74ad4e93502413c039235bcc07fb2c06238e91d authorMatus Tejiscak <ziman@functor.sk> dateWed 12 Feb 2014, 10:42 (13 years ago) parent6b86378

3 files changed+7−11

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+1−1 src/Idris/ElabDecls.hs+4−4 src/Idris/Erasure.hs+2−6

src/Idris/AbsSyntaxTree.hs+1−1

@@ -853,7 +853,7 @@ data OptInfo = Optimise { collapsible :: Bool,

853853 -- Let's store a list and convert it to IntMap whenever needed.

854854 forceable :: [(Int, Forceability)],

855855 recursive :: [Int],

856− inaccessible :: [Int] }

856+ inaccessible :: [(Int,Name)] } -- arg name for error reporting

857857 deriving Show

858858{-!

859859deriving instance Binary OptInfo

src/Idris/ElabDecls.hs+4−4

@@ -166,7 +166,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

166166 lst = txt "List"

167167 errrep = txt "ErrorReportPart"

168168

169− saveInaccArgs :: Name -> [Int] -> Idris ()

169+ saveInaccArgs :: Name -> [(Int,Name)] -> Idris ()

170170 saveInaccArgs n is = do

171171 ist <- getIState

172172 case lookupCtxt n (idris_optimisation ist) of

@@ -179,12 +179,12 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

179179 addDef n (Optimise False False [] [] is) (idris_optimisation ist) }

180180 addIBC (IBCOpt n)

181181

182− inaccessible :: Int -> PTerm -> [Int]

182+ inaccessible :: Int -> PTerm -> [(Int, Name)]

183183 inaccessible i (PPi (Imp _ _ _ _) n Placeholder t)

184− = i : inaccessible (i+1) t -- unbound implicit

184+ = (i,n) : inaccessible (i+1) t -- unbound implicit

185185 inaccessible i (PPi plicity n ty t)

186186 | InaccessibleArg `elem` pargopts plicity

187− = i : inaccessible (i+1) t -- an .{erased : Implicit}

187+ = (i,n) : inaccessible (i+1) t -- an .{erased : Implicit}

188188 | otherwise

189189 = inaccessible (i+1) t -- a {regular : Implicit}

190190 inaccessible _ _ = []

src/Idris/Erasure.hs+2−6

@@ -102,12 +102,8 @@ performUsageAnalysis = do

102102 checkAccessibility :: Ctxt OptInfo -> (Name, IntSet) -> Idris ()

103103 checkAccessibility opt (n, reachable)

104104 | [Optimise col nt forc rec inaccessible] <- lookupCtxt n opt

105− = let collision = IS.fromList inaccessible `IS.intersection` reachable

106− in unless (IS.null collision) . ifail . concat $

107− [ show n

108− , ": inaccessible arguments reachable: "

109− , intercalate ", " . map show $ IS.toList collision

110− ]

105+ , eargs@(_:_) <- [show n | (i,n) <- inaccessible, i `IS.member` reachable]

106+ = ifail $ show n ++ ": inaccessible arguments reachable: " ++ intercalate ", " eargs

111107

112108 | otherwise = return ()

113109