Safe Haskell	None
Language	Haskell98

Language.Fixpoint.Types.Errors

Contents

Concrete Location Type
Result
Abstract Error Type
Constructor
Accessors
Adding Insult to Injury
Fatal Exit
Some popular errors
Orphan instances

Synopsis

Concrete Location Type

data SrcSpan Source #

A Reusable SrcSpan Type ------------------------------------------

Constructors

SS
Fields sp_start :: !SourcePos sp_stop :: !SourcePos

Instances

Eq SrcSpan Source #
Methods (==) :: SrcSpan -> SrcSpan -> Bool # (/=) :: SrcSpan -> SrcSpan -> Bool #
Data SrcSpan Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SrcSpan -> c SrcSpan # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SrcSpan # toConstr :: SrcSpan -> Constr # dataTypeOf :: SrcSpan -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c SrcSpan) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SrcSpan) # gmapT :: (forall b. Data b => b -> b) -> SrcSpan -> SrcSpan # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SrcSpan -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SrcSpan -> r # gmapQ :: (forall d. Data d => d -> u) -> SrcSpan -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> SrcSpan -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> SrcSpan -> m SrcSpan # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SrcSpan -> m SrcSpan # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SrcSpan -> m SrcSpan #
Ord SrcSpan Source #
Methods compare :: SrcSpan -> SrcSpan -> Ordering # (<) :: SrcSpan -> SrcSpan -> Bool # (<=) :: SrcSpan -> SrcSpan -> Bool # (>) :: SrcSpan -> SrcSpan -> Bool # (>=) :: SrcSpan -> SrcSpan -> Bool # max :: SrcSpan -> SrcSpan -> SrcSpan # min :: SrcSpan -> SrcSpan -> SrcSpan #
Show SrcSpan Source #
Methods showsPrec :: Int -> SrcSpan -> ShowS # show :: SrcSpan -> String # showList :: [SrcSpan] -> ShowS #
Generic SrcSpan Source #
Associated Types type Rep SrcSpan :: * -> * # Methods from :: SrcSpan -> Rep SrcSpan x # to :: Rep SrcSpan x -> SrcSpan #
Serialize SrcSpan Source #
Methods put :: Putter SrcSpan # get :: Get SrcSpan #
Hashable SrcSpan Source #
Methods hashWithSalt :: Int -> SrcSpan -> Int # hash :: SrcSpan -> Int #
PPrint SrcSpan Source #
Methods pprintTidy :: Tidy -> SrcSpan -> Doc Source # pprintPrec :: Int -> Tidy -> SrcSpan -> Doc Source #
type Rep SrcSpan Source #
type Rep SrcSpan = D1 (MetaData "SrcSpan" "Language.Fixpoint.Types.Spans" "liquid-fixpoint-0.7.0.2-3repHVQ2bkqGganvJ6cFNP" False) (C1 (MetaCons "SS" PrefixI True) ((:*:) (S1 (MetaSel (Just Symbol "sp_start") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 SourcePos)) (S1 (MetaSel (Just Symbol "sp_stop") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 SourcePos))))

dummySpan :: SrcSpan Source #

sourcePosElts :: SourcePos -> (SourceName, Line, Column) Source #

Result

data FixResult a Source #

Result ---------------------------------------------------------

Constructors

Crash [a] String
Safe
Unsafe ![a]

Instances

Functor FixResult Source #
Methods fmap :: (a -> b) -> FixResult a -> FixResult b # (<$) :: a -> FixResult b -> FixResult a #
Foldable FixResult Source #
Methods fold :: Monoid m => FixResult m -> m # foldMap :: Monoid m => (a -> m) -> FixResult a -> m # foldr :: (a -> b -> b) -> b -> FixResult a -> b # foldr' :: (a -> b -> b) -> b -> FixResult a -> b # foldl :: (b -> a -> b) -> b -> FixResult a -> b # foldl' :: (b -> a -> b) -> b -> FixResult a -> b # foldr1 :: (a -> a -> a) -> FixResult a -> a # foldl1 :: (a -> a -> a) -> FixResult a -> a # toList :: FixResult a -> [a] # null :: FixResult a -> Bool # length :: FixResult a -> Int # elem :: Eq a => a -> FixResult a -> Bool # maximum :: Ord a => FixResult a -> a # minimum :: Ord a => FixResult a -> a # sum :: Num a => FixResult a -> a # product :: Num a => FixResult a -> a #
Traversable FixResult Source #
Methods traverse :: Applicative f => (a -> f b) -> FixResult a -> f (FixResult b) # sequenceA :: Applicative f => FixResult (f a) -> f (FixResult a) # mapM :: Monad m => (a -> m b) -> FixResult a -> m (FixResult b) # sequence :: Monad m => FixResult (m a) -> m (FixResult a) #
Eq a => Eq (FixResult a) Source #
Methods (==) :: FixResult a -> FixResult a -> Bool # (/=) :: FixResult a -> FixResult a -> Bool #
Data a => Data (FixResult a) Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FixResult a -> c (FixResult a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (FixResult a) # toConstr :: FixResult a -> Constr # dataTypeOf :: FixResult a -> DataType # dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c (FixResult a)) # dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (FixResult a)) # gmapT :: (forall b. Data b => b -> b) -> FixResult a -> FixResult a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FixResult a -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FixResult a -> r # gmapQ :: (forall d. Data d => d -> u) -> FixResult a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> FixResult a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> FixResult a -> m (FixResult a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FixResult a -> m (FixResult a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FixResult a -> m (FixResult a) #
Show a => Show (FixResult a) Source #
Methods showsPrec :: Int -> FixResult a -> ShowS # show :: FixResult a -> String # showList :: [FixResult a] -> ShowS #
Generic (FixResult a) Source #
Associated Types type Rep (FixResult a) :: * -> * # Methods from :: FixResult a -> Rep (FixResult a) x # to :: Rep (FixResult a) x -> FixResult a #
Monoid (FixResult a) Source #
Methods mempty :: FixResult a # mappend :: FixResult a -> FixResult a -> FixResult a # mconcat :: [FixResult a] -> FixResult a #
Exception (FixResult Error) Source #
Methods toException :: FixResult Error -> SomeException # fromException :: SomeException -> Maybe (FixResult Error) # displayException :: FixResult Error -> String #
Binary a => Binary (FixResult a) Source #
Methods put :: FixResult a -> Put # get :: Get (FixResult a) # putList :: [FixResult a] -> Put #
Serialize (FixResult Error) Source #
Methods put :: Putter (FixResult Error) # get :: Get (FixResult Error) #
NFData a => NFData (FixResult a) Source #
Methods rnf :: FixResult a -> () #
(Ord a, Fixpoint a) => Fixpoint (FixResult (SubC a)) Source #
Methods toFix :: FixResult (SubC a) -> Doc Source # simplify :: FixResult (SubC a) -> FixResult (SubC a) Source #
Inputable (FixResult Integer) Source #
Methods rr :: String -> FixResult Integer Source # rr' :: String -> String -> FixResult Integer Source #
Inputable (FixResult Integer, FixSolution) Source #
Methods rr :: String -> (FixResult Integer, FixSolution) Source # rr' :: String -> String -> (FixResult Integer, FixSolution) Source #
type Rep (FixResult a) Source #
type Rep (FixResult a) = D1 (MetaData "FixResult" "Language.Fixpoint.Types.Errors" "liquid-fixpoint-0.7.0.2-3repHVQ2bkqGganvJ6cFNP" False) ((:+:) (C1 (MetaCons "Crash" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [a])) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)))) ((:+:) (C1 (MetaCons "Safe" PrefixI False) U1) (C1 (MetaCons "Unsafe" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [a])))))

colorResult :: FixResult a -> Moods Source #

resultDoc :: Fixpoint a => FixResult a -> Doc Source #

Abstract Error Type

data Error Source #

A BareBones Error Type ----------------------------------------------------

Instances

Eq Error Source #
Methods (==) :: Error -> Error -> Bool # (/=) :: Error -> Error -> Bool #
Ord Error Source #
Methods compare :: Error -> Error -> Ordering # (<) :: Error -> Error -> Bool # (<=) :: Error -> Error -> Bool # (>) :: Error -> Error -> Bool # (>=) :: Error -> Error -> Bool # max :: Error -> Error -> Error # min :: Error -> Error -> Error #
Show Error Source #
Methods showsPrec :: Int -> Error -> ShowS # show :: Error -> String # showList :: [Error] -> ShowS #
Generic Error Source #
Associated Types type Rep Error :: * -> * # Methods from :: Error -> Rep Error x # to :: Rep Error x -> Error #
Exception Error Source #
Methods toException :: Error -> SomeException # fromException :: SomeException -> Maybe Error # displayException :: Error -> String #
Serialize Error Source #
Methods put :: Putter Error # get :: Get Error #
PPrint Error Source #
Methods pprintTidy :: Tidy -> Error -> Doc Source # pprintPrec :: Int -> Tidy -> Error -> Doc Source #
Exception (FixResult Error) Source #
Methods toException :: FixResult Error -> SomeException # fromException :: SomeException -> Maybe (FixResult Error) # displayException :: FixResult Error -> String #
Serialize (FixResult Error) Source #
Methods put :: Putter (FixResult Error) # get :: Get (FixResult Error) #
type Rep Error Source #
type Rep Error

Constructor

err :: SrcSpan -> Doc -> Error Source #

Accessors

errLoc :: Error1 -> SrcSpan Source #

errMsg :: Error1 -> Doc Source #

Adding Insult to Injury

catError :: Error -> Error -> Error Source #

catErrors :: ListNE Error -> Error Source #

Fatal Exit

panic :: String -> a Source #

die :: Error -> a Source #

dieAt :: SrcSpan -> Error -> a Source #

exit :: a -> IO a -> IO a Source #

Some popular errors

errFreeVarInQual :: (PPrint q, Loc q, PPrint x) => q -> x -> Error Source #

Catalogue of Errors --------------------------------------------

errFreeVarInConstraint :: PPrint a => (Integer, a) -> Error Source #

errIllScopedKVar :: (PPrint k, PPrint bs) => (k, Integer, Integer, bs) -> Error Source #

Orphan instances

Serialize Doc Source #
Methods put :: Putter Doc # get :: Get Doc #
Serialize TextDetails Source #
Methods put :: Putter TextDetails # get :: Get TextDetails #
Generic (AnnotDetails a) Source #
Associated Types type Rep (AnnotDetails a) :: * -> * # Methods from :: AnnotDetails a -> Rep (AnnotDetails a) x # to :: Rep (AnnotDetails a) x -> AnnotDetails a #
Serialize a => Serialize (Doc a) Source #
Methods put :: Putter (Doc a) # get :: Get (Doc a) #
Serialize a => Serialize (AnnotDetails a) Source #
Methods put :: Putter (AnnotDetails a) # get :: Get (AnnotDetails a) #