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

git.iko.soy/Idris-dev

Use the ErrorT failure functions and attempt to preserve error structure

commit63038b3f995e07b19a1efd034bba5832286c025d authorDavid Christiansen <david@davidchristiansen.dk> dateWed 16 Oct 2013, 14:49 (13 years ago) parent53b28e6

8 files changed+132−128

compare with master

unifiedsplit

src/IRTS/LParser.hs+4−3 src/Idris/AbsSyntax.hs+19−19 src/Idris/ElabDecls.hs+16−16 src/Idris/IBC.hs+14−13 src/Idris/Prover.hs+12−13 src/Idris/Providers.hs+3−3 src/Idris/REPL.hs+61−61 src/Idris/Unlit.hs+3

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

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

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

src/Idris/IBC.hs+14−13

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

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

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

122122 _ -> ""

123123 c <- colourise

124124 case parseCmd i "(input)" cmd of

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

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

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

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

127127 idrisCatch

128128 (do process fn (Prove n'))

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

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

130130 isetPrompt (mkPrompt mods)

131131 Success cmd -> idrisCatch

132132 (do ideslaveProcess fn cmd)

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

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

134134 Just (REPLCompletions str) ->

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

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

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

146146 -- Report either success or failure

147147 i <- getIState

148148 case (errLine i) of

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

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

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

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

151151 ideslave orig [filename]

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

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

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

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

154154 ideslave orig mods

155155

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

157157ideslaveProcess fn Help = process fn Help

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

159− iResult "changed directory to"

159+ iPrintResult "changed directory to"

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

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

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

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

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

165165ideslaveProcess fn Universes = process fn Universes

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

167− iResult ""

167+ iPrintResult ""

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

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

170− iResult ""

170+ iPrintResult ""

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

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

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

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

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

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

181181ideslaveProcess fn Execute = do process fn Execute

182− iResult ""

182+ iPrintResult ""

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

184− iResult ""

184+ iPrintResult ""

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

186− iResult ""

186+ iPrintResult ""

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

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

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

190− iResult ""

190+ iPrintResult ""

191191ideslaveProcess fn ListDynamic = do process fn ListDynamic

192− iResult ""

192+ iPrintResult ""

193193ideslaveProcess fn Metavars = process fn Metavars

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

195− iResult ""

195+ iPrintResult ""

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

197− iResult ""

197+ iPrintResult ""

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

199− iResult ""

199+ iPrintResult ""

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

201− iResult ""

201+ iPrintResult ""

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

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

205205

206206

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

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

261261 n <- case lookupNames n' ctxt of

262262 [x] -> return x

263263 [] -> return n'

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

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

265265 return n

266266

267267removeProof :: Name -> Idris ()

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

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

310310

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

312−process fn Help = iResult displayHelp

312+process fn Help = iPrintResult displayHelp

313313process fn (ChangeDirectory f)

314314 = do liftIO $ setCurrentDirectory f

315315 return ()

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

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

326326 imp <- impShow

327327 c <- colourise

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

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

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

330330process fn (ExecVal t)

331331 = do ctxt <- getContext

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

336336 res <- execute tm

337337 imp <- impShow

338338 c <- colourise

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

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

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

341341process fn (Check (PRef _ n))

342342 = do ctxt <- getContext

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

346346 case lookupNames n ctxt of

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

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

349− iResult ""

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

349+ iPrintResult ""

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

351351process fn (Check t)

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

353353 ctxt <- getContext

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

356356 c <- colourise

357357 let ty' = normaliseC ctxt [] ty

358358 case tm of

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

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

361− 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))

362362

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

364364 case lookupCtxtName n (idris_docstrings i) of

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

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

366366 ns -> do mapM_ showDoc ns

367− iResult ""

367+ iPrintResult ""

368368 where showDoc (n, d)

369369 = do doc <- getDocs n

370370 iputStrLn $ show doc

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

375375 let n = length cs

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

377377 case ucheck cs of

378− Error e -> iFail $ pshow i e

379− OK _ -> iResult "Universes OK"

378+ Error e -> iPrintError $ pshow i e

379+ OK _ -> iPrintResult "Universes OK"

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

381381 iputStrLn "Compiled patterns:\n"

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

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

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

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

395395 case lookupTotal n (tt_ctxt i) of

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

397− _ -> do iFail ""

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

397+ _ -> do iPrintError ""

398398 return ()

399399process fn (DebugInfo n)

400400 = do i <- getIState

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

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

418418 case lookupCtxt n (idris_classes i) of

419419 [c] -> classInfo c

420− _ -> iFail "Not a class"

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

420+ _ -> iPrintError "Not a class"

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

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

423423 ctxt <- getContext

424424 ist <- getIState

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

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

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

427427

428428process fn (RmProof n')

429429 = do i <- getIState

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

450450 then return fn'

451451 else if exExt

452452 then return fnExt

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

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

454454 let fb = fn ++ "~"

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

456456 prog <- liftIO $ readFile fb

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

458458 let proofs = proof_list i

459459 n' <- case prf of

460460 Nothing -> case proofs of

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

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

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

463463 Just nm -> return nm

464464 n <- resolveProof n'

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

475475 n <- resolveProof n'

476476 let proofs = proof_list i

477477 case lookup n proofs of

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

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

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

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

480480

481481process fn (Prove n')

482482 = do ctxt <- getContext

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

484484 n <- case lookupNames n' ctxt of

485485 [x] -> return x

486486 [] -> return n'

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

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

488488 prover (lit fn) n

489489 -- recheck totality

490490 i <- getIState

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

496496 ctxt <- getContext

497497 ist <- getIState

498498 let tm' = hnf ctxt [] tm

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

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

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

501501 ctxt <- getContext

502502 ist <- getIState

503503 let tm' = inlineTerm ist tm

504504 imp <- impShow

505505 c <- colourise

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

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

507507process fn TTShell = do ist <- getIState

508508 let shst = initState (tt_ctxt ist)

509509 runShell shst

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

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

531531process fn (Pattelab t)

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

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

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

534534

535535process fn (Missing n)

536536 = do i <- getIState

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

538538 case lookupCtxt n (idris_patdefs i) of

539539 [] -> return ()

540540 [(_, tms)] ->

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

542− _ -> iFail $ "Ambiguous name"

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

542+ _ -> iPrintError $ "Ambiguous name"

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

544544 let lib = trim l

545545 handle <- lift . lift $ tryLoadLib lib

546546 case handle of

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

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

548548 Just x -> do let libs = idris_dynamic_libs i

549549 if x `elem` libs

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

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

560560 = do ist <- getIState

561561 let mvs = idris_metavars ist \\ primDefs

562562 case mvs of

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

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

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

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

565565process fn NOP = return ()

566566

567567process fn (SetOpt ErrContext) = setErrContext True

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

569569process fn (SetOpt ShowImpl) = setImpShow True

570570process fn (UnsetOpt ShowImpl) = setImpShow False

571571

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

573−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"

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

575575process fn ColourOn = do ist <- getIState

576576 putIState $ ist { idris_colourRepl = True }

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

584584 iputStrLn ""

585585 iputStrLn "Instances:\n"

586586 mapM_ dumpInstance (class_instances ci)

587− iResult ""

587+ iPrintResult ""

588588

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

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

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

891891 h <- liftIO $ openFile script ReadMode

892892 runInit h

893893 liftIO $ hClose h)

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

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

895895 where runInit :: Handle -> Idris ()

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

897897 ist <- getIState

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

904904 processLine i cmd input clr =

905905 case parseCmd i input cmd of

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

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

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

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

910− 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"

911911 Success Proofs -> proofs i

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

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

913913 Success cmd -> process [] cmd

914914

915915getFile :: 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 ()