92923b7 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #539 from david-christiansen/errort

ErrorT

commit92923b7cd60784ee926f5b775d6e6d041fe46536 authorEdwin Brady <edwin.brady@gmail.com> dateWed 16 Oct 2013, 06:18 (13 years ago) parent3544af3 63038b3

16 files changed+192−182

compare with master

unifiedsplit

src/Core/Execute.hs+2−2 src/Core/TT.hs+4 src/IRTS/Compiler.hs+7−6 src/IRTS/LParser.hs+4−3 src/Idris/AbsSyntax.hs+20−20 src/Idris/AbsSyntaxTree.hs+2−1 src/Idris/ElabDecls.hs+19−19 src/Idris/Error.hs+22−29 src/Idris/IBC.hs+15−14 src/Idris/Parser.hs+5−4 src/Idris/Prover.hs+12−13 src/Idris/Providers.hs+3−3 src/Idris/REPL.hs+71−66 src/Idris/Unlit.hs+3 src/Main.hs+2−1 src/Pkg/Package.hs+1−1

src/Core/Execute.hs+2−2

@@ -159,8 +159,8 @@ debugThunks = do st <- getExecState

159159execute :: Term -> Idris Term

160160execute tm = do est <- initState

161161 ctxt <- getContext

162− res <- lift $ flip runExec est $ do res <- doExec [] ctxt tm

163− toTT res

162+ res <- lift . lift $ flip runExec est $ do res <- doExec [] ctxt tm

163+ toTT res

164164 case res of

165165 Left err -> fail err

166166 Right tm' -> return tm'

src/Core/TT.hs+4

@@ -21,6 +21,7 @@

2121module Core.TT where

2222

2323import Control.Monad.State

24+import Control.Monad.Trans.Error (Error(..))

2425import Debug.Trace

2526import qualified Data.Map as Map

2627import Data.Char

@@ -133,6 +134,9 @@ instance Pretty Err where

133134 pretty (ProviderError msg) = text msg

134135 pretty _ = text "Error"

135136

137+instance Error Err where

138+ strMsg = Msg

139+

136140data TC a = OK a

137141 | Error Err

138142 deriving (Eq, Functor)

src/IRTS/Compiler.hs+7−6

@@ -19,6 +19,7 @@ import IRTS.Inliner

1919

2020import Idris.AbsSyntax

2121import Idris.UnusedArgs

22+import Idris.Error

2223

2324import Core.TT

2425import Core.Evaluate

@@ -91,11 +92,11 @@ compile codegen f tm

9192 ViaLLVM -> codegenLLVM c triple cpu optimize f outty

9293

9394 Bytecode -> dumpBC c f

94− Error e -> fail $ show e

95+ Error e -> ierror e

9596 where checkMVs = do i <- getIState

9697 case idris_metavars i \\ primDefs of

9798 [] -> return ()

98− ms -> fail $ "There are undefined metavariables: " ++ show ms

99+ ms -> ifail $ "There are undefined metavariables: " ++ show ms

99100 inDir d h = do let f = d </> h

100101 ex <- doesFileExist f

101102 if ex then return f else return h

@@ -249,7 +250,7 @@ instance ToIR (TT Name) where

249250-- = return $ LConst (BI 0)

250251 ir' env (P _ n _) = return $ LV (Glob n)

251252 ir' env (V i) | i >= 0 && i < length env = return $ LV (Glob (env!!i))

252− | otherwise = error $ "IR fail " ++ show i ++ " " ++ show tm

253+ | otherwise = ifail $ "IR fail " ++ show i ++ " " ++ show tm

253254 ir' env (Bind n (Lam _) sc)

254255 = do let n' = uniqueName n env

255256 sc' <- ir' (n' : env) sc

@@ -286,14 +287,14 @@ instance ToIR (TT Name) where

286287 = let maybeTys = getFTypes fgnArgTys

287288 rty = mkIty' ret in

288289 case maybeTys of

289− Nothing -> fail $ "Foreign type specification is not a constant list: " ++ show (fgn:args)

290+ Nothing -> ifail $ "Foreign type specification is not a constant list: " ++ show (fgn:args)

290291 Just tys -> do

291292 args' <- mapM (ir' env) (init args)

292293 -- wrap it in a prim__IO

293294 -- return $ con_ 0 @@ impossible @@

294295 return $ -- LLazyExp $

295296 LForeign LANG_C rty fgnName (zip tys args')

296− | otherwise = fail "Badly formed foreign function call"

297+ | otherwise = ifail "Badly formed foreign function call"

297298

298299getFTypes :: TT Name -> Maybe [FType]

299300getFTypes tm = case unApply tm of

@@ -386,7 +387,7 @@ instance ToIR SC where

386387 LConst (BI 1)]) rhs')

387388-- return $ LSucCase n rhs'

388389 mkIRAlt _ (ConstCase c rhs)

389− = fail $ "Can't match on (" ++ show c ++ ")"

390+ = ifail $ "Can't match on (" ++ show c ++ ")"

390391 mkIRAlt _ (DefaultCase rhs)

391392 = do rhs' <- ir rhs

392393 return $ LDefaultCase rhs'

src/IRTS/LParser.hs+4−3

@@ -24,6 +24,7 @@ import Control.Monad.State

2424import Debug.Trace

2525import Data.Maybe

2626import System.FilePath

27+import Idris.Error

2728

2829type TokenParser a = PTok.TokenParser a

2930

@@ -62,14 +63,14 @@ fovm cgn outty f

6263 OK c -> case cgn of

6364 ViaC -> codegenC c "a.out" outty ["math.h"] "" "" "" TRACE

6465 ViaJava -> codegenJava [] c "a.out" [] [] outty

65− Error e -> fail $ show e

66+ Error e -> fail (show e)

6667

6768parseFOVM :: FilePath -> IO [(Name, LDecl)]

6869parseFOVM fname = do -- putStrLn $ "Reading " ++ fname

6970 fp <- readFile fname

7071 case runParser pProgram () fname fp of

71− Left err-> fail (show err)

72− Right x -> return x

72+ Left err -> fail (show err)

73+ Right x -> return x

7374

7475pProgram :: LParser [(Name, LDecl)]

7576pProgram = do fs <- many1 pLDecl

src/Idris/AbsSyntax.hs+20−20

@@ -60,7 +60,7 @@ addDyLib libs = do i <- getIState

6060 case mapMaybe (findDyLib ls) libs of

6161 x:_ -> return (Left x)

6262 [] -> do

63− handle <- lift $ mapM (\l -> catchIO (tryLoadLib l) (\_ -> return Nothing)) $ libs

63+ handle <- lift . lift $ mapM (\l -> catchIO (tryLoadLib l) (\_ -> return Nothing)) $ libs

6464 case msum handle of

6565 Nothing -> return (Right $ "Could not load dynamic alternatives \"" ++

6666 concat (intersperse "," libs) ++ "\"")

@@ -277,25 +277,25 @@ solveDeferred :: Name -> Idris ()

277277solveDeferred n = do i <- getIState

278278 putIState $ i { idris_metavars = idris_metavars i \\ [n] }

279279

280−iResult :: String -> Idris ()

281−iResult s = do i <- getIState

282− case idris_outputmode i of

283− RawOutput -> case s of

284− "" -> return ()

285− s -> liftIO $ putStrLn s

286− IdeSlave n ->

287− let good = SexpList [SymbolAtom "ok", toSExp s] in

288− liftIO $ putStrLn $ convSExp "return" good n

289−

290−iFail :: String -> Idris ()

291−iFail s = do i <- getIState

292− case idris_outputmode i of

293− RawOutput -> case s of

294− "" -> return ()

295− s -> liftIO $ putStrLn s

296− IdeSlave n ->

297− let good = SexpList [SymbolAtom "error", toSExp s] in

298− liftIO . putStrLn $ convSExp "return" good n

280+iPrintResult :: String -> Idris ()

281+iPrintResult s = do i <- getIState

282+ case idris_outputmode i of

283+ RawOutput -> case s of

284+ "" -> return ()

285+ s -> liftIO $ putStrLn s

286+ IdeSlave n ->

287+ let good = SexpList [SymbolAtom "ok", toSExp s] in

288+ liftIO $ putStrLn $ convSExp "return" good n

289+

290+iPrintError :: String -> Idris ()

291+iPrintError s = do i <- getIState

292+ case idris_outputmode i of

293+ RawOutput -> case s of

294+ "" -> return ()

295+ s -> liftIO $ putStrLn s

296+ IdeSlave n ->

297+ let good = SexpList [SymbolAtom "error", toSExp s] in

298+ liftIO . putStrLn $ convSExp "return" good n

299299

300300iputStrLn :: String -> Idris ()

301301iputStrLn s = do i <- getIState

src/Idris/AbsSyntaxTree.hs+2−1

@@ -20,6 +20,7 @@ import System.Console.Haskeline

2020

2121

2222import Control.Monad.Trans.State.Strict

23+import Control.Monad.Trans.Error

2324

2425import Data.List

2526import Data.Char

@@ -187,7 +188,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

187188-- | The monad for the main REPL - reading and processing files and updating

188189-- global state (hence the IO inner monad).

189190--type Idris = WriterT [Either String (IO ())] (State IState a))

190−type Idris = StateT IState IO

191+type Idris = StateT IState (ErrorT Err IO)

191192

192193-- Commands in the REPL

193194

src/Idris/ElabDecls.hs+19−19

@@ -289,21 +289,21 @@ elabProvider info syn fc n ty tm

289289 = do i <- getIState

290290 -- Ensure that the experimental extension is enabled

291291 unless (TypeProviders `elem` idris_language_extensions i) $

292− fail $ "Failed to define type provider \"" ++ show n ++

293− "\".\nYou must turn on the TypeProviders extension."

292+ ifail $ "Failed to define type provider \"" ++ show n ++

293+ "\".\nYou must turn on the TypeProviders extension."

294294

295295 ctxt <- getContext

296296

297297 -- First elaborate the expected type (and check that it's a type)

298298 (ty', typ) <- elabVal toplevel False ty

299299 unless (isTType typ) $

300− fail ("Expected a type, got " ++ show ty' ++ " : " ++ show typ)

300+ ifail ("Expected a type, got " ++ show ty' ++ " : " ++ show typ)

301301

302302 -- Elaborate the provider term to TT and check that the type matches

303303 (e, et) <- elabVal toplevel False tm

304304 unless (isProviderOf ty' et) $

305− fail $ "Expected provider type IO (Provider (" ++

306− show ty' ++ "))" ++ ", got " ++ show et ++ " instead."

305+ ifail $ "Expected provider type IO (Provider (" ++

306+ show ty' ++ "))" ++ ", got " ++ show et ++ " instead."

307307

308308 -- Create the top-level type declaration

309309 elabType info syn "" fc [] n ty

@@ -376,7 +376,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

376376 i <- getIState

377377 cty <- case lookupTy cn (tt_ctxt i) of

378378 [t] -> return (delab i t)

379− _ -> fail "Something went inexplicably wrong"

379+ _ -> ifail "Something went inexplicably wrong"

380380 cimp <- case lookupCtxt cn (idris_implicits i) of

381381 [imps] -> return imps

382382 let ptys = getProjs [] (renameBs cimp cty)

@@ -784,7 +784,7 @@ elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])

784784 = do let tcgen = Dictionary `elem` opts

785785 b <- checkPossible info fc tcgen fname lhs_in

786786 case b of

787− True -> fail $ show fc ++ ":" ++ show lhs_in ++ " is a possible case"

787+ True -> ifail $ show fc ++ ":" ++ show lhs_in ++ " is a possible case"

788788 False -> do ptm <- mkPatTm lhs_in

789789 return (Left ptm)

790790elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

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

10421042 mkAuxC wname lhs ns ns' (PClauses fc o n cs)

10431043 | True = do cs' <- mapM (mkAux wname lhs ns ns') cs

10441044 return $ PClauses fc o wname cs'

1045− | otherwise = fail $ show fc ++ "with clause uses wrong function name " ++ show n

1045+ | otherwise = ifail $ show fc ++ "with clause uses wrong function name " ++ show n

10461046 mkAuxC wname lhs ns ns' d = return $ d

10471047

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

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

10511051 logLvl 2 ("Matching " ++ showImp Nothing True False tm ++ " against " ++

10521052 showImp Nothing True False toplhs)

10531053 case matchClause i toplhs tm of

1054− Left f -> fail $ show fc ++ ":with clause does not match top level"

1054+ Left f -> ifail $ show fc ++ ":with clause does not match top level"

10551055 Right mvars ->

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

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

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

10631063 showImp Nothing True False toplhs)

10641064 withs' <- mapM (mkAuxC wname toplhs ns ns') withs

10651065 case matchClause i toplhs tm of

1066− Left _ -> fail $ show fc ++ "with clause does not match top level"

1066+ Left _ -> ifail $ show fc ++ "with clause does not match top level"

10671067 Right mvars ->

10681068 do lhs <- updateLHS n wname mvars ns ns' (fullApp tm) w

10691069 return $ PWith fc wname lhs ws wval withs'

10701070 mkAux wname toplhs ns ns' c

1071− = fail $ show fc ++ "badly formed with clause"

1071+ = ifail $ show fc ++ "badly formed with clause"

10721072

10731073 updateLHS n wname mvars ns_in ns_in' (PApp fc (PRef fc' n') args) w

10741074 = let ns = map (keepMvar (map fst mvars) fc') ns_in

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

10771077 PApp fc (PRef fc' wname)

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

10791079 updateLHS n wname mvars ns ns' tm w

1080− = fail $ "Not implemented match " ++ show tm

1080+ = ifail $ "Not implemented match " ++ show tm

10811081

10821082 keepMvar mvs fc v | v `elem` mvs = PRef fc v

10831083 | otherwise = Placeholder

@@ -1161,7 +1161,7 @@ elabClass info syn doc fc constraints tn ps ds

11611161 return ( (n, (toExp (map fst ps) Exp t')),

11621162 (n, (doc, o, (toExp (map fst ps) Imp t'))),

11631163 (n, (syn, o, t) ) )

1164− tdecl _ _ = fail "Not allowed in a class declaration"

1164+ tdecl _ _ = ifail "Not allowed in a class declaration"

11651165

11661166 -- Create default definitions

11671167 defdecl mtys c d@(PClauses fc opts n cs) =

@@ -1172,8 +1172,8 @@ elabClass info syn doc fc constraints tn ps ds

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

11731173 iLOG (show ds)

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

1175− _ -> fail $ show n ++ " is not a method"

1176− defdecl _ _ _ = fail "Can't happen (defdecl)"

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

1176+ defdecl _ _ _ = ifail "Can't happen (defdecl)"

11771177

11781178 defaultdec (UN n) = UN ("default#" ++ n)

11791179 defaultdec (NS n ns) = NS (defaultdec n) ns

@@ -1263,7 +1263,7 @@ elabInstance info syn fc cs n ps t expn ds

12631263 = do i <- getIState

12641264 (n, ci) <- case lookupCtxtName n (idris_classes i) of

12651265 [c] -> return c

1266− _ -> fail $ show fc ++ ":" ++ show n ++ " is not a type class"

1266+ _ -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"

12671267 let constraint = PApp fc (PRef fc n) (map pexp ps)

12681268 let iname = case expn of

12691269 Nothing -> SN (InstanceN n (map show ps))

@@ -1467,9 +1467,9 @@ elabDecls info ds = do mapM_ (elabDecl EAll info) ds

14671467elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()

14681468elabDecl what info d

14691469 = idrisCatch (elabDecl' what info d)

1470− (\e -> do let msg = show e

1471− setErrLine (getErrLine msg)

1472− iputStrLn msg)

1470+ (\e -> do setErrLine (getErrLine e)

1471+ ist <- getIState

1472+ iputStrLn $ pshow ist e)

14731473

14741474elabDecl' _ info (PFix _ _ _)

14751475 = return () -- nothing to elaborate

src/Idris/Error.hs+22−29

@@ -13,6 +13,7 @@ import Core.Constraints

1313import System.Console.Haskeline

1414import System.Console.Haskeline.MonadException

1515import Control.Monad.State

16+import Control.Monad.Error (throwError, catchError)

1617import System.IO.Error(isUserError, ioeGetErrorString)

1718import Data.Char

1819import Data.Typeable

@@ -21,42 +22,36 @@ iucheck :: Idris ()

2122iucheck = do tit <- typeInType

2223 when (not tit) $

2324 do ist <- getIState

24− idrisCatch (tclift $ ucheck (idris_constraints ist))

25− (\e -> do let msg = show e

26− setErrLine (getErrLine msg)

27− iputStrLn msg)

25+ (tclift $ ucheck (idris_constraints ist)) `idrisCatch`

26+ (\e -> do setErrLine (getErrLine e)

27+ iputStrLn (pshow ist e))

28+

29+showErr :: Err -> Idris String

30+showErr e = getIState >>= return . flip pshow e

31+

2832

2933report :: IOError -> String

3034report e

3135 | isUserError e = ioeGetErrorString e

3236 | otherwise = show e

3337

34−idrisCatch :: Idris a -> (SomeException -> Idris a) -> Idris a

35−idrisCatch = catch

38+--idrisCatch :: Idris a -> (SomeException -> Idris a) -> Idris a

39+--idrisCatch = catch

3640

37−data IdrisErr = IErr String

38− deriving Typeable

41+idrisCatch :: Idris a -> (Err -> Idris a) -> Idris a

42+idrisCatch = catchError

3943

40−instance Show IdrisErr where

41− show (IErr s) = s

4244

43−instance Exception IdrisErr

44−

45−ifail :: String -> Idris ()

46−ifail str = throwIO (IErr str)

45+ifail :: String -> Idris a

46+ifail = throwError . Msg

4747

4848ierror :: Err -> Idris a

49−ierror err = do i <- getIState

50− throwIO (IErr $ pshow i err)

49+ierror = throwError

5150

5251tclift :: TC a -> Idris a

53−tclift tc = case tc of

54− OK v -> return v

55− Error err -> do i <- getIState

56− case err of

57− At (FC f l) e -> setErrLine l

58− _ -> return ()

59− throwIO (IErr $ pshow i err)

52+tclift (OK v) = return v

53+tclift (Error err@(At (FC f l) e)) = do setErrLine l ; throwError err

54+tclift (Error err) = throwError err

6055

6156tctry :: TC a -> TC a -> Idris a

6257tctry tc1 tc2

@@ -64,10 +59,8 @@ tctry tc1 tc2

6459 OK v -> return v

6560 Error err -> tclift tc2

6661

67−getErrLine str

68− = case span (/=':') str of

69− (_, ':':rest) -> case span isDigit rest of

70− ([], _) -> 0

71− (num, _) -> read num

72− _ -> 0

62+getErrLine :: Err -> Int

63+getErrLine (At (FC _ l) _) = l

64+getErrLine _ = 0

65+

7366

src/Idris/IBC.hs+15−14

@@ -70,7 +70,7 @@ writeIBC src f

7070 = do iLOG $ "Writing ibc " ++ show f

7171 i <- getIState

7272 case idris_metavars i \\ primDefs of

73− (_:_) -> fail "Can't write ibc when there are unsolved metavariables"

73+ (_:_) -> ifail "Can't write ibc when there are unsolved metavariables"

7474 [] -> return ()

7575 ibcf <- mkIBC (ibc_write i) (initIBC { sourcefile = src })

7676 idrisCatch (do liftIO $ createDirectoryIfMissing True (dropFileName f)

@@ -86,31 +86,32 @@ mkIBC (i:is) f = do ist <- getIState

8686 f' <- ibc ist i f

8787 mkIBC is f'

8888

89+ibc :: IState -> IBCWrite -> IBCFile -> Idris IBCFile

8990ibc i (IBCFix d) f = return f { ibc_fixes = d : ibc_fixes f }

9091ibc i (IBCImp n) f = case lookupCtxt n (idris_implicits i) of

9192 [v] -> return f { ibc_implicits = (n,v): ibc_implicits f }

92− _ -> fail "IBC write failed"

93+ _ -> ifail "IBC write failed"

9394ibc i (IBCStatic n) f

9495 = case lookupCtxt n (idris_statics i) of

9596 [v] -> return f { ibc_statics = (n,v): ibc_statics f }

96− _ -> fail "IBC write failed"

97+ _ -> ifail "IBC write failed"

9798ibc i (IBCClass n) f

9899 = case lookupCtxt n (idris_classes i) of

99100 [v] -> return f { ibc_classes = (n,v): ibc_classes f }

100− _ -> fail "IBC write failed"

101+ _ -> ifail "IBC write failed"

101102ibc i (IBCInstance int n ins) f

102103 = return f { ibc_instances = (int,n,ins): ibc_instances f }

103104ibc i (IBCDSL n) f

104105 = case lookupCtxt n (idris_dsls i) of

105106 [v] -> return f { ibc_dsls = (n,v): ibc_dsls f }

106− _ -> fail "IBC write failed"

107+ _ -> ifail "IBC write failed"

107108ibc i (IBCData n) f

108109 = case lookupCtxt n (idris_datatypes i) of

109110 [v] -> return f { ibc_datatypes = (n,v): ibc_datatypes f }

110− _ -> fail "IBC write failed"

111+ _ -> ifail "IBC write failed"

111112ibc i (IBCOpt n) f = case lookupCtxt n (idris_optimisation i) of

112113 [v] -> return f { ibc_optimise = (n,v): ibc_optimise f }

113− _ -> fail "IBC write failed"

114+ _ -> ifail "IBC write failed"

114115ibc i (IBCSyntax n) f = return f { ibc_syntax = n : ibc_syntax f }

115116ibc i (IBCKeyword n) f = return f { ibc_keywords = n : ibc_keywords f }

116117ibc i (IBCImport n) f = return f { ibc_imports = n : ibc_imports f }

@@ -121,13 +122,13 @@ ibc i (IBCDyLib n) f = return f {ibc_dynamic_libs = n : ibc_dynamic_libs f }

121122ibc i (IBCHeader tgt n) f = return f { ibc_hdrs = (tgt, n) : ibc_hdrs f }

122123ibc i (IBCDef n) f = case lookupDef n (tt_ctxt i) of

123124 [v] -> return f { ibc_defs = (n,v) : ibc_defs f }

124− _ -> fail "IBC write failed"

125+ _ -> ifail "IBC write failed"

125126ibc i (IBCDoc n) f = case lookupCtxt n (idris_docstrings i) of

126127 [v] -> return f { ibc_docstrings = (n,v) : ibc_docstrings f }

127− _ -> fail "IBC write failed"

128+ _ -> ifail "IBC write failed"

128129ibc i (IBCCG n) f = case lookupCtxt n (idris_callgraph i) of

129130 [v] -> return f { ibc_cg = (n,v) : ibc_cg f }

130− _ -> fail "IBC write failed"

131+ _ -> ifail "IBC write failed"

131132ibc i (IBCCoercion n) f = return f { ibc_coercions = n : ibc_coercions f }

132133ibc i (IBCAccess n a) f = return f { ibc_access = (n,a) : ibc_access f }

133134ibc i (IBCFlags n a) f = return f { ibc_flags = (n,a) : ibc_flags f }

@@ -137,7 +138,7 @@ ibc i (IBCTrans t) f = return f { ibc_transforms = t : ibc_transforms f }

137138process :: IBCFile -> FilePath -> Idris ()

138139process i fn

139140 | ver i /= ibcVersion = do iLOG "ibc out of date"

140− fail "Incorrect ibc version --- please rebuild"

141+ ifail "Incorrect ibc version --- please rebuild"

141142 | otherwise =

142143 do srcok <- liftIO $ doesFileExist (sourcefile i)

143144 when srcok $ liftIO $ timestampOlder (sourcefile i) fn

@@ -186,9 +187,9 @@ pImports fs

186187 else do putIState (i { imported = f : imported i })

187188 case fp of

188189 LIDR fn -> do iLOG $ "Failed at " ++ fn

189− fail "Must be an ibc"

190+ ifail "Must be an ibc"

190191 IDR fn -> do iLOG $ "Failed at " ++ fn

191− fail "Must be an ibc"

192+ ifail "Must be an ibc"

192193 IBC fn src -> loadIBC fn)

193194 fs

194195

@@ -272,7 +273,7 @@ pDyLibs ls = do res <- mapM (addDyLib . return) ls

272273 mapM_ checkLoad res

273274 return ()

274275 where checkLoad (Left _) = return ()

275− checkLoad (Right err) = fail err

276+ checkLoad (Right err) = ifail err

276277

277278pHdrs :: [(Codegen, String)] -> Idris ()

278279pHdrs hs = mapM_ (uncurry addHdr) hs

src/Idris/Parser.hs+5−4

@@ -941,8 +941,9 @@ loadModule f

941941 LIDR sfn -> loadSource True sfn)

942942 let (dir, fh) = splitFileName file

943943 return (dropExtension fh))

944− (\e -> do let msg = show e

945− setErrLine (getErrLine msg)

944+ (\e -> do setErrLine (getErrLine e)

945+ ist <- getIState

946+ msg <- showErr e

946947 iputStrLn msg

947948 return "")

948949

@@ -964,8 +965,8 @@ loadFromIFile (LIDR fn) = loadSource' True fn

964965loadSource' :: Bool -> FilePath -> Idris ()

965966loadSource' lidr r

966967 = idrisCatch (loadSource lidr r)

967− (\e -> do let msg = show e

968− setErrLine (getErrLine msg)

968+ (\e -> do setErrLine (getErrLine e)

969+ msg <- showErr e

969970 iputStrLn msg)

970971

971972{- | Load Idris source code-}

src/Idris/Prover.hs+12−13

@@ -32,7 +32,7 @@ prover lit x =

3232 case lookupTy x ctxt of

3333 [t] -> if elem x (idris_metavars i)

3434 then prove ctxt lit x t

35− else fail $ show x ++ " is not a metavariable"

35+ else ifail $ show x ++ " is not a metavariable"

3636 _ -> fail "No such metavariable"

3737

3838showProof :: Bool -> Name -> [String] -> String

@@ -84,8 +84,7 @@ prove ctxt lit n ty

8484elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])

8585elabStep st e = do case runStateT e st of

8686 OK (a, st') -> return (a, st')

87− Error a -> do i <- getIState

88− fail (pshow i a)

87+ Error a -> ierror a

8988

9089dumpState :: IState -> ProofState -> Idris ()

9190dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _) =

@@ -168,33 +167,33 @@ ploop d prompt prf e h

168167 i <- receiveInput e

169168 return (i, h)

170169 (cmd, step) <- case x of

171− Nothing -> do iFail ""; fail "Abandoned"

170+ Nothing -> do iPrintError ""; fail "Abandoned"

172171 Just input -> do return (parseTactic i input, input)

173172 case cmd of

174− Success Abandon -> do iFail ""; fail "Abandoned"

173+ Success Abandon -> do iPrintError ""; fail "Abandoned"

175174 _ -> return ()

176175 (d, st, done, prf') <- idrisCatch

177176 (case cmd of

178− Failure err -> do iFail (show err)

177+ Failure err -> do iPrintError (show err)

179178 return (False, e, False, prf)

180179 Success Undo -> do (_, st) <- elabStep e loadState

181− iResult ""

180+ iPrintResult ""

182181 return (True, st, False, init prf)

183− Success ProofState -> do iResult ""

182+ Success ProofState -> do iPrintResult ""

184183 return (True, e, False, prf)

185184 Success ProofTerm -> do tm <- lifte e get_term

186− iResult $ "TT: " ++ show tm ++ "\n"

185+ iPrintResult $ "TT: " ++ show tm ++ "\n"

187186 return (False, e, False, prf)

188187 Success Qed -> do hs <- lifte e get_holes

189− when (not (null hs)) $ fail "Incomplete proof"

190− iResult "Proof completed!"

188+ when (not (null hs)) $ ifail "Incomplete proof"

189+ iPrintResult "Proof completed!"

191190 return (False, e, True, prf)

192191 Success tac -> do (_, e) <- elabStep e saveState

193192 (_, st) <- elabStep e (runTac True i tac)

194193-- trace (show (problems (proof st))) $

195− iResult ""

194+ iPrintResult ""

196195 return (True, st, False, prf ++ [step]))

197− (\err -> do iFail (show err)

196+ (\err -> do iPrintError (show err)

198197 return (False, e, False, prf))

199198 ideslavePutSExp "write-proof-state" (prf', length prf')

200199 if done then do (tm, _) <- elabStep st get_term

src/Idris/Providers.hs+3−3

@@ -19,9 +19,9 @@ getProvided tm | (P _ (UN "prim_io_return") _, [tp, result]) <- unApply tm

1919 , (P _ (NS (UN "Error") ["Providers"]) _, [_, err]) <- unApply result =

2020 case err of

2121 Constant (Str msg) -> ierror . ProviderError $ msg

22− _ -> fail "Internal error in type provider, non-normalised error"

22+ _ -> ifail "Internal error in type provider, non-normalised error"

2323 | (P _ (UN "prim_io_return") _, [tp, result]) <- unApply tm

2424 , (P _ (NS (UN "Provide") ["Providers"]) _, [_, res]) <- unApply result =

2525 return res

26− | otherwise = fail $ "Internal type provider error: result was not " ++

27− "IO (Provider a), or perhaps missing normalisation."

26+ | otherwise = ifail $ "Internal type provider error: result was not " ++

27+ "IO (Provider a), or perhaps missing normalisation."

src/Idris/REPL.hs+71−66

@@ -56,6 +56,7 @@ import System.Process

5656import System.Directory

5757import System.IO

5858import Control.Monad

59+import Control.Monad.Trans.Error (ErrorT(..))

5960import Control.Monad.Trans.State.Strict ( StateT, execStateT, get, put )

6061import Control.Monad.Trans ( liftIO, lift )

6162import Data.Maybe

@@ -121,15 +122,15 @@ ideslave orig mods

121122 _ -> ""

122123 c <- colourise

123124 case parseCmd i "(input)" cmd of

124− Failure err -> iFail $ show (fixColour c err)

125− Success (Prove n') -> do iResult ""

125+ Failure err -> iPrintError $ show (fixColour c err)

126+ Success (Prove n') -> do iPrintResult ""

126127 idrisCatch

127128 (do process fn (Prove n'))

128− (\e -> do iFail $ show e)

129+ (\e -> do iPrintError $ show e)

129130 isetPrompt (mkPrompt mods)

130131 Success cmd -> idrisCatch

131132 (do ideslaveProcess fn cmd)

132− (\e -> do iFail $ show e)

133+ (\e -> do iPrintError $ show e)

133134 Just (REPLCompletions str) ->

134135 do (unused, compls) <- replCompletion (reverse str, "")

135136 let good = SexpList [SymbolAtom "ok", toSExp (map replacement compls, reverse unused)]

@@ -145,17 +146,17 @@ ideslave orig mods

145146 -- Report either success or failure

146147 i <- getIState

147148 case (errLine i) of

148− Nothing -> iResult $ "loaded " ++ filename

149− Just x -> iFail $ "didn't load " ++ filename

149+ Nothing -> iPrintResult $ "loaded " ++ filename

150+ Just x -> iPrintError $ "didn't load " ++ filename

150151 ideslave orig [filename]

151− Nothing -> do iFail "did not understand")

152− (\e -> do iFail $ show e)

152+ Nothing -> do iPrintError "did not understand")

153+ (\e -> do iPrintError $ show e)

153154 ideslave orig mods

154155

155156ideslaveProcess :: FilePath -> Command -> Idris ()

156157ideslaveProcess fn Help = process fn Help

157158ideslaveProcess fn (ChangeDirectory f) = do process fn (ChangeDirectory f)

158− iResult "changed directory to"

159+ iPrintResult "changed directory to"

159160ideslaveProcess fn (Eval t) = process fn (Eval t)

160161ideslaveProcess fn (ExecVal t) = process fn (ExecVal t)

161162ideslaveProcess fn (Check (PRef x n)) = process fn (Check (PRef x n))

@@ -163,10 +164,10 @@ ideslaveProcess fn (Check t) = process fn (Check t)

163164ideslaveProcess fn (DocStr n) = process fn (DocStr n)

164165ideslaveProcess fn Universes = process fn Universes

165166ideslaveProcess fn (Defn n) = do process fn (Defn n)

166− iResult ""

167+ iPrintResult ""

167168ideslaveProcess fn (TotCheck n) = process fn (TotCheck n)

168169ideslaveProcess fn (DebugInfo n) = do process fn (DebugInfo n)

169− iResult ""

170+ iPrintResult ""

170171ideslaveProcess fn (Info n) = process fn (Info n)

171172ideslaveProcess fn (Search t) = process fn (Search t)

172173ideslaveProcess fn (Spec t) = process fn (Spec t)

@@ -178,29 +179,29 @@ ideslaveProcess fn (HNF t) = process fn (HNF t)

178179--that most likely does not work, since we need to wrap

179180--input/output of the executed binary...

180181ideslaveProcess fn Execute = do process fn Execute

181− iResult ""

182+ iPrintResult ""

182183ideslaveProcess fn (Compile codegen f) = do process fn (Compile codegen f)

183− iResult ""

184+ iPrintResult ""

184185ideslaveProcess fn (LogLvl i) = do process fn (LogLvl i)

185− iResult ""

186+ iPrintResult ""

186187ideslaveProcess fn (Pattelab t) = process fn (Pattelab t)

187188ideslaveProcess fn (Missing n) = process fn (Missing n)

188189ideslaveProcess fn (DynamicLink l) = do process fn (DynamicLink l)

189− iResult ""

190+ iPrintResult ""

190191ideslaveProcess fn ListDynamic = do process fn ListDynamic

191− iResult ""

192+ iPrintResult ""

192193ideslaveProcess fn Metavars = process fn Metavars

193194ideslaveProcess fn (SetOpt ErrContext) = do process fn (SetOpt ErrContext)

194− iResult ""

195+ iPrintResult ""

195196ideslaveProcess fn (UnsetOpt ErrContext) = do process fn (UnsetOpt ErrContext)

196− iResult ""

197+ iPrintResult ""

197198ideslaveProcess fn (SetOpt ShowImpl) = do process fn (SetOpt ShowImpl)

198− iResult ""

199+ iPrintResult ""

199200ideslaveProcess fn (UnsetOpt ShowImpl) = do process fn (UnsetOpt ShowImpl)

200− iResult ""

201+ iPrintResult ""

201202ideslaveProcess fn (SetOpt x) = process fn (SetOpt x)

202203ideslaveProcess fn (UnsetOpt x) = process fn (UnsetOpt x)

203−ideslaveProcess fn _ = iFail "command not recognized or not supported"

204+ideslaveProcess fn _ = iPrintError "command not recognized or not supported"

204205

205206

206207-- | The prompt consists of the currently loaded modules, or "Idris" if there are none

@@ -250,7 +251,7 @@ processInput cmd orig inputs

250251 Success Quit -> do when (not quiet) (iputStrLn "Bye bye")

251252 return Nothing

252253 Success cmd -> do idrisCatch (process fn cmd)

253− (\e -> iputStrLn (show e))

254+ (\e -> do msg <- showErr e ; iputStrLn msg)

254255 return (Just inputs)

255256

256257resolveProof :: Name -> Idris Name

@@ -260,7 +261,7 @@ resolveProof n'

260261 n <- case lookupNames n' ctxt of

261262 [x] -> return x

262263 [] -> return n'

263− ns -> fail $ pshow i (CantResolveAlts (map show ns))

264+ ns -> ierror (CantResolveAlts (map show ns))

264265 return n

265266

266267removeProof :: Name -> Idris ()

@@ -308,7 +309,7 @@ insertScript prf (p@"---------- Proofs ----------" : "" : xs)

308309insertScript prf (x : xs) = x : insertScript prf xs

309310

310311process :: FilePath -> Command -> Idris ()

311−process fn Help = iResult displayHelp

312+process fn Help = iPrintResult displayHelp

312313process fn (ChangeDirectory f)

313314 = do liftIO $ setCurrentDirectory f

314315 return ()

@@ -324,7 +325,7 @@ process fn (Eval t)

324325 logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'

325326 imp <- impShow

326327 c <- colourise

327− iResult (showImp (Just ist) imp c (delab ist tm') ++ " : " ++

328+ iPrintResult (showImp (Just ist) imp c (delab ist tm') ++ " : " ++

328329 showImp (Just ist) imp c (delab ist ty'))

329330process fn (ExecVal t)

330331 = do ctxt <- getContext

@@ -335,7 +336,7 @@ process fn (ExecVal t)

335336 res <- execute tm

336337 imp <- impShow

337338 c <- colourise

338− iResult (showImp (Just ist) imp c (delab ist res) ++ " : " ++

339+ iPrintResult (showImp (Just ist) imp c (delab ist res) ++ " : " ++

339340 showImp (Just ist) imp c (delab ist ty'))

340341process fn (Check (PRef _ n))

341342 = do ctxt <- getContext

@@ -345,8 +346,8 @@ process fn (Check (PRef _ n))

345346 case lookupNames n ctxt of

346347 ts@(_:_) -> do mapM_ (\n -> iputStrLn $ showName (Just ist) [] False c n ++ " : " ++

347348 showImp (Just ist) imp c (delabTy ist n)) ts

348− iResult ""

349− [] -> iFail $ "No such variable " ++ show n

349+ iPrintResult ""

350+ [] -> iPrintError $ "No such variable " ++ show n

350351process fn (Check t)

351352 = do (tm, ty) <- elabVal toplevel False t

352353 ctxt <- getContext

@@ -355,15 +356,15 @@ process fn (Check t)

355356 c <- colourise

356357 let ty' = normaliseC ctxt [] ty

357358 case tm of

358− TType _ -> iResult ("Type : Type 1")

359− _ -> iResult (showImp (Just ist) imp c (delab ist tm) ++ " : " ++

360− showImp (Just ist) imp c (delab ist ty))

359+ TType _ -> iPrintResult ("Type : Type 1")

360+ _ -> iPrintResult (showImp (Just ist) imp c (delab ist tm) ++ " : " ++

361+ showImp (Just ist) imp c (delab ist ty))

361362

362363process fn (DocStr n) = do i <- getIState

363364 case lookupCtxtName n (idris_docstrings i) of

364− [] -> iFail $ "No documentation for " ++ show n

365+ [] -> iPrintError $ "No documentation for " ++ show n

365366 ns -> do mapM_ showDoc ns

366− iResult ""

367+ iPrintResult ""

367368 where showDoc (n, d)

368369 = do doc <- getDocs n

369370 iputStrLn $ show doc

@@ -374,8 +375,8 @@ process fn Universes = do i <- getIState

374375 let n = length cs

375376 iputStrLn $ "(" ++ show n ++ " constraints)"

376377 case ucheck cs of

377− Error e -> iFail $ pshow i e

378− OK _ -> iResult "Universes OK"

378+ Error e -> iPrintError $ pshow i e

379+ OK _ -> iPrintResult "Universes OK"

379380process fn (Defn n) = do i <- getIState

380381 iputStrLn "Compiled patterns:\n"

381382 iputStrLn $ show (lookupDef n (tt_ctxt i))

@@ -392,8 +393,8 @@ process fn (Defn n) = do i <- getIState

392393 showImp (Just i) True c (delab i rhs))

393394process fn (TotCheck n) = do i <- getIState

394395 case lookupTotal n (tt_ctxt i) of

395− [t] -> iResult (showTotal t i)

396− _ -> do iFail ""

396+ [t] -> iPrintResult (showTotal t i)

397+ _ -> do iPrintError ""

397398 return ()

398399process fn (DebugInfo n)

399400 = do i <- getIState

@@ -416,13 +417,13 @@ process fn (DebugInfo n)

416417process fn (Info n) = do i <- getIState

417418 case lookupCtxt n (idris_classes i) of

418419 [c] -> classInfo c

419− _ -> iFail "Not a class"

420−process fn (Search t) = iFail "Not implemented"

420+ _ -> iPrintError "Not a class"

421+process fn (Search t) = iPrintError "Not implemented"

421422process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t

422423 ctxt <- getContext

423424 ist <- getIState

424425 let tm' = simplify ctxt [] {- (idris_statics ist) -} tm

425− iResult (show (delab ist tm'))

426+ iPrintResult (show (delab ist tm'))

426427

427428process fn (RmProof n')

428429 = do i <- getIState

@@ -449,7 +450,7 @@ process fn' (AddProof prf)

449450 then return fn'

450451 else if exExt

451452 then return fnExt

452− else fail $ "Neither \""++fn'++"\" nor \""++fnExt++"\" exist"

453+ else ifail $ "Neither \""++fn'++"\" nor \""++fnExt++"\" exist"

453454 let fb = fn ++ "~"

454455 liftIO $ copyFile fn fb -- make a backup in case something goes wrong!

455456 prog <- liftIO $ readFile fb

@@ -457,7 +458,7 @@ process fn' (AddProof prf)

457458 let proofs = proof_list i

458459 n' <- case prf of

459460 Nothing -> case proofs of

460− [] -> fail "No proof to add"

461+ [] -> ifail "No proof to add"

461462 ((x, p) : _) -> return x

462463 Just nm -> return nm

463464 n <- resolveProof n'

@@ -474,8 +475,8 @@ process fn (ShowProof n')

474475 n <- resolveProof n'

475476 let proofs = proof_list i

476477 case lookup n proofs of

477− Nothing -> iFail "No proof to show"

478− Just p -> iResult $ showProof False n p

478+ Nothing -> iPrintError "No proof to show"

479+ Just p -> iPrintResult $ showProof False n p

479480

480481process fn (Prove n')

481482 = do ctxt <- getContext

@@ -483,7 +484,7 @@ process fn (Prove n')

483484 n <- case lookupNames n' ctxt of

484485 [x] -> return x

485486 [] -> return n'

486− ns -> fail $ pshow ist (CantResolveAlts (map show ns))

487+ ns -> ierror (CantResolveAlts (map show ns))

487488 prover (lit fn) n

488489 -- recheck totality

489490 i <- getIState

@@ -495,14 +496,14 @@ process fn (HNF t) = do (tm, ty) <- elabVal toplevel False t

495496 ctxt <- getContext

496497 ist <- getIState

497498 let tm' = hnf ctxt [] tm

498− iResult (show (delab ist tm'))

499+ iPrintResult (show (delab ist tm'))

499500process fn (TestInline t) = do (tm, ty) <- elabVal toplevel False t

500501 ctxt <- getContext

501502 ist <- getIState

502503 let tm' = inlineTerm ist tm

503504 imp <- impShow

504505 c <- colourise

505− iResult (showImp (Just ist) imp c (delab ist tm'))

506+ iPrintResult (showImp (Just ist) imp c (delab ist tm'))

506507process fn TTShell = do ist <- getIState

507508 let shst = initState (tt_ctxt ist)

508509 runShell shst

@@ -529,7 +530,7 @@ process fn (LogLvl i) = setLogLevel i

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

530531process fn (Pattelab t)

531532 = do (tm, ty) <- elabVal toplevel True t

532− iResult $ show tm ++ "\n\n : " ++ show ty

533+ iPrintResult $ show tm ++ "\n\n : " ++ show ty

533534

534535process fn (Missing n)

535536 = do i <- getIState

@@ -537,13 +538,13 @@ process fn (Missing n)

537538 case lookupCtxt n (idris_patdefs i) of

538539 [] -> return ()

539540 [(_, tms)] ->

540− iResult (showSep "\n" (map (showImp (Just i) True c) tms))

541− _ -> iFail $ "Ambiguous name"

541+ iPrintResult (showSep "\n" (map (showImp (Just i) True c) tms))

542+ _ -> iPrintError $ "Ambiguous name"

542543process fn (DynamicLink l) = do i <- getIState

543544 let lib = trim l

544− handle <- lift $ tryLoadLib lib

545+ handle <- lift . lift $ tryLoadLib lib

545546 case handle of

546− Nothing -> iFail $ "Could not load dynamic lib \"" ++ l ++ "\""

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

547548 Just x -> do let libs = idris_dynamic_libs i

548549 if x `elem` libs

549550 then do iLOG ("Tried to load duplicate library " ++ lib_name x)

@@ -559,8 +560,8 @@ process fn Metavars

559560 = do ist <- getIState

560561 let mvs = idris_metavars ist \\ primDefs

561562 case mvs of

562− [] -> iFail "No global metavariables to solve"

563− _ -> iResult $ "Global metavariables:\n\t" ++ show mvs

563+ [] -> iPrintError "No global metavariables to solve"

564+ _ -> iPrintResult $ "Global metavariables:\n\t" ++ show mvs

564565process fn NOP = return ()

565566

566567process fn (SetOpt ErrContext) = setErrContext True

@@ -568,8 +569,8 @@ process fn (UnsetOpt ErrContext) = setErrContext False

568569process fn (SetOpt ShowImpl) = setImpShow True

569570process fn (UnsetOpt ShowImpl) = setImpShow False

570571

571−process fn (SetOpt _) = iFail "Not a valid option"

572−process fn (UnsetOpt _) = iFail "Not a valid option"

572+process fn (SetOpt _) = iPrintError "Not a valid option"

573+process fn (UnsetOpt _) = iPrintError "Not a valid option"

573574process fn (SetColour ty c) = setColour ty c

574575process fn ColourOn = do ist <- getIState

575576 putIState $ ist { idris_colourRepl = True }

@@ -583,7 +584,7 @@ classInfo ci = do iputStrLn "Methods:\n"

583584 iputStrLn ""

584585 iputStrLn "Instances:\n"

585586 mapM_ dumpInstance (class_instances ci)

586− iResult ""

587+ iPrintResult ""

587588

588589dumpMethod :: (Name, (FnOpts, PTerm)) -> Idris ()

589590dumpMethod (n, (_, t)) = iputStrLn $ show n ++ " : " ++ show t

@@ -686,8 +687,12 @@ replSettings hFile = setComplete replCompletion $ defaultSettings {

686687 }

687688

688689-- invoke as if from command line

689−idris :: [Opt] -> IO IState

690−idris opts = execStateT (idrisMain opts) idrisInit

690+idris :: [Opt] -> IO ()

691+idris opts = do res <- runErrorT $ execStateT (idrisMain opts) idrisInit

692+ case res of

693+ Left err -> putStrLn $ pshow idrisInit err

694+ Right ist -> return ()

695+

691696

692697loadInputs :: [FilePath] -> Idris ()

693698loadInputs inputs

@@ -886,9 +891,9 @@ initScript = do script <- getInitScript

886891 h <- liftIO $ openFile script ReadMode

887892 runInit h

888893 liftIO $ hClose h)

889− (\e -> iFail $ "Error reading init file: " ++ show e)

894+ (\e -> iPrintError $ "Error reading init file: " ++ show e)

890895 where runInit :: Handle -> Idris ()

891− runInit h = do eof <- lift (hIsEOF h)

896+ runInit h = do eof <- lift . lift $ hIsEOF h

892897 ist <- getIState

893898 unless eof $ do

894899 line <- liftIO $ hGetLine h

@@ -899,12 +904,12 @@ initScript = do script <- getInitScript

899904 processLine i cmd input clr =

900905 case parseCmd i input cmd of

901906 Failure err -> liftIO $ print (fixColour clr err)

902− Success Reload -> iFail "Init scripts cannot reload the file"

903− Success (Load f) -> iFail "Init scripts cannot load files"

904− Success (ModImport f) -> iFail "Init scripts cannot import modules"

905− Success Edit -> iFail "Init scripts cannot invoke the editor"

907+ Success Reload -> iPrintError "Init scripts cannot reload the file"

908+ Success (Load f) -> iPrintError "Init scripts cannot load files"

909+ Success (ModImport f) -> iPrintError "Init scripts cannot import modules"

910+ Success Edit -> iPrintError "Init scripts cannot invoke the editor"

906911 Success Proofs -> proofs i

907− Success Quit -> iFail "Init scripts cannot quit Idris"

912+ Success Quit -> iPrintError "Init scripts cannot quit Idris"

908913 Success cmd -> process [] cmd

909914

910915getFile :: Opt -> Maybe String

src/Idris/Unlit.hs+3

@@ -10,17 +10,20 @@ unlit f s = do let s' = map ulLine (lines s)

1010

1111data LineType = Prog | Blank | Comm

1212

13+ulLine :: String -> (LineType, String)

1314ulLine ('>':' ':xs) = (Prog, xs)

1415ulLine ('>':xs) = (Prog, xs)

1516ulLine xs | all isSpace xs = (Blank, "")

1617-- make sure it's not a doc comment

1718 | otherwise = (Comm, '-':'-':' ':'>':xs)

1819

20+check :: FilePath -> Int -> [(LineType, String)] -> TC ()

1921check f l (a:b:cs) = do chkAdj f l (fst a) (fst b)

2022 check f (l+1) (b:cs)

2123check f l [x] = return ()

2224check f l [] = return ()

2325

26+chkAdj :: FilePath -> Int -> LineType -> LineType -> TC ()

2427chkAdj f l Prog Comm = tfail $ At (FC f l) ProgramLineComment

2528chkAdj f l Comm Prog = tfail $ At (FC f l) ProgramLineComment

2629chkAdj f l _ _ = return ()

src/Main.hs+2−1

@@ -8,6 +8,7 @@ import System.FilePath ((</>), addTrailingPathSeparator)

99import Data.Maybe

1010import Data.Version

11+import Control.Monad.Trans.Error ( ErrorT(..) )

1112import Control.Monad.Trans.State.Strict ( execStateT, get, put )

1213import Control.Monad.Trans ( liftIO )

1314import Control.Monad ( when )

@@ -40,7 +41,7 @@ import Paths_idris

4041

4142main = do xs <- getArgs

4243 let opts = parseArgs xs

43− execStateT (runIdris opts) idrisInit

44+ runErrorT $ execStateT (runIdris opts) idrisInit

4445

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

4647runIdris opts = do

src/Pkg/Package.hs+1−1

@@ -70,7 +70,7 @@ installPkg pkgdesc

7070buildMods :: [Opt] -> [Name] -> IO ()

7171buildMods opts ns = do let f = map (toPath . show) ns

7272-- putStrLn $ "MODULE: " ++ show f

73− idris (map Filename f ++ opts)

73+ idris (map Filename f ++ opts)

7474 return ()

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

7676