Safe Haskell	Safe-Inferred
Language	Haskell98

Language.Fixpoint.Types.Errors

Contents

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

Synopsis

data SrcSpan = SS {
- sp_start :: !SourcePos
- sp_stop :: !SourcePos
}
dummySpan :: SrcSpan
sourcePosElts :: SourcePos -> (SourceName, Line, Column)
data FixResult a
- = Crash [(a, Maybe String)] String
- | Unsafe Stats ![a]
- | Safe Stats
colorResult :: FixResult a -> Moods
resultDoc :: Fixpoint a => FixResult a -> Doc
resultExit :: FixResult a -> ExitCode
data Error
data Error1
err :: SrcSpan -> Doc -> Error
errLoc :: Error1 -> SrcSpan
errMsg :: Error1 -> Doc
errs :: Error -> [Error1]
catError :: Error -> Error -> Error
catErrors :: ListNE Error -> Error
panic :: String -> a
die :: Error -> a
dieAt :: SrcSpan -> Error -> a
exit :: a -> IO a -> IO a
errFreeVarInQual :: (PPrint q, Loc q, PPrint x) => q -> x -> Error
errFreeVarInConstraint :: PPrint a => (Integer, a) -> Error
errIllScopedKVar :: (PPrint k, PPrint bs) => (k, Integer, Integer, bs) -> Error
errBadDataDecl :: (Loc x, PPrint x) => x -> Error

Concrete Location Type

data SrcSpan Source #

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

Constructors

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

Instances

Instances details

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 :: forall r r'. (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 #
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 #
Show SrcSpan Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods showsPrec :: Int -> SrcSpan -> ShowS # show :: SrcSpan -> String # showList :: [SrcSpan] -> ShowS #
Binary SrcSpan Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods put :: SrcSpan -> Put # get :: Get SrcSpan # putList :: [SrcSpan] -> Put #
Serialize SrcSpan Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods put :: Putter SrcSpan # get :: Get SrcSpan #
NFData SrcSpan Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods rnf :: SrcSpan -> () #
Eq SrcSpan Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods (==) :: SrcSpan -> SrcSpan -> Bool # (/=) :: SrcSpan -> SrcSpan -> Bool #
Ord SrcSpan Source #
Instance details Defined in Language.Fixpoint.Types.Spans 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 #
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 Methods pprintTidy :: Tidy -> SrcSpan -> Doc Source # pprintPrec :: Int -> Tidy -> SrcSpan -> Doc Source #
Loc SrcSpan Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods srcSpan :: SrcSpan -> SrcSpan Source #
Store SrcSpan Source #
Instance details Defined in Language.Fixpoint.Types.Spans Methods size :: Size SrcSpan # poke :: SrcSpan -> Poke () # peek :: Peek SrcSpan #
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.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" '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)))

dummySpan :: SrcSpan Source #

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

Result

data FixResult a Source #

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

Constructors

Crash [(a, Maybe String)] String
Unsafe Stats ![a]
Safe Stats	The `Solver` statistics, which include also the constraints actually checked. A program will be "trivially safe" in case this number is 0.

Instances

Instances details

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 # 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) #
Functor FixResult Source #
Instance details Defined in Language.Fixpoint.Types.Errors Methods fmap :: (a -> b) -> FixResult a -> FixResult b # (<$) :: a -> FixResult b -> FixResult a #
ToJSON a => ToJSON (FixResult a) Source #
Instance details Defined in Language.Fixpoint.Types.Errors Methods toJSON :: FixResult a -> Value # toEncoding :: FixResult a -> Encoding # toJSONList :: [FixResult a] -> Value # toEncodingList :: [FixResult a] -> Encoding #
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 :: forall r r'. (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) #
Monoid (FixResult a) Source #
Instance details Defined in Language.Fixpoint.Types.Errors Methods mempty :: FixResult a # mappend :: FixResult a -> FixResult a -> FixResult a # mconcat :: [FixResult a] -> 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 #
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 #
Show a => Show (FixResult a) Source #
Instance details Defined in Language.Fixpoint.Types.Errors Methods showsPrec :: Int -> FixResult a -> ShowS # show :: FixResult a -> String # showList :: [FixResult a] -> ShowS #
Serialize (FixResult Error) Source #
Instance details Defined in Language.Fixpoint.Types.Errors Methods put :: Putter (FixResult Error) # get :: Get (FixResult Error) #
NFData a => NFData (FixResult a) Source #
Instance details Defined in Language.Fixpoint.Types.Errors Methods rnf :: 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 #
Inputable (FixResult Integer) Source #
Instance details Defined in Language.Fixpoint.Parse Methods rr :: String -> FixResult Integer Source # rr' :: String -> String -> FixResult Integer Source #
(Ord a, Fixpoint a) => Fixpoint (FixResult (SubC a)) Source #
Instance details Defined in Language.Fixpoint.Types.Constraints Methods toFix :: FixResult (SubC a) -> Doc Source # simplify :: FixResult (SubC a) -> FixResult (SubC a) Source #
Fixpoint a => PPrint (FixResult a) Source #
Instance details Defined in Language.Fixpoint.Types.Errors Methods pprintTidy :: Tidy -> FixResult a -> Doc Source # pprintPrec :: Int -> Tidy -> FixResult a -> Doc Source #
Store a => Store (FixResult a) Source #
Instance details Defined in Language.Fixpoint.Types.Errors Methods size :: Size (FixResult a) # poke :: FixResult a -> Poke () # peek :: Peek (FixResult a) #
Inputable (FixResult Integer, FixSolution) Source #
Instance details Defined in Language.Fixpoint.Parse Methods rr :: String -> (FixResult Integer, FixSolution) Source # rr' :: String -> String -> (FixResult Integer, FixSolution) Source #
type Rep (FixResult a) Source #
Instance details Defined in Language.Fixpoint.Types.Errors type Rep (FixResult a) = D1 ('MetaData "FixResult" "Language.Fixpoint.Types.Errors" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'False) (C1 ('MetaCons "Crash" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(a, Maybe String)]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: (C1 ('MetaCons "Unsafe" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Stats) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [a])) :+: C1 ('MetaCons "Safe" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Stats))))

colorResult :: FixResult a -> Moods Source #

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

resultExit :: FixResult a -> ExitCode Source #

Error Type

data Error Source #

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

Instances

Instances details

Exception Error Source #
Instance details Defined in Language.Fixpoint.Types.Errors Methods toException :: Error -> SomeException # fromException :: SomeException -> Maybe Error # displayException :: Error -> String #
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 #
Show Error Source #
Instance details Defined in Language.Fixpoint.Types.Errors Methods showsPrec :: Int -> Error -> ShowS # show :: Error -> String # showList :: [Error] -> ShowS #
Serialize Error Source #
Instance details Defined in Language.Fixpoint.Types.Errors Methods put :: Putter Error # get :: Get Error #
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 #
PPrint Error Source #
Instance details Defined in Language.Fixpoint.Types.Errors Methods pprintTidy :: Tidy -> Error -> Doc Source # pprintPrec :: Int -> Tidy -> Error -> Doc Source #
Serialize (FixResult Error) Source #
Instance details Defined in Language.Fixpoint.Types.Errors Methods put :: Putter (FixResult Error) # get :: Get (FixResult Error) #
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.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'True) (C1 ('MetaCons "Error" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Error1])))

data Error1 Source #

Instances

Instances details

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 #
Show Error1 Source #
Instance details Defined in Language.Fixpoint.Types.Errors Methods showsPrec :: Int -> Error1 -> ShowS # show :: Error1 -> String # showList :: [Error1] -> ShowS #
Serialize Error1 Source #
Instance details Defined in Language.Fixpoint.Types.Errors Methods put :: Putter Error1 # get :: Get Error1 #
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 Methods compare :: Error1 -> Error1 -> Ordering # (<) :: Error1 -> Error1 -> Bool # (<=) :: Error1 -> Error1 -> Bool # (>) :: Error1 -> Error1 -> Bool # (>=) :: Error1 -> Error1 -> Bool # max :: Error1 -> Error1 -> Error1 # min :: Error1 -> Error1 -> Error1 #
Fixpoint Error1 Source #
Instance details Defined in Language.Fixpoint.Types.Errors Methods toFix :: Error1 -> Doc Source # simplify :: Error1 -> Error1 Source #
PPrint Error1 Source #
Instance details Defined in Language.Fixpoint.Types.Errors Methods pprintTidy :: Tidy -> Error1 -> Doc Source # pprintPrec :: Int -> Tidy -> Error1 -> Doc Source #
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.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" '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

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

Accessors

errLoc :: Error1 -> SrcSpan Source #

errMsg :: Error1 -> Doc Source #

errs :: Error -> [Error1] 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 #

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

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

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

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

Orphan instances

Serialize TextDetails Source #
Instance details Methods put :: Putter TextDetails # get :: Get TextDetails #
Serialize Doc Source #
Instance details Methods put :: Putter Doc # get :: Get Doc #
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 (AnnotDetails a) Source #
Instance details Methods put :: Putter (AnnotDetails a) # get :: Get (AnnotDetails a) #
Serialize a => Serialize (Doc a) Source #
Instance details Methods put :: Putter (Doc a) # get :: Get (Doc a) #