Top-level Queries

Methods

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

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

Generic (WfC a) Source #

Instance details

Associated Types

type Rep (WfC a)

Instance details

type Rep (WfC a) = D1 ('MetaData "WfC" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) (C1 ('MetaCons "WfC" 'PrefixI 'True) (S1 ('MetaSel ('Just "wenv") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 IBindEnv) :*: (S1 ('MetaSel ('Just "wrft") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Symbol, Sort, KVar)) :*: S1 ('MetaSel ('Just "winfo") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 a))))

Methods

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

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

Fixpoint a => Show (WfC a) Source #

Instance details

Methods

showsPrec :: Int -> WfC a -> ShowS #

show :: WfC a -> String #

showList :: [WfC a] -> ShowS #

NFData a => NFData (WfC a) Source #

Instance details

Methods

rnf :: WfC a -> () #

Eq a => Eq (WfC a) Source #

Instance details

Methods

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

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

Defunc (WfC a) Source #

Instance details

Defined in Language.Fixpoint.Defunctionalize

Methods

defunc :: WfC a -> DF (WfC a) Source #

Fixpoint a => Fixpoint (WfC a) Source #

Instance details

Methods

toFix :: WfC a -> Doc Source #

simplify :: WfC a -> WfC a Source #

Fixpoint a => PPrint (WfC a) Source #

Instance details

Methods

pprintTidy :: Tidy -> WfC a -> Doc Source #

pprintPrec :: Int -> Tidy -> WfC a -> Doc Source #

Store a => Store (WfC a) Source #

Instance details

Methods

size :: Size (WfC a) #

poke :: WfC a -> Poke () #

peek :: Peek (WfC a) #

type Rep (WfC a) Source #

Instance details

type Rep (WfC a) = D1 ('MetaData "WfC" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) (C1 ('MetaCons "WfC" 'PrefixI 'True) (S1 ('MetaSel ('Just "wenv") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 IBindEnv) :*: (S1 ('MetaSel ('Just "wrft") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Symbol, Sort, KVar)) :*: S1 ('MetaSel ('Just "winfo") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 a))))

data SubC a Source #

Instances

Instances details

Functor SubC Source #

Instance details

Methods

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

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

TaggedC SubC a Source #

Instance details

Methods

senv :: SubC a -> IBindEnv Source #

updateSEnv :: SubC a -> (IBindEnv -> IBindEnv) -> SubC a Source #

sid :: SubC a -> Maybe Integer Source #

stag :: SubC a -> Tag Source #

sinfo :: SubC a -> a Source #

clhs :: BindEnv a -> SubC a -> [(Symbol, SortedReft)] Source #

crhs :: SubC a -> Expr Source #

Generic (SubC a) Source #

Instance details

Associated Types

type Rep (SubC a)

Instance details

type Rep (SubC a) = D1 ('MetaData "SubC" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) (C1 ('MetaCons "SubC" 'PrefixI 'True) ((S1 ('MetaSel ('Just "_senv") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 IBindEnv) :*: (S1 ('MetaSel ('Just "slhs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SortedReft) :*: S1 ('MetaSel ('Just "srhs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SortedReft))) :*: (S1 ('MetaSel ('Just "_sid") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe SubcId)) :*: (S1 ('MetaSel ('Just "_stag") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Tag) :*: S1 ('MetaSel ('Just "_sinfo") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 a)))))

Methods

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

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

Fixpoint a => Show (SubC a) Source #

Instance details

Methods

showsPrec :: Int -> SubC a -> ShowS #

show :: SubC a -> String #

showList :: [SubC a] -> ShowS #

NFData a => NFData (SubC a) Source #

Instance details

Methods

rnf :: SubC a -> () #

Eq a => Eq (SubC a) Source #

Instance details

Methods

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

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

Inputable (FInfo ()) Source #

Instance details

Defined in Language.Fixpoint.Parse

Methods

rr :: String -> FInfo () Source #

rr' :: String -> String -> FInfo () Source #

Fixpoint a => Fixpoint (SubC a) Source #

Instance details

Methods

toFix :: SubC a -> Doc Source #

simplify :: SubC a -> SubC a Source #

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

Instance details

Methods

toFix :: FixResult (SubC a) -> Doc Source #

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

Fixpoint a => PPrint (SubC a) Source #

Instance details

Methods

pprintTidy :: Tidy -> SubC a -> Doc Source #

pprintPrec :: Int -> Tidy -> SubC a -> Doc Source #

Foldable (SubC a) Source #

Instance details

Methods

foldE :: Monoid a0 => Folder a0 c -> c -> SubC a -> FoldM a0 (SubC a) Source #

SymConsts (SubC a) Source #

Instance details

Methods

symConsts :: SubC a -> [SymConst] Source #

Visitable (SubC a) Source #

Instance details

Methods

transE :: (Expr -> Expr) -> SubC a -> SubC a Source #

Store a => Store (SubC a) Source #

Instance details

Methods

size :: Size (SubC a) #

poke :: SubC a -> Poke () #

peek :: Peek (SubC a) #

type Rep (SubC a) Source #

Instance details

type Rep (SubC a) = D1 ('MetaData "SubC" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) (C1 ('MetaCons "SubC" 'PrefixI 'True) ((S1 ('MetaSel ('Just "_senv") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 IBindEnv) :*: (S1 ('MetaSel ('Just "slhs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SortedReft) :*: S1 ('MetaSel ('Just "srhs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SortedReft))) :*: (S1 ('MetaSel ('Just "_sid") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe SubcId)) :*: (S1 ('MetaSel ('Just "_stag") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Tag) :*: S1 ('MetaSel ('Just "_sinfo") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 a)))))

type SubcId = Integer Source #

mkSubC :: IBindEnv -> SortedReft -> SortedReft -> Maybe Integer -> Tag -> a -> SubC a Source #

subcId :: TaggedC c a => c a -> SubcId Source #

sid :: TaggedC c a => c a -> Maybe Integer Source #

senv :: TaggedC c a => c a -> IBindEnv Source #

updateSEnv :: TaggedC c a => c a -> (IBindEnv -> IBindEnv) -> c a Source #

slhs :: SubC a -> SortedReft Source #

srhs :: SubC a -> SortedReft Source #

stag :: TaggedC c a => c a -> Tag Source #

subC :: IBindEnv -> SortedReft -> SortedReft -> Maybe Integer -> Tag -> a -> [SubC a] Source #

wfC :: Fixpoint a => IBindEnv -> SortedReft -> a -> [WfC a] Source #

"Smart Constructors" for Constraints ---------------------------------

data SimpC a Source #

Constructors

SimpC
Fields _cenv :: !IBindEnv _crhs :: !Expr _cid :: !(Maybe Integer) cbind :: !BindId Id of lhs/rhs binder _ctag :: !Tag _cinfo :: !a

Instances

Instances details

Functor SimpC Source #

Instance details

Methods

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

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

TaggedC SimpC a Source #

Instance details

Methods

senv :: SimpC a -> IBindEnv Source #

updateSEnv :: SimpC a -> (IBindEnv -> IBindEnv) -> SimpC a Source #

sid :: SimpC a -> Maybe Integer Source #

stag :: SimpC a -> Tag Source #

sinfo :: SimpC a -> a Source #

clhs :: BindEnv a -> SimpC a -> [(Symbol, SortedReft)] Source #

crhs :: SimpC a -> Expr Source #

Generic (SimpC a) Source #

Instance details

Associated Types

type Rep (SimpC a)

Instance details

type Rep (SimpC a) = D1 ('MetaData "SimpC" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) (C1 ('MetaCons "SimpC" 'PrefixI 'True) ((S1 ('MetaSel ('Just "_cenv") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 IBindEnv) :*: (S1 ('MetaSel ('Just "_crhs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Expr) :*: S1 ('MetaSel ('Just "_cid") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe Integer)))) :*: (S1 ('MetaSel ('Just "cbind") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 BindId) :*: (S1 ('MetaSel ('Just "_ctag") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Tag) :*: S1 ('MetaSel ('Just "_cinfo") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 a)))))

Methods

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

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

Fixpoint a => Show (SimpC a) Source #

Instance details

Methods

showsPrec :: Int -> SimpC a -> ShowS #

show :: SimpC a -> String #

showList :: [SimpC a] -> ShowS #

NFData a => NFData (SimpC a) Source #

Instance details

Methods

rnf :: SimpC a -> () #

Defunc (SimpC a) Source #

Instance details

Defined in Language.Fixpoint.Defunctionalize

Methods

defunc :: SimpC a -> DF (SimpC a) Source #

Loc a => Elaborate (SInfo a) Source #

Instance details

Methods

elaborate :: ElabParam -> SInfo a -> SInfo a Source #

Loc a => Elaborate (SimpC a) Source #

Instance details

Methods

elaborate :: ElabParam -> SimpC a -> SimpC a Source #

Fixpoint a => Fixpoint (SimpC a) Source #

Instance details

Methods

toFix :: SimpC a -> Doc Source #

simplify :: SimpC a -> SimpC a Source #

Fixpoint a => PPrint (SimpC a) Source #

Instance details

Methods

pprintTidy :: Tidy -> SimpC a -> Doc Source #

pprintPrec :: Int -> Tidy -> SimpC a -> Doc Source #

PTable (SInfo a) Source #

Instance details

Methods

ptable :: SInfo a -> DocTable Source #

Loc a => Loc (SimpC a) Source #

Instance details

Methods

srcSpan :: SimpC a -> SrcSpan Source #

Foldable (SimpC a) Source #

Instance details

Methods

foldE :: Monoid a0 => Folder a0 c -> c -> SimpC a -> FoldM a0 (SimpC a) Source #

SymConsts (SimpC a) Source #

Instance details

Methods

symConsts :: SimpC a -> [SymConst] Source #

Visitable (SimpC a) Source #

Instance details

Methods

transE :: (Expr -> Expr) -> SimpC a -> SimpC a Source #

Store a => Store (SimpC a) Source #

Instance details

Methods

size :: Size (SimpC a) #

poke :: SimpC a -> Poke () #

peek :: Peek (SimpC a) #

type Rep (SimpC a) Source #

Instance details

type Rep (SimpC a) = D1 ('MetaData "SimpC" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) (C1 ('MetaCons "SimpC" 'PrefixI 'True) ((S1 ('MetaSel ('Just "_cenv") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 IBindEnv) :*: (S1 ('MetaSel ('Just "_crhs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Expr) :*: S1 ('MetaSel ('Just "_cid") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe Integer)))) :*: (S1 ('MetaSel ('Just "cbind") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 BindId) :*: (S1 ('MetaSel ('Just "_ctag") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Tag) :*: S1 ('MetaSel ('Just "_cinfo") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 a)))))

type Tag = [Int] Source #

Constraints ---------------------------------------------------------------

class TaggedC (c :: Type -> Type) a Source #

Minimal complete definition

senv, updateSEnv, sid, stag, sinfo, clhs, crhs

Instances

Instances details

TaggedC SimpC a Source #
Instance details Defined in Language.Fixpoint.Types.Constraints Methods senv :: SimpC a -> IBindEnv Source # updateSEnv :: SimpC a -> (IBindEnv -> IBindEnv) -> SimpC a Source # sid :: SimpC a -> Maybe Integer Source # stag :: SimpC a -> Tag Source # sinfo :: SimpC a -> a Source # clhs :: BindEnv a -> SimpC a -> [(Symbol, SortedReft)] Source # crhs :: SimpC a -> Expr Source #
TaggedC SubC a Source #
Instance details Defined in Language.Fixpoint.Types.Constraints Methods senv :: SubC a -> IBindEnv Source # updateSEnv :: SubC a -> (IBindEnv -> IBindEnv) -> SubC a Source # sid :: SubC a -> Maybe Integer Source # stag :: SubC a -> Tag Source # sinfo :: SubC a -> a Source # clhs :: BindEnv a -> SubC a -> [(Symbol, SortedReft)] Source # crhs :: SubC a -> Expr Source #

clhs :: TaggedC c a => BindEnv a -> c a -> [(Symbol, SortedReft)] Source #

crhs :: TaggedC c a => c a -> Expr Source #

strengthenHyp :: SInfo a -> [(Integer, Expr)] -> BindEnv a Source #

strengthenBinds :: SInfo a -> HashMap BindId Expr -> BindEnv a Source #

Accessing Constraints

addIds :: [SubC a] -> [(Integer, SubC a)] Source #

sinfo :: TaggedC c a => c a -> a Source #

shiftVV :: Reft -> Symbol -> Reft Source #

Qualifiers

type Qualifier = QualifierV Symbol Source #

Qualifiers ----------------------------------------------------------------

data QualifierV v Source #

Constructors

Q
Fields qName :: !Symbol Name qParams :: [QualParam] Parameters qBody :: !(ExprV v) Predicate qPos :: !SourcePos Source Location

Instances

Instances details

FromJSON Qualifier Source #

Instance details

Methods

parseJSON :: Value -> Parser Qualifier #

parseJSONList :: Value -> Parser [Qualifier] #

omittedField :: Maybe Qualifier #

ToJSON Qualifier Source #

Instance details

Methods

toJSON :: Qualifier -> Value #

toEncoding :: Qualifier -> Encoding #

toJSONList :: [Qualifier] -> Value #

toEncodingList :: [Qualifier] -> Encoding #

omitField :: Qualifier -> Bool #

Foldable QualifierV Source #

Instance details

Methods

fold :: Monoid m => QualifierV m -> m #

foldMap :: Monoid m => (a -> m) -> QualifierV a -> m #

foldMap' :: Monoid m => (a -> m) -> QualifierV a -> m #

foldr :: (a -> b -> b) -> b -> QualifierV a -> b #

foldr' :: (a -> b -> b) -> b -> QualifierV a -> b #

foldl :: (b -> a -> b) -> b -> QualifierV a -> b #

foldl' :: (b -> a -> b) -> b -> QualifierV a -> b #

foldr1 :: (a -> a -> a) -> QualifierV a -> a #

foldl1 :: (a -> a -> a) -> QualifierV a -> a #

toList :: QualifierV a -> [a] #

null :: QualifierV a -> Bool #

length :: QualifierV a -> Int #

elem :: Eq a => a -> QualifierV a -> Bool #

maximum :: Ord a => QualifierV a -> a #

minimum :: Ord a => QualifierV a -> a #

sum :: Num a => QualifierV a -> a #

product :: Num a => QualifierV a -> a #

Traversable QualifierV Source #

Instance details

Methods

traverse :: Applicative f => (a -> f b) -> QualifierV a -> f (QualifierV b) #

sequenceA :: Applicative f => QualifierV (f a) -> f (QualifierV a) #

mapM :: Monad m => (a -> m b) -> QualifierV a -> m (QualifierV b) #

sequence :: Monad m => QualifierV (m a) -> m (QualifierV a) #

Functor QualifierV Source #

Instance details

Methods

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

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

Fixpoint Qualifier Source #

Instance details

Methods

toFix :: Qualifier -> Doc Source #

simplify :: Qualifier -> Qualifier Source #

Subable Qualifier Source #

Instance details

Methods

syms :: Qualifier -> [Symbol] Source #

substa :: (Symbol -> Symbol) -> Qualifier -> Qualifier Source #

substf :: (Symbol -> Expr) -> Qualifier -> Qualifier Source #

subst :: Subst -> Qualifier -> Qualifier Source #

subst1 :: Qualifier -> (Symbol, Expr) -> Qualifier Source #

ToHornSMT Qualifier Source #

Instance details

Methods

toHornSMT :: Qualifier -> Doc Source #

Loc Qualifier Source #

Instance details

Methods

srcSpan :: Qualifier -> SrcSpan Source #

Store Qualifier Source #

Instance details

Methods

size :: Size Qualifier #

poke :: Qualifier -> Poke () #

peek :: Peek Qualifier #

Data v => Data (QualifierV v) Source #

Instance details

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> QualifierV v -> c (QualifierV v) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (QualifierV v) #

toConstr :: QualifierV v -> Constr #

dataTypeOf :: QualifierV v -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (QualifierV v)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (QualifierV v)) #

gmapT :: (forall b. Data b => b -> b) -> QualifierV v -> QualifierV v #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QualifierV v -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QualifierV v -> r #

gmapQ :: (forall d. Data d => d -> u) -> QualifierV v -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> QualifierV v -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> QualifierV v -> m (QualifierV v) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> QualifierV v -> m (QualifierV v) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> QualifierV v -> m (QualifierV v) #

Generic (QualifierV v) Source #

Instance details

Associated Types

type Rep (QualifierV v)

Instance details

type Rep (QualifierV v) = D1 ('MetaData "QualifierV" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) (C1 ('MetaCons "Q" 'PrefixI 'True) ((S1 ('MetaSel ('Just "qName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol) :*: S1 ('MetaSel ('Just "qParams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [QualParam])) :*: (S1 ('MetaSel ('Just "qBody") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)) :*: S1 ('MetaSel ('Just "qPos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SourcePos))))

Methods

from :: QualifierV v -> Rep (QualifierV v) x #

to :: Rep (QualifierV v) x -> QualifierV v #

(Show v, Fixpoint v, Ord v) => Show (QualifierV v) Source #

Instance details

Methods

showsPrec :: Int -> QualifierV v -> ShowS #

show :: QualifierV v -> String #

showList :: [QualifierV v] -> ShowS #

Binary v => Binary (QualifierV v) Source #

Instance details

Methods

put :: QualifierV v -> Put #

get :: Get (QualifierV v) #

putList :: [QualifierV v] -> Put #

NFData v => NFData (QualifierV v) Source #

Instance details

Methods

rnf :: QualifierV v -> () #

Eq v => Eq (QualifierV v) Source #

Instance details

Methods

(==) :: QualifierV v -> QualifierV v -> Bool #

(/=) :: QualifierV v -> QualifierV v -> Bool #

Ord v => Ord (QualifierV v) Source #

Instance details

Methods

compare :: QualifierV v -> QualifierV v -> Ordering #

(<) :: QualifierV v -> QualifierV v -> Bool #

(<=) :: QualifierV v -> QualifierV v -> Bool #

(>) :: QualifierV v -> QualifierV v -> Bool #

(>=) :: QualifierV v -> QualifierV v -> Bool #

max :: QualifierV v -> QualifierV v -> QualifierV v #

min :: QualifierV v -> QualifierV v -> QualifierV v #

Hashable v => Hashable (QualifierV v) Source #

Instance details

Methods

hashWithSalt :: Int -> QualifierV v -> Int #

hash :: QualifierV v -> Int #

(Ord v, Fixpoint v, PPrint v) => PPrint (QualifierV v) Source #

Instance details

Methods

pprintTidy :: Tidy -> QualifierV v -> Doc Source #

pprintPrec :: Int -> Tidy -> QualifierV v -> Doc Source #

type Rep (QualifierV v) Source #

Instance details

type Rep (QualifierV v) = D1 ('MetaData "QualifierV" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) (C1 ('MetaCons "Q" 'PrefixI 'True) ((S1 ('MetaSel ('Just "qName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol) :*: S1 ('MetaSel ('Just "qParams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [QualParam])) :*: (S1 ('MetaSel ('Just "qBody") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)) :*: S1 ('MetaSel ('Just "qPos") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 SourcePos))))

data QualParam Source #

Constructors

QP
Fields qpSym :: !Symbol qpPat :: !QualPattern qpSort :: !Sort

Instances

Instances details

FromJSON QualParam Source #

Instance details

Methods

parseJSON :: Value -> Parser QualParam #

parseJSONList :: Value -> Parser [QualParam] #

omittedField :: Maybe QualParam #

ToJSON QualParam Source #

Instance details

Methods

toJSON :: QualParam -> Value #

toEncoding :: QualParam -> Encoding #

toJSONList :: [QualParam] -> Value #

toEncodingList :: [QualParam] -> Encoding #

omitField :: QualParam -> Bool #

Data QualParam Source #

Instance details

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> QualParam -> c QualParam #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c QualParam #

toConstr :: QualParam -> Constr #

dataTypeOf :: QualParam -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c QualParam) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QualParam) #

gmapT :: (forall b. Data b => b -> b) -> QualParam -> QualParam #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QualParam -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QualParam -> r #

gmapQ :: (forall d. Data d => d -> u) -> QualParam -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> QualParam -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> QualParam -> m QualParam #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> QualParam -> m QualParam #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> QualParam -> m QualParam #

Generic QualParam Source #

Instance details

Associated Types

type Rep QualParam

Instance details

type Rep QualParam = D1 ('MetaData "QualParam" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) (C1 ('MetaCons "QP" 'PrefixI 'True) (S1 ('MetaSel ('Just "qpSym") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol) :*: (S1 ('MetaSel ('Just "qpPat") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 QualPattern) :*: S1 ('MetaSel ('Just "qpSort") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Sort))))

Methods

from :: QualParam -> Rep QualParam x #

to :: Rep QualParam x -> QualParam #

Show QualParam Source #

Instance details

Methods

showsPrec :: Int -> QualParam -> ShowS #

show :: QualParam -> String #

showList :: [QualParam] -> ShowS #

Binary QualParam Source #

Instance details

Methods

put :: QualParam -> Put #

get :: Get QualParam #

putList :: [QualParam] -> Put #

NFData QualParam Source #

Instance details

Methods

rnf :: QualParam -> () #

Eq QualParam Source #

Instance details

Methods

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

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

Ord QualParam Source #

Instance details

Methods

compare :: QualParam -> QualParam -> Ordering #

(<) :: QualParam -> QualParam -> Bool #

(<=) :: QualParam -> QualParam -> Bool #

(>) :: QualParam -> QualParam -> Bool #

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

max :: QualParam -> QualParam -> QualParam #

min :: QualParam -> QualParam -> QualParam #

Hashable QualParam Source #

Instance details

Methods

hashWithSalt :: Int -> QualParam -> Int #

hash :: QualParam -> Int #

Fixpoint QualParam Source #

Instance details

Methods

toFix :: QualParam -> Doc Source #

simplify :: QualParam -> QualParam Source #

PPrint QualParam Source #

Instance details

Methods

pprintTidy :: Tidy -> QualParam -> Doc Source #

pprintPrec :: Int -> Tidy -> QualParam -> Doc Source #

ToHornSMT QualParam Source #

Instance details

Methods

toHornSMT :: QualParam -> Doc Source #

Store QualParam Source #

Instance details

Methods

size :: Size QualParam #

poke :: QualParam -> Poke () #

peek :: Peek QualParam #

type Rep QualParam Source #

Instance details

type Rep QualParam = D1 ('MetaData "QualParam" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) (C1 ('MetaCons "QP" 'PrefixI 'True) (S1 ('MetaSel ('Just "qpSym") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol) :*: (S1 ('MetaSel ('Just "qpPat") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 QualPattern) :*: S1 ('MetaSel ('Just "qpSort") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Sort))))

data QualPattern Source #

Constructors

PatNone	match everything
PatPrefix !Symbol !Int	str . $i i.e. match prefix `str` with suffix bound to $i
PatSuffix !Int !Symbol	$i . str i.e. match suffix `str` with prefix bound to $i
PatExact !Symbol	str i.e. exactly match `str`

Instances

Instances details

FromJSON QualPattern Source #

Instance details

Methods

parseJSON :: Value -> Parser QualPattern #

parseJSONList :: Value -> Parser [QualPattern] #

omittedField :: Maybe QualPattern #

ToJSON QualPattern Source #

Instance details

Methods

toJSON :: QualPattern -> Value #

toEncoding :: QualPattern -> Encoding #

toJSONList :: [QualPattern] -> Value #

toEncodingList :: [QualPattern] -> Encoding #

omitField :: QualPattern -> Bool #

Data QualPattern Source #

Instance details

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> QualPattern -> c QualPattern #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c QualPattern #

toConstr :: QualPattern -> Constr #

dataTypeOf :: QualPattern -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c QualPattern) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QualPattern) #

gmapT :: (forall b. Data b => b -> b) -> QualPattern -> QualPattern #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QualPattern -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QualPattern -> r #

gmapQ :: (forall d. Data d => d -> u) -> QualPattern -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> QualPattern -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> QualPattern -> m QualPattern #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> QualPattern -> m QualPattern #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> QualPattern -> m QualPattern #

Generic QualPattern Source #

Instance details

Associated Types

type Rep QualPattern

Instance details

type Rep QualPattern = D1 ('MetaData "QualPattern" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) ((C1 ('MetaCons "PatNone" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PatPrefix" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int))) :+: (C1 ('MetaCons "PatSuffix" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol)) :+: C1 ('MetaCons "PatExact" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol))))

Methods

from :: QualPattern -> Rep QualPattern x #

to :: Rep QualPattern x -> QualPattern #

Show QualPattern Source #

Instance details

Methods

showsPrec :: Int -> QualPattern -> ShowS #

show :: QualPattern -> String #

showList :: [QualPattern] -> ShowS #

Binary QualPattern Source #

Instance details

Methods

put :: QualPattern -> Put #

get :: Get QualPattern #

putList :: [QualPattern] -> Put #

NFData QualPattern Source #

Instance details

Methods

rnf :: QualPattern -> () #

Eq QualPattern Source #

Instance details

Methods

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

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

Ord QualPattern Source #

Instance details

Methods

compare :: QualPattern -> QualPattern -> Ordering #

(<) :: QualPattern -> QualPattern -> Bool #

(<=) :: QualPattern -> QualPattern -> Bool #

(>) :: QualPattern -> QualPattern -> Bool #

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

max :: QualPattern -> QualPattern -> QualPattern #

min :: QualPattern -> QualPattern -> QualPattern #

Hashable QualPattern Source #

Instance details

Methods

hashWithSalt :: Int -> QualPattern -> Int #

hash :: QualPattern -> Int #

PPrint QualPattern Source #

Instance details

Methods

pprintTidy :: Tidy -> QualPattern -> Doc Source #

pprintPrec :: Int -> Tidy -> QualPattern -> Doc Source #

Store QualPattern Source #

Instance details

Methods

size :: Size QualPattern #

poke :: QualPattern -> Poke () #

peek :: Peek QualPattern #

type Rep QualPattern Source #

Instance details

type Rep QualPattern = D1 ('MetaData "QualPattern" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) ((C1 ('MetaCons "PatNone" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PatPrefix" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int))) :+: (C1 ('MetaCons "PatSuffix" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol)) :+: C1 ('MetaCons "PatExact" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol))))

trueQual :: Qualifier Source #

qualifier :: SEnv Sort -> SourcePos -> SEnv Sort -> Symbol -> Sort -> Expr -> Qualifier Source #

mkQual :: Symbol -> [QualParam] -> ExprV v -> SourcePos -> QualifierV v Source #

constructing qualifiers

remakeQual :: Qualifier -> Qualifier Source #

mkQ :: Symbol -> [(Symbol, Sort)] -> Expr -> SourcePos -> Qualifier Source #

qualBinds :: Qualifier -> [(Symbol, Sort)] Source #

Results

type FixSolution = HashMap KVar Expr Source #

type FixDelayedSolution = HashMap KVar (Delayed Expr) Source #

data Delayed a Source #

Solutions and Results

Since some solutions are expensive to compute, we wrap them in a Delayed type to compute them only if needed.

Constructors

Delayed
Fields forceDelayed :: a

Instances

Instances details

Functor Delayed Source #

Instance details

Methods

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

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

Generic (Delayed a) Source #

Instance details

Associated Types

type Rep (Delayed a)
Instance details Defined in Language.Fixpoint.Types.Constraints type Rep (Delayed a) = D1 ('MetaData "Delayed" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) (C1 ('MetaCons "Delayed" 'PrefixI 'True) (S1 ('MetaSel ('Just "forceDelayed") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))

Methods

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

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

Show a => Show (Delayed a) Source #

Instance details

Methods

showsPrec :: Int -> Delayed a -> ShowS #

show :: Delayed a -> String #

showList :: [Delayed a] -> ShowS #

NFData a => NFData (Delayed a) Source #

Instance details

Methods

rnf :: Delayed a -> () #

type Rep (Delayed a) Source #

Instance details

type Rep (Delayed a) = D1 ('MetaData "Delayed" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) (C1 ('MetaCons "Delayed" 'PrefixI 'True) (S1 ('MetaSel ('Just "forceDelayed") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))

data Result a Source #

Constructors

Result
Fields resStatus :: !(FixResult a) resSolution :: !FixSolution resNonCutsSolution :: !FixDelayedSolution resSorts :: !ResultSorts

Instances

Instances details

Functor Result Source #

Instance details

Methods

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

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

ToJSON a => ToJSON (Result a) Source #

Instance details

Methods

toJSON :: Result a -> Value #

toEncoding :: Result a -> Encoding #

toJSONList :: [Result a] -> Value #

toEncodingList :: [Result a] -> Encoding #

omitField :: Result a -> Bool #

Monoid (Result a) Source #

Instance details

Methods

mempty :: Result a #

mappend :: Result a -> Result a -> Result a #

mconcat :: [Result a] -> Result a #

Semigroup (Result a) Source #

Instance details

Methods

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

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

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

Generic (Result a) Source #

Instance details

Associated Types

type Rep (Result a)

Instance details

type Rep (Result a) = D1 ('MetaData "Result" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) (C1 ('MetaCons "Result" 'PrefixI 'True) ((S1 ('MetaSel ('Just "resStatus") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (FixResult a)) :*: S1 ('MetaSel ('Just "resSolution") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 FixSolution)) :*: (S1 ('MetaSel ('Just "resNonCutsSolution") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 FixDelayedSolution) :*: S1 ('MetaSel ('Just "resSorts") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 ResultSorts))))

Methods

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

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

Show a => Show (Result a) Source #

Instance details

Methods

showsPrec :: Int -> Result a -> ShowS #

show :: Result a -> String #

showList :: [Result a] -> ShowS #

NFData a => NFData (Result a) Source #

Instance details

Methods

rnf :: Result a -> () #

type Rep (Result a) Source #

Instance details

type Rep (Result a) = D1 ('MetaData "Result" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) (C1 ('MetaCons "Result" 'PrefixI 'True) ((S1 ('MetaSel ('Just "resStatus") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (FixResult a)) :*: S1 ('MetaSel ('Just "resSolution") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 FixSolution)) :*: (S1 ('MetaSel ('Just "resNonCutsSolution") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 FixDelayedSolution) :*: S1 ('MetaSel ('Just "resSorts") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 ResultSorts))))

type ResultSorts = HashMap KVar [(Symbol, Sort)] Source #

unsafe :: Result a Source #

isUnsafe :: Result a -> Bool Source #

isSafe :: Result a -> Bool Source #

safe :: Result a Source #

Cut KVars

newtype Kuts Source #

Constraint Cut Sets -------------------------------------------------------

Constructors

KS
Fields ksVars :: HashSet KVar

Instances

Instances details

Monoid Kuts Source #

Instance details

Methods

mempty :: Kuts #

mappend :: Kuts -> Kuts -> Kuts #

mconcat :: [Kuts] -> Kuts #

Semigroup Kuts Source #

Instance details

Methods

(<>) :: Kuts -> Kuts -> Kuts #

sconcat :: NonEmpty Kuts -> Kuts #

stimes :: Integral b => b -> Kuts -> Kuts #

Generic Kuts Source #

Instance details

Associated Types

type Rep Kuts
Instance details Defined in Language.Fixpoint.Types.Constraints type Rep Kuts = D1 ('MetaData "Kuts" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'True) (C1 ('MetaCons "KS" 'PrefixI 'True) (S1 ('MetaSel ('Just "ksVars") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet KVar))))

Methods

from :: Kuts -> Rep Kuts x #

to :: Rep Kuts x -> Kuts #

Show Kuts Source #

Instance details

Methods

showsPrec :: Int -> Kuts -> ShowS #

show :: Kuts -> String #

showList :: [Kuts] -> ShowS #

NFData Kuts Source #

Instance details

Methods

rnf :: Kuts -> () #

Eq Kuts Source #

Instance details

Methods

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

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

Fixpoint Kuts Source #

Instance details

Methods

toFix :: Kuts -> Doc Source #

simplify :: Kuts -> Kuts Source #

Store Kuts Source #

Instance details

Methods

size :: Size Kuts #

poke :: Kuts -> Poke () #

peek :: Peek Kuts #

type Rep Kuts Source #

Instance details

type Rep Kuts = D1 ('MetaData "Kuts" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'True) (C1 ('MetaCons "KS" 'PrefixI 'True) (S1 ('MetaSel ('Just "ksVars") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet KVar))))

ksMember :: KVar -> Kuts -> Bool Source #

Higher Order Logic

data HOInfo Source #

Constructors

HOI
Fields hoBinds :: Bool Allow higher order binds in the environemnt hoQuals :: Bool Allow higher order quals

Instances

Instances details

Monoid HOInfo Source #

Instance details

Methods

mempty :: HOInfo #

mappend :: HOInfo -> HOInfo -> HOInfo #

mconcat :: [HOInfo] -> HOInfo #

Semigroup HOInfo Source #

Instance details

Methods

(<>) :: HOInfo -> HOInfo -> HOInfo #

sconcat :: NonEmpty HOInfo -> HOInfo #

stimes :: Integral b => b -> HOInfo -> HOInfo #

Generic HOInfo Source #

Instance details

Associated Types

type Rep HOInfo

Instance details

type Rep HOInfo = D1 ('MetaData "HOInfo" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) (C1 ('MetaCons "HOI" 'PrefixI 'True) (S1 ('MetaSel ('Just "hoBinds") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "hoQuals") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))

Methods

from :: HOInfo -> Rep HOInfo x #

to :: Rep HOInfo x -> HOInfo #

Show HOInfo Source #

Instance details

Methods

showsPrec :: Int -> HOInfo -> ShowS #

show :: HOInfo -> String #

showList :: [HOInfo] -> ShowS #

NFData HOInfo Source #

Instance details

Methods

rnf :: HOInfo -> () #

Eq HOInfo Source #

Instance details

Methods

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

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

Store HOInfo Source #

Instance details

Methods

size :: Size HOInfo #

poke :: HOInfo -> Poke () #

peek :: Peek HOInfo #

type Rep HOInfo Source #

Instance details

type Rep HOInfo = D1 ('MetaData "HOInfo" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) (C1 ('MetaCons "HOI" 'PrefixI 'True) (S1 ('MetaSel ('Just "hoBinds") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "hoQuals") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))

allowHO :: forall (c :: Type -> Type) a. GInfo c a -> Bool Source #

allowHOquals :: forall (c :: Type -> Type) a. GInfo c a -> Bool Source #

cfgHoInfo :: Config -> HOInfo Source #

Axioms

data AxiomEnv Source #

Axiom Instantiation Information --------------------------------------

Constructors

AEnv
Fields aenvEqs :: ![Equation] aenvSimpl :: ![Rewrite] aenvExpand :: HashMap SubcId Bool aenvAutoRW :: HashMap SubcId [AutoRewrite]

Instances

Instances details

Monoid AxiomEnv Source #

Instance details

Methods

mempty :: AxiomEnv #

mappend :: AxiomEnv -> AxiomEnv -> AxiomEnv #

mconcat :: [AxiomEnv] -> AxiomEnv #

Semigroup AxiomEnv Source #

Instance details

Methods

(<>) :: AxiomEnv -> AxiomEnv -> AxiomEnv #

sconcat :: NonEmpty AxiomEnv -> AxiomEnv #

stimes :: Integral b => b -> AxiomEnv -> AxiomEnv #

Generic AxiomEnv Source #

Instance details

Associated Types

type Rep AxiomEnv

Instance details

type Rep AxiomEnv = D1 ('MetaData "AxiomEnv" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) (C1 ('MetaCons "AEnv" 'PrefixI 'True) ((S1 ('MetaSel ('Just "aenvEqs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Equation]) :*: S1 ('MetaSel ('Just "aenvSimpl") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Rewrite])) :*: (S1 ('MetaSel ('Just "aenvExpand") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap SubcId Bool)) :*: S1 ('MetaSel ('Just "aenvAutoRW") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap SubcId [AutoRewrite])))))

Methods

from :: AxiomEnv -> Rep AxiomEnv x #

to :: Rep AxiomEnv x -> AxiomEnv #

Show AxiomEnv Source #

Instance details

Methods

showsPrec :: Int -> AxiomEnv -> ShowS #

show :: AxiomEnv -> String #

showList :: [AxiomEnv] -> ShowS #

NFData AxiomEnv Source #

Instance details

Methods

rnf :: AxiomEnv -> () #

Eq AxiomEnv Source #

Instance details

Methods

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

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

Elaborate AxiomEnv Source #

Instance details

Methods

elaborate :: ElabParam -> AxiomEnv -> AxiomEnv Source #

Fixpoint AxiomEnv Source #

Instance details

Methods

toFix :: AxiomEnv -> Doc Source #

simplify :: AxiomEnv -> AxiomEnv Source #

PPrint AxiomEnv Source #

Instance details

Methods

pprintTidy :: Tidy -> AxiomEnv -> Doc Source #

pprintPrec :: Int -> Tidy -> AxiomEnv -> Doc Source #

Foldable AxiomEnv Source #

Instance details

Methods

foldE :: Monoid a => Folder a c -> c -> AxiomEnv -> FoldM a AxiomEnv Source #

SymConsts AxiomEnv Source #

Instance details

Methods

symConsts :: AxiomEnv -> [SymConst] Source #

Visitable AxiomEnv Source #

Instance details

Methods

transE :: (Expr -> Expr) -> AxiomEnv -> AxiomEnv Source #

Store AxiomEnv Source #

Instance details

Methods

size :: Size AxiomEnv #

poke :: AxiomEnv -> Poke () #

peek :: Peek AxiomEnv #

type Rep AxiomEnv Source #

Instance details

type Rep AxiomEnv = D1 ('MetaData "AxiomEnv" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) (C1 ('MetaCons "AEnv" 'PrefixI 'True) ((S1 ('MetaSel ('Just "aenvEqs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Equation]) :*: S1 ('MetaSel ('Just "aenvSimpl") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Rewrite])) :*: (S1 ('MetaSel ('Just "aenvExpand") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap SubcId Bool)) :*: S1 ('MetaSel ('Just "aenvAutoRW") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap SubcId [AutoRewrite])))))

type Equation = EquationV Symbol Source #

newtype DefinedFuns Source #

Constructors

MkDefinedFuns [Equation]

Instances

Instances details

Data DefinedFuns Source #

Instance details

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DefinedFuns -> c DefinedFuns #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DefinedFuns #

toConstr :: DefinedFuns -> Constr #

dataTypeOf :: DefinedFuns -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DefinedFuns) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DefinedFuns) #

gmapT :: (forall b. Data b => b -> b) -> DefinedFuns -> DefinedFuns #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DefinedFuns -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DefinedFuns -> r #

gmapQ :: (forall d. Data d => d -> u) -> DefinedFuns -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> DefinedFuns -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DefinedFuns -> m DefinedFuns #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DefinedFuns -> m DefinedFuns #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DefinedFuns -> m DefinedFuns #

Monoid DefinedFuns Source #

Instance details

Methods

mempty :: DefinedFuns #

mappend :: DefinedFuns -> DefinedFuns -> DefinedFuns #

mconcat :: [DefinedFuns] -> DefinedFuns #

Semigroup DefinedFuns Source #

Instance details

Methods

(<>) :: DefinedFuns -> DefinedFuns -> DefinedFuns #

sconcat :: NonEmpty DefinedFuns -> DefinedFuns #

stimes :: Integral b => b -> DefinedFuns -> DefinedFuns #

Generic DefinedFuns Source #

Instance details

Associated Types

type Rep DefinedFuns
Instance details Defined in Language.Fixpoint.Types.Constraints type Rep DefinedFuns = D1 ('MetaData "DefinedFuns" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'True) (C1 ('MetaCons "MkDefinedFuns" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Equation])))

Methods

from :: DefinedFuns -> Rep DefinedFuns x #

to :: Rep DefinedFuns x -> DefinedFuns #

Show DefinedFuns Source #

Instance details

Methods

showsPrec :: Int -> DefinedFuns -> ShowS #

show :: DefinedFuns -> String #

showList :: [DefinedFuns] -> ShowS #

NFData DefinedFuns Source #

Instance details

Methods

rnf :: DefinedFuns -> () #

Eq DefinedFuns Source #

Instance details

Methods

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

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

Ord DefinedFuns Source #

Instance details

Methods

compare :: DefinedFuns -> DefinedFuns -> Ordering #

(<) :: DefinedFuns -> DefinedFuns -> Bool #

(<=) :: DefinedFuns -> DefinedFuns -> Bool #

(>) :: DefinedFuns -> DefinedFuns -> Bool #

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

max :: DefinedFuns -> DefinedFuns -> DefinedFuns #

min :: DefinedFuns -> DefinedFuns -> DefinedFuns #

Elaborate DefinedFuns Source #

Instance details

Methods

elaborate :: ElabParam -> DefinedFuns -> DefinedFuns Source #

PPrint DefinedFuns Source #

Instance details

Methods

pprintTidy :: Tidy -> DefinedFuns -> Doc Source #

pprintPrec :: Int -> Tidy -> DefinedFuns -> Doc Source #

TheorySymbols DefinedFuns Source #

Instance details

Defined in Language.Fixpoint.Smt.Theories

Methods

theorySymbols :: DefinedFuns -> SEnv TheorySymbol Source #

Store DefinedFuns Source #

Instance details

Methods

size :: Size DefinedFuns #

poke :: DefinedFuns -> Poke () #

peek :: Peek DefinedFuns #

type Rep DefinedFuns Source #

Instance details

type Rep DefinedFuns = D1 ('MetaData "DefinedFuns" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'True) (C1 ('MetaCons "MkDefinedFuns" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Equation])))

data EquationV v Source #

Constructors

Equ
Fields eqName :: !Symbol name of reflected function eqArgs :: [(Symbol, Sort)] names of parameters eqBody :: !(ExprV v) definition of body eqSort :: !Sort sort of body eqRec :: !Bool is this a recursive definition

Instances

Instances details

FromJSON Equation Source #

Instance details

Methods

parseJSON :: Value -> Parser Equation #

parseJSONList :: Value -> Parser [Equation] #

omittedField :: Maybe Equation #

ToJSON Equation Source #

Instance details

Methods

toJSON :: Equation -> Value #

toEncoding :: Equation -> Encoding #

toJSONList :: [Equation] -> Value #

toEncodingList :: [Equation] -> Encoding #

omitField :: Equation -> Bool #

Functor EquationV Source #

Instance details

Methods

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

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

NFData Equation Source #

Instance details

Methods

rnf :: Equation -> () #

Elaborate Equation Source #

Instance details

Methods

elaborate :: ElabParam -> Equation -> Equation Source #

Fixpoint Equation Source #

Instance details

Methods

toFix :: Equation -> Doc Source #

simplify :: Equation -> Equation Source #

PPrint Equation Source #

Instance details

Methods

pprintTidy :: Tidy -> Equation -> Doc Source #

pprintPrec :: Int -> Tidy -> Equation -> Doc Source #

Subable Equation Source #

Instance details

Methods

syms :: Equation -> [Symbol] Source #

substa :: (Symbol -> Symbol) -> Equation -> Equation Source #

substf :: (Symbol -> Expr) -> Equation -> Equation Source #

subst :: Subst -> Equation -> Equation Source #

subst1 :: Equation -> (Symbol, Expr) -> Equation Source #

Foldable Equation Source #

Instance details

Methods

foldE :: Monoid a => Folder a c -> c -> Equation -> FoldM a Equation Source #

SymConsts Equation Source #

Instance details

Methods

symConsts :: Equation -> [SymConst] Source #

Visitable Equation Source #

Instance details

Methods

transE :: (Expr -> Expr) -> Equation -> Equation Source #

Store Equation Source #

Instance details

Methods

size :: Size Equation #

poke :: Equation -> Poke () #

peek :: Peek Equation #

Data v => Data (EquationV v) Source #

Instance details

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EquationV v -> c (EquationV v) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (EquationV v) #

toConstr :: EquationV v -> Constr #

dataTypeOf :: EquationV v -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (EquationV v)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (EquationV v)) #

gmapT :: (forall b. Data b => b -> b) -> EquationV v -> EquationV v #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EquationV v -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EquationV v -> r #

gmapQ :: (forall d. Data d => d -> u) -> EquationV v -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> EquationV v -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> EquationV v -> m (EquationV v) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> EquationV v -> m (EquationV v) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> EquationV v -> m (EquationV v) #

Generic (EquationV v) Source #

Instance details

Associated Types

type Rep (EquationV v)

Instance details

type Rep (EquationV v) = D1 ('MetaData "EquationV" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) (C1 ('MetaCons "Equ" 'PrefixI 'True) ((S1 ('MetaSel ('Just "eqName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol) :*: S1 ('MetaSel ('Just "eqArgs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Symbol, Sort)])) :*: (S1 ('MetaSel ('Just "eqBody") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)) :*: (S1 ('MetaSel ('Just "eqSort") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Sort) :*: S1 ('MetaSel ('Just "eqRec") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Bool)))))

Methods

from :: EquationV v -> Rep (EquationV v) x #

to :: Rep (EquationV v) x -> EquationV v #

(Show v, Fixpoint v, Ord v) => Show (EquationV v) Source #

Instance details

Methods

showsPrec :: Int -> EquationV v -> ShowS #

show :: EquationV v -> String #

showList :: [EquationV v] -> ShowS #

Binary v => Binary (EquationV v) Source #

Instance details

Methods

put :: EquationV v -> Put #

get :: Get (EquationV v) #

putList :: [EquationV v] -> Put #

Eq v => Eq (EquationV v) Source #

Instance details

Methods

(==) :: EquationV v -> EquationV v -> Bool #

(/=) :: EquationV v -> EquationV v -> Bool #

Ord v => Ord (EquationV v) Source #

Instance details

Methods

compare :: EquationV v -> EquationV v -> Ordering #

(<) :: EquationV v -> EquationV v -> Bool #

(<=) :: EquationV v -> EquationV v -> Bool #

(>) :: EquationV v -> EquationV v -> Bool #

(>=) :: EquationV v -> EquationV v -> Bool #

max :: EquationV v -> EquationV v -> EquationV v #

min :: EquationV v -> EquationV v -> EquationV v #

Hashable v => Hashable (EquationV v) Source #

Instance details

Methods

hashWithSalt :: Int -> EquationV v -> Int #

hash :: EquationV v -> Int #

TheorySymbols [Equation] Source #

Instance details

Defined in Language.Fixpoint.Smt.Theories

Methods

theorySymbols :: [Equation] -> SEnv TheorySymbol Source #

type Rep (EquationV v) Source #

Instance details

type Rep (EquationV v) = D1 ('MetaData "EquationV" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) (C1 ('MetaCons "Equ" 'PrefixI 'True) ((S1 ('MetaSel ('Just "eqName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol) :*: S1 ('MetaSel ('Just "eqArgs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Symbol, Sort)])) :*: (S1 ('MetaSel ('Just "eqBody") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (ExprV v)) :*: (S1 ('MetaSel ('Just "eqSort") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Sort) :*: S1 ('MetaSel ('Just "eqRec") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Bool)))))

mkEquation :: Symbol -> [(Symbol, Sort)] -> Expr -> Sort -> Equation Source #

data Rewrite Source #

Constructors

SMeasure
Fields smName :: Symbol smDC :: Symbol smArgs :: [Symbol] smBody :: Expr

Instances

Instances details

FromJSON Rewrite Source #

Instance details

Methods

parseJSON :: Value -> Parser Rewrite #

parseJSONList :: Value -> Parser [Rewrite] #

omittedField :: Maybe Rewrite #

ToJSON Rewrite Source #

Instance details

Methods

toJSON :: Rewrite -> Value #

toEncoding :: Rewrite -> Encoding #

toJSONList :: [Rewrite] -> Value #

toEncodingList :: [Rewrite] -> Encoding #

omitField :: Rewrite -> Bool #

Data Rewrite Source #

Instance details

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Rewrite -> c Rewrite #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Rewrite #

toConstr :: Rewrite -> Constr #

dataTypeOf :: Rewrite -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Rewrite) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Rewrite) #

gmapT :: (forall b. Data b => b -> b) -> Rewrite -> Rewrite #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Rewrite -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Rewrite -> r #

gmapQ :: (forall d. Data d => d -> u) -> Rewrite -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Rewrite -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Rewrite -> m Rewrite #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Rewrite -> m Rewrite #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Rewrite -> m Rewrite #

Generic Rewrite Source #

Instance details

Associated Types

type Rep Rewrite

Instance details

type Rep Rewrite = D1 ('MetaData "Rewrite" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) (C1 ('MetaCons "SMeasure" 'PrefixI 'True) ((S1 ('MetaSel ('Just "smName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol) :*: S1 ('MetaSel ('Just "smDC") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol)) :*: (S1 ('MetaSel ('Just "smArgs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Symbol]) :*: S1 ('MetaSel ('Just "smBody") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))))

Methods

from :: Rewrite -> Rep Rewrite x #

to :: Rep Rewrite x -> Rewrite #

Show Rewrite Source #

Instance details

Methods

showsPrec :: Int -> Rewrite -> ShowS #

show :: Rewrite -> String #

showList :: [Rewrite] -> ShowS #

NFData Rewrite Source #

Instance details

Methods

rnf :: Rewrite -> () #

Eq Rewrite Source #

Instance details

Methods

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

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

Ord Rewrite Source #

Instance details

Methods

compare :: Rewrite -> Rewrite -> Ordering #

(<) :: Rewrite -> Rewrite -> Bool #

(<=) :: Rewrite -> Rewrite -> Bool #

(>) :: Rewrite -> Rewrite -> Bool #

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

max :: Rewrite -> Rewrite -> Rewrite #

min :: Rewrite -> Rewrite -> Rewrite #

Elaborate Rewrite Source #

Instance details

Methods

elaborate :: ElabParam -> Rewrite -> Rewrite Source #

Fixpoint Rewrite Source #

Instance details

Methods

toFix :: Rewrite -> Doc Source #

simplify :: Rewrite -> Rewrite Source #

PPrint Rewrite Source #

Instance details

Methods

pprintTidy :: Tidy -> Rewrite -> Doc Source #

pprintPrec :: Int -> Tidy -> Rewrite -> Doc Source #

ToHornSMT Rewrite Source #

Instance details

Methods

toHornSMT :: Rewrite -> Doc Source #

Foldable Rewrite Source #

Instance details

Methods

foldE :: Monoid a => Folder a c -> c -> Rewrite -> FoldM a Rewrite Source #

SymConsts Rewrite Source #

Instance details

Methods

symConsts :: Rewrite -> [SymConst] Source #

Visitable Rewrite Source #

Instance details

Methods

transE :: (Expr -> Expr) -> Rewrite -> Rewrite Source #

Store Rewrite Source #

Instance details

Methods

size :: Size Rewrite #

poke :: Rewrite -> Poke () #

peek :: Peek Rewrite #

type Rep Rewrite Source #

Instance details

type Rep Rewrite = D1 ('MetaData "Rewrite" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) (C1 ('MetaCons "SMeasure" 'PrefixI 'True) ((S1 ('MetaSel ('Just "smName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol) :*: S1 ('MetaSel ('Just "smDC") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol)) :*: (S1 ('MetaSel ('Just "smArgs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Symbol]) :*: S1 ('MetaSel ('Just "smBody") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))))

data AutoRewrite Source #

Constructors

AutoRewrite
Fields arArgs :: [SortedReft] arLHS :: Expr arRHS :: Expr

Instances

Instances details

Generic AutoRewrite Source #

Instance details

Associated Types

type Rep AutoRewrite

Instance details

type Rep AutoRewrite = D1 ('MetaData "AutoRewrite" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) (C1 ('MetaCons "AutoRewrite" 'PrefixI 'True) (S1 ('MetaSel ('Just "arArgs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SortedReft]) :*: (S1 ('MetaSel ('Just "arLHS") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Just "arRHS") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))))

Methods

from :: AutoRewrite -> Rep AutoRewrite x #

to :: Rep AutoRewrite x -> AutoRewrite #

Show AutoRewrite Source #

Instance details

Methods

showsPrec :: Int -> AutoRewrite -> ShowS #

show :: AutoRewrite -> String #

showList :: [AutoRewrite] -> ShowS #

NFData AutoRewrite Source #

Instance details

Methods

rnf :: AutoRewrite -> () #

Eq AutoRewrite Source #

Instance details

Methods

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

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

Ord AutoRewrite Source #

Instance details

Methods

compare :: AutoRewrite -> AutoRewrite -> Ordering #

(<) :: AutoRewrite -> AutoRewrite -> Bool #

(<=) :: AutoRewrite -> AutoRewrite -> Bool #

(>) :: AutoRewrite -> AutoRewrite -> Bool #

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

max :: AutoRewrite -> AutoRewrite -> AutoRewrite #

min :: AutoRewrite -> AutoRewrite -> AutoRewrite #

Hashable AutoRewrite Source #

Instance details

Methods

hashWithSalt :: Int -> AutoRewrite -> Int #

hash :: AutoRewrite -> Int #

Store AutoRewrite Source #

Instance details

Methods

size :: Size AutoRewrite #

poke :: AutoRewrite -> Poke () #

peek :: Peek AutoRewrite #

Fixpoint (HashMap SubcId [AutoRewrite]) Source #

Instance details

Methods

toFix :: HashMap SubcId [AutoRewrite] -> Doc Source #

simplify :: HashMap SubcId [AutoRewrite] -> HashMap SubcId [AutoRewrite] Source #

type Rep AutoRewrite Source #

Instance details

type Rep AutoRewrite = D1 ('MetaData "AutoRewrite" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'False) (C1 ('MetaCons "AutoRewrite" 'PrefixI 'True) (S1 ('MetaSel ('Just "arArgs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SortedReft]) :*: (S1 ('MetaSel ('Just "arLHS") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :*: S1 ('MetaSel ('Just "arRHS") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))))

dedupAutoRewrites :: HashMap SubcId [AutoRewrite] -> [AutoRewrite] Source #

newtype LocalRewritesEnv Source #

Constructors

LocalRewritesMap (HashMap BindId LocalRewrites)

Instances

Instances details

Monoid LocalRewritesEnv Source #

Instance details

Methods

mempty :: LocalRewritesEnv #

mappend :: LocalRewritesEnv -> LocalRewritesEnv -> LocalRewritesEnv #

mconcat :: [LocalRewritesEnv] -> LocalRewritesEnv #

Semigroup LocalRewritesEnv Source #

Instance details

Methods

(<>) :: LocalRewritesEnv -> LocalRewritesEnv -> LocalRewritesEnv #

sconcat :: NonEmpty LocalRewritesEnv -> LocalRewritesEnv #

stimes :: Integral b => b -> LocalRewritesEnv -> LocalRewritesEnv #

Generic LocalRewritesEnv Source #

Instance details

Associated Types

type Rep LocalRewritesEnv

Instance details

type Rep LocalRewritesEnv = D1 ('MetaData "LocalRewritesEnv" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'True) (C1 ('MetaCons "LocalRewritesMap" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap BindId LocalRewrites))))

Methods

from :: LocalRewritesEnv -> Rep LocalRewritesEnv x #

to :: Rep LocalRewritesEnv x -> LocalRewritesEnv #

Show LocalRewritesEnv Source #

Instance details

Methods

showsPrec :: Int -> LocalRewritesEnv -> ShowS #

show :: LocalRewritesEnv -> String #

showList :: [LocalRewritesEnv] -> ShowS #

NFData LocalRewritesEnv Source #

Instance details

Methods

rnf :: LocalRewritesEnv -> () #

Eq LocalRewritesEnv Source #

Instance details

Methods

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

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

Fixpoint LocalRewritesEnv Source #

Instance details

Methods

toFix :: LocalRewritesEnv -> Doc Source #

simplify :: LocalRewritesEnv -> LocalRewritesEnv Source #

Store LocalRewritesEnv Source #

Instance details

Methods

size :: Size LocalRewritesEnv #

poke :: LocalRewritesEnv -> Poke () #

peek :: Peek LocalRewritesEnv #

type Rep LocalRewritesEnv Source #

Instance details

type Rep LocalRewritesEnv = D1 ('MetaData "LocalRewritesEnv" "Language.Fixpoint.Types.Constraints" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" 'True) (C1 ('MetaCons "LocalRewritesMap" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap BindId LocalRewrites))))

newtype LocalRewrites Source #

Constructors

LocalRewrites (HashMap Symbol Expr)

Instances

Instances details

Monoid LocalRewrites Source #

Instance details

Methods

mempty :: LocalRewrites #

mappend :: LocalRewrites -> LocalRewrites -> LocalRewrites #

mconcat :: [LocalRewrites] -> LocalRewrites #

Semigroup LocalRewrites Source #

Instance details

Methods

(<>) :: LocalRewrites -> LocalRewrites -> LocalRewrites #

sconcat :: NonEmpty LocalRewrites -> LocalRewrites #

stimes :: Integral b => b -> LocalRewrites -> LocalRewrites #

Generic LocalRewrites Source #

Instance details