79d43a7 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge branch 'master' of github.com:idris-lang/Idris-dev

79d43a7Aaron Craelius11 years ago

CHANGELOG+13−2

compare with master

unifiedsplit

@@ -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+* New flag `--listlogcats` to list logging categories.`

11+

1New in 0.9.20:

12New in 0.9.20:

2==============

13==============

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

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

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

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

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

21 arguments, are treated as bound pattern variables.

32 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

23 deprecated name is referenced.

34 deprecated name is referenced.

25Library updates

36Library updates

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

39 from Effectful programs.

50 from Effectful programs.

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

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

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

52 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

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

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

44 that they may fail.

55 that they may fail.

INSTALL.md+13−7

@@ -84,10 +84,16 @@ version of GHC.

85### `libGMP` and `libFFI`

87+By default the stack configuration in `stack.yaml` will build with

87−To build with support for `libGMP` and `libFFI` you need to pass build

88+support for `libGMP` and `libFFI`. To turn this support off, the

88−commands for the Idris library either from the command line:

89+option flags needs to be fully commented out.

89−

90+

90−* `stack build --flag idris:GMP --flag idris:FFI`

91+There have been reports in the past over building Idris on Mac OS X,

91−

92+using stack, and linking to a HomeBrew installation of `libFFI`. The

92−or un-comment the options `idris:GMP` and `idris:FFI` and their

93+build has failed to find the correct `libFFI` installation. If you

93−dependencies in the `stack.yaml` file.

94+encounter this then the fix is to augment the `PKG_CONFIG_PATH` when

95+running the stack build:

96+

97+```

98+PKG_CONFIG_PATH=/usr/local/Cellar/libffi/3.0.13/lib/pkgconfig stack build

99+```

docs/reference/compilation.rst+21−2

@@ -45,8 +45,27 @@ Use of this option will still result in the generation of the Idris binary ``.ib

45Logging Output

46==============

48−Logging of the Idris output can be used to diagnose problems with the compilation of your program.

48+The internal operation of Idris is captured using a category based logger.

49−Idris supports the logging at various different levels of verbosity: 1 to 10.

49+Currently, the logging infrastructure has support for the following categories:

50+

51++ Parser

52++ Elaborator

53++ Code generation

54++ Erasure

55++ Coverage Checking

56++ IBC generation

57+

58+

59+These categories are specified using the command-line option:

60+``--logging-categories CATS``, where ``CATS`` is a quoted colon

61+seperated string of the categories you want to see. By default if this

62+option is not specified all categories are allowed. Sub-categories

63+have yet to be defined but will be in the future, especially for the

64+elaborator.

65+

66+Further, the verbosity of logging can be controlled by specifying a

67+logging level between: 1 to 10 using the command-line option: ``--log

68+<level>``.

51+ Level 0: Show no logging output. Default level

70+ Level 0: Show no logging output. Default level

52+ Level 1: High level details of the compilation process.

71+ Level 1: High level details of the compilation process.

main/Main.hs+6

@@ -45,6 +45,7 @@ main = do opts <- runArgParser

45runIdris :: [Opt] -> Idris ()

46runIdris opts = do

47 runIO setupBundledCC

48+ when (ShowLoggingCats `elem` opts) $ runIO showLoggingCats

48 when (ShowIncs `elem` opts) $ runIO showIncs

49 when (ShowIncs `elem` opts) $ runIO showIncs

49 when (ShowLibs `elem` opts) $ runIO showLibs

50 when (ShowLibs `elem` opts) $ runIO showLibs

50 when (ShowLibdir `elem` opts) $ runIO showLibdir

51 when (ShowLibdir `elem` opts) $ runIO showLibdir

@@ -101,3 +102,8 @@ showIncs = do incFlags <- getIncFlags

101showPkgs :: IO b

102showPkgs :: IO b

102showPkgs = do mapM putStrLn =<< installedPackages

103showPkgs = do mapM putStrLn =<< installedPackages

103 exitWith ExitSuccess

104 exitWith ExitSuccess

105+

106+showLoggingCats :: IO b

107+showLoggingCats = do

108+ putStrLn loggingCatsStr

109+ exitWith ExitSuccess

src/IRTS/Compiler.hs+18−18

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

54 Nothing -> []

55 Just t -> freeNames t

57− reachableNames <- performUsageAnalysis

57+ reachableNames <- performUsageAnalysis

58 (rootNames ++ getExpNames exports)

59 maindef <- case mtm of

60 Nothing -> return []

61 Just tm -> do md <- irMain tm

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

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

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

64 objs <- getObjectFiles codegen

65 libs <- getLibs codegen

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

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

83 let ctxtIn = addAlist tagged emptyContext

85− logLvl 1 "Defunctionalising"

85+ logCodeGen 1 "Defunctionalising"

86 let defuns_in = defunctionalise nexttag ctxtIn

87− logLvl 5 $ show defuns_in

87+ logCodeGen 5 $ show defuns_in

88− logLvl 1 "Inlining"

88+ logCodeGen 1 "Inlining"

89 let defuns = inline defuns_in

90− logLvl 5 $ show defuns

90+ logCodeGen 5 $ show defuns

91− logLvl 1 "Resolving variables for CG"

91+ logCodeGen 1 "Resolving variables for CG"

93 let checked = simplifyDefs defuns (toAlist defuns)

94 outty <- outputTy

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

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

103 triple <- Idris.AbsSyntax.targetTriple

104 cpu <- Idris.AbsSyntax.targetCPU

105− logLvl 1 "Building output"

105+ logCodeGen 1 "Building output"

106 case checked of

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

108 hdrs impdirs objs libs flags

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

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

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

186 _ -> 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

188 return (n, def)

189− where getPrim n i

189+ where getPrim n i

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

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

191 = Just (ar, op)

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

193 = Just (ar, LExternal n)

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

224type Vars = M.Map Name VarInfo

225

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

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

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

228 ist <- getIState

229 case unApply tm of

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

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

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

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

456 = do args' <- mapM splitArg args

457− let fname' = toFDesc fname

457+ let fname' = toFDesc fname

458 let ret' = toFDesc ret

459 return $ LForeign ret' fname' args'

460 where

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

462− = do let l' = toFDesc l

462+ = do let l' = toFDesc l

463 r' <- irTerm vs env r

464 return (l', r')

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

466

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

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

468− toFDesc tm

468+ toFDesc tm

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

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

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

471 toFDesc _ = FUnknown

472

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

476

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

478irTree args tree = do

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

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

480 LLam args <$> irSC M.empty tree

481

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

src/IRTS/Exports.hs+8−11

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

13findExports :: Idris [ExportIFace]

14findExports = do exps <- getExports

15 es <- mapM toIFace exps

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

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

17 return es

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

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

39 getExpList _ = ifail "Badly formed export list"

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

42−toIFaceTyVal ty tm

42+toIFaceTyVal ty tm

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

44 = do tm' <- toIFaceVal tm

45 return $ Export ffi hdr tm'

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

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

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

53 = do rest' <- toIFaceVal rest

54− return $

54+ return $

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

56 : rest'

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

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

63toFDesc :: Term -> FDesc

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

65toFDesc tm

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

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

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

68toFDesc _ = FUnknown

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

91 | otherwise = error "Badly formed export type"

93toFDescArgs :: Term -> [FDesc]

94−toFDescArgs tm

94+toFDescArgs tm

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

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

97 = toFDescBase b : toFDescArgs t

98 | otherwise = []

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

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

101−toFDescPrim tm

101+toFDescPrim tm

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

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

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

104toFDescPrim _ = FUnknown

105

106deNS (NS n _) = n

107deNS n = n

108−

109−

110−

src/Idris/AbsSyntax.hs+60−14

@@ -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,55 @@ 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+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

973−logLvl l str = do i <- getIState

1014+ i <- getIState

974− let lvl = opt_logLevel (idris_options i)

1015+ let lvl = opt_logLevel (idris_options i)

1016+ let cats = opt_logcats (idris_options i)

975− when (lvl >= l) $

1017+ when (lvl >= l) $

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

976− case idris_outputmode i of

1019+ case idris_outputmode i of

1020+ RawOutput h -> do

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

1021+ runIO $ hPutStrLn h str

978− IdeMode n h ->

1022+ IdeMode n h -> do

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

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

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

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

981

1028

982cmdOptType :: Opt -> Idris Bool

1029cmdOptType :: Opt -> Idris Bool

983cmdOptType x = do i <- getIState

1030cmdOptType x = do i <- getIState

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

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

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

1397 scopedimpl _ = False

1444 scopedimpl _ = False

1398

1445

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

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

1400 | scopedimpl i = getImps sc imps

1447 | scopedimpl i = getImps sc imps

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

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

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

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

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

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

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

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

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

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

1679 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'

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

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

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

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

1707 -> Either Err PTerm

1754 -> Either Err PTerm

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

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

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

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

1710− | otherwise

1757+ | otherwise

1711 = case lookupDef f (tt_ctxt ist) of

1758 = case lookupDef f (tt_ctxt ist) of

1712 [] -> Right $ PPatvar ffc f

1759 [] -> Right $ PPatvar ffc f

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

1760 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

1743 [] -> nh

1790 [] -> nh

1744 x -> x

1791 x -> x

1745 case ns' of

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

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

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

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

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

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

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

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

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

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

2174-- about with shadowing anywhere else).

2221-- about with shadowing anywhere else).

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

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

2176−mkUniqueNames env shadows tm

2223+mkUniqueNames env shadows tm

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

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

2178

2225

2179 initMap = M.fromList shadows

2226 initMap = M.fromList shadows

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

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

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

2296

2343

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

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

2298−

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

451

454

452data OutputFmt = HTMLOutput | LaTeXOutput

455data OutputFmt = HTMLOutput | LaTeXOutput

453

456

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+strLogCat :: LogCat -> String

469+strLogCat IParse = "parser"

470+strLogCat IElab = "elab"

471+strLogCat ICodeGen = "codegen"

472+strLogCat IErasure = "erasure"

473+strLogCat ICoverage = "coverage"

474+strLogCat IIBC = "ibc"

475+

476+codegenCats :: [LogCat]

477+codegenCats = [ICodeGen]

478+

479+parserCats :: [LogCat]

480+parserCats = [IParse]

481+

482+elabCats :: [LogCat]

483+elabCats = [IElab]

484+

485+loggingCatsStr :: String

486+loggingCatsStr = unlines

487+ [ (strLogCat IParse)

488+ , (strLogCat IElab)

489+ , (strLogCat ICodeGen)

490+ , (strLogCat IErasure)

491+ , (strLogCat ICoverage)

492+ , (strLogCat IIBC)

493+ ]

494+

454data Opt = Filename String

495data Opt = Filename String

455 | Quiet

496 | Quiet

456 | NoBanner

497 | NoBanner

@@ -461,11 +502,13 @@ data Opt = Filename String

461 | ShowLibdir

502 | ShowLibdir

462 | ShowIncs

503 | ShowIncs

463 | ShowPkgs

504 | ShowPkgs

505+ | ShowLoggingCats

464 | NoBasePkgs

506 | NoBasePkgs

465 | NoPrelude

507 | NoPrelude

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

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

467 | NoREPL

509 | NoREPL

468 | OLogging Int

510 | OLogging Int

511+ | OLogCats [LogCat]

469 | Output String

512 | Output String

470 | Interface

513 | Interface

471 | TypeCase

514 | TypeCase

@@ -767,7 +810,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 }

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

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

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

769 deriving Functor

812 deriving Functor

770−

813+

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

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

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

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

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

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

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

1088 | MatchRefine Name

1131 | MatchRefine Name

1089 | LetTac Name t | LetTacTy Name t t

1132 | LetTac Name t | LetTacTy Name t t

1090 | Exact t | Compute | Trivial | TCInstance

1133 | Exact t | Compute | Trivial | TCInstance

1091− | ProofSearch Bool Bool Int (Maybe Name)

1134+ | ProofSearch Bool Bool Int (Maybe Name)

1092 [Name] -- allowed local names

1135 [Name] -- allowed local names

1093 [Name] -- hints

1136 [Name] -- hints

1094 -- ^ the bool is whether to search recursively

1137 -- ^ the bool is whether to search recursively

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

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

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

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

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

1181 argopts :: [ArgOpt],

1224 argopts :: [ArgOpt],

1182− pname :: Name,

1225+ pname :: Name,

1183 getTm :: t }

1226 getTm :: t }

1184 | PExp { priority :: Int,

1227 | PExp { priority :: Int,

1185 argopts :: [ArgOpt],

1228 argopts :: [ArgOpt],

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

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

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

1891 text "%runElab" <$>

1934 text "%runElab" <$>

1892 prettySe (decD d) funcAppPrec bnd tm

1935 prettySe (decD d) funcAppPrec bnd tm

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

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

1894

1937

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

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

1896

1939

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

2137showTmImpls :: PTerm -> String

2180showTmImpls :: PTerm -> String

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

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

2139

2182

2140−-- | Show a term with specific options

2183+-- | Show a term with specific options

2141showTmOpts :: PPOption -> PTerm -> String

2184showTmOpts :: PPOption -> PTerm -> String

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

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

2143

2186

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

2253

2296

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

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

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

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

2256−implicitNamesIn uvars ist tm

2299+implicitNamesIn uvars ist tm

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

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

2258 nub imps \\ nub fns

2301 nub imps \\ nub fns

2259 where

2302 where

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

2282 ni 0 env (PRef _ _ n)

2325 ni 0 env (PRef _ _ n)

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

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

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

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

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

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

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

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

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

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

2288 [] -> return ()

2331 [] -> return ()

2289 _ -> addFn n

2332 _ -> addFn n

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

2350 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

2351 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

2352 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

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

2311 ni 0 env t

2354 ni 0 env t

2312 ni 0 env r

2355 ni 0 env r

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

2356 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'

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

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

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

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

70-- iputStrLn (show pats)

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

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

72 let ctxt = tt_ctxt ist

73 case lookup n pats of

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

75 Just ty ->

76 do let splits = findPats ist ty

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

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

78 (map showTmImpls splits))

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

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

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

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

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

82 (map (showTmImpls) newPats_in))

83 newPats_in <- mapM elabNewPat newPats_in

84 case anyValid [] [] newPats_in of

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

86 let fails' = mergeAllPats ist n t fails

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

88 Right newPats -> do

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

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

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

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

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

92− logLvl 3 "----"

92+ logElab 3 "----"

93 let newPats' = mergeAllPats ist n t newPats

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

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

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

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

97− where

97+ where

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

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

99 else Right (reverse ok)

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

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

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

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

112

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

114−inventName ist ty n =

114+inventName ist ty n =

115 do ms <- get

116 let supp = case ty of

117 Nothing -> []

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

131 do let n' = uniqueNameFrom nsupp badnames

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

133 return n'

134−

134+

135mkSupply :: [Name] -> [Name]

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

137 where mkSupply' xs ns' = xs ++ mkSupply ns'

138−

138+

139varlist :: [Name]

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

141

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

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

148mergeAllPats ist cv t [] = []

149mergeAllPats 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)

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

152 ps' = mergeAllPats ist cv t ps in

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

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

192mergeUserImpl x y = x

193

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

195−argTys ist (PRef fc hls n)

195+argTys ist (PRef fc hls n)

196 = case lookupTy n (tt_ctxt ist) of

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

198 _ -> repeat Nothing

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

227 i <- getIState

228 return (True, delab i tm))

229 (\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

231 return (False, t))

232

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

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

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

251 | isDConName v ctxt = orig

252 subst (PRef _ _ _) = Placeholder

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

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

254 | isTConName t ctxt = Placeholder -- infer types

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

256 subst x = x

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

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

266splitOnLine l n fn = do

267 cl <- getInternalApp fn l

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

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

269 tms <- split n cl

270− return tms

270+ return tms

271

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

273replaceSplits l ups impossible

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

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

278

279 updateRHSs i [] = return []

280− updateRHSs i (x : xs)

280+ updateRHSs i (x : xs)

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

282 return (setImpossible False x : xs')

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

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

286

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

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

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

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

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

291 || x == '(')) xs

292 let rest = if last then rest_in else

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

341 | otherwise = tm

342

343

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

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

345getUniq nm i

346 = do ist <- getIState

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

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

360 -> Name -- ^ User given name

361 -> FilePath -- ^ Source file name

362 -> Idris String

363−getClause l fn un fp

363+getClause l fn un fp

364 = do i <- getIState

365 case lookupCtxt un (idris_classes i) of

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

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

370 x -> x

371 ist <- get

372 let ap = mkApp ist ty []

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

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

374 ++ show un ++ "_rhs")

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

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

377 = let n = getNameFrom i used ty in

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

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

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

380 | thead n == '_'

381 = let n = getNameFrom i used ty in

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

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

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

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

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

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

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

386 mkApp i _ _ = ""

387

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

394 sUN "z"]) used

395 ns -> uniqueNameFrom (mkSupply ns) used

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

397− sUN "z"]) used

397+ sUN "z"]) used

398

399 -- write method declarations, indent with 4 spaces

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

401− mkClassBodies i ns

401+ mkClassBodies i ns

402 = showSep "\n"

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

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

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

405 ++ mkApp i ty []

406− ++ "= ?"

406+ ++ "= ?"

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

408

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

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

456 case mptm of

457 (False, _) -> return ptm

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

459−

460−

461−

462−

src/Idris/CmdOptions.hs+43−13

@@ -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 "logging-categories"

91+ <> metavar "CATS"

92+ <> help "Colon separated logging categories. Use --listlogcats to see list."))

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

@@ -101,11 +106,13 @@ parseFlags = many $

101 <|> flag' WarnReach (long "warnreach" <> help "Warn about reachable but inaccessible arguments")

106 <|> flag' WarnReach (long "warnreach" <> help "Warn about reachable but inaccessible arguments")

102 <|> flag' NoCoverage (long "nocoverage")

107 <|> flag' NoCoverage (long "nocoverage")

103 <|> flag' ErrContext (long "errorcontext")

108 <|> flag' ErrContext (long "errorcontext")

109+ -- Show things

110+ <|> flag' ShowLoggingCats (long "listlogcats" <> help "Display logging categories")

104− <|> flag' ShowLibs (long "link" <> help "Display link flags")

111+ <|> flag' ShowLibs (long "link" <> help "Display link flags")

105− <|> flag' ShowPkgs (long "listlibs" <> help "Display installed libraries")

112+ <|> flag' ShowPkgs (long "listlibs" <> help "Display installed libraries")

106− <|> flag' ShowLibdir (long "libdir" <> help "Display library directory")

113+ <|> flag' ShowLibdir (long "libdir" <> help "Display library directory")

107− <|> flag' ShowIncs (long "include" <> help "Display the includes flags")

114+ <|> flag' ShowIncs (long "include" <> help "Display the includes flags")

108− <|> flag' Verbose (short 'V' <> long "verbose" <> help "Loud verbosity")

115+ <|> flag' Verbose (short 'V' <> long "verbose" <> help "Loud verbosity")

109 <|> (IBCSubDir <$> strOption (long "ibcsubdir" <> metavar "FILE" <> help "Write IBC files into sub directory"))

116 <|> (IBCSubDir <$> strOption (long "ibcsubdir" <> metavar "FILE" <> help "Write IBC files into sub directory"))

110 <|> (ImportDir <$> strOption (short 'i' <> long "idrispath" <> help "Add directory to the list of import paths"))

117 <|> (ImportDir <$> strOption (short 'i' <> long "idrispath" <> help "Add directory to the list of import paths"))

111 <|> flag' WarnOnly (long "warn")

118 <|> flag' WarnOnly (long "warn")

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

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

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

162

169

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

170preProcOpts :: [Opt] -> [Opt] -> [Opt]

164−preProcOpts [] ys = ys

171+preProcOpts [] ys = ys

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

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

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

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

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

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

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

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

169

176

170parseCodegen :: String -> Codegen

177parseCodegen :: String -> Codegen

171parseCodegen "bytecode" = Bytecode

178parseCodegen "bytecode" = Bytecode

172−parseCodegen cg = Via (map toLower cg)

179+parseCodegen cg = Via (map toLower cg)

173−

174−

175

180

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

182+parseLogCats s =

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

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

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

186+ where

187+ doParse :: ReadP [LogCat]

188+ doParse = do

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

190+ eof

191+ return (concat cs)

192+

193+ parseLogCat :: ReadP [LogCat]

194+ parseLogCat = (string (strLogCat IParse) *> return parserCats)

195+ <|> (string (strLogCat IElab) *> return elabCats)

196+ <|> (string (strLogCat ICodeGen) *> return codegenCats)

197+ <|> (string (strLogCat ICoverage) *> return [ICoverage])

198+ <|> (string (strLogCat IIBC) *> return [IIBC])

199+ <|> (string (strLogCat IErasure) *> return [IErasure])

200+ <|> parseLogCatBad

201+

202+ parseLogCatBad :: ReadP [LogCat]

203+ parseLogCatBad = do

204+ s <- look

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

176

206

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

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

178−parseConsoleWidth "auto" = return AutomaticWidth

208+parseConsoleWidth "auto" = return AutomaticWidth

179parseConsoleWidth "infinite" = return InfinitelyWide

209parseConsoleWidth "infinite" = return InfinitelyWide

180parseConsoleWidth s =

210parseConsoleWidth s =

181 case lastMay (readP_to_S (integerReader) s) of

211 case lastMay (readP_to_S (integerReader) s) of

src/Idris/Coverage.hs+24−24

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

56 = do i <- getIState

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

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

60 (map (stripUnmatchable i) (map flattenArgs given))

61 let lhss = map pUnApply lhs_tms'

63 let argss = transpose lhss

64 let all_args = map (genAll i) argss

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

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

66− logLvl 5 $ show (lhs_tms, lhss)

66+ logCoverage 5 $ show (lhs_tms, lhss)

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

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

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

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

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

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

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

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

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

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

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

78 _ -> repeat (pexp Placeholder)

79 let tryclauses = mkClauses parg all_args

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

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

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

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

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

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

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

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

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

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

86 return new

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

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

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

93 pUnApply _ = []

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

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

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

97 flattenArgs t = t

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

248

249 -- put it back to its original form

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

251− | n == sigmaCon

251+ | n == sigmaCon

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

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

254 | n == pairCon

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

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

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

332 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

334 addIBC (IBCTotal cn tot)

335 return tot

336 where

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

432

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

434checkDeclTotality (fc, n)

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

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

436-- buildSCG (fc, n)

437−-- logLvl 2 $ "Built SCG"

437+-- logCoverage 2 $ "Built SCG"

438 i <- getIState

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

440 [fs] -> fs

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

446 -- typechecking decidable

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

448 addIBC (IBCAccess n Frozen)

449− logLvl 5 $ "HIDDEN: "

449+ logCoverage 5 $ "HIDDEN: "

450 ++ show n ++ show p

451 _ -> return ()

452 return t

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

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

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

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

473 ++ show pats ++ "\n" ++ show sc

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

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

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

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

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

479

480delazy = delazy' False -- not lazy codata

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

594 ist <- getIState

595 case lookupCtxt n (idris_callgraph ist) of

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

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

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

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

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

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

601− logLvl 6 (show cg)

601+ logCoverage 6 (show cg)

602 -- every multipath must have an infinitely descending

603 -- thread, then the function terminates

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

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

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

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

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

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

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

609 return (noPartial tot)

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

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

611 return Unchecked

612 where getArity ist n

613 = case lookupTy n (tt_ctxt ist) of

src/Idris/DeepSeq.hs+9−3

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

107 rnf (ColourREPL bool) = rnf bool `seq` ()

108 rnf (Idemode) = ()

109 rnf (IdemodeSocket) = ()

110+ rnf (ShowLoggingCats) = ()

110 rnf (ShowLibs) = ()

111 rnf (ShowLibs) = ()

111 rnf (ShowLibdir) = ()

112 rnf (ShowLibdir) = ()

112 rnf (ShowIncs) = ()

113 rnf (ShowIncs) = ()

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

116 rnf (NoBuiltins) = ()

117 rnf (NoBuiltins) = ()

117 rnf (NoREPL) = ()

118 rnf (NoREPL) = ()

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

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

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

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

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

120 rnf (Interface) = ()

122 rnf (Interface) = ()

121 rnf (TypeCase) = ()

123 rnf (TypeCase) = ()

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

174instance NFData IOption where

176instance NFData IOption where

175 rnf (IOption

177 rnf (IOption

176 opt_logLevel

178 opt_logLevel

179+ opt_logcats

177 opt_typecase

180 opt_typecase

178 opt_typeintype

181 opt_typeintype

179 opt_coverage

182 opt_coverage

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

226instance NFData LanguageExt where

229instance NFData LanguageExt where

227 rnf TypeProviders = ()

230 rnf TypeProviders = ()

228 rnf ErrorReflection = ()

231 rnf ErrorReflection = ()

229−

232+

230instance NFData Optimisation where

233instance NFData Optimisation where

231 rnf PETransform = ()

234 rnf PETransform = ()

232

235

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

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

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

359 rnf Bytecode = ()

362 rnf Bytecode = ()

360

363

364+instance NFData LogCat where

365+ rnf _ = ()

366+

361instance NFData CGInfo where

367instance NFData CGInfo where

362 rnf (CGInfo x1 x2 x3 x4 x5)

368 rnf (CGInfo x1 x2 x3 x4 x5)

363 = rnf x1 `seq`

369 = rnf x1 `seq`

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

563instance NFData PAltType where

569instance NFData PAltType where

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

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

565 rnf FirstSuccess = ()

571 rnf FirstSuccess = ()

566− rnf TryImplicit = ()

572+ rnf TryImplicit = ()

567

573

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

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

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

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

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

687

693

688

694

689instance NFData IState where

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

696+ 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

697 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

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

699 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

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

79 mapM_ checkDefaultSuperclassInstance idecls

80 let mnames = map getMName mdecls

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

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

82 ims <- mapM (tdecl mnames) mdecls

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

84 (filter clause ds)

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

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

95 let ddecl = PDatadecl tn NoFC tty cons

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

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

99 -- Elaborate the data declaration

100 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

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

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

111 (map fst imethods)) imethods

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

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

113 -- Elaborate the the top level methods

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

115

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

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

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

161 = 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'

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

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

165 (\ 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

174 let ds = map (decorateid defaultdec)

175 [PTy emptyDocstring [] syn fc [] n nfc ty',

176 PClauses fc (o ++ opts) n cs]

177− logLvl 1 (show ds)

177+ logElab 1 (show ds)

178 return (n, ((defaultdec n, ds!!1), ds))

179 _ -> ifail $ show n ++ " is not a method"

180 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

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

200 let rhs = PResolveTC (fileFC "HACK")

201 let ty = PPi constraint cnm NoFC c con

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

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

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

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

204 i <- getIState

205 let conn = case con of

206 PRef _ _ n -> n

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

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

231 let lhs = PApp fc (PRef fc [] m) (pconst capp : lhsArgs margs anames)

232 let rhs = PApp fc (getMeth mnames all m) (rhsArgs margs anames)

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

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

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

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

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

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

236 return [PTy doc [] syn fc o m mfc ty',

237 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]

238

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

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

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

320 getDetPos _ _ _ = []

321−

322−

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

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

84 -- no simplification or PE

85 let (pats_in, cs_full) = unzip cs_elab

86 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

89 solveDeferred n

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

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

103 -- RHS

104 pe_tm <- doPartialEval ist tpats

105− let pats_pe = if petrans

105+ let pats_pe = if petrans

106 then map (simple_lhs (tt_ctxt ist)) pe_tm

107 else pats_raw

108

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

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

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

113 -- for partially evaluated definitions

114− newrules <- if petrans

114+ newrules <- if petrans

115 then mapM (\ e -> case e of

116 Left _ -> return []

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

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

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

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

136 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

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

139 let pdef_pe = map debind pats_transformed

140

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

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

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

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

143

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

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

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

152 numArgs <- tclift $ sameLength pdef

153

154 case specNames opts of

155− Just _ ->

155+ Just _ ->

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

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

157 _ -> return ()

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

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

159

160 erInfo <- getErasureInfo <$> getIState

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

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

167 -- missing <- genMissing n scargs sc

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

169 let clhs = map getLHS pdef

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

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

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

172 "\nAgainst: " ++

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

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

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

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

187

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

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

189

190 ist <- getIState

191 -- let wf = wellFounded ist n sc

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

193− | PEGenerated `elem` opts = Generated

193+ | PEGenerated `elem` opts = Generated

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

195

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

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

206 ":warning - Unreachable case: " ++

207 show (delab ist x)) xs

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

209− let defaultcase = if knowncovering

209+ let defaultcase = if knowncovering

210 then STerm Erased

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

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

212− show fc ++

212+ show fc ++

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

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

214 " ***"

215

216 tree' <- tclift $ simpleCase tcase defaultcase reflect

217 RunTime fc inacc atys pdef' erInfo

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

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

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

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

220 ctxt <- getContext

221 ist <- getIState

222 let opt = idris_optimisation ist

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

224 (idris_patdefs ist) })

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

226 case lookupTyExact n ctxt of

227− Just ty ->

227+ Just ty ->

228 do ctxt' <- do ctxt <- getContext

229 tclift $

230 addCasedef n erInfo caseInfo

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

242 setContext ctxt'

243 addIBC (IBCDef n)

244 setTotality n tot

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

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

246 do totcheck (fc, n)

247 defer_totcheck (fc, n)

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

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

256 -- let scg = buildSCG i sc scargs

257 -- add SCG later, when checking totality

258 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

260 addToCG n cg

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

262 addIBC (IBCCG n)

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

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

361 Nothing -> True

362 _ -> False

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

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

364 idrisCatch

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

366 cgns <- getAllNames n

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

374 [Total _] -> 65536

375 [Productive] -> 16

376 _ -> 1

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

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

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

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

379 else []) ++

380− (n, Just maxred) :

380+ (n, Just maxred) :

381 mapMaybe (specName (pe_simple specdecl))

382 (snd specapp))]

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

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

384 ++ " in " ++ show caller ++

385 " with " ++ show opts

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

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

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

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

388 ++ "\n" ++ show opts

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

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

390 showSep "\n"

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

392 (showTmImpls lhs ++ " = " ++

393 showTmImpls rhs)) (pe_clauses specdecl))

394

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

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

396 showTmImpls rhs ++ " ==> " ++ showTmImpls lhs

397

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

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

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

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

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

402− (pe_clauses specdecl)

402+ (pe_clauses specdecl)

403 trans <- elabTransform info fc False rhs lhs

404 elabClauses info fc (PEGenerated:opts) newnm def

405 return [trans]

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

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

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

409 -- lifted out).

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

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

411 return [])

412

413 hiddenToPH (PHidden _) = Placeholder

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

450 -- get the clause of a specialised application

451 getSpecClause ist (n, args)

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

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

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

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

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

456 where showArg (ExplicitS, n) = qshow n

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

477 let lhs = addImplPat i lhs_in

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

479 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

481 (allNamesIn lhs_in)

482 (infTerm lhs))) of

483 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

570

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

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

573−-- let lhs = mkLHSapp $

573+-- let lhs = mkLHSapp $

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

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

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

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

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

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

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

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

579

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

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

582 (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

584 (allNamesIn lhs_in)

585 (infTerm lhs)))

586 probs <- get_probs

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

589 setContext ctxt'

590 processTacticDecls info newDecls

591 sendHighlighting highlights

592−

592+

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

594

595 let lhs_tm = orderPats (getInferTerm lhs')

596 let lhs_ty = getInferType lhs'

597 let static_names = getStaticNames i lhs_tm

598

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

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

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

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

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

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

602

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

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

615 -- Issue #1615 on the Issue Tracker.

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

617 when (not (null borrowed)) $

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

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

619

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

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

621

622 rep <- useREPL

623 when rep $ do

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

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

626

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

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

628 -- Elaborate where block

629 ist <- getIState

630 windex <- getName

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

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

648 let (wbefore, wafter) = sepBlocks wb

649

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

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

651 mapM_ (rec_elabDecl info EAll winfo) wbefore

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

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

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

656 (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

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

659− logLvl 5 "STARTING CHECK"

659+ logElab 5 "STARTING CHECK"

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

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

662 (do pbinds ist lhs_tm

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

671 (erun fc $ psolve lhs_tm)

672 tt <- get_term

673 aux <- getAux

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

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

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

676 probs <- get_probs

677 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

681

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

683

684− logLvl 5 "DONE CHECK"

684+ logElab 5 "DONE CHECK"

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

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

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

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

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

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

689 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

700 mapM_ (elabCaseBlock winfo opts) is

701

702 ctxt <- getContext

703− logLvl 5 $ "Rechecking"

703+ logElab 5 $ "Rechecking"

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

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

705

706 (crhs, crhsty) <- if not inf

707 then recheckC_borrowing True (PEGenerated `notElem` opts)

708 borrowed fc id [] rhs'

709 else return (rhs', clhsty)

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

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

711 ctxt <- getContext

712 let constv = next_tvar ctxt

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

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

715− addConstraints fc cs

715+ addConstraints fc cs

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

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

717 return ()

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

719 i <- getIState

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

805 [t] -> t

806 _ -> []

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

808− let lhs = stripLinear i $ stripUnmatchable i $

808+ let lhs = stripLinear i $ stripUnmatchable i $

809− propagateParams i params fn_ty (allNamesIn lhs_in)

809+ propagateParams i params fn_ty (allNamesIn lhs_in)

810 (addImplPat i lhs_in)

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

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

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

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

814 (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

816 (allNamesIn lhs_in)

817 (infTerm lhs))) )

818 setContext ctxt'

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

823 let lhs_ty = getInferType lhs'

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

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

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

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

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

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

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

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

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

832 -- Elaborate wval in this context

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

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

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

852 addDeferred def''

853 mapM_ (elabCaseBlock info opts) is

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

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

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

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

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

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

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

861 -- so this doesn't lose anything)

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

876 -- Highlight explicit proofs

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

878

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

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

880 " 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)

882 windex <- getName

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

884 -- (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)

886 let wargtype = getRetTy cwvaltyN

887 let wargname = sMN windex "warg"

888

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

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

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

891 (wargname, wargtype) :

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

896 P Bound wargname Erased, wargval])]

897 Nothing -> [])

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

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

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

900 let wname = SN (WithN windex fname)

901

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

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

904 let statics = getStatics static_names wtype

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

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

906 i <- getIState

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

908

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

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

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

921 withblock

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

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

923 -- propagate totality assertion to the new definitions

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

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

935 [ pimp (sUN "A") Placeholder False

936 , pimp (sUN "x") Placeholder False

937 ])])

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

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

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

940 i <- getIState

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

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

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

956 addDeferred def''

957 mapM_ (elabCaseBlock info opts) is

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

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

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

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

961 where

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

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

972 = do i <- getIState

973 let tm = addImplPat i tm_in

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

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

975 showTmImpls toplhs)

976 case matchClause i toplhs tm of

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

978 Right mvars ->

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

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

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

981 return $ PClause fc wname lhs ws rhs wheres

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

983 = do i <- getIState

984 let tm = addImplPat i tm_in

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

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

986 showTmImpls toplhs)

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

988 case matchClause i toplhs tm of

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

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

1002 return $ substMatches mvars $

1003 PApp fc (PRef fc' [] wname)

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

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

1005 case pn of

1006 Nothing -> []

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

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

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

51import Util.Pretty

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

54−warnLC fc n

54+warnLC fc n

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

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

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

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

60 = do let codata = Codata `elem` opts

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

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

62 checkUndefined fc n

63 when (implicitable n) $ warnLC fc n

64 (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)

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

71 = do let codata = Codata `elem` opts

72− logLvl 1 (show fc)

72+ logElab 1 (show fc)

73 undef <- isUndefined fc n

74 when (implicitable n) $ warnLC fc n

75 (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)

91 i <- getIState

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

93 let params = findParams (map snd cons)

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

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

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

96 -- be updated when the mutual block is complete

97 putIState (i { idris_datatypes =

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

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

233 = do checkUndefined fc n

234 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

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

237 ctxt <- getContext

238 let cty' = normalise ctxt [] cty

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

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

243 tyIs n cty'

244

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

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

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

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

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

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

248

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

250 -- can be indexed by it)

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

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

252

253 addIBC (IBCDef n)

254 checkDocs fc argDocs t

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

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

299 checkUniqueKind (UType AllTypes) (UType AllTypes) = return ()

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

301− checkUniqueKind (UType AllTypes) _

301+ checkUniqueKind (UType AllTypes) _

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

303 checkUniqueKind _ _ = return ()

304

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

306− addDataConstraint (TType con) (TType exp)

306+ addDataConstraint (TType con) (TType exp)

307 = do ctxt <- getContext

308 let v = next_tvar ctxt

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

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

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

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

356 where elimLog :: String -> EliminatorState ()

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

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

358

359 elimFC :: FC

360 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

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

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

73 let emptyclass = null (class_methods ci)

74− when (what /= EDefns) $ do

74+ when (what /= EDefns) $ do

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

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

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

106 (decorate ns iname n,

107 op, coninsert cs t', t'))

108 (class_methods ci)

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

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

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

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

111 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")

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

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

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

115 mapM_ (warnMissing ds' ns iname) (map fst (class_methods ci))

116 mapM_ (checkInClass (map fst (class_methods ci))) (concatMap defined ds')

117 let wbTys = map mkTyDecl mtys

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

119 let wb = wbTys ++ wbVals

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

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

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

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

122 show (concat (nub wparams))

123

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

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

135 (map (pexp . mkMethApp) mtys)

136

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

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

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

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

139

140 let idecls = [PClauses fc [Dictionary] iname

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

142− logLvl 1 (show idecls)

142+ logElab 1 (show idecls)

143 push_estack iname True

144 mapM_ (rec_elabDecl info EAll info) idecls

145 pop_estack

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

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

268 reorderDefs ns [] = []

269 reorderDefs [] ds = ds

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

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

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

272 Nothing -> reorderDefs ns ds

273

274− pick n acc [] = Nothing

274+ pick n acc [] = Nothing

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

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

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

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

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

314 ci 0 ist args

315 where

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

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

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

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

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

320 ci i ist [] = return ()

321

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

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

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

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

325 isInj i (V _) = True

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

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

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

331 instantiateRetTy t = t

332−

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

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

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

85 [Erased, e])

86 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

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

90 provided <- getProvided fc rhs'

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

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

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

97 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

99 | ProvPostulate _ <- what ->

100 do -- Add the postulate

101 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

103 | otherwise ->

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

105

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

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

47 -> SyntaxInfo -- ^ Constructor SyntaxInfo

48 -> Idris ()

49elabRecord 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

51 -- Type constructor

52 let tycon = generateTyConType params

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

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

54−

54+

55 -- Data constructor

56 dconName <- generateDConName (fmap fst cname)

57 let dconTy = generateDConType params fieldsWithNameAndDoc

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

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

60 -- Build data declaration for elaboration

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

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

62 let datadecl = case what of

63 ETypes -> PLaterdecl tyn NoFC tycon

64 _ -> 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

71 addIBC (IBCRecord tyn)

73 when (what /= ETypes) $ do

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

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

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

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

76 elabRecordFunctions info rsyn fc tyn paramsAndDoc fieldsWithNameAndDoc dconName target

78 sendHighlighting $

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

162 -> PTerm -- ^ Target type

163 -> Idris ()

164elabRecordFunctions 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

166

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

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

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

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

169 -- The elaborated constructor type for the data declaration

170 i <- getIState

171 ttConsTy <-

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

175

176 -- The arguments to the constructor

177 let constructorArgs = getArgTys ttConsTy

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

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

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

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

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

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

182−

182+

183 -- The parameters for elaboration with their documentation

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

185 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

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

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

189

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

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

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

192 -- Build and elaborate projection functions

193 elabProj dconName projectors

194

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

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

196

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

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

198

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

200 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

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

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

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

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

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

241

242 freeName :: Name -> Name

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

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

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

279 optionalSetter :: Name -> Bool

280 optionalSetter n = n `elem` dependedOn

281−

281+

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

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

284 fieldDependencies = map (uncurry fieldDep) [(n, t) | (n, _, _, t, _) <- fields ++ params]

@@ -314,15 +314,15 @@ elabProjection :: ElabInfo

314 -> Int -- ^ Argument Index

315 -> Idris ()

316elabProjection info cname pname plicity projTy pdoc psyn fc targetTy cn phArgs fnames index

317− = do logLvl 1 $ "Generating Projection for " ++ show pname

317+ = do logElab 1 $ "Generating Projection for " ++ show pname

318−

318+

319 let ty = generateTy

320− logLvl 1 $ "Type of " ++ show pname ++ ": " ++ show ty

320+ logElab 1 $ "Type of " ++ show pname ++ ": " ++ show ty

321−

321+

322 let lhs = generateLhs

323− logLvl 1 $ "LHS of " ++ show pname ++ ": " ++ showTmImpls lhs

323+ logElab 1 $ "LHS of " ++ show pname ++ ": " ++ showTmImpls lhs

324 let rhs = generateRhs

325− logLvl 1 $ "RHS of " ++ show pname ++ ": " ++ showTmImpls rhs

325+ logElab 1 $ "RHS of " ++ show pname ++ ": " ++ showTmImpls rhs

326

327 rec_elabDecl info EAll info ty

328

@@ -372,24 +372,24 @@ elabUpdate :: ElabInfo

372 -> Bool -- ^ Optional

373 -> Idris ()

374elabUpdate info cname pname plicity pty pdoc psyn fc sty cn args fnames i optional

375− = do logLvl 1 $ "Generating Update for " ++ show pname

375+ = do logElab 1 $ "Generating Update for " ++ show pname

376−

376+

377 let ty = generateTy

378− logLvl 1 $ "Type of " ++ show set_pname ++ ": " ++ show ty

378+ logElab 1 $ "Type of " ++ show set_pname ++ ": " ++ show ty

379−

379+

380 let lhs = generateLhs

381− logLvl 1 $ "LHS of " ++ show set_pname ++ ": " ++ showTmImpls lhs

381+ logElab 1 $ "LHS of " ++ show set_pname ++ ": " ++ showTmImpls lhs

382−

382+

383 let rhs = generateRhs

384− logLvl 1 $ "RHS of " ++ show set_pname ++ ": " ++ showTmImpls rhs

384+ logElab 1 $ "RHS of " ++ show set_pname ++ ": " ++ showTmImpls rhs

385

386− let clause = PClause fc set_pname lhs [] rhs []

386+ let clause = PClause fc set_pname lhs [] rhs []

387

388 idrisCatch (do rec_elabDecl info EAll info ty

389 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)

391 {-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

393 else tclift $ tfail $ At fc (Elaborating "record update function " pname err)) -}

394 where

395 -- | The type of the update function.

@@ -463,4 +463,3 @@ projectInType xs = mapPT st

463-- | Creates an PArg from a plicity and a name where the term is a PRef.

464asPRefArg :: Plicity -> Name -> PArg

465asPRefArg 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

91 g <- goal

92 ptm <- get_term

93 resolveTC' True True 10 g fn ist) ivs

94−

94+

95 when (not pattern) $ solveAutos ist fn False

97 tm <- get_term

@@ -138,7 +138,7 @@ build ist info emode opts fn tm

138-- (Separate, so we don't go overboard resolving things that we don't

139-- know about yet on the LHS of a pattern def)

140

141−buildTC :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name ->

141+buildTC :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name ->

142 [Name] -> -- Cached names in the PTerm, before adding PAlternatives

143 PTerm ->

144 ElabD ElabResult

@@ -147,7 +147,7 @@ buildTC ist info emode opts fn ns tm

147 let inf = case lookupCtxt fn (idris_tyinfodata ist) of

148 [TIPartial] -> True

149 _ -> False

150− -- set name supply to begin after highest index in tm

150+ -- set name supply to begin after highest index in tm

151 initNextNameFrom ns

152 elab ist info emode opts fn tm

153 probs <- get_probs

@@ -171,7 +171,7 @@ buildTC ist info emode opts fn ns tm

171 else return (ElabResult tm ds (map snd is) ctxt impls highlights)

172 where pattern = emode == ELHS

173

174−-- return whether arguments of the given constructor name can be

174+-- return whether arguments of the given constructor name can be

175-- matched on. If they're polymorphic, no, unless the type has beed made

176-- concrete by the time we get around to elaborating the argument.

177getUnmatchable :: Context -> Name -> [Bool]

@@ -180,11 +180,11 @@ getUnmatchable ctxt n | isDConName n ctxt && n /= inferCon

180 Nothing -> []

181 Just ty -> checkArgs [] [] ty

182 where checkArgs :: [Name] -> [[Name]] -> Type -> [Bool]

183− checkArgs env ns (Bind n (Pi _ t _) sc)

183+ checkArgs env ns (Bind n (Pi _ t _) sc)

184 = let env' = case t of

185 TType _ -> n : env

186 _ -> env in

187− checkArgs env' (intersect env (refsIn t) : ns)

187+ checkArgs env' (intersect env (refsIn t) : ns)

188 (instantiate (P Bound n t) sc)

189 checkArgs env ns t

190 = map (not . null) (reverse ns)

@@ -193,7 +193,7 @@ getUnmatchable ctxt n = []

193

194data ElabCtxt = ElabCtxt { e_inarg :: Bool,

195 e_isfn :: Bool, -- ^ Function part of application

196− e_guarded :: Bool,

196+ e_guarded :: Bool,

197 e_intype :: Bool,

198 e_qq :: Bool,

199 e_nomatching :: Bool -- ^ can't pattern match

@@ -267,17 +267,17 @@ elab ist info emode opts fn tm

267 -- normally correct to call elabE - the ones that don't are desugarings

268 -- typically

269 elabE :: ElabCtxt -> Maybe FC -> PTerm -> ElabD ()

270− elabE ina fc' t =

270+ elabE ina fc' t =

271 do solved <- get_recents

272 as <- get_autos

273 hs <- get_holes

274 -- If any of the autos use variables which have recently been solved,

275 -- have another go at solving them now.

276− mapM_ (\(a, (failc, ns)) ->

276+ mapM_ (\(a, (failc, ns)) ->

277 if any (\n -> n `elem` solved) ns && head hs /= a

278 then solveAuto ist fn False (a, failc)

279 else return ()) as

280−

280+

281 itm <- if not pattern then insertImpLam ina t else return t

282 ct <- insertCoerce ina itm

283 t' <- insertLazy ct

@@ -343,7 +343,7 @@ elab ist info emode opts fn tm

343-- elab' (_,_,inty) (PConstant c)

344-- | constType c && pattern && not reflection && not inty

345-- = lift $ tfail (Msg "Typecase is not allowed")

346− elab' ina fc tm@(PConstant fc' c)

346+ elab' ina fc tm@(PConstant fc' c)

347 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)

348 && isTypeConst c

349 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)

@@ -397,7 +397,7 @@ elab ist info emode opts fn tm

397 UType _ -> elab' ina (Just fc) (PApp fc (PRef fc hls upairTy)

398 [pexp l,pexp r])

399 _ -> case tc of

400− P _ n _ | n == upairTy

400+ P _ n _ | n == upairTy

401 -> elab' ina (Just fc) (PApp fc (PRef fc hls upairCon)

402 [pimp (sUN "A") Placeholder False,

403 pimp (sUN "B") Placeholder False,

@@ -509,7 +509,7 @@ elab ist info emode opts fn tm

509 ty <- goal

510 let doelab = elab' ina fc orig

511 tryCatch doelab

512− (\err ->

512+ (\err ->

513 if recoverableErr err

514 then -- trace ("NEED IMPLICIT! " ++ show orig ++ "\n" ++

515 -- show alts ++ "\n" ++

@@ -547,7 +547,7 @@ elab ist info emode opts fn tm

547 pruneAlts err alts _ = filter isLend alts

548

549 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) _)

551 = case lookupTyExact a (tt_ctxt ist) of

552 Just ty -> let args = map snd (getArgTys (normalise (tt_ctxt ist) env ty)) in

553 any (fnIs n) args

@@ -662,7 +662,7 @@ elab ist info emode opts fn tm

662 introTy (Var tyn) (Just n)

663 addPSname n -- okay for proof search

664 focus tyn

665−

665+

666 elabE (ec { e_inarg = True, e_intype = True }) (Just fc) ty

667 elabE (ec { e_inarg = True }) (Just fc) sc

668 solve

@@ -701,10 +701,10 @@ elab ist info emode opts fn tm

701 Placeholder -> return ()

702 _ -> do focus tyn

703 explicit tyn

704− elabE (ina { e_inarg = True, e_intype = True })

704+ elabE (ina { e_inarg = True, e_intype = True })

705 (Just fc) ty

706 focus valn

707− elabE (ina { e_inarg = True, e_intype = True })

707+ elabE (ina { e_inarg = True, e_intype = True })

708 (Just fc) val

709 ivs' <- get_instances

710 env <- get_env

@@ -808,14 +808,14 @@ elab ist info emode opts fn tm

808 annot <- findHighlight f

809 mapM_ checkKnownImplicit args_in

810 let args = insertScopedImps fc (normalise ctxt env fty) args_in

811− let unmatchableArgs = if pattern

811+ let unmatchableArgs = if pattern

812 then getUnmatchable (tt_ctxt ist) f

813 else []

814−-- trace ("BEFORE " ++ show f ++ ": " ++ show ty) $

814+-- trace ("BEFORE " ++ show f ++ ": " ++ show ty) $

815 when (pattern && not reflection && not (e_qq ina) && not (e_intype ina)

816 && isTConName f (tt_ctxt ist)) $

817 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)) $

819 if (f `elem` map fst env && length args == 1 && length args_in == 1)

820 then -- simple app, as below

821 do simple_app False

@@ -853,7 +853,7 @@ elab ist info emode opts fn tm

853 mapM (uncurry highlightSource) $

854 (ffc, annot) : map (\f -> (f, annot)) hls

855

856− elabArgs ist (ina { e_inarg = e_inarg ina || not isinf })

856+ elabArgs ist (ina { e_inarg = e_inarg ina || not isinf })

857 [] fc False f

858 (zip ns (unmatchableArgs ++ repeat False))

859 (f == sUN "Force")

@@ -880,7 +880,7 @@ elab ist info emode opts fn tm

880 ivs' <- get_instances

881 -- Attempt to resolve any type classes which have 'complete' types,

882 -- i.e. no holes in them

883− when (not pattern || (e_inarg ina && not tcgen &&

883+ when (not pattern || (e_inarg ina && not tcgen &&

884 not (e_guarded ina))) $

885 mapM_ (\n -> do focus n

886 g <- goal

@@ -893,14 +893,14 @@ elab ist info emode opts fn tm

893 else movelast n)

894 (ivs' \\ ivs)

895 return []

896− where

896+ where

897 -- Run the elaborator, which returns how many implicit

898 -- args were needed, then run it again with those args. We need

899 -- this because we have to elaborate the whole application to

900 -- find out whether any computations have caused more implicits

901 -- to be needed.

902 implicitApp :: ElabD [ImplicitInfo] -> ElabD ()

903− implicitApp elab

903+ implicitApp elab

904 | pattern || intransform = do elab; return ()

905 | otherwise

906 = do s <- get

@@ -909,7 +909,7 @@ elab ist info emode opts fn tm

909 [] -> return ()

910 es -> do put s

911 elab' ina topfc (PAppImpl tm es)

912−

912+

913 checkKnownImplicit imp

914 | UnknownImp `elem` argopts imp

915 = lift $ tfail $ UnknownImplicit (pname imp) f

@@ -966,7 +966,7 @@ elab ist info emode opts fn tm

966 headRef (PAlternative _ _ as) = all headRef as

967 headRef _ = False

968

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...

970 solve

971 where appImpl [] = elab' (ina { e_isfn = False }) fc f -- e_isfn not set, so no recursive expansion of implicits

972 appImpl (e : es) = simple_app False

@@ -1028,14 +1028,14 @@ elab ist info emode opts fn tm

1028 solve

1029 elab' ina _ c@(PCase fc scr opts)

1030 = do attack

1031−

1031+

1032 tyn <- getNameFrom (sMN 0 "scty")

1033 claim tyn RType

1034 valn <- getNameFrom (sMN 0 "scval")

1035 scvn <- getNameFrom (sMN 0 "scvar")

1036 claim valn (Var tyn)

1037 letbind scvn (Var tyn) (Var valn)

1038−

1038+

1039 -- Start filling in the scrutinee type, if we can work one

1040 -- out from the case options

1041 let scrTy = getScrType (map fst opts)

@@ -1056,7 +1056,7 @@ elab ist info emode opts fn tm

1056

1057 -- Drop the unique arguments used in the term already

1058 -- and in the scrutinee (since it's

1059− -- not valid to use them again anyway)

1059+ -- not valid to use them again anyway)

1060 --

1061 -- Also drop unique arguments which don't appear explicitly

1062 -- in either case branch so they don't count as used

@@ -1065,7 +1065,7 @@ elab ist info emode opts fn tm

1065 ptm <- get_term

1066 let inOpts = (filter (/= scvn) (map fst args)) \\ (concatMap (\x -> allNamesIn (snd x)) opts)

1067

1068− let argsDropped = filter (isUnique envU)

1068+ let argsDropped = filter (isUnique envU)

1069 (nub $ allNamesIn scr ++ inApp ptm ++

1070 inOpts)

1071

@@ -1097,9 +1097,9 @@ elab ist info emode opts fn tm

1097 getScrType [] = Nothing

1098 getScrType (f : os) = maybe (getScrType os) Just (getAppType f)

1099

1100− getAppType (PRef _ _ n) =

1100+ getAppType (PRef _ _ n) =

1101 case lookupTyName n (tt_ctxt ist) of

1102− [(n', ty)] | isDConName n' (tt_ctxt ist) ->

1102+ [(n', ty)] | isDConName n' (tt_ctxt ist) ->

1103 case unApply (getRetTy ty) of

1104 (P _ tyn _, args) ->

1105 Just (PApp fc (PRef fc [] tyn)

@@ -1250,12 +1250,12 @@ elab ist info emode opts fn tm

1250 [] -> lift . tfail . NoSuchVariable $ n

1251 more -> lift . tfail . CantResolveAlts $ map fst more

1252 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)

1254 | reflection = elab' ina fc t

1255 | otherwise

1256 = do (h : hs) <- get_holes

1257 -- 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)

1259 -- must be solvable by unification as well as being filled

1260 -- in directly.

1261 -- Delay dotted things to the end, then when we elaborate them

@@ -1323,7 +1323,7 @@ elab ist info emode opts fn tm

1323 -- The delayed things with lower numbered priority will be elaborated

1324 -- first. (In practice, this means delayed alternatives, then PHidden

1325 -- things.)

1326− delayElab pri t

1326+ delayElab pri t

1327 = updateAux (\e -> e { delayed_elab = delayed_elab e ++ [(pri, t)] })

1328

1329 isScr :: PTerm -> (Name, Binder Term) -> (Name, (Bool, Binder Term))

@@ -1476,7 +1476,7 @@ elab ist info emode opts fn tm

1476 let t' = case (t, cs) of

1477 (PCoerced tm, _) -> tm

1478 (_, []) -> t

1479− (_, cs) -> PAlternative [] TryImplicit

1479+ (_, cs) -> PAlternative [] TryImplicit

1480 (t : map (mkCoerce env t) cs)

1481 return t'

1482 where

@@ -1598,7 +1598,7 @@ pruneByType env (P _ n _) ist as

1598 [] -> asV

1599 _ -> as'

1600 where

1601− ctxt = tt_ctxt ist

1601+ ctxt = tt_ctxt ist

1602

1603 headIs var f (PRef _ _ f') = typeHead var f f'

1604 headIs var f (PApp _ (PRef _ _ (UN l)) [_, _, arg])

@@ -1617,7 +1617,7 @@ pruneByType env (P _ n _) ist as

1617 _ -> let ty' = normalise ctxt [] ty in

1618 case unApply (getRetTy ty') of

1619 (P _ ftyn _, _) -> ftyn == f

1620− (V _, _) ->

1620+ (V _, _) ->

1621 -- keep, variable

1622-- trace ("Keeping " ++ show (f', ty')

1623-- ++ " for " ++ show n) $

@@ -1634,22 +1634,22 @@ pruneByType _ t _ as = as

1634-- (FIXME: This isn't complete, but I'm leaving it here and coming back

1635-- to it later - just returns 'var' for now. EB)

1636isPlausible :: IState -> Bool -> Env -> Name -> Type -> Bool

1637−isPlausible ist var env n ty

1637+isPlausible ist var env n ty

1638 = let (hvar, classes) = collectConstraints [] [] ty in

1639 case hvar of

1640 Nothing -> True

1641 Just rth -> var -- trace (show (rth, classes)) var

1642 where

1643− collectConstraints :: [Name] -> [(Term, [Name])] -> Type ->

1643+ collectConstraints :: [Name] -> [(Term, [Name])] -> Type ->

1644 (Maybe Name, [(Term, [Name])])

1645 collectConstraints env tcs (Bind n (Pi _ ty _) sc)

1646 = let tcs' = case unApply ty of

1647− (P _ c _, _) ->

1647+ (P _ c _, _) ->

1648 case lookupCtxtExact c (idris_classes ist) of

1649− Just tc -> ((ty, map fst (class_instances tc))

1649+ Just tc -> ((ty, map fst (class_instances tc))

1650− : tcs)

1650+ : tcs)

1651 Nothing -> tcs

1652− _ -> tcs

1652+ _ -> tcs

1653 in

1654 collectConstraints (n : env) tcs' sc

1655 collectConstraints env tcs t

@@ -1669,7 +1669,7 @@ findHighlight n = do ctxt <- get_context

1669

1670-- Try again to solve auto implicits

1671solveAuto :: IState -> Name -> Bool -> (Name, [FailContext]) -> ElabD ()

1672−solveAuto ist fn ambigok (n, failc)

1672+solveAuto ist fn ambigok (n, failc)

1673 = do hs <- get_holes

1674 when (not (null hs)) $ do

1675 env <- get_env

@@ -1682,8 +1682,8 @@ solveAuto ist fn ambigok (n, failc)

1682 (lift $ Error (addLoc failc

1683 (CantSolveGoal g (map (\(n, b) -> (n, binderTy b)) env))))

1684 return ()

1685− where addLoc (FailContext fc f x : prev) err

1685+ where addLoc (FailContext fc f x : prev) err

1686− = At fc (ElaboratingArg f x

1686+ = At fc (ElaboratingArg f x

1687 (map (\(FailContext _ f' x') -> (f', x')) prev) err)

1688 addLoc _ err = err

1689

@@ -1728,7 +1728,7 @@ collectDeferred top casenames ctxt tm = cd [] tm

1728 t' <- collectDeferred top casenames ctxt t

1729 when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, t', psns))])

1730 cd env app

1731− cd env (Bind n b t)

1731+ cd env (Bind n b t)

1732 = do b' <- cdb b

1733 t' <- cd ((n, b) : env) t

1734 return (Bind n b' t')

@@ -1737,7 +1737,7 @@ collectDeferred top casenames ctxt tm = cd [] tm

1737 cdb (Guess t v) = liftM2 Guess (cd env t) (cd env v)

1738 cdb b = do ty' <- cd env (binderTy b)

1739 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)

1741 (cd env a)

1742 cd env t = return t

1743

@@ -2148,7 +2148,7 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

2148 | n == tacN "Prim__Fixity", [op'] <- args

2149 = do opTm <- eval op'

2150 case opTm of

2151− Constant (Str op) ->

2151+ Constant (Str op) ->

2152 let opChars = ":!#$%&*+./<=>?@\\^|-~"

2153 invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\", "%", "~", "?", "!"]

2154 fixities = idris_infixes ist

@@ -2185,7 +2185,7 @@ runTac autoSolve ist perhapsFC fn tac

2185 bname _ = Nothing

2186 runT (Intro xs) = mapM_ (\x -> do attack; intro (Just x)) xs

2187 runT Intros = do g <- goal

2188− attack;

2188+ attack;

2189 intro (bname g)

2190 try' (runT Intros)

2191 (return ()) True

@@ -2430,18 +2430,18 @@ elaboratingArgErr ((f,x):during) err = fromMaybe err (rewrite err)

2430withErrorReflection :: Idris a -> Idris a

2431withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

2432 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"

2434 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"

2436 return e

2437 -- 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"

2439 err' <- handle err

2440 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"

2442 err' <- handle err

2443 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"

2445 hs <- getFnHandlers f a

2446 err' <- if null hs

2447 then handle err

@@ -2451,8 +2451,8 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

2451 handle (ProofSearchFail e) = handle e

2452 -- TODO: argument-specific error handlers go here for ElaboratingArg

2453 handle e = do ist <- getIState

2454− logLvl 2 "Starting error reflection"

2454+ logElab 2 "Starting error reflection"

2455− logLvl 5 (show e)

2455+ logElab 5 (show e)

2456 let handlers = idris_errorhandlers ist

2457 applyHandlers e handlers

2458 getFnHandlers :: Name -> Name -> Idris [Name]

@@ -2466,7 +2466,7 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

2466 applyHandlers e handlers =

2467 do ist <- getIState

2468 let err = fmap (errReverse ist) e

2469− logLvl 3 $ "Using reflection handlers " ++

2469+ logElab 3 $ "Using reflection handlers " ++

2470 concat (intersperse ", " (map show handlers))

2471 let reports = map (\n -> RApp (Var n) (reflectErr err)) handlers

2472

@@ -2478,7 +2478,7 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

2478 -- Normalize error handler terms to produce the new messages

2479 ctxt <- getContext

2480 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))

2482

2483 -- For each handler term output, either discard it if it is Nothing or reify it the Haskell equivalent

2484 let errorpartsTT = mapMaybe unList (mapMaybe fromTTMaybe results)

@@ -2499,8 +2499,8 @@ processTacticDecls info steps =

2499 -- establish metavars that later function bodies resolve.

2500 forM_ (reverse steps) $ \case

2501 RTyDeclInstrs n fc impls ty ->

2502− do logLvl 3 $ "Declaration from tactics: " ++ show n ++ " : " ++ show ty

2502+ do logElab 3 $ "Declaration from tactics: " ++ show n ++ " : " ++ show ty

2503− logLvl 3 $ " It has impls " ++ show impls

2503+ logElab 3 $ " It has impls " ++ show impls

2504 updateIState $ \i -> i { idris_implicits =

2505 addDef n impls (idris_implicits i) }

2506 addIBC (IBCImp n)

@@ -2517,13 +2517,13 @@ processTacticDecls info steps =

2517 in addDeferred ds'

2518 _ -> return ()

2519 RAddInstance className instName ->

2520− do -- The type class resolution machinery relies on a special

2520+ do -- The type class resolution machinery relies on a special

2521− logLvl 2 $ "Adding elab script instance " ++ show instName ++

2521+ logElab 2 $ "Adding elab script instance " ++ show instName ++

2522 " for " ++ show className

2523 addInstance False True className instName

2524 addIBC (IBCInstance False True className instName)

2525 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

2527 solveDeferred n

2528 let lhss = map (\(_, lhs, _) -> lhs) cs

2529 let fc = fileFC "elab_reflected"

@@ -2553,7 +2553,7 @@ processTacticDecls info steps =

2553 calls = findCalls sc' scargs

2554 used = findUsedArgs sc' scargs'

2555 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

2557 addToCG n cg

2558 addToCalledG n (nub (map fst calls))

2559 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

53 = do ctxt <- getContext

54 i <- getIState

55 let lhs = addImplPat i lhs_in

56− logLvl 5 ("Transform LHS input: " ++ showTmImpls lhs)

56+ logElab 5 ("Transform LHS input: " ++ showTmImpls lhs)

57 (ElabResult lhs' dlhs [] ctxt' newDecls highlights, _) <-

58 tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "transLHS") infP initEState

59 (erun fc (buildTC i info ETransLHS [] (sUN "transform")

@@ -67,11 +67,11 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ _ tf) _) rhs_in

68 (clhs_tm_in, clhs_ty) <- recheckC_borrowing False False [] fc id [] lhs_tm

69 let clhs_tm = renamepats pnames clhs_tm_in

70− logLvl 3 ("Transform LHS " ++ show clhs_tm)

70+ logElab 3 ("Transform LHS " ++ show clhs_tm)

71− logLvl 3 ("Transform type " ++ show clhs_ty)

71+ logElab 3 ("Transform type " ++ show clhs_ty)

72−

72+

73 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)

76 ((rhs', defer, ctxt', newDecls), _) <-

77 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

89 (crhs_tm_in, crhs_ty) <- recheckC_borrowing False False [] fc id [] rhs'

90 let crhs_tm = renamepats pnames crhs_tm_in

91− logLvl 3 ("Transform RHS " ++ show crhs_tm)

91+ logElab 3 ("Transform RHS " ++ show crhs_tm)

93 -- Types must always convert

94 case converts ctxt [] clhs_ty crhs_ty of

@@ -118,6 +118,5 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ _ tf) _) rhs_in

118 -- with any other names when applying rules, so rename here.

119 pnames = map (\i -> sMN i ("tvar" ++ show i)) [0..]

120

121−elabTransform info fc safe lhs_in rhs_in

121+elabTransform info fc safe lhs_in rhs_in

122 = ierror (At fc (Msg "Invalid transformation rule (must be function application)"))

123−

src/Idris/Elab/Type.hs+18−21

@@ -1,5 +1,5 @@

1{-# LANGUAGE PatternGuards #-}

2−module Idris.Elab.Type (buildType, elabType, elabType',

2+module Idris.Elab.Type (buildType, elabType, elabType',

3 elabPostulate, elabExtern) where

5import Idris.AbsSyntax

@@ -52,20 +52,20 @@ import Data.List.Split (splitOn)

53import Util.Pretty(pretty, text)

55−buildType :: ElabInfo -> SyntaxInfo -> FC -> FnOpts -> Name -> PTerm ->

55+buildType :: ElabInfo -> SyntaxInfo -> FC -> FnOpts -> Name -> PTerm ->

56 Idris (Type, Type, PTerm, [(Int, Name)])

57buildType info syn fc opts n ty' = do

58 ctxt <- getContext

59 i <- getIState

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)

62 ty' <- addUsingConstraints syn fc ty'

63 ty' <- addUsingImpls syn n fc ty'

64 let ty = addImpl (imp_methods syn) i ty'

66− logLvl 5 $ show n ++ " type pre-addimpl " ++ showTmImpls ty'

66+ logElab 5 $ show n ++ " type pre-addimpl " ++ showTmImpls ty'

67− logLvl 5 $ show "with methods " ++ show (imp_methods syn)

67+ logElab 5 $ show "with methods " ++ show (imp_methods syn)

68− logLvl 2 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty

68+ logElab 2 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty

70 (ElabResult tyT' defer is ctxt' newDecls highlights, log) <-

71 tclift $ elaborate ctxt (idris_datatypes i) n (TType (UVal 0)) initEState

@@ -76,7 +76,7 @@ buildType info syn fc opts n ty' = do

77 let tyT = patToImp tyT'

79− logLvl 3 $ show ty ++ "\nElaborated: " ++ show tyT'

79+ logElab 3 $ show ty ++ "\nElaborated: " ++ show tyT'

81 ds <- checkAddDef True False fc iderr defer

82 -- 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

87 mapM_ (elabCaseBlock info opts) is

88 ctxt <- getContext

89− logLvl 5 $ "Rechecking"

89+ logElab 5 $ "Rechecking"

90− logLvl 6 $ show tyT

90+ logElab 6 $ show tyT

91− logLvl 10 $ "Elaborated to " ++ showEnvDbg [] tyT

91+ logElab 10 $ "Elaborated to " ++ showEnvDbg [] tyT

92 (cty, ckind) <- recheckC fc id [] tyT

94 -- record the implicit and inaccessible arguments

95 i <- getIState

96 let (inaccData, impls) = unzip $ getUnboundImplicits i cty ty

97 let inacc = inaccessibleImps 0 cty inaccData

98− logLvl 3 $ show n ++ ": inaccessible arguments: " ++ show inacc ++

98+ logElab 3 $ show n ++ ": inaccessible arguments: " ++ show inacc ++

99 " from " ++ show cty ++ "\n" ++ showTmImpls ty

100

101 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)

103 addIBC (IBCImp n)

104

105 when (Constructor `notElem` opts) $ do

@@ -114,7 +114,7 @@ buildType info syn fc opts n ty' = do

114 patToImp (Bind n b sc) = Bind n b (patToImp sc)

115 patToImp t = t

116

117− param_pos i ns (Bind n (Pi _ t _) sc)

117+ param_pos i ns (Bind n (Pi _ t _) sc)

118 | n `elem` ns = i : param_pos (i + 1) ns sc

119 | otherwise = param_pos (i + 1) ns sc

120 param_pos i ns t = []

@@ -140,9 +140,9 @@ elabType' norm info syn doc argDocs fc opts n nfc ty' = {- let ty' = piBind (par

140 let nty = cty -- normalise ctxt [] cty

141 -- if the return type is something coinductive, freeze the definition

142 ctxt <- getContext

143− logLvl 2 $ "Rechecked to " ++ show nty

143+ logElab 2 $ "Rechecked to " ++ show nty

144 let nty' = normalise ctxt [] nty

145− logLvl 2 $ "Rechecked to " ++ show nty'

145+ logElab 2 $ "Rechecked to " ++ show nty'

146

147 -- Add function name to internals (used for making :addclause know

148 -- the name unambiguously)

@@ -158,7 +158,7 @@ elabType' norm info syn doc argDocs fc opts n nfc ty' = {- let ty' = piBind (par

158 [TI _ True _ _ _] -> True

159 _ -> False

160 _ -> False

161− -- Productivity checking now via checking for guarded 'Delay'

161+ -- Productivity checking now via checking for guarded 'Delay'

162 let opts' = opts -- if corec then (Coinductive : opts) else opts

163 let usety = if norm then nty' else nty

164 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

177 addIBC (IBCOpt n)

178 when (Implicit `elem` opts') $ do addCoercion n

179 addIBC (IBCCoercion n)

180− when (AutoHint `elem` opts') $

180+ when (AutoHint `elem` opts') $

181 case fam of

182 P _ tyn _ -> do addAutoHint tyn n

183 addIBC (IBCAutoHint tyn n)

@@ -201,7 +201,7 @@ elabType' norm info syn doc argDocs fc opts n nfc ty' = {- let ty' = piBind (par

201 sendHighlighting [(nfc, AnnName n Nothing Nothing Nothing)]

202 -- if it's an export list type, make a note of it

203 case (unApply usety) of

204− (P _ ut _, _)

204+ (P _ ut _, _)

205 | ut == ffiexport -> do addIBC (IBCExport n)

206 addExport n

207 _ -> return ()

@@ -256,6 +256,3 @@ elabExtern info syn doc fc nfc opts n ty = do

256

257 -- remove it from the deferred definitions list

258 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

37 (tm, ty, cs) <- tclift $ case recheck_borrowing uniq_check bs ctxt env t' t of

38 Error e -> tfail (At fc (mkerr e))

39 OK x -> return x

40− logLvl 6 $ "CONSTRAINTS ADDED: " ++ show (tm, ty, cs)

40+ logElab 6 $ "CONSTRAINTS ADDED: " ++ show (tm, ty, cs)

41 when addConstrs $ addConstraints fc cs

42 mapM_ (checkDeprecated fc) (allTTNames tm)

43 mapM_ (checkDeprecated fc) (allTTNames ty)

44 return (tm, ty)

46checkDeprecated :: FC -> Name -> Idris ()

47−checkDeprecated fc n

47+checkDeprecated fc n

48 = do r <- getDeprecated n

49 case r of

50 Nothing -> return ()

@@ -64,9 +64,9 @@ checkAddDef :: Bool -> Bool -> FC -> (Name -> Err -> Err)

64 -> [(Name, (Int, Maybe Name, Type, [Name]))]

65 -> Idris [(Name, (Int, Maybe Name, Type, [Name]))]

66checkAddDef 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)

68 = do ctxt <- getContext

69− logLvl 5 $ "Rechecking deferred name " ++ show (n, t)

69+ logElab 5 $ "Rechecking deferred name " ++ show (n, t)

70 (t', _) <- recheckC fc (mkerr n) [] t

71 when add $ do addDeferred [(n, (i, top, t, psns, toplvl))]

72 addIBC (IBCDef n)

@@ -93,7 +93,7 @@ inaccessibleArgs _ _ = []

93elabCaseBlock :: ElabInfo -> FnOpts -> PDecl -> Idris ()

94elabCaseBlock info opts d@(PClauses f o n ps)

95 = do addIBC (IBCDef n)

96− logLvl 5 $ "CASE BLOCK: " ++ show (n, d)

96+ logElab 5 $ "CASE BLOCK: " ++ show (n, d)

97 let opts' = nub (o ++ opts)

98 -- propagate totality assertion to the new definitions

99 when (AssertTotal `elem` opts) $ setFlags n [AssertTotal]

@@ -104,16 +104,16 @@ elabCaseBlock info opts d@(PClauses f o n ps)

104-- they are the same!)

105checkInferred :: FC -> PTerm -> PTerm -> Idris ()

106checkInferred 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" ++

108 showTmImpls user

109− logLvl 10 $ "Checking match"

109+ logElab 10 $ "Checking match"

110 i <- getIState

111 tclift $ case matchClause' True i user inf of

112 _ -> return ()

113-- Left (x, y) -> tfail $ At fc

114-- (Msg $ "The type-checked term and given term do not match: "

115-- ++ show x ++ " and " ++ show y)

116− logLvl 10 $ "Checked match"

116+ logElab 10 $ "Checked match"

117-- ++ "\n" ++ showImp True inf ++ "\n" ++ showImp True user)

118

119-- | Return whether inferred term is different from given term

@@ -121,7 +121,7 @@ checkInferred fc inf user =

121inferredDiff :: FC -> PTerm -> PTerm -> Idris Bool

122inferredDiff fc inf user =

123 do i <- getIState

124− logLvl 6 $ "Checked to\n" ++ showTmImpls inf ++ "\n" ++

124+ logElab 6 $ "Checked to\n" ++ showTmImpls inf ++ "\n" ++

125 showTmImpls user

126 tclift $ case matchClause' True i user inf of

127 Right vs -> return False

@@ -152,7 +152,7 @@ decorateid decorate (PClauses f o n cs)

152

153-- if 't' is a type class application, assume its arguments are injective

154pbinds :: IState -> Term -> ElabD ()

155−pbinds i (Bind n (PVar t) sc)

155+pbinds i (Bind n (PVar t) sc)

156 = do attack; patbind n

157 env <- get_env

158 case unApply (normalise (tt_ctxt i) env t) of

@@ -207,14 +207,14 @@ getFlexInType i env ps tm@(App _ f a)

207 | (P nt tn _, args) <- unApply tm, nt /= Bound

208 = case lookupCtxtExact tn (idris_datatypes i) of

209 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)]

211 ++ getFlexInType i env ps f ++

212 getFlexInType i env ps a

213 Nothing -> let ppos = case lookupCtxtExact tn (idris_fninfo i) of

214 Just fi -> fn_params fi

215 Nothing -> []

216 in nub $ paramNames args env [x | x <- [0..length args],

217− not (x `elem` ppos)]

217+ not (x `elem` ppos)]

218 ++ getFlexInType i env ps f ++

219 getFlexInType i env ps a

220 | otherwise = nub $ getFlexInType i env ps f ++

@@ -228,7 +228,7 @@ getParamsInType i env ps t = let fix = getFixedInType i env ps t

228 flex = getFlexInType i env fix t in

229 [x | x <- fix, not (x `elem` flex)]

230

231−getTCinj i (Bind n (Pi _ t _) sc)

231+getTCinj i (Bind n (Pi _ t _) sc)

232 = getTCinj i t ++ getTCinj i (instantiate (P Bound n t) sc)

233getTCinj i ap@(App _ f a)

234 | (P _ n _, args) <- unApply ap,

@@ -258,7 +258,7 @@ paramNames args env (p : ps)

258getUniqueUsed :: Context -> Term -> [Name]

259getUniqueUsed ctxt tm = execState (getUniq [] [] tm) []

260 where

261− getUniq :: Env -> [(Name, Bool)] -> Term -> State [Name] ()

261+ getUniq :: Env -> [(Name, Bool)] -> Term -> State [Name] ()

262 getUniq env us (Bind n b sc)

263 = let uniq = case check ctxt env (forgetEnv (map fst env) (binderTy b)) of

264 OK (_, UType UniqueType) -> True

@@ -285,9 +285,9 @@ getUniqueUsed ctxt tm = execState (getUniq [] [] tm) []

285-- In a functional application, return the names which are used

286-- directly in a static position

287getStaticNames :: IState -> Term -> [Name]

288−getStaticNames ist (Bind n (PVar _) sc)

288+getStaticNames ist (Bind n (PVar _) sc)

289 = getStaticNames ist (instantiate (P Bound n Erased) sc)

290−getStaticNames ist tm

290+getStaticNames ist tm

291 | (P _ fn _, args) <- unApply tm

292 = case lookupCtxtExact fn (idris_statics ist) of

293 Just stpos -> getStatics args stpos

@@ -305,15 +305,12 @@ getStatics ns (Bind n (Pi _ _ _) t)

305getStatics _ _ = []

306

307mkStatic :: [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)

309 = PTy doc argdocs syn fc o n nfc (mkStaticTy ns ty)

310mkStatic ns t = t

311

312mkStaticTy :: [Name] -> PTerm -> PTerm

313−mkStaticTy ns (PPi p n fc ty sc)

313+mkStaticTy ns (PPi p n fc ty sc)

314 | n `elem` ns = PPi (p { pstatic = Static }) n fc ty (mkStaticTy ns sc)

315 | otherwise = PPi p n fc ty (mkStaticTy ns sc)

316mkStaticTy ns t = t

317−

318−

319−

src/Idris/Elab/Value.hs+4−4

@@ -1,6 +1,6 @@

1{-# LANGUAGE PatternGuards #-}

2{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

3−module Idris.Elab.Value(elabVal, elabValBind, elabDocTerms,

3+module Idris.Elab.Value(elabVal, elabValBind, elabDocTerms,

4 elabExec, elabREPL) where

6import Idris.AbsSyntax

@@ -58,7 +58,7 @@ elabValBind info aspat norm tm_in

58 = do ctxt <- getContext

59 i <- getIState

60 let tm = addImpl [] i tm_in

61− logLvl 10 (showTmImpls tm)

61+ logElab 10 (showTmImpls tm)

62 -- try:

63 -- * ordinary elaboration

64 -- * elaboration as a Type

@@ -80,7 +80,7 @@ elabValBind info aspat norm tm_in

80 addDeferred def''

81 mapM_ (elabCaseBlock info []) is

83− logLvl 3 ("Value: " ++ show vtm)

83+ logElab 3 ("Value: " ++ show vtm)

84 (vtm_in, vty) <- recheckC (fileFC "(input)") id [] vtm

86 let vtm = if norm then normalise (tt_ctxt i) [] vtm_in

@@ -127,7 +127,7 @@ elabExec fc tm = runtm (PAlternative [] FirstSuccess

127 printtm tm

128 ])

129 where

130− runtm t = PApp fc (PRef fc [] (sUN "run__IO"))

130+ runtm t = PApp fc (PRef fc [] (sUN "run__IO"))

131 [pimp (sUN "ffi") (PRef fc [] (sUN "FFI_C")) False, pexp t]

132 printtm t = PApp fc (PRef fc [] (sUN "printLn"))

133 [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)

159 = return () -- nothing to elaborate

160elabDecl' what info (PTy doc argdocs s f o n nfc ty)

161 | what /= EDefns

162− = do logLvl 1 $ "Elaborating type decl " ++ show n ++ show o

162+ = do logElab 1 $ "Elaborating type decl " ++ show n ++ show o

163 elabType info s doc argdocs f o n nfc ty

164 return ()

165elabDecl' what info (PPostulate b doc s f nfc o n ty)

166 | what /= EDefns

167− = do logLvl 1 $ "Elaborating postulate " ++ show n ++ show o

167+ = do logElab 1 $ "Elaborating postulate " ++ show n ++ show o

168− if b

168+ if b

169 then elabExtern info s doc f nfc o n ty

170 else elabPostulate info s doc f nfc o n ty

171elabDecl' what info (PData doc argDocs s f co d)

172 | what /= ETypes

173− = do logLvl 1 $ "Elaborating " ++ show (d_name d)

173+ = do logElab 1 $ "Elaborating " ++ show (d_name d)

174 elabData info s doc argDocs f co d

175 | otherwise

176− = do logLvl 1 $ "Elaborating [type of] " ++ show (d_name d)

176+ = do logElab 1 $ "Elaborating [type of] " ++ show (d_name d)

177 elabData info s doc argDocs f co (PLaterdecl (d_name d) (d_name_fc d) (d_tcon d))

178elabDecl' what info d@(PClauses f o n ps)

179 | what /= ETypes

180− = do logLvl 1 $ "Elaborating clause " ++ show n

180+ = do logElab 1 $ "Elaborating clause " ++ show n

181 i <- getIState -- get the type options too

182 let o' = case lookupCtxt n (idris_flags i) of

183 [fs] -> fs

@@ -191,11 +191,11 @@ elabDecl' what info (PMutual f ps)

191 -- record mutually defined data definitions

192 let datans = concatMap declared (filter isDataDecl ps)

193 mapM_ (setMutData datans) datans

194− logLvl 1 $ "Rechecking for positivity " ++ show datans

194+ logElab 1 $ "Rechecking for positivity " ++ show datans

195 mapM_ (\x -> do setTotality x Unchecked) datans

196 -- Do totality checking after entire mutual block

197 i <- get

198− mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n

198+ mapM_ (\n -> do logElab 5 $ "Simplifying " ++ show n

199 ctxt' <- do ctxt <- getContext

200 tclift $ simplifyCasedef n (getErasureInfo i) ctxt

201 setContext ctxt')

@@ -216,7 +216,7 @@ elabDecl' what info (PMutual f ps)

216

217elabDecl' what info (PParams f ns ps)

218 = do i <- getIState

219− logLvl 1 $ "Expanding params block with " ++ show ns ++ " decls " ++

219+ logElab 1 $ "Expanding params block with " ++ show ns ++ " decls " ++

220 show (concatMap tldeclared ps)

221 let nblock = pblock i

222 mapM_ (elabDecl' what info) nblock

@@ -240,17 +240,17 @@ elabDecl' what info (PNamespace n nfc ps) =

240

241elabDecl' what info (PClass doc s f cs n nfc ps pdocs fds ds cn cd)

242 | what /= EDefns

243− = do logLvl 1 $ "Elaborating class " ++ show n

243+ = do logElab 1 $ "Elaborating class " ++ show n

244 elabClass info (s { syn_params = [] }) doc f cs n nfc ps pdocs fds ds cn cd

245elabDecl' 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

247 elabInstance info s doc argDocs what f cs n nfc ps t expn ds

248elabDecl' 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

250 elabRecord info what doc rsyn fc opts name nfc ps pdocs fs cname cdoc csyn

251{-

252 | otherwise

253− = do logLvl 1 $ "Elaborating [type of] " ++ show tyn

253+ = do logElab 1 $ "Elaborating [type of] " ++ show tyn

254 elabData info s doc [] f [] (PLaterdecl tyn ty)

255-}

256elabDecl' _ info (PDSL n dsl)

@@ -261,7 +261,7 @@ elabDecl' what info (PDirective i)

261 | what /= EDefns = directiveAction i

262elabDecl' what info (PProvider doc syn fc nfc provWhat n)

263 | what /= EDefns

264− = do logLvl 1 $ "Elaborating type provider " ++ show n

264+ = do logElab 1 $ "Elaborating type provider " ++ show n

265 elabProvider doc info syn fc nfc provWhat n

266elabDecl' what info (PTransform fc safety old new)

267 = do elabTransform info fc safety old new

src/Idris/Erasure.hs+12−12

@@ -85,10 +85,10 @@ performUsageAnalysis startNames = do

85 usage = M.toList minUse

87 -- Print some debug info.

88− logLvl 5 $ "Original deps:\n" ++ unlines (map fmtItem . M.toList $ depMap)

88+ logErasure 5 $ "Original deps:\n" ++ unlines (map fmtItem . M.toList $ depMap)

89− logLvl 3 $ "Reachable names:\n" ++ unlines (map (indent . show) . S.toList $ reachableNames)

89+ logErasure 3 $ "Reachable names:\n" ++ unlines (map (indent . show) . S.toList $ reachableNames)

90− logLvl 4 $ "Minimal usage:\n" ++ fmtUseMap usage

90+ logErasure 4 $ "Minimal usage:\n" ++ fmtUseMap usage

91− logLvl 5 $ "Residual deps:\n" ++ unlines (map fmtItem . M.toList $ residDeps)

91+ logErasure 5 $ "Residual deps:\n" ++ unlines (map fmtItem . M.toList $ residDeps)

93 -- Check that everything reachable is accessible.

94 checkEnabled <- (WarnReach `elem`) . opt_cmdline . idris_options <$> getIState

@@ -135,7 +135,7 @@ performUsageAnalysis startNames = do

135 where

136 fmt n [] = show n ++ " (no more information available)"

137 fmt n rs = show n ++ " from " ++ intercalate ", " [show rn ++ " arg# " ++ show ri | (rn,ri) <- rs]

138− warn = logLvl 0

138+ warn = logErasure 0

139

140-- Find the minimal consistent usage by forward chaining.

141minimalUsage :: Deps -> (Deps, (Set Name, UseMap))

@@ -150,7 +150,7 @@ minimalUsage = second gather . forwardChain

150

151forwardChain :: Deps -> (Deps, DepSet)

152forwardChain deps

153− | Just trivials <- M.lookup S.empty deps

153+ | Just trivials <- M.lookup S.empty deps

154 = (M.unionWith S.union trivials)

155 `second` forwardChain (remove trivials . M.delete S.empty $ deps)

156 | otherwise = (deps, M.empty)

@@ -164,7 +164,7 @@ forwardChain deps

164-- starting the depth-first search from a list of Names.

165buildDepMap :: Ctxt ClassInfo -> [(Name, Int)] -> [(Name, Int)] ->

166 Context -> [Name] -> Deps

167−buildDepMap ci used externs ctx startNames

167+buildDepMap ci used externs ctx startNames

168 = addPostulates used $ dfs S.empty M.empty startNames

169 where

170 -- mark the result of Main.main as used with the empty assumption

@@ -181,7 +181,7 @@ buildDepMap ci used externs ctx startNames

181 usedNames = allNames deps S.\\ specialPrims

182 usedPrims = [(p_name p, p_arity p) | p <- primitives, p_name p `S.member` usedNames]

183

184− postulates used =

184+ postulates used =

185 [ [] ==> concat

186 -- Main.main ( + export lists) and run__IO, are always evaluated

187 -- but they elude analysis since they come from the seed term.

@@ -190,7 +190,7 @@ buildDepMap ci used externs ctx startNames

190 ,[(sUN "call__IO", Result), (sUN "call__IO", Arg 2)]

191

192 -- Explicit usage declarations from a %used pragma

193− , map (\(n, i) -> (n, Arg i)) used

193+ , map (\(n, i) -> (n, Arg i)) used

194

195 -- MkIO is read by run__IO,

196 -- but this cannot be observed in the source code of programs.

@@ -200,7 +200,7 @@ buildDepMap ci used externs ctx startNames

200 -- Foreign calls are built with pairs, but mkForeign doesn't

201 -- have an implementation so analysis won't see them

202 , [(pairCon, Arg 2),

203− (pairCon, Arg 3)] -- Used in foreign calls

203+ (pairCon, Arg 3)] -- Used in foreign calls

204

205 -- these have been discovered as builtins but are not listed

206 -- among Idris.Primitives.primitives

@@ -211,7 +211,7 @@ buildDepMap ci used externs ctx startNames

211 -- believe_me is a primitive but it only uses its third argument

212 -- it is special-cased in usedNames above

213 , it "prim__believe_me" [2]

214−

214+

215 -- in general, all other primitives use all their arguments

216 , [(n, Arg i) | (n,arity) <- usedPrims, i <- [0..arity-1]]

217

@@ -324,7 +324,7 @@ buildDepMap ci used externs ctx startNames

324 , viMethod = meth j

325 })

326 | (v, j) <- zip ns [0..]]

327−

327+

328 -- this is safe because it's certainly a patvar

329 varIdx = fromJust (viFunArg var)

330

src/Idris/IBC.hs+20−18

@@ -113,7 +113,7 @@ loadIBC reexport fp

113 Nothing -> True

114 Just p -> not p && reexport

115 when redo $

116− do logLvl 1 $ "Loading ibc " ++ fp ++ " " ++ show reexport

116+ do logIBC 1 $ "Loading ibc " ++ fp ++ " " ++ show reexport

117 archiveFile <- runIO $ B.readFile fp

118 case toArchiveOrFail archiveFile of

119 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

189

190writeIBC :: FilePath -> FilePath -> Idris ()

191writeIBC src f

192− = do logLvl 1 $ "Writing ibc " ++ show f

192+ = do logIBC 1 $ "Writing ibc " ++ show f

193 i <- getIState

194-- case (Data.List.map fst (idris_metavars i)) \\ primDefs of

195-- (_:_) -> ifail "Can't write ibc when there are unsolved metavariables"

@@ -198,8 +198,8 @@ writeIBC src f

198 ibcf <- mkIBC (ibc_write i) (initIBC { sourcefile = src })

199 idrisCatch (do runIO $ createDirectoryIfMissing True (dropFileName f)

200 writeArchive f ibcf

201− logLvl 1 "Written")

201+ logIBC 1 "Written")

202− (\c -> do logLvl 1 $ "Failed " ++ pshow i c)

202+ (\c -> do logIBC 1 $ "Failed " ++ pshow i c)

203 return ()

204

205-- Write a package index containing all the imports in the current IState

@@ -208,20 +208,20 @@ writePkgIndex :: FilePath -> Idris ()

208writePkgIndex f

209 = do i <- getIState

210 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" ++

212 show (map snd imps)

213 resetNameIdx

214 let ibcf = initIBC { ibc_imports = imps }

215 idrisCatch (do runIO $ createDirectoryIfMissing True (dropFileName f)

216 writeArchive f ibcf

217− logLvl 1 "Written")

217+ logIBC 1 "Written")

218− (\c -> do logLvl 1 $ "Failed " ++ pshow i c)

218+ (\c -> do logIBC 1 $ "Failed " ++ pshow i c)

219 return ()

220

221mkIBC :: [IBCWrite] -> IBCFile -> Idris IBCFile

222mkIBC [] f = return f

223mkIBC (i:is) f = do ist <- getIState

224− logLvl 5 $ show i ++ " " ++ show (L.length is)

224+ logIBC 5 $ show i ++ " " ++ show (L.length is)

225 f' <- ibc ist i f

226 mkIBC is f'

227

@@ -319,7 +319,7 @@ process :: Bool -- ^ Reexporting

319process reexp i fn = do

320 ver <- getEntry 0 "ver" i

321 when (ver /= ibcVersion) $ do

322− logLvl 1 "ibc out of date"

322+ logIBC 1 "ibc out of date"

323 let e = if ver < ibcVersion

324 then " an earlier " else " a later "

325 ifail $ "Incompatible ibc version.\nThis library was built with"

@@ -415,10 +415,12 @@ pImports reexp fs

415-- then logLvl 1 $ "Already read " ++ f

416 putIState (i { imported = f : imported i })

417 case fp of

418+ LIDR fn -> do

418− LIDR fn -> do logLvl 1 $ "Failed at " ++ fn

419+ logIBC 1 $ "Failed at " ++ fn

419− ifail "Must be an ibc"

420+ ifail "Must be an ibc"

421+ IDR fn -> do

420− IDR fn -> do logLvl 1 $ "Failed at " ++ fn

422+ logIBC 1 $ "Failed at " ++ fn

421− ifail "Must be an ibc"

423+ ifail "Must be an ibc"

422 IBC fn src -> loadIBC (reexp && re) fn)

424 IBC fn src -> loadIBC (reexp && re) fn)

423 fs

425 fs

424

426

@@ -515,13 +517,13 @@ pDefs reexp ds

515 do d' <- updateDef d

517 do d' <- updateDef d

516 case d' of

518 case d' of

517 TyDecl _ _ -> return ()

519 TyDecl _ _ -> return ()

518− _ -> do logLvl 1 $ "SOLVING " ++ show n

520+ _ -> do logIBC 1 $ "SOLVING " ++ show n

519 solveDeferred n

521 solveDeferred n

520 updateIState (\i -> i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })

522 updateIState (\i -> i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })

521-- logLvl 1 $ "Added " ++ show (n, d')

523-- 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

523 setAccessibility n Hidden

525 setAccessibility n Hidden

524− else logLvl 1 $ "Exporting " ++ show n) ds

526+ else logIBC 1 $ "Exporting " ++ show n) ds

525 where

527 where

526 updateDef (CaseOp c t args o s cd)

528 updateDef (CaseOp c t args o s cd)

527 = do o' <- mapM updateOrig o

529 = do o' <- mapM updateOrig o

@@ -586,7 +588,7 @@ pAccess :: Bool -- ^ Reexporting?

586pAccess reexp ds

588pAccess reexp ds

587 = mapM_ (\ (n, a_in) ->

589 = mapM_ (\ (n, a_in) ->

588 do let a = if reexp then a_in else Hidden

590 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

590 updateIState (\i -> i { tt_ctxt = setAccess n a (tt_ctxt i) })) ds

592 updateIState (\i -> i { tt_ctxt = setAccess n a (tt_ctxt i) })) ds

591

593

592pFlags :: [(Name, [FnOpt])] -> Idris ()

594pFlags :: [(Name, [FnOpt])] -> Idris ()

@@ -1843,7 +1845,7 @@ instance Binary PTerm where

1843 _ -> error "Corrupted binary data for PTerm"

1845 _ -> error "Corrupted binary data for PTerm"

1844

1846

1845instance Binary PAltType where

1847instance Binary PAltType where

1846− put x

1848+ put x

1847 = case x of

1849 = case x of

1848 ExactlyOne x1 -> do putWord8 0

1850 ExactlyOne x1 -> do putWord8 0

1849 put x1

1851 put x1

src/Idris/Parser.hs+13−13

@@ -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

@@ -1552,7 +1552,7 @@ loadModule' f

1552 ids <- allImportDirs

1553 fp <- findImport ids ibcsd file

1554 if file `elem` imported i

1555− then do logLvl 1 $ "Already read " ++ file

1555+ then do logParser 1 $ "Already read " ++ file

1556 return Nothing

1557 else do putIState (i { imported = file : imported i })

1558 case fp of

@@ -1560,7 +1560,7 @@ loadModule' f

1560 LIDR fn -> loadSource True fn Nothing

1561 IBC fn src ->

1562 idrisCatch (loadIBC True fn)

1563− (\c -> do logLvl 1 $ fn ++ " failed " ++ pshow i c

1563+ (\c -> do logParser 1 $ fn ++ " failed " ++ pshow i c

1564 case src of

1565 IDR sfn -> loadSource False sfn Nothing

1566 LIDR sfn -> loadSource True sfn Nothing)

@@ -1569,7 +1569,7 @@ loadModule' f

1569{- | Load idris code from file -}

1570loadFromIFile :: Bool -> IFileType -> Maybe Int -> Idris ()

1571loadFromIFile reexp i@(IBC fn src) maxline

1572− = do logLvl 1 $ "Skipping " ++ getSrcFile i

1572+ = do logParser 1 $ "Skipping " ++ getSrcFile i

1573 idrisCatch (loadIBC reexp fn)

1574 (\err -> ierror $ LoadingFailed fn err)

1575 where

@@ -1593,7 +1593,7 @@ loadSource' lidr r maxline

1593{- | Load Idris source code-}

1594loadSource :: Bool -> FilePath -> Maybe Int -> Idris ()

1595loadSource lidr f toline

1596− = do logLvl 1 ("Reading " ++ f)

1596+ = do logParser 1 ("Reading " ++ f)

1597 i <- getIState

1598 let def_total = default_total i

1599 file_in <- runIO $ readSource f

@@ -1637,7 +1637,7 @@ loadSource lidr f toline

1637 ]

1638 histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames

1639 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)

1641 (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n

1642

1643 i <- getIState

@@ -1676,7 +1676,7 @@ loadSource lidr f toline

1676 -- Parsing done, now process declarations

1677

1678 let ds = namespaces mname ds'

1679− logLvl 3 (show $ showDecls verbosePPOption ds)

1679+ logParser 3 (show $ showDecls verbosePPOption ds)

1680 i <- getIState

1681 logLvl 10 (show (toAlist (idris_implicits i)))

1682 logLvl 3 (show (idris_infixes i))

src/Idris/REPL.hs+24−22

@@ -801,11 +801,11 @@ process fn (ModImport f) = do fmod <- loadModule f

801 Nothing -> iPrintError $ "Can't find import " ++ f

802process fn (Eval t)

803 = withErrorReflection $

804− do logLvl 5 $ show t

804+ do logParser 5 $ show 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"]

@@ -814,8 +814,8 @@ process fn (Eval t)

814 -- Add value to context, call it "it"

815 updateContext (addCtxtDef (sUN "it") (Function ty' tm'))

816 ist <- getIState

817− logLvl 3 $ "Raw: " ++ show (tm', ty')

817+ logParser 3 $ "Raw: " ++ show (tm', ty')

818− logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'

818+ logParser 10 $ "Debug: " ++ showEnvDbg [] tm'

819 let tmDoc = pprintDelab ist tm'

820 -- errReverse to make type more readable

821 tyDoc = pprintDelab ist (errReverse ist ty')

@@ -824,7 +824,7 @@ process fn (Eval t)

824 | otherwise = tm

825

826process 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))

828 mapM_ defineName namedGroups where

829 namedGroups = groupBy (\d1 d2 -> getName d1 == getName d2) decls

830 getName :: PDecl -> Maybe Name

@@ -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

@@ -1252,7 +1253,7 @@ process fn (DynamicLink l)

1252 Nothing -> iPrintError $ "Could not load dynamic lib \"" ++ l ++ "\""

1253 Nothing -> iPrintError $ "Could not load dynamic lib \"" ++ l ++ "\""

1253 Just x -> do let libs = idris_dynamic_libs i

1254 Just x -> do let libs = idris_dynamic_libs i

1254 if x `elem` libs

1255 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)

1256 return ()

1257 return ()

1257 else putIState $ i { idris_dynamic_libs = x:libs }

1258 else putIState $ i { idris_dynamic_libs = x:libs }

1258 where trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace

1259 where trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace

@@ -1523,18 +1524,18 @@ loadInputs inputs toline -- furthest line to read in input source files

1523

1524

1524 importlists <- getImports [] inputs

1525 importlists <- getImports [] inputs

1525

1526

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))

1527

1528

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

1535 let ifiles = getModuleFiles modTree

1536 let ifiles = getModuleFiles modTree

1536− logLvl 1 ("MODULE TREE : " ++ show modTree)

1537+ logParser 1 ("MODULE TREE : " ++ show modTree)

1537− logLvl 1 ("RELOAD: " ++ show ifiles)

1538+ logParser 1 ("RELOAD: " ++ show ifiles)

1538 when (not (all ibc ifiles) || loadCode) $

1539 when (not (all ibc ifiles) || loadCode) $

1539 tryLoad False (filter (not . ibc) ifiles)

1540 tryLoad False (filter (not . ibc) ifiles)

1540 -- return the files that need rechecking

1541 -- return the files that need rechecking

@@ -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+34−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+ , ( ["logcats"]

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,25 @@ 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 (strLogCat IParse) >> return parserCats)

411+ <|> try (P.symbol (strLogCat IElab) >> return elabCats)

412+ <|> try (P.symbol (strLogCat ICodeGen) >> return codegenCats)

413+ <|> try (P.symbol (strLogCat ICoverage) >> return [ICoverage])

414+ <|> try (P.symbol (strLogCat IIBC) >> return [IIBC])

415+ <|> try (P.symbol (strLogCat IErasure) >> return [IErasure])

416+ <|> badCat

417+

395cmd_let :: String -> P.IdrisParser (Either String Command)

418cmd_let :: String -> P.IdrisParser (Either String Command)

396cmd_let name = do

419cmd_let name = do

397 defn <- concat <$> many (P.decl defaultSyntax)

420 defn <- concat <$> many (P.decl defaultSyntax)

src/Util/System.hs+2

@@ -24,6 +24,8 @@ import System.IO.Error

25#ifdef FREESTANDING

26import Tools_idris

27+import System.FilePath (isAbsolute, dropFileName)

28+import System.Directory (doesDirectoryExist)

27import System.Environment (getEnv, setEnv, getExecutablePath)

29import System.Environment (getEnv, setEnv, getExecutablePath)

28#endif

30#endif

stack.yaml+6−6

@@ -2,12 +2,12 @@ resolver: lts-3.16

2packages:

3- '.'

4flags:

5− # idris:

5+ idris:

6− # FFI: true

6+ FFI: true

7− # GMP: True

7+ GMP: True

8− # curses: True

8+ curses: True

9extra-deps:

10- annotated-wl-pprint-0.7.0

11- cheapskate-0.1.0.4

12−# - hscurses-1.4.2.0

12+- hscurses-1.4.2.0

13−# - libffi-0.1

13+- libffi-0.1