Safe Haskell	None
Language	Haskell98

TraceError

Documentation

data TraceError Source #

Constructors

Err String
TrErr String TraceError

Instances

Instances details

MonadCxt TypeCheck Source #
Instance details Defined in TCM Methods newVar :: Name -> OneOrTwo Domain -> (Int -> OneOrTwo Val -> TypeCheck a) -> TypeCheck a Source # newWithGen :: Name -> Domain -> (Int -> Val -> TypeCheck a) -> TypeCheck a Source # new2WithGen :: Name -> (Domain, Domain) -> (Int -> (Val, Val) -> TypeCheck a) -> TypeCheck a Source # new :: Name -> Domain -> (Val -> TypeCheck a) -> TypeCheck a Source # new2 :: Name -> (Domain, Domain) -> ((Val, Val) -> TypeCheck a) -> TypeCheck a Source # new' :: Name -> Domain -> TypeCheck a -> TypeCheck a Source # newIrr :: Name -> TypeCheck a -> TypeCheck a Source # addName :: Name -> (Val -> TypeCheck a) -> TypeCheck a Source # addKindedTypeSigs :: [Kinded (TySig TVal)] -> TypeCheck a -> TypeCheck a Source # setType :: Int -> Domain -> TypeCheck a -> TypeCheck a Source # setTypeOfName :: Name -> Domain -> TypeCheck a -> TypeCheck a Source # genOfName :: Name -> TypeCheck Int Source # nameOfGen :: Int -> TypeCheck Name Source # uniqueName :: Name -> Int -> TypeCheck Name Source # lookupGen :: Int -> TypeCheck CxtEntry Source # lookupGenType2 :: Int -> TypeCheck (TVal, TVal) Source # lookupName :: Name -> TypeCheck CxtEntry Source # lookupName1 :: Name -> TypeCheck CxtEntry1 Source # getContextTele :: TypeCheck TeleVal Source # getLen :: TypeCheck Int Source # getEnv :: TypeCheck Env Source # getRen :: TypeCheck Ren Source # applyDec :: Dec -> TypeCheck a -> TypeCheck a Source # resurrect :: TypeCheck a -> TypeCheck a Source # addRewrite :: Rewrite -> [Val] -> ([Val] -> TypeCheck a) -> TypeCheck a Source # addPattern :: TVal -> Pattern -> Env -> (TVal -> Val -> Env -> TypeCheck a) -> TypeCheck a Source # addPatterns :: TVal -> [Pattern] -> Env -> (TVal -> [Val] -> Env -> TypeCheck a) -> TypeCheck a Source # addSizeRel :: Int -> Int -> Int -> TypeCheck a -> TypeCheck a Source # addBelowInfty :: Int -> TypeCheck a -> TypeCheck a Source # addBoundHyp :: Bound Val -> TypeCheck a -> TypeCheck a Source # isBelowInfty :: Int -> TypeCheck Bool Source # sizeVarBelow :: Int -> Int -> TypeCheck (Maybe Int) Source # getMinSize :: Int -> TypeCheck (Maybe Int) Source # getSizeVarsInScope :: TypeCheck [Name] Source # checkingCon :: Bool -> TypeCheck a -> TypeCheck a Source # checkingDom :: TypeCheck a -> TypeCheck a Source # setCo :: Co -> TypeCheck a -> TypeCheck a Source # installFuns :: Co -> [Kinded Fun] -> TypeCheck a -> TypeCheck a Source # setMeasure :: Measure Val -> TypeCheck a -> TypeCheck a Source # activateFuns :: TypeCheck a -> TypeCheck a Source # goImpredicative :: TypeCheck a -> TypeCheck a Source # checkingMutual :: Maybe DefId -> TypeCheck a -> TypeCheck a Source #
MonadMeta TypeCheck Source #
Instance details Defined in TCM Methods resetConstraints :: TypeCheck () Source # mkConstraint :: Val -> Val -> TypeCheck (Maybe Constraint) Source # addMeta :: Ren -> MVar -> TypeCheck () Source # addLeq :: Val -> Val -> TypeCheck () Source # addLe :: LtLe -> Val -> Val -> TypeCheck () Source # solveConstraints :: TypeCheck Solution Source # solveAndModify :: [Expr] -> Env -> TypeCheck [Expr] Source #
MonadSig TypeCheck Source #
Instance details Defined in TCM Methods lookupSymbTypQ :: QName -> TypeCheck TVal Source # lookupSymbQ :: QName -> TypeCheck SigDef Source # addSigQ :: QName -> SigDef -> TypeCheck () Source # modifySigQ :: QName -> (SigDef -> SigDef) -> TypeCheck () Source # setExtrTypQ :: QName -> Expr -> TypeCheck () Source # lookupSymbTyp :: Name -> TypeCheck TVal Source # lookupSymb :: Name -> TypeCheck SigDef Source # addSig :: Name -> SigDef -> TypeCheck () Source # modifySig :: Name -> (SigDef -> SigDef) -> TypeCheck () Source # setExtrTyp :: Name -> Expr -> TypeCheck () Source #
MonadAssert TypeCheck Source #
Instance details Defined in TCM Methods assert :: Bool -> String -> TypeCheck () Source # assertDoc :: Bool -> TypeCheck Doc -> TypeCheck () Source # newAssertionHandling :: AssertionHandling -> TypeCheck a -> TypeCheck a Source # recoverFail :: String -> TypeCheck () Source # recoverFailDoc :: TypeCheck Doc -> TypeCheck () Source #
Show TraceError Source #
Instance details Defined in TraceError Methods showsPrec :: Int -> TraceError -> ShowS # show :: TraceError -> String # showList :: [TraceError] -> ShowS #
Monoid (TypeCheck Bool) Source #
Instance details Defined in Eval Methods mempty :: TypeCheck Bool # mappend :: TypeCheck Bool -> TypeCheck Bool -> TypeCheck Bool # mconcat :: [TypeCheck Bool] -> TypeCheck Bool #
Semigroup (TypeCheck Bool) Source #
Instance details Defined in Eval Methods (<>) :: TypeCheck Bool -> TypeCheck Bool -> TypeCheck Bool # sconcat :: NonEmpty (TypeCheck Bool) -> TypeCheck Bool # stimes :: Integral b => b -> TypeCheck Bool -> TypeCheck Bool #

throwErrorMsg :: MonadError TraceError m => String -> m a Source #

newErrorMsg :: MonadError TraceError m => m a -> String -> m a Source #

throwTrace :: MonadError TraceError m => m a -> String -> m a Source #

enter :: MonadError TraceError m => String -> m a -> m a Source #

enterTrace :: MonadError TraceError m => String -> m a -> m a Source #

enterShow :: (MonadError TraceError m, Show a) => a -> m b -> m b Source #

enterDoc :: (MonadError TraceError m, Pretty d) => m d -> m a -> m a Source #

failDoc :: MonadError TraceError m => m Doc -> m a Source #

newErrorDoc :: MonadError TraceError m => m a -> m Doc -> m a Source #

errorToMaybe :: MonadError e m => m a -> m (Maybe a) Source #

errorToBool :: MonadError e m => m () -> m Bool Source #

boolToErrorDoc :: MonadError TraceError m => m Doc -> Bool -> m () Source #

boolToError :: MonadError TraceError m => String -> Bool -> m () Source #

orM :: MonadError e m => m a -> m a -> m a Source #

data AssertionHandling Source #

Constructors

Failure
Warning
Ignore

Instances

Instances details

Show AssertionHandling Source #
Instance details Defined in TraceError Methods showsPrec :: Int -> AssertionHandling -> ShowS # show :: AssertionHandling -> String # showList :: [AssertionHandling] -> ShowS #
Eq AssertionHandling Source #
Instance details Defined in TraceError Methods (==) :: AssertionHandling -> AssertionHandling -> Bool # (/=) :: AssertionHandling -> AssertionHandling -> Bool #
Ord AssertionHandling Source #
Instance details Defined in TraceError Methods compare :: AssertionHandling -> AssertionHandling -> Ordering # (<) :: AssertionHandling -> AssertionHandling -> Bool # (<=) :: AssertionHandling -> AssertionHandling -> Bool # (>) :: AssertionHandling -> AssertionHandling -> Bool # (>=) :: AssertionHandling -> AssertionHandling -> Bool # max :: AssertionHandling -> AssertionHandling -> AssertionHandling # min :: AssertionHandling -> AssertionHandling -> AssertionHandling #

assert' :: (MonadError TraceError m, MonadIO m) => AssertionHandling -> Bool -> String -> m () Source #

assertDoc' :: (MonadError TraceError m, MonadIO m) => AssertionHandling -> Bool -> m Doc -> m () Source #

class Monad m => MonadAssert (m :: Type -> Type) where Source #

Minimal complete definition

assert, newAssertionHandling

Methods

assert :: Bool -> String -> m () Source #

assertDoc :: Bool -> m Doc -> m () Source #

newAssertionHandling :: AssertionHandling -> m a -> m a Source #

recoverFail :: String -> m () Source #

recoverFailDoc :: m Doc -> m () Source #

Instances

Instances details

MonadAssert TypeCheck Source #
Instance details Defined in TCM Methods assert :: Bool -> String -> TypeCheck () Source # assertDoc :: Bool -> TypeCheck Doc -> TypeCheck () Source # newAssertionHandling :: AssertionHandling -> TypeCheck a -> TypeCheck a Source # recoverFail :: String -> TypeCheck () Source # recoverFailDoc :: TypeCheck Doc -> TypeCheck () Source #