a8e9ec5 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #2856 from jfdm/log-by-category

Category based logging for Idris.

commita8e9ec55b9fc03e4f8800f6ab7ba0fb33ccf926d authorJan de Muijnck-Hughes <jfdm@users.noreply.github.com> dateSat 19 Dec 2015, 14:49 (11 years ago) parent9c99198 5f3e700

26 files changed+646−523

compare with master

unifiedsplit

CHANGELOG+13−2

@@ -1,3 +1,14 @@

1+New in 0.9.21:

2+==============

4+* Idris' logging infrastructure has been categorised. Command line and repl

5+ are available. For command line the option `--logging-categories CATS`

6+ is used to pass in the categories. Here `CATS` is a colon separated quoted

7+ string containing the categories to log. The REPL command is `logcats CATS`.

8+ Where `CATS` is a whitespace separated list of categoriese. Default is for

9+ all categories to be logged.

10+

11+

112New in 0.9.20:

213==============

314

@@ -19,7 +30,7 @@ Language updates

1930* Name binding in patterns follows the same rule as name binding for implicits

2031 in types: names which begin with lower case letters, not applied to any

2132 arguments, are treated as bound pattern variables.

22−* Added %deprecate directive, which gives a warning and a message when a

33+* Added %deprecate directive, which gives a warning and a message when a

2334 deprecated name is referenced.

2435

2536Library updates

@@ -39,7 +50,7 @@ Library updates

3950 from Effectful programs.

4051* Some constructors that never actually occurred have been removed from

4152 the TT and Raw reflection datatypes in Language.Reflection.

42−* File IO operations (for example openFile/fread/fwrite) now return

53+* File IO operations (for example openFile/fread/fwrite) now return

4354 'Either FileError ty' where the return type was previously 'ty' to indicate

4455 that they may fail.

4556

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+60−14

@@ -699,6 +699,13 @@ setLogLevel l = do i <- getIState

699699 let opt' = opts { opt_logLevel = l }

700700 putIState $ i { idris_options = opt' }

701701

702+setLogCats :: [LogCat] -> Idris ()

703+setLogCats cs = do

704+ i <- getIState

705+ let opts = idris_options i

706+ let opt' = opts { opt_logcats = cs }

707+ putIState $ i { idris_options = opt' }

708+

702709setCmdLine :: [Opt] -> Idris ()

703710setCmdLine opts = do i <- getIState

704711 let iopts = idris_options i

@@ -969,15 +976,55 @@ setColour ct c = do i <- getIState

969976 setColour' PromptColour c t = t { promptColour = c }

970977 setColour' PostulateColour c t = t { postulateColour = c }

971978

979+

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

973−logLvl l str = do i <- getIState

974− let lvl = opt_logLevel (idris_options i)

975− when (lvl >= l) $

976− case idris_outputmode i of

977− RawOutput h -> do runIO $ hPutStrLn h str

978− IdeMode n h ->

979− do let good = SexpList [IntegerAtom (toInteger l), toSExp str]

980− runIO . hPutStrLn h $ convSExp "log" good n

981+logLvl = logLvlCats []

982+

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

984+logCoverage = logLvlCats [ICoverage]

985+

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

987+logErasure = logLvlCats [IErasure]

988+

989+-- | Log an action of the parser

990+logParser :: Int -> String -> Idris ()

991+logParser = logLvlCats parserCats

992+

993+-- | Log an action of the elaborator.

994+logElab :: Int -> String -> Idris ()

995+logElab = logLvlCats elabCats

996+

997+-- | Log an action of the compiler.

998+logCodeGen :: Int -> String -> Idris ()

999+logCodeGen = logLvlCats codegenCats

1000+

1001+logIBC :: Int -> String -> Idris ()

1002+logIBC = logLvlCats [IIBC]

1003+

1004+-- | Log aspect of Idris execution

1005+--

1006+-- An empty set of logging levels is used to denote all categories.

1007+--

1008+-- @TODO update IDE protocol

1009+logLvlCats :: [LogCat] -- ^ The categories that the message should appear under.

1010+ -> Int -- ^ The Logging level the message should appear.

1011+ -> String -- ^ The message to show the developer.

1012+ -> Idris ()

1013+logLvlCats cs l str = do

1014+ i <- getIState

1015+ let lvl = opt_logLevel (idris_options i)

1016+ let cats = opt_logcats (idris_options i)

1017+ when (lvl >= l) $

1018+ when (inCat cs cats || null cats) $

1019+ case idris_outputmode i of

1020+ RawOutput h -> do

1021+ runIO $ hPutStrLn h str

1022+ IdeMode n h -> do

1023+ let good = SexpList [IntegerAtom (toInteger l), toSExp str]

1024+ runIO . hPutStrLn h $ convSExp "log" good n

1025+ where

1026+ inCat :: [LogCat] -> [LogCat] -> Bool

1027+ inCat cs cats = or $ map (\x -> elem x cats) cs

9811028

9821029cmdOptType :: Opt -> Idris Bool

9831030cmdOptType x = do i <- getIState

@@ -1396,7 +1443,7 @@ getUnboundImplicits i t tm = getImps t (collectImps tm)

13961443 scopedimpl (Just i) = not (toplevel_imp i)

13971444 scopedimpl _ = False

13981445

1399− getImps (Bind n (Pi i _ _) sc) imps

1446+ getImps (Bind n (Pi i _ _) sc) imps

14001447 | scopedimpl i = getImps sc imps

14011448 getImps (Bind n (Pi _ t _) sc) imps

14021449 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps

@@ -1628,7 +1675,7 @@ addImpl' inpat env infns imp_meths ist ptm

16281675 ai inpat qq env ds (PApp fc ftm@(PRef ffc hl f) as)

16291676 | f `elem` infns = ai inpat qq env ds (PApp fc (PInferRef ffc hl f) as)

16301677 | not (f `elem` map fst env)

1631− = let as' = map (fmap (ai inpat qq env ds)) as

1678+ = let as' = map (fmap (ai inpat qq env ds)) as

16321679 asdotted' = map (fmap (ai False qq env ds)) as in

16331680 handleErr $ aiFn topname inpat False qq imp_meths ist fc f ffc ds as' asdotted'

16341681 | Just (Just ty) <- lookup f env =

@@ -1707,7 +1754,7 @@ aiFn :: Name -> Bool -> Bool -> Bool

17071754 -> Either Err PTerm

17081755aiFn topname inpat True qq imp_meths ist fc f ffc ds [] _

17091756 | inpat && implicitable f && unqualified f = Right $ PPatvar ffc f

1710− | otherwise

1757+ | otherwise

17111758 = case lookupDef f (tt_ctxt ist) of

17121759 [] -> Right $ PPatvar ffc f

17131760 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in

@@ -1743,7 +1790,7 @@ aiFn topname inpat expat qq imp_meths ist fc f ffc ds as asexp

17431790 [] -> nh

17441791 x -> x

17451792 case ns' of

1746− [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))

1793+ [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))

17471794 (insertImpl ns (chooseArgs f' as asexp))

17481795 [] -> if f `elem` (map fst (idris_metavars ist))

17491796 then Right $ PApp fc (PRef ffc [ffc] f) as

@@ -2173,7 +2220,7 @@ shadow n n' t = sm 0 t where

21732220-- | Rename any binders which are repeated (so that we don't have to mess

21742221-- about with shadowing anywhere else).

21752222mkUniqueNames :: [Name] -> [(Name, Name)] -> PTerm -> PTerm

2176−mkUniqueNames env shadows tm

2223+mkUniqueNames env shadows tm

21772224 = evalState (mkUniq 0 initMap tm) (S.fromList env) where

21782225

21792226 initMap = M.fromList shadows

@@ -2295,4 +2342,3 @@ mkUniqueNames env shadows tm

22952342 mkUniq ql nmap (PUnquote tm) = fmap PUnquote (mkUniq (ql - 1) nmap tm)

22962343

22972344 mkUniq ql nmap tm = descendM (mkUniq ql nmap) tm

2298−

src/Idris/AbsSyntaxTree.hs+61−37

@@ -68,34 +68,36 @@ toplevel = EInfo [] emptyContext id Nothing Nothing (\_ _ _ -> fail "Not impleme

6868eInfoNames :: ElabInfo -> [Name]

6969eInfoNames info = map fst (params info) ++ M.keys (inblock info)

7070

71−data IOption = IOption { opt_logLevel :: Int,

72− opt_typecase :: Bool,

73− opt_typeintype :: Bool,

74− opt_coverage :: Bool,

75− opt_showimp :: Bool, -- ^^ show implicits

76− opt_errContext :: Bool,

77− opt_repl :: Bool,

78− opt_verbose :: Bool,

79− opt_nobanner :: Bool,

80− opt_quiet :: Bool,

81− opt_codegen :: Codegen,

82− opt_outputTy :: OutputType,

83− opt_ibcsubdir :: FilePath,

84− opt_importdirs :: [FilePath],

85− opt_triple :: String,

86− opt_cpu :: String,

87− opt_cmdline :: [Opt], -- remember whole command line

88− opt_origerr :: Bool,

89− opt_autoSolve :: Bool, -- ^ automatically apply "solve" tactic in prover

90− opt_autoImport :: [FilePath], -- ^ e.g. Builtins+Prelude

91− opt_optimise :: [Optimisation],

92− opt_printdepth :: Maybe Int,

93− opt_evaltypes :: Bool, -- ^ normalise types in :t

94− opt_desugarnats :: Bool

95− }

96− deriving (Show, Eq)

71+data IOption = IOption {

72+ opt_logLevel :: Int

73+ , opt_logcats :: [LogCat] -- ^ List of logging categories.

74+ , opt_typecase :: Bool

75+ , opt_typeintype :: Bool

76+ , opt_coverage :: Bool

77+ , opt_showimp :: Bool -- ^ show implicits

78+ , opt_errContext :: Bool

79+ , opt_repl :: Bool

80+ , opt_verbose :: Bool

81+ , opt_nobanner :: Bool

82+ , opt_quiet :: Bool

83+ , opt_codegen :: Codegen

84+ , opt_outputTy :: OutputType

85+ , opt_ibcsubdir :: FilePath

86+ , opt_importdirs :: [FilePath]

87+ , opt_triple :: String

88+ , opt_cpu :: String

89+ , opt_cmdline :: [Opt] -- remember whole command line

90+ , opt_origerr :: Bool

91+ , opt_autoSolve :: Bool -- ^ automatically apply "solve" tactic in prover

92+ , opt_autoImport :: [FilePath] -- ^ e.g. Builtins+Prelude

93+ , opt_optimise :: [Optimisation]

94+ , opt_printdepth :: Maybe Int

95+ , opt_evaltypes :: Bool -- ^ normalise types in :t

96+ , opt_desugarnats :: Bool

97+ } deriving (Show, Eq)

9798

9899defaultOpts = IOption { opt_logLevel = 0

100+ , opt_logcats = []

99101 , opt_typecase = False

100102 , opt_typeintype = False

101103 , opt_coverage = True

@@ -135,7 +137,7 @@ defaultOptimise = [PETransform]

135137

136138-- | Pretty printing options with default verbosity.

137139defaultPPOption :: PPOption

138−defaultPPOption = PPOption { ppopt_impl = False,

140+defaultPPOption = PPOption { ppopt_impl = False,

139141 ppopt_desugarnats = False,

140142 ppopt_pinames = False,

141143 ppopt_depth = Just 200 }

@@ -406,6 +408,7 @@ data Command = Quit

406408 | Proofs

407409 | Universes

408410 | LogLvl Int

411+ | LogCategory [LogCat]

409412 | Spec PTerm

410413 | WHNF PTerm

411414 | TestInline PTerm

@@ -451,6 +454,26 @@ data Command = Quit

451454

452455data OutputFmt = HTMLOutput | LaTeXOutput

453456

457+-- | Recognised logging categories for the Idris compiler.

458+--

459+-- @TODO add in sub categories.

460+data LogCat = IParse

461+ | IElab

462+ | ICodeGen

463+ | IErasure

464+ | ICoverage

465+ | IIBC

466+ deriving (Show, Eq, Ord)

467+

468+codegenCats :: [LogCat]

469+codegenCats = [ICodeGen]

470+

471+parserCats :: [LogCat]

472+parserCats = [IParse]

473+

474+elabCats :: [LogCat]

475+elabCats = [IElab]

476+

454477data Opt = Filename String

455478 | Quiet

456479 | NoBanner

@@ -466,6 +489,7 @@ data Opt = Filename String

466489 | NoBuiltins -- only for the really primitive stuff!

467490 | NoREPL

468491 | OLogging Int

492+ | OLogCats [LogCat]

469493 | Output String

470494 | Interface

471495 | TypeCase

@@ -767,7 +791,7 @@ data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype

767791 | PLaterdecl { d_name :: Name, d_name_fc :: FC, d_tcon :: t }

768792 -- ^ "Placeholder" for data whose constructors are defined later

769793 deriving Functor

770−

794+

771795-- | Transform the FCs in a PData and its associated terms. The first

772796-- function transforms the general-purpose FCs, and the second transforms

773797-- those that are used for semantic source highlighting, so they can be

@@ -1088,7 +1112,7 @@ data PTactic' t = Intro [Name] | Intros | Focus Name

10881112 | MatchRefine Name

10891113 | LetTac Name t | LetTacTy Name t t

10901114 | Exact t | Compute | Trivial | TCInstance

1091− | ProofSearch Bool Bool Int (Maybe Name)

1115+ | ProofSearch Bool Bool Int (Maybe Name)

10921116 [Name] -- allowed local names

10931117 [Name] -- hints

10941118 -- ^ the bool is whether to search recursively

@@ -1179,7 +1203,7 @@ type PDo = PDo' PTerm

11791203data PArg' t = PImp { priority :: Int,

11801204 machine_inf :: Bool, -- true if the machine inferred it

11811205 argopts :: [ArgOpt],

1182− pname :: Name,

1206+ pname :: Name,

11831207 getTm :: t }

11841208 | PExp { priority :: Int,

11851209 argopts :: [ArgOpt],

@@ -1890,7 +1914,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

18901914 bracket p funcAppPrec . group . align . hang 2 $

18911915 text "%runElab" <$>

18921916 prettySe (decD d) funcAppPrec bnd tm

1893− prettySe d p bnd (PConstSugar fc tm) = prettySe d p bnd tm -- should never occur, but harmless

1917+ prettySe d p bnd (PConstSugar fc tm) = prettySe d p bnd tm -- should never occur, but harmless

18941918

18951919 prettySe d p bnd _ = text "missing pretty-printer for term"

18961920

@@ -2137,7 +2161,7 @@ showTm ist = displayDecorated (consoleDecorate ist) .

21372161showTmImpls :: PTerm -> String

21382162showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""

21392163

2140−-- | Show a term with specific options

2164+-- | Show a term with specific options

21412165showTmOpts :: PPOption -> PTerm -> String

21422166showTmOpts opt = flip (displayS . renderPretty 1.0 10000000 . prettyImp opt) ""

21432167

@@ -2253,7 +2277,7 @@ boundNamesIn tm = S.toList (ni 0 S.empty tm)

22532277

22542278-- Return names which are valid implicits in the given term (type).

22552279implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]

2256−implicitNamesIn uvars ist tm

2280+implicitNamesIn uvars ist tm

22572281 = let (imps, fns) = execState (ni 0 [] tm) ([], []) in

22582282 nub imps \\ nub fns

22592283 where

@@ -2282,15 +2306,15 @@ implicitNamesIn uvars ist tm

22822306 ni 0 env (PRef _ _ n)

22832307 | not (n `elem` env) && implicitable n || n `elem` uvars = addImp n

22842308 ni 0 env (PApp _ f@(PRef _ _ n) as)

2285− | n `elem` uvars = do ni 0 env f

2309+ | n `elem` uvars = do ni 0 env f

22862310 mapM_ (ni 0 env) (map getTm as)

22872311 | otherwise = do case lookupTy n (tt_ctxt ist) of

22882312 [] -> return ()

22892313 _ -> addFn n

22902314 mapM_ (ni 0 env) (map getTm as)

2291− ni 0 env (PApp _ f as) = do ni 0 env f

2315+ ni 0 env (PApp _ f as) = do ni 0 env f

22922316 mapM_ (ni 0 env) (map getTm as)

2293− ni 0 env (PAppBind _ f as) = do ni 0 env f

2317+ ni 0 env (PAppBind _ f as) = do ni 0 env f

22942318 mapM_ (ni 0 env) (map getTm as)

22952319 ni 0 env (PCase _ c os) = do ni 0 env c

22962320 -- names in 'os', not counting the names bound in the cases

@@ -2307,7 +2331,7 @@ implicitNamesIn uvars ist tm

23072331 ni 0 env (PTyped l r) = do ni 0 env l; ni 0 env r

23082332 ni 0 env (PPair _ _ _ l r) = do ni 0 env l; ni 0 env r

23092333 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = do ni 0 env t; ni 0 (n:env) r

2310− ni 0 env (PDPair _ _ _ l t r) = do ni 0 env l

2334+ ni 0 env (PDPair _ _ _ l t r) = do ni 0 env l

23112335 ni 0 env t

23122336 ni 0 env r

23132337 ni 0 env (PAlternative ns a as) = mapM_ (ni 0 env) as

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+36−8

@@ -86,6 +86,11 @@ parseFlags = many $

8686 <|> (Client <$> strOption (long "client"))

8787 -- Logging Flags

8888 <|> (OLogging <$> option auto (long "log" <> metavar "LEVEL" <> help "Debugging log level"))

89+ <|> (OLogCats <$> option (str >>= parseLogCats)

90+ (long "logging-categories"

91+ <> metavar "CATS"

92+ <> help "Colon separated logging categories: parser, elab, codegen, coverage, erasure"))

93+

8994 -- Turn off Certain libraries.

9095 <|> flag' NoBasePkgs (long "nobasepkgs" <> help "Do not use the given base package")

9196 <|> flag' NoPrelude (long "noprelude" <> help "Do not use the given prelude")

@@ -161,21 +166,44 @@ parseVersion :: Parser (a -> a)

161166parseVersion = infoOption ver (short 'v' <> long "version" <> help "Print version information")

162167

163168preProcOpts :: [Opt] -> [Opt] -> [Opt]

164−preProcOpts [] ys = ys

169+preProcOpts [] ys = ys

165170preProcOpts (NoBuiltins:xs) ys = NoBuiltins : NoPrelude : preProcOpts xs ys

166−preProcOpts (Output s:xs) ys = Output s : NoREPL : preProcOpts xs ys

167−preProcOpts (BCAsm s:xs) ys = BCAsm s : NoREPL : preProcOpts xs ys

168−preProcOpts (x:xs) ys = preProcOpts xs (x:ys)

171+preProcOpts (Output s:xs) ys = Output s : NoREPL : preProcOpts xs ys

172+preProcOpts (BCAsm s:xs) ys = BCAsm s : NoREPL : preProcOpts xs ys

173+preProcOpts (x:xs) ys = preProcOpts xs (x:ys)

169174

170175parseCodegen :: String -> Codegen

171176parseCodegen "bytecode" = Bytecode

172−parseCodegen cg = Via (map toLower cg)

173−

174−

177+parseCodegen cg = Via (map toLower cg)

175178

179+parseLogCats :: Monad m => String -> m [LogCat]

180+parseLogCats s =

181+ case lastMay (readP_to_S (doParse) s) of

182+ Just (xs, _) -> return xs

183+ _ -> fail $ "Incorrect categories specified"

184+ where

185+ doParse :: ReadP [LogCat]

186+ doParse = do

187+ cs <- sepBy1 parseLogCat (char ':')

188+ eof

189+ return (concat cs)

190+

191+ parseLogCat :: ReadP [LogCat]

192+ parseLogCat = (string "parser" *> return parserCats)

193+ <|> (string "elab" *> return elabCats)

194+ <|> (string "codegen" *> return codegenCats)

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

196+ <|> (string "ibc" *> return [IIBC])

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

198+ <|> parseLogCatBad

199+

200+ parseLogCatBad :: ReadP [LogCat]

201+ parseLogCatBad = do

202+ s <- look

203+ fail $ "Category: " ++ s ++ " is not recognised."

176204

177205parseConsoleWidth :: Monad m => String -> m ConsoleWidth

178−parseConsoleWidth "auto" = return AutomaticWidth

206+parseConsoleWidth "auto" = return AutomaticWidth

179207parseConsoleWidth "infinite" = return InfinitelyWide

180208parseConsoleWidth s =

181209 case lastMay (readP_to_S (integerReader) s) of

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/DeepSeq.hs+8−3

@@ -116,6 +116,7 @@ instance NFData Opt where

116116 rnf (NoBuiltins) = ()

117117 rnf (NoREPL) = ()

118118 rnf (OLogging i) = rnf i `seq` ()

119+ rnf (OLogCats cs) = rnf cs `seq` ()

119120 rnf (Output str) = rnf str `seq` ()

120121 rnf (Interface) = ()

121122 rnf (TypeCase) = ()

@@ -174,6 +175,7 @@ instance NFData TIData where

174175instance NFData IOption where

175176 rnf (IOption

176177 opt_logLevel

178+ opt_logcats

177179 opt_typecase

178180 opt_typeintype

179181 opt_coverage

@@ -226,7 +228,7 @@ instance NFData IOption where

226228instance NFData LanguageExt where

227229 rnf TypeProviders = ()

228230 rnf ErrorReflection = ()

229−

231+

230232instance NFData Optimisation where

231233 rnf PETransform = ()

232234

@@ -358,6 +360,9 @@ instance NFData Codegen where

358360 rnf (Via x1) = rnf x1 `seq` ()

359361 rnf Bytecode = ()

360362

363+instance NFData LogCat where

364+ rnf _ = ()

365+

361366instance NFData CGInfo where

362367 rnf (CGInfo x1 x2 x3 x4 x5)

363368 = rnf x1 `seq`

@@ -563,7 +568,7 @@ instance NFData PTerm where

563568instance NFData PAltType where

564569 rnf (ExactlyOne x1) = rnf x1 `seq` ()

565570 rnf FirstSuccess = ()

566− rnf TryImplicit = ()

571+ rnf TryImplicit = ()

567572

568573instance (NFData t) => NFData (PTactic' t) where

569574 rnf (Intro x1) = rnf x1 `seq` ()

@@ -687,7 +692,7 @@ instance NFData OutputMode where

687692

688693

689694instance NFData IState where

690− rnf (IState x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20

695+ rnf (IState x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20

691696 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40

692697 x41 x42 x43 x44 x45 x46 x47 x48 x49 x50 x51 x52 x53 x54 x55 x56 x57 x58 x59 x60

693698 x61 x62 x63 x64 x65 x66 x67 x68 x69 x70 x71 x72 x73 x74)

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 logIBC 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 logIBC 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+ logIBC 1 "Written")

202+ (\c -> do logIBC 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+ logIBC 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+ logIBC 1 "Written")

218+ (\c -> do logIBC 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+ logIBC 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+ logIBC 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+ logIBC 1 $ "Failed at " ++ fn

420+ ifail "Must be an ibc"

421+ IDR fn -> do

422+ logIBC 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 logIBC 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 logIBC 1 $ "Not exporting " ++ show n

523525 setAccessibility n Hidden

524− else logLvl 1 $ "Exporting " ++ show n) ds

526+ else logIBC 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+ logIBC 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+13−13

@@ -189,7 +189,7 @@ decl syn = try (externalDecl syn)

189189 <?> "declaration"

190190

191191internalDecl :: SyntaxInfo -> IdrisParser [PDecl]

192−internalDecl syn

192+internalDecl syn

193193 = do fc <- getFC

194194 -- if we're after maxline, stop at the next type declaration

195195 -- (so we get all cases of a definition to preserve totality

@@ -204,7 +204,7 @@ internalDecl syn

204204 -- the end of the definition, reset the state. But I've lost

205205 -- patience with trying to find out how to do that from the

206206 -- trifecta docs, so this does the job instead.

207− if continue then

207+ if continue then

208208 do notEndBlock

209209 declBody continue

210210 else try (do notEndBlock

@@ -283,7 +283,7 @@ declExtensions syn rules = declExtension syn [] (filter isDeclRule rules)

283283 isDeclRule (DeclRule _ _) = True

284284 isDeclRule _ = False

285285

286−declExtension :: SyntaxInfo -> [Maybe (Name, SynMatch)] -> [Syntax]

286+declExtension :: SyntaxInfo -> [Maybe (Name, SynMatch)] -> [Syntax]

287287 -> IdrisParser [PDecl]

288288declExtension syn ns rules =

289289 choice $ flip map (groupBy (ruleGroup `on` syntaxSymbols) rules) $ \rs ->

@@ -318,7 +318,7 @@ declExtension syn ns rules =

318318 updateNs :: [(Name, SynMatch)] -> PDecl -> PDecl

319319 updateNs ns (PTy doc argdoc s fc o n fc' t)

320320 = PTy doc argdoc s fc o (updateB ns n) fc' t

321− updateNs ns (PClauses fc o n cs)

321+ updateNs ns (PClauses fc o n cs)

322322 = PClauses fc o (updateB ns n) (map (updateClause ns) cs)

323323 updateNs ns (PCAF fc n t) = PCAF fc (updateB ns n) t

324324 updateNs ns (PData ds cds s fc o dat)

@@ -338,10 +338,10 @@ declExtension syn ns rules =

338338 cdocs

339339 updateNs ns (PInstance docs pdocs s fc cs cn fc' ps ity ni ds)

340340 = PInstance docs pdocs s fc cs (updateB ns cn) fc'

341− ps ity (fmap (updateB ns) ni)

341+ ps ity (fmap (updateB ns) ni)

342342 (map (updateNs ns) ds)

343343 updateNs ns (PMutual fc ds) = PMutual fc (map (updateNs ns) ds)

344− updateNs ns (PProvider docs s fc fc' pw n)

344+ updateNs ns (PProvider docs s fc fc' pw n)

345345 = PProvider docs s fc fc' pw (updateB ns n)

346346 updateNs ns d = d

347347

@@ -482,7 +482,7 @@ syntaxRule syn

482482 where ts = dropWhile isSpace . dropWhileEnd isSpace $ s

483483 mkSimple' (e : es) = e : mkSimple' es

484484 mkSimple' [] = []

485−

485+

486486 -- Prevent syntax variable capture by making all binders under syntax unique

487487 -- (the ol' Common Lisp GENSYM approach)

488488 uniquifyBinders :: [Name] -> PTerm -> IdrisParser PTerm

@@ -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+24−22

@@ -801,11 +801,11 @@ 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

808− let tm' = perhapsForce $ normaliseBlocking ctxt []

808+ let tm' = perhapsForce $ normaliseBlocking ctxt []

809809 [sUN "foreign",

810810 sUN "prim_read",

811811 sUN "prim_write"]

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

@@ -951,10 +951,10 @@ process fn (Check (PRef _ _ n))

951951 = let current = case n of

952952 MN _ _ -> text ""

953953 UN nm | ('_':'_':_) <- str nm -> text ""

954− _ -> text " " <>

954+ _ -> text " " <>

955955 bindingOf n False

956− <+> colon

957− <+> align (tPretty bnd ist t)

956+ <+> colon

957+ <+> align (tPretty bnd ist t)

958958 <> line

959959 in

960960 current <> putTy ppo ist (i-1) ((n,False):bnd) sc

@@ -986,8 +986,8 @@ process fn (Core t)

986986 iPrintTermWithType (pprintTT [] tm) (pprintTT [] ty)

987987

988988process fn (DocStr (Left n) w)

989− | UN ty <- n, ty == T.pack "Type" = getIState >>= iRenderResult . pprintTypeDoc

990− | otherwise = do

989+ | UN ty <- n, ty == T.pack "Type" = getIState >>= iRenderResult . pprintTypeDoc

990+ | otherwise = do

991991 ist <- getIState

992992 let docs = lookupCtxtName n (idris_docstrings ist) ++

993993 map (\(n,d)-> (n, (d, [])))

@@ -1010,7 +1010,7 @@ process fn (DocStr (Right c) _) -- constants only have overviews

10101010process fn Universes

10111011 = do i <- getIState

10121012 let cs = idris_constraints i

1013− let cslist = S.toAscList cs

1013+ let cslist = S.toAscList cs

10141014-- iputStrLn $ showSep "\n" (map show cs)

10151015 iputStrLn $ show (map uconstraint cslist)

10161016 let n = length cslist

@@ -1226,6 +1226,7 @@ process fn (Compile codegen f)

12261226 runIO $ generate codegen (fst (head (idris_imported i))) ir

12271227 where fc = fileFC "main"

12281228process fn (LogLvl i) = setLogLevel i

1229+process fn (LogCategory cs) = setLogCats cs

12291230-- Elaborate as if LHS of a pattern (debug command)

12301231process fn (Pattelab t)

12311232 = do (tm, ty) <- elabVal recinfo ELHS t

@@ -1252,7 +1253,7 @@ process fn (DynamicLink l)

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

12531254 Just x -> do let libs = idris_dynamic_libs i

12541255 if x `elem` libs

1255− 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)

12561257 return ()

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

12581259 where trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace

@@ -1523,18 +1524,18 @@ loadInputs inputs toline -- furthest line to read in input source files

15231524

15241525 importlists <- getImports [] inputs

15251526

1526− 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))

15271528

15281529 let ninputs = zip [1..] inputs

15291530 ifiles <- mapWhileOK (\(num, input) ->

15301531 do putIState ist

1531− modTree <- buildTree

1532+ modTree <- buildTree

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

15331534 importlists

15341535 input

15351536 let ifiles = getModuleFiles modTree

1536− logLvl 1 ("MODULE TREE : " ++ show modTree)

1537− logLvl 1 ("RELOAD: " ++ show ifiles)

1537+ logParser 1 ("MODULE TREE : " ++ show modTree)

1538+ logParser 1 ("RELOAD: " ++ show ifiles)

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

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

15401541 -- return the files that need rechecking

@@ -1777,12 +1778,13 @@ idrisMain opts =

17771778 ok <- noErrors

17781779 when (not ok) $ runIO (exitWith (ExitFailure 1))

17791780 where

1780− makeOption (OLogging i) = setLogLevel i

1781− makeOption TypeCase = setTypeCase True

1782− makeOption TypeInType = setTypeInType True

1783− makeOption NoCoverage = setCoverage False

1784− makeOption ErrContext = setErrContext True

1785− makeOption _ = return ()

1781+ makeOption (OLogging i) = setLogLevel i

1782+ makeOption (OLogCats cs) = setLogCats cs

1783+ makeOption TypeCase = setTypeCase True

1784+ makeOption TypeInType = setTypeInType True

1785+ makeOption NoCoverage = setCoverage False

1786+ makeOption ErrContext = setErrContext True

1787+ makeOption _ = return ()

17861788

17871789 addPkgDir :: String -> Idris ()

17881790 addPkgDir p = do ddir <- runIO $ getIdrisLibDir

src/Idris/REPLParser.hs+34−11

@@ -43,11 +43,11 @@ setOptions = [("errorcontext", ErrContext),

4343 ("desugarnats", DesugarNats)]

4444

4545help :: [([String], CmdArg, String)]

46−help = (["<expr>"], NoArg, "Evaluate an expression") :

46+help = (["<expr>"], NoArg, "Evaluate an expression") :

4747 [ (map (':' :) names, args, text) | (names, args, text, _) <- parserCommandsForHelp ]

4848

4949allHelp :: [([String], CmdArg, String)]

50−allHelp = [ (map (':' :) names, args, text)

50+allHelp = [ (map (':' :) names, args, text)

5151 | (names, args, text, _) <- parserCommandsForHelp ++ parserCommands ]

5252

5353parserCommandsForHelp :: CommandTable

@@ -124,7 +124,7 @@ parserCommands =

124124 , exprArgCmd ["spec"] Spec "?"

125125 , exprArgCmd ["whnf"] WHNF "(Debugging) Show weak head normal form of an expression"

126126 , exprArgCmd ["inline"] TestInline "?"

127− , proofArgCmd ["cs", "casesplit"] CaseSplitAt

127+ , proofArgCmd ["cs", "casesplit"] CaseSplitAt

128128 ":cs <line> <name> splits the pattern variable on the line"

129129 , proofArgCmd ["apc", "addproofclause"] AddProofClauseFrom

130130 ":apc <line> <name> adds a pattern-matching proof clause to name on line"

@@ -138,6 +138,10 @@ parserCommands =

138138 ":mc <line> <name> adds a case block for the definition of the metavariable on the line"

139139 , proofArgCmd ["ml", "makelemma"] MakeLemma "?"

140140 , (["log"], NumberArg, "Set logging verbosity level", cmd_log)

141+ , ( ["logcats"]

142+ , ManyArgs NameArg

143+ , "Set logging categories"

144+ , cmd_cats)

141145 , (["lto", "loadto"], SeqArgs NumberArg FileArg

142146 , "Load file up to line number", cmd_loadto)

143147 , (["ps", "proofsearch"], NoArg

@@ -148,8 +152,8 @@ parserCommands =

148152 , cmd_refine)

149153 , (["debugunify"], SeqArgs ExprArg ExprArg

150154 , "(Debugging) Try to unify two expressions", const $ do

151− l <- P.simpleExpr defaultSyntax

152− r <- P.simpleExpr defaultSyntax

155+ l <- P.simpleExpr defaultSyntax

156+ r <- P.simpleExpr defaultSyntax

153157 eof

154158 return (Right (DebugUnify l r))

155159 )

@@ -171,9 +175,9 @@ proofArgCmd names command doc =

171175 (names, NoArg, doc, proofArg command)

172176

173177pCmd :: P.IdrisParser (Either String Command)

174−pCmd = choice [ do c <- cmd names; parser c

178+pCmd = choice [ do c <- cmd names; parser c

175179 | (names, _, _, parser) <- parserCommandsForHelp ++ parserCommands ]

176− <|> unrecognized

180+ <|> unrecognized

177181 <|> nop

178182 <|> eval

179183 where nop = do eof; return (Right NOP)

@@ -227,7 +231,7 @@ exprArg cmd name = do

227231

228232

229233

230−genArg :: String -> P.IdrisParser a -> (a -> Command)

234+genArg :: String -> P.IdrisParser a -> (a -> Command)

231235 -> String -> P.IdrisParser (Either String Command)

232236genArg argName argParser cmd name = do

233237 let emptyArgs = do eof; failure

@@ -246,12 +250,12 @@ strArg :: (String -> Command) -> String -> P.IdrisParser (Either String Command)

246250strArg = genArg "string" (many anyChar)

247251

248252moduleArg :: (FilePath -> Command) -> String -> P.IdrisParser (Either String Command)

249−moduleArg = genArg "module" (fmap (toPath . fst) P.identifier)

253+moduleArg = genArg "module" (fmap (toPath . fst) P.identifier)

250254 where

251255 toPath n = foldl1' (</>) $ splitOn "." n

252256

253257namespaceArg :: ([String] -> Command) -> String -> P.IdrisParser (Either String Command)

254−namespaceArg = genArg "namespace" (fmap (toNS . fst) P.identifier)

258+namespaceArg = genArg "namespace" (fmap (toNS . fst) P.identifier)

255259 where

256260 toNS = splitOn "."

257261

@@ -290,7 +294,7 @@ cmd_doc name = do

290294 c <- fmap fst P.constant

291295 eof

292296 return $ Right (DocStr (Right c) FullDocs)

293−

297+

294298 let pType = do

295299 P.reserved "Type"

296300 eof

@@ -392,6 +396,25 @@ cmd_log name = do

392396 eof

393397 return (Right (LogLvl i))

394398

399+cmd_cats :: String -> P.IdrisParser (Either String Command)

400+cmd_cats name = do

401+ cs <- sepBy pLogCats (P.whiteSpace)

402+ eof

403+ return $ Right $ LogCategory (concat cs)

404+ where

405+ badCat = do

406+ c <- fst <$> P.identifier

407+ fail $ "Category: " ++ c ++ " is not recognised."

408+

409+ 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)

413+ <|> try (P.symbol "coverage" >> return [ICoverage])

414+ <|> try (P.symbol "ibc" >> return [IIBC])

415+ <|> try (P.symbol "erasure" >> return [IErasure])

416+ <|> badCat

417+

395418cmd_let :: String -> P.IdrisParser (Either String Command)

396419cmd_let name = do

397420 defn <- concat <$> many (P.decl defaultSyntax)