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

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #539 from david-christiansen/errort

92923b7Edwin Brady13 years ago

src/Core/Execute.hs+2−2

compare with master

unifiedsplit

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

159execute :: Term -> Idris Term

160execute tm = do est <- initState

161 ctxt <- getContext

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

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

163− toTT res

163+ toTT res

164 case res of

165 Left err -> fail err

166 Right tm' -> return tm'

src/Core/TT.hs+4

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

21module Core.TT where

23import Control.Monad.State

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

24import Debug.Trace

25import Debug.Trace

25import qualified Data.Map as Map

26import qualified Data.Map as Map

26import Data.Char

27import Data.Char

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

133 pretty (ProviderError msg) = text msg

134 pretty (ProviderError msg) = text msg

134 pretty _ = text "Error"

135 pretty _ = text "Error"

135

136

137+instance Error Err where

138+ strMsg = Msg

139+

136data TC a = OK a

140data TC a = OK a

137 | Error Err

141 | Error Err

138 deriving (Eq, Functor)

142 deriving (Eq, Functor)

src/IRTS/Compiler.hs+7−6

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

20import Idris.AbsSyntax

21import Idris.UnusedArgs

22+import Idris.Error

23import Core.TT

24import Core.TT

24import Core.Evaluate

25import Core.Evaluate

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

91 ViaLLVM -> codegenLLVM c triple cpu optimize f outty

92 ViaLLVM -> codegenLLVM c triple cpu optimize f outty

93 Bytecode -> dumpBC c f

94 Bytecode -> dumpBC c f

94− Error e -> fail $ show e

95+ Error e -> ierror e

95 where checkMVs = do i <- getIState

96 where checkMVs = do i <- getIState

96 case idris_metavars i \\ primDefs of

97 case idris_metavars i \\ primDefs of

97 [] -> return ()

98 [] -> return ()

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

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

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

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

100 ex <- doesFileExist f

101 ex <- doesFileExist f

101 if ex then return f else return h

102 if ex then return f else return h

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

249-- = return $ LConst (BI 0)

250-- = return $ LConst (BI 0)

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

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

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

252 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

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

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

254 = do let n' = uniqueName n env

255 = do let n' = uniqueName n env

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

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

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

286 = let maybeTys = getFTypes fgnArgTys

287 = let maybeTys = getFTypes fgnArgTys

287 rty = mkIty' ret in

288 rty = mkIty' ret in

288 case maybeTys of

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

290 Just tys -> do

291 Just tys -> do

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

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

292 -- wrap it in a prim__IO

293 -- wrap it in a prim__IO

293 -- return $ con_ 0 @@ impossible @@

294 -- return $ con_ 0 @@ impossible @@

294 return $ -- LLazyExp $

295 return $ -- LLazyExp $

295 LForeign LANG_C rty fgnName (zip tys args')

296 LForeign LANG_C rty fgnName (zip tys args')

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

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

297

298

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

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

299getFTypes tm = case unApply tm of

300getFTypes tm = case unApply tm of

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

386 LConst (BI 1)]) rhs')

387 LConst (BI 1)]) rhs')

387-- return $ LSucCase n rhs'

388-- return $ LSucCase n rhs'

388 mkIRAlt _ (ConstCase c rhs)

389 mkIRAlt _ (ConstCase c rhs)

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

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

390 mkIRAlt _ (DefaultCase rhs)

391 mkIRAlt _ (DefaultCase rhs)

391 = do rhs' <- ir rhs

392 = do rhs' <- ir rhs

392 return $ LDefaultCase rhs'

393 return $ LDefaultCase rhs'

src/IRTS/LParser.hs+4−3

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

24import Debug.Trace

25import Data.Maybe

26import System.FilePath

27+import Idris.Error

28type TokenParser a = PTok.TokenParser a

29type TokenParser a = PTok.TokenParser a

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

62 OK c -> case cgn of

63 OK c -> case cgn of

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

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

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

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

65− Error e -> fail $ show e

66+ Error e -> fail (show e)

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

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

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

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

69 fp <- readFile fname

70 fp <- readFile fname

70 case runParser pProgram () fname fp of

71 case runParser pProgram () fname fp of

71− Left err-> fail (show err)

72+ Left err -> fail (show err)

72− Right x -> return x

73+ Right x -> return x

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

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

75pProgram = do fs <- many1 pLDecl

76pProgram = do fs <- many1 pLDecl

src/Idris/AbsSyntax.hs+20−20

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

60 case mapMaybe (findDyLib ls) libs of

61 x:_ -> return (Left x)

62 [] -> do

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

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

64 case msum handle of

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

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

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

277solveDeferred n = do i <- getIState

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

279

280−iResult :: String -> Idris ()

280+iPrintResult :: String -> Idris ()

281−iResult s = do i <- getIState

281+iPrintResult s = do i <- getIState

282− case idris_outputmode i of

282+ case idris_outputmode i of

283− RawOutput -> case s of

283+ RawOutput -> case s of

284− "" -> return ()

284+ "" -> return ()

285− s -> liftIO $ putStrLn s

285+ s -> liftIO $ putStrLn s

286− IdeSlave n ->

286+ IdeSlave n ->

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

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

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

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

289−

289+

290−iFail :: String -> Idris ()

290+iPrintError :: String -> Idris ()

291−iFail s = do i <- getIState

291+iPrintError s = do i <- getIState

292− case idris_outputmode i of

292+ case idris_outputmode i of

293− RawOutput -> case s of

293+ RawOutput -> case s of

294− "" -> return ()

294+ "" -> return ()

295− s -> liftIO $ putStrLn s

295+ s -> liftIO $ putStrLn s

296− IdeSlave n ->

296+ IdeSlave n ->

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

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

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

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

299

300iputStrLn :: String -> Idris ()

301iputStrLn s = do i <- getIState

src/Idris/AbsSyntaxTree.hs+2−1

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

22import Control.Monad.Trans.State.Strict

23+import Control.Monad.Trans.Error

24import Data.List

25import Data.List

25import Data.Char

26import Data.Char

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

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

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

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

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

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

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

190−type Idris = StateT IState IO

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

191

192

192-- Commands in the REPL

193-- Commands in the REPL

193

194

src/Idris/ElabDecls.hs+19−19

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

289 = do i <- getIState

290 -- Ensure that the experimental extension is enabled

291 unless (TypeProviders `elem` idris_language_extensions i) $

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

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

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

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

294

295 ctxt <- getContext

296

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

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

299 unless (isTType typ) $

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

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

301

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

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

304 unless (isProviderOf ty' et) $

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

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

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

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

307

308 -- Create the top-level type declaration

309 elabType info syn "" fc [] n ty

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

376 i <- getIState

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

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

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

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

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

381 [imps] -> return imps

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

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

784 = do let tcgen = Dictionary `elem` opts

785 b <- checkPossible info fc tcgen fname lhs_in

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

788 False -> do ptm <- mkPatTm lhs_in

789 return (Left ptm)

790elabClause 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)

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

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

1044 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

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

1047

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

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

1052 showImp Nothing True False toplhs)

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

1055 Right mvars ->

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

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

1063 showImp Nothing True False toplhs)

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

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

1067 Right mvars ->

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

1069 return $ PWith fc wname lhs ws wval withs'

1070 mkAux wname toplhs ns ns' c

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

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

1072

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

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

1077 PApp fc (PRef fc' wname)

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

1079 updateLHS n wname mvars ns ns' tm w

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

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

1081

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

1083 | otherwise = Placeholder

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

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

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

1163 (n, (syn, o, t) ) )

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

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

1165

1166 -- Create default definitions

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

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

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

1173 iLOG (show ds)

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

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

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

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

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

1177

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

1179 defaultdec (NS n ns) = NS (defaultdec n) ns

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

1263 = do i <- getIState

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

1265 [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"

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

1268 let iname = case expn of

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

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

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

1468elabDecl what info d

1469 = idrisCatch (elabDecl' what info d)

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

1471− setErrLine (getErrLine msg)

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

1471+ ist <- getIState

1472− iputStrLn msg)

1472+ iputStrLn $ pshow ist e)

1473

1474elabDecl' _ info (PFix _ _ _)

1475 = return () -- nothing to elaborate

src/Idris/Error.hs+22−29

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

13import System.Console.Haskeline

14import System.Console.Haskeline.MonadException

15import Control.Monad.State

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

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

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

17import Data.Char

18import Data.Char

18import Data.Typeable

19import Data.Typeable

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

21iucheck = do tit <- typeInType

22iucheck = do tit <- typeInType

22 when (not tit) $

23 when (not tit) $

23 do ist <- getIState

24 do ist <- getIState

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

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

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

26− setErrLine (getErrLine msg)

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

27− iputStrLn msg)

27+ iputStrLn (pshow ist e))

28+

29+showErr :: Err -> Idris String

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

31+

29report :: IOError -> String

33report :: IOError -> String

30report e

34report e

31 | isUserError e = ioeGetErrorString e

35 | isUserError e = ioeGetErrorString e

32 | otherwise = show e

36 | otherwise = show e

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

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

35−idrisCatch = catch

39+--idrisCatch = catch

37−data IdrisErr = IErr String

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

38− deriving Typeable

42+idrisCatch = catchError

40−instance Show IdrisErr where

41− show (IErr s) = s

43−instance Exception IdrisErr

44−

45−ifail :: String -> Idris ()

45+ifail :: String -> Idris a

46−ifail str = throwIO (IErr str)

46+ifail = throwError . Msg

48ierror :: Err -> Idris a

49−ierror err = do i <- getIState

49+ierror = throwError

50− throwIO (IErr $ pshow i err)

52tclift :: TC a -> Idris a

51tclift :: TC a -> Idris a

53−tclift tc = case tc of

54− OK v -> return v

52+tclift (OK v) = return v

55− Error err -> do i <- getIState

56− case err of

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

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

58− _ -> return ()

54+tclift (Error err) = throwError err

59− throwIO (IErr $ pshow i err)

61tctry :: TC a -> TC a -> Idris a

56tctry :: TC a -> TC a -> Idris a

62tctry tc1 tc2

57tctry tc1 tc2

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

64 OK v -> return v

59 OK v -> return v

65 Error err -> tclift tc2

60 Error err -> tclift tc2

67−getErrLine str

62+getErrLine :: Err -> Int

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

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

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

64+getErrLine _ = 0

70− ([], _) -> 0

65+

71− (num, _) -> read num

72− _ -> 0

src/Idris/IBC.hs+15−14

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

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

71 i <- getIState

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

74 [] -> return ()

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

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

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

86 f' <- ibc ist i f

87 mkIBC is f'

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

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

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

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

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

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

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

92− _ -> fail "IBC write failed"

93+ _ -> ifail "IBC write failed"

93ibc i (IBCStatic n) f

94ibc i (IBCStatic n) f

94 = case lookupCtxt n (idris_statics i) of

95 = case lookupCtxt n (idris_statics i) of

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

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

96− _ -> fail "IBC write failed"

97+ _ -> ifail "IBC write failed"

97ibc i (IBCClass n) f

98ibc i (IBCClass n) f

98 = case lookupCtxt n (idris_classes i) of

99 = case lookupCtxt n (idris_classes i) of

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

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

100− _ -> fail "IBC write failed"

101+ _ -> ifail "IBC write failed"

101ibc i (IBCInstance int n ins) f

102ibc i (IBCInstance int n ins) f

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

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

103ibc i (IBCDSL n) f

104ibc i (IBCDSL n) f

104 = case lookupCtxt n (idris_dsls i) of

105 = case lookupCtxt n (idris_dsls i) of

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

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

106− _ -> fail "IBC write failed"

107+ _ -> ifail "IBC write failed"

107ibc i (IBCData n) f

108ibc i (IBCData n) f

108 = case lookupCtxt n (idris_datatypes i) of

109 = case lookupCtxt n (idris_datatypes i) of

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

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

110− _ -> fail "IBC write failed"

111+ _ -> ifail "IBC write failed"

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

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

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

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

113− _ -> fail "IBC write failed"

114+ _ -> ifail "IBC write failed"

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

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

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

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

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

117ibc 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 }

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

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

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

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

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

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

124− _ -> fail "IBC write failed"

125+ _ -> ifail "IBC write failed"

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

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

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

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

127− _ -> fail "IBC write failed"

128+ _ -> ifail "IBC write failed"

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

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

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

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

130− _ -> fail "IBC write failed"

131+ _ -> ifail "IBC write failed"

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

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

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

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

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

134ibc 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 }

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

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

138process i fn

139process i fn

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

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

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

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

141 | otherwise =

142 | otherwise =

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

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

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

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

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

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

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

187 case fp of

188 case fp of

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

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

189− fail "Must be an ibc"

190+ ifail "Must be an ibc"

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

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

191− fail "Must be an ibc"

192+ ifail "Must be an ibc"

192 IBC fn src -> loadIBC fn)

193 IBC fn src -> loadIBC fn)

193 fs

194 fs

194

195

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

272 mapM_ checkLoad res

273 mapM_ checkLoad res

273 return ()

274 return ()

274 where checkLoad (Left _) = return ()

275 where checkLoad (Left _) = return ()

275− checkLoad (Right err) = fail err

276+ checkLoad (Right err) = ifail err

276

277

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

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

278pHdrs hs = mapM_ (uncurry addHdr) hs

279pHdrs hs = mapM_ (uncurry addHdr) hs

src/Idris/Parser.hs+5−4

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

941 LIDR sfn -> loadSource True sfn)

942 let (dir, fh) = splitFileName file

943 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

946 iputStrLn msg

947 iputStrLn msg

947 return "")

948 return "")

948

949

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

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

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

965loadSource' lidr r

966loadSource' lidr r

966 = idrisCatch (loadSource lidr r)

967 = 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

969 iputStrLn msg)

970 iputStrLn msg)

970

971

971{- | Load Idris source code-}

972{- | Load Idris source code-}

src/Idris/Prover.hs+12−13

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

32 case lookupTy x ctxt of

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

34 then prove ctxt lit x t

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

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

36 _ -> fail "No such metavariable"

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

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

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

85elabStep st e = do case runStateT e st of

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

87− Error a -> do i <- getIState

87+ Error a -> ierror a

88− fail (pshow i a)

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

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

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

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

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

168 i <- receiveInput e

167 i <- receiveInput e

169 return (i, h)

168 return (i, h)

170 (cmd, step) <- case x of

169 (cmd, step) <- case x of

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

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

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

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

173 case cmd of

172 case cmd of

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

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

175 _ -> return ()

174 _ -> return ()

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

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

177 (case cmd of

176 (case cmd of

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

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

179 return (False, e, False, prf)

178 return (False, e, False, prf)

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

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

181− iResult ""

180+ iPrintResult ""

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

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

183− Success ProofState -> do iResult ""

182+ Success ProofState -> do iPrintResult ""

184 return (True, e, False, prf)

183 return (True, e, False, prf)

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

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

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

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

187 return (False, e, False, prf)

186 return (False, e, False, prf)

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

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

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

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

190− iResult "Proof completed!"

189+ iPrintResult "Proof completed!"

191 return (False, e, True, prf)

190 return (False, e, True, prf)

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

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

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

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

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

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

195− iResult ""

194+ iPrintResult ""

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

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

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

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

198 return (False, e, False, prf))

197 return (False, e, False, prf))

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

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

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

199 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

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

20 case err of

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

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

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

25 return res

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

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

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

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

src/Idris/REPL.hs+71−66

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

56import System.Directory

57import System.IO

58import Control.Monad

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

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

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

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

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

61import Data.Maybe

62import Data.Maybe

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

121 _ -> ""

122 _ -> ""

122 c <- colourise

123 c <- colourise

123 case parseCmd i "(input)" cmd of

124 case parseCmd i "(input)" cmd of

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

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

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

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

126 idrisCatch

127 idrisCatch

127 (do process fn (Prove n'))

128 (do process fn (Prove n'))

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

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

129 isetPrompt (mkPrompt mods)

130 isetPrompt (mkPrompt mods)

130 Success cmd -> idrisCatch

131 Success cmd -> idrisCatch

131 (do ideslaveProcess fn cmd)

132 (do ideslaveProcess fn cmd)

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

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

133 Just (REPLCompletions str) ->

134 Just (REPLCompletions str) ->

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

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

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

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

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

145 -- Report either success or failure

146 -- Report either success or failure

146 i <- getIState

147 i <- getIState

147 case (errLine i) of

148 case (errLine i) of

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

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

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

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

150 ideslave orig [filename]

151 ideslave orig [filename]

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

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

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

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

153 ideslave orig mods

154 ideslave orig mods

154

155

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

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

156ideslaveProcess fn Help = process fn Help

157ideslaveProcess fn Help = process fn Help

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

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

158− iResult "changed directory to"

159+ iPrintResult "changed directory to"

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

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

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

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

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

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

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

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

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

164ideslaveProcess fn Universes = process fn Universes

165ideslaveProcess fn Universes = process fn Universes

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

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

166− iResult ""

167+ iPrintResult ""

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

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

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

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

169− iResult ""

170+ iPrintResult ""

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

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

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

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

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

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

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

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

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

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

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

180ideslaveProcess fn Execute = do process fn Execute

181ideslaveProcess fn Execute = do process fn Execute

181− iResult ""

182+ iPrintResult ""

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

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

183− iResult ""

184+ iPrintResult ""

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

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

185− iResult ""

186+ iPrintResult ""

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

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

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

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

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

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

189− iResult ""

190+ iPrintResult ""

190ideslaveProcess fn ListDynamic = do process fn ListDynamic

191ideslaveProcess fn ListDynamic = do process fn ListDynamic

191− iResult ""

192+ iPrintResult ""

192ideslaveProcess fn Metavars = process fn Metavars

193ideslaveProcess fn Metavars = process fn Metavars

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

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

194− iResult ""

195+ iPrintResult ""

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

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

196− iResult ""

197+ iPrintResult ""

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

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

198− iResult ""

199+ iPrintResult ""

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

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

200− iResult ""

201+ iPrintResult ""

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

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

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

203ideslaveProcess 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"

204

205

206

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

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

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

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

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

251 return Nothing

252 return Nothing

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

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

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

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

254 return (Just inputs)

255 return (Just inputs)

255

256

256resolveProof :: Name -> Idris Name

257resolveProof :: Name -> Idris Name

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

260 n <- case lookupNames n' ctxt of

261 n <- case lookupNames n' ctxt of

261 [x] -> return x

262 [x] -> return x

262 [] -> return n'

263 [] -> return n'

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

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

264 return n

265 return n

265

266

266removeProof :: Name -> Idris ()

267removeProof :: Name -> Idris ()

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

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

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

309

310

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

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

311−process fn Help = iResult displayHelp

312+process fn Help = iPrintResult displayHelp

312process fn (ChangeDirectory f)

313process fn (ChangeDirectory f)

313 = do liftIO $ setCurrentDirectory f

314 = do liftIO $ setCurrentDirectory f

314 return ()

315 return ()

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

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

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

325 imp <- impShow

326 imp <- impShow

326 c <- colourise

327 c <- colourise

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

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

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

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

329process fn (ExecVal t)

330process fn (ExecVal t)

330 = do ctxt <- getContext

331 = do ctxt <- getContext

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

335 res <- execute tm

336 res <- execute tm

336 imp <- impShow

337 imp <- impShow

337 c <- colourise

338 c <- colourise

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

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

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

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

340process fn (Check (PRef _ n))

341process fn (Check (PRef _ n))

341 = do ctxt <- getContext

342 = do ctxt <- getContext

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

345 case lookupNames n ctxt of

346 case lookupNames n ctxt of

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

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

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

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

348− iResult ""

349+ iPrintResult ""

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

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

350process fn (Check t)

351process fn (Check t)

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

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

352 ctxt <- getContext

353 ctxt <- getContext

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

355 c <- colourise

356 c <- colourise

356 let ty' = normaliseC ctxt [] ty

357 let ty' = normaliseC ctxt [] ty

357 case tm of

358 case tm of

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

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

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

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

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

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

361

362

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

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

363 case lookupCtxtName n (idris_docstrings i) of

364 case lookupCtxtName n (idris_docstrings i) of

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

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

365 ns -> do mapM_ showDoc ns

366 ns -> do mapM_ showDoc ns

366− iResult ""

367+ iPrintResult ""

367 where showDoc (n, d)

368 where showDoc (n, d)

368 = do doc <- getDocs n

369 = do doc <- getDocs n

369 iputStrLn $ show doc

370 iputStrLn $ show doc

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

374 let n = length cs

375 let n = length cs

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

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

376 case ucheck cs of

377 case ucheck cs of

377− Error e -> iFail $ pshow i e

378+ Error e -> iPrintError $ pshow i e

378− OK _ -> iResult "Universes OK"

379+ OK _ -> iPrintResult "Universes OK"

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

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

380 iputStrLn "Compiled patterns:\n"

381 iputStrLn "Compiled patterns:\n"

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

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

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

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

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

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

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

394 case lookupTotal n (tt_ctxt i) of

395 case lookupTotal n (tt_ctxt i) of

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

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

396− _ -> do iFail ""

397+ _ -> do iPrintError ""

397 return ()

398 return ()

398process fn (DebugInfo n)

399process fn (DebugInfo n)

399 = do i <- getIState

400 = do i <- getIState

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

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

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

417 case lookupCtxt n (idris_classes i) of

418 case lookupCtxt n (idris_classes i) of

418 [c] -> classInfo c

419 [c] -> classInfo c

419− _ -> iFail "Not a class"

420+ _ -> iPrintError "Not a class"

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

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

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

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

422 ctxt <- getContext

423 ctxt <- getContext

423 ist <- getIState

424 ist <- getIState

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

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

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

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

426

427

427process fn (RmProof n')

428process fn (RmProof n')

428 = do i <- getIState

429 = do i <- getIState

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

449 then return fn'

450 then return fn'

450 else if exExt

451 else if exExt

451 then return fnExt

452 then return fnExt

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

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

453 let fb = fn ++ "~"

454 let fb = fn ++ "~"

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

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

455 prog <- liftIO $ readFile fb

456 prog <- liftIO $ readFile fb

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

457 let proofs = proof_list i

458 let proofs = proof_list i

458 n' <- case prf of

459 n' <- case prf of

459 Nothing -> case proofs of

460 Nothing -> case proofs of

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

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

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

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

462 Just nm -> return nm

463 Just nm -> return nm

463 n <- resolveProof n'

464 n <- resolveProof n'

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

474 n <- resolveProof n'

475 n <- resolveProof n'

475 let proofs = proof_list i

476 let proofs = proof_list i

476 case lookup n proofs of

477 case lookup n proofs of

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

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

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

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

479

480

480process fn (Prove n')

481process fn (Prove n')

481 = do ctxt <- getContext

482 = do ctxt <- getContext

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

483 n <- case lookupNames n' ctxt of

484 n <- case lookupNames n' ctxt of

484 [x] -> return x

485 [x] -> return x

485 [] -> return n'

486 [] -> return n'

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

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

487 prover (lit fn) n

488 prover (lit fn) n

488 -- recheck totality

489 -- recheck totality

489 i <- getIState

490 i <- getIState

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

495 ctxt <- getContext

496 ctxt <- getContext

496 ist <- getIState

497 ist <- getIState

497 let tm' = hnf ctxt [] tm

498 let tm' = hnf ctxt [] tm

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

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

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

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

500 ctxt <- getContext

501 ctxt <- getContext

501 ist <- getIState

502 ist <- getIState

502 let tm' = inlineTerm ist tm

503 let tm' = inlineTerm ist tm

503 imp <- impShow

504 imp <- impShow

504 c <- colourise

505 c <- colourise

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

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

506process fn TTShell = do ist <- getIState

507process fn TTShell = do ist <- getIState

507 let shst = initState (tt_ctxt ist)

508 let shst = initState (tt_ctxt ist)

508 runShell shst

509 runShell shst

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

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

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

530process fn (Pattelab t)

531process fn (Pattelab t)

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

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

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

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

533

534

534process fn (Missing n)

535process fn (Missing n)

535 = do i <- getIState

536 = do i <- getIState

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

537 case lookupCtxt n (idris_patdefs i) of

538 case lookupCtxt n (idris_patdefs i) of

538 [] -> return ()

539 [] -> return ()

539 [(_, tms)] ->

540 [(_, tms)] ->

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

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

541− _ -> iFail $ "Ambiguous name"

542+ _ -> iPrintError $ "Ambiguous name"

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

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

543 let lib = trim l

544 let lib = trim l

544− handle <- lift $ tryLoadLib lib

545+ handle <- lift . lift $ tryLoadLib lib

545 case handle of

546 case handle of

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

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

547 Just x -> do let libs = idris_dynamic_libs i

548 Just x -> do let libs = idris_dynamic_libs i

548 if x `elem` libs

549 if x `elem` libs

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

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

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

559 = do ist <- getIState

560 = do ist <- getIState

560 let mvs = idris_metavars ist \\ primDefs

561 let mvs = idris_metavars ist \\ primDefs

561 case mvs of

562 case mvs of

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

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

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

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

564process fn NOP = return ()

565process fn NOP = return ()

565

566

566process fn (SetOpt ErrContext) = setErrContext True

567process fn (SetOpt ErrContext) = setErrContext True

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

568process fn (SetOpt ShowImpl) = setImpShow True

569process fn (SetOpt ShowImpl) = setImpShow True

569process fn (UnsetOpt ShowImpl) = setImpShow False

570process fn (UnsetOpt ShowImpl) = setImpShow False

570

571

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

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

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

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

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

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

574process fn ColourOn = do ist <- getIState

575process fn ColourOn = do ist <- getIState

575 putIState $ ist { idris_colourRepl = True }

576 putIState $ ist { idris_colourRepl = True }

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

583 iputStrLn ""

584 iputStrLn ""

584 iputStrLn "Instances:\n"

585 iputStrLn "Instances:\n"

585 mapM_ dumpInstance (class_instances ci)

586 mapM_ dumpInstance (class_instances ci)

586− iResult ""

587+ iPrintResult ""

587

588

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

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

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

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

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

686 }

687 }

687

688

688-- invoke as if from command line

689-- invoke as if from command line

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

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

690−idris opts = execStateT (idrisMain opts) idrisInit

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+

691

696

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

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

693loadInputs inputs

698loadInputs inputs

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

886 h <- liftIO $ openFile script ReadMode

891 h <- liftIO $ openFile script ReadMode

887 runInit h

892 runInit h

888 liftIO $ hClose h)

893 liftIO $ hClose h)

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

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

890 where runInit :: Handle -> Idris ()

895 where runInit :: Handle -> Idris ()

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

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

892 ist <- getIState

897 ist <- getIState

893 unless eof $ do

898 unless eof $ do

894 line <- liftIO $ hGetLine h

899 line <- liftIO $ hGetLine h

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

899 processLine i cmd input clr =

904 processLine i cmd input clr =

900 case parseCmd i input cmd of

905 case parseCmd i input cmd of

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

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

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

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

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

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

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

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

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

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

906 Success Proofs -> proofs i

911 Success Proofs -> proofs i

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

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

908 Success cmd -> process [] cmd

913 Success cmd -> process [] cmd

909

914

910getFile :: Opt -> Maybe String

915getFile :: Opt -> Maybe String

src/Idris/Unlit.hs+3

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

11data LineType = Prog | Blank | Comm

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

21check f l [x] = return ()

23check f l [x] = return ()

22check f l [] = return ()

24check f l [] = return ()

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

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

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

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

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

26chkAdj f l _ _ = return ()

29chkAdj f l _ _ = return ()

src/Main.hs+2−1

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

9import Data.Maybe

10import Data.Version

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

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

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

12import Control.Monad.Trans ( liftIO )

13import Control.Monad.Trans ( liftIO )

13import Control.Monad ( when )

14import Control.Monad ( when )

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

41main = do xs <- getArgs

42main = do xs <- getArgs

42 let opts = parseArgs xs

43 let opts = parseArgs xs

43− execStateT (runIdris opts) idrisInit

44+ runErrorT $ execStateT (runIdris opts) idrisInit

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

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

46runIdris opts = do

47runIdris opts = do

src/Pkg/Package.hs+1−1

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

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

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

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

73− idris (map Filename f ++ opts)

73+ idris (map Filename f ++ opts)

74 return ()

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