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

idris.cabal−1

compare with master

unifiedsplit

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

600 , Idris.Core.Execute

601 , Idris.Core.ProofState

602 , Idris.Core.ProofTerm

603− , Idris.Core.TC

604 , Idris.Core.TT

603 , Idris.Core.TT

605 , Idris.Core.Typecheck

604 , Idris.Core.Typecheck

606 , Idris.Core.Unify

605 , Idris.Core.Unify

src/Idris/AbsSyntaxTree.hs+2−2

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

19import System.IO

20

21import Control.Monad.Trans.State.Strict

22−import Control.Monad.Trans.Error

22+import Control.Monad.Trans.Except

23

24import Data.Function (on)

25import Data.List hiding (group)

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

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

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

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

304

305-- Commands in the REPL

306

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

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

786 -> Bool

787 -> [a]

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

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

789+ (ElabState t) TC t1

790 -> ElabState t

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

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

792prunStateT pmax zok ps x s

793 = case runStateT x s of

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

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

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

571

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

573

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

575convEq 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

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

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

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

22import Control.Exception

23import Control.Monad.Trans

24import Control.Monad.Trans.State.Strict

25−import Control.Monad.Trans.Error

25+import Control.Monad.Trans.Except

26import Control.Monad hiding (forM)

27import Data.Maybe

28import Data.Bits

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

126initState = do ist <- getIState

127 return $ ExecState (idris_dynamic_libs ist) []

128

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

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

130

131runExec :: 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

133

134getExecState :: Exec ExecState

135getExecState = 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 @@

18 programs with implicit syntax into fully explicit terms.

19-}

20

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

21+module Idris.Core.TT where

22−

23−import Idris.Core.TC

24

22

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

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

25import Control.Monad.State.Strict

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

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

27import Debug.Trace

28import qualified Data.Map.Strict as Map

29import Data.Char

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

162

163type Err = Err' Term

164

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+

165{-!

195{-!

166deriving instance NFData Err

196deriving instance NFData Err

167!-}

197!-}

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

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

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

235 pretty _ = text "Error"

265 pretty _ = text "Error"

236

266

237−instance Error Err where

238− strMsg = InternalMsg

239−

240−type TC = TC' Err

241−

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

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

243 pretty (OK ok) = pretty ok

268 pretty (OK ok) = pretty ok

244 pretty (Error err) =

269 pretty (Error err) =

src/Idris/IdrisDoc.hs+2−2

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

18import IRTS.System (getDataFileName)

19

20import Control.Monad (forM_)

21−import Control.Monad.Trans.Error

21+import Control.Monad.Trans.Except

22import Control.Monad.Trans.State.Strict

23

24import Data.Maybe

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

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

259 -> IO (Maybe Docs)

260loadDocs ist n

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

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

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

263 Left _ -> return Nothing

264 | otherwise = return Nothing

src/Idris/Output.hs+8−3

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

13import Util.Pretty

14import Util.ScreenSize (getScreenWidth)

15

16−import Debug.Trace

17−

18−import Control.Monad.Except (throwError)

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

19

17

18+import System.Console.Haskeline.MonadException

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

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

21

22import Data.Char (isAlpha)

23import Data.List (nub, intersperse)

24import Data.Maybe (fromMaybe)

25

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+

26pshow :: IState -> Err -> String

31pshow :: IState -> Err -> String

27pshow ist err = displayDecorated (consoleDecorate ist) .

32pshow ist err = displayDecorated (consoleDecorate ist) .

28 renderPretty 1.0 80 .

33 renderPretty 1.0 80 .

src/Idris/REPL.hs+4−4

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

75import System.Directory

76import System.IO

77import Control.Monad

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

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

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

80import Control.Monad.Trans ( lift )

81import Control.Concurrent.MVar

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

169processNetCmd orig i h fn cmd

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

171 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

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

174 case res of

175 Right x -> return x

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

1316

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

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

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

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

1320 case res of

1321 Left err -> do putStrLn $ pshow idrisInit err

1322 return Nothing

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

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

1591

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

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

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

1594 case res of

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

1596 Right _ -> return ()

src/Idris/TypeSearch.hs+1−1

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

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

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

246

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

247+tcToMaybe :: TC a -> Maybe a

248tcToMaybe (OK x) = Just x

249tcToMaybe (Error _) = Nothing

250

src/Pkg/Package.hs+2−2

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

12

13import Control.Monad

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

15−import Control.Monad.Error (runErrorT)

15+import Control.Monad.Except (runExceptT)

16

17import Data.List

18import Data.List.Split(splitOn)

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

145 setCurrentDirectory $ pkgDir </> sourcedir pkgdesc

146 make (makefile pkgdesc)

147 setCurrentDirectory $ pkgDir

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

148+ let run l = runExceptT . execStateT l

149 load [] = return ()

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

151 loader = do idrisMain opts; load fs