Language.Fixpoint.Types.Errors

Concrete Location Type

data SrcSpan

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

Constructors

SS

Fields

• sp_start :: !SourcePos
• sp_stop :: !SourcePos

Instances

Eq SrcSpan

Defined in Language.Fixpoint.Types.Spans

Methods

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

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

Data SrcSpan

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

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

Show SrcSpan

Defined in Language.Fixpoint.Types.Spans

Methods

showsPrec :: Int -> SrcSpan -> ShowS

show :: SrcSpan -> String

showList :: [SrcSpan] -> ShowS

Generic SrcSpan

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

Defined in Language.Fixpoint.Types.Refinements

Methods

put :: SrcSpan -> Put

get :: Get SrcSpan

putList :: [SrcSpan] -> Put

Serialize SrcSpan

Defined in Language.Fixpoint.Types.Spans

Methods

put :: Putter SrcSpan

get :: Get SrcSpan

NFData SrcSpan

Defined in Language.Fixpoint.Types.Refinements

Methods

rnf :: SrcSpan -> ()

Hashable SrcSpan

Defined in Language.Fixpoint.Types.Spans

Methods

hashWithSalt :: Int -> SrcSpan -> Int

hash :: SrcSpan -> Int

PPrint SrcSpan

Defined in Language.Fixpoint.Types.Spans

Methods

pprintTidy :: Tidy -> SrcSpan -> Doc

pprintPrec :: Int -> Tidy -> SrcSpan -> Doc

Loc SrcSpan

Defined in Language.Fixpoint.Types.Spans

Methods

srcSpan :: SrcSpan -> SrcSpan

type Rep SrcSpan

Defined in Language.Fixpoint.Types.Spans

type Rep SrcSpan = D1 (MetaData "SrcSpan" "Language.Fixpoint.Types.Spans" "liquid-fixpoint-0.8.0.2-EGSzGwrlcJrCaUaEYLNzOY" 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

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

Result

data FixResult a

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

Defined in Language.Fixpoint.Types.Errors

Methods

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

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

Foldable FixResult

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

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)

Defined in Language.Fixpoint.Types.Errors

Methods

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

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

Data a => Data (FixResult a)

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)

Defined in Language.Fixpoint.Types.Errors

Methods

showsPrec :: Int -> FixResult a -> ShowS

show :: FixResult a -> String

showList :: [FixResult a] -> ShowS

Generic (FixResult a)

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)

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)

Defined in Language.Fixpoint.Types.Errors

Methods

mempty :: FixResult a

mappend :: FixResult a -> FixResult a -> FixResult a

mconcat :: [FixResult a] -> FixResult a

Exception (FixResult Error)

Defined in Language.Fixpoint.Types.Errors

Methods

toException :: FixResult Error -> SomeException

fromException :: SomeException -> Maybe (FixResult Error)

displayException :: FixResult Error -> String

Binary a => Binary (FixResult a)

Defined in Language.Fixpoint.Types.Errors

Methods

put :: FixResult a -> Put

get :: Get (FixResult a)

putList :: [FixResult a] -> Put

Serialize (FixResult Error)

Defined in Language.Fixpoint.Types.Errors

Methods

put :: Putter (FixResult Error)

get :: Get (FixResult Error)

NFData a => NFData (FixResult a)

Defined in Language.Fixpoint.Types.Errors

Methods

rnf :: FixResult a -> ()

(Ord a, Fixpoint a) => Fixpoint (FixResult (SubC a))

Defined in Language.Fixpoint.Types.Constraints

Methods

toFix :: FixResult (SubC a) -> Doc

simplify :: FixResult (SubC a) -> FixResult (SubC a)

Inputable (FixResult Integer)

Defined in Language.Fixpoint.Parse

Methods

rr :: String -> FixResult Integer

rr' :: String -> String -> FixResult Integer

Inputable (FixResult Integer, FixSolution)

Defined in Language.Fixpoint.Parse

Methods

rr :: String -> (FixResult Integer, FixSolution)

rr' :: String -> String -> (FixResult Integer, FixSolution)

type Rep (FixResult a)

Defined in Language.Fixpoint.Types.Errors

type Rep (FixResult a) = D1 (MetaData "FixResult" "Language.Fixpoint.Types.Errors" "liquid-fixpoint-0.8.0.2-EGSzGwrlcJrCaUaEYLNzOY" False) (C1 (MetaCons "Crash" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [a]) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) :+: (C1 (MetaCons "Safe" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Stats)) :+: 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]))))

colorResult :: FixResult a -> Moods

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

resultExit :: FixResult a -> ExitCode

Error Type

data Error

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

Instances

Eq Error

Defined in Language.Fixpoint.Types.Errors

Methods

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

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

Ord Error

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

Defined in Language.Fixpoint.Types.Errors

Methods

showsPrec :: Int -> Error -> ShowS

show :: Error -> String

showList :: [Error] -> ShowS

Generic Error

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

Defined in Language.Fixpoint.Types.Errors

Methods

toException :: Error -> SomeException

fromException :: SomeException -> Maybe Error

displayException :: Error -> String

Serialize Error

Defined in Language.Fixpoint.Types.Errors

Methods

put :: Putter Error

get :: Get Error

PPrint Error

Defined in Language.Fixpoint.Types.Errors

Methods

pprintTidy :: Tidy -> Error -> Doc

pprintPrec :: Int -> Tidy -> Error -> Doc

Exception (FixResult Error)

Defined in Language.Fixpoint.Types.Errors

Methods

toException :: FixResult Error -> SomeException

fromException :: SomeException -> Maybe (FixResult Error)

displayException :: FixResult Error -> String

Serialize (FixResult Error)

Defined in Language.Fixpoint.Types.Errors

Methods

put :: Putter (FixResult Error)

get :: Get (FixResult Error)

type Rep Error

Defined in Language.Fixpoint.Types.Errors

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

data Error1

Instances

Eq Error1

Defined in Language.Fixpoint.Types.Errors

Methods

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

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

Ord Error1

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

Show Error1

Defined in Language.Fixpoint.Types.Errors

Methods

showsPrec :: Int -> Error1 -> ShowS

show :: Error1 -> String

showList :: [Error1] -> ShowS

Generic Error1

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

Defined in Language.Fixpoint.Types.Errors

Methods

put :: Putter Error1

get :: Get Error1

PPrint Error1

Defined in Language.Fixpoint.Types.Errors

Methods

pprintTidy :: Tidy -> Error1 -> Doc

pprintPrec :: Int -> Tidy -> Error1 -> Doc

Fixpoint Error1

Defined in Language.Fixpoint.Types.Errors

Methods

toFix :: Error1 -> Doc

simplify :: Error1 -> Error1

type Rep Error1

Defined in Language.Fixpoint.Types.Errors

type Rep Error1 = D1 (MetaData "Error1" "Language.Fixpoint.Types.Errors" "liquid-fixpoint-0.8.0.2-EGSzGwrlcJrCaUaEYLNzOY" 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

Accessors

errLoc :: Error1 -> SrcSpan

errMsg :: Error1 -> Doc

errs :: Error -> [Error1]

Adding Insult to Injury

catError :: Error -> Error -> Error

catErrors :: ListNE Error -> Error

Fatal Exit

panic :: String -> a

die :: Error -> a

dieAt :: SrcSpan -> Error -> a

exit :: a -> IO a -> IO a

Some popular errors

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

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

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

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

Orphan instances

Serialize Doc

Methods

put :: Putter Doc

get :: Get Doc

Serialize TextDetails

Methods

put :: Putter TextDetails

get :: Get TextDetails

Generic (AnnotDetails a)

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)

Methods

put :: Putter (Doc a)

get :: Get (Doc a)

Serialize a => Serialize (AnnotDetails a)

Methods

put :: Putter (AnnotDetails a)

get :: Get (AnnotDetails a)