39a8c78 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Categorised the Logs.

Most, but not all the logging statements have been categorised. Several new categories have been defined: + Coverage :: For coverage checking. + Erasure :: For erasure.

commit39a8c780595e8a6d5e5b2954fa30844b946cae23 authorJan de Muijnck-Hughes <jfdm@st-andrews.ac.uk> dateFri 18 Dec 2015, 13:18 (11 years ago) parent5dc9d1a

24 files changed+426−430

compare with master

unifiedsplit

src/IRTS/Compiler.hs+18−18

@@ -54,12 +54,12 @@ compile codegen f mtm

5454 Nothing -> []

5555 Just t -> freeNames t

5656

57− reachableNames <- performUsageAnalysis

57+ reachableNames <- performUsageAnalysis

5858 (rootNames ++ getExpNames exports)

5959 maindef <- case mtm of

6060 Nothing -> return []

6161 Just tm -> do md <- irMain tm

62− logLvl 1 $ "MAIN: " ++ show md

62+ logCodeGen 1 $ "MAIN: " ++ show md

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

6464 objs <- getObjectFiles codegen

6565 libs <- getLibs codegen

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

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

8383 let ctxtIn = addAlist tagged emptyContext

8484

85− logLvl 1 "Defunctionalising"

85+ logCodeGen 1 "Defunctionalising"

8686 let defuns_in = defunctionalise nexttag ctxtIn

87− logLvl 5 $ show defuns_in

88− logLvl 1 "Inlining"

87+ logCodeGen 5 $ show defuns_in

88+ logCodeGen 1 "Inlining"

8989 let defuns = inline defuns_in

90− logLvl 5 $ show defuns

91− logLvl 1 "Resolving variables for CG"

90+ logCodeGen 5 $ show defuns

91+ logCodeGen 1 "Resolving variables for CG"

9292

9393 let checked = simplifyDefs defuns (toAlist defuns)

9494 outty <- outputTy

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

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

103103 triple <- Idris.AbsSyntax.targetTriple

104104 cpu <- Idris.AbsSyntax.targetCPU

105− logLvl 1 "Building output"

105+ logCodeGen 1 "Building output"

106106 case checked of

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

108108 hdrs impdirs objs libs flags

@@ -184,10 +184,10 @@ build (n, d)

184184 return (n, (LFun [] n (take ar args)

185185 (LOp op (map (LV . Glob) (take ar args)))))

186186 _ -> do def <- mkLDecl n d

187− logLvl 3 $ "Compiled " ++ show n ++ " =\n\t" ++ show def

187+ logCodeGen 3 $ "Compiled " ++ show n ++ " =\n\t" ++ show def

188188 return (n, def)

189− where getPrim n i

190− | Just (ar, op) <- lookup n (idris_scprims i)

189+ where getPrim n i

190+ | Just (ar, op) <- lookup n (idris_scprims i)

191191 = Just (ar, op)

192192 | Just ar <- lookup n (S.toList (idris_externs i))

193193 = Just (ar, LExternal n)

@@ -224,7 +224,7 @@ data VarInfo = VI

224224type Vars = M.Map Name VarInfo

225225

226226irTerm :: Vars -> [Name] -> Term -> Idris LExp

227−irTerm vs env tm@(App _ f a) = do

227+irTerm vs env tm@(App _ f a) = do

228228 ist <- getIState

229229 case unApply tm of

230230 (P _ (UN m) _, args)

@@ -454,19 +454,19 @@ irTerm vs env Impossible = return $ LNothing

454454doForeign :: Vars -> [Name] -> [Term] -> Idris LExp

455455doForeign vs env (ret : fname : world : args)

456456 = do args' <- mapM splitArg args

457− let fname' = toFDesc fname

457+ let fname' = toFDesc fname

458458 let ret' = toFDesc ret

459459 return $ LForeign ret' fname' args'

460460 where

461461 splitArg tm | (_, [_,_,l,r]) <- unApply tm -- pair, two implicits

462− = do let l' = toFDesc l

462+ = do let l' = toFDesc l

463463 r' <- irTerm vs env r

464464 return (l', r')

465465 splitArg _ = ifail "Badly formed foreign function call"

466466

467− toFDesc (Constant (Str str)) = FStr str

468− toFDesc tm

469− | (P _ n _, []) <- unApply tm = FCon (deNS n)

467+ toFDesc (Constant (Str str)) = FStr str

468+ toFDesc tm

469+ | (P _ n _, []) <- unApply tm = FCon (deNS n)

470470 | (P _ n _, as) <- unApply tm = FApp (deNS n) (map toFDesc as)

471471 toFDesc _ = FUnknown

472472

@@ -476,7 +476,7 @@ doForeign vs env xs = ifail "Badly formed foreign function call"

476476

477477irTree :: [Name] -> SC -> Idris LExp

478478irTree args tree = do

479− logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree

479+ logCodeGen 3 $ "Compiling " ++ show args ++ "\n" ++ show tree

480480 LLam args <$> irSC M.empty tree

481481

482482irSC :: Vars -> SC -> Idris LExp

src/IRTS/Exports.hs+8−11

@@ -13,7 +13,7 @@ import Data.Maybe

1313findExports :: Idris [ExportIFace]

1414findExports = do exps <- getExports

1515 es <- mapM toIFace exps

16− logLvl 2 $ "Exporting " ++ show es

16+ logCodeGen 2 $ "Exporting " ++ show es

1717 return es

1818

1919getExpNames :: [ExportIFace] -> [Name]

@@ -39,7 +39,7 @@ toIFace n = do i <- getIState

3939 getExpList _ = ifail "Badly formed export list"

4040

4141toIFaceTyVal :: Type -> Term -> Idris ExportIFace

42−toIFaceTyVal ty tm

42+toIFaceTyVal ty tm

4343 | (P _ exp _, [P _ ffi _, Constant (Str hdr), _]) <- unApply ty

4444 = do tm' <- toIFaceVal tm

4545 return $ Export ffi hdr tm'

@@ -51,7 +51,7 @@ toIFaceVal tm

5151 | (P _ fun _, [_,_,_,_,(P _ fn _),extnm,prf,rest]) <- unApply tm,

5252 fun == sNS (sUN "Fun") ["FFI_Export"]

5353 = do rest' <- toIFaceVal rest

54− return $

54+ return $

5555 ExportFun fn (toFDesc extnm) (toFDescRet prf) (toFDescArgs prf)

5656 : rest'

5757 | (P _ dat _, [_,_,_,_,d,rest]) <- unApply tm,

@@ -63,7 +63,7 @@ toIFaceVal tm

6363toFDesc :: Term -> FDesc

6464toFDesc (Constant (Str str)) = FStr str

6565toFDesc tm

66− | (P _ n _, []) <- unApply tm = FCon (deNS n)

66+ | (P _ n _, []) <- unApply tm = FCon (deNS n)

6767 | (P _ n _, as) <- unApply tm = FApp (deNS n) (map toFDesc as)

6868toFDesc _ = FUnknown

6969

@@ -91,20 +91,17 @@ toFDescBase tm

9191 | otherwise = error "Badly formed export type"

9292

9393toFDescArgs :: Term -> [FDesc]

94−toFDescArgs tm

94+toFDescArgs tm

9595 | (P _ fun _, [_,_,_,_,b,t]) <- unApply tm,

9696 fun == sNS (sUN "FFI_Fun") ["FFI_Export"]

9797 = toFDescBase b : toFDescArgs t

9898 | otherwise = []

9999

100−toFDescPrim (Constant (Str str)) = FStr str

101−toFDescPrim tm

102− | (P _ n _, []) <- unApply tm = FCon (deNS n)

100+toFDescPrim (Constant (Str str)) = FStr str

101+toFDescPrim tm

102+ | (P _ n _, []) <- unApply tm = FCon (deNS n)

103103 | (P _ n _, as) <- unApply tm = FApp (deNS n) (map toFDescPrim as)

104104toFDescPrim _ = FUnknown

105105

106106deNS (NS n _) = n

107107deNS n = n

108−

109−

110−

src/Idris/AbsSyntax.hs+6

@@ -980,6 +980,12 @@ setColour ct c = do i <- getIState

980980logLvl :: Int -> String -> Idris ()

981981logLvl = logLvlCats []

982982

983+logCoverage :: Int -> String -> Idris ()

984+logCoverage = logLvlCats [ICoverage]

985+

986+logErasure :: Int -> String -> Idris ()

987+logErasure = logLvlCats [IErasure]

988+

983989-- | Log an action of the parser

984990logParser :: Int -> String -> Idris ()

985991logParser = logLvlCats parserCats

src/Idris/AbsSyntaxTree.hs+2

@@ -460,6 +460,8 @@ data OutputFmt = HTMLOutput | LaTeXOutput

460460data LogCat = IParse

461461 | IElab

462462 | ICodeGen

463+ | IErasure

464+ | ICoverage

463465 deriving (Show, Eq, Ord)

464466

465467codegenCats :: [LogCat]

src/Idris/CaseSplit.hs+33−37

@@ -65,20 +65,20 @@ split n t'

6565 -- ASSUMPTION: tm is in normal form after elabValBind, so we don't

6666 -- need to do anything special to find out what family each argument

6767 -- is in

68− logLvl 4 ("Elaborated:\n" ++ show tm ++ " : " ++ show ty ++ "\n" ++ show pats)

68+ logElab 4 ("Elaborated:\n" ++ show tm ++ " : " ++ show ty ++ "\n" ++ show pats)

6969-- iputStrLn (show (delab ist tm) ++ " : " ++ show (delab ist ty))

7070-- iputStrLn (show pats)

71− let t = mergeUserImpl (addImplPat ist t') (delab ist tm)

71+ let t = mergeUserImpl (addImplPat ist t') (delab ist tm)

7272 let ctxt = tt_ctxt ist

7373 case lookup n pats of

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

7575 Just ty ->

7676 do let splits = findPats ist ty

77− logLvl 1 ("New patterns " ++ showSep ", "

77+ logElab 1 ("New patterns " ++ showSep ", "

7878 (map showTmImpls splits))

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

80− logLvl 4 ("Working from " ++ show t)

81− logLvl 4 ("Trying " ++ showSep "\n"

80+ logElab 4 ("Working from " ++ show t)

81+ logElab 4 ("Trying " ++ showSep "\n"

8282 (map (showTmImpls) newPats_in))

8383 newPats_in <- mapM elabNewPat newPats_in

8484 case anyValid [] [] newPats_in of

@@ -86,16 +86,16 @@ split n t'

8686 let fails' = mergeAllPats ist n t fails

8787 return (False, (map snd fails'))

8888 Right newPats -> do

89− logLvl 3 ("Original:\n" ++ show t)

90− logLvl 3 ("Split:\n" ++

89+ logElab 3 ("Original:\n" ++ show t)

90+ logElab 3 ("Split:\n" ++

9191 (showSep "\n" (map show newPats)))

92− logLvl 3 "----"

92+ logElab 3 "----"

9393 let newPats' = mergeAllPats ist n t newPats

94− logLvl 1 ("Name updates " ++ showSep "\n"

94+ logElab 1 ("Name updates " ++ showSep "\n"

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

9696 return (True, (map snd newPats'))

97− where

98− anyValid ok bad [] = if null ok then Left (reverse bad)

97+ where

98+ anyValid ok bad [] = if null ok then Left (reverse bad)

9999 else Right (reverse ok)

100100 anyValid ok bad ((tc, p) : ps)

101101 | tc = anyValid (p : ok) bad ps

@@ -111,7 +111,7 @@ addUpdate n tm = do ms <- get

111111 put (ms { updates = ((n, stripNS tm) : updates ms) } )

112112

113113inventName :: Idris.AbsSyntaxTree.IState -> Maybe Name -> Name -> State MergeState Name

114−inventName ist ty n =

114+inventName ist ty n =

115115 do ms <- get

116116 let supp = case ty of

117117 Nothing -> []

@@ -131,11 +131,11 @@ inventName ist ty n =

131131 do let n' = uniqueNameFrom nsupp badnames

132132 put (ms { invented = (n, n') : invented ms })

133133 return n'

134−

134+

135135mkSupply :: [Name] -> [Name]

136136mkSupply ns = mkSupply' ns (map nextName ns)

137137 where mkSupply' xs ns' = xs ++ mkSupply ns'

138−

138+

139139varlist :: [Name]

140140varlist = map (sUN . (:[])) "xyzwstuv" -- EB's personal preference :)

141141

@@ -147,7 +147,7 @@ stripNS tm = mapPT dens tm where

147147mergeAllPats :: IState -> Name -> PTerm -> [PTerm] -> [(PTerm, [(Name, PTerm)])]

148148mergeAllPats ist cv t [] = []

149149mergeAllPats ist cv t (p : ps)

150− = let (p', MS _ _ _ u) = runState (mergePat ist t p Nothing)

150+ = let (p', MS _ _ _ u) = runState (mergePat ist t p Nothing)

151151 (MS [] [] (filter (/=cv) (patvars t)) [])

152152 ps' = mergeAllPats ist cv t ps in

153153 ((p', u) : ps')

@@ -192,7 +192,7 @@ mergeUserImpl :: PTerm -> PTerm -> PTerm

192192mergeUserImpl x y = x

193193

194194argTys :: IState -> PTerm -> [Maybe Name]

195−argTys ist (PRef fc hls n)

195+argTys ist (PRef fc hls n)

196196 = case lookupTy n (tt_ctxt ist) of

197197 [ty] -> map (tyName . snd) (getArgTys ty) ++ repeat Nothing

198198 _ -> repeat Nothing

@@ -227,7 +227,7 @@ elabNewPat t = idrisCatch (do (tm, ty) <- elabVal recinfo ELHS t

227227 i <- getIState

228228 return (True, delab i tm))

229229 (\e -> do i <- getIState

230− logLvl 5 $ "Not a valid split:\n" ++ pshow i e

230+ logElab 5 $ "Not a valid split:\n" ++ pshow i e

231231 return (False, t))

232232

233233findPats :: IState -> Type -> [PTerm]

@@ -250,7 +250,7 @@ replaceVar ctxt n t (PApp fc f pats) = PApp fc f (map substArg pats)

250250 subst orig@(PRef _ _ v) | v == n = t

251251 | isDConName v ctxt = orig

252252 subst (PRef _ _ _) = Placeholder

253− subst (PApp fc (PRef _ _ t) pats)

253+ subst (PApp fc (PRef _ _ t) pats)

254254 | isTConName t ctxt = Placeholder -- infer types

255255 subst (PApp fc f pats) = PApp fc f (map substArg pats)

256256 subst x = x

@@ -265,9 +265,9 @@ splitOnLine :: Int -- ^ line number

265265 -> Idris (Bool, [[(Name, PTerm)]])

266266splitOnLine l n fn = do

267267 cl <- getInternalApp fn l

268− logLvl 3 ("Working with " ++ showTmImpls cl)

268+ logElab 3 ("Working with " ++ showTmImpls cl)

269269 tms <- split n cl

270− return tms

270+ return tms

271271

272272replaceSplits :: String -> [[(Name, PTerm)]] -> Bool -> Idris [String]

273273replaceSplits l ups impossible

@@ -277,7 +277,7 @@ replaceSplits l ups impossible

277277 rep str ((n, tm) : ups) = rep (updatePat False (show n) (nshow tm) str) ups

278278

279279 updateRHSs i [] = return []

280− updateRHSs i (x : xs)

280+ updateRHSs i (x : xs)

281281 | impossible = do xs' <- updateRHSs i xs

282282 return (setImpossible False x : xs')

283283 | otherwise = do (x', i') <- updateRHS (null xs) i x

@@ -286,7 +286,7 @@ replaceSplits l ups impossible

286286

287287 updateRHS last i ('?':'=':xs) = do (xs', i') <- updateRHS last i xs

288288 return ("?=" ++ xs', i')

289− updateRHS last i ('?':xs)

289+ updateRHS last i ('?':xs)

290290 = do let (nm, rest_in) = span (not . (\x -> isSpace x || x == ')'

291291 || x == '(')) xs

292292 let rest = if last then rest_in else

@@ -341,7 +341,7 @@ replaceSplits l ups impossible

341341 | otherwise = tm

342342

343343

344−getUniq :: (Show t, Num t) => [Char] -> t -> Idris ([Char], t)

344+getUniq :: (Show t, Num t) => [Char] -> t -> Idris ([Char], t)

345345getUniq nm i

346346 = do ist <- getIState

347347 let n = nameRoot [] nm ++ "_" ++ show i

@@ -360,7 +360,7 @@ getClause :: Int -- ^ line number that the type is declared on

360360 -> Name -- ^ User given name

361361 -> FilePath -- ^ Source file name

362362 -> Idris String

363−getClause l fn un fp

363+getClause l fn un fp

364364 = do i <- getIState

365365 case lookupCtxt un (idris_classes i) of

366366 [c] -> return (mkClassBodies i (class_methods c))

@@ -370,18 +370,18 @@ getClause l fn un fp

370370 x -> x

371371 ist <- get

372372 let ap = mkApp ist ty []

373− return (show un ++ " " ++ ap ++ "= ?"

373+ return (show un ++ " " ++ ap ++ "= ?"

374374 ++ show un ++ "_rhs")

375375 where mkApp :: IState -> PTerm -> [Name] -> String

376376 mkApp i (PPi (Exp _ _ False) (MN _ _) _ ty sc) used

377377 = let n = getNameFrom i used ty in

378− show n ++ " " ++ mkApp i sc (n : used)

378+ show n ++ " " ++ mkApp i sc (n : used)

379379 mkApp i (PPi (Exp _ _ False) (UN n) _ ty sc) used

380380 | thead n == '_'

381381 = let n = getNameFrom i used ty in

382− show n ++ " " ++ mkApp i sc (n : used)

383− mkApp i (PPi (Exp _ _ False) n _ _ sc) used

384− = show n ++ " " ++ mkApp i sc (n : used)

382+ show n ++ " " ++ mkApp i sc (n : used)

383+ mkApp i (PPi (Exp _ _ False) n _ _ sc) used

384+ = show n ++ " " ++ mkApp i sc (n : used)

385385 mkApp i (PPi _ _ _ _ sc) used = mkApp i sc used

386386 mkApp i _ _ = ""

387387

@@ -394,16 +394,16 @@ getClause l fn un fp

394394 sUN "z"]) used

395395 ns -> uniqueNameFrom (mkSupply ns) used

396396 getNameFrom i used _ = uniqueNameFrom (mkSupply [sUN "x", sUN "y",

397− sUN "z"]) used

397+ sUN "z"]) used

398398

399399 -- write method declarations, indent with 4 spaces

400400 mkClassBodies :: IState -> [(Name, (FnOpts, PTerm))] -> String

401− mkClassBodies i ns

401+ mkClassBodies i ns

402402 = showSep "\n"

403− (zipWith (\(n, (_, ty)) m -> " " ++

403+ (zipWith (\(n, (_, ty)) m -> " " ++

404404 def (show (nsroot n)) ++ " "

405405 ++ mkApp i ty []

406− ++ "= ?"

406+ ++ "= ?"

407407 ++ show un ++ "_rhs_" ++ show m) ns [1..])

408408

409409 def n@(x:xs) | not (isAlphaNum x) = "(" ++ n ++ ")"

@@ -456,7 +456,3 @@ nameMissing ps = do ist <- get

456456 case mptm of

457457 (False, _) -> return ptm

458458 (True, ptm') -> return ptm'

459−

460−

461−

462−

src/Idris/CmdOptions.hs+2

@@ -192,6 +192,8 @@ parseLogCats s =

192192 parseLogCat = (string "parser" *> return parserCats)

193193 <|> (string "elab" *> return elabCats)

194194 <|> (string "codegen" *> return codegenCats)

195+ <|> (string "coverage" *> return [ICoverage])

196+ <|> (string "erasure" *> return [IErasure])

195197 <|> parseLogCatBad

196198

197199 parseLogCatBad :: ReadP [LogCat]

src/Idris/Coverage.hs+24−24

@@ -56,17 +56,17 @@ genClauses fc n xs given

5656 = do i <- getIState

5757 let lhs_tms = map (\x -> flattenArgs $ delab' i x True True) xs

5858 -- if a placeholder was given, don't bother generating cases for it

59− let lhs_tms' = zipWith mergePlaceholders lhs_tms

59+ let lhs_tms' = zipWith mergePlaceholders lhs_tms

6060 (map (stripUnmatchable i) (map flattenArgs given))

6161 let lhss = map pUnApply lhs_tms'

6262

6363 let argss = transpose lhss

6464 let all_args = map (genAll i) argss

65− logLvl 5 $ "COVERAGE of " ++ show n

66− logLvl 5 $ show (lhs_tms, lhss)

67− logLvl 5 $ show (map length argss) ++ "\n" ++ show (map length all_args)

68− logLvl 10 $ show argss ++ "\n" ++ show all_args

69− logLvl 3 $ "Original: \n" ++

65+ logCoverage 5 $ "COVERAGE of " ++ show n

66+ logCoverage 5 $ show (lhs_tms, lhss)

67+ logCoverage 5 $ show (map length argss) ++ "\n" ++ show (map length all_args)

68+ logCoverage 10 $ show argss ++ "\n" ++ show all_args

69+ logCoverage 3 $ "Original: \n" ++

7070 showSep "\n" (map (\t -> showTm i (delab' i t True True)) xs)

7171 -- add an infinite supply of explicit arguments to update the possible

7272 -- cases for (the return type may be variadic, or function type, so

@@ -77,11 +77,11 @@ genClauses fc n xs given

7777 p ++ repeat (PExp 0 [] (sMN 0 "gcarg") Placeholder)

7878 _ -> repeat (pexp Placeholder)

7979 let tryclauses = mkClauses parg all_args

80− logLvl 3 $ show (length tryclauses) ++ " initially to check"

81− logLvl 2 $ showSep "\n" (map (showTm i) tryclauses)

80+ logCoverage 3 $ show (length tryclauses) ++ " initially to check"

81+ logCoverage 2 $ showSep "\n" (map (showTm i) tryclauses)

8282 let new = filter (noMatch i) (nub tryclauses)

83− logLvl 2 $ show (length new) ++ " clauses to check for impossibility"

84− logLvl 4 $ "New clauses: \n" ++ showSep "\n" (map (showTm i) new)

83+ logCoverage 2 $ show (length new) ++ " clauses to check for impossibility"

84+ logCoverage 4 $ "New clauses: \n" ++ showSep "\n" (map (showTm i) new)

8585-- ++ " from:\n" ++ showSep "\n" (map (showImp True) tryclauses)

8686 return new

8787-- return (map (\t -> PClause n t [] PImpossible []) new)

@@ -92,7 +92,7 @@ genClauses fc n xs given

9292 pUnApply (PApp _ f args) = map getTm args

9393 pUnApply _ = []

9494

95− flattenArgs (PApp fc (PApp _ f as) as')

95+ flattenArgs (PApp fc (PApp _ f as) as')

9696 = flattenArgs (PApp fc f (as ++ as'))

9797 flattenArgs t = t

9898

@@ -248,7 +248,7 @@ genAll i args

248248

249249 -- put it back to its original form

250250 resugar (PApp _ (PRef fc hl n) [_,_,t,v])

251− | n == sigmaCon

251+ | n == sigmaCon

252252 = PDPair fc [] TypeOrTerm (getTm t) Placeholder (getTm v)

253253 resugar (PApp _ (PRef fc hl n) [_,_,l,r])

254254 | n == pairCon

@@ -330,7 +330,7 @@ checkPositive mut_ns (cn, ty')

330330 let tot = if p then Total (args ty) else Partial NotPositive

331331 let ctxt' = setTotal cn tot (tt_ctxt i)

332332 putIState (i { tt_ctxt = ctxt' })

333− logLvl 5 $ "Constructor " ++ show cn ++ " is " ++ show tot ++ " with " ++ show mut_ns

333+ logCoverage 5 $ "Constructor " ++ show cn ++ " is " ++ show tot ++ " with " ++ show mut_ns

334334 addIBC (IBCTotal cn tot)

335335 return tot

336336 where

@@ -432,9 +432,9 @@ checkTotality path fc n

432432

433433checkDeclTotality :: (FC, Name) -> Idris Totality

434434checkDeclTotality (fc, n)

435− = do logLvl 2 $ "Checking " ++ show n ++ " for totality"

435+ = do logCoverage 2 $ "Checking " ++ show n ++ " for totality"

436436-- buildSCG (fc, n)

437−-- logLvl 2 $ "Built SCG"

437+-- logCoverage 2 $ "Built SCG"

438438 i <- getIState

439439 let opts = case lookupCtxt n (idris_flags i) of

440440 [fs] -> fs

@@ -446,7 +446,7 @@ checkDeclTotality (fc, n)

446446 -- typechecking decidable

447447 p@(Partial _) -> do setAccessibility n Frozen

448448 addIBC (IBCAccess n Frozen)

449− logLvl 5 $ "HIDDEN: "

449+ logCoverage 5 $ "HIDDEN: "

450450 ++ show n ++ show p

451451 _ -> return ()

452452 return t

@@ -469,12 +469,12 @@ buildSCG (_, n) = do

469469 [cg] -> case lookupDefExact n (tt_ctxt ist) of

470470 Just (CaseOp _ _ _ pats _ cd) ->

471471 let (args, sc) = cases_totcheck cd in

472− do logLvl 2 $ "Building SCG for " ++ show n ++ " from\n"

472+ do logCoverage 2 $ "Building SCG for " ++ show n ++ " from\n"

473473 ++ show pats ++ "\n" ++ show sc

474474 let newscg = buildSCG' ist (rights pats) args

475− logLvl 5 $ "SCG is: " ++ show newscg

475+ logCoverage 5 $ "SCG is: " ++ show newscg

476476 addToCG n ( cg { scg = newscg } )

477− [] -> logLvl 5 $ "Could not build SCG for " ++ show n ++ "\n"

477+ [] -> logCoverage 5 $ "Could not build SCG for " ++ show n ++ "\n"

478478 x -> error $ "buildSCG: " ++ show (n, x)

479479

480480delazy = delazy' False -- not lazy codata

@@ -594,20 +594,20 @@ checkSizeChange n = do

594594 ist <- getIState

595595 case lookupCtxt n (idris_callgraph ist) of

596596 [cg] -> do let ms = mkMultiPaths ist [] (scg cg)

597− logLvl 5 ("Multipath for " ++ show n ++ ":\n" ++

597+ logCoverage 5 ("Multipath for " ++ show n ++ ":\n" ++

598598 "from " ++ show (scg cg) ++ "\n" ++

599599 show (length ms) ++ "\n" ++

600600 showSep "\n" (map show ms))

601− logLvl 6 (show cg)

601+ logCoverage 6 (show cg)

602602 -- every multipath must have an infinitely descending

603603 -- thread, then the function terminates

604604 -- also need to checks functions called are all total

605605 -- (Unchecked is okay as we'll spot problems here)

606606 let tot = map (checkMP ist (getArity ist n)) ms

607− logLvl 4 $ "Generated " ++ show (length tot) ++ " paths"

608− logLvl 6 $ "Paths for " ++ show n ++ " yield " ++ (show tot)

607+ logCoverage 4 $ "Generated " ++ show (length tot) ++ " paths"

608+ logCoverage 6 $ "Paths for " ++ show n ++ " yield " ++ (show tot)

609609 return (noPartial tot)

610− [] -> do logLvl 5 $ "No paths for " ++ show n

610+ [] -> do logCoverage 5 $ "No paths for " ++ show n

611611 return Unchecked

612612 where getArity ist n

613613 = case lookupTy n (tt_ctxt ist) of

src/Idris/Elab/Class.hs+10−12

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

7878 let idecls = filter instdecl ds -- default superclass instance declarations

7979 mapM_ checkDefaultSuperclassInstance idecls

8080 let mnames = map getMName mdecls

81− logLvl 1 $ "Building methods " ++ show mnames

81+ logElab 1 $ "Building methods " ++ show mnames

8282 ims <- mapM (tdecl mnames) mdecls

8383 defs <- mapM (defdecl (map (\ (x,y,z) -> z) ims) constraint)

8484 (filter clause ds)

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

9494 let cons = [(cd, pDocs ++ mapMaybe memberDocs ds, cn, NoFC, cty, fc, [])]

9595 let ddecl = PDatadecl tn NoFC tty cons

9696

97− logLvl 5 $ "Class data " ++ show (showDImp verbosePPOption ddecl)

97+ logElab 5 $ "Class data " ++ show (showDImp verbosePPOption ddecl)

9898

9999 -- Elaborate the data declaration

100100 elabData info (syn { no_imp = no_imp syn ++ mnames,

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

109109 -- for each method, build a top level function

110110 fns <- mapM (tfun cn constraint (syn { imp_methods = mnames })

111111 (map fst imethods)) imethods

112− logLvl 5 $ "Functions " ++ show fns

112+ logElab 5 $ "Functions " ++ show fns

113113 -- Elaborate the the top level methods

114114 mapM_ (rec_elabDecl info EAll info) (concat fns)

115115

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

159159 getMName (PTy _ _ _ _ _ n nfc _) = nsroot n

160160 tdecl allmeths (PTy doc _ syn _ o n nfc t)

161161 = do t' <- implicit' info syn (map (\(n, _, _) -> n) ps ++ allmeths) n t

162− logLvl 2 $ "Method " ++ show n ++ " : " ++ showTmImpls t'

162+ logElab 2 $ "Method " ++ show n ++ " : " ++ showTmImpls t'

163163 return ( (n, (toExp (map (\(pn, _, _) -> pn) ps) Exp t')),

164164 (n, (nfc, doc, o, (toExp (map (\(pn, _, _) -> pn) ps)

165165 (\ l s p -> Imp l s p Nothing) t'))),

@@ -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− logLvl 1 (show ds)

177+ logElab 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)"

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

199199 let lhs = PApp fc (PRef fc [] cfn) [pconst capp]

200200 let rhs = PResolveTC (fileFC "HACK")

201201 let ty = PPi constraint cnm NoFC c con

202− logLvl 2 ("Dictionary constraint: " ++ showTmImpls ty)

203− logLvl 2 (showTmImpls lhs ++ " = " ++ showTmImpls rhs)

202+ logElab 2 ("Dictionary constraint: " ++ showTmImpls ty)

203+ logElab 2 (showTmImpls lhs ++ " = " ++ showTmImpls rhs)

204204 i <- getIState

205205 let conn = case con of

206206 PRef _ _ n -> n

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

230230 let anames = map (\x -> sMN x "arg") [0..]

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)

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

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

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

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

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

235+ logElab 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 []]]

238238

@@ -318,5 +318,3 @@ findDets n ns =

318318 | n `elem` ns = i : getDetPos (i + 1) ns sc

319319 | otherwise = getDetPos (i + 1) ns sc

320320 getDetPos _ _ _ = []

321−

322−

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

@@ -84,7 +84,7 @@ elabClauses info' fc opts n_in cs =

8484 -- no simplification or PE

8585 let (pats_in, cs_full) = unzip cs_elab

8686 let pats_raw = map (simple_lhs (tt_ctxt ist)) pats_in

87− logLvl 3 $ "Elaborated patterns:\n" ++ show pats_raw

87+ logElab 3 $ "Elaborated patterns:\n" ++ show pats_raw

8888

8989 solveDeferred n

9090

@@ -102,7 +102,7 @@ elabClauses info' fc opts n_in cs =

102102 -- If the definition is specialisable, this reduces the

103103 -- RHS

104104 pe_tm <- doPartialEval ist tpats

105− let pats_pe = if petrans

105+ let pats_pe = if petrans

106106 then map (simple_lhs (tt_ctxt ist)) pe_tm

107107 else pats_raw

108108

@@ -111,7 +111,7 @@ elabClauses info' fc opts n_in cs =

111111 -- Look for 'static' names and generate new specialised

112112 -- definitions for them, as well as generating rewrite rules

113113 -- for partially evaluated definitions

114− newrules <- if petrans

114+ newrules <- if petrans

115115 then mapM (\ e -> case e of

116116 Left _ -> return []

117117 Right (l, r) -> elabPE info fc n r) pats_pe

@@ -134,12 +134,12 @@ elabClauses info' fc opts n_in cs =

134134 -- pdef is the compile-time pattern definition.

135135 -- This will get further inlined to help with totality checking.

136136 let pdef = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) $ map debind pats_raw

137− -- pdef_pe is the one which will get further optimised

137+ -- pdef_pe is the one which will get further optimised

138138 -- for run-time, and, partially evaluated

139139 let pdef_pe = map debind pats_transformed

140140

141− logLvl 5 $ "Initial typechecked patterns:\n" ++ show pats_raw

142− logLvl 5 $ "Initial typechecked pattern def:\n" ++ show pdef

141+ logElab 5 $ "Initial typechecked patterns:\n" ++ show pats_raw

142+ logElab 5 $ "Initial typechecked pattern def:\n" ++ show pdef

143143

144144 -- NOTE: Need to store original definition so that proofs which

145145 -- rely on its structure aren't affected by any changes to the

@@ -152,10 +152,10 @@ elabClauses info' fc opts n_in cs =

152152 numArgs <- tclift $ sameLength pdef

153153

154154 case specNames opts of

155− Just _ ->

156− do logLvl 3 $ "Partially evaluated:\n" ++ show pats_pe

155+ Just _ ->

156+ do logElab 3 $ "Partially evaluated:\n" ++ show pats_pe

157157 _ -> return ()

158− logLvl 3 $ "Transformed:\n" ++ show pats_transformed

158+ logElab 3 $ "Transformed:\n" ++ show pats_transformed

159159

160160 erInfo <- getErasureInfo <$> getIState

161161 tree@(CaseDef scargs sc _) <- tclift $

@@ -167,7 +167,7 @@ elabClauses info' fc opts n_in cs =

167167 -- missing <- genMissing n scargs sc

168168 missing' <- filterM (checkPossible info fc True n) missing

169169 let clhs = map getLHS pdef

170− logLvl 2 $ "Must be unreachable:\n" ++

170+ logElab 2 $ "Must be unreachable:\n" ++

171171 showSep "\n" (map showTmImpls missing') ++

172172 "\nAgainst: " ++

173173 showSep "\n" (map (\t -> showTmImpls (delab ist t)) (map getLHS pdef))

@@ -185,12 +185,12 @@ elabClauses info' fc opts n_in cs =

185185 pdef_in' <- applyOpts $ map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) pdef_pe

186186 let pdef' = map (simple_rt (tt_ctxt ist)) pdef_in'

187187

188− logLvl 5 $ "After data structure transformations:\n" ++ show pdef'

188+ logElab 5 $ "After data structure transformations:\n" ++ show pdef'

189189

190190 ist <- getIState

191191 -- let wf = wellFounded ist n sc

192192 let tot | pcover || AssertTotal `elem` opts = Unchecked -- finish later

193− | PEGenerated `elem` opts = Generated

193+ | PEGenerated `elem` opts = Generated

194194 | otherwise = Partial NotCovering -- already know it's not total

195195

196196 -- case lookupCtxt (namespace info) n (idris_flags ist) of

@@ -206,17 +206,17 @@ elabClauses info' fc opts n_in cs =

206206 ":warning - Unreachable case: " ++

207207 show (delab ist x)) xs

208208 let knowncovering = (pcover && cov) || AssertTotal `elem` opts

209− let defaultcase = if knowncovering

209+ let defaultcase = if knowncovering

210210 then STerm Erased

211− else UnmatchedCase $ "*** " ++

212− show fc ++

213− ":unmatched case in " ++ show n ++

211+ else UnmatchedCase $ "*** " ++

212+ show fc ++

213+ ":unmatched case in " ++ show n ++

214214 " ***"

215215

216216 tree' <- tclift $ simpleCase tcase defaultcase reflect

217217 RunTime fc inacc atys pdef' erInfo

218− logLvl 3 $ "Unoptimised " ++ show n ++ ": " ++ show tree

219− logLvl 3 $ "Optimised: " ++ show tree'

218+ logElab 3 $ "Unoptimised " ++ show n ++ ": " ++ show tree

219+ logElab 3 $ "Optimised: " ++ show tree'

220220 ctxt <- getContext

221221 ist <- getIState

222222 let opt = idris_optimisation ist

@@ -224,7 +224,7 @@ elabClauses info' fc opts n_in cs =

224224 (idris_patdefs ist) })

225225 let caseInfo = CaseInfo (inlinable opts) (inlinable opts) (dictionary opts)

226226 case lookupTyExact n ctxt of

227− Just ty ->

227+ Just ty ->

228228 do ctxt' <- do ctxt <- getContext

229229 tclift $

230230 addCasedef n erInfo caseInfo

@@ -242,7 +242,7 @@ elabClauses info' fc opts n_in cs =

242242 setContext ctxt'

243243 addIBC (IBCDef n)

244244 setTotality n tot

245− when (not reflect && PEGenerated `notElem` opts) $

245+ when (not reflect && PEGenerated `notElem` opts) $

246246 do totcheck (fc, n)

247247 defer_totcheck (fc, n)

248248 when (tot /= Unchecked) $ addIBC (IBCTotal n tot)

@@ -256,7 +256,7 @@ elabClauses info' fc opts n_in cs =

256256 -- let scg = buildSCG i sc scargs

257257 -- add SCG later, when checking totality

258258 let cg = CGInfo scargs' calls [] used [] -- TODO: remove this, not needed anymore

259− logLvl 2 $ "Called names: " ++ show cg

259+ logElab 2 $ "Called names: " ++ show cg

260260 addToCG n cg

261261 addToCalledG n (nub (map fst calls)) -- plus names in type!

262262 addIBC (IBCCG n)

@@ -360,7 +360,7 @@ elabPE info fc caller r =

360360 let undef = case lookupDefExact newnm (tt_ctxt ist) of

361361 Nothing -> True

362362 _ -> False

363− logLvl 5 $ show (newnm, undef, map (concreteArg ist) (snd specapp))

363+ logElab 5 $ show (newnm, undef, map (concreteArg ist) (snd specapp))

364364 idrisCatch

365365 (if (undef && all (concreteArg ist) (snd specapp)) then do

366366 cgns <- getAllNames n

@@ -374,32 +374,32 @@ elabPE info fc caller r =

374374 [Total _] -> 65536

375375 [Productive] -> 16

376376 _ -> 1

377− let opts = [Specialise ((if pe_simple specdecl

378− then map (\x -> (x, Nothing)) cgns'

377+ let opts = [Specialise ((if pe_simple specdecl

378+ then map (\x -> (x, Nothing)) cgns'

379379 else []) ++

380− (n, Just maxred) :

380+ (n, Just maxred) :

381381 mapMaybe (specName (pe_simple specdecl))

382382 (snd specapp))]

383− logLvl 3 $ "Specialising application: " ++ show specapp

383+ logElab 3 $ "Specialising application: " ++ show specapp

384384 ++ " in " ++ show caller ++

385385 " with " ++ show opts

386− logLvl 3 $ "New name: " ++ show newnm

387− logLvl 3 $ "PE definition type : " ++ (show specTy)

386+ logElab 3 $ "New name: " ++ show newnm

387+ logElab 3 $ "PE definition type : " ++ (show specTy)

388388 ++ "\n" ++ show opts

389− logLvl 3 $ "PE definition " ++ show newnm ++ ":\n" ++

389+ logElab 3 $ "PE definition " ++ show newnm ++ ":\n" ++

390390 showSep "\n"

391391 (map (\ (lhs, rhs) ->

392392 (showTmImpls lhs ++ " = " ++

393393 showTmImpls rhs)) (pe_clauses specdecl))

394394

395− logLvl 2 $ show n ++ " transformation rule: " ++

395+ logElab 2 $ show n ++ " transformation rule: " ++

396396 showTmImpls rhs ++ " ==> " ++ showTmImpls lhs

397397

398398 elabType info defaultSyntax emptyDocstring [] fc opts newnm NoFC specTy

399399 let def = map (\(lhs, rhs) ->

400400 let lhs' = mapPT hiddenToPH $ stripUnmatchable ist lhs in

401− PClause fc newnm lhs' [] rhs [])

402− (pe_clauses specdecl)

401+ PClause fc newnm lhs' [] rhs [])

402+ (pe_clauses specdecl)

403403 trans <- elabTransform info fc False rhs lhs

404404 elabClauses info fc (PEGenerated:opts) newnm def

405405 return [trans]

@@ -407,7 +407,7 @@ elabPE info fc caller r =

407407 -- if it doesn't work, just don't specialise. Could happen for lots

408408 -- of valid reasons (e.g. local variables in scope which can't be

409409 -- lifted out).

410− (\e -> do logLvl 3 $ "Couldn't specialise: " ++ (pshow ist e)

410+ (\e -> do logElab 3 $ "Couldn't specialise: " ++ (pshow ist e)

411411 return [])

412412

413413 hiddenToPH (PHidden _) = Placeholder

@@ -450,7 +450,7 @@ elabPE info fc caller r =

450450 -- get the clause of a specialised application

451451 getSpecClause ist (n, args)

452452 = let newnm = sUN ("PE_" ++ show (nsroot n) ++ "_" ++

453− qhash 5381 (showSep "_" (map showArg args))) in

453+ qhash 5381 (showSep "_" (map showArg args))) in

454454 -- UN (show n ++ show (map snd args)) in

455455 (n, newnm, mkPE_TermDecl ist newnm n args)

456456 where showArg (ExplicitS, n) = qshow n

@@ -477,7 +477,7 @@ checkPossible info fc tcgen fname lhs_in

477477 let lhs = addImplPat i lhs_in

478478 -- if the LHS type checks, it is possible

479479 case elaborate ctxt (idris_datatypes i) (sMN 0 "patLHS") infP initEState

480− (erun fc (buildTC i info ELHS [] fname

480+ (erun fc (buildTC i info ELHS [] fname

481481 (allNamesIn lhs_in)

482482 (infTerm lhs))) of

483483 OK (ElabResult lhs' _ _ ctxt' newDecls highlights, _) ->

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

570570

571571 let lhs = mkLHSapp $ stripLinear i $ stripUnmatchable i $

572572 propagateParams i params norm_ty (allNamesIn lhs_in) (addImplPat i lhs_in)

573−-- let lhs = mkLHSapp $

573+-- let lhs = mkLHSapp $

574574-- propagateParams i params fn_ty (addImplPat i lhs_in)

575− logLvl 10 (show (params, fn_ty) ++ " " ++ showTmImpls (addImplPat i lhs_in))

576− logLvl 5 ("LHS: " ++ show fc ++ " " ++ showTmImpls lhs)

577− logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show lhs_in ++

575+ logElab 10 (show (params, fn_ty) ++ " " ++ showTmImpls (addImplPat i lhs_in))

576+ logElab 5 ("LHS: " ++ show fc ++ " " ++ showTmImpls lhs)

577+ logElab 4 ("Fixed parameters: " ++ show params ++ " from " ++ show lhs_in ++

578578 "\n" ++ show (fn_ty, fn_is))

579579

580580 ((ElabResult lhs' dlhs [] ctxt' newDecls highlights, probs, inj), _) <-

581581 tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "patLHS") infP initEState

582582 (do res <- errAt "left hand side of " fname Nothing

583− (erun fc (buildTC i info ELHS opts fname

583+ (erun fc (buildTC i info ELHS opts fname

584584 (allNamesIn lhs_in)

585585 (infTerm lhs)))

586586 probs <- get_probs

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

589589 setContext ctxt'

590590 processTacticDecls info newDecls

591591 sendHighlighting highlights

592−

592+

593593 when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_,_) -> (x,y)) probs)

594594

595595 let lhs_tm = orderPats (getInferTerm lhs')

596596 let lhs_ty = getInferType lhs'

597597 let static_names = getStaticNames i lhs_tm

598598

599− logLvl 3 ("Elaborated: " ++ show lhs_tm)

600− logLvl 3 ("Elaborated type: " ++ show lhs_ty)

601− logLvl 5 ("Injective: " ++ show fname ++ " " ++ show inj)

599+ logElab 3 ("Elaborated: " ++ show lhs_tm)

600+ logElab 3 ("Elaborated type: " ++ show lhs_ty)

601+ logElab 5 ("Injective: " ++ show fname ++ " " ++ show inj)

602602

603603 -- If we're inferring metavariables in the type, don't recheck,

604604 -- because we're only doing this to try to work out those metavariables

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

615615 -- Issue #1615 on the Issue Tracker.

616616 -- https://github.com/idris-lang/Idris-dev/issues/1615

617617 when (not (null borrowed)) $

618− logLvl 5 ("Borrowed names on LHS: " ++ show borrowed)

618+ logElab 5 ("Borrowed names on LHS: " ++ show borrowed)

619619

620− logLvl 3 ("Normalised LHS: " ++ showTmImpls (delabMV i clhs))

620+ logElab 3 ("Normalised LHS: " ++ showTmImpls (delabMV i clhs))

621621

622622 rep <- useREPL

623623 when rep $ do

624624 addInternalApp (fc_fname fc) (fst . fc_start $ fc) (delabMV i clhs) -- TODO: Should use span instead of line and filename?

625625 addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) (delabMV i clhs))

626626

627− logLvl 5 ("Checked " ++ show clhs ++ "\n" ++ show clhsty)

627+ logElab 5 ("Checked " ++ show clhs ++ "\n" ++ show clhsty)

628628 -- Elaborate where block

629629 ist <- getIState

630630 windex <- getName

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

647647 -- Elaborate those with a type *before* RHS, those without *after*

648648 let (wbefore, wafter) = sepBlocks wb

649649

650− logLvl 2 $ "Where block:\n " ++ show wbefore ++ "\n" ++ show wafter

650+ logElab 2 $ "Where block:\n " ++ show wbefore ++ "\n" ++ show wafter

651651 mapM_ (rec_elabDecl info EAll winfo) wbefore

652652 -- Now build the RHS, using the type of the LHS as the goal.

653653 i <- getIState -- new implicits from where block

654− logLvl 5 (showTmImpls (expandParams decorate newargs defs (defs \\ decls) rhs_in))

654+ logElab 5 (showTmImpls (expandParams decorate newargs defs (defs \\ decls) rhs_in))

655655 let rhs = addImplBoundInf i (map fst newargs_all) (defs \\ decls)

656656 (expandParams decorate newargs defs (defs \\ decls) rhs_in)

657− logLvl 2 $ "RHS: " ++ show (map fst newargs_all) ++ " " ++ showTmImpls rhs

657+ logElab 2 $ "RHS: " ++ show (map fst newargs_all) ++ " " ++ showTmImpls rhs

658658 ctxt <- getContext -- new context with where block added

659− logLvl 5 "STARTING CHECK"

659+ logElab 5 "STARTING CHECK"

660660 ((rhs', defer, is, probs, ctxt', newDecls, highlights), _) <-

661661 tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "patRHS") clhsty initEState

662662 (do pbinds ist lhs_tm

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

671671 (erun fc $ psolve lhs_tm)

672672 tt <- get_term

673673 aux <- getAux

674− let (tm, ds) = runState (collectDeferred (Just fname)

674+ let (tm, ds) = runState (collectDeferred (Just fname)

675675 (map fst $ case_decls aux) ctxt tt) []

676676 probs <- get_probs

677677 return (tm, ds, is, probs, ctxt', newDecls, highlights))

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

681681

682682 when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_,_) -> (x,y)) probs)

683683

684− logLvl 5 "DONE CHECK"

685− logLvl 4 $ "---> " ++ show rhs'

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

684+ logElab 5 "DONE CHECK"

685+ logElab 4 $ "---> " ++ show rhs'

686+ when (not (null defer)) $ logElab 1 $ "DEFERRED " ++

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

688688 def' <- checkDef fc (\n -> Elaborating "deferred type of " n Nothing) defer

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

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

700700 mapM_ (elabCaseBlock winfo opts) is

701701

702702 ctxt <- getContext

703− logLvl 5 $ "Rechecking"

704− logLvl 6 $ " ==> " ++ show (forget rhs')

703+ logElab 5 $ "Rechecking"

704+ logElab 6 $ " ==> " ++ show (forget rhs')

705705

706706 (crhs, crhsty) <- if not inf

707707 then recheckC_borrowing True (PEGenerated `notElem` opts)

708708 borrowed fc id [] rhs'

709709 else return (rhs', clhsty)

710− logLvl 6 $ " ==> " ++ showEnvDbg [] crhsty ++ " against " ++ showEnvDbg [] clhsty

710+ logElab 6 $ " ==> " ++ showEnvDbg [] crhsty ++ " against " ++ showEnvDbg [] clhsty

711711 ctxt <- getContext

712712 let constv = next_tvar ctxt

713713 case LState.runStateT (convertsC ctxt [] crhsty clhsty) (constv, []) of

714714 OK (_, cs) -> when (PEGenerated `notElem` opts) $ do

715− addConstraints fc cs

716− logLvl 6 $ "CONSTRAINTS ADDED: " ++ show cs ++ "\n" ++ show (clhsty, crhsty)

715+ addConstraints fc cs

716+ logElab 6 $ "CONSTRAINTS ADDED: " ++ show cs ++ "\n" ++ show (clhsty, crhsty)

717717 return ()

718718 Error e -> ierror (At fc (CantUnify False (clhsty, Nothing) (crhsty, Nothing) e [] 0))

719719 i <- getIState

@@ -805,14 +805,14 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

805805 [t] -> t

806806 _ -> []

807807 let params = getParamsInType i [] fn_is (normalise ctxt [] fn_ty)

808− let lhs = stripLinear i $ stripUnmatchable i $

809− propagateParams i params fn_ty (allNamesIn lhs_in)

808+ let lhs = stripLinear i $ stripUnmatchable i $

809+ propagateParams i params fn_ty (allNamesIn lhs_in)

810810 (addImplPat i lhs_in)

811− logLvl 2 ("LHS: " ++ show lhs)

811+ logElab 2 ("LHS: " ++ show lhs)

812812 (ElabResult lhs' dlhs [] ctxt' newDecls highlights, _) <-

813813 tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "patLHS") infP initEState

814814 (errAt "left hand side of with in " fname Nothing

815− (erun fc (buildTC i info ELHS opts fname

815+ (erun fc (buildTC i info ELHS opts fname

816816 (allNamesIn lhs_in)

817817 (infTerm lhs))) )

818818 setContext ctxt'

@@ -823,12 +823,12 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

823823 let lhs_ty = getInferType lhs'

824824 let ret_ty = getRetTy (explicitNames (normalise ctxt [] lhs_ty))

825825 let static_names = getStaticNames i lhs_tm

826− logLvl 5 (show lhs_tm ++ "\n" ++ show static_names)

826+ logElab 5 (show lhs_tm ++ "\n" ++ show static_names)

827827 (clhs, clhsty) <- recheckC fc id [] lhs_tm

828− logLvl 5 ("Checked " ++ show clhs)

828+ logElab 5 ("Checked " ++ show clhs)

829829 let bargs = getPBtys (explicitNames (normalise ctxt [] lhs_tm))

830830 let wval = addImplBound i (map fst bargs) wval_in

831− logLvl 5 ("Checking " ++ showTmImpls wval)

831+ logElab 5 ("Checking " ++ showTmImpls wval)

832832 -- Elaborate wval in this context

833833 ((wval', defer, is, ctxt', newDecls, highlights), _) <-

834834 tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "withRHS")

@@ -851,11 +851,11 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

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

852852 addDeferred def''

853853 mapM_ (elabCaseBlock info opts) is

854− logLvl 5 ("Checked wval " ++ show wval')

854+ logElab 5 ("Checked wval " ++ show wval')

855855 (cwval, cwvalty) <- recheckC fc id [] (getInferTerm wval')

856856 let cwvaltyN = explicitNames (normalise ctxt [] cwvalty)

857857 let cwvalN = explicitNames (normalise ctxt [] cwval)

858− logLvl 3 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)

858+ logElab 3 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)

859859 -- We're going to assume the with type is not a function shortly,

860860 -- so report an error if it is (you can't match on a function anyway

861861 -- so this doesn't lose anything)

@@ -876,9 +876,9 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

876876 -- Highlight explicit proofs

877877 sendHighlighting $ [(fc, AnnBoundName n False) | (n, fc) <- maybeToList pn_in]

878878

879− logLvl 10 ("With type " ++ show (getRetTy cwvaltyN) ++

879+ logElab 10 ("With type " ++ show (getRetTy cwvaltyN) ++

880880 " depends on " ++ show pdeps ++ " from " ++ show pvars)

881− logLvl 10 ("Pre " ++ show bargs_pre ++ "\nPost " ++ show bargs_post)

881+ logElab 10 ("Pre " ++ show bargs_pre ++ "\nPost " ++ show bargs_post)

882882 windex <- getName

883883 -- build a type declaration for the new function:

884884 -- (ps : Xs) -> (withval : cwvalty) -> (ps' : Xs') -> ret_ty

@@ -886,7 +886,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

886886 let wargtype = getRetTy cwvaltyN

887887 let wargname = sMN windex "warg"

888888

889− logLvl 5 ("Abstract over " ++ show wargval ++ " in " ++ show wargtype)

889+ logElab 5 ("Abstract over " ++ show wargval ++ " in " ++ show wargtype)

890890 let wtype = bindTyArgs (flip (Pi Nothing) (TType (UVar 0))) (bargs_pre ++

891891 (wargname, wargtype) :

892892 map (abstract wargname wargval wargtype) bargs_post ++

@@ -896,13 +896,13 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

896896 P Bound wargname Erased, wargval])]

897897 Nothing -> [])

898898 (substTerm wargval (P Bound wargname wargtype) ret_ty)

899− logLvl 3 ("New function type " ++ show wtype)

899+ logElab 3 ("New function type " ++ show wtype)

900900 let wname = SN (WithN windex fname)

901901

902902 let imps = getImps wtype -- add to implicits context

903903 putIState (i { idris_implicits = addDef wname imps (idris_implicits i) })

904904 let statics = getStatics static_names wtype

905− logLvl 5 ("Static positions " ++ show statics)

905+ logElab 5 ("Static positions " ++ show statics)

906906 i <- getIState

907907 putIState (i { idris_statics = addDef wname statics (idris_statics i) })

908908

@@ -919,7 +919,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

919919 -- ==> fname' ps wpat [rest], match pats against toplevel for ps

920920 wb <- mapM (mkAuxC mpn wname lhs (map fst bargs_pre) (map fst bargs_post))

921921 withblock

922− logLvl 3 ("with block " ++ show wb)

922+ logElab 3 ("with block " ++ show wb)

923923 -- propagate totality assertion to the new definitions

924924 when (AssertTotal `elem` opts) $ setFlags wname [AssertTotal]

925925 mapM_ (rec_elabDecl info EAll info) wb

@@ -935,7 +935,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

935935 [ pimp (sUN "A") Placeholder False

936936 , pimp (sUN "x") Placeholder False

937937 ])])

938− logLvl 5 ("New RHS " ++ showTmImpls rhs)

938+ logElab 5 ("New RHS " ++ showTmImpls rhs)

939939 ctxt <- getContext -- New context with block added

940940 i <- getIState

941941 ((rhs', defer, is, ctxt', newDecls, highlights), _) <-

@@ -955,7 +955,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

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

956956 addDeferred def''

957957 mapM_ (elabCaseBlock info opts) is

958− logLvl 5 ("Checked RHS " ++ show rhs')

958+ logElab 5 ("Checked RHS " ++ show rhs')

959959 (crhs, crhsty) <- recheckC fc id [] rhs'

960960 return $ (Right (clhs, crhs), lhs)

961961 where

@@ -971,18 +971,18 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

971971 mkAux pn wname toplhs ns ns' (PClause fc n tm_in (w:ws) rhs wheres)

972972 = do i <- getIState

973973 let tm = addImplPat i tm_in

974− logLvl 2 ("Matching " ++ showTmImpls tm ++ " against " ++

974+ logElab 2 ("Matching " ++ showTmImpls tm ++ " against " ++

975975 showTmImpls toplhs)

976976 case matchClause i toplhs tm of

977977 Left (a,b) -> ifail $ show fc ++ ":with clause does not match top level"

978978 Right mvars ->

979− do logLvl 3 ("Match vars : " ++ show mvars)

979+ do logElab 3 ("Match vars : " ++ show mvars)

980980 lhs <- updateLHS n pn wname mvars ns ns' (fullApp tm) w

981981 return $ PClause fc wname lhs ws rhs wheres

982982 mkAux pn wname toplhs ns ns' (PWith fc n tm_in (w:ws) wval pn' withs)

983983 = do i <- getIState

984984 let tm = addImplPat i tm_in

985− logLvl 2 ("Matching " ++ showTmImpls tm ++ " against " ++

985+ logElab 2 ("Matching " ++ showTmImpls tm ++ " against " ++

986986 showTmImpls toplhs)

987987 withs' <- mapM (mkAuxC pn wname toplhs ns ns') withs

988988 case matchClause i toplhs tm of

@@ -1001,7 +1001,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

10011001 ns' = map (keepMvar (map fst mvars) fc') ns_in' in

10021002 return $ substMatches mvars $

10031003 PApp fc (PRef fc' [] wname)

1004− (map pexp ns ++ pexp w : (map pexp ns') ++

1004+ (map pexp ns ++ pexp w : (map pexp ns') ++

10051005 case pn of

10061006 Nothing -> []

10071007 Just pnm -> [pexp (PRef fc [] pnm)])

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

@@ -51,14 +51,14 @@ import Data.List.Split (splitOn)

5151import Util.Pretty

5252

5353warnLC :: FC -> Name -> Idris ()

54−warnLC fc n

54+warnLC fc n

5555 = iWarn fc $ annName n <+> text "has a name which may be implicitly bound."

5656 <> line <> text "This is likely to lead to problems!"

5757

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

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

6060 = do let codata = Codata `elem` opts

61− logLvl 1 (show (fc, doc))

61+ logElab 1 (show (fc, doc))

6262 checkUndefined fc n

6363 when (implicitable n) $ warnLC fc n

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

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

6969

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

7171 = do let codata = Codata `elem` opts

72− logLvl 1 (show fc)

72+ logElab 1 (show fc)

7373 undef <- isUndefined fc n

7474 when (implicitable n) $ warnLC fc n

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

@@ -91,7 +91,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n nfc t_in dcons)

9191 i <- getIState

9292 let as = map (const (Left (Msg ""))) (getArgTys cty)

9393 let params = findParams (map snd cons)

94− logLvl 2 $ "Parameters : " ++ show params

94+ logElab 2 $ "Parameters : " ++ show params

9595 -- TI contains information about mutually declared types - this will

9696 -- be updated when the mutual block is complete

9797 putIState (i { idris_datatypes =

@@ -232,7 +232,7 @@ elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->

232232elabCon info syn tn codata expkind dkind (doc, argDocs, n, nfc, t_in, fc, forcenames)

233233 = do checkUndefined fc n

234234 when (implicitable n) $ warnLC fc n

235− logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t_in

235+ logElab 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t_in

236236 (cty, ckind, t, inacc) <- buildType info syn fc [Constructor] n (if codata then mkLazy t_in else t_in)

237237 ctxt <- getContext

238238 let cty' = normalise ctxt [] cty

@@ -242,13 +242,13 @@ elabCon info syn tn codata expkind dkind (doc, argDocs, n, nfc, t_in, fc, forcen

242242 -- Check that the constructor type is, in fact, a part of the family being defined

243243 tyIs n cty'

244244

245− logLvl 5 $ show fc ++ ":Constructor " ++ show n ++ " elaborated : " ++ show t

246− logLvl 5 $ "Inaccessible args: " ++ show inacc

247− logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty'

245+ logElab 5 $ show fc ++ ":Constructor " ++ show n ++ " elaborated : " ++ show t

246+ logElab 5 $ "Inaccessible args: " ++ show inacc

247+ logElab 2 $ "---> " ++ show n ++ " : " ++ show cty'

248248

249249 -- Add to the context (this is temporary, so that later constructors

250250 -- can be indexed by it)

251− updateContext (addTyDecl n (DCon 0 0 False) cty)

251+ updateContext (addTyDecl n (DCon 0 0 False) cty)

252252

253253 addIBC (IBCDef n)

254254 checkDocs fc argDocs t

@@ -298,12 +298,12 @@ elabCon info syn tn codata expkind dkind (doc, argDocs, n, nfc, t_in, fc, forcen

298298 = tclift $ tfail (At fc (UniqueKindError UniqueType n))

299299 checkUniqueKind (UType AllTypes) (UType AllTypes) = return ()

300300 checkUniqueKind (UType AllTypes) (UType UniqueType) = return ()

301− checkUniqueKind (UType AllTypes) _

301+ checkUniqueKind (UType AllTypes) _

302302 = tclift $ tfail (At fc (UniqueKindError AllTypes n))

303303 checkUniqueKind _ _ = return ()

304304

305305 -- Constructor's kind must be <= expected kind

306− addDataConstraint (TType con) (TType exp)

306+ addDataConstraint (TType con) (TType exp)

307307 = do ctxt <- getContext

308308 let v = next_tvar ctxt

309309 addConstraints fc (v, [ULT con exp])

@@ -354,7 +354,7 @@ elabCaseFun ind paramPos n ty cons info = do

354354 _ -> State.lift $ idrisCatch (rec_elabDecl info EAll info eliminatorDef)

355355 (ierror . Elaborating "clauses of " elimDeclName Nothing)

356356 where elimLog :: String -> EliminatorState ()

357− elimLog s = State.lift (logLvl 2 s)

357+ elimLog s = State.lift (logElab 2 s)

358358

359359 elimFC :: FC

360360 elimFC = fileFC "(casefun)"

src/Idris/Elab/Instance.hs+14−15

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

7171 let constraint = PApp fc (PRef fc [] n) (map pexp ps)

7272 let iname = mkiname n (namespace info) ps expn

7373 let emptyclass = null (class_methods ci)

74− when (what /= EDefns) $ do

74+ when (what /= EDefns) $ do

7575 nty <- elabType' True info syn doc argDocs fc [] iname NoFC t

7676 -- if the instance type matches any of the instances we have already,

7777 -- and it's not a named instance, then it's overlapping, so report an error

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

106106 (decorate ns iname n,

107107 op, coninsert cs t', t'))

108108 (class_methods ci)

109− logLvl 3 (show (mtys, ips))

110− logLvl 5 ("Before defaults: " ++ show ds ++ "\n" ++ show (map fst (class_methods ci)))

109+ logElab 3 (show (mtys, ips))

110+ logElab 5 ("Before defaults: " ++ show ds ++ "\n" ++ show (map fst (class_methods ci)))

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

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

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

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

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

114+ logElab 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

118118 let wbVals = map (decorateid (decorate ns iname)) ds'

119119 let wb = wbTys ++ wbVals

120− logLvl 3 $ "Method types " ++ showSep "\n" (map (show . showDeclImp verbosePPOption . mkTyDecl) mtys)

121− logLvl 3 $ "Instance is " ++ show ps ++ " implicits " ++

120+ logElab 3 $ "Method types " ++ showSep "\n" (map (show . showDeclImp verbosePPOption . mkTyDecl) mtys)

121+ logElab 3 $ "Instance is " ++ show ps ++ " implicits " ++

122122 show (concat (nub wparams))

123123

124124 -- Bring variables in instance head into scope

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

134134 let rhs = PApp fc (PRef fc [] (instanceCtorName ci))

135135 (map (pexp . mkMethApp) mtys)

136136

137− logLvl 5 $ "Instance LHS " ++ show lhs ++ " " ++ show headVars

138− logLvl 5 $ "Instance RHS " ++ show rhs

137+ logElab 5 $ "Instance LHS " ++ show lhs ++ " " ++ show headVars

138+ logElab 5 $ "Instance RHS " ++ show rhs

139139

140140 let idecls = [PClauses fc [Dictionary] iname

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

142− logLvl 1 (show idecls)

142+ logElab 1 (show idecls)

143143 push_estack iname True

144144 mapM_ (rec_elabDecl info EAll info) idecls

145145 pop_estack

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

267267 reorderDefs :: [Name] -> [PDecl] -> [PDecl]

268268 reorderDefs ns [] = []

269269 reorderDefs [] ds = ds

270− reorderDefs (n : ns) ds = case pick n [] ds of

270+ reorderDefs (n : ns) ds = case pick n [] ds of

271271 Just (def, ds') -> def : reorderDefs ns ds'

272272 Nothing -> reorderDefs ns ds

273273

274− pick n acc [] = Nothing

274+ pick n acc [] = Nothing

275275 pick n acc (def@(PClauses _ _ cn cs) : ds)

276276 | nsroot n == nsroot cn = Just (def, acc ++ ds)

277277 pick n acc (d : ds) = pick n (acc ++ [d]) ds

@@ -313,13 +313,13 @@ checkInjectiveArgs fc n ds (Just ty)

313313 let (_, args) = unApply (instantiateRetTy ty)

314314 ci 0 ist args

315315 where

316− ci i ist (a : as) | i `elem` ds

316+ ci i ist (a : as) | i `elem` ds

317317 = if isInj ist a then ci (i + 1) ist as

318318 else tclift $ tfail (At fc (InvalidTCArg n a))

319319 ci i ist (a : as) = ci (i + 1) ist as

320320 ci i ist [] = return ()

321321

322− isInj i (P Bound n _) = True

322+ isInj i (P Bound n _) = True

323323 isInj i (P _ n _) = isConName n (tt_ctxt i)

324324 isInj i (App _ f a) = isInj i f && isInj i a

325325 isInj i (V _) = True

@@ -329,4 +329,3 @@ checkInjectiveArgs fc n ds (Just ty)

329329 instantiateRetTy (Bind n (Pi _ _ _) sc)

330330 = substV (P Bound n Erased) (instantiateRetTy sc)

331331 instantiateRetTy t = t

332−

src/Idris/Elab/Provider.hs+3−3

@@ -84,7 +84,7 @@ elabProvider doc info syn fc nfc what n

8484 rhs <- execute (mkApp (P Ref (sUN "run__provider") Erased)

8585 [Erased, e])

8686 let rhs' = normalise ctxt [] rhs

87− logLvl 3 $ "Normalised " ++ show n ++ "'s RHS to " ++ show rhs

87+ logElab 3 $ "Normalised " ++ show n ++ "'s RHS to " ++ show rhs

8888

8989 -- Extract the provided term or postulate from the type provider

9090 provided <- getProvided fc rhs'

@@ -95,11 +95,11 @@ elabProvider doc info syn fc nfc what n

9595 do -- Finally add a top-level definition of the provided term

9696 elabType info syn doc [] fc [] n NoFC ty

9797 elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc [] n) []) [] (delab i tm) []]

98− logLvl 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm

98+ logElab 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm

9999 | ProvPostulate _ <- what ->

100100 do -- Add the postulate

101101 elabPostulate info syn doc fc nfc [] n (delab i tm)

102− logLvl 3 $ "Elaborated provided postulate " ++ show n

102+ logElab 3 $ "Elaborated provided postulate " ++ show n

103103 | otherwise ->

104104 ierror . Msg $ "Attempted to provide a postulate where a term was expected."

105105

src/Idris/Elab/Record.hs+35−36

@@ -47,18 +47,18 @@ elabRecord :: ElabInfo

4747 -> SyntaxInfo -- ^ Constructor SyntaxInfo

4848 -> Idris ()

4949elabRecord info what doc rsyn fc opts tyn nfc params paramDocs fields cname cdoc csyn

50− = do logLvl 1 $ "Building data declaration for " ++ show tyn

50+ = do logElab 1 $ "Building data declaration for " ++ show tyn

5151 -- Type constructor

5252 let tycon = generateTyConType params

53− logLvl 1 $ "Type constructor " ++ showTmImpls tycon

54−

53+ logElab 1 $ "Type constructor " ++ showTmImpls tycon

54+

5555 -- Data constructor

5656 dconName <- generateDConName (fmap fst cname)

5757 let dconTy = generateDConType params fieldsWithNameAndDoc

58− logLvl 1 $ "Data constructor: " ++ showTmImpls dconTy

58+ logElab 1 $ "Data constructor: " ++ showTmImpls dconTy

5959

6060 -- Build data declaration for elaboration

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

61+ logElab 1 $ foldr (++) "" $ intersperse "\n" (map show dconsArgDocs)

6262 let datadecl = case what of

6363 ETypes -> PLaterdecl tyn NoFC tycon

6464 _ -> PDatadecl tyn NoFC tycon [(cdoc, dconsArgDocs, dconName, NoFC, dconTy, fc, [])]

@@ -71,8 +71,8 @@ elabRecord info what doc rsyn fc opts tyn nfc params paramDocs fields cname cdoc

7171 addIBC (IBCRecord tyn)

7272

7373 when (what /= ETypes) $ do

74− logLvl 1 $ "fieldsWithName " ++ show fieldsWithName

75− logLvl 1 $ "fieldsWIthNameAndDoc " ++ show fieldsWithNameAndDoc

74+ logElab 1 $ "fieldsWithName " ++ show fieldsWithName

75+ logElab 1 $ "fieldsWIthNameAndDoc " ++ show fieldsWithNameAndDoc

7676 elabRecordFunctions info rsyn fc tyn paramsAndDoc fieldsWithNameAndDoc dconName target

7777

7878 sendHighlighting $

@@ -162,10 +162,10 @@ elabRecordFunctions :: ElabInfo -> SyntaxInfo -> FC

162162 -> PTerm -- ^ Target type

163163 -> Idris ()

164164elabRecordFunctions info rsyn fc tyn params fields dconName target

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

165+ = do logElab 1 $ "Elaborating helper functions for record " ++ show tyn

166166

167− logLvl 1 $ "Fields: " ++ show fieldNames

168− logLvl 1 $ "Params: " ++ show paramNames

167+ logElab 1 $ "Fields: " ++ show fieldNames

168+ logElab 1 $ "Params: " ++ show paramNames

169169 -- The elaborated constructor type for the data declaration

170170 i <- getIState

171171 ttConsTy <-

@@ -175,11 +175,11 @@ elabRecordFunctions info rsyn fc tyn params fields dconName target

175175

176176 -- The arguments to the constructor

177177 let constructorArgs = getArgTys ttConsTy

178− logLvl 1 $ "Cons args: " ++ show constructorArgs

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

178+ logElab 1 $ "Cons args: " ++ show constructorArgs

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

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

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

182−

182+

183183 -- The parameters for elaboration with their documentation

184184 -- Parameter functions are all prefixed with "param_".

185185 let paramsForElab = [((nsroot n), (paramName n), impl, t, d) | (n, _, _, t, d) <- params] -- zipParams i params paramDocs]

@@ -187,14 +187,14 @@ elabRecordFunctions info rsyn fc tyn params fields dconName target

187187 -- The fields (written by the user) with their documentation.

188188 let userFieldsForElab = [((nsroot n), n, p, t, d) | (n, nfc, p, t, d) <- fields]

189189

190− -- All things we need to elaborate projection functions for, together with a number denoting their position in the constructor.

191− let projectors = [(n, n', p, t, d, i) | ((n, n', p, t, d), i) <- zip (freeFieldsForElab ++ paramsForElab ++ userFieldsForElab) [0..]]

190+ -- All things we need to elaborate projection functions for, together with a number denoting their position in the constructor.

191+ let projectors = [(n, n', p, t, d, i) | ((n, n', p, t, d), i) <- zip (freeFieldsForElab ++ paramsForElab ++ userFieldsForElab) [0..]]

192192 -- Build and elaborate projection functions

193193 elabProj dconName projectors

194194

195− logLvl 1 $ "Dependencies: " ++ show fieldDependencies

195+ logElab 1 $ "Dependencies: " ++ show fieldDependencies

196196

197− logLvl 1 $ "Depended on: " ++ show dependedOn

197+ logElab 1 $ "Depended on: " ++ show dependedOn

198198

199199 -- All things we need to elaborate update functions for, together with a number denoting their position in the constructor.

200200 let updaters = [(n, n', p, t, d, i) | ((n, n', p, t, d), i) <- zip (paramsForElab ++ userFieldsForElab) [0..]]

@@ -237,7 +237,7 @@ elabRecordFunctions info rsyn fc tyn params fields dconName target

237237 plicity = impl -- All free fields are implicit as they are machine generated

238238 fieldType = delab i (snd arg) -- The type of the field

239239 doc = emptyDocstring -- No docmentation for machine generated fields

240− in (nameInCons, nameFree, plicity, fieldType, doc)

240+ in (nameInCons, nameFree, plicity, fieldType, doc)

241241

242242 freeName :: Name -> Name

243243 freeName (UN n) = sUN ("free_" ++ str n)

@@ -278,7 +278,7 @@ elabRecordFunctions info rsyn fc tyn params fields dconName target

278278 -- | Decides whether a setter should be generated for a field or not.

279279 optionalSetter :: Name -> Bool

280280 optionalSetter n = n `elem` dependedOn

281−

281+

282282 -- | A map from a field name to the other fields it depends on.

283283 fieldDependencies :: [(Name, [Name])]

284284 fieldDependencies = map (uncurry fieldDep) [(n, t) | (n, _, _, t, _) <- fields ++ params]

@@ -314,15 +314,15 @@ elabProjection :: ElabInfo

314314 -> Int -- ^ Argument Index

315315 -> Idris ()

316316elabProjection info cname pname plicity projTy pdoc psyn fc targetTy cn phArgs fnames index

317− = do logLvl 1 $ "Generating Projection for " ++ show pname

318−

317+ = do logElab 1 $ "Generating Projection for " ++ show pname

318+

319319 let ty = generateTy

320− logLvl 1 $ "Type of " ++ show pname ++ ": " ++ show ty

321−

320+ logElab 1 $ "Type of " ++ show pname ++ ": " ++ show ty

321+

322322 let lhs = generateLhs

323− logLvl 1 $ "LHS of " ++ show pname ++ ": " ++ showTmImpls lhs

323+ logElab 1 $ "LHS of " ++ show pname ++ ": " ++ showTmImpls lhs

324324 let rhs = generateRhs

325− logLvl 1 $ "RHS of " ++ show pname ++ ": " ++ showTmImpls rhs

325+ logElab 1 $ "RHS of " ++ show pname ++ ": " ++ showTmImpls rhs

326326

327327 rec_elabDecl info EAll info ty

328328

@@ -372,24 +372,24 @@ elabUpdate :: ElabInfo

372372 -> Bool -- ^ Optional

373373 -> Idris ()

374374elabUpdate info cname pname plicity pty pdoc psyn fc sty cn args fnames i optional

375− = do logLvl 1 $ "Generating Update for " ++ show pname

376−

375+ = do logElab 1 $ "Generating Update for " ++ show pname

376+

377377 let ty = generateTy

378− logLvl 1 $ "Type of " ++ show set_pname ++ ": " ++ show ty

379−

378+ logElab 1 $ "Type of " ++ show set_pname ++ ": " ++ show ty

379+

380380 let lhs = generateLhs

381− logLvl 1 $ "LHS of " ++ show set_pname ++ ": " ++ showTmImpls lhs

382−

381+ logElab 1 $ "LHS of " ++ show set_pname ++ ": " ++ showTmImpls lhs

382+

383383 let rhs = generateRhs

384− logLvl 1 $ "RHS of " ++ show set_pname ++ ": " ++ showTmImpls rhs

384+ logElab 1 $ "RHS of " ++ show set_pname ++ ": " ++ showTmImpls rhs

385385

386− let clause = PClause fc set_pname lhs [] rhs []

386+ let clause = PClause fc set_pname lhs [] rhs []

387387

388388 idrisCatch (do rec_elabDecl info EAll info ty

389389 rec_elabDecl info EAll info $ PClauses fc [] set_pname [clause])

390− (\err -> logLvl 1 $ "Could not generate update function for " ++ show pname)

390+ (\err -> logElab 1 $ "Could not generate update function for " ++ show pname)

391391 {-if optional

392− then logLvl 1 $ "Could not generate update function for " ++ show pname

392+ then logElab 1 $ "Could not generate update function for " ++ show pname

393393 else tclift $ tfail $ At fc (Elaborating "record update function " pname err)) -}

394394 where

395395 -- | The type of the update function.

@@ -463,4 +463,3 @@ projectInType xs = mapPT st

463463-- | Creates an PArg from a plicity and a name where the term is a PRef.

464464asPRefArg :: Plicity -> Name -> PArg

465465asPRefArg p n = asArg p (nsroot n) $ PRef emptyFC [] (nsroot n)

466−

src/Idris/Elab/Term.hs+66−66

@@ -91,7 +91,7 @@ build ist info emode opts fn tm

9191 g <- goal

9292 ptm <- get_term

9393 resolveTC' True True 10 g fn ist) ivs

94−

94+

9595 when (not pattern) $ solveAutos ist fn False

9696

9797 tm <- get_term

@@ -138,7 +138,7 @@ build ist info emode opts fn tm

138138-- (Separate, so we don't go overboard resolving things that we don't

139139-- know about yet on the LHS of a pattern def)

140140

141−buildTC :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name ->

141+buildTC :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name ->

142142 [Name] -> -- Cached names in the PTerm, before adding PAlternatives

143143 PTerm ->

144144 ElabD ElabResult

@@ -147,7 +147,7 @@ buildTC ist info emode opts fn ns tm

147147 let inf = case lookupCtxt fn (idris_tyinfodata ist) of

148148 [TIPartial] -> True

149149 _ -> False

150− -- set name supply to begin after highest index in tm

150+ -- set name supply to begin after highest index in tm

151151 initNextNameFrom ns

152152 elab ist info emode opts fn tm

153153 probs <- get_probs

@@ -171,7 +171,7 @@ buildTC ist info emode opts fn ns tm

171171 else return (ElabResult tm ds (map snd is) ctxt impls highlights)

172172 where pattern = emode == ELHS

173173

174−-- return whether arguments of the given constructor name can be

174+-- return whether arguments of the given constructor name can be

175175-- matched on. If they're polymorphic, no, unless the type has beed made

176176-- concrete by the time we get around to elaborating the argument.

177177getUnmatchable :: Context -> Name -> [Bool]

@@ -180,11 +180,11 @@ getUnmatchable ctxt n | isDConName n ctxt && n /= inferCon

180180 Nothing -> []

181181 Just ty -> checkArgs [] [] ty

182182 where checkArgs :: [Name] -> [[Name]] -> Type -> [Bool]

183− checkArgs env ns (Bind n (Pi _ t _) sc)

183+ checkArgs env ns (Bind n (Pi _ t _) sc)

184184 = let env' = case t of

185185 TType _ -> n : env

186186 _ -> env in

187− checkArgs env' (intersect env (refsIn t) : ns)

187+ checkArgs env' (intersect env (refsIn t) : ns)

188188 (instantiate (P Bound n t) sc)

189189 checkArgs env ns t

190190 = map (not . null) (reverse ns)

@@ -193,7 +193,7 @@ getUnmatchable ctxt n = []

193193

194194data ElabCtxt = ElabCtxt { e_inarg :: Bool,

195195 e_isfn :: Bool, -- ^ Function part of application

196− e_guarded :: Bool,

196+ e_guarded :: Bool,

197197 e_intype :: Bool,

198198 e_qq :: Bool,

199199 e_nomatching :: Bool -- ^ can't pattern match

@@ -267,17 +267,17 @@ elab ist info emode opts fn tm

267267 -- normally correct to call elabE - the ones that don't are desugarings

268268 -- typically

269269 elabE :: ElabCtxt -> Maybe FC -> PTerm -> ElabD ()

270− elabE ina fc' t =

270+ elabE ina fc' t =

271271 do solved <- get_recents

272272 as <- get_autos

273273 hs <- get_holes

274274 -- If any of the autos use variables which have recently been solved,

275275 -- have another go at solving them now.

276− mapM_ (\(a, (failc, ns)) ->

276+ mapM_ (\(a, (failc, ns)) ->

277277 if any (\n -> n `elem` solved) ns && head hs /= a

278278 then solveAuto ist fn False (a, failc)

279279 else return ()) as

280−

280+

281281 itm <- if not pattern then insertImpLam ina t else return t

282282 ct <- insertCoerce ina itm

283283 t' <- insertLazy ct

@@ -343,7 +343,7 @@ elab ist info emode opts fn tm

343343-- elab' (_,_,inty) (PConstant c)

344344-- | constType c && pattern && not reflection && not inty

345345-- = lift $ tfail (Msg "Typecase is not allowed")

346− elab' ina fc tm@(PConstant fc' c)

346+ elab' ina fc tm@(PConstant fc' c)

347347 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)

348348 && isTypeConst c

349349 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)

@@ -397,7 +397,7 @@ elab ist info emode opts fn tm

397397 UType _ -> elab' ina (Just fc) (PApp fc (PRef fc hls upairTy)

398398 [pexp l,pexp r])

399399 _ -> case tc of

400− P _ n _ | n == upairTy

400+ P _ n _ | n == upairTy

401401 -> elab' ina (Just fc) (PApp fc (PRef fc hls upairCon)

402402 [pimp (sUN "A") Placeholder False,

403403 pimp (sUN "B") Placeholder False,

@@ -509,7 +509,7 @@ elab ist info emode opts fn tm

509509 ty <- goal

510510 let doelab = elab' ina fc orig

511511 tryCatch doelab

512− (\err ->

512+ (\err ->

513513 if recoverableErr err

514514 then -- trace ("NEED IMPLICIT! " ++ show orig ++ "\n" ++

515515 -- show alts ++ "\n" ++

@@ -547,7 +547,7 @@ elab ist info emode opts fn tm

547547 pruneAlts err alts _ = filter isLend alts

548548

549549 hasArg n env ap | isLend ap = True -- special case hack for 'Borrowed'

550− hasArg n env (PApp _ (PRef _ _ a) _)

550+ hasArg n env (PApp _ (PRef _ _ a) _)

551551 = case lookupTyExact a (tt_ctxt ist) of

552552 Just ty -> let args = map snd (getArgTys (normalise (tt_ctxt ist) env ty)) in

553553 any (fnIs n) args

@@ -662,7 +662,7 @@ elab ist info emode opts fn tm

662662 introTy (Var tyn) (Just n)

663663 addPSname n -- okay for proof search

664664 focus tyn

665−

665+

666666 elabE (ec { e_inarg = True, e_intype = True }) (Just fc) ty

667667 elabE (ec { e_inarg = True }) (Just fc) sc

668668 solve

@@ -701,10 +701,10 @@ elab ist info emode opts fn tm

701701 Placeholder -> return ()

702702 _ -> do focus tyn

703703 explicit tyn

704− elabE (ina { e_inarg = True, e_intype = True })

704+ elabE (ina { e_inarg = True, e_intype = True })

705705 (Just fc) ty

706706 focus valn

707− elabE (ina { e_inarg = True, e_intype = True })

707+ elabE (ina { e_inarg = True, e_intype = True })

708708 (Just fc) val

709709 ivs' <- get_instances

710710 env <- get_env

@@ -808,14 +808,14 @@ elab ist info emode opts fn tm

808808 annot <- findHighlight f

809809 mapM_ checkKnownImplicit args_in

810810 let args = insertScopedImps fc (normalise ctxt env fty) args_in

811− let unmatchableArgs = if pattern

811+ let unmatchableArgs = if pattern

812812 then getUnmatchable (tt_ctxt ist) f

813813 else []

814−-- trace ("BEFORE " ++ show f ++ ": " ++ show ty) $

814+-- trace ("BEFORE " ++ show f ++ ": " ++ show ty) $

815815 when (pattern && not reflection && not (e_qq ina) && not (e_intype ina)

816816 && isTConName f (tt_ctxt ist)) $

817817 lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)

818−-- trace (show (f, args_in, args)) $

818+-- trace (show (f, args_in, args)) $

819819 if (f `elem` map fst env && length args == 1 && length args_in == 1)

820820 then -- simple app, as below

821821 do simple_app False

@@ -853,7 +853,7 @@ elab ist info emode opts fn tm

853853 mapM (uncurry highlightSource) $

854854 (ffc, annot) : map (\f -> (f, annot)) hls

855855

856− elabArgs ist (ina { e_inarg = e_inarg ina || not isinf })

856+ elabArgs ist (ina { e_inarg = e_inarg ina || not isinf })

857857 [] fc False f

858858 (zip ns (unmatchableArgs ++ repeat False))

859859 (f == sUN "Force")

@@ -880,7 +880,7 @@ elab ist info emode opts fn tm

880880 ivs' <- get_instances

881881 -- Attempt to resolve any type classes which have 'complete' types,

882882 -- i.e. no holes in them

883− when (not pattern || (e_inarg ina && not tcgen &&

883+ when (not pattern || (e_inarg ina && not tcgen &&

884884 not (e_guarded ina))) $

885885 mapM_ (\n -> do focus n

886886 g <- goal

@@ -893,14 +893,14 @@ elab ist info emode opts fn tm

893893 else movelast n)

894894 (ivs' \\ ivs)

895895 return []

896− where

896+ where

897897 -- Run the elaborator, which returns how many implicit

898898 -- args were needed, then run it again with those args. We need

899899 -- this because we have to elaborate the whole application to

900900 -- find out whether any computations have caused more implicits

901901 -- to be needed.

902902 implicitApp :: ElabD [ImplicitInfo] -> ElabD ()

903− implicitApp elab

903+ implicitApp elab

904904 | pattern || intransform = do elab; return ()

905905 | otherwise

906906 = do s <- get

@@ -909,7 +909,7 @@ elab ist info emode opts fn tm

909909 [] -> return ()

910910 es -> do put s

911911 elab' ina topfc (PAppImpl tm es)

912−

912+

913913 checkKnownImplicit imp

914914 | UnknownImp `elem` argopts imp

915915 = lift $ tfail $ UnknownImplicit (pname imp) f

@@ -966,7 +966,7 @@ elab ist info emode opts fn tm

966966 headRef (PAlternative _ _ as) = all headRef as

967967 headRef _ = False

968968

969− elab' ina fc (PAppImpl f es) = do appImpl (reverse es) -- not that we look...

969+ elab' ina fc (PAppImpl f es) = do appImpl (reverse es) -- not that we look...

970970 solve

971971 where appImpl [] = elab' (ina { e_isfn = False }) fc f -- e_isfn not set, so no recursive expansion of implicits

972972 appImpl (e : es) = simple_app False

@@ -1028,14 +1028,14 @@ elab ist info emode opts fn tm

10281028 solve

10291029 elab' ina _ c@(PCase fc scr opts)

10301030 = do attack

1031−

1031+

10321032 tyn <- getNameFrom (sMN 0 "scty")

10331033 claim tyn RType

10341034 valn <- getNameFrom (sMN 0 "scval")

10351035 scvn <- getNameFrom (sMN 0 "scvar")

10361036 claim valn (Var tyn)

10371037 letbind scvn (Var tyn) (Var valn)

1038−

1038+

10391039 -- Start filling in the scrutinee type, if we can work one

10401040 -- out from the case options

10411041 let scrTy = getScrType (map fst opts)

@@ -1056,7 +1056,7 @@ elab ist info emode opts fn tm

10561056

10571057 -- Drop the unique arguments used in the term already

10581058 -- and in the scrutinee (since it's

1059− -- not valid to use them again anyway)

1059+ -- not valid to use them again anyway)

10601060 --

10611061 -- Also drop unique arguments which don't appear explicitly

10621062 -- in either case branch so they don't count as used

@@ -1065,7 +1065,7 @@ elab ist info emode opts fn tm

10651065 ptm <- get_term

10661066 let inOpts = (filter (/= scvn) (map fst args)) \\ (concatMap (\x -> allNamesIn (snd x)) opts)

10671067

1068− let argsDropped = filter (isUnique envU)

1068+ let argsDropped = filter (isUnique envU)

10691069 (nub $ allNamesIn scr ++ inApp ptm ++

10701070 inOpts)

10711071

@@ -1097,9 +1097,9 @@ elab ist info emode opts fn tm

10971097 getScrType [] = Nothing

10981098 getScrType (f : os) = maybe (getScrType os) Just (getAppType f)

10991099

1100− getAppType (PRef _ _ n) =

1100+ getAppType (PRef _ _ n) =

11011101 case lookupTyName n (tt_ctxt ist) of

1102− [(n', ty)] | isDConName n' (tt_ctxt ist) ->

1102+ [(n', ty)] | isDConName n' (tt_ctxt ist) ->

11031103 case unApply (getRetTy ty) of

11041104 (P _ tyn _, args) ->

11051105 Just (PApp fc (PRef fc [] tyn)

@@ -1250,12 +1250,12 @@ elab ist info emode opts fn tm

12501250 [] -> lift . tfail . NoSuchVariable $ n

12511251 more -> lift . tfail . CantResolveAlts $ map fst more

12521252 elab' ina fc (PAs _ n t) = lift . tfail . Msg $ "@-pattern not allowed here"

1253− elab' ina fc (PHidden t)

1253+ elab' ina fc (PHidden t)

12541254 | reflection = elab' ina fc t

12551255 | otherwise

12561256 = do (h : hs) <- get_holes

12571257 -- Dotting a hole means that either the hole or any outer

1258− -- hole (a hole outside any occurrence of it)

1258+ -- hole (a hole outside any occurrence of it)

12591259 -- must be solvable by unification as well as being filled

12601260 -- in directly.

12611261 -- Delay dotted things to the end, then when we elaborate them

@@ -1323,7 +1323,7 @@ elab ist info emode opts fn tm

13231323 -- The delayed things with lower numbered priority will be elaborated

13241324 -- first. (In practice, this means delayed alternatives, then PHidden

13251325 -- things.)

1326− delayElab pri t

1326+ delayElab pri t

13271327 = updateAux (\e -> e { delayed_elab = delayed_elab e ++ [(pri, t)] })

13281328

13291329 isScr :: PTerm -> (Name, Binder Term) -> (Name, (Bool, Binder Term))

@@ -1476,7 +1476,7 @@ elab ist info emode opts fn tm

14761476 let t' = case (t, cs) of

14771477 (PCoerced tm, _) -> tm

14781478 (_, []) -> t

1479− (_, cs) -> PAlternative [] TryImplicit

1479+ (_, cs) -> PAlternative [] TryImplicit

14801480 (t : map (mkCoerce env t) cs)

14811481 return t'

14821482 where

@@ -1598,7 +1598,7 @@ pruneByType env (P _ n _) ist as

15981598 [] -> asV

15991599 _ -> as'

16001600 where

1601− ctxt = tt_ctxt ist

1601+ ctxt = tt_ctxt ist

16021602

16031603 headIs var f (PRef _ _ f') = typeHead var f f'

16041604 headIs var f (PApp _ (PRef _ _ (UN l)) [_, _, arg])

@@ -1617,7 +1617,7 @@ pruneByType env (P _ n _) ist as

16171617 _ -> let ty' = normalise ctxt [] ty in

16181618 case unApply (getRetTy ty') of

16191619 (P _ ftyn _, _) -> ftyn == f

1620− (V _, _) ->

1620+ (V _, _) ->

16211621 -- keep, variable

16221622-- trace ("Keeping " ++ show (f', ty')

16231623-- ++ " for " ++ show n) $

@@ -1634,22 +1634,22 @@ pruneByType _ t _ as = as

16341634-- (FIXME: This isn't complete, but I'm leaving it here and coming back

16351635-- to it later - just returns 'var' for now. EB)

16361636isPlausible :: IState -> Bool -> Env -> Name -> Type -> Bool

1637−isPlausible ist var env n ty

1637+isPlausible ist var env n ty

16381638 = let (hvar, classes) = collectConstraints [] [] ty in

16391639 case hvar of

16401640 Nothing -> True

16411641 Just rth -> var -- trace (show (rth, classes)) var

16421642 where

1643− collectConstraints :: [Name] -> [(Term, [Name])] -> Type ->

1643+ collectConstraints :: [Name] -> [(Term, [Name])] -> Type ->

16441644 (Maybe Name, [(Term, [Name])])

16451645 collectConstraints env tcs (Bind n (Pi _ ty _) sc)

16461646 = let tcs' = case unApply ty of

1647− (P _ c _, _) ->

1647+ (P _ c _, _) ->

16481648 case lookupCtxtExact c (idris_classes ist) of

1649− Just tc -> ((ty, map fst (class_instances tc))

1650− : tcs)

1649+ Just tc -> ((ty, map fst (class_instances tc))

1650+ : tcs)

16511651 Nothing -> tcs

1652− _ -> tcs

1652+ _ -> tcs

16531653 in

16541654 collectConstraints (n : env) tcs' sc

16551655 collectConstraints env tcs t

@@ -1669,7 +1669,7 @@ findHighlight n = do ctxt <- get_context

16691669

16701670-- Try again to solve auto implicits

16711671solveAuto :: IState -> Name -> Bool -> (Name, [FailContext]) -> ElabD ()

1672−solveAuto ist fn ambigok (n, failc)

1672+solveAuto ist fn ambigok (n, failc)

16731673 = do hs <- get_holes

16741674 when (not (null hs)) $ do

16751675 env <- get_env

@@ -1682,8 +1682,8 @@ solveAuto ist fn ambigok (n, failc)

16821682 (lift $ Error (addLoc failc

16831683 (CantSolveGoal g (map (\(n, b) -> (n, binderTy b)) env))))

16841684 return ()

1685− where addLoc (FailContext fc f x : prev) err

1686− = At fc (ElaboratingArg f x

1685+ where addLoc (FailContext fc f x : prev) err

1686+ = At fc (ElaboratingArg f x

16871687 (map (\(FailContext _ f' x') -> (f', x')) prev) err)

16881688 addLoc _ err = err

16891689

@@ -1728,7 +1728,7 @@ collectDeferred top casenames ctxt tm = cd [] tm

17281728 t' <- collectDeferred top casenames ctxt t

17291729 when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, t', psns))])

17301730 cd env app

1731− cd env (Bind n b t)

1731+ cd env (Bind n b t)

17321732 = do b' <- cdb b

17331733 t' <- cd ((n, b) : env) t

17341734 return (Bind n b' t')

@@ -1737,7 +1737,7 @@ collectDeferred top casenames ctxt tm = cd [] tm

17371737 cdb (Guess t v) = liftM2 Guess (cd env t) (cd env v)

17381738 cdb b = do ty' <- cd env (binderTy b)

17391739 return (b { binderTy = ty' })

1740− cd env (App s f a) = liftM2 (App s) (cd env f)

1740+ cd env (App s f a) = liftM2 (App s) (cd env f)

17411741 (cd env a)

17421742 cd env t = return t

17431743

@@ -2148,7 +2148,7 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

21482148 | n == tacN "Prim__Fixity", [op'] <- args

21492149 = do opTm <- eval op'

21502150 case opTm of

2151− Constant (Str op) ->

2151+ Constant (Str op) ->

21522152 let opChars = ":!#$%&*+./<=>?@\\^|-~"

21532153 invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\", "%", "~", "?", "!"]

21542154 fixities = idris_infixes ist

@@ -2185,7 +2185,7 @@ runTac autoSolve ist perhapsFC fn tac

21852185 bname _ = Nothing

21862186 runT (Intro xs) = mapM_ (\x -> do attack; intro (Just x)) xs

21872187 runT Intros = do g <- goal

2188− attack;

2188+ attack;

21892189 intro (bname g)

21902190 try' (runT Intros)

21912191 (return ()) True

@@ -2430,18 +2430,18 @@ elaboratingArgErr ((f,x):during) err = fromMaybe err (rewrite err)

24302430withErrorReflection :: Idris a -> Idris a

24312431withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

24322432 where handle :: Err -> Idris Err

2433− handle e@(ReflectionError _ _) = do logLvl 3 "Skipping reflection of error reflection result"

2433+ handle e@(ReflectionError _ _) = do logElab 3 "Skipping reflection of error reflection result"

24342434 return e -- Don't do meta-reflection of errors

2435− handle e@(ReflectionFailed _ _) = do logLvl 3 "Skipping reflection of reflection failure"

2435+ handle e@(ReflectionFailed _ _) = do logElab 3 "Skipping reflection of reflection failure"

24362436 return e

24372437 -- At and Elaborating are just plumbing - error reflection shouldn't rewrite them

2438− handle e@(At fc err) = do logLvl 3 "Reflecting body of At"

2438+ handle e@(At fc err) = do logElab 3 "Reflecting body of At"

24392439 err' <- handle err

24402440 return (At fc err')

2441− handle e@(Elaborating what n ty err) = do logLvl 3 "Reflecting body of Elaborating"

2441+ handle e@(Elaborating what n ty err) = do logElab 3 "Reflecting body of Elaborating"

24422442 err' <- handle err

24432443 return (Elaborating what n ty err')

2444− handle e@(ElaboratingArg f a prev err) = do logLvl 3 "Reflecting body of ElaboratingArg"

2444+ handle e@(ElaboratingArg f a prev err) = do logElab 3 "Reflecting body of ElaboratingArg"

24452445 hs <- getFnHandlers f a

24462446 err' <- if null hs

24472447 then handle err

@@ -2451,8 +2451,8 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

24512451 handle (ProofSearchFail e) = handle e

24522452 -- TODO: argument-specific error handlers go here for ElaboratingArg

24532453 handle e = do ist <- getIState

2454− logLvl 2 "Starting error reflection"

2455− logLvl 5 (show e)

2454+ logElab 2 "Starting error reflection"

2455+ logElab 5 (show e)

24562456 let handlers = idris_errorhandlers ist

24572457 applyHandlers e handlers

24582458 getFnHandlers :: Name -> Name -> Idris [Name]

@@ -2466,7 +2466,7 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

24662466 applyHandlers e handlers =

24672467 do ist <- getIState

24682468 let err = fmap (errReverse ist) e

2469− logLvl 3 $ "Using reflection handlers " ++

2469+ logElab 3 $ "Using reflection handlers " ++

24702470 concat (intersperse ", " (map show handlers))

24712471 let reports = map (\n -> RApp (Var n) (reflectErr err)) handlers

24722472

@@ -2478,7 +2478,7 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

24782478 -- Normalize error handler terms to produce the new messages

24792479 ctxt <- getContext

24802480 let results = map (normalise ctxt []) (map fst handlers)

2481− logLvl 3 $ "New error message info: " ++ concat (intersperse " and " (map show results))

2481+ logElab 3 $ "New error message info: " ++ concat (intersperse " and " (map show results))

24822482

24832483 -- For each handler term output, either discard it if it is Nothing or reify it the Haskell equivalent

24842484 let errorpartsTT = mapMaybe unList (mapMaybe fromTTMaybe results)

@@ -2499,8 +2499,8 @@ processTacticDecls info steps =

24992499 -- establish metavars that later function bodies resolve.

25002500 forM_ (reverse steps) $ \case

25012501 RTyDeclInstrs n fc impls ty ->

2502− do logLvl 3 $ "Declaration from tactics: " ++ show n ++ " : " ++ show ty

2503− logLvl 3 $ " It has impls " ++ show impls

2502+ do logElab 3 $ "Declaration from tactics: " ++ show n ++ " : " ++ show ty

2503+ logElab 3 $ " It has impls " ++ show impls

25042504 updateIState $ \i -> i { idris_implicits =

25052505 addDef n impls (idris_implicits i) }

25062506 addIBC (IBCImp n)

@@ -2517,13 +2517,13 @@ processTacticDecls info steps =

25172517 in addDeferred ds'

25182518 _ -> return ()

25192519 RAddInstance className instName ->

2520− do -- The type class resolution machinery relies on a special

2521− logLvl 2 $ "Adding elab script instance " ++ show instName ++

2520+ do -- The type class resolution machinery relies on a special

2521+ logElab 2 $ "Adding elab script instance " ++ show instName ++

25222522 " for " ++ show className

25232523 addInstance False True className instName

25242524 addIBC (IBCInstance False True className instName)

25252525 RClausesInstrs n cs ->

2526− do logLvl 3 $ "Pattern-matching definition from tactics: " ++ show n

2526+ do logElab 3 $ "Pattern-matching definition from tactics: " ++ show n

25272527 solveDeferred n

25282528 let lhss = map (\(_, lhs, _) -> lhs) cs

25292529 let fc = fileFC "elab_reflected"

@@ -2553,7 +2553,7 @@ processTacticDecls info steps =

25532553 calls = findCalls sc' scargs

25542554 used = findUsedArgs sc' scargs'

25552555 cg = CGInfo scargs' calls [] used []

2556− in do logLvl 2 $ "Called names in reflected elab: " ++ show cg

2556+ in do logElab 2 $ "Called names in reflected elab: " ++ show cg

25572557 addToCG n cg

25582558 addToCalledG n (nub (map fst calls))

25592559 addIBC $ IBCCG n

src/Idris/Elab/Transform.hs+7−8

@@ -53,7 +53,7 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ _ tf) _) rhs_in

5353 = do ctxt <- getContext

5454 i <- getIState

5555 let lhs = addImplPat i lhs_in

56− logLvl 5 ("Transform LHS input: " ++ showTmImpls lhs)

56+ logElab 5 ("Transform LHS input: " ++ showTmImpls lhs)

5757 (ElabResult lhs' dlhs [] ctxt' newDecls highlights, _) <-

5858 tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "transLHS") infP initEState

5959 (erun fc (buildTC i info ETransLHS [] (sUN "transform")

@@ -67,11 +67,11 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ _ tf) _) rhs_in

6767

6868 (clhs_tm_in, clhs_ty) <- recheckC_borrowing False False [] fc id [] lhs_tm

6969 let clhs_tm = renamepats pnames clhs_tm_in

70− logLvl 3 ("Transform LHS " ++ show clhs_tm)

71− logLvl 3 ("Transform type " ++ show clhs_ty)

72−

70+ logElab 3 ("Transform LHS " ++ show clhs_tm)

71+ logElab 3 ("Transform type " ++ show clhs_ty)

72+

7373 let rhs = addImplBound i (map fst newargs) rhs_in

74− logLvl 5 ("Transform RHS input: " ++ showTmImpls rhs)

74+ logElab 5 ("Transform RHS input: " ++ showTmImpls rhs)

7575

7676 ((rhs', defer, ctxt', newDecls), _) <-

7777 tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "transRHS") clhs_ty initEState

@@ -88,7 +88,7 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ _ tf) _) rhs_in

8888

8989 (crhs_tm_in, crhs_ty) <- recheckC_borrowing False False [] fc id [] rhs'

9090 let crhs_tm = renamepats pnames crhs_tm_in

91− logLvl 3 ("Transform RHS " ++ show crhs_tm)

91+ logElab 3 ("Transform RHS " ++ show crhs_tm)

9292

9393 -- Types must always convert

9494 case converts ctxt [] clhs_ty crhs_ty of

@@ -118,6 +118,5 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ _ tf) _) rhs_in

118118 -- with any other names when applying rules, so rename here.

119119 pnames = map (\i -> sMN i ("tvar" ++ show i)) [0..]

120120

121−elabTransform info fc safe lhs_in rhs_in

121+elabTransform info fc safe lhs_in rhs_in

122122 = ierror (At fc (Msg "Invalid transformation rule (must be function application)"))

123−

src/Idris/Elab/Type.hs+18−21

@@ -1,5 +1,5 @@

11{-# LANGUAGE PatternGuards #-}

2−module Idris.Elab.Type (buildType, elabType, elabType',

2+module Idris.Elab.Type (buildType, elabType, elabType',

33 elabPostulate, elabExtern) where

55import Idris.AbsSyntax

@@ -52,20 +52,20 @@ import Data.List.Split (splitOn)

5252

5353import Util.Pretty(pretty, text)

5454

55−buildType :: ElabInfo -> SyntaxInfo -> FC -> FnOpts -> Name -> PTerm ->

55+buildType :: ElabInfo -> SyntaxInfo -> FC -> FnOpts -> Name -> PTerm ->

5656 Idris (Type, Type, PTerm, [(Int, Name)])

5757buildType info syn fc opts n ty' = do

5858 ctxt <- getContext

5959 i <- getIState

6060

61− logLvl 2 $ show n ++ " pre-type " ++ showTmImpls ty' ++ show (no_imp syn)

61+ logElab 2 $ show n ++ " pre-type " ++ showTmImpls ty' ++ show (no_imp syn)

6262 ty' <- addUsingConstraints syn fc ty'

6363 ty' <- addUsingImpls syn n fc ty'

6464 let ty = addImpl (imp_methods syn) i ty'

6565

66− logLvl 5 $ show n ++ " type pre-addimpl " ++ showTmImpls ty'

67− logLvl 5 $ show "with methods " ++ show (imp_methods syn)

68− logLvl 2 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty

66+ logElab 5 $ show n ++ " type pre-addimpl " ++ showTmImpls ty'

67+ logElab 5 $ show "with methods " ++ show (imp_methods syn)

68+ logElab 2 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty

6969

7070 (ElabResult tyT' defer is ctxt' newDecls highlights, log) <-

7171 tclift $ elaborate ctxt (idris_datatypes i) n (TType (UVal 0)) initEState

@@ -76,7 +76,7 @@ buildType info syn fc opts n ty' = do

7676

7777 let tyT = patToImp tyT'

7878

79− logLvl 3 $ show ty ++ "\nElaborated: " ++ show tyT'

79+ logElab 3 $ show ty ++ "\nElaborated: " ++ show tyT'

8080

8181 ds <- checkAddDef True False fc iderr defer

8282 -- if the type is not complete, note that we'll need to infer

@@ -86,20 +86,20 @@ buildType info syn fc opts n ty' = do

8686

8787 mapM_ (elabCaseBlock info opts) is

8888 ctxt <- getContext

89− logLvl 5 $ "Rechecking"

90− logLvl 6 $ show tyT

91− logLvl 10 $ "Elaborated to " ++ showEnvDbg [] tyT

89+ logElab 5 $ "Rechecking"

90+ logElab 6 $ show tyT

91+ logElab 10 $ "Elaborated to " ++ showEnvDbg [] tyT

9292 (cty, ckind) <- recheckC fc id [] tyT

9393

9494 -- record the implicit and inaccessible arguments

9595 i <- getIState

9696 let (inaccData, impls) = unzip $ getUnboundImplicits i cty ty

9797 let inacc = inaccessibleImps 0 cty inaccData

98− logLvl 3 $ show n ++ ": inaccessible arguments: " ++ show inacc ++

98+ logElab 3 $ show n ++ ": inaccessible arguments: " ++ show inacc ++

9999 " from " ++ show cty ++ "\n" ++ showTmImpls ty

100100

101101 putIState $ i { idris_implicits = addDef n impls (idris_implicits i) }

102− logLvl 3 ("Implicit " ++ show n ++ " " ++ show impls)

102+ logElab 3 ("Implicit " ++ show n ++ " " ++ show impls)

103103 addIBC (IBCImp n)

104104

105105 when (Constructor `notElem` opts) $ do

@@ -114,7 +114,7 @@ buildType info syn fc opts n ty' = do

114114 patToImp (Bind n b sc) = Bind n b (patToImp sc)

115115 patToImp t = t

116116

117− param_pos i ns (Bind n (Pi _ t _) sc)

117+ param_pos i ns (Bind n (Pi _ t _) sc)

118118 | n `elem` ns = i : param_pos (i + 1) ns sc

119119 | otherwise = param_pos (i + 1) ns sc

120120 param_pos i ns t = []

@@ -140,9 +140,9 @@ elabType' norm info syn doc argDocs fc opts n nfc ty' = {- let ty' = piBind (par

140140 let nty = cty -- normalise ctxt [] cty

141141 -- if the return type is something coinductive, freeze the definition

142142 ctxt <- getContext

143− logLvl 2 $ "Rechecked to " ++ show nty

143+ logElab 2 $ "Rechecked to " ++ show nty

144144 let nty' = normalise ctxt [] nty

145− logLvl 2 $ "Rechecked to " ++ show nty'

145+ logElab 2 $ "Rechecked to " ++ show nty'

146146

147147 -- Add function name to internals (used for making :addclause know

148148 -- the name unambiguously)

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

158158 [TI _ True _ _ _] -> True

159159 _ -> False

160160 _ -> False

161− -- Productivity checking now via checking for guarded 'Delay'

161+ -- Productivity checking now via checking for guarded 'Delay'

162162 let opts' = opts -- if corec then (Coinductive : opts) else opts

163163 let usety = if norm then nty' else nty

164164 ds <- checkDef fc iderr [(n, (-1, Nothing, usety, []))]

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

177177 addIBC (IBCOpt n)

178178 when (Implicit `elem` opts') $ do addCoercion n

179179 addIBC (IBCCoercion n)

180− when (AutoHint `elem` opts') $

180+ when (AutoHint `elem` opts') $

181181 case fam of

182182 P _ tyn _ -> do addAutoHint tyn n

183183 addIBC (IBCAutoHint tyn n)

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

201201 sendHighlighting [(nfc, AnnName n Nothing Nothing Nothing)]

202202 -- if it's an export list type, make a note of it

203203 case (unApply usety) of

204− (P _ ut _, _)

204+ (P _ ut _, _)

205205 | ut == ffiexport -> do addIBC (IBCExport n)

206206 addExport n

207207 _ -> return ()

@@ -256,6 +256,3 @@ elabExtern info syn doc fc nfc opts n ty = do

256256

257257 -- remove it from the deferred definitions list

258258 solveDeferred n

259−

260−

261−

src/Idris/Elab/Utils.hs+18−21

@@ -37,14 +37,14 @@ recheckC_borrowing uniq_check addConstrs bs fc mkerr env t

3737 (tm, ty, cs) <- tclift $ case recheck_borrowing uniq_check bs ctxt env t' t of

3838 Error e -> tfail (At fc (mkerr e))

3939 OK x -> return x

40− logLvl 6 $ "CONSTRAINTS ADDED: " ++ show (tm, ty, cs)

40+ logElab 6 $ "CONSTRAINTS ADDED: " ++ show (tm, ty, cs)

4141 when addConstrs $ addConstraints fc cs

4242 mapM_ (checkDeprecated fc) (allTTNames tm)

4343 mapM_ (checkDeprecated fc) (allTTNames ty)

4444 return (tm, ty)

4545

4646checkDeprecated :: FC -> Name -> Idris ()

47−checkDeprecated fc n

47+checkDeprecated fc n

4848 = do r <- getDeprecated n

4949 case r of

5050 Nothing -> return ()

@@ -64,9 +64,9 @@ checkAddDef :: Bool -> Bool -> FC -> (Name -> Err -> Err)

6464 -> [(Name, (Int, Maybe Name, Type, [Name]))]

6565 -> Idris [(Name, (Int, Maybe Name, Type, [Name]))]

6666checkAddDef add toplvl fc mkerr [] = return []

67−checkAddDef add toplvl fc mkerr ((n, (i, top, t, psns)) : ns)

67+checkAddDef add toplvl fc mkerr ((n, (i, top, t, psns)) : ns)

6868 = do ctxt <- getContext

69− logLvl 5 $ "Rechecking deferred name " ++ show (n, t)

69+ logElab 5 $ "Rechecking deferred name " ++ show (n, t)

7070 (t', _) <- recheckC fc (mkerr n) [] t

7171 when add $ do addDeferred [(n, (i, top, t, psns, toplvl))]

7272 addIBC (IBCDef n)

@@ -93,7 +93,7 @@ inaccessibleArgs _ _ = []

9393elabCaseBlock :: ElabInfo -> FnOpts -> PDecl -> Idris ()

9494elabCaseBlock info opts d@(PClauses f o n ps)

9595 = do addIBC (IBCDef n)

96− logLvl 5 $ "CASE BLOCK: " ++ show (n, d)

96+ logElab 5 $ "CASE BLOCK: " ++ show (n, d)

9797 let opts' = nub (o ++ opts)

9898 -- propagate totality assertion to the new definitions

9999 when (AssertTotal `elem` opts) $ setFlags n [AssertTotal]

@@ -104,16 +104,16 @@ elabCaseBlock info opts d@(PClauses f o n ps)

104104-- they are the same!)

105105checkInferred :: FC -> PTerm -> PTerm -> Idris ()

106106checkInferred fc inf user =

107− do logLvl 6 $ "Checked to\n" ++ showTmImpls inf ++ "\n\nFROM\n\n" ++

107+ do logElab 6 $ "Checked to\n" ++ showTmImpls inf ++ "\n\nFROM\n\n" ++

108108 showTmImpls user

109− logLvl 10 $ "Checking match"

109+ logElab 10 $ "Checking match"

110110 i <- getIState

111111 tclift $ case matchClause' True i user inf of

112112 _ -> return ()

113113-- Left (x, y) -> tfail $ At fc

114114-- (Msg $ "The type-checked term and given term do not match: "

115115-- ++ show x ++ " and " ++ show y)

116− logLvl 10 $ "Checked match"

116+ logElab 10 $ "Checked match"

117117-- ++ "\n" ++ showImp True inf ++ "\n" ++ showImp True user)

118118

119119-- | Return whether inferred term is different from given term

@@ -121,7 +121,7 @@ checkInferred fc inf user =

121121inferredDiff :: FC -> PTerm -> PTerm -> Idris Bool

122122inferredDiff fc inf user =

123123 do i <- getIState

124− logLvl 6 $ "Checked to\n" ++ showTmImpls inf ++ "\n" ++

124+ logElab 6 $ "Checked to\n" ++ showTmImpls inf ++ "\n" ++

125125 showTmImpls user

126126 tclift $ case matchClause' True i user inf of

127127 Right vs -> return False

@@ -152,7 +152,7 @@ decorateid decorate (PClauses f o n cs)

152152

153153-- if 't' is a type class application, assume its arguments are injective

154154pbinds :: IState -> Term -> ElabD ()

155−pbinds i (Bind n (PVar t) sc)

155+pbinds i (Bind n (PVar t) sc)

156156 = do attack; patbind n

157157 env <- get_env

158158 case unApply (normalise (tt_ctxt i) env t) of

@@ -207,14 +207,14 @@ getFlexInType i env ps tm@(App _ f a)

207207 | (P nt tn _, args) <- unApply tm, nt /= Bound

208208 = case lookupCtxtExact tn (idris_datatypes i) of

209209 Just t -> nub $ paramNames args env [x | x <- [0..length args],

210− not (x `elem` param_pos t)]

210+ not (x `elem` param_pos t)]

211211 ++ getFlexInType i env ps f ++

212212 getFlexInType i env ps a

213213 Nothing -> let ppos = case lookupCtxtExact tn (idris_fninfo i) of

214214 Just fi -> fn_params fi

215215 Nothing -> []

216216 in nub $ paramNames args env [x | x <- [0..length args],

217− not (x `elem` ppos)]

217+ not (x `elem` ppos)]

218218 ++ getFlexInType i env ps f ++

219219 getFlexInType i env ps a

220220 | otherwise = nub $ getFlexInType i env ps f ++

@@ -228,7 +228,7 @@ getParamsInType i env ps t = let fix = getFixedInType i env ps t

228228 flex = getFlexInType i env fix t in

229229 [x | x <- fix, not (x `elem` flex)]

230230

231−getTCinj i (Bind n (Pi _ t _) sc)

231+getTCinj i (Bind n (Pi _ t _) sc)

232232 = getTCinj i t ++ getTCinj i (instantiate (P Bound n t) sc)

233233getTCinj i ap@(App _ f a)

234234 | (P _ n _, args) <- unApply ap,

@@ -258,7 +258,7 @@ paramNames args env (p : ps)

258258getUniqueUsed :: Context -> Term -> [Name]

259259getUniqueUsed ctxt tm = execState (getUniq [] [] tm) []

260260 where

261− getUniq :: Env -> [(Name, Bool)] -> Term -> State [Name] ()

261+ getUniq :: Env -> [(Name, Bool)] -> Term -> State [Name] ()

262262 getUniq env us (Bind n b sc)

263263 = let uniq = case check ctxt env (forgetEnv (map fst env) (binderTy b)) of

264264 OK (_, UType UniqueType) -> True

@@ -285,9 +285,9 @@ getUniqueUsed ctxt tm = execState (getUniq [] [] tm) []

285285-- In a functional application, return the names which are used

286286-- directly in a static position

287287getStaticNames :: IState -> Term -> [Name]

288−getStaticNames ist (Bind n (PVar _) sc)

288+getStaticNames ist (Bind n (PVar _) sc)

289289 = getStaticNames ist (instantiate (P Bound n Erased) sc)

290−getStaticNames ist tm

290+getStaticNames ist tm

291291 | (P _ fn _, args) <- unApply tm

292292 = case lookupCtxtExact fn (idris_statics ist) of

293293 Just stpos -> getStatics args stpos

@@ -305,15 +305,12 @@ getStatics ns (Bind n (Pi _ _ _) t)

305305getStatics _ _ = []

306306

307307mkStatic :: [Name] -> PDecl -> PDecl

308−mkStatic ns (PTy doc argdocs syn fc o n nfc ty)

308+mkStatic ns (PTy doc argdocs syn fc o n nfc ty)

309309 = PTy doc argdocs syn fc o n nfc (mkStaticTy ns ty)

310310mkStatic ns t = t

311311

312312mkStaticTy :: [Name] -> PTerm -> PTerm

313−mkStaticTy ns (PPi p n fc ty sc)

313+mkStaticTy ns (PPi p n fc ty sc)

314314 | n `elem` ns = PPi (p { pstatic = Static }) n fc ty (mkStaticTy ns sc)

315315 | otherwise = PPi p n fc ty (mkStaticTy ns sc)

316316mkStaticTy ns t = t

317−

318−

319−

src/Idris/Elab/Value.hs+4−4

@@ -1,6 +1,6 @@

11{-# LANGUAGE PatternGuards #-}

22{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

3−module Idris.Elab.Value(elabVal, elabValBind, elabDocTerms,

3+module Idris.Elab.Value(elabVal, elabValBind, elabDocTerms,

44 elabExec, elabREPL) where

66import Idris.AbsSyntax

@@ -58,7 +58,7 @@ elabValBind info aspat norm tm_in

5858 = do ctxt <- getContext

5959 i <- getIState

6060 let tm = addImpl [] i tm_in

61− logLvl 10 (showTmImpls tm)

61+ logElab 10 (showTmImpls tm)

6262 -- try:

6363 -- * ordinary elaboration

6464 -- * elaboration as a Type

@@ -80,7 +80,7 @@ elabValBind info aspat norm tm_in

8080 addDeferred def''

8181 mapM_ (elabCaseBlock info []) is

8282

83− logLvl 3 ("Value: " ++ show vtm)

83+ logElab 3 ("Value: " ++ show vtm)

8484 (vtm_in, vty) <- recheckC (fileFC "(input)") id [] vtm

8585

8686 let vtm = if norm then normalise (tt_ctxt i) [] vtm_in

@@ -127,7 +127,7 @@ elabExec fc tm = runtm (PAlternative [] FirstSuccess

127127 printtm tm

128128 ])

129129 where

130− runtm t = PApp fc (PRef fc [] (sUN "run__IO"))

130+ runtm t = PApp fc (PRef fc [] (sUN "run__IO"))

131131 [pimp (sUN "ffi") (PRef fc [] (sUN "FFI_C")) False, pexp t]

132132 printtm t = PApp fc (PRef fc [] (sUN "printLn"))

133133 [pimp (sUN "ffi") (PRef fc [] (sUN "FFI_C")) False, pexp t]

src/Idris/ElabDecls.hs+14−14

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

159159 = return () -- nothing to elaborate

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

161161 | what /= EDefns

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

162+ = do logElab 1 $ "Elaborating type decl " ++ show n ++ show o

163163 elabType info s doc argdocs f o n nfc ty

164164 return ()

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

166166 | what /= EDefns

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

168− if b

167+ = do logElab 1 $ "Elaborating postulate " ++ show n ++ show o

168+ if b

169169 then elabExtern info s doc f nfc o n ty

170170 else elabPostulate info s doc f nfc o n ty

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

172172 | what /= ETypes

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

173+ = do logElab 1 $ "Elaborating " ++ show (d_name d)

174174 elabData info s doc argDocs f co d

175175 | otherwise

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

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

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

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

179179 | what /= ETypes

180− = do logLvl 1 $ "Elaborating clause " ++ show n

180+ = do logElab 1 $ "Elaborating clause " ++ show n

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

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

183183 [fs] -> fs

@@ -191,11 +191,11 @@ elabDecl' what info (PMutual f ps)

191191 -- record mutually defined data definitions

192192 let datans = concatMap declared (filter isDataDecl ps)

193193 mapM_ (setMutData datans) datans

194− logLvl 1 $ "Rechecking for positivity " ++ show datans

194+ logElab 1 $ "Rechecking for positivity " ++ show datans

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

196196 -- Do totality checking after entire mutual block

197197 i <- get

198− mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n

198+ mapM_ (\n -> do logElab 5 $ "Simplifying " ++ show n

199199 ctxt' <- do ctxt <- getContext

200200 tclift $ simplifyCasedef n (getErasureInfo i) ctxt

201201 setContext ctxt')

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

216216

217217elabDecl' what info (PParams f ns ps)

218218 = do i <- getIState

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

219+ logElab 1 $ "Expanding params block with " ++ show ns ++ " decls " ++

220220 show (concatMap tldeclared ps)

221221 let nblock = pblock i

222222 mapM_ (elabDecl' what info) nblock

@@ -240,17 +240,17 @@ elabDecl' what info (PNamespace n nfc ps) =

240240

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

242242 | what /= EDefns

243− = do logLvl 1 $ "Elaborating class " ++ show n

243+ = do logElab 1 $ "Elaborating class " ++ show n

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

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

246− = do logLvl 1 $ "Elaborating instance " ++ show n

246+ = do logElab 1 $ "Elaborating instance " ++ show n

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

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

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

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

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

251251{-

252252 | otherwise

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

253+ = do logElab 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 nfc provWhat n)

263263 | what /= EDefns

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

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

265265 elabProvider doc info syn fc nfc provWhat n

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

267267 = do elabTransform info fc safety old new

src/Idris/Erasure.hs+12−12

@@ -85,10 +85,10 @@ performUsageAnalysis startNames = do

8585 usage = M.toList minUse

8686

8787 -- Print some debug info.

88− logLvl 5 $ "Original deps:\n" ++ unlines (map fmtItem . M.toList $ depMap)

89− logLvl 3 $ "Reachable names:\n" ++ unlines (map (indent . show) . S.toList $ reachableNames)

90− logLvl 4 $ "Minimal usage:\n" ++ fmtUseMap usage

91− logLvl 5 $ "Residual deps:\n" ++ unlines (map fmtItem . M.toList $ residDeps)

88+ logErasure 5 $ "Original deps:\n" ++ unlines (map fmtItem . M.toList $ depMap)

89+ logErasure 3 $ "Reachable names:\n" ++ unlines (map (indent . show) . S.toList $ reachableNames)

90+ logErasure 4 $ "Minimal usage:\n" ++ fmtUseMap usage

91+ logErasure 5 $ "Residual deps:\n" ++ unlines (map fmtItem . M.toList $ residDeps)

9292

9393 -- Check that everything reachable is accessible.

9494 checkEnabled <- (WarnReach `elem`) . opt_cmdline . idris_options <$> getIState

@@ -135,7 +135,7 @@ performUsageAnalysis startNames = do

135135 where

136136 fmt n [] = show n ++ " (no more information available)"

137137 fmt n rs = show n ++ " from " ++ intercalate ", " [show rn ++ " arg# " ++ show ri | (rn,ri) <- rs]

138− warn = logLvl 0

138+ warn = logErasure 0

139139

140140-- Find the minimal consistent usage by forward chaining.

141141minimalUsage :: Deps -> (Deps, (Set Name, UseMap))

@@ -150,7 +150,7 @@ minimalUsage = second gather . forwardChain

150150

151151forwardChain :: Deps -> (Deps, DepSet)

152152forwardChain deps

153− | Just trivials <- M.lookup S.empty deps

153+ | Just trivials <- M.lookup S.empty deps

154154 = (M.unionWith S.union trivials)

155155 `second` forwardChain (remove trivials . M.delete S.empty $ deps)

156156 | otherwise = (deps, M.empty)

@@ -164,7 +164,7 @@ forwardChain deps

164164-- starting the depth-first search from a list of Names.

165165buildDepMap :: Ctxt ClassInfo -> [(Name, Int)] -> [(Name, Int)] ->

166166 Context -> [Name] -> Deps

167−buildDepMap ci used externs ctx startNames

167+buildDepMap ci used externs ctx startNames

168168 = addPostulates used $ dfs S.empty M.empty startNames

169169 where

170170 -- mark the result of Main.main as used with the empty assumption

@@ -181,7 +181,7 @@ buildDepMap ci used externs ctx startNames

181181 usedNames = allNames deps S.\\ specialPrims

182182 usedPrims = [(p_name p, p_arity p) | p <- primitives, p_name p `S.member` usedNames]

183183

184− postulates used =

184+ postulates used =

185185 [ [] ==> concat

186186 -- Main.main ( + export lists) and run__IO, are always evaluated

187187 -- but they elude analysis since they come from the seed term.

@@ -190,7 +190,7 @@ buildDepMap ci used externs ctx startNames

190190 ,[(sUN "call__IO", Result), (sUN "call__IO", Arg 2)]

191191

192192 -- Explicit usage declarations from a %used pragma

193− , map (\(n, i) -> (n, Arg i)) used

193+ , map (\(n, i) -> (n, Arg i)) used

194194

195195 -- MkIO is read by run__IO,

196196 -- but this cannot be observed in the source code of programs.

@@ -200,7 +200,7 @@ buildDepMap ci used externs ctx startNames

200200 -- Foreign calls are built with pairs, but mkForeign doesn't

201201 -- have an implementation so analysis won't see them

202202 , [(pairCon, Arg 2),

203− (pairCon, Arg 3)] -- Used in foreign calls

203+ (pairCon, Arg 3)] -- Used in foreign calls

204204

205205 -- these have been discovered as builtins but are not listed

206206 -- among Idris.Primitives.primitives

@@ -211,7 +211,7 @@ buildDepMap ci used externs ctx startNames

211211 -- believe_me is a primitive but it only uses its third argument

212212 -- it is special-cased in usedNames above

213213 , it "prim__believe_me" [2]

214−

214+

215215 -- in general, all other primitives use all their arguments

216216 , [(n, Arg i) | (n,arity) <- usedPrims, i <- [0..arity-1]]

217217

@@ -324,7 +324,7 @@ buildDepMap ci used externs ctx startNames

324324 , viMethod = meth j

325325 })

326326 | (v, j) <- zip ns [0..]]

327−

327+

328328 -- this is safe because it's certainly a patvar

329329 varIdx = fromJust (viFunArg var)

330330

src/Idris/IBC.hs+20−18

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

113113 Nothing -> True

114114 Just p -> not p && reexport

115115 when redo $

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

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

117117 archiveFile <- runIO $ B.readFile fp

118118 case toArchiveOrFail archiveFile of

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

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

189189

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

191191writeIBC src f

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

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

193193 i <- getIState

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

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

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

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

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

200200 writeArchive f ibcf

201− logLvl 1 "Written")

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

201+ logCodeGen 1 "Written")

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

203203 return ()

204204

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

@@ -208,20 +208,20 @@ writePkgIndex :: FilePath -> Idris ()

208208writePkgIndex f

209209 = do i <- getIState

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

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

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

212212 show (map snd imps)

213213 resetNameIdx

214214 let ibcf = initIBC { ibc_imports = imps }

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

216216 writeArchive f ibcf

217− logLvl 1 "Written")

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

217+ logCodeGen 1 "Written")

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

219219 return ()

220220

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

222222mkIBC [] f = return f

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

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

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

225225 f' <- ibc ist i f

226226 mkIBC is f'

227227

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

319319process reexp i fn = do

320320 ver <- getEntry 0 "ver" i

321321 when (ver /= ibcVersion) $ do

322− logLvl 1 "ibc out of date"

322+ logCodeGen 1 "ibc out of date"

323323 let e = if ver < ibcVersion

324324 then " an earlier " else " a later "

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

@@ -415,10 +415,12 @@ pImports reexp fs

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

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

417417 case fp of

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

419− ifail "Must be an ibc"

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

421− ifail "Must be an ibc"

418+ LIDR fn -> do

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

420+ ifail "Must be an ibc"

421+ IDR fn -> do

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

423+ ifail "Must be an ibc"

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

423425 fs

424426

@@ -515,13 +517,13 @@ pDefs reexp ds

515517 do d' <- updateDef d

516518 case d' of

517519 TyDecl _ _ -> return ()

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

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

519521 solveDeferred n

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

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

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

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

523525 setAccessibility n Hidden

524− else logLvl 1 $ "Exporting " ++ show n) ds

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

525527 where

526528 updateDef (CaseOp c t args o s cd)

527529 = do o' <- mapM updateOrig o

@@ -586,7 +588,7 @@ pAccess :: Bool -- ^ Reexporting?

586588pAccess reexp ds

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

588590 do let a = if reexp then a_in else Hidden

589− logLvl 3 $ "Setting " ++ show (a, n) ++ " to " ++ show a

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

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

591593

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

@@ -1843,7 +1845,7 @@ instance Binary PTerm where

18431845 _ -> error "Corrupted binary data for PTerm"

18441846

18451847instance Binary PAltType where

1846− put x

1848+ put x

18471849 = case x of

18481850 ExactlyOne x1 -> do putWord8 0

18491851 put x1

src/Idris/Parser.hs+6−6

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

15521552 ids <- allImportDirs

15531553 fp <- findImport ids ibcsd file

15541554 if file `elem` imported i

1555− then do logLvl 1 $ "Already read " ++ file

1555+ then do logParser 1 $ "Already read " ++ file

15561556 return Nothing

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

15581558 case fp of

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

15601560 LIDR fn -> loadSource True fn Nothing

15611561 IBC fn src ->

15621562 idrisCatch (loadIBC True fn)

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

1563+ (\c -> do logParser 1 $ fn ++ " failed " ++ pshow i c

15641564 case src of

15651565 IDR sfn -> loadSource False sfn Nothing

15661566 LIDR sfn -> loadSource True sfn Nothing)

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

15691569{- | Load idris code from file -}

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

15711571loadFromIFile reexp i@(IBC fn src) maxline

1572− = do logLvl 1 $ "Skipping " ++ getSrcFile i

1572+ = do logParser 1 $ "Skipping " ++ getSrcFile i

15731573 idrisCatch (loadIBC reexp fn)

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

15751575 where

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

15931593{- | Load Idris source code-}

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

15951595loadSource lidr f toline

1596− = do logLvl 1 ("Reading " ++ f)

1596+ = do logParser 1 ("Reading " ++ f)

15971597 i <- getIState

15981598 let def_total = default_total i

15991599 file_in <- runIO $ readSource f

@@ -1637,7 +1637,7 @@ loadSource lidr f toline

16371637 ]

16381638 histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames

16391639 case map head . filter ((/= 1) . length) $ histogram of

1640− [] -> logLvl 3 $ "Module aliases: " ++ show (M.toList modAliases)

1640+ [] -> logParser 3 $ "Module aliases: " ++ show (M.toList modAliases)

16411641 (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n

16421642

16431643 i <- getIState

@@ -1676,7 +1676,7 @@ loadSource lidr f toline

16761676 -- Parsing done, now process declarations

16771677

16781678 let ds = namespaces mname ds'

1679− logLvl 3 (show $ showDecls verbosePPOption ds)

1679+ logParser 3 (show $ showDecls verbosePPOption ds)

16801680 i <- getIState

16811681 logLvl 10 (show (toAlist (idris_implicits i)))

16821682 logLvl 3 (show (idris_infixes i))

src/Idris/REPL.hs+8−8

@@ -801,7 +801,7 @@ process fn (ModImport f) = do fmod <- loadModule f

801801 Nothing -> iPrintError $ "Can't find import " ++ f

802802process fn (Eval t)

803803 = withErrorReflection $

804− do logLvl 5 $ show t

804+ do logParser 5 $ show t

805805 getIState >>= flip warnDisamb t

806806 (tm, ty) <- elabREPL recinfo ERHS t

807807 ctxt <- getContext

@@ -814,8 +814,8 @@ process fn (Eval t)

814814 -- Add value to context, call it "it"

815815 updateContext (addCtxtDef (sUN "it") (Function ty' tm'))

816816 ist <- getIState

817− logLvl 3 $ "Raw: " ++ show (tm', ty')

818− logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'

817+ logParser 3 $ "Raw: " ++ show (tm', ty')

818+ logParser 10 $ "Debug: " ++ showEnvDbg [] tm'

819819 let tmDoc = pprintDelab ist tm'

820820 -- errReverse to make type more readable

821821 tyDoc = pprintDelab ist (errReverse ist ty')

@@ -824,7 +824,7 @@ process fn (Eval t)

824824 | otherwise = tm

825825

826826process fn (NewDefn decls) = do

827− logLvl 3 ("Defining names using these decls: " ++ show (showDecls verbosePPOption decls))

827+ logParser 3 ("Defining names using these decls: " ++ show (showDecls verbosePPOption decls))

828828 mapM_ defineName namedGroups where

829829 namedGroups = groupBy (\d1 d2 -> getName d1 == getName d2) decls

830830 getName :: PDecl -> Maybe Name

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

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

12541254 Just x -> do let libs = idris_dynamic_libs i

12551255 if x `elem` libs

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

1256+ then do logParser 1 ("Tried to load duplicate library " ++ lib_name x)

12571257 return ()

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

12591259 where trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace

@@ -1524,7 +1524,7 @@ loadInputs inputs toline -- furthest line to read in input source files

15241524

15251525 importlists <- getImports [] inputs

15261526

1527− logLvl 1 (show (map (\(i,m) -> (i, map import_path m)) importlists))

1527+ logParser 1 (show (map (\(i,m) -> (i, map import_path m)) importlists))

15281528

15291529 let ninputs = zip [1..] inputs

15301530 ifiles <- mapWhileOK (\(num, input) ->

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

15341534 importlists

15351535 input

15361536 let ifiles = getModuleFiles modTree

1537− logLvl 1 ("MODULE TREE : " ++ show modTree)

1538− logLvl 1 ("RELOAD: " ++ show ifiles)

1537+ logParser 1 ("MODULE TREE : " ++ show modTree)

1538+ logParser 1 ("RELOAD: " ++ show ifiles)

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

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

15411541 -- return the files that need rechecking

src/Idris/REPLParser.hs+5−3

@@ -407,9 +407,11 @@ cmd_cats name = do

407407 fail $ "Category: " ++ c ++ " is not recognised."

408408

409409 pLogCats :: P.IdrisParser [LogCat]

410− pLogCats = try (P.symbol "parser" >> return parserCats)

411− <|> try (P.symbol "elab" >> return elabCats)

412− <|> try (P.symbol "codegen" >> return codegenCats)

410+ pLogCats = try (P.symbol "parser" >> return parserCats)

411+ <|> try (P.symbol "elab" >> return elabCats)

412+ <|> try (P.symbol "codegen" >> return codegenCats)

413+ <|> try (P.symbol "coverage" >> return [ICoverage])

414+ <|> try (P.symbol "erasure" >> return [IErasure])

413415 <|> badCat

414416

415417cmd_let :: String -> P.IdrisParser (Either String Command)