From: Anders <mortberg@chalmers.se>
Date: Fri, 17 Apr 2015 12:38:07 +0000 (+0200)
Subject: Use Except instead or Error
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=b1a94bbc57ae97c02f9c5827296e4ddcab1dcd05;p=cubicaltt.git

Use Except instead or Error
---

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