d901c69 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Initial commit for a category based logger for Idris.

Currently logging is based on horizontally defined levels across the entire language infrastructure. This commit introduces vertical splits. Logging statements record both the level the message is to be recorded at and the categories it belongs too. No categories is an alias for belonging to all categories. The State record stores both the current logging level, and also the categories to show. Logging is decided if a given logging statement is at the right level and if the categories specified are listed. By default all categories are allowed, as levels will take care of logging statement visibility.

commitd901c69fbb0f24a1f60a490134ffd25718b1a44a authorJan de Muijnck-Hughes <jfdm@st-andrews.ac.uk> dateThu 10 Dec 2015, 18:45 (11 years ago) parent10a22eb

7 files changed+256−94

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+78−14 src/Idris/AbsSyntaxTree.hs+63−37 src/Idris/CmdOptions.hs+43−8 src/Idris/DeepSeq.hs+8−3 src/Idris/Parser.hs+7−7 src/Idris/REPL.hs+16−14 src/Idris/REPLParser.hs+41−11

src/Idris/AbsSyntax.hs+78−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,73 @@ 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+logParser :: Int -> String -> Idris ()

984+logParser = logLvlCats parserCats

985+

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

987+logParse = logLvlCats [IParse]

988+

989+logTypeChecking :: Int -> String -> Idris ()

990+logTypeChecking = logLvlCats checkingCats

991+

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

993+logElab = logLvlCats [IElab]

994+

995+logCover :: Int -> String -> Idris ()

996+logCover = logLvlCats [ICover]

997+

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

999+logUnify = logLvlCats [IUnify]

1000+

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

1002+logTotal = logLvlCats [ITotal]

1003+

1004+logErase :: Int -> String -> Idris ()

1005+logErase = logLvlCats [IErase]

1006+

1007+logBackend :: Int -> String -> Idris ()

1008+logBackend = logLvlCats backendCats

1009+

1010+logDefun :: Int -> String -> Idris ()

1011+logDefun = logLvlCats [IDefun]

1012+

1013+logInline :: Int -> String -> Idris ()

1014+logInline = logLvlCats [IInline]

1015+

1016+logResolve :: Int -> String -> Idris ()

1017+logResolve = logLvlCats [IResolve]

1018+

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

1020+logCodeGen = logLvlCats [ICodeGen]

1021+

1022+-- | Log aspect of Idris execution

1023+--

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

1025+--

1026+-- @TODO update IDE protocol

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

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

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

1030+ -> Idris ()

1031+logLvlCats cs l str = do

1032+ i <- getIState

1033+ let lvl = opt_logLevel (idris_options i)

1034+ let cats = opt_logcats (idris_options i)

1035+ when (lvl >= l) $

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

1037+ case idris_outputmode i of

1038+ RawOutput h -> do

1039+ runIO $ hPutStrLn h str

1040+ IdeMode n h -> do

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

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

1043+ where

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

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

9811046

9821047cmdOptType :: Opt -> Idris Bool

9831048cmdOptType x = do i <- getIState

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

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

13971462 scopedimpl _ = False

13981463

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

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

14001465 | scopedimpl i = getImps sc imps

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

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

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

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

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

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

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

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

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

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

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

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

17071772 -> Either Err PTerm

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

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

1710− | otherwise

1775+ | otherwise

17111776 = case lookupDef f (tt_ctxt ist) of

17121777 [] -> Right $ PPatvar ffc f

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

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

17431808 [] -> nh

17441809 x -> x

17451810 case ns' of

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

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

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

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

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

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

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

21742239-- about with shadowing anywhere else).

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

2176−mkUniqueNames env shadows tm

2241+mkUniqueNames env shadows tm

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

21782243

21792244 initMap = M.fromList shadows

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

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

22962361

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

2298−

src/Idris/AbsSyntaxTree.hs+63−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,28 @@ data Command = Quit

451454

452455data OutputFmt = HTMLOutput | LaTeXOutput

453456

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

458+data LogCat = IParse

459+ | IElab

460+ | ICover

461+ | IUnify

462+ | ITotal

463+ | IErase

464+ | IDefun

465+ | IInline

466+ | IResolve

467+ | ICodeGen

468+ deriving (Show, Eq, Ord)

469+

470+backendCats :: [LogCat]

471+backendCats = [IDefun, IInline, IResolve, ICodeGen]

472+

473+parserCats :: [LogCat]

474+parserCats = [IParse]

475+

476+checkingCats :: [LogCat]

477+checkingCats = [IElab, ICover, IUnify, ITotal, IElab]

478+

454479data Opt = Filename String

455480 | Quiet

456481 | NoBanner

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

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

467492 | NoREPL

468493 | OLogging Int

494+ | OLogCats [LogCat]

469495 | Output String

470496 | Interface

471497 | TypeCase

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

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

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

769795 deriving Functor

770−

796+

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

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

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

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

10881114 | MatchRefine Name

10891115 | LetTac Name t | LetTacTy Name t t

10901116 | Exact t | Compute | Trivial | TCInstance

1091− | ProofSearch Bool Bool Int (Maybe Name)

1117+ | ProofSearch Bool Bool Int (Maybe Name)

10921118 [Name] -- allowed local names

10931119 [Name] -- hints

10941120 -- ^ the bool is whether to search recursively

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

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

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

11811207 argopts :: [ArgOpt],

1182− pname :: Name,

1208+ pname :: Name,

11831209 getTm :: t }

11841210 | PExp { priority :: Int,

11851211 argopts :: [ArgOpt],

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

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

18911917 text "%runElab" <$>

18921918 prettySe (decD d) funcAppPrec bnd tm

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

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

18941920

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

18961922

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

21372163showTmImpls :: PTerm -> String

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

21392165

2140−-- | Show a term with specific options

2166+-- | Show a term with specific options

21412167showTmOpts :: PPOption -> PTerm -> String

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

21432169

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

22532279

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

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

2256−implicitNamesIn uvars ist tm

2282+implicitNamesIn uvars ist tm

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

22582284 nub imps \\ nub fns

22592285 where

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

22822308 ni 0 env (PRef _ _ n)

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

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

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

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

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

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

22882314 [] -> return ()

22892315 _ -> addFn n

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

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

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

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

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

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

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

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

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

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

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

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

23092335 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

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

23112337 ni 0 env t

23122338 ni 0 env r

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

src/Idris/CmdOptions.hs+43−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 "logcats"

91+ <> metavar "CATS"

92+ <> help "Colon separated logging categories: parser, tychecker, backend, parse, elaborator, coverage, unifyer, totality, eraser, defunc, inliner, resolver, codegen"))

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,51 @@ 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 "tychecker" *> return checkingCats)

194+ <|> (string "backend" *> return backendCats)

195+ <|> (string "parse" *> return [IParse])

196+ <|> (string "elaborator" *> return [IElab])

197+ <|> (string "coverage" *> return [ICover])

198+ <|> (string "unifyer" *> return [IUnify])

199+ <|> (string "totality" *> return [ITotal])

200+ <|> (string "eraser" *> return [IErase])

201+ <|> (string "defunc" *> return [IDefun])

202+ <|> (string "inliner" *> return [IInline])

203+ <|> (string "resolver" *> return [IResolve])

204+ <|> (string "codegen" *> return [ICodeGen])

205+ <|> parseLogCatBad

206+

207+ parseLogCatBad :: ReadP [LogCat]

208+ parseLogCatBad = do

209+ s <- look

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

176211

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

178−parseConsoleWidth "auto" = return AutomaticWidth

213+parseConsoleWidth "auto" = return AutomaticWidth

179214parseConsoleWidth "infinite" = return InfinitelyWide

180215parseConsoleWidth s =

181216 case lastMay (readP_to_S (integerReader) s) 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/Parser.hs+7−7

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

src/Idris/REPL.hs+16−14

@@ -805,7 +805,7 @@ process fn (Eval 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"]

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

@@ -1528,7 +1529,7 @@ loadInputs inputs toline -- furthest line to read in input source files

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

@@ -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+41−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+ , ( ["logacts"]

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,32 @@ 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 "tychecker" >> return checkingCats)

412+ <|> try (P.symbol "backend" >> return backendCats)

413+ <|> try (P.symbol "parse" >> return [IParse])

414+ <|> try (P.symbol "elaborator" >> return [IElab])

415+ <|> try (P.symbol "coverage" >> return [ICover])

416+ <|> try (P.symbol "unifyer" >> return [IUnify])

417+ <|> try (P.symbol "totality" >> return [ITotal])

418+ <|> try (P.symbol "eraser" >> return [IErase])

419+ <|> try (P.symbol "defunc" >> return [IDefun])

420+ <|> try (P.symbol "inliner" >> return [IInline])

421+ <|> try (P.symbol "resolver" >> return [IResolve])

422+ <|> try (P.symbol "codegen" >> return [ICodeGen])

423+ <|> badCat

424+

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

396426cmd_let name = do

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