liquid-fixpoint-0.8.10.2: 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 # 
Instance details

Defined in Language.Fixpoint.Types.Spans

Methods

(==) :: SrcSpan -> SrcSpan -> Bool #

(/=) :: SrcSpan -> SrcSpan -> Bool #

Data SrcSpan Source # 
Instance details

Defined in Language.Fixpoint.Types.Spans

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 # 
Instance details

Defined in Language.Fixpoint.Types.Spans

Show SrcSpan Source # 
Instance details

Defined in Language.Fixpoint.Types.Spans

Generic SrcSpan Source # 
Instance details

Defined in Language.Fixpoint.Types.Spans

Associated Types

type Rep SrcSpan :: Type -> Type #

Methods

from :: SrcSpan -> Rep SrcSpan x #

to :: Rep SrcSpan x -> SrcSpan #

Binary SrcSpan Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

put :: SrcSpan -> Put #

get :: Get SrcSpan #

putList :: [SrcSpan] -> Put #

Serialize SrcSpan Source # 
Instance details

Defined in Language.Fixpoint.Types.Spans

NFData SrcSpan Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Methods

rnf :: SrcSpan -> () #

Hashable SrcSpan Source # 
Instance details

Defined in Language.Fixpoint.Types.Spans

Methods

hashWithSalt :: Int -> SrcSpan -> Int #

hash :: SrcSpan -> Int #

PPrint SrcSpan Source # 
Instance details

Defined in Language.Fixpoint.Types.Spans

Loc SrcSpan Source # 
Instance details

Defined in Language.Fixpoint.Types.Spans

type Rep SrcSpan Source # 
Instance details

Defined in Language.Fixpoint.Types.Spans

type Rep SrcSpan = D1 (MetaData "SrcSpan" "Language.Fixpoint.Types.Spans" "liquid-fixpoint-0.8.10.2-Ld6PWXA9XrKe3HZnOCc57" False) (C1 (MetaCons "SS" PrefixI True) (S1 (MetaSel (Just "sp_start") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 SourcePos) :*: S1 (MetaSel (Just "sp_stop") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 SourcePos)))

Result

data FixResult a Source #

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

Constructors

Crash [a] String 
Safe Stats

The Solver statistics, which include also the constraints actually checked. A program will be "trivially safe" in case this number is 0.

Unsafe Stats ![a] 
Instances
Functor FixResult Source # 
Instance details

Defined in Language.Fixpoint.Types.Errors

Methods

fmap :: (a -> b) -> FixResult a -> FixResult b #

(<$) :: a -> FixResult b -> FixResult a #

Foldable FixResult Source # 
Instance details

Defined in Language.Fixpoint.Types.Errors

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 # 
Instance details

Defined in Language.Fixpoint.Types.Errors

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 # 
Instance details

Defined in Language.Fixpoint.Types.Errors

Methods

(==) :: FixResult a -> FixResult a -> Bool #

(/=) :: FixResult a -> FixResult a -> Bool #

Data a => Data (FixResult a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Errors

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 # 
Instance details

Defined in Language.Fixpoint.Types.Errors

Generic (FixResult a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Errors

Associated Types

type Rep (FixResult a) :: Type -> Type #

Methods

from :: FixResult a -> Rep (FixResult a) x #

to :: Rep (FixResult a) x -> FixResult a #

Semigroup (FixResult a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Errors

Methods

(<>) :: FixResult a -> FixResult a -> FixResult a #

sconcat :: NonEmpty (FixResult a) -> FixResult a #

stimes :: Integral b => b -> FixResult a -> FixResult a #

Monoid (FixResult a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Errors

Exception (FixResult Error) Source # 
Instance details

Defined in Language.Fixpoint.Types.Errors

Binary a => Binary (FixResult a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Errors

Methods

put :: FixResult a -> Put #

get :: Get (FixResult a) #

putList :: [FixResult a] -> Put #

Serialize (FixResult Error) Source # 
Instance details

Defined in Language.Fixpoint.Types.Errors

NFData a => NFData (FixResult a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Errors

Methods

rnf :: FixResult a -> () #

(Ord a, Fixpoint a) => Fixpoint (FixResult (SubC a)) Source # 
Instance details

Defined in Language.Fixpoint.Types.Constraints

Inputable (FixResult Integer) Source # 
Instance details

Defined in Language.Fixpoint.Parse

Inputable (FixResult Integer, FixSolution) Source # 
Instance details

Defined in Language.Fixpoint.Parse

type Rep (FixResult a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Errors

Error Type

data Error Source #

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

Instances
Eq Error Source # 
Instance details

Defined in Language.Fixpoint.Types.Errors

Methods

(==) :: Error -> Error -> Bool #

(/=) :: Error -> Error -> Bool #

Ord Error Source # 
Instance details

Defined in Language.Fixpoint.Types.Errors

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 # 
Instance details

Defined in Language.Fixpoint.Types.Errors

Methods

showsPrec :: Int -> Error -> ShowS #

show :: Error -> String #

showList :: [Error] -> ShowS #

Generic Error Source # 
Instance details

Defined in Language.Fixpoint.Types.Errors

Associated Types

type Rep Error :: Type -> Type #

Methods

from :: Error -> Rep Error x #

to :: Rep Error x -> Error #

Exception Error Source # 
Instance details

Defined in Language.Fixpoint.Types.Errors

Serialize Error Source # 
Instance details

Defined in Language.Fixpoint.Types.Errors

Methods

put :: Putter Error #

get :: Get Error #

PPrint Error Source # 
Instance details

Defined in Language.Fixpoint.Types.Errors

Exception (FixResult Error) Source # 
Instance details

Defined in Language.Fixpoint.Types.Errors

Serialize (FixResult Error) Source # 
Instance details

Defined in Language.Fixpoint.Types.Errors

type Rep Error Source # 
Instance details

Defined in Language.Fixpoint.Types.Errors

type Rep Error = D1 (MetaData "Error" "Language.Fixpoint.Types.Errors" "liquid-fixpoint-0.8.10.2-Ld6PWXA9XrKe3HZnOCc57" True) (C1 (MetaCons "Error" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Error1])))

data Error1 Source #

Instances
Eq Error1 Source # 
Instance details

Defined in Language.Fixpoint.Types.Errors

Methods

(==) :: Error1 -> Error1 -> Bool #

(/=) :: Error1 -> Error1 -> Bool #

Ord Error1 Source # 
Instance details

Defined in Language.Fixpoint.Types.Errors

Show Error1 Source # 
Instance details

Defined in Language.Fixpoint.Types.Errors

Generic Error1 Source # 
Instance details

Defined in Language.Fixpoint.Types.Errors

Associated Types

type Rep Error1 :: Type -> Type #

Methods

from :: Error1 -> Rep Error1 x #

to :: Rep Error1 x -> Error1 #

Serialize Error1 Source # 
Instance details

Defined in Language.Fixpoint.Types.Errors

PPrint Error1 Source # 
Instance details

Defined in Language.Fixpoint.Types.Errors

Fixpoint Error1 Source # 
Instance details

Defined in Language.Fixpoint.Types.Errors

type Rep Error1 Source # 
Instance details

Defined in Language.Fixpoint.Types.Errors

type Rep Error1 = D1 (MetaData "Error1" "Language.Fixpoint.Types.Errors" "liquid-fixpoint-0.8.10.2-Ld6PWXA9XrKe3HZnOCc57" False) (C1 (MetaCons "Error1" PrefixI True) (S1 (MetaSel (Just "errLoc") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 SrcSpan) :*: S1 (MetaSel (Just "errMsg") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Doc)))

Constructor

Accessors

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

Serialize Doc Source # 
Instance details

Methods

put :: Putter Doc #

get :: Get Doc #

Serialize TextDetails Source # 
Instance details

Generic (AnnotDetails a) Source # 
Instance details

Associated Types

type Rep (AnnotDetails a) :: Type -> Type #

Methods

from :: AnnotDetails a -> Rep (AnnotDetails a) x #

to :: Rep (AnnotDetails a) x -> AnnotDetails a #

Serialize a => Serialize (Doc a) Source # 
Instance details

Methods

put :: Putter (Doc a) #

get :: Get (Doc a) #

Serialize a => Serialize (AnnotDetails a) Source # 
Instance details