5f3e700 · Idris-dev · git.iko.soy

113 Nothing -> True

114 Just p -> not p && reexport

115 when redo $

116− do logCodeGen 1 $ "Loading ibc " ++ fp ++ " " ++ show reexport

116+ do logIBC 1 $ "Loading ibc " ++ fp ++ " " ++ show reexport

117 archiveFile <- runIO $ B.readFile fp

118 case toArchiveOrFail archiveFile of

119 Left _ -> ifail $ fp ++ " isn't loadable, it may have an old ibc format.\n"

189

190writeIBC :: FilePath -> FilePath -> Idris ()

191writeIBC src f

192− = do logCodeGen 1 $ "Writing ibc " ++ show f

192+ = do logIBC 1 $ "Writing ibc " ++ show f

193 i <- getIState

194-- case (Data.List.map fst (idris_metavars i)) \\ primDefs of

195-- (_:_) -> ifail "Can't write ibc when there are unsolved metavariables"

198 ibcf <- mkIBC (ibc_write i) (initIBC { sourcefile = src })

199 idrisCatch (do runIO $ createDirectoryIfMissing True (dropFileName f)

200 writeArchive f ibcf

201− logCodeGen 1 "Written")

201+ logIBC 1 "Written")

202− (\c -> do logCodeGen 1 $ "Failed " ++ pshow i c)

202+ (\c -> do logIBC 1 $ "Failed " ++ pshow i c)

203 return ()

204

205-- Write a package index containing all the imports in the current IState

208writePkgIndex f

209 = do i <- getIState

210 let imps = map (\ (x, y) -> (True, x)) $ idris_imported i

211− logCodeGen 1 $ "Writing package index " ++ show f ++ " including\n" ++

211+ logIBC 1 $ "Writing package index " ++ show f ++ " including\n" ++

212 show (map snd imps)

213 resetNameIdx

214 let ibcf = initIBC { ibc_imports = imps }

215 idrisCatch (do runIO $ createDirectoryIfMissing True (dropFileName f)

216 writeArchive f ibcf

217− logCodeGen 1 "Written")

217+ logIBC 1 "Written")

218− (\c -> do logCodeGen 1 $ "Failed " ++ pshow i c)

218+ (\c -> do logIBC 1 $ "Failed " ++ pshow i c)

219 return ()

220

221mkIBC :: [IBCWrite] -> IBCFile -> Idris IBCFile

222mkIBC [] f = return f

223mkIBC (i:is) f = do ist <- getIState

224− logCodeGen 5 $ show i ++ " " ++ show (L.length is)

224+ logIBC 5 $ show i ++ " " ++ show (L.length is)

225 f' <- ibc ist i f

226 mkIBC is f'

227

319process reexp i fn = do

320 ver <- getEntry 0 "ver" i

321 when (ver /= ibcVersion) $ do

322− logCodeGen 1 "ibc out of date"

322+ logIBC 1 "ibc out of date"

323 let e = if ver < ibcVersion

324 then " an earlier " else " a later "

325 ifail $ "Incompatible ibc version.\nThis library was built with"

416 putIState (i { imported = f : imported i })

417 case fp of

418 LIDR fn -> do

419− logCodeGen 1 $ "Failed at " ++ fn

419+ logIBC 1 $ "Failed at " ++ fn

420 ifail "Must be an ibc"

421 IDR fn -> do

422− logCodeGen 1 $ "Failed at " ++ fn

422+ logIBC 1 $ "Failed at " ++ fn

423 ifail "Must be an ibc"

424 IBC fn src -> loadIBC (reexp && re) fn)

425 fs

517 do d' <- updateDef d

518 case d' of

519 TyDecl _ _ -> return ()

520− _ -> do logCodeGen 1 $ "SOLVING " ++ show n

520+ _ -> do logIBC 1 $ "SOLVING " ++ show n

521 solveDeferred n

522 updateIState (\i -> i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })

523-- logLvl 1 $ "Added " ++ show (n, d')

524− if (not reexp) then do logCodeGen 1 $ "Not exporting " ++ show n

524+ if (not reexp) then do logIBC 1 $ "Not exporting " ++ show n

525 setAccessibility n Hidden

526− else logCodeGen 1 $ "Exporting " ++ show n) ds

526+ else logIBC 1 $ "Exporting " ++ show n) ds

527 where

528 updateDef (CaseOp c t args o s cd)

529 = do o' <- mapM updateOrig o

588pAccess reexp ds

589 = mapM_ (\ (n, a_in) ->

590 do let a = if reexp then a_in else Hidden

591− logCodeGen 3 $ "Setting " ++ show (a, n) ++ " to " ++ show a

591+ logIBC 3 $ "Setting " ++ show (a, n) ++ " to " ++ show a

592 updateIState (\i -> i { tt_ctxt = setAccess n a (tt_ctxt i) })) ds

593

594pFlags :: [(Name, [FnOpt])] -> Idris ()