liquid-fixpoint-0.7.0.5: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver

Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Types.Errors

Contents

Synopsis

Concrete Location Type

data SrcSpan Source #

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

Constructors

SS 

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 # 
Show SrcSpan Source # 
Generic SrcSpan Source # 

Associated Types

type Rep SrcSpan :: * -> * #

Methods

from :: SrcSpan -> Rep SrcSpan x #

to :: Rep SrcSpan x -> SrcSpan #

Serialize SrcSpan Source # 
Hashable SrcSpan Source # 

Methods

hashWithSalt :: Int -> SrcSpan -> Int #

hash :: SrcSpan -> Int #

PPrint SrcSpan Source # 
type Rep SrcSpan Source # 
type Rep SrcSpan = D1 (MetaData "SrcSpan" "Language.Fixpoint.Types.Spans" "liquid-fixpoint-0.7.0.5-Gva8geyEo6wB3a0li3tGtO" 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))))

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 # 
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 # 
Exception (FixResult Error) Source # 
Binary a => Binary (FixResult a) Source # 

Methods

put :: FixResult a -> Put #

get :: Get (FixResult a) #

putList :: [FixResult a] -> Put #

Serialize (FixResult Error) Source # 
NFData a => NFData (FixResult a) Source # 

Methods

rnf :: FixResult a -> () #

(Ord a, Fixpoint a) => Fixpoint (FixResult (SubC a)) Source # 
Inputable (FixResult Integer) Source # 
Inputable (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.5-Gva8geyEo6wB3a0li3tGtO" 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])))))

Abstract Error Type

Constructor

Accessors

errLoc :: Error1 -> SrcSpan Source #

errMsg :: Error1 -> Doc Source #

Adding Insult to Injury

Fatal Exit

die :: 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 --------------------------------------------

Orphan instances