00f1cd5 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Use ExceptT instead of ErrorT

commit00f1cd5d2e14f491e345aca7d53a864d35b5e169 authorbmsherman <bmsherman@users.noreply.github.com> dateWed 17 Dec 2014, 21:24 (12 years ago) parentf7b72a6

12 files changed+60−68

compare with master

unifiedsplit

idris.cabal−1 src/Idris/AbsSyntaxTree.hs+2−2 src/Idris/Core/Elaborate.hs+2−2 src/Idris/Core/Evaluate.hs+2−2 src/Idris/Core/Execute.hs+3−3 src/Idris/Core/TC.hs−37 src/Idris/Core/TT.hs+34−9 src/Idris/IdrisDoc.hs+2−2 src/Idris/Output.hs+8−3 src/Idris/REPL.hs+4−4 src/Idris/TypeSearch.hs+1−1 src/Pkg/Package.hs+2−2

idris.cabal−1

@@ -600,7 +600,6 @@ Library

600600 , Idris.Core.Execute

601601 , Idris.Core.ProofState

602602 , Idris.Core.ProofTerm

603− , Idris.Core.TC

604603 , Idris.Core.TT

605604 , Idris.Core.Typecheck

606605 , Idris.Core.Unify

src/Idris/AbsSyntaxTree.hs+2−2

@@ -19,7 +19,7 @@ import System.Console.Haskeline

1919import System.IO

2020

2121import Control.Monad.Trans.State.Strict

22−import Control.Monad.Trans.Error

22+import Control.Monad.Trans.Except

2323

2424import Data.Function (on)

2525import Data.List hiding (group)

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

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

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

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

303−type Idris = StateT IState (ErrorT Err IO)

303+type Idris = StateT IState (ExceptT Err IO)

304304

305305-- Commands in the REPL

306306

src/Idris/Core/Elaborate.hs+2−2

@@ -786,9 +786,9 @@ prunStateT

786786 -> Bool

787787 -> [a]

788788 -> Control.Monad.State.Strict.StateT

789− (ElabState t) (TC' Err) t1

789+ (ElabState t) TC t1

790790 -> ElabState t

791− -> TC' Err ((t1, Int, Idris.Core.Unify.Fails), ElabState t)

791+ -> TC ((t1, Int, Idris.Core.Unify.Fails), ElabState t)

792792prunStateT pmax zok ps x s

793793 = case runStateT x s of

794794 OK (v, s'@(ES (p, _) _ _)) ->

src/Idris/Core/Evaluate.hs+2−2

@@ -571,9 +571,9 @@ isUsableUniverse x = isUniverse x

571571

572572convEq' ctxt hs x y = evalStateT (convEq ctxt hs x y) (0, [])

573573

574−convEq :: Context -> [Name] -> TT Name -> TT Name -> StateT UCs (TC' Err) Bool

574+convEq :: Context -> [Name] -> TT Name -> TT Name -> StateT UCs TC Bool

575575convEq ctxt holes topx topy = ceq [] topx topy where

576− ceq :: [(Name, Name)] -> TT Name -> TT Name -> StateT UCs (TC' Err) Bool

576+ ceq :: [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool

577577 ceq ps (P xt x _) (P yt y _)

578578 | x `elem` holes || y `elem` holes = return True

579579 | x == y || (x, y) `elem` ps || (y,x) `elem` ps = return True

src/Idris/Core/Execute.hs+3−3

@@ -22,7 +22,7 @@ import Control.Applicative hiding (Const)

2222import Control.Exception

2323import Control.Monad.Trans

2424import Control.Monad.Trans.State.Strict

25−import Control.Monad.Trans.Error

25+import Control.Monad.Trans.Except

2626import Control.Monad hiding (forM)

2727import Data.Maybe

2828import Data.Bits

@@ -126,10 +126,10 @@ initState :: Idris ExecState

126126initState = do ist <- getIState

127127 return $ ExecState (idris_dynamic_libs ist) []

128128

129−type Exec = ErrorT Err (StateT ExecState IO)

129+type Exec = ExceptT Err (StateT ExecState IO)

130130

131131runExec :: Exec a -> ExecState -> IO (Either Err a)

132−runExec ex st = fst <$> runStateT (runErrorT ex) st

132+runExec ex st = fst <$> runStateT (runExceptT ex) st

133133

134134getExecState :: Exec ExecState

135135getExecState = lift get

src/Idris/Core/TC.hsdeleted−37

@@ -1,37 +0,0 @@

1−{-# LANGUAGE DeriveFunctor #-}

2−

3−module Idris.Core.TC(TC'(..)) where

4−

5−import Control.Applicative

6−import Control.Monad

7−import Control.Monad.Trans.Error(Error(..))

8−

9−data TC' e a = OK !a

10− | Error e

11− deriving (Eq, Functor)

12−

13−bindTC :: TC' e a -> (a -> TC' e b) -> TC' e b

14−bindTC x k = case x of

15− OK v -> k v

16− Error e -> Error e

17−{-# INLINE bindTC #-}

18−

19−instance Error e => Monad (TC' e) where

20− return x = OK x

21− x >>= k = bindTC x k

22− fail e = Error (strMsg e)

23−

24−instance Error e => MonadPlus (TC' e) where

25− mzero = fail "Unknown error"

26− (OK x) `mplus` _ = OK x

27− _ `mplus` (OK y) = OK y

28− err `mplus` _ = err

29−

30−

31−instance Error e => Applicative (TC' e) where

32− pure = return

33− (<*>) = ap

34−

35−instance Error e => Alternative (TC' e) where

36− empty = mzero

37− (<|>) = mplus

src/Idris/Core/TT.hs+34−9

@@ -18,12 +18,12 @@

1818 programs with implicit syntax into fully explicit terms.

1919-}

2020

21−module Idris.Core.TT(module Idris.Core.TT, module Idris.Core.TC) where

22−

23−import Idris.Core.TC

21+module Idris.Core.TT where

2422

23+import Control.Applicative (Applicative (..), Alternative)

24+import qualified Control.Applicative as A (Alternative (..))

2525import Control.Monad.State.Strict

26−import Control.Monad.Trans.Error (Error(..))

26+import Control.Monad.Trans.Except (Except (..))

2727import Debug.Trace

2828import qualified Data.Map.Strict as Map

2929import Data.Char

@@ -162,6 +162,36 @@ data Err' t

162162

163163type Err = Err' Term

164164

165+data TC a = OK !a

166+ | Error Err

167+ deriving (Eq, Functor)

168+

169+bindTC :: TC a -> (a -> TC b) -> TC b

170+bindTC x k = case x of

171+ OK v -> k v

172+ Error e -> Error e

173+{-# INLINE bindTC #-}

174+

175+instance Monad TC where

176+ return x = OK x

177+ x >>= k = bindTC x k

178+ fail e = Error (InternalMsg e)

179+

180+instance MonadPlus TC where

181+ mzero = fail "Unknown error"

182+ (OK x) `mplus` _ = OK x

183+ _ `mplus` (OK y) = OK y

184+ err `mplus` _ = err

185+

186+

187+instance Applicative TC where

188+ pure = return

189+ (<*>) = ap

190+

191+instance Alternative TC where

192+ empty = mzero

193+ (<|>) = mplus

194+

165195{-!

166196deriving instance NFData Err

167197!-}

@@ -234,11 +264,6 @@ instance Pretty Err OutputAnnotation where

234264 pretty err@(LoadingFailed _ _) = text (show err)

235265 pretty _ = text "Error"

236266

237−instance Error Err where

238− strMsg = InternalMsg

239−

240−type TC = TC' Err

241−

242267instance (Pretty a OutputAnnotation) => Pretty (TC a) OutputAnnotation where

243268 pretty (OK ok) = pretty ok

244269 pretty (Error err) =

src/Idris/IdrisDoc.hs+2−2

@@ -18,7 +18,7 @@ import qualified Idris.Docstrings as Docstrings

1818import IRTS.System (getDataFileName)

1919

2020import Control.Monad (forM_)

21−import Control.Monad.Trans.Error

21+import Control.Monad.Trans.Except

2222import Control.Monad.Trans.State.Strict

2323

2424import Data.Maybe

@@ -258,7 +258,7 @@ loadDocs :: IState -- ^ IState to extract infomation from

258258 -> Name -- ^ Name to load Docs for

259259 -> IO (Maybe Docs)

260260loadDocs ist n

261− | mayHaveDocs n = do docs <- runErrorT $ evalStateT (getDocs n) ist

261+ | mayHaveDocs n = do docs <- runExceptT $ evalStateT (getDocs n) ist

262262 case docs of Right d -> return (Just d)

263263 Left _ -> return Nothing

264264 | otherwise = return Nothing

src/Idris/Output.hs+8−3

@@ -13,16 +13,21 @@ import Idris.IdeSlave

1313import Util.Pretty

1414import Util.ScreenSize (getScreenWidth)

1515

16−import Debug.Trace

17−

18−import Control.Monad.Except (throwError)

16+import Control.Monad.Except (ExceptT (ExceptT), runExceptT, throwError)

1917

18+import System.Console.Haskeline.MonadException

19+ (MonadException (controlIO), RunIO (RunIO))

2020import System.IO (stdout, Handle, hPutStrLn)

2121

2222import Data.Char (isAlpha)

2323import Data.List (nub, intersperse)

2424import Data.Maybe (fromMaybe)

2525

26+instance MonadException m => MonadException (ExceptT Err m) where

27+ controlIO f = ExceptT $ controlIO $ \(RunIO run) -> let

28+ run' = RunIO (fmap ExceptT . run . runExceptT)

29+ in fmap runExceptT $ f run'

30+

2631pshow :: IState -> Err -> String

2732pshow ist err = displayDecorated (consoleDecorate ist) .

2833 renderPretty 1.0 80 .

src/Idris/REPL.hs+4−4

@@ -75,7 +75,7 @@ import System.Process

7575import System.Directory

7676import System.IO

7777import Control.Monad

78−import Control.Monad.Trans.Error (ErrorT(..))

78+import Control.Monad.Trans.Except (ExceptT, runExceptT)

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

8080import Control.Monad.Trans ( lift )

8181import Control.Concurrent.MVar

@@ -169,7 +169,7 @@ processNetCmd :: IState -> IState -> Handle -> FilePath -> String ->

169169processNetCmd orig i h fn cmd

170170 = do res <- case parseCmd i "(net)" cmd of

171171 Failure err -> return (Left (Msg " invalid command"))

172− Success (Right c) -> runErrorT $ evalStateT (processNet fn c) i

172+ Success (Right c) -> runExceptT $ evalStateT (processNet fn c) i

173173 Success (Left err) -> return (Left (Msg err))

174174 case res of

175175 Right x -> return x

@@ -1316,7 +1316,7 @@ replSettings hFile = setComplete replCompletion $ defaultSettings {

13161316

13171317-- | Invoke as if from command line. It is an error if there are unresolved totality problems.

13181318idris :: [Opt] -> IO (Maybe IState)

1319−idris opts = do res <- runErrorT $ execStateT totalMain idrisInit

1319+idris opts = do res <- runExceptT $ execStateT totalMain idrisInit

13201320 case res of

13211321 Left err -> do putStrLn $ pshow idrisInit err

13221322 return Nothing

@@ -1590,7 +1590,7 @@ idrisMain opts =

15901590 addIBC (IBCImportDir (ddir </> p))

15911591

15921592runMain :: Idris () -> IO ()

1593−runMain prog = do res <- runErrorT $ execStateT prog idrisInit

1593+runMain prog = do res <- runExceptT $ execStateT prog idrisInit

15941594 case res of

15951595 Left err -> putStrLn $ "Uncaught error: " ++ show err

15961596 Right _ -> return ()

src/Idris/TypeSearch.hs+1−1

@@ -244,7 +244,7 @@ findName n (args, classes) = findNameInArgsDAG n args <|> ((,) <$> lookup n clas

244244deleteName :: Name -> (ArgsDAG, Classes) -> (ArgsDAG, Classes)

245245deleteName n (args, classes) = (deleteFromDag n args, filter ((/= n) . fst) classes)

246246

247−tcToMaybe :: TC' e a -> Maybe a

247+tcToMaybe :: TC a -> Maybe a

248248tcToMaybe (OK x) = Just x

249249tcToMaybe (Error _) = Nothing

250250

src/Pkg/Package.hs+2−2

@@ -12,7 +12,7 @@ import Util.System

1212

1313import Control.Monad

1414import Control.Monad.Trans.State.Strict (execStateT)

15−import Control.Monad.Error (runErrorT)

15+import Control.Monad.Except (runExceptT)

1616

1717import Data.List

1818import Data.List.Split(splitOn)

@@ -145,7 +145,7 @@ documentPkg fp =

145145 setCurrentDirectory $ pkgDir </> sourcedir pkgdesc

146146 make (makefile pkgdesc)

147147 setCurrentDirectory $ pkgDir

148− let run l = runErrorT . (execStateT l)

148+ let run l = runExceptT . execStateT l

149149 load [] = return ()

150150 load (f:fs) = do loadModule f; load fs

151151 loader = do idrisMain opts; load fs