packages feed

MiniAgda 0.2014.5.5 → 0.2014.9.12

raw patch · 15 files changed

+210/−198 lines, 15 filesdep −IfElsedep ~haskell-src-extsdep ~mtl

Dependencies removed: IfElse

Dependency ranges changed: haskell-src-exts, mtl

Files

Abstract.hs view
@@ -676,11 +676,11 @@         succMeas (e:es) = e : succMeas es -} -applyLastM :: Monad m => (a -> m a) -> Measure a -> m (Measure a)-applyLastM f (Measure mu) = loop mu >>= return . Measure+applyLastM :: (a -> Maybe a) -> Measure a -> Maybe (Measure a)+applyLastM f (Measure mu) = Measure <$> loop mu   where loop []     = fail "empty measure"-        loop [e]    = f e >>= return . (:[])-        loop (e:es) = loop es >>= return . (e:)+        loop [e]    = (:[]) <$> f e+        loop (e:es) = (e:)  <$> loop es  instance HasPred a => HasPred (Measure a) where   predecessor mu = applyLastM predecessor mu
Eval.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE TupleSections, FlexibleInstances, NamedFieldPuns #-}+{-# LANGUAGE TupleSections, FlexibleInstances, FlexibleContexts, NamedFieldPuns #-} {-# LANGUAGE NoImplicitPrelude #-} {-# LANGUAGE CPP #-} @@ -12,10 +12,8 @@ import Control.Applicative import Control.Monad.Identity hiding (mapM) import Control.Monad.State hiding (mapM)-import Control.Monad.Error hiding (mapM)+import Control.Monad.Except hiding (mapM) import Control.Monad.Reader hiding (mapM)-import Control.Monad.IfElse  -- unlessM--- import Control.Monad.HT      -- andLazy  -- because liftM2 (&&) is NOT lazy!  import qualified Data.Array as Array import Data.Maybe -- fromMaybe@@ -72,6 +70,9 @@ traceSizeM msg = traceM msg -} +failValInv :: (MonadError TraceError m) => Val -> m a+failValInv v = throwErrorMsg $ "internal error: value " ++ show v ++ " violates representation invariant"+ -- evaluation with rewriting -------------------------------------  {-@@ -546,7 +547,7 @@       bv  <- whnf env b -- not adding measure constraint to context!       case (envBound env) of         Nothing   -> return $ VMeasured muv bv-           -- fail $ "panic: whnf " ++ show e ++ " : no measure in environment " ++ show env+           -- throwErrorMsg $ "panic: whnf " ++ show e ++ " : no measure in environment " ++ show env         Just muv' -> return $ VGuard (Bound Lt muv muv') bv      Quant Pi (TBound (Bound ltle mu mu')) b -> do@@ -603,7 +604,7 @@         whnfClos (definingVal item)      Def (DefId (ConK DefPat) n) -> whnfClos . definingVal =<< lookupSymbQ n---    Def (DefId (ConK DefPat) n) -> fail $ "internal error: whnf of defined pattern " ++ show n+--    Def (DefId (ConK DefPat) n) -> throwErrorMsg $ "internal error: whnf of defined pattern " ++ show n     Def id   -> return $ vDef id {-     Con co n -> return $ VCon co n@@ -619,7 +620,7 @@     Var y -> lookupEnv env y >>= whnfClos     Ann e -> whnf env (unTag e) -- return VIrr -- NEED TO KEEP because of eta-exp!     Irr -> return VIrr-    e   -> fail $ "NYI whnf " ++ show e+    e   -> throwErrorMsg $ "NYI whnf " ++ show e  whnfMeasure :: Env -> Measure Expr -> TypeCheck (Measure Val) whnfMeasure rho (Measure mu) = mapM (whnf rho) mu >>= return . Measure@@ -704,7 +705,7 @@             VProj Pre n -> flip (app' expandDefs) (VProj Post n) =<< whnfClos v             VRecord ri rho -> do               let VProj Post n = v-              maybe (fail $ "app: projection " ++ show n ++ " not found in " ++ show u)+              maybe (throwErrorMsg $ "app: projection " ++ show n ++ " not found in " ++ show u)                 whnfClos (lookup n rho)             VDef (DefId FunK n) -> appDef_ n [v]             VApp (VDef (DefId FunK n)) vl -> appDef_ n (vl ++ [v])@@ -739,7 +740,7 @@              VIrr -> return VIrr {- 2010-11-01 this breaks extraction for System U example-            VIrr -> fail $ "app internal error: " ++ show (VApp u [v])+            VIrr -> throwErrorMsg $ "app internal error: " ++ show (VApp u [v]) -}             _ -> return $ VApp u [v] --@@ -764,7 +765,7 @@ -- -- ALT: VIrr consumes applications --             (VIrr,_) -> return VIrr --  -}---             (VIrr,_) -> fail $ "app internal error: " ++ show (VApp u c)+--             (VIrr,_) -> throwErrorMsg $ "app internal error: " ++ show (VApp u c) --             _ -> return $ VApp u c  @@ -871,7 +872,7 @@ matchingConstructors v@(VDef d) = failValInv v -- matchingConstructors' d [] matchingConstructors (VApp (VDef (DefId DatK d)) vl) = matchingConstructors' d vl >>= return . Just matchingConstructors v = return Nothing--- fail $ "matchingConstructors: not a data type: " ++ show v -- return []+-- throwErrorMsg $ "matchingConstructors: not a data type: " ++ show v -- return []  matchingConstructors' :: QName -> [Val] -> TypeCheck [(ConstructorInfo,Env)] matchingConstructors' n vl = do@@ -1183,7 +1184,7 @@ matchList env (p:pl) (v:vl) =   match env p v `bindMaybe` \ env' ->   matchList env' pl vl-matchList env pl     vl     = fail $ "matchList internal error: inequal length while trying to match patterns " ++ show pl ++ " against values " ++ show vl+matchList env pl     vl     = throwErrorMsg $ "matchList internal error: inequal length while trying to match patterns " ++ show pl ++ " against values " ++ show vl  -- * Typed Non-linear Matching ----------------------------------------- @@ -1255,7 +1256,7 @@     VQuant Pi x dom fv ->       nonLinMatch undot symm st p v (typ dom) `bindMaybe` \ st' ->       nonLinMatchList' undot symm st' pl vl =<< app fv v-    _ -> fail $ "nonLinMatchList': cannot match in absence of pi-type"+    _ -> throwErrorMsg $ "nonLinMatchList': cannot match in absence of pi-type" nonLinMatchList' _ _ _ _ _ _ = return Nothing  @@ -1264,7 +1265,7 @@ expandDefPat p@(ConP pi c ps) | coPat pi == DefPat = do   PatSig ns pat v <- lookupSymbQ c   unless (length ns == length ps) $-    fail ("underapplied defined pattern in " ++ show p)+    throwErrorMsg ("underapplied defined pattern in " ++ show p)   let pat' = if dottedPat pi then dotConstructors pat else pat   return $ patSubst (zip ns ps) pat' expandDefPat p = return p@@ -1341,7 +1342,7 @@       VIrr                  -> mempty       VCase v tv env cls    -> nocc ks $ v : tv : map snd (envMap env)       -- impossible: closure (reduced away)-      VClos{}               -> fail $ "internal error: nocc " ++ show (ks,v)+      VClos{}               -> throwErrorMsg $ "internal error: nocc " ++ show (ks,v)   -- heterogeneous typed equality and subtyping ------------------------@@ -1450,7 +1451,7 @@     Set   v -> ShSet   (One v)     CoSet v -> ShCoSet (One v) -typeView12 :: (Functor m, Error e, MonadError e m) => OneOrTwo TVal -> m TypeShape+typeView12 :: (Functor m, Monad m, MonadError TraceError m) => OneOrTwo TVal -> m TypeShape -- typeView12 :: OneOrTwo TVal -> TypeCheck TypeShape typeView12 (One tv) = return $ typeView tv typeView12 (Two tv1 tv2) =@@ -1465,16 +1466,16 @@            (ShSort s1, ShSort s2) | s1 == s2 -> return $ ShSort $ s1            (ShData n1 _, ShData n2 _) | n1 == n2 -> return $ ShData n1 (Two tv1 tv2)            (ShNe{}     , ShNe{}     )            -> return $ ShNe (Two tv1 tv2)-           _ -> throwError $ strMsg $ "type " ++ show tv1 ++ " has different shape than " ++ show tv2+           _ -> throwErrorMsg $ "type " ++ show tv1 ++ " has different shape than " ++ show tv2 -sortView12 :: (Monad m) => OneOrTwo (Sort Val) -> m SortShape+sortView12 :: (Monad m, MonadError TraceError m) => OneOrTwo (Sort Val) -> m SortShape sortView12 (One s) = return $ sortView s sortView12 (Two s1 s2) =   case (s1, s2) of     (SortC c1, SortC c2) | c1 == c2 -> return $ ShSortC c1     (Set v1, Set v2)                -> return $ ShSet (Two v1 v2)     (CoSet v1, CoSet v2)            -> return $ ShCoSet (Two v1 v2)-    _ -> fail $ "sort " ++ show s1 ++ " has different shape than " ++ show s2+    _ -> throwErrorMsg $ "sort " ++ show s1 ++ " has different shape than " ++ show s2  whnf12 :: OneOrTwo Env -> OneOrTwo Expr -> TypeCheck (OneOrTwo Val) whnf12 env12 e12 = Traversable.traverse id $ zipWith12 whnf env12 e12@@ -1514,9 +1515,9 @@     mt12f <- mapM (mapM force) mt12 -- leads to LOOP, see HungryEta.ma     sh12 <- case mt12f of               Nothing -> return Nothing-              Just tv12 -> case typeView12 tv12 of+              Just tv12 -> case runExcept $ typeView12 tv12 of                 Right sh -> return $ Just sh-                Left err -> (recoverFail err) >> return Nothing+                Left err -> (recoverFail $ show err) >> return Nothing     case sh12 of        -- subtyping directed by common type shape@@ -1740,14 +1741,14 @@             loop cls1' cls2'  eqPattern :: Pattern -> Pattern -> TypeCheck ()-eqPattern p1 p2 = if p1 == p2 then return () else fail $ "pattern " ++ show p1 ++ " != " ++ show p2+eqPattern p1 p2 = if p1 == p2 then return () else throwErrorMsg $ "pattern " ++ show p1 ++ " != " ++ show p2 -}  type NameMap = [(Name,Name)]  alphaPattern :: Pattern -> Pattern -> StateT NameMap TypeCheck () alphaPattern p1 p2 = do-  let failure = fail $ "pattern " ++ show p1 ++ " != " ++ show p2+  let failure = throwErrorMsg $ "pattern " ++ show p1 ++ " != " ++ show p2       alpha x1 x2 = do         ns <- get         case lookup x1 ns of@@ -1836,7 +1837,7 @@            <+> prettyTCM vl1 <+> text " to "            <+> prettyTCM vl2 <+> text " at type "            <+> prettyTCM tv12---    _ -> fail $ "leqVals': not (compatible) function types or mismatch number of arguments when comparing  " ++ show vl1 ++ "  to  " ++ show vl2 ++ "  at type  " ++ show tv12+--    _ -> throwErrorMsg $ "leqVals': not (compatible) function types or mismatch number of arguments when comparing  " ++ show vl1 ++ "  to  " ++ show vl2 ++ "  at type  " ++ show tv12  {- leqVals' f q (VPi x1 dom1@(Domain av1 _ dec1) env1 b1,@@ -2084,8 +2085,8 @@          (v1,VMeta i rho n) -> addLe ltle v1 v2          _ -> leSize'' ltle 0 v1 v2 {- HANDLED BY leSize'' ltle-         (VSucc{}, VGen{}) -> fail err-         (VSucc{}, VPlus{}) -> fail err+         (VSucc{}, VGen{}) -> throwErrorMsg err+         (VSucc{}, VPlus{}) -> throwErrorMsg err -} -- leSize'' ltle bal v v'  checks whether  Succ^bal v `lt` v' -- invariant: bal is zero in cases for VMax and VMeta@@ -2254,7 +2255,7 @@     (True,False) -> ret LT -- THIS IS COMPLETE BOGUS!!!     (True,True)  -> ret EQ     (False,True) -> ret GT-    (False,False) -> fail $ "compareSize (" ++ show a1 ++ ", " ++ show a2 ++ "): sizes incomparable"+    (False,False) -> throwErrorMsg $ "compareSize (" ++ show a1 ++ ", " ++ show a2 ++ "): sizes incomparable" -}  {- Bound entailment
Extract.hs view
@@ -152,7 +152,7 @@  import Control.Applicative import Control.Monad-import Control.Monad.Error+import Control.Monad.Except import Control.Monad.Reader import Control.Monad.Writer import Control.Monad.State@@ -176,7 +176,7 @@  traceExtrM s = return () -runExtract sig k = runErrorT (runReaderT (runStateT k (initWithSig sig)) emptyContext)+runExtract sig k = runExceptT (runReaderT (runStateT k (initWithSig sig)) emptyContext)  -- extraction @@ -198,7 +198,7 @@ extractDecl d =   case d of     MutualDecl _ ds -> extractDecls ds -- TODO!-    OverrideDecl{} -> fail $ "extractDecls internal error: overrides impossible"+    OverrideDecl{} -> throwErrorMsg $ "extractDecls internal error: overrides impossible"     MutualFunDecl _ co funs -> extractFuns co funs     FunDecl co fun -> extractFun co fun     LetDecl evl x tel (Just t) e | null tel -> extractLet evl x t e@@ -354,7 +354,7 @@             Prod av1 av2 ->               extractPattern' av1 p1 $ \ [p1] -> do                 extractPattern' av2 p2 $ \ [p2] -> cont [PairP p1 p2]-            _ -> fail $ "extractPattern': IMPOSSIBLE: pattern " +++            _ -> throwErrorMsg $ "extractPattern': IMPOSSIBLE: pattern " ++                           show p ++ " : " ++ show av -}         ConP pi n ps -> do@@ -369,7 +369,7 @@   ConSig { conPars, extrTyp, dataPars } <- lookupSymbQ c   traceExtrM ("extrConType " ++ show c ++ " has extrTyp = " ++ show extrTyp)   tv <- whnf' extrTyp-  numPars <- maybe (return dataPars) (const $ fail $ "NYI: extrConType for pattern parameters") conPars+  numPars <- maybe (return dataPars) (const $ throwErrorMsg $ "NYI: extrConType for pattern parameters") conPars   case numPars of    0 -> return tv    _ -> do@@ -387,7 +387,7 @@         piApps tv pars -}       _ -> piApps tv $ replicate numPars VIrr---      _ -> fail $ "extrConType " ++ show c ++ ": expected datatype, found " ++ show av+--      _ -> throwErrorMsg $ "extrConType " ++ show c ++ ": expected datatype, found " ++ show av  -- extracting a term from a term ------------------------------------- @@ -412,7 +412,7 @@      Def f -> (Def f,) <$> do (whnf' . extrTyp) =<< lookupSymbQ (idName f) -    Pair{} -> fail $ "extractInfer: IMPOSSIBLE: pair " ++ show e+    Pair{} -> throwErrorMsg $ "extractInfer: IMPOSSIBLE: pair " ++ show e     -- other expressions are erased or types      _ -> return (Irr, VIrr)@@ -458,7 +458,7 @@ {-       case view of         Prod av1 av2 -> Pair <$> extractCheck e1 av1 <*> extractCheck e2 av2-        _ -> fail $ "extractCheck: tuple type expected " ++ show e ++ " : " ++ show tv+        _ -> throwErrorMsg $ "extractCheck: tuple type expected " ++ show e ++ " : " ++ show tv -}      -- TODO: case
Makefile view
@@ -3,11 +3,11 @@ files=Abstract Collection Concrete Eval Extract HsSyntax Lexer Main Parser Polarity PrettyTCM ScopeChecker Semiring SparseMatrix TCM Termination ToHaskell Tokens TraceError TreeShapedOrder TypeChecker Util Value Warshall hsfiles=$(foreach file,$(files),$(file).hs) ghcflags=-ignore-package monads-fd -rtsopts-# -fglasgow-exts +# -fglasgow-exts optflags= # -O  #slow compilation, not much speedup profflags=-prof -auto-all-distfiles=*.hs *.hs-boot Lexer.x Parser.y Makefile +distfiles=*.hs *.hs-boot Lexer.x Parser.y Makefile distdirs=test/succeed test/fail examples  cabalp=cabal install -p --enable-executable-profiling@@ -43,10 +43,10 @@ #	Main test/fail/OverlappingPatternIndFam.ma # vec.ma # examples/List.ma  # ship : ../dist/miniagda-2009-07-03.tgz # 06-27.tgz-# +# # ../dist/%.tgz : $(distfiles) # 	tar czf $@ $^ $(distdirs)-# +#  miniagda-prof : Main.hs $(hsfiles) 	ghc $(ghcflags) $(profflags) $< --make -o $@@@ -76,13 +76,13 @@  test : Main succeed fail -succeed : +succeed : 	@echo "======================================================================" 	@echo "===================== Suite of successfull tests =====================" 	@echo "======================================================================" 	make -C test/succeed -fail : +fail : 	@echo "======================================================================" 	@echo "======================= Suite of failing tests =======================" 	@echo "======================================================================"@@ -101,7 +101,7 @@ 	make -C lib  -clean : +clean : 	-rm *.o *.hi Main miniagda-prof # 	make -C test/fail clean
MiniAgda.cabal view
@@ -1,7 +1,7 @@ name:            MiniAgda-version:         0.2014.5.5+version:         0.2014.9.12 build-type:      Simple-cabal-version:   >= 1.8 +cabal-version:   >= 1.8 license:         OtherLicense license-file:    LICENSE author:          Andreas Abel and Karl Mehltretter@@ -20,10 +20,9 @@   arguments are discarded during equality checking and compilation.    Recent features include bounded size quantification and destructor-  patterns for a more general handling of coinduction. +  patterns for a more general handling of coinduction. -tested-with:        GHC == 7.6.3,-                    GHC == 7.8.2+tested-with:        GHC == 7.8.3  extra-source-files: Makefile @@ -44,12 +43,9 @@   build-depends:    array >= 0.3 && < 0.6,                     base >= 4.2 && < 4.8,                     containers >= 0.3 && < 0.6,-                    haskell-src-exts >= 1.14 && < 1.15,-                    -- mtl-2.1 contains a severe bug-                    mtl >= 2.0 && < 2.1 || >= 2.1.1 && < 2.2,-                    pretty >= 1.0 && < 1.2,---                    utility-ht >= 0.0.1 && < 1.0,-                    IfElse >= 0.85 && < 2.0+                    haskell-src-exts >= 1.14 && < 1.16,+                    mtl >= 2.2.0.1 && < 2.3,+                    pretty >= 1.0 && < 1.2   build-tools:      happy >= 1.15 && < 2,                     alex >= 3.0 && < 4   extensions:       CPP
ScopeChecker.hs view
@@ -9,12 +9,11 @@  import Prelude hiding (mapM, null) -import Control.Applicative -- <$>-import Control.Monad.IfElse+import Control.Applicative import Control.Monad.Identity hiding (mapM) import Control.Monad.Reader hiding (mapM) import Control.Monad.State hiding (mapM)-import Control.Monad.Error hiding (mapM)+import Control.Monad.Except hiding (mapM)  import Data.List as List hiding (null) import Data.Maybe@@ -153,7 +152,7 @@ -- State monad (hidden) for global signature. -- Error monad for reporting scope violations. newtype ScopeCheck a = ScopeCheck { unScopeCheck ::-  ReaderT SCCxt (StateT SCState (ErrorT TraceError Identity)) a }+  ReaderT SCCxt (StateT SCState (ExceptT TraceError Identity)) a }   deriving (Functor, Applicative, Monad,     MonadReader SCCxt, MonadError TraceError) @@ -162,7 +161,7 @@   -> SCState        -- ^ Global identifier mapping.   -> ScopeCheck a   -- ^ The computation.   -> Either TraceError (a, SCState)-runScopeCheck ctx st (ScopeCheck sc) = runIdentity $ runErrorT $+runScopeCheck ctx st (ScopeCheck sc) = runIdentity $ runExceptT $   runStateT (runReaderT sc ctx) st  -- ** Local state.@@ -419,7 +418,7 @@   let (ns, mll) = unzip $ compressMaybes mmm   let measured = null mll || isJust (head mll)   let ok = null mll || all ((head mll)==) (tail mll)-  when (not ok) $ fail $ "in a mutual function block, either all functions must be without measure or have a measure of the same length"+  when (not ok) $ throwErrorMsg $ "in a mutual function block, either all functions must be without measure or have a measure of the same length" {-   -- switch to internal fun ids   let funNames = [ n | (FunK _ , A.TypeSig n _) <- ktsigs ] -- internal fun names@@ -483,11 +482,11 @@  mutualFlattenDecl :: C.Declaration -> ScopeCheck [C.Declaration] mutualFlattenDecl (C.MutualDecl ds) = mutualFlattenDecls ds-mutualFlattenDecl (C.OverrideDecl Fail _) = fail $ "fail declaration not supported in mutual block"+mutualFlattenDecl (C.OverrideDecl Fail _) = throwErrorMsg $ "fail declaration not supported in mutual block" mutualFlattenDecl (C.OverrideDecl o ds) = do   ds' <- mutualFlattenDecls ds   return $ map (\ d -> C.OverrideDecl o [d]) ds'-mutualFlattenDecl (C.LetDecl{}) = fail $ "let in mutual block not supported"+mutualFlattenDecl (C.LetDecl{}) = throwErrorMsg $ "let in mutual block not supported" mutualFlattenDecl d = return $ [d]  -- extract type sigs of a mutual block in order, error on nested mutual@@ -600,7 +599,7 @@   r <- mapM (\ (C.FunDecl _ tysig _) -> scopeCheckFunSig tysig) l   let (ml:mll, tsl') = unzip r   let ok = all (ml==) mll-  when (not ok) $ fail $ "in a mutual function block, either all functions must be without measure or have a measure of the same length"+  when (not ok) $ throwErrorMsg $ "in a mutual function block, either all functions must be without measure or have a measure of the same length"   -- add names as internal ids and check bodies   let nxs = zipWith (\ (C.FunDecl _ (C.TypeSig n _) _) (A.TypeSig x _) -> (n,x)) l tsl'   --let addFuns b = mapM (uncurry $ addAName $ FunK b) nxs@@ -785,7 +784,7 @@           A.Param   -> return dec           A.Const   -> return dec           A.PVar{}  -> return dec-          _         -> fail $ "illegal polarity " ++ show (polarity dec) ++ " in type of constructor " ++ show a+          _         -> throwErrorMsg $ "illegal polarity " ++ show (polarity dec) ++ " in type of constructor " ++ show a  -- | Allow shadowing of previous locals. --   Always if we enter a subexpression which is not the body@@ -827,7 +826,7 @@       -- measure & bound       -- measures can only appear in fun sigs!       C.Quant pisig [C.TMeasure mu] e1 -> do-        fail $ "measure not allowed in expression " ++ show e+        throwErrorMsg $ "measure not allowed in expression " ++ show e        -- measure bound mu < mu'       C.Quant A.Pi [C.TBound beta] e1 -> do@@ -836,7 +835,7 @@         e1'   <- scopeCheckExpr' e1         return $ A.pi (A.TBound beta') e1' -      C.Quant A.Sigma [C.TBound beta] e1 -> fail $+      C.Quant A.Sigma [C.TBound beta] e1 -> throwErrorMsg $         "measure bound not allowed in expression " ++ show e        C.Quant pisig tel e -> do@@ -875,7 +874,7 @@           Just x -> return $ A.Var x           Nothing -> scopeCheckGlobalVar n -      _ -> fail $ "NYI: scopeCheckExpr " ++ show e+      _ -> throwErrorMsg $ "NYI: scopeCheckExpr " ++ show e  scopeCheckGlobalVar :: C.QName -> ScopeCheck A.Expr scopeCheckGlobalVar n = do@@ -1065,7 +1064,7 @@     C.Record fs          -> mapM_ (scpField e) fs     C.Ident n            -> scpApp e n []     C.App (C.Ident n) es -> scpApp e n es-    C.App C.App{} es     -> fail $ "scopeCheckParameter " ++ show e ++ ": internal invariant violated"+    C.App C.App{} es     -> throwErrorMsg $ "scopeCheckParameter " ++ show e ++ ": internal invariant violated"     _ -> errorInvalidParameter e   where     -- we can only treat a record expression as pattern
TCM.hs view
@@ -5,10 +5,9 @@ import Prelude hiding (null)  import Control.Monad-import Control.Monad.IfElse import Control.Monad.Identity import Control.Monad.State-import Control.Monad.Error+import Control.Monad.Except import Control.Monad.Reader  import Control.Applicative@@ -226,7 +225,7 @@ emptyPosGraph = []  -- type TypeCheck = StateT TCState (ReaderT TCContext (CallStackT String IO))-type TypeCheck = StateT TCState (ReaderT TCContext (ErrorT TraceError IO))+type TypeCheck = StateT TCState (ReaderT TCContext (ExceptT TraceError IO))  instance MonadAssert TypeCheck where   assert b s = do@@ -412,49 +411,21 @@         -- upperDecs need not be updated         } -{---- only defined for single bindings-cxtSetType :: Int -> Dec -> TVal -> SemCxt -> SemCxt-cxtSetType k dec tv delta =-  delta { cxt  = Map.insert k (One tv) (cxt delta)-        , decs = Map.insert k (One dec) (decs delta)-        -- upperDecs need not be updated-        }---        , decs = Map.insert k dec (decs delta) }--}-{--cxtLookupGen :: Monad m => SemCxt -> Int -> m Domain-cxtLookupGen delta k = do-  One tv  <- lookupM k (cxt delta)-  One dec <- lookupM k (decs delta)---  dec    <- lookupM k (decs delta)-  return $ Domain { typ = tv, decor = dec }+-- | Version of 'Map.lookup' that throws 'TraceError'.+lookupM :: (MonadError TraceError m, Show k, Ord k) => k -> Map k v -> m v+lookupM k m = maybe (throwErrorMsg $ "lookupM: unbound key " ++ show k) return $ Map.lookup k m -cxtLookupGen :: Monad m => SemCxt -> Int -> m CxtEntry-cxtLookupGen delta k = do-  tv12  <- lookupM k (cxt delta)-  dec12 <- lookupM k (decs delta)-  udec  <- lookupM k (upperDecs delta)-  return $ CxtEntry (zipWith12 Domain tv12 dec12) udec--}-cxtLookupGen :: Monad m => SemCxt -> Int -> m CxtEntry+cxtLookupGen :: MonadError TraceError m => SemCxt -> Int -> m CxtEntry cxtLookupGen delta k = do   dom12 <- lookupM k (cxt delta)   udec  <- lookupM k (upperDecs delta)   return $ CxtEntry dom12 udec -cxtLookupName :: Monad m => SemCxt -> Ren -> Name -> m CxtEntry+cxtLookupName :: MonadError TraceError m => SemCxt -> Ren -> Name -> m CxtEntry cxtLookupName delta ren x = do   i <- lookupM x ren   cxtLookupGen delta i -{--cxtLookupName :: Monad m => SemCxt -> Ren -> Name -> m Domain-cxtLookupName delta ren x = do-  i <- lookupM x ren-  cxtLookupGen delta i--}- -- apply decoration, possibly resurrecting (see Pfenning, LICS 2001) -- and changing polarities (see Abel, MSCS 2008) cxtApplyDec :: Dec -> SemCxt -> SemCxt@@ -631,14 +602,14 @@   genOfName x = do     ce <- ask     case Map.lookup x (renaming ce) of-      Nothing -> fail $ "internal error: variable not bound: " ++ show x+      Nothing -> throwErrorMsg $ "internal error: variable not bound: " ++ show x       Just k -> return k    nameOfGen k = do     ce <- ask     case Map.lookup k (naming ce) of       Nothing -> return $ fresh $ "error_unnamed_gen" ++ show k-       -- fail $ "internal error: no name for variable " ++ show k+       -- throwErrorMsg $ "internal error: no name for variable " ++ show k       Just x -> return x  {-@@ -784,7 +755,7 @@            TSO.increasesHeight son (dist, father) <$> asks sizeRels) $ do       recoverFail $ "cannot add hypothesis " ++ s ++ " because it is not satisfyable under all possible valuations of the current hypotheses"     -- if the new son is an ancestor of the father, we are cyclic-    awhenM (TSO.isAncestor father son <$> asks sizeRels) $ \ n -> -- n steps from father up to son+    whenJustM (TSO.isAncestor father son <$> asks sizeRels) $ \ n -> -- n steps from father up to son       when (dist > - n) $ -- still ok if dist == n == 0, otherwise fail         recoverFail$ "cannot add hypothesis " ++ s ++ " because it makes the set of hyptheses unsatisfiable"     local (\ cxt -> cxt@@ -982,11 +953,11 @@     VApp (VDef (DefId DatK d)) vl ->       case p of         ProjP n -> cont =<< projectType tv n VIrr -- no record value here-        _       -> fail $ "introPatType: internal error, expected projection pattern, found " ++ show p ++ " at type " ++ show tv+        _       -> throwErrorMsg $ "introPatType: internal error, expected projection pattern, found " ++ show p ++ " at type " ++ show tv     VQuant Pi x dom fv -> do        v  <- whnfClos v        matchPatType (p,v) dom . cont =<< app fv v-    _ -> fail $ "introPatType: internal error, expected Pi-type, found " ++ show tv+    _ -> throwErrorMsg $ "introPatType: internal error, expected Pi-type, found " ++ show tv  introPatTypes :: [(Pattern,Val)] -> TVal -> (TVal -> TypeCheck a) -> TypeCheck a introPatTypes pvs tv f = do@@ -1021,12 +992,12 @@                  matchPatType (p1,v1) dom1 $ do                    bv <- app fv v1                    matchPatType (p2,v2) (Domain bv ki dec) cont-               _ -> fail $ "matchPatType: IMPOSSIBLE " ++ show p ++ "  :  " ++ show dom+               _ -> throwErrorMsg $ "matchPatType: IMPOSSIBLE " ++ show p ++ "  :  " ++ show dom            (DotP e, _) -> cont           (AbsurdP, _) -> cont           (ErasedP p,_) -> matchPatType (p,v) dom cont-          _ -> fail $ "matchPatType: IMPOSSIBLE " ++ show (p,v)+          _ -> throwErrorMsg $ "matchPatType: IMPOSSIBLE " ++ show (p,v)   -- Signature -----------------------------------------------------@@ -1164,7 +1135,7 @@       dv <- dataView tv       case dv of         Data d _ -> return $ Qual d n-        _ -> fail $ "cannot resolve constructor " ++ show n+        _ -> throwErrorMsg $ "cannot resolve constructor " ++ show n  -- | @conType c tv@ returns the type of constructor @c@ at datatype @tv@ --   with parameters instantiated.@@ -1209,7 +1180,7 @@     NoData    -> failDoc (text ("conType " ++ show c ++ ": expected")                    <+> prettyTCM tv <+> text "to be a data type")     Data d vs -> do-      unless (d == dataName) $ fail $ "expected constructor of datatype " ++ show d ++ ", but found one of datatype " ++ show dataName+      unless (d == dataName) $ throwErrorMsg $ "expected constructor of datatype " ++ show d ++ ", but found one of datatype " ++ show dataName       let (pars, inds) = splitAt numPars vs       unless (length pars == numPars) $         failDoc (text ("conType " ++ show c ++ ": expected")@@ -1247,8 +1218,8 @@                    <+> prettyTCM tv <+> text "to be a data type")     Data d vs -> do       whenJust md $ \ d' ->-        unless (d == d') $ fail $ "expected constructor of datatype " ++ show d ++ ", but found one of datatype " ++ show d'-      -- whenJust conPars $ fail $ "NYI: constructor with pattern parameters"+        unless (d == d') $ throwErrorMsg $ "expected constructor of datatype " ++ show d ++ ", but found one of datatype " ++ show d'+      -- whenJust conPars $ throwErrorMsg $ "NYI: constructor with pattern parameters"       let (pars, inds) = splitAt dataPars vs       unless (length pars == dataPars) failure       case (isSized, inds) of@@ -1364,7 +1335,7 @@       -- lookupSig :: Name -> Signature -> TypeCheck SigDef       lookupSig n sig =         case (Map.lookup n sig) of-          Nothing -> fail $ "identifier " ++ show n ++ " not in signature "  ++ show (Map.keys sig)+          Nothing -> throwErrorMsg $ "identifier " ++ show n ++ " not in signature "  ++ show (Map.keys sig)           Just k -> return k  @@ -1411,8 +1382,8 @@   mkConstraint v (VMax vs) = do     bs <- mapM (errorToBool . leqSize' v) vs     if any id bs then return Nothing else-     fail $ "cannot handle constraint " ++ show v ++ " <= " ++ show (VMax vs)-  mkConstraint w@(VMax vs) v = fail $ "cannot handle constraint " ++ show w ++ " <= " ++ show v+     throwErrorMsg $ "cannot handle constraint " ++ show v ++ " <= " ++ show (VMax vs)+  mkConstraint w@(VMax vs) v = throwErrorMsg $ "cannot handle constraint " ++ show w ++ " <= " ++ show v   mkConstraint (VMeta i rho n) (VMeta j rho' m) = retret $ arc (Flex i) (m-n) (Flex j)   mkConstraint (VMeta i rho n) VInfty      = retret $ arc (Flex i) 0 (Rigid (RConst Infinite))   mkConstraint (VMeta i rho n) v           = retret $ arc (Flex i) (m-n) (Rigid (RVar j))@@ -1420,7 +1391,7 @@   mkConstraint VInfty (VMeta i rho n)      = retret $ arc (Rigid (RConst Infinite)) 0 (Flex i)   mkConstraint v (VMeta j rho m)           = retret $ arc (Rigid (RVar i)) (m-n) (Flex j)     where (i,n) = vGenSuccs v 0-  mkConstraint v1 v2 = fail $ "mkConstraint undefined for " ++ show (v1,v2)+  mkConstraint v1 v2 = throwErrorMsg $ "mkConstraint undefined for " ++ show (v1,v2)    -- addMeta k x  adds a metavariable which can refer to VGens < k   -- addMeta :: Ren -> MVar -> TypeCheck ()@@ -1450,7 +1421,7 @@      else case solve cs of         Just subst -> traceMeta ("solution" ++ show subst) $                       return subst-        Nothing    -> fail $ "size constraints " ++ show cs ++ " unsolvable"+        Nothing    -> throwErrorMsg $ "size constraints " ++ show cs ++ " unsolvable"   nameOf :: EnvMap -> Int -> Maybe Name
TCM.hs-boot view
@@ -5,7 +5,7 @@  import Control.Monad.Identity import Control.Monad.State-import Control.Monad.Error+import Control.Monad.Except import Control.Monad.Reader  data OneOrTwo a = One a | Two a a@@ -14,4 +14,4 @@ data TCState  -- type TypeCheck = StateT TCState (ReaderT TCContext (CallStackT String IO))-type TypeCheck = StateT TCState (ReaderT TCContext (ErrorT TraceError IO))+type TypeCheck = StateT TCState (ReaderT TCContext (ExceptT TraceError IO))
ToHaskell.hs view
@@ -45,7 +45,7 @@  import Control.Applicative import Control.Monad-import Control.Monad.Error+import Control.Monad.Except import Control.Monad.Reader import Control.Monad.Writer import Control.Monad.State@@ -66,7 +66,7 @@  -- translation monad -type Translate = StateT TState (ReaderT TContext (ErrorT TraceError IO))+type Translate = StateT TState (ReaderT TContext (ExceptT TraceError IO))  {- no longer needed with mtl-2 instance Applicative Translate where@@ -85,7 +85,7 @@ initCxt = TContext  runTranslate :: Translate a -> IO (Either TraceError a)-runTranslate t = runErrorT (runReaderT (evalStateT t initSt) initCxt)+runTranslate t = runExceptT (runReaderT (evalStateT t initSt) initCxt)  -- translation @@ -101,7 +101,7 @@ translateDecl d =   case d of     MutualDecl _ ds -> translateDecls ds-    OverrideDecl{} -> fail $ "translateDecls internal error: overrides impossible"+    OverrideDecl{} -> throwErrorMsg $ "translateDecls internal error: overrides impossible"     MutualFunDecl _ _ funs -> translateFuns funs     FunDecl _ fun -> translateFun fun     LetDecl _ x tel (Just t) e | null tel -> translateLet x t e@@ -196,7 +196,7 @@     _ -> return H.unit_tycon  {- TODO:-    _ -> fail $ "no Haskell representation for type " ++ show t+    _ -> throwErrorMsg $ "no Haskell representation for type " ++ show t  -}  translateExpr :: FExpr -> Translate H.Exp@@ -269,7 +269,7 @@   (DefId DatK (QName x)) -> do     let n = suggestion x     unless (isUpper $ head n) $-      fail $ "data names need to be capitalized"+      throwErrorMsg $ "data names need to be capitalized"     return $ H.Ident n   (DefId (ConK co) (Qual d x)) -> do     let n = suggestion x@@ -283,7 +283,7 @@     let n = suggestion $ unqual x {- ignore for now      unless (isLower $ head n) $-       fail $ "function names need to start with a lowercase letter"+       throwErrorMsg $ "function names need to start with a lowercase letter"  -}     return $ H.Ident n
TraceError.hs view
@@ -2,7 +2,7 @@  module TraceError where -import Control.Monad.Error+import Control.Monad.Except import Debug.Trace  import Util@@ -10,9 +10,9 @@  data TraceError = Err String | TrErr String TraceError -instance Error TraceError where-    noMsg = Err "no message"-    strMsg s = Err s+-- instance Error TraceError where+--     noMsg = Err "no message"+--     strMsg s = Err s  instance Show TraceError where     show (Err str) = str@@ -35,8 +35,8 @@   d <- md   enter (render (pretty d)) cont -failDoc :: (Monad m) => m Doc -> m a-failDoc d = fail . render =<< d+failDoc :: (MonadError TraceError m) => m Doc -> m a+failDoc d = throwErrorMsg . render =<< d  newErrorDoc :: (MonadError TraceError m) => m a -> m Doc -> m a newErrorDoc c d = c `catchError` (\ _ -> failDoc d)@@ -47,13 +47,13 @@ errorToBool :: (MonadError e m) => m () -> m Bool errorToBool m = (m >> return True) `catchError` (\ _ -> return False) -boolToErrorDoc :: (Monad m) => m Doc -> Bool -> m ()+boolToErrorDoc :: (MonadError TraceError m) => m Doc -> Bool -> m () boolToErrorDoc d True  = return () boolToErrorDoc d False = failDoc d -boolToError :: (Monad m) => String -> Bool -> m ()+boolToError :: (MonadError TraceError m) => String -> Bool -> m () boolToError msg True  = return ()-boolToError msg False = fail msg+boolToError msg False = throwErrorMsg msg  instance MonadError () Maybe where   catchError Nothing k = k ()@@ -68,13 +68,13 @@ data AssertionHandling = Failure | Warning | Ignore                        deriving (Eq,Ord,Show) -assert' :: (MonadIO m) => AssertionHandling -> Bool -> String -> m ()+assert' :: (MonadError TraceError m, MonadIO m) => AssertionHandling -> Bool -> String -> m () assert' Ignore b s      = return () assert' h True s        = return () assert' Warning False s = liftIO $ putStrLn $ "warning: ignoring error: " ++ s-assert' Failure False s = fail s+assert' Failure False s = throwErrorMsg s -assertDoc' :: (MonadIO m) => AssertionHandling -> Bool -> m Doc -> m ()+assertDoc' :: (MonadError TraceError m, MonadIO m) => AssertionHandling -> Bool -> m Doc -> m () assertDoc' h b md = assert' h b . render =<< md  class Monad m => MonadAssert m where
TreeShapedOrder.hs view
@@ -61,7 +61,7 @@  -- | @parent a o@ returns the immediate parent, if it exists. parent :: (Ord a, Eq a) => a -> TSO a -> Maybe (Int,a)-parent a t = headM $ parents a t+parent a t = headMaybe $ parents a t  -- | @isAncestor a b o = Just n@ if there are n steps up from a to b. isAncestor :: (Ord a, Eq a) => a -> a -> TSO a -> Maybe Int
TypeChecker.hs view
@@ -7,10 +7,9 @@  import Control.Applicative hiding (Const) -- ((<$>)) import Control.Monad-import Control.Monad.IfElse import Control.Monad.Identity import Control.Monad.State-import Control.Monad.Error+import Control.Monad.Except import Control.Monad.Reader  import qualified Data.List as List@@ -68,17 +67,17 @@  {- DEAD CODE runWhnf :: Signature -> TypeCheck a -> IO (Either TraceError (a,Signature))-runWhnf sig tc = (runErrorT (runStateT tc  sig))+runWhnf sig tc = (runExceptT (runStateT tc  sig)) -} -doNf sig e = runErrorT (runReaderT (runStateT (whnf emptyEnv e >>= reify) (initWithSig sig)) emptyContext)-doWhnf sig e = runErrorT (runReaderT (runStateT (whnf emptyEnv e >>= whnfClos) (initWithSig sig)) emptyContext)+doNf sig e = runExceptT (runReaderT (runStateT (whnf emptyEnv e >>= reify) (initWithSig sig)) emptyContext)+doWhnf sig e = runExceptT (runReaderT (runStateT (whnf emptyEnv e >>= whnfClos) (initWithSig sig)) emptyContext)   -- top-level functions -------------------------------------------  runTypeCheck :: TCState -> TypeCheck a -> IO (Either TraceError (a,TCState))-runTypeCheck st tc = runErrorT (runReaderT (runStateT tc st) emptyContext)+runTypeCheck st tc = runExceptT (runReaderT (runStateT tc st) emptyContext) -- runTypeCheck st tc = runCallStackT (runReaderT (runStateT tc st) emptyContext) []  typeCheck dl = runTypeCheck initSt (typeCheckDecls dl)@@ -130,7 +129,7 @@   r <- (typeCheckDecls ds >> return True) `catchError`         (\ s -> do liftIO $ putStrLn ("block fails as expected, error message:\n" ++ show s)                    return False)-  if r then fail "unexpected success" else do+  if r then throwErrorMsg "unexpected success" else do     put st     return [] @@ -242,7 +241,7 @@   newAssertionHandling Warning $ typeCheckMutualSig d typeCheckMutualSig (OverrideDecl Impredicative [d]) =   goImpredicative $ typeCheckMutualSig d-typeCheckMutualSig d = fail $ "typeCheckMutualSig: panic: unexpected declaration " ++ show d+typeCheckMutualSig d = throwErrorMsg $ "typeCheckMutualSig: panic: unexpected declaration " ++ show d  -- typeCheckMutualBody measured kindCandidate typeCheckMutualBody :: Bool -> Kind -> Declaration -> TypeCheck [EDeclaration]@@ -272,7 +271,7 @@                  -- insert correct polarity annotation if none was there                  pol | pol `elem` [Param,Rec] -> return $ Quant Pi (TBind x $ Domain tSize kSize $ setPol polsz dec) b                  pol | pol == polsz -> return t0-                 pol -> fail $ "sized type " ++ show n ++ " has wrong polarity annotation " ++ show pol ++ " at Size argument, it should be " ++ show polsz+                 pol -> throwErrorMsg $ "sized type " ++ show n ++ " has wrong polarity annotation " ++ show pol ++ " at Size argument, it should be " ++ show polsz              t0 -> return t0            return (params + 1, pos0 ++ [polsz], t)          NotSized -> return (params, pos0, t0)@@ -418,7 +417,7 @@   return (cxt, ps)    where-    errorParamNotPattern e = fail $+    errorParamNotPattern e = throwErrorMsg $       "expected parameter to be a pattern, but I found " ++ show es  -- |@@ -683,7 +682,7 @@              addBind (mapDec (const paramDec) tb) $ do  -- size is parametric in constructor type                Kinded ki t2e <- checkConType' t2                return $ Kinded ki $ Quant Pi (mapDec (const irrelevantDec) tb) t2e -- size is irrelevant in constructor-      _ -> fail $ "checkConType: expecting size quantification, found " ++ show t+      _ -> throwErrorMsg $ "checkConType: expecting size quantification, found " ++ show t  checkConType' :: Expr -> TypeCheck (Kinded Extr) checkConType' t = do@@ -691,7 +690,7 @@   case s of     Set{} -> return kte     CoSet{} -> return kte-    _ -> fail $ "checkConType: type " ++ show t ++ " of constructor not a universe"+    _ -> throwErrorMsg $ "checkConType: type " ++ show t ++ " of constructor not a universe"  -- check that the data type and the parameter arguments (written down like declared in telescope) -- precondition: target tg type checks in current context@@ -704,7 +703,7 @@       enter ("checking datatype parameters in constructor target") $         leqVals' N mixed (One dv) (take (size tel) vs) telvs       return ()-    _ -> fail $ "constructor should produce something in data type " ++ show d+    _ -> throwErrorMsg $ "constructor should produce something in data type " ++ show d  {- RETIRED (syntactic check) checkTarget :: Name -> Telescope -> Type -> TypeCheck ()@@ -1263,7 +1262,7 @@   let parametric = checkingConType cxt  -- are we dealing with a parametric pi?   let err = "ptsRule " ++ show (s1,s2) ++ " " ++ (if parametric then "(in type of constructor)" else "") ++ ": "   case (s1,s2) of-    (Set VInfty,_) -> fail $ err ++ "domain too big"+    (Set VInfty,_) -> throwErrorMsg $ err ++ "domain too big"     (Set v1, Set v2) ->       if parametric then do          unless er $ leqSize Pos v1 v2 -- when we are checking a constructor, to reject@@ -1273,15 +1272,15 @@     (CoSet v1, Set VZero)        | parametric   -> return $ CoSet v1        | v1 == VInfty -> return $ Set VZero-       | otherwise    -> fail $ err ++ "domain cannot be sized"+       | otherwise    -> throwErrorMsg $ err ++ "domain cannot be sized"     (CoSet v1, CoSet v2)        | parametric   -> do            let v2' = maybe v2 id $ predSize v2            case minSize v1 v2 of              Just v  -> return $ CoSet v-             Nothing -> fail $ err ++ "min" ++ show (v1,v2) ++ " does not exist"+             Nothing -> throwErrorMsg $ err ++ "min" ++ show (v1,v2) ++ " does not exist"        | v1 == VInfty -> return $ CoSet $ succSize v2-       | otherwise    -> fail $ err ++ "domain cannot be sized"+       | otherwise    -> throwErrorMsg $ err ++ "domain cannot be sized"     _ -> return s2  checkOrInfer :: Dec -> Expr -> Maybe Type -> TypeCheck (TVal, EType, Kinded Extr)@@ -1302,7 +1301,7 @@   (sv, te) <- inferExpr t   case sv of     VSort s | not (s `elem` map SortC [Tm,Size]) -> return (s,te)-    _ -> fail $ "inferExpr: expected " ++ show t ++ " to be a type!"+    _ -> throwErrorMsg $ "inferExpr: expected " ++ show t ++ " to be a type!"  -- inferExpr e = (tv, s, ee) -- input : expr e | inferable e@@ -1380,9 +1379,9 @@         let dec = decor item         let pol = polarity dec         if erased dec then-          fail $ err ++ ", because it is marked as erased"+          throwErrorMsg $ err ++ ", because it is marked as erased"          else if not (leqPol pol SPos) then-          fail $ err ++ ", because it has polarity " ++ show pol+          throwErrorMsg $ err ++ ", because it has polarity " ++ show pol          else do            -- traceCheckM ("infer variable " ++ x ++ " : " ++ show  (typ item))            return $ (typ item, Var x) -- TODO: (typ item, kind item, Var x)@@ -1408,7 +1407,7 @@         checkCon <- asks checkingConType {- TODO         when (checkCon && polarity dec /= Mixed) $-          fail $ "constructor arguments must be declared mixed-variant"+          throwErrorMsg $ "constructor arguments must be declared mixed-variant" -}         (s1, Kinded ki0 t1e) <- (if pisig==Pi then checkingDom else id) $           checkingCon False $ inferType t1 -- switch off parametric Pi@@ -1579,7 +1578,7 @@       case s of         Set VZero -> return te         CoSet{} -> return te-        _ -> fail $ "expected " ++ show s ++ " to be Set or CoSet _"+        _ -> throwErrorMsg $ "expected " ++ show s ++ " to be Set or CoSet _"  {- -- small type@@ -1620,8 +1619,8 @@         tel <- getContextTele -- TODO!         case (absp,mrhs) of            (True,Nothing) -> return $ Kinded NoKind (Clause tel [pe] Nothing)-           (False,Nothing) -> fail ("missing right hand side in case " ++ showCase cl)-           (True,Just rhs) -> fail ("absurd pattern requires no right hand side in case " ++ showCase cl)+           (False,Nothing) -> throwErrorMsg ("missing right hand side in case " ++ showCase cl)+           (True,Just rhs) -> throwErrorMsg ("absurd pattern requires no right hand side in case " ++ showCase cl)            (False,Just rhs) -> do               -- pv <- whnf' (patternToExpr p) -- DIFFICULT FOR DOT PATTERNS!       --        vp <- patternToVal p -- BUG: INTRODUCES FRESH GENS, BUT THEY HAVE ALREADY BEEN INTRODUCED IN checkPattern@@ -1676,8 +1675,8 @@       tel <- getContextTele -- WRONG TELE, has VGens for DotPs       case (absp,mrhs) of          (True,Nothing) -> return $ Kinded NoKind (Clause tel ple Nothing)-         (False,Nothing) -> fail ("missing right hand side in clause " ++ show cl)-         (True,Just rhs) -> fail ("absurd pattern requires no right hand side in clause " ++ show cl)+         (False,Nothing) -> throwErrorMsg ("missing right hand side in clause " ++ show cl)+         (True,Just rhs) -> throwErrorMsg ("absurd pattern requires no right hand side in clause " ++ show cl)          (False,Just rhs) -> do             Kinded ki rhse <- checkRHS ins rhs tv0             env  <- getEnv@@ -1712,7 +1711,7 @@     VMeasured mu vb -> setMeasure mu $ checkPatterns dec0 flex ins vb pl     VGuard beta vb -> addBoundHyp beta $ checkPatterns dec0 flex ins vb pl {--    VGuard beta vb -> fail $ "checkPattern at type " ++ show v ++ " --- introduction of constraints not supported"+    VGuard beta vb -> throwErrorMsg $ "checkPattern at type " ++ show v ++ " --- introduction of constraints not supported" -}     _ -> case pl of       [] -> do cxt <- ask@@ -1794,7 +1793,7 @@                   co <- asks mutualCo                  when (co /= CoInd) $-                   fail ("successor pattern only allowed in cofun")+                   throwErrorMsg ("successor pattern only allowed in cofun")                   enterDoc (text ("checkPattern " ++ show p ++" : matching on size, checking that target") <+> prettyTCM tv <+> text "ends in correct coinductive sized type") $                    underAbs x domEr fv $ \ i _ bv -> endsInSizedCo i bv@@ -1911,7 +1910,7 @@                  return (flex, ins, cxt', maybeErase $ SizeP e y, xv, False)            AbsurdP -> do-                 when (isFunType av) $ fail ("absurd pattern " ++ show p ++ " does not match function types, like " ++ show av)+                 when (isFunType av) $ throwErrorMsg ("absurd pattern " ++ show p ++ " does not match function types, like " ++ show av)                  cxt' <- ask                  return (MaxMatches 0 av : flex, ins, cxt', maybeErase $ AbsurdP, VIrr, True) {-@@ -1945,7 +1944,7 @@ -}                  (vc,(flex',ins',cxt',vc',ple,pvs,absp)) <- checkConstructorPattern co n pl -                 when (isFunType vc') $ fail ("higher-order matching of pattern " ++ show p ++ " of type " ++ show vc' ++ " not allowed")+                 when (isFunType vc') $ throwErrorMsg ("higher-order matching of pattern " ++ show p ++ " of type " ++ show vc' ++ " not allowed")                  let flexgen = concat $ map (\ g -> case g of                         DotFlex i _ _ -> [i]                         _ -> []) flex'@@ -2040,7 +2039,7 @@       maybeErase p = if erased decEr then ErasedP p else p        checkConstructorPattern co n pl = do-                 when (isFunType av) $ fail ("higher-order matching of pattern " ++ show p ++ " at type " ++ show av ++ " not allowed")+                 when (isFunType av) $ throwErrorMsg ("higher-order matching of pattern " ++ show p ++ " at type " ++ show av ++ " not allowed") -- TODO: ensure that matchings against erased arguments are forced --                 when (erased dec) $ throwErrorMsg $ "checkPattern: cannot match on erased argument " ++ show p ++ " : " ++ show av @@ -2076,7 +2075,7 @@         when (co == CoCons && isJust sz) $ do           let sizep = head pl  -- 2012-01-22: WAS (pl !! nPars)           unless (isDotPattern sizep) $-            fail $ "in pattern " ++ show p  ++ ", coinductive size sub pattern " ++ show sizep ++ " must be dotted"+            throwErrorMsg $ "in pattern " ++ show p  ++ ", coinductive size sub pattern " ++ show sizep ++ " must be dotted"          when (not $ decEr `elem` map Dec [Const,Rec]) $           recoverFail $ "cannot match pattern " ++ show p ++ " against non-computational argument"@@ -2150,7 +2149,7 @@ checkDot :: Substitution -> DotFlex -> TypeCheck () checkDot subst (i,(e,it)) = enter ("dot pattern " ++ show e) $   case (lookup i subst) of-    Nothing -> fail $ "not instantiated"+    Nothing -> throwErrorMsg $ "not instantiated"     Just v -> do       tv <- substitute subst (typ it)       ask >>= \ ce -> traceCheckM ("checking dot pattern " ++ show ce ++ " |- " ++ show e ++ " : " ++ show (decor it) ++ " " ++ show tv)@@ -2325,7 +2324,7 @@       (VQuant Pi x dom fv) -> do         vb   <- app fv v2         instList' (np - 1) (tailPosl posl) flex vb vl1 vl2-instList' np pos flex tv vl1 vl2 = fail $ "internal error: instList' " ++ show (np,pos,flex,tv,vl1,vl2) ++ " not handled"+instList' np pos flex tv vl1 vl2 = throwErrorMsg $ "internal error: instList' " ++ show (np,pos,flex,tv,vl1,vl2) ++ " not handled"  headPosl :: [Pol] -> Pol headPosl [] = mixed@@ -2497,7 +2496,7 @@        VQuant Pi x dom fv | isVSize (typ dom) ->           underAbs x dom fv $ \ k xv bv -> do             szSizeVarUsage n co p k bv-       _ -> fail $ "not a valid sized constructor: expected size quantification"+       _ -> throwErrorMsg $ "not a valid sized constructor: expected size quantification"  szSizeVarUsage :: Name -> Co -> Int -> Int -> TVal -> TypeCheck () szSizeVarUsage n co p i tv = enterDoc (text "szSizeVarUsage of" <+> prettyTCM (VGen i) <+> text "in" <+> prettyTCM tv) $@@ -2637,7 +2636,7 @@ admFunDef co cls tv = do   (cls, inco) <- admClauses cls tv   when (co==CoInd && not (co `elem` inco)) $-    fail $ show tv ++ " is not a type of a cofun" -- ++ if co==Ind then "fun" else "cofun"+    throwErrorMsg $ show tv ++ " is not a type of a cofun" -- ++ if co==Ind then "fun" else "cofun"   return cls  admClauses :: [Clause] -> TVal -> TypeCheck ([Clause], [Co])@@ -2988,7 +2987,7 @@       VApp (VDef (DefId DatK d)) vl -> do          case p of            ProjP n -> return (p, [])-           _ -> fail "admPattern: IMPOSSIBLE: non-projection pattern for record type"+           _ -> throwErrorMsg "admPattern: IMPOSSIBLE: non-projection pattern for record type"       VQuant Pi x dom fv -> underAbs x dom fv $ \ k xv bv -> do   {-          if p is successor pattern@@ -3004,7 +3003,7 @@             else return (UnusableP p, inco)           else return (p, []) -      _ -> fail "admPattern: IMPOSSIBLE: pattern for a non-function type"+      _ -> throwErrorMsg "admPattern: IMPOSSIBLE: pattern for a non-function type"  cannotMatchDeep p tv = recoverFailDoc $   text "cannot match against deep successor pattern"@@ -3297,6 +3296,6 @@                       do s <- whnfClos $ vl !! p                          case s of                            VGen i' | i == i' -> return ()-                           _ -> fail $ "expected size variable"-                  _ -> fail $ "expected (co)inductive sized type"-         _ -> fail $ "expected (co)inductive sized type"+                           _ -> throwErrorMsg $ "expected size variable"+                  _ -> throwErrorMsg $ "expected (co)inductive sized type"+         _ -> throwErrorMsg $ "expected (co)inductive sized type"
Util.hs view
@@ -7,6 +7,7 @@ import Prelude hiding (showList, null)  import Control.Applicative hiding (empty)+import Control.Monad import Control.Monad.Writer (Writer, runWriter, All, getAll)  import qualified Data.List as List@@ -68,9 +69,15 @@ (<.>) :: Functor m => (b -> c) -> (a -> m b) -> a -> m c (f <.> g) a = f <$> g a -liftMaybe :: (Monad m) => Maybe a -> m a-liftMaybe = maybe (fail "Util.liftMaybe: unexpected Nothing") return+whenM :: Monad m => m Bool -> m () -> m ()+whenM mb k = mb >>= (`when` k) +unlessM :: Monad m => m Bool -> m () -> m ()+unlessM mb k = mb >>= (`unless` k)++whenJustM :: (Monad m) => m (Maybe a) -> (a -> m ()) -> m ()+whenJustM mm k = mm >>= (`whenJust` k)+ whenJust :: (Monad m) => Maybe a -> (a -> m ()) -> m () whenJust (Just a) k = k a whenJust Nothing  k = return ()@@ -85,9 +92,6 @@ ifJustM :: (Monad m) => m (Maybe a) -> (a -> m b) -> m b -> m b ifJustM mma f mb = maybe mb f =<< mma -lookupM :: (Monad m, Show k, Ord k) => k -> Map k v -> m v-lookupM k m = maybe (fail $ "lookupM: unbound key " ++ show k) return $ Map.lookup k m- mapMapM :: (Monad m, Ord k) => (a -> m b) -> Map k a -> m (Map k b) mapMapM f = Map.foldrWithKey step (return $ Map.empty)   where step k a m = do a' <- f a@@ -164,10 +168,6 @@ headMaybe :: [a] -> Maybe a headMaybe [] = Nothing headMaybe (a:as) = Just a--headM :: Monad m => [a] -> m a-headM [] = fail "headM"-headM (a:as) = return a  firstJust :: [Maybe a] -> Maybe a firstJust = headMaybe . compressMaybes
Value.hs view
@@ -167,9 +167,6 @@ vApp f vs = VApp f vs -} -failValInv :: (Monad m) => Val -> m a-failValInv v = fail $ "internal error: value " ++ show v ++ " violates representation invariant"- vAbs :: Name -> Int -> Val -> FVal vAbs x i v = VAbs x i v emptyVal
+ test/succeed/AgdaIssue1052.ma view
@@ -0,0 +1,49 @@++data Eq [A : Set] (a : A) (b : A) : Set+{ refl : Eq A a a }++fun X : Set {}+fun f : X -> X {}++data StepsTo (x, z : X) : Set+{ done : StepsTo x x+; next : (y : X) -> Eq X (f y) z -> StepsTo x y -> StepsTo x z+}++fun trans : (x, y, z : X) -> StepsTo x y -> StepsTo y z -> StepsTo x z+{ trans x y .y p done          = p+; trans x y  z p (next z' r q) = next z' r (trans x y z' p q)+}++fun const : (x, y : X) -> StepsTo x y -> Eq X (f x) x -> Eq X x y+{ const x .x done q = refl+-- ; const _ _  (next _ r p) q = -- TODO+}++{-+fun bad : (x, y, z : X) -> StepsTo x z -> Eq X (f z) x -> StepsTo x y -> StepsTo y x+{ bad x y z (next z' p q) r s =+  next z r (bad z y _ (trans _ _ _ (next _ r done) q) p (trans _ _ _ (next _ r done) s))+}  -- Giving up, need unification!!++-}+{-+data _=⟨_⟩⇒*_ {X : Set}(x : X)(f : X → X) : X → Set where+  done : x =⟨ f ⟩⇒* x+  next : ∀{y z} → f y ≡ z → x =⟨ f ⟩⇒* y → x =⟨ f ⟩⇒* z++trans* : ∀{X}{x y z}{f : X → X} → x =⟨ f ⟩⇒* y → y =⟨ f ⟩⇒* z → x =⟨ f ⟩⇒* z+trans* p done = p+trans* p (next r q) = next r (trans* p q)++const* : ∀{X}{x y}{f : X → X} → x =⟨ f ⟩⇒* y → f x ≡ x → x ≡ y+const* done q = refl+const* (next r p) q with const* p q+const* (next r p) q | refl = trans (sym q) r++bad : ∀{X}{x y z}{f : X → X} → x =⟨ f ⟩⇒* z → f z ≡ x → x =⟨ f ⟩⇒* y →+      y =⟨ f ⟩⇒* x+bad done p q rewrite const* q p = done+bad (next p q) r s =+  next r (bad (trans* (next r done) q) p (trans* (next r done) s))+-}