Use Except instead or Error

diff --git a/Main.hs b/Main.hs
index a16426b5e8ec43adcf0ad7bd5b75813c49fb274f..e90edcfd3b4f31272ae2510f8d3ba012e62d3118 100644 (file)
--- a/Main.hs
+++ b/Main.hs
@@ -1,7 +1,7 @@
 module Main where
 
-import Control.Monad.Trans.Reader
-import Control.Monad.Error
+import Control.Monad.Reader
+import Control.Monad.Except
 import Control.Exception (try)
 import Data.List
 import System.Directory

diff --git a/Resolver.hs b/Resolver.hs
index 79d4529a8d87f187f74a8d90eccaca7239a82dc0..8e4e9c7e25d2c9fde6fba03644e0e6dcee21f622 100644 (file)
--- a/Resolver.hs
+++ b/Resolver.hs
@@ -1,26 +1,22 @@
-{-# LANGUAGE TupleSections, ParallelListComp #-}
+{-# LANGUAGE TupleSections #-}
 
 -- | Convert the concrete syntax into the syntax of cubical TT.
 module Resolver where
 
-import Exp.Abs
-import qualified CTT
-import qualified Connections as C
-
 import Control.Applicative
-import Control.Monad.Trans
-import Control.Monad.Trans.Reader
-import Control.Monad.Trans.Error hiding (throwError)
-import Control.Monad.Error (throwError)
 import Control.Monad
-import Data.Functor.Identity
+import Control.Monad.Reader
+import Control.Monad.Except
+import Control.Monad.Identity
 import Data.List (nub)
 import Data.Map (Map,(!))
 import qualified Data.Map as Map
-import Prelude hiding (pi)
 
-type Ter = CTT.Ter
-type Ident = CTT.Ident
+import Exp.Abs
+import CTT (Ter,Ident,Loc(..),mkApps,mkWheres)
+import qualified CTT
+import Connections (negFormula,andFormula,orFormula)
+import qualified Connections as C
 
 -- | Useful auxiliary functions
 
@@ -74,13 +70,13 @@ data Env = Env { envModule :: String,
                  variables :: [(Ident,SymKind)] }
   deriving (Eq,Show)
 
-type Resolver a = ReaderT Env (ErrorT String Identity) a
+type Resolver a = ReaderT Env (ExceptT String Identity) a
 
 emptyEnv :: Env
 emptyEnv = Env "" []
 
 runResolver :: Resolver a -> Either String a
-runResolver x = runIdentity $ runErrorT $ runReaderT x emptyEnv
+runResolver x = runIdentity $ runExceptT $ runReaderT x emptyEnv
 
 updateModule :: String -> Env -> Env
 updateModule mod e = e{envModule = mod}
@@ -108,8 +104,8 @@ insertAIdent (AIdent (_,x)) = insertIdent (x,Variable)
 insertAIdents :: [AIdent] -> Env -> Env
 insertAIdents  = flip $ foldr insertAIdent
 
-getLoc :: (Int,Int) -> Resolver CTT.Loc
-getLoc l = CTT.Loc <$> asks envModule <*> pure l
+getLoc :: (Int,Int) -> Resolver Loc
+getLoc l = Loc <$> asks envModule <*> pure l
 
 unAIdent :: AIdent -> Ident
 unAIdent (AIdent (_,x)) = x
@@ -160,7 +156,7 @@ binds :: (Ter -> Ter) -> [(Ident,Exp)] -> Resolver Ter -> Resolver Ter
 binds f = flip $ foldr $ bind f
 
 resolveApps :: Exp -> [Exp] -> Resolver Ter
-resolveApps x xs = CTT.mkApps <$> resolveExp x <*> mapM resolveExp xs
+resolveApps x xs = mkApps <$> resolveExp x <*> mapM resolveExp xs
 
 resolveExp :: Exp -> Resolver Ter
 resolveExp e = case e of
@@ -186,7 +182,7 @@ resolveExp e = case e of
     return $ foldr1 CTT.Pair (e:es)
   Let decls e   -> do
     (rdecls,names) <- resolveDecls decls
-    CTT.mkWheres rdecls <$> local (insertIdents names) (resolveExp e)
+    mkWheres rdecls <$> local (insertIdents names) (resolveExp e)
   Path is e     -> paths is (resolveExp e)
   Hole (HoleIdent (l,_)) -> CTT.Hole <$> getLoc l
   AppFormula e phi ->
@@ -235,11 +231,11 @@ resolveDir Dir1 = return 1
 resolveFormula :: Formula -> Resolver C.Formula
 resolveFormula (Dir d)          = C.Dir <$> resolveDir d
 resolveFormula (Atom i)         = C.Atom <$> resolveName i
-resolveFormula (Neg phi)        = C.negFormula <$> resolveFormula phi
+resolveFormula (Neg phi)        = negFormula <$> resolveFormula phi
 resolveFormula (Conj phi _ psi) =
-    C.andFormula <$> resolveFormula phi <*> resolveFormula psi
+    andFormula <$> resolveFormula phi <*> resolveFormula psi
 resolveFormula (Disj phi psi)   =
-    C.orFormula <$> resolveFormula phi <*> resolveFormula psi
+    orFormula <$> resolveFormula phi <*> resolveFormula psi
 
 resolveBranch :: Branch -> Resolver CTT.Branch
 resolveBranch (OBranch (AIdent (_,lbl)) args e) = do
@@ -247,7 +243,7 @@ resolveBranch (OBranch (AIdent (_,lbl)) args e) = do
   return $ CTT.OBranch lbl (map unAIdent args) re
 resolveBranch (PBranch (AIdent (_,lbl)) args i e) = do
   re <- local (insertName i . insertAIdents args) $ resolveWhere e
-  return $ CTT.PBranch lbl (map unAIdent args) (C.Name $ unAIdent i) re
+  return $ CTT.PBranch lbl (map unAIdent args) (C.Name (unAIdent i)) re
 
 resolveTele :: [(Ident,Exp)] -> Resolver CTT.Tele
 resolveTele []        = return []

diff --git a/TypeChecker.hs b/TypeChecker.hs
index aa90d9d50d39a75aaff9e838f5cb92205c704ce5..a4c9a48178176daaf95d3d8bf2d7b1ed0cb5c11b 100644 (file)
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -1,24 +1,22 @@
 {-# LANGUAGE TupleSections #-}\r
 module TypeChecker where\r
 \r
+import Control.Applicative\r
+import Control.Monad\r
+import Control.Monad.Except\r
+import Control.Monad.Reader\r
 import Data.Map (Map,(!),mapWithKey,assocs,filterWithKey,elems,keys\r
                 ,intersection,intersectionWith,intersectionWithKey\r
                 ,toList,fromList)\r
 import qualified Data.Map as Map\r
 import qualified Data.Traversable as T\r
-import Control.Monad\r
-import Control.Monad.Trans\r
-import Control.Monad.Trans.Error hiding (throwError)\r
-import Control.Monad.Trans.Reader\r
-import Control.Monad.Error (throwError)\r
-import Control.Applicative\r
 \r
 import Connections\r
 import CTT\r
 import Eval\r
 \r
 -- Type checking monad\r
-type Typing a = ReaderT TEnv (ErrorT String IO) a\r
+type Typing a = ReaderT TEnv (ExceptT String IO) a\r
 \r
 -- Environment for type checker\r
 data TEnv =\r
@@ -42,7 +40,7 @@ trace s = do
 -- | Functions for running computations in the type checker monad\r
 \r
 runTyping :: TEnv -> Typing a -> IO (Either String a)\r
-runTyping env t = runErrorT $ runReaderT t env\r
+runTyping env t = runExceptT $ runReaderT t env\r
 \r
 runDecls :: TEnv -> [Decl] -> IO (Either String TEnv)\r
 runDecls tenv d = runTyping tenv $ do\r