202c913 · Idris-dev · git.iko.soy

src/IRTS/Compiler.hs+5−5

@@ -60,7 +60,7 @@ compile codegen f mtm

6060 maindef <- case mtm of

6161 Nothing -> return []

6262 Just tm -> do md <- irMain tm

63− iLOG $ "MAIN: " ++ show md

63+ logLvl 1 $ "MAIN: " ++ show md

6464 return [(sMN 0 "runMain", md)]

6565 objs <- getObjectFiles codegen

6666 libs <- getLibs codegen

@@ -83,13 +83,13 @@ compile codegen f mtm

8383 let (nexttag, tagged) = addTags 65536 (liftAll defsUniq)

8484 let ctxtIn = addAlist tagged emptyContext

8585

86− iLOG "Defunctionalising"

86+ logLvl 1 "Defunctionalising"

8787 let defuns_in = defunctionalise nexttag ctxtIn

8888 logLvl 5 $ show defuns_in

89− iLOG "Inlining"

89+ logLvl 1 "Inlining"

9090 let defuns = inline defuns_in

9191 logLvl 5 $ show defuns

92− iLOG "Resolving variables for CG"

92+ logLvl 1 "Resolving variables for CG"

9393 -- iputStrLn $ showSep "\n" (map show (toAlist defuns))

9494 let checked = simplifyDefs defuns (toAlist defuns)

9595 outty <- outputTy

@@ -103,7 +103,7 @@ compile codegen f mtm

103103 Just f -> runIO $ writeFile f (dumpDefuns defuns)

104104 triple <- Idris.AbsSyntax.targetTriple

105105 cpu <- Idris.AbsSyntax.targetCPU

106− iLOG "Building output"

106+ logLvl 1 "Building output"

107107 case checked of

108108 OK c -> do return $ CodegenInfo f outty triple cpu

109109 hdrs impdirs objs libs flags

src/Idris/AbsSyntax.hs+7−10

@@ -345,7 +345,7 @@ addToCalledG :: Name -> [Name] -> Idris ()

345345addToCalledG n ns = return () -- TODO

346346

347347push_estack :: Name -> Bool -> Idris ()

348−push_estack n inst

348+push_estack n inst

349349 = do i <- getIState

350350 putIState (i { elab_stack = (n, inst) : elab_stack i })

351351

@@ -401,10 +401,10 @@ addAutoHint :: Name -> Name -> Idris ()

401401addAutoHint n hint =

402402 do ist <- getIState

403403 case lookupCtxtExact n (idris_autohints ist) of

404− Nothing ->

404+ Nothing ->

405405 do let hs = addDef n [hint] (idris_autohints ist)

406406 putIState $ ist { idris_autohints = hs }

407− Just nhints ->

407+ Just nhints ->

408408 do let hs = addDef n (hint : nhints) (idris_autohints ist)

409409 putIState $ ist { idris_autohints = hs }

410410

@@ -589,7 +589,7 @@ addConstraints fc (v, cs)

589589 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }

590590 where

591591 insertAll [] c = c

592− insertAll ((c, fc) : cs) ics

592+ insertAll ((c, fc) : cs) ics

593593 = insertAll cs $ S.insert (ConstraintFC c fc) ics

594594

595595addDeferred = addDeferred' Ref

@@ -946,9 +946,6 @@ cmdOptType :: Opt -> Idris Bool

946946cmdOptType x = do i <- getIState

947947 return $ x `elem` opt_cmdline (idris_options i)

948948

949−iLOG :: String -> Idris ()

950−iLOG = logLvl 1

951−

952949noErrors :: Idris Bool

953950noErrors = do i <- getIState

954951 case errSpan i of

@@ -1714,9 +1711,9 @@ aiFn inpat expat qq imp_meths ist fc f ffc ds as

17141711 insertImpl :: [PArg] -- ^ expected argument types (from idris_implicits)

17151712 -> [PArg] -- ^ given arguments

17161713 -> [PArg]

1717− insertImpl ps as

1714+ insertImpl ps as

17181715 = let (as', badimpls) = partition (impIn ps) as in

1719− map addUnknownImp badimpls ++

1716+ map addUnknownImp badimpls ++

17201717 insImpAcc M.empty ps (filter expArg as') (filter (not . expArg) as')

17211718

17221719 insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms

@@ -1761,7 +1758,7 @@ aiFn inpat expat qq imp_meths ist fc f ffc ds as

17611758 find n (PTacImplicit _ _ n' _ t : gs) acc

17621759 | n == n' = Just (t, reverse acc ++ gs)

17631760 find n (g : gs) acc = find n gs (g : acc)

1764−

1761+

17651762-- return True if the second argument is an implicit argument which is

17661763-- expected in the implicits, or if it's not an implicit

17671764impIn :: [PArg] -> PArg -> Bool

src/Idris/CaseSplit.hs+2−2

@@ -72,7 +72,7 @@ split n t'

7272 Nothing -> ifail $ show n ++ " is not a pattern variable"

7373 Just ty ->

7474 do let splits = findPats ist ty

75− iLOG ("New patterns " ++ showSep ", "

75+ logLvl 1 ("New patterns " ++ showSep ", "

7676 (map showTmImpls splits))

7777 let newPats_in = zipWith (replaceVar ctxt n) splits (repeat t)

7878 logLvl 4 ("Working from " ++ show t)

@@ -84,7 +84,7 @@ split n t'

8484 (showSep "\n" (map show (mapMaybe id newPats))))

8585 logLvl 3 "----"

8686 let newPats' = mergeAllPats ist n t (mapMaybe id newPats)

87− iLOG ("Name updates " ++ showSep "\n"

87+ logLvl 1 ("Name updates " ++ showSep "\n"

8888 (map (\ (p, u) -> show u ++ " " ++ show p) newPats'))

8989 return (map snd newPats')

9090

src/Idris/Chaser.hs+2−2

@@ -90,11 +90,11 @@ buildTree built fp = btree [] fp

9090 btree done f =

9191 do i <- getIState

9292 let file = extractFileName f

93− iLOG $ "CHASING " ++ show file

93+ logLvl 1 $ "CHASING " ++ show file

9494 ibcsd <- valIBCSubDir i

9595 ids <- allImportDirs

9696 fp <- findImport ids ibcsd file

97− iLOG $ "Found " ++ show fp

97+ logLvl 1 $ "Found " ++ show fp

9898 mt <- runIO $ getIModTime fp

9999 if (file `elem` built)

100100 then return [MTree fp False mt []]

src/Idris/Elab/Class.hs+2−2

@@ -174,7 +174,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

174174 let ds = map (decorateid defaultdec)

175175 [PTy emptyDocstring [] syn fc [] n nfc ty',

176176 PClauses fc (o ++ opts) n cs]

177− iLOG (show ds)

177+ logLvl 1 (show ds)

178178 return (n, ((defaultdec n, ds!!1), ds))

179179 _ -> ifail $ show n ++ " is not a method"

180180 defdecl _ _ _ = ifail "Can't happen (defdecl)"

@@ -231,7 +231,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

231231 let lhs = PApp fc (PRef fc m) (pconst capp : lhsArgs margs anames)

232232 let rhs = PApp fc (getMeth mnames all m) (rhsArgs margs anames)

233233 logLvl 2 ("Top level type: " ++ showTmImpls ty')

234− iLOG (show (m, ty', capp, margs))

234+ logLvl 1 (show (m, ty', capp, margs))

235235 logLvl 2 ("Definition: " ++ showTmImpls lhs ++ " = " ++ showTmImpls rhs)

236236 return [PTy doc [] syn fc o m mfc ty',

237237 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]

src/Idris/Elab/Clause.hs+1−1

@@ -650,7 +650,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

650650

651651 logLvl 5 "DONE CHECK"

652652 logLvl 4 $ "---> " ++ show rhs'

653− when (not (null defer)) $ iLOG $ "DEFERRED " ++

653+ when (not (null defer)) $ logLvl 1 $ "DEFERRED " ++

654654 show (map (\ (n, (_,_,t)) -> (n, t)) defer)

655655 def' <- checkDef fc (Elaborating "deferred type of ") defer

656656 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

src/Idris/Elab/Data.hs+2−2

@@ -53,7 +53,7 @@ import Util.Pretty(pretty, text)

5353elabData :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm)-> [(Name, Docstring (Either Err PTerm))] -> FC -> DataOpts -> PData -> Idris ()

5454elabData info syn doc argDocs fc opts (PLaterdecl n nfc t_in)

5555 = do let codata = Codata `elem` opts

56− iLOG (show (fc, doc))

56+ logLvl 1 (show (fc, doc))

5757 checkUndefined fc n

5858 (cty, _, t, inacc) <- buildType info syn fc [] n t_in

5959

@@ -63,7 +63,7 @@ elabData info syn doc argDocs fc opts (PLaterdecl n nfc t_in)

6363

6464elabData info syn doc argDocs fc opts (PDatadecl n nfc t_in dcons)

6565 = do let codata = Codata `elem` opts

66− iLOG (show fc)

66+ logLvl 1 (show fc)

6767 undef <- isUndefined fc n

6868 (cty, ckind, t, inacc) <- buildType info syn fc [] n t_in

6969 -- if n is defined already, make sure it is just a type declaration

src/Idris/Elab/Instance.hs+2−2

@@ -111,7 +111,7 @@ elabInstance info syn doc argDocs what fc cs n nfc ps t expn ds = do

111111 let ds_defs = insertDefaults i iname (class_defaults ci) ns ds

112112 logLvl 3 ("After defaults: " ++ show ds_defs ++ "\n")

113113 let ds' = reorderDefs (map fst (class_methods ci)) $ ds_defs

114− iLOG ("Reordered: " ++ show ds' ++ "\n")

114+ logLvl 1 ("Reordered: " ++ show ds' ++ "\n")

115115 mapM_ (warnMissing ds' ns iname) (map fst (class_methods ci))

116116 mapM_ (checkInClass (map fst (class_methods ci))) (concatMap defined ds')

117117 let wbTys = map mkTyDecl mtys

@@ -139,7 +139,7 @@ elabInstance info syn doc argDocs what fc cs n nfc ps t expn ds = do

139139

140140 let idecls = [PClauses fc [Dictionary] iname

141141 [PClause fc iname lhs [] rhs wb]]

142− iLOG (show idecls)

142+ logLvl 1 (show idecls)

143143 push_estack iname True

144144 mapM_ (rec_elabDecl info EAll info) idecls

145145 pop_estack

src/Idris/Elab/Record.hs+7−7

@@ -57,12 +57,12 @@ elabRecord info doc rsyn fc opts tyn nfc params paramDocs fields cname cdoc csyn

5757 logLvl 1 $ "Data constructor: " ++ showTmImpls dconTy

5858

5959 -- Build data declaration for elaboration

60− iLOG $ foldr (++) "" $ intersperse "\n" (map show dconsArgDocs)

60+ logLvl 1 $ foldr (++) "" $ intersperse "\n" (map show dconsArgDocs)

6161 let datadecl = PDatadecl tyn NoFC tycon [(cdoc, dconsArgDocs, dconName, NoFC, dconTy, fc, [])]

6262 elabData info rsyn doc paramDocs fc opts datadecl

6363

64− iLOG $ "fieldsWithName " ++ show fieldsWithName

65− iLOG $ "fieldsWIthNameAndDoc " ++ show fieldsWithNameAndDoc

64+ logLvl 1 $ "fieldsWithName " ++ show fieldsWithName

65+ logLvl 1 $ "fieldsWIthNameAndDoc " ++ show fieldsWithNameAndDoc

6666 elabRecordFunctions info rsyn fc tyn paramsAndDoc fieldsWithNameAndDoc dconName target

6767

6868 sendHighlighting $

@@ -154,8 +154,8 @@ elabRecordFunctions :: ElabInfo -> SyntaxInfo -> FC

154154elabRecordFunctions info rsyn fc tyn params fields dconName target

155155 = do logLvl 1 $ "Elaborating helper functions for record " ++ show tyn

156156

157− iLOG $ "Fields: " ++ show fieldNames

158− iLOG $ "Params: " ++ show paramNames

157+ logLvl 1 $ "Fields: " ++ show fieldNames

158+ logLvl 1 $ "Params: " ++ show paramNames

159159 -- The elaborated constructor type for the data declaration

160160 i <- getIState

161161 ttConsTy <-

@@ -165,8 +165,8 @@ elabRecordFunctions info rsyn fc tyn params fields dconName target

165165

166166 -- The arguments to the constructor

167167 let constructorArgs = getArgTys ttConsTy

168− iLOG $ "Cons args: " ++ show constructorArgs

169− iLOG $ "Free fields: " ++ show (filter (not . isFieldOrParam') constructorArgs)

168+ logLvl 1 $ "Cons args: " ++ show constructorArgs

169+ logLvl 1 $ "Free fields: " ++ show (filter (not . isFieldOrParam') constructorArgs)

170170 -- If elaborating the constructor has resulted in some new implicit fields we make projection functions for them.

171171 let freeFieldsForElab = map (freeField i) (filter (not . isFieldOrParam') constructorArgs)

172172

src/Idris/ElabDecls.hs+12−12

@@ -158,25 +158,25 @@ elabDecl' _ info (PSyntax _ p)

158158 = return () -- nothing to elaborate

159159elabDecl' what info (PTy doc argdocs s f o n nfc ty)

160160 | what /= EDefns

161− = do iLOG $ "Elaborating type decl " ++ show n ++ show o

161+ = do logLvl 1 $ "Elaborating type decl " ++ show n ++ show o

162162 elabType info s doc argdocs f o n nfc ty

163163 return ()

164164elabDecl' what info (PPostulate b doc s f o n ty)

165165 | what /= EDefns

166− = do iLOG $ "Elaborating postulate " ++ show n ++ show o

166+ = do logLvl 1 $ "Elaborating postulate " ++ show n ++ show o

167167 if b

168168 then elabExtern info s doc f o n ty

169169 else elabPostulate info s doc f o n ty

170170elabDecl' what info (PData doc argDocs s f co d)

171171 | what /= ETypes

172− = do iLOG $ "Elaborating " ++ show (d_name d)

172+ = do logLvl 1 $ "Elaborating " ++ show (d_name d)

173173 elabData info s doc argDocs f co d

174174 | otherwise

175− = do iLOG $ "Elaborating [type of] " ++ show (d_name d)

175+ = do logLvl 1 $ "Elaborating [type of] " ++ show (d_name d)

176176 elabData info s doc argDocs f co (PLaterdecl (d_name d) (d_name_fc d) (d_tcon d))

177177elabDecl' what info d@(PClauses f o n ps)

178178 | what /= ETypes

179− = do iLOG $ "Elaborating clause " ++ show n

179+ = do logLvl 1 $ "Elaborating clause " ++ show n

180180 i <- getIState -- get the type options too

181181 let o' = case lookupCtxt n (idris_flags i) of

182182 [fs] -> fs

@@ -190,7 +190,7 @@ elabDecl' what info (PMutual f ps)

190190 -- record mutually defined data definitions

191191 let datans = concatMap declared (filter isDataDecl ps)

192192 mapM_ (setMutData datans) datans

193− iLOG $ "Rechecking for positivity " ++ show datans

193+ logLvl 1 $ "Rechecking for positivity " ++ show datans

194194 mapM_ (\x -> do setTotality x Unchecked) datans

195195 -- Do totality checking after entire mutual block

196196 i <- get

@@ -215,7 +215,7 @@ elabDecl' what info (PMutual f ps)

215215

216216elabDecl' what info (PParams f ns ps)

217217 = do i <- getIState

218− iLOG $ "Expanding params block with " ++ show ns ++ " decls " ++

218+ logLvl 1 $ "Expanding params block with " ++ show ns ++ " decls " ++

219219 show (concatMap tldeclared ps)

220220 let nblock = pblock i

221221 mapM_ (elabDecl' what info) nblock

@@ -239,18 +239,18 @@ elabDecl' what info (PNamespace n nfc ps) =

239239

240240elabDecl' what info (PClass doc s f cs n nfc ps pdocs fds ds cn cd)

241241 | what /= EDefns

242− = do iLOG $ "Elaborating class " ++ show n

242+ = do logLvl 1 $ "Elaborating class " ++ show n

243243 elabClass info (s { syn_params = [] }) doc f cs n nfc ps pdocs fds ds cn cd

244244elabDecl' what info (PInstance doc argDocs s f cs n nfc ps t expn ds)

245− = do iLOG $ "Elaborating instance " ++ show n

245+ = do logLvl 1 $ "Elaborating instance " ++ show n

246246 elabInstance info s doc argDocs what f cs n nfc ps t expn ds

247247elabDecl' what info (PRecord doc rsyn fc opts name nfc ps pdocs fs cname cdoc csyn)

248248 | what /= ETypes

249− = do iLOG $ "Elaborating record " ++ show name

249+ = do logLvl 1 $ "Elaborating record " ++ show name

250250 elabRecord info doc rsyn fc opts name nfc ps pdocs fs cname cdoc csyn

251251{-

252252 | otherwise

253− = do iLOG $ "Elaborating [type of] " ++ show tyn

253+ = do logLvl 1 $ "Elaborating [type of] " ++ show tyn

254254 elabData info s doc [] f [] (PLaterdecl tyn ty)

255255-}

256256elabDecl' _ info (PDSL n dsl)

@@ -261,7 +261,7 @@ elabDecl' what info (PDirective i)

261261 | what /= EDefns = directiveAction i

262262elabDecl' what info (PProvider doc syn fc provWhat n)

263263 | what /= EDefns

264− = do iLOG $ "Elaborating type provider " ++ show n

264+ = do logLvl 1 $ "Elaborating type provider " ++ show n

265265 elabProvider doc info syn fc provWhat n

266266elabDecl' what info (PTransform fc safety old new)

267267 = do elabTransform info fc safety old new

src/Idris/IBC.hs+14−14

@@ -105,7 +105,7 @@ loadIBC reexport fp

105105 Nothing -> True

106106 Just p -> not p && reexport

107107 when redo $

108− do iLOG $ "Loading ibc " ++ fp ++ " " ++ show reexport

108+ do logLvl 1 $ "Loading ibc " ++ fp ++ " " ++ show reexport

109109 archiveFile <- runIO $ B.readFile fp

110110 case toArchiveOrFail archiveFile of

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

@@ -180,7 +180,7 @@ writeArchive fp i = do let a = L.foldl (\x y -> addEntryToArchive y x) emptyArch

180180

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

182182writeIBC src f

183− = do iLOG $ "Writing ibc " ++ show f

183+ = do logLvl 1 $ "Writing ibc " ++ show f

184184 i <- getIState

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

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

@@ -189,8 +189,8 @@ writeIBC src f

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

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

191191 writeArchive f ibcf

192− iLOG "Written")

193− (\c -> do iLOG $ "Failed " ++ pshow i c)

192+ logLvl 1 "Written")

193+ (\c -> do logLvl 1 $ "Failed " ++ pshow i c)

194194 return ()

195195

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

@@ -199,14 +199,14 @@ writePkgIndex :: FilePath -> Idris ()

199199writePkgIndex f

200200 = do i <- getIState

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

202− iLOG $ "Writing package index " ++ show f ++ " including\n" ++

202+ logLvl 1 $ "Writing package index " ++ show f ++ " including\n" ++

203203 show (map snd imps)

204204 resetNameIdx

205205 let ibcf = initIBC { ibc_imports = imps }

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

207207 writeArchive f ibcf

208− iLOG "Written")

209− (\c -> do iLOG $ "Failed " ++ pshow i c)

208+ logLvl 1 "Written")

209+ (\c -> do logLvl 1 $ "Failed " ++ pshow i c)

210210 return ()

211211

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

@@ -305,7 +305,7 @@ process :: Bool -- ^ Reexporting

305305process reexp i fn = do

306306 ver <- getEntry 0 "ver" i

307307 when (ver /= ibcVersion) $ do

308− iLOG "ibc out of date"

308+ logLvl 1 "ibc out of date"

309309 let e = if ver < ibcVersion

310310 then " an earlier " else " a later "

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

@@ -395,12 +395,12 @@ pImports fs

395395 ids <- allImportDirs

396396 fp <- findImport ids ibcsd f

397397-- if (f `elem` imported i)

398−-- then iLOG $ "Already read " ++ f

398+-- then logLvl 1 $ "Already read " ++ f

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

400400 case fp of

401− LIDR fn -> do iLOG $ "Failed at " ++ fn

401+ LIDR fn -> do logLvl 1 $ "Failed at " ++ fn

402402 ifail "Must be an ibc"

403− IDR fn -> do iLOG $ "Failed at " ++ fn

403+ IDR fn -> do logLvl 1 $ "Failed at " ++ fn

404404 ifail "Must be an ibc"

405405 IBC fn src -> loadIBC re fn)

406406 fs

@@ -491,13 +491,13 @@ pDefs reexp syms ds

491491 do d' <- updateDef d

492492 case d' of

493493 TyDecl _ _ -> return ()

494− _ -> do iLOG $ "SOLVING " ++ show n

494+ _ -> do logLvl 1 $ "SOLVING " ++ show n

495495 solveDeferred n

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

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

498− if (not reexp) then do iLOG $ "Not exporting " ++ show n

498+ if (not reexp) then do logLvl 1 $ "Not exporting " ++ show n

499499 setAccessibility n Hidden

500− else iLOG $ "Exporting " ++ show n) ds

500+ else logLvl 1 $ "Exporting " ++ show n) ds

501501 where

502502 updateDef (CaseOp c t args o s cd)

503503 = do o' <- mapM updateOrig o

src/Idris/Interactive.hs+1−1

@@ -35,7 +35,7 @@ caseSplitAt :: FilePath -> Bool -> Int -> Name -> Idris ()

3535caseSplitAt fn updatefile l n

3636 = do src <- runIO $ readSource fn

3737 res <- splitOnLine l n fn

38− iLOG (showSep "\n" (map show res))

38+ logLvl 1 (showSep "\n" (map show res))

3939 let (before, (ap : later)) = splitAt (l-1) (lines src)

4040 res' <- replaceSplits ap res

4141 let new = concat res'

src/Idris/Parser.hs+8−8

@@ -1362,7 +1362,7 @@ loadModule' f

13621362 ids <- allImportDirs

13631363 fp <- findImport ids ibcsd file

13641364 if file `elem` imported i

1365− then do iLOG $ "Already read " ++ file

1365+ then do logLvl 1 $ "Already read " ++ file

13661366 return Nothing

13671367 else do putIState (i { imported = file : imported i })

13681368 case fp of

@@ -1370,7 +1370,7 @@ loadModule' f

13701370 LIDR fn -> loadSource True fn Nothing

13711371 IBC fn src ->

13721372 idrisCatch (loadIBC True fn)

1373− (\c -> do iLOG $ fn ++ " failed " ++ pshow i c

1373+ (\c -> do logLvl 1 $ fn ++ " failed " ++ pshow i c

13741374 case src of

13751375 IDR sfn -> loadSource False sfn Nothing

13761376 LIDR sfn -> loadSource True sfn Nothing)

@@ -1379,7 +1379,7 @@ loadModule' f

13791379{- | Load idris code from file -}

13801380loadFromIFile :: Bool -> IFileType -> Maybe Int -> Idris ()

13811381loadFromIFile reexp i@(IBC fn src) maxline

1382− = do iLOG $ "Skipping " ++ getSrcFile i

1382+ = do logLvl 1 $ "Skipping " ++ getSrcFile i

13831383 idrisCatch (loadIBC reexp fn)

13841384 (\err -> ierror $ LoadingFailed fn err)

13851385 where

@@ -1403,7 +1403,7 @@ loadSource' lidr r maxline

14031403{- | Load Idris source code-}

14041404loadSource :: Bool -> FilePath -> Maybe Int -> Idris ()

14051405loadSource lidr f toline

1406− = do iLOG ("Reading " ++ f)

1406+ = do logLvl 1 ("Reading " ++ f)

14071407 i <- getIState

14081408 let def_total = default_total i

14091409 file_in <- runIO $ readSource f

@@ -1505,14 +1505,14 @@ loadSource lidr f toline

15051505 setContext ctxt')

15061506 (map snd (idris_totcheck i))

15071507 -- build size change graph from simplified definitions

1508− iLOG "Totality checking"

1508+ logLvl 1 "Totality checking"

15091509 i <- getIState

15101510 mapM_ buildSCG (idris_totcheck i)

15111511 mapM_ checkDeclTotality (idris_totcheck i)

15121512

15131513 -- Redo totality check for deferred names

15141514 let deftots = idris_defertotcheck i

1515− iLOG $ "Totality checking " ++ show deftots

1515+ logLvl 1 $ "Totality checking " ++ show deftots

15161516 mapM_ (\x -> do tot <- getTotality x

15171517 case tot of

15181518 Total _ -> setTotality x Unchecked

@@ -1520,9 +1520,9 @@ loadSource lidr f toline

15201520 mapM_ buildSCG deftots

15211521 mapM_ checkDeclTotality deftots

15221522

1523− iLOG ("Finished " ++ f)

1523+ logLvl 1 ("Finished " ++ f)

15241524 ibcsd <- valIBCSubDir i

1525− iLOG "Universe checking"

1525+ logLvl 1 "Universe checking"

15261526 iucheck

15271527 let ibc = ibcPathNoFallback ibcsd f

15281528 i <- getIState

src/Idris/Prover.hs+1−1

@@ -90,7 +90,7 @@ prove mode opt ctxt lit n ty

9090 if mode

9191 then elabloop n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) [] Nothing []

9292 else ploop n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) Nothing

93− iLOG $ "Adding " ++ show tm

93+ logLvl 1 $ "Adding " ++ show tm

9494 i <- getIState

9595 let shower = if mode

9696 then showRunElab

src/Idris/REPL.hs+4−4

@@ -1205,7 +1205,7 @@ process fn (DynamicLink l)

12051205 Nothing -> iPrintError $ "Could not load dynamic lib \"" ++ l ++ "\""

12061206 Just x -> do let libs = idris_dynamic_libs i

12071207 if x `elem` libs

1208− then do iLOG ("Tried to load duplicate library " ++ lib_name x)

1208+ then do logLvl 1 ("Tried to load duplicate library " ++ lib_name x)

12091209 return ()

12101210 else putIState $ i { idris_dynamic_libs = x:libs }

12111211 where trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace

@@ -1476,8 +1476,8 @@ loadInputs inputs toline -- furthest line to read in input source files

14761476 (map snd (take (num-1) ninputs))

14771477 input

14781478 let ifiles = getModuleFiles modTree

1479− iLOG ("MODULE TREE : " ++ show modTree)

1480− iLOG ("RELOAD: " ++ show ifiles)

1479+ logLvl 1 ("MODULE TREE : " ++ show modTree)

1480+ logLvl 1 ("RELOAD: " ++ show ifiles)

14811481 when (not (all ibc ifiles) || loadCode) $

14821482 tryLoad False (filter (not . ibc) ifiles)

14831483 -- return the files that need rechecking

@@ -1696,7 +1696,7 @@ idrisMain opts =

16961696 -- Create Idris data dir + repl history and config dir

16971697 idrisCatch (do dir <- getIdrisUserDataDir

16981698 exists <- runIO $ doesDirectoryExist dir

1699− unless exists $ iLOG ("Creating " ++ dir)

1699+ unless exists $ logLvl 1 ("Creating " ++ dir)

17001700 runIO $ createDirectoryIfMissing True (dir </> "repl"))

17011701 (\e -> return ())

17021702