b74ad4e · Idris-dev · git.iko.soy

src/Idris/AbsSyntaxTree.hs+1−1

compare with master

unifiedsplit

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

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

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

855 recursive :: [Int],

856− inaccessible :: [Int] }

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

857 deriving Show

858{-!

859deriving 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

166 lst = txt "List"

167 errrep = txt "ErrorReportPart"

168

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

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

170 saveInaccArgs n is = do

171 ist <- getIState

172 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

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

180 addIBC (IBCOpt n)

181

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

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

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

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

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

185 inaccessible i (PPi plicity n ty t)

186 | InaccessibleArg `elem` pargopts plicity

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

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

188 | otherwise

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

190 inaccessible _ _ = []

src/Idris/Erasure.hs+2−6

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

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

103 checkAccessibility opt (n, reachable)

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

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

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

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

107− [ show n

108− , ": inaccessible arguments reachable: "

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

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

110− ]

111

107

112 | otherwise = return ()

108 | otherwise = return ()

113

109