ecab241 · Idris-dev · git.iko.soy

src/IRTS/Compiler.hs+5−5

compare with master

unifiedsplit

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

60 maindef <- case mtm of

61 Nothing -> return []

62 Just tm -> do md <- irMain tm

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

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

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

65 objs <- getObjectFiles codegen

66 libs <- getLibs codegen

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

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

84 let ctxtIn = addAlist tagged emptyContext

85

86− iLOG "Defunctionalising"

86+ logLvl 1 "Defunctionalising"

87 let defuns_in = defunctionalise nexttag ctxtIn

88 logLvl 5 $ show defuns_in

89− iLOG "Inlining"

89+ logLvl 1 "Inlining"

90 let defuns = inline defuns_in

91 logLvl 5 $ show defuns

92− iLOG "Resolving variables for CG"

92+ logLvl 1 "Resolving variables for CG"

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

94 let checked = simplifyDefs defuns (toAlist defuns)

95 outty <- outputTy

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

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

104 triple <- Idris.AbsSyntax.targetTriple

105 cpu <- Idris.AbsSyntax.targetCPU

106− iLOG "Building output"

106+ logLvl 1 "Building output"

107 case checked of

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

109 hdrs impdirs objs libs flags

src/Idris/AbsSyntax.hs+7−10

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

345addToCalledG n ns = return () -- TODO

346

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

348−push_estack n inst

348+push_estack n inst

349 = do i <- getIState

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

351

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

401addAutoHint n hint =

402 do ist <- getIState

403 case lookupCtxtExact n (idris_autohints ist) of

404− Nothing ->

404+ Nothing ->

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

406 putIState $ ist { idris_autohints = hs }

407− Just nhints ->

407+ Just nhints ->

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

409 putIState $ ist { idris_autohints = hs }

410

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

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

590 where

591 insertAll [] c = c

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

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

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

594

595addDeferred = addDeferred' Ref

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

946cmdOptType x = do i <- getIState

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

948

949−iLOG :: String -> Idris ()

950−iLOG = logLvl 1

951−

952noErrors :: Idris Bool

949noErrors :: Idris Bool

953noErrors = do i <- getIState

950noErrors = do i <- getIState

954 case errSpan i of

951 case errSpan i of

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

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

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

1715 -> [PArg] -- ^ given arguments

1712 -> [PArg] -- ^ given arguments

1716 -> [PArg]

1713 -> [PArg]

1717− insertImpl ps as

1714+ insertImpl ps as

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

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

1719− map addUnknownImp badimpls ++

1716+ map addUnknownImp badimpls ++

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

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

1721

1718

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

1719 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

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

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

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

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

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

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

1764−

1761+

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

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

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

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

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

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

src/Idris/CaseSplit.hs+2−2

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

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

73 Just ty ->

74 do let splits = findPats ist ty

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

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

76 (map showTmImpls splits))

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

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

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

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

85 logLvl 3 "----"

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

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

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

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

89 return (map snd newPats')

90

src/Idris/Chaser.hs+2−2

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

90 btree done f =

91 do i <- getIState

92 let file = extractFileName f

93− iLOG $ "CHASING " ++ show file

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

94 ibcsd <- valIBCSubDir i

95 ids <- allImportDirs

96 fp <- findImport ids ibcsd file

97− iLOG $ "Found " ++ show fp

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

98 mt <- runIO $ getIModTime fp

99 if (file `elem` built)

100 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

174 let ds = map (decorateid defaultdec)

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

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

177− iLOG (show ds)

177+ logLvl 1 (show ds)

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

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

180 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

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

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

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

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

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

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

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

237 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

650

651 logLvl 5 "DONE CHECK"

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

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

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

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

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

656 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)

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

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

55 = do let codata = Codata `elem` opts

56− iLOG (show (fc, doc))

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

57 checkUndefined fc n

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

59

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

63

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

65 = do let codata = Codata `elem` opts

66− iLOG (show fc)

66+ logLvl 1 (show fc)

67 undef <- isUndefined fc n

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

69 -- 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

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

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

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

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

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

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

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

117 let wbTys = map mkTyDecl mtys

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

139

140 let idecls = [PClauses fc [Dictionary] iname

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

142− iLOG (show idecls)

142+ logLvl 1 (show idecls)

143 push_estack iname True

144 mapM_ (rec_elabDecl info EAll info) idecls

145 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

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

58

59 -- Build data declaration for elaboration

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

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

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

62 elabData info rsyn doc paramDocs fc opts datadecl

63

64− iLOG $ "fieldsWithName " ++ show fieldsWithName

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

65− iLOG $ "fieldsWIthNameAndDoc " ++ show fieldsWithNameAndDoc

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

66 elabRecordFunctions info rsyn fc tyn paramsAndDoc fieldsWithNameAndDoc dconName target

67

68 sendHighlighting $

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

154elabRecordFunctions info rsyn fc tyn params fields dconName target

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

156

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

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

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

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

159 -- The elaborated constructor type for the data declaration

160 i <- getIState

161 ttConsTy <-

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

165

166 -- The arguments to the constructor

167 let constructorArgs = getArgTys ttConsTy

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

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

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

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

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

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

172

src/Idris/ElabDecls.hs+12−12

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

158 = return () -- nothing to elaborate

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

160 | what /= EDefns

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

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

162 elabType info s doc argdocs f o n nfc ty

163 return ()

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

165 | what /= EDefns

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

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

167 if b

168 then elabExtern info s doc f o n ty

169 else elabPostulate info s doc f o n ty

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

171 | what /= ETypes

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

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

173 elabData info s doc argDocs f co d

174 | otherwise

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

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

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

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

178 | what /= ETypes

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

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

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

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

182 [fs] -> fs

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

190 -- record mutually defined data definitions

191 let datans = concatMap declared (filter isDataDecl ps)

192 mapM_ (setMutData datans) datans

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

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

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

195 -- Do totality checking after entire mutual block

196 i <- get

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

215

216elabDecl' what info (PParams f ns ps)

217 = do i <- getIState

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

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

219 show (concatMap tldeclared ps)

220 let nblock = pblock i

221 mapM_ (elabDecl' what info) nblock

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

239

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

241 | what /= EDefns

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

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

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

244elabDecl' 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

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

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

248 | what /= ETypes

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

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

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

251{-

252 | otherwise

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

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

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

255-}

256elabDecl' _ info (PDSL n dsl)

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

261 | what /= EDefns = directiveAction i

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

263 | what /= EDefns

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

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

265 elabProvider doc info syn fc provWhat n

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

267 = do elabTransform info fc safety old new

src/Idris/IBC.hs+14−14

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

105 Nothing -> True

106 Just p -> not p && reexport

107 when redo $

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

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

109 archiveFile <- runIO $ B.readFile fp

110 case toArchiveOrFail archiveFile of

111 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

180

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

182writeIBC src f

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

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

184 i <- getIState

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

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

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

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

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

191 writeArchive f ibcf

192− iLOG "Written")

192+ logLvl 1 "Written")

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

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

194 return ()

195

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

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

199writePkgIndex f

200 = do i <- getIState

201 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" ++

203 show (map snd imps)

204 resetNameIdx

205 let ibcf = initIBC { ibc_imports = imps }

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

207 writeArchive f ibcf

208− iLOG "Written")

208+ logLvl 1 "Written")

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

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

210 return ()

211

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

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

305process reexp i fn = do

306 ver <- getEntry 0 "ver" i

307 when (ver /= ibcVersion) $ do

308− iLOG "ibc out of date"

308+ logLvl 1 "ibc out of date"

309 let e = if ver < ibcVersion

310 then " an earlier " else " a later "

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

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

395 ids <- allImportDirs

396 fp <- findImport ids ibcsd f

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

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

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

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

400 case fp of

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

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

402 ifail "Must be an ibc"

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

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

404 ifail "Must be an ibc"

405 IBC fn src -> loadIBC re fn)

406 fs

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

491 do d' <- updateDef d

492 case d' of

493 TyDecl _ _ -> return ()

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

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

495 solveDeferred n

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

497-- 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

499 setAccessibility n Hidden

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

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

501 where

502 updateDef (CaseOp c t args o s cd)

503 = do o' <- mapM updateOrig o

src/Idris/Interactive.hs+1−1

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

35caseSplitAt fn updatefile l n

36 = do src <- runIO $ readSource fn

37 res <- splitOnLine l n fn

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

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

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

40 res' <- replaceSplits ap res

41 let new = concat res'

src/Idris/Parser.hs+8−8

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

1362 ids <- allImportDirs

1363 fp <- findImport ids ibcsd file

1364 if file `elem` imported i

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

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

1366 return Nothing

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

1368 case fp of

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

1370 LIDR fn -> loadSource True fn Nothing

1371 IBC fn src ->

1372 idrisCatch (loadIBC True fn)

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

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

1374 case src of

1375 IDR sfn -> loadSource False sfn Nothing

1376 LIDR sfn -> loadSource True sfn Nothing)

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

1379{- | Load idris code from file -}

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

1381loadFromIFile reexp i@(IBC fn src) maxline

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

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

1383 idrisCatch (loadIBC reexp fn)

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

1385 where

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

1403{- | Load Idris source code-}

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

1405loadSource lidr f toline

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

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

1407 i <- getIState

1408 let def_total = default_total i

1409 file_in <- runIO $ readSource f

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

1505 setContext ctxt')

1506 (map snd (idris_totcheck i))

1507 -- build size change graph from simplified definitions

1508− iLOG "Totality checking"

1508+ logLvl 1 "Totality checking"

1509 i <- getIState

1510 mapM_ buildSCG (idris_totcheck i)

1511 mapM_ checkDeclTotality (idris_totcheck i)

1512

1513 -- Redo totality check for deferred names

1514 let deftots = idris_defertotcheck i

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

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

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

1517 case tot of

1518 Total _ -> setTotality x Unchecked

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

1520 mapM_ buildSCG deftots

1521 mapM_ checkDeclTotality deftots

1522

1523− iLOG ("Finished " ++ f)

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

1524 ibcsd <- valIBCSubDir i

1525− iLOG "Universe checking"

1525+ logLvl 1 "Universe checking"

1526 iucheck

1527 let ibc = ibcPathNoFallback ibcsd f

1528 i <- getIState

src/Idris/Prover.hs+1−1

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

90 if mode

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

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

93− iLOG $ "Adding " ++ show tm

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

94 i <- getIState

95 let shower = if mode

96 then showRunElab

src/Idris/REPL.hs+4−4

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

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

1206 Just x -> do let libs = idris_dynamic_libs i

1207 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)

1209 return ()

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

1211 where trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace

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

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

1477 input

1478 let ifiles = getModuleFiles modTree

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

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

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

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

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

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

1483 -- return the files that need rechecking

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

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

1697 idrisCatch (do dir <- getIdrisUserDataDir

1698 exists <- runIO $ doesDirectoryExist dir

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

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

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

1701 (\e -> return ())

1702