63038b3 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Use the ErrorT failure functions and attempt to preserve error structure

63038b3David Christiansen13 years ago

src/IRTS/LParser.hs+4−3

compare with master

unifiedsplit

@@ -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+19−19

@@ -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/ElabDecls.hs+16−16

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

src/Idris/IBC.hs+14−13

@@ -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 }

@@ -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/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+61−61

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

122 _ -> ""

123 c <- colourise

124 case parseCmd i "(input)" cmd of

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

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

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

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

127 idrisCatch

128 (do process fn (Prove n'))

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

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

130 isetPrompt (mkPrompt mods)

131 Success cmd -> idrisCatch

132 (do ideslaveProcess fn cmd)

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

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

134 Just (REPLCompletions str) ->

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

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

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

146 -- Report either success or failure

147 i <- getIState

148 case (errLine i) of

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

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

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

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

151 ideslave orig [filename]

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

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

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

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

154 ideslave orig mods

155

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

157ideslaveProcess fn Help = process fn Help

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

159− iResult "changed directory to"

159+ iPrintResult "changed directory to"

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

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

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

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

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

165ideslaveProcess fn Universes = process fn Universes

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

167− iResult ""

167+ iPrintResult ""

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

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

170− iResult ""

170+ iPrintResult ""

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

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

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

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

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

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

181ideslaveProcess fn Execute = do process fn Execute

182− iResult ""

182+ iPrintResult ""

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

184− iResult ""

184+ iPrintResult ""

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

186− iResult ""

186+ iPrintResult ""

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

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

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

190− iResult ""

190+ iPrintResult ""

191ideslaveProcess fn ListDynamic = do process fn ListDynamic

192− iResult ""

192+ iPrintResult ""

193ideslaveProcess fn Metavars = process fn Metavars

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

195− iResult ""

195+ iPrintResult ""

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

197− iResult ""

197+ iPrintResult ""

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

199− iResult ""

199+ iPrintResult ""

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

201− iResult ""

201+ iPrintResult ""

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

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

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

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

205

206

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

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

261 n <- case lookupNames n' ctxt of

262 [x] -> return x

263 [] -> return n'

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

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

265 return n

266

267removeProof :: Name -> Idris ()

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

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

310

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

312−process fn Help = iResult displayHelp

312+process fn Help = iPrintResult displayHelp

313process fn (ChangeDirectory f)

314 = do liftIO $ setCurrentDirectory f

315 return ()

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

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

326 imp <- impShow

327 c <- colourise

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

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

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

330process fn (ExecVal t)

331 = do ctxt <- getContext

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

336 res <- execute tm

337 imp <- impShow

338 c <- colourise

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

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

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

341process fn (Check (PRef _ n))

342 = do ctxt <- getContext

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

346 case lookupNames n ctxt of

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

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

349− iResult ""

349+ iPrintResult ""

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

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

351process fn (Check t)

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

353 ctxt <- getContext

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

356 c <- colourise

357 let ty' = normaliseC ctxt [] ty

358 case tm of

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

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

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

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

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

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

362

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

364 case lookupCtxtName n (idris_docstrings i) of

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

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

366 ns -> do mapM_ showDoc ns

367− iResult ""

367+ iPrintResult ""

368 where showDoc (n, d)

369 = do doc <- getDocs n

370 iputStrLn $ show doc

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

375 let n = length cs

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

377 case ucheck cs of

378− Error e -> iFail $ pshow i e

378+ Error e -> iPrintError $ pshow i e

379− OK _ -> iResult "Universes OK"

379+ OK _ -> iPrintResult "Universes OK"

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

381 iputStrLn "Compiled patterns:\n"

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

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

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

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

395 case lookupTotal n (tt_ctxt i) of

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

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

397− _ -> do iFail ""

397+ _ -> do iPrintError ""

398 return ()

399process fn (DebugInfo n)

400 = do i <- getIState

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

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

418 case lookupCtxt n (idris_classes i) of

419 [c] -> classInfo c

420− _ -> iFail "Not a class"

420+ _ -> iPrintError "Not a class"

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

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

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

423 ctxt <- getContext

424 ist <- getIState

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

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

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

427

428process fn (RmProof n')

429 = do i <- getIState

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

450 then return fn'

451 else if exExt

452 then return fnExt

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

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

454 let fb = fn ++ "~"

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

456 prog <- liftIO $ readFile fb

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

458 let proofs = proof_list i

459 n' <- case prf of

460 Nothing -> case proofs of

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

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

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

463 Just nm -> return nm

464 n <- resolveProof n'

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

475 n <- resolveProof n'

476 let proofs = proof_list i

477 case lookup n proofs of

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

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

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

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

480

481process fn (Prove n')

482 = do ctxt <- getContext

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

484 n <- case lookupNames n' ctxt of

485 [x] -> return x

486 [] -> return n'

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

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

488 prover (lit fn) n

489 -- recheck totality

490 i <- getIState

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

496 ctxt <- getContext

497 ist <- getIState

498 let tm' = hnf ctxt [] tm

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

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

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

501 ctxt <- getContext

502 ist <- getIState

503 let tm' = inlineTerm ist tm

504 imp <- impShow

505 c <- colourise

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

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

507process fn TTShell = do ist <- getIState

508 let shst = initState (tt_ctxt ist)

509 runShell shst

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

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

531process fn (Pattelab t)

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

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

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

534

535process fn (Missing n)

536 = do i <- getIState

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

538 case lookupCtxt n (idris_patdefs i) of

539 [] -> return ()

540 [(_, tms)] ->

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

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

542− _ -> iFail $ "Ambiguous name"

542+ _ -> iPrintError $ "Ambiguous name"

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

544 let lib = trim l

545 handle <- lift . lift $ tryLoadLib lib

546 case handle of

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

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

548 Just x -> do let libs = idris_dynamic_libs i

549 if x `elem` libs

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

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

560 = do ist <- getIState

561 let mvs = idris_metavars ist \\ primDefs

562 case mvs of

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

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

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

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

565process fn NOP = return ()

566

567process fn (SetOpt ErrContext) = setErrContext True

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

569process fn (SetOpt ShowImpl) = setImpShow True

570process fn (UnsetOpt ShowImpl) = setImpShow False

571

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

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

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

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

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

575process fn ColourOn = do ist <- getIState

576 putIState $ ist { idris_colourRepl = True }

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

584 iputStrLn ""

585 iputStrLn "Instances:\n"

586 mapM_ dumpInstance (class_instances ci)

587− iResult ""

587+ iPrintResult ""

588

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

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

@@ -891,7 +891,7 @@ initScript = do script <- getInitScript

891 h <- liftIO $ openFile script ReadMode

892 runInit h

893 liftIO $ hClose h)

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

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

895 where runInit :: Handle -> Idris ()

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

897 ist <- getIState

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

904 processLine i cmd input clr =

905 case parseCmd i input cmd of

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

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

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

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

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

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

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

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

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

911 Success Proofs -> proofs i

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

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

913 Success cmd -> process [] cmd

914

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