5dc9d1a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Updated logging categories.

Simplified the logging categories to three: + Parser :: Reading Idris Files + Elab :: Type Checking + CodeGen :: Code Generation. Renamed command line flag to `logging-categories`.

commit5dc9d1af6e5e0a8e32c63dda6320a810daf9f867 authorJan de Muijnck-Hughes <jfdm@st-andrews.ac.uk> dateFri 18 Dec 2015, 12:53 (11 years ago) parentd901c69

4 files changed+19−70

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+6−32 src/Idris/AbsSyntaxTree.hs+6−11 src/Idris/CmdOptions.hs+5−15 src/Idris/REPLParser.hs+2−12

src/Idris/AbsSyntax.hs+6−32

@@ -980,44 +980,18 @@ setColour ct c = do i <- getIState

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

981981logLvl = logLvlCats []

982982

983+-- | Log an action of the parser

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

984985logParser = logLvlCats parserCats

985986

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

987−logParse = logLvlCats [IParse]

988−

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

990−logTypeChecking = logLvlCats checkingCats

991−

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

992988logElab :: 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]

989+logElab = logLvlCats elabCats

1018990

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

1019992logCodeGen :: Int -> String -> Idris ()

1020−logCodeGen = logLvlCats [ICodeGen]

993+logCodeGen = logLvlCats codegenCats

994+

1021995

1022996-- | Log aspect of Idris execution

1023997--

src/Idris/AbsSyntaxTree.hs+6−11

@@ -455,26 +455,21 @@ data Command = Quit

455455data OutputFmt = HTMLOutput | LaTeXOutput

456456

457457-- | Recognised logging categories for the Idris compiler.

458+--

459+-- @TODO add in sub categories.

458460data LogCat = IParse

459461 | IElab

460− | ICover

461− | IUnify

462− | ITotal

463− | IErase

464− | IDefun

465− | IInline

466− | IResolve

467462 | ICodeGen

468463 deriving (Show, Eq, Ord)

469464

470−backendCats :: [LogCat]

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

465+codegenCats :: [LogCat]

466+codegenCats = [ICodeGen]

472467

473468parserCats :: [LogCat]

474469parserCats = [IParse]

475470

476−checkingCats :: [LogCat]

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

471+elabCats :: [LogCat]

472+elabCats = [IElab]

478473

479474data Opt = Filename String

480475 | Quiet

src/Idris/CmdOptions.hs+5−15

@@ -87,9 +87,9 @@ parseFlags = many $

8787 -- Logging Flags

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

8989 <|> (OLogCats <$> option (str >>= parseLogCats)

90− (long "logcats"

90+ (long "logging-categories"

9191 <> metavar "CATS"

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

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

9393

9494 -- Turn off Certain libraries.

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

@@ -189,19 +189,9 @@ parseLogCats s =

189189 return (concat cs)

190190

191191 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])

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

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

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

205195 <|> parseLogCatBad

206196

207197 parseLogCatBad :: ReadP [LogCat]

src/Idris/REPLParser.hs+2−12

@@ -408,18 +408,8 @@ cmd_cats name = do

408408

409409 pLogCats :: P.IdrisParser [LogCat]

410410 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])

411+ <|> try (P.symbol "elab" >> return elabCats)

412+ <|> try (P.symbol "codegen" >> return codegenCats)

423413 <|> badCat

424414

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