d901c69 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Initial commit for a category based logger for Idris.

d901c69Jan de Muijnck-Hughes11 years ago

src/Idris/AbsSyntax.hs+78−14

compare with master

unifiedsplit

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

699 let opt' = opts { opt_logLevel = l }

700 putIState $ i { idris_options = opt' }

701

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+

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

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

703setCmdLine opts = do i <- getIState

710setCmdLine opts = do i <- getIState

704 let iopts = idris_options i

711 let iopts = idris_options i

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

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

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

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

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

971

978

979+

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

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

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

973−logLvl l str = do i <- getIState

1032+ i <- getIState

974− let lvl = opt_logLevel (idris_options i)

1033+ let lvl = opt_logLevel (idris_options i)

1034+ let cats = opt_logcats (idris_options i)

975− when (lvl >= l) $

1035+ when (lvl >= l) $

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

976− case idris_outputmode i of

1037+ case idris_outputmode i of

1038+ RawOutput h -> do

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

1039+ runIO $ hPutStrLn h str

978− IdeMode n h ->

1040+ IdeMode n h -> do

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

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

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

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

981

1046

982cmdOptType :: Opt -> Idris Bool

1047cmdOptType :: Opt -> Idris Bool

983cmdOptType x = do i <- getIState

1048cmdOptType x = do i <- getIState

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

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

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

1397 scopedimpl _ = False

1462 scopedimpl _ = False

1398

1463

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

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

1400 | scopedimpl i = getImps sc imps

1465 | scopedimpl i = getImps sc imps

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1707 -> Either Err PTerm

1772 -> Either Err PTerm

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

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

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

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

1710− | otherwise

1775+ | otherwise

1711 = case lookupDef f (tt_ctxt ist) of

1776 = case lookupDef f (tt_ctxt ist) of

1712 [] -> Right $ PPatvar ffc f

1777 [] -> Right $ PPatvar ffc f

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

1778 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

1743 [] -> nh

1808 [] -> nh

1744 x -> x

1809 x -> x

1745 case ns' of

1810 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'))

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

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

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

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

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

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

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

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

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

2174-- about with shadowing anywhere else).

2239-- about with shadowing anywhere else).

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

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

2176−mkUniqueNames env shadows tm

2241+mkUniqueNames env shadows tm

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

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

2178

2243

2179 initMap = M.fromList shadows

2244 initMap = M.fromList shadows

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

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

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

2296

2361

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

2362 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

68eInfoNames :: ElabInfo -> [Name]

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

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

71+data IOption = IOption {

72+ opt_logLevel :: Int

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

72− opt_typecase :: Bool,

74+ , opt_typecase :: Bool

73− opt_typeintype :: Bool,

75+ , opt_typeintype :: Bool

74− opt_coverage :: Bool,

76+ , opt_coverage :: Bool

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

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

76− opt_errContext :: Bool,

78+ , opt_errContext :: Bool

77− opt_repl :: Bool,

79+ , opt_repl :: Bool

78− opt_verbose :: Bool,

80+ , opt_verbose :: Bool

79− opt_nobanner :: Bool,

81+ , opt_nobanner :: Bool

80− opt_quiet :: Bool,

82+ , opt_quiet :: Bool

81− opt_codegen :: Codegen,

83+ , opt_codegen :: Codegen

82− opt_outputTy :: OutputType,

84+ , opt_outputTy :: OutputType

83− opt_ibcsubdir :: FilePath,

85+ , opt_ibcsubdir :: FilePath

84− opt_importdirs :: [FilePath],

86+ , opt_importdirs :: [FilePath]

85− opt_triple :: String,

87+ , opt_triple :: String

86− opt_cpu :: String,

88+ , opt_cpu :: String

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

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

88− opt_origerr :: Bool,

90+ , opt_origerr :: Bool

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

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

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

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

91− opt_optimise :: [Optimisation],

93+ , opt_optimise :: [Optimisation]

92− opt_printdepth :: Maybe Int,

94+ , opt_printdepth :: Maybe Int

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

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

94− opt_desugarnats :: Bool

96+ , opt_desugarnats :: Bool

95− }

96− deriving (Show, Eq)

97+ } deriving (Show, Eq)

98defaultOpts = IOption { opt_logLevel = 0

99defaultOpts = IOption { opt_logLevel = 0

100+ , opt_logcats = []

99 , opt_typecase = False

101 , opt_typecase = False

100 , opt_typeintype = False

102 , opt_typeintype = False

101 , opt_coverage = True

103 , opt_coverage = True

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

135

137

136-- | Pretty printing options with default verbosity.

138-- | Pretty printing options with default verbosity.

137defaultPPOption :: PPOption

139defaultPPOption :: PPOption

138−defaultPPOption = PPOption { ppopt_impl = False,

140+defaultPPOption = PPOption { ppopt_impl = False,

139 ppopt_desugarnats = False,

141 ppopt_desugarnats = False,

140 ppopt_pinames = False,

142 ppopt_pinames = False,

141 ppopt_depth = Just 200 }

143 ppopt_depth = Just 200 }

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

406 | Proofs

408 | Proofs

407 | Universes

409 | Universes

408 | LogLvl Int

410 | LogLvl Int

411+ | LogCategory [LogCat]

409 | Spec PTerm

412 | Spec PTerm

410 | WHNF PTerm

413 | WHNF PTerm

411 | TestInline PTerm

414 | TestInline PTerm

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

451

454

452data OutputFmt = HTMLOutput | LaTeXOutput

455data OutputFmt = HTMLOutput | LaTeXOutput

453

456

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+

454data Opt = Filename String

479data Opt = Filename String

455 | Quiet

480 | Quiet

456 | NoBanner

481 | NoBanner

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

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

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

467 | NoREPL

492 | NoREPL

468 | OLogging Int

493 | OLogging Int

494+ | OLogCats [LogCat]

469 | Output String

495 | Output String

470 | Interface

496 | Interface

471 | TypeCase

497 | TypeCase

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

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

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

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

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

769 deriving Functor

795 deriving Functor

770−

796+

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

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

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

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

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

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

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

1088 | MatchRefine Name

1114 | MatchRefine Name

1089 | LetTac Name t | LetTacTy Name t t

1115 | LetTac Name t | LetTacTy Name t t

1090 | Exact t | Compute | Trivial | TCInstance

1116 | Exact t | Compute | Trivial | TCInstance

1091− | ProofSearch Bool Bool Int (Maybe Name)

1117+ | ProofSearch Bool Bool Int (Maybe Name)

1092 [Name] -- allowed local names

1118 [Name] -- allowed local names

1093 [Name] -- hints

1119 [Name] -- hints

1094 -- ^ the bool is whether to search recursively

1120 -- ^ the bool is whether to search recursively

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

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

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

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

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

1181 argopts :: [ArgOpt],

1207 argopts :: [ArgOpt],

1182− pname :: Name,

1208+ pname :: Name,

1183 getTm :: t }

1209 getTm :: t }

1184 | PExp { priority :: Int,

1210 | PExp { priority :: Int,

1185 argopts :: [ArgOpt],

1211 argopts :: [ArgOpt],

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

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

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

1891 text "%runElab" <$>

1917 text "%runElab" <$>

1892 prettySe (decD d) funcAppPrec bnd tm

1918 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

1894

1920

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

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

1896

1922

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

2137showTmImpls :: PTerm -> String

2163showTmImpls :: PTerm -> String

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

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

2139

2165

2140−-- | Show a term with specific options

2166+-- | Show a term with specific options

2141showTmOpts :: PPOption -> PTerm -> String

2167showTmOpts :: PPOption -> PTerm -> String

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

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

2143

2169

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

2253

2279

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

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

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

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

2256−implicitNamesIn uvars ist tm

2282+implicitNamesIn uvars ist tm

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

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

2258 nub imps \\ nub fns

2284 nub imps \\ nub fns

2259 where

2285 where

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

2282 ni 0 env (PRef _ _ n)

2308 ni 0 env (PRef _ _ n)

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

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

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

2310 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

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

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

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

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

2288 [] -> return ()

2314 [] -> return ()

2289 _ -> addFn n

2315 _ -> addFn n

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

2316 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

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

2318 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

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

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

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

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

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

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

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

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

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

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

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

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

2335 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

2311 ni 0 env t

2337 ni 0 env t

2312 ni 0 env r

2338 ni 0 env r

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

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

src/Idris/CmdOptions.hs+43−8

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

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

87 -- Logging Flags

88 <|> (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+

89 -- Turn off Certain libraries.

94 -- Turn off Certain libraries.

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

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

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

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

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

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

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

162

167

163preProcOpts :: [Opt] -> [Opt] -> [Opt]

168preProcOpts :: [Opt] -> [Opt] -> [Opt]

164−preProcOpts [] ys = ys

169+preProcOpts [] ys = ys

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

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

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

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

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

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

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

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

169

174

170parseCodegen :: String -> Codegen

175parseCodegen :: String -> Codegen

171parseCodegen "bytecode" = Bytecode

176parseCodegen "bytecode" = Bytecode

172−parseCodegen cg = Via (map toLower cg)

177+parseCodegen cg = Via (map toLower cg)

173−

174−

175

178

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."

176

211

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

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

178−parseConsoleWidth "auto" = return AutomaticWidth

213+parseConsoleWidth "auto" = return AutomaticWidth

179parseConsoleWidth "infinite" = return InfinitelyWide

214parseConsoleWidth "infinite" = return InfinitelyWide

180parseConsoleWidth s =

215parseConsoleWidth s =

181 case lastMay (readP_to_S (integerReader) s) of

216 case lastMay (readP_to_S (integerReader) s) of

src/Idris/DeepSeq.hs+8−3

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

116 rnf (NoBuiltins) = ()

117 rnf (NoREPL) = ()

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

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

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

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

120 rnf (Interface) = ()

121 rnf (Interface) = ()

121 rnf (TypeCase) = ()

122 rnf (TypeCase) = ()

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

174instance NFData IOption where

175instance NFData IOption where

175 rnf (IOption

176 rnf (IOption

176 opt_logLevel

177 opt_logLevel

178+ opt_logcats

177 opt_typecase

179 opt_typecase

178 opt_typeintype

180 opt_typeintype

179 opt_coverage

181 opt_coverage

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

226instance NFData LanguageExt where

228instance NFData LanguageExt where

227 rnf TypeProviders = ()

229 rnf TypeProviders = ()

228 rnf ErrorReflection = ()

230 rnf ErrorReflection = ()

229−

231+

230instance NFData Optimisation where

232instance NFData Optimisation where

231 rnf PETransform = ()

233 rnf PETransform = ()

232

234

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

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

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

359 rnf Bytecode = ()

361 rnf Bytecode = ()

360

362

363+instance NFData LogCat where

364+ rnf _ = ()

365+

361instance NFData CGInfo where

366instance NFData CGInfo where

362 rnf (CGInfo x1 x2 x3 x4 x5)

367 rnf (CGInfo x1 x2 x3 x4 x5)

363 = rnf x1 `seq`

368 = rnf x1 `seq`

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

563instance NFData PAltType where

568instance NFData PAltType where

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

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

565 rnf FirstSuccess = ()

570 rnf FirstSuccess = ()

566− rnf TryImplicit = ()

571+ rnf TryImplicit = ()

567

572

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

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

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

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

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

687

692

688

693

689instance NFData IState where

694instance 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

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

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

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

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

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

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

189 <?> "declaration"

190

191internalDecl :: SyntaxInfo -> IdrisParser [PDecl]

192−internalDecl syn

192+internalDecl syn

193 = do fc <- getFC

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

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

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

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

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

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

207− if continue then

207+ if continue then

208 do notEndBlock

209 declBody continue

210 else try (do notEndBlock

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

283 isDeclRule (DeclRule _ _) = True

284 isDeclRule _ = False

285

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

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

287 -> IdrisParser [PDecl]

288declExtension syn ns rules =

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

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

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

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

320 = 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)

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

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

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

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

338 cdocs

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

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

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

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

342 (map (updateNs ns) ds)

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

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

346 updateNs ns d = d

347

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

482 where ts = dropWhile isSpace . dropWhileEnd isSpace $ s

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

484 mkSimple' [] = []

485−

485+

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

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

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

src/Idris/REPL.hs+16−14

@@ -805,7 +805,7 @@ process fn (Eval t)

805 getIState >>= flip warnDisamb t

806 (tm, ty) <- elabREPL recinfo ERHS t

807 ctxt <- getContext

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

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

809 [sUN "foreign",

810 sUN "prim_read",

811 sUN "prim_write"]

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

951 = let current = case n of

952 MN _ _ -> text ""

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

954− _ -> text " " <>

954+ _ -> text " " <>

955 bindingOf n False

956− <+> colon

956+ <+> colon

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

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

958 <> line

959 in

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

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

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

987

988process fn (DocStr (Left n) w)

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

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

990− | otherwise = do

990+ | otherwise = do

991 ist <- getIState

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

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

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

1010process fn Universes

1011 = do i <- getIState

1012 let cs = idris_constraints i

1013− let cslist = S.toAscList cs

1013+ let cslist = S.toAscList cs

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

1015 iputStrLn $ show (map uconstraint cslist)

1016 let n = length cslist

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

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

1227 where fc = fileFC "main"

1228process fn (LogLvl i) = setLogLevel i

1229+process fn (LogCategory cs) = setLogCats cs

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

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

1230process fn (Pattelab t)

1231process fn (Pattelab t)

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

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

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

1528 let ninputs = zip [1..] inputs

1529 let ninputs = zip [1..] inputs

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

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

1530 do putIState ist

1531 do putIState ist

1531− modTree <- buildTree

1532+ modTree <- buildTree

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

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

1533 importlists

1534 importlists

1534 input

1535 input

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

1777 ok <- noErrors

1778 ok <- noErrors

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

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

1779 where

1780 where

1780− makeOption (OLogging i) = setLogLevel i

1781+ makeOption (OLogging i) = setLogLevel i

1782+ makeOption (OLogCats cs) = setLogCats cs

1781− makeOption TypeCase = setTypeCase True

1783+ makeOption TypeCase = setTypeCase True

1782− makeOption TypeInType = setTypeInType True

1784+ makeOption TypeInType = setTypeInType True

1783− makeOption NoCoverage = setCoverage False

1785+ makeOption NoCoverage = setCoverage False

1784− makeOption ErrContext = setErrContext True

1786+ makeOption ErrContext = setErrContext True

1785− makeOption _ = return ()

1787+ makeOption _ = return ()

1786

1788

1787 addPkgDir :: String -> Idris ()

1789 addPkgDir :: String -> Idris ()

1788 addPkgDir p = do ddir <- runIO $ getIdrisLibDir

1790 addPkgDir p = do ddir <- runIO $ getIdrisLibDir

src/Idris/REPLParser.hs+41−11

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

43 ("desugarnats", DesugarNats)]

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

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

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

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

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

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

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

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

53parserCommandsForHelp :: CommandTable

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

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

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

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

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

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

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

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

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

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

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

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

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

141+ , ( ["logacts"]

142+ , ManyArgs NameArg

143+ , "Set logging categories"

144+ , cmd_cats)

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

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

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

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

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

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

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

148 , cmd_refine)

152 , cmd_refine)

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

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

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

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

151− l <- P.simpleExpr defaultSyntax

155+ l <- P.simpleExpr defaultSyntax

152− r <- P.simpleExpr defaultSyntax

156+ r <- P.simpleExpr defaultSyntax

153 eof

157 eof

154 return (Right (DebugUnify l r))

158 return (Right (DebugUnify l r))

155 )

159 )

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

171 (names, NoArg, doc, proofArg command)

175 (names, NoArg, doc, proofArg command)

172

176

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

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

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

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

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

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

176− <|> unrecognized

180+ <|> unrecognized

177 <|> nop

181 <|> nop

178 <|> eval

182 <|> eval

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

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

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

227

231

228

232

229

233

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

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

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

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

232genArg argName argParser cmd name = do

236genArg argName argParser cmd name = do

233 let emptyArgs = do eof; failure

237 let emptyArgs = do eof; failure

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

246strArg = genArg "string" (many anyChar)

250strArg = genArg "string" (many anyChar)

247

251

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

252moduleArg :: (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)

250 where

254 where

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

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

252

256

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

257namespaceArg :: ([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)

255 where

259 where

256 toNS = splitOn "."

260 toNS = splitOn "."

257

261

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

290 c <- fmap fst P.constant

294 c <- fmap fst P.constant

291 eof

295 eof

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

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

293−

297+

294 let pType = do

298 let pType = do

295 P.reserved "Type"

299 P.reserved "Type"

296 eof

300 eof

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

392 eof

396 eof

393 return (Right (LogLvl i))

397 return (Right (LogLvl i))

394

398

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+

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

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

396cmd_let name = do

426cmd_let name = do

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

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