liquid-fixpoint-0.9.2.5: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
Safe HaskellSafe-Inferred
LanguageHaskell98

Language.Fixpoint.Types.Sorts

Description

This module contains the data types, operations and serialization functions for representing Fixpoint's Horn and well-formedness constraints.

Synopsis

Fixpoint Types

data Sort Source #

Sorts ---------------------------------------------------------------------

Constructors

FInt 
FReal 
FNum

numeric kind for Num tyvars

FFrac

numeric kind for Fractional tyvars

FObj !Symbol

uninterpreted type

FVar !Int

fixpoint type variable

FFunc !Sort !Sort

function

FAbs !Int !Sort

type-abstraction

FTC !FTycon 
FApp !Sort !Sort

constructed type

Instances

Instances details
Data Sort Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

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

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

toConstr :: Sort -> Constr #

dataTypeOf :: Sort -> DataType #

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

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

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

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

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

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

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

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

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

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

Monoid Sort Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

mempty :: Sort #

mappend :: Sort -> Sort -> Sort #

mconcat :: [Sort] -> Sort #

Semigroup Sort Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

(<>) :: Sort -> Sort -> Sort #

sconcat :: NonEmpty Sort -> Sort #

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

Generic Sort Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Associated Types

type Rep Sort :: Type -> Type #

Methods

from :: Sort -> Rep Sort x #

to :: Rep Sort x -> Sort #

Show Sort Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

showsPrec :: Int -> Sort -> ShowS #

show :: Sort -> String #

showList :: [Sort] -> ShowS #

Binary Sort Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

put :: Sort -> Put #

get :: Get Sort #

putList :: [Sort] -> Put #

NFData Sort Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

rnf :: Sort -> () #

Eq Sort Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

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

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

Ord Sort Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

compare :: Sort -> Sort -> Ordering #

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

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

(>) :: Sort -> Sort -> Bool #

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

max :: Sort -> Sort -> Sort #

min :: Sort -> Sort -> Sort #

Hashable Sort Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

hashWithSalt :: Int -> Sort -> Int #

hash :: Sort -> Int #

Defunc Sort Source # 
Instance details

Defined in Language.Fixpoint.Defunctionalize

Methods

defunc :: Sort -> DF Sort Source #

Elaborate Sort Source # 
Instance details

Defined in Language.Fixpoint.SortCheck

Fixpoint Sort Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

PPrint Sort Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Store Sort Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

size :: Size Sort #

poke :: Sort -> Poke () #

peek :: Peek Sort #

Defunc (Symbol, Sort) Source # 
Instance details

Defined in Language.Fixpoint.Defunctionalize

Methods

defunc :: (Symbol, Sort) -> DF (Symbol, Sort) Source #

SMTLIB2 (Symbol, Sort) Source # 
Instance details

Defined in Language.Fixpoint.Smt.Serialize

Methods

smt2 :: SymEnv -> (Symbol, Sort) -> Builder Source #

Elaborate (Symbol, Sort) Source # 
Instance details

Defined in Language.Fixpoint.SortCheck

type Rep Sort Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

type Rep Sort = D1 ('MetaData "Sort" "Language.Fixpoint.Types.Sorts" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'False) (((C1 ('MetaCons "FInt" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FReal" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "FNum" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "FFrac" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FObj" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol))))) :+: ((C1 ('MetaCons "FVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int)) :+: C1 ('MetaCons "FFunc" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Sort) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Sort))) :+: (C1 ('MetaCons "FAbs" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Sort)) :+: (C1 ('MetaCons "FTC" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 FTycon)) :+: C1 ('MetaCons "FApp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Sort) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Sort))))))

newtype Sub Source #

Constructors

Sub [(Int, Sort)] 

Instances

Instances details
Generic Sub Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Associated Types

type Rep Sub :: Type -> Type #

Methods

from :: Sub -> Rep Sub x #

to :: Rep Sub x -> Sub #

NFData Sub Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

rnf :: Sub -> () #

Store Sub Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

size :: Size Sub #

poke :: Sub -> Poke () #

peek :: Peek Sub #

type Rep Sub Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

type Rep Sub = D1 ('MetaData "Sub" "Language.Fixpoint.Types.Sorts" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'True) (C1 ('MetaCons "Sub" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Int, Sort)])))

data FTycon Source #

Instances

Instances details
Data FTycon Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

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

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

toConstr :: FTycon -> Constr #

dataTypeOf :: FTycon -> DataType #

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

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

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

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

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

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

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

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

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

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

Generic FTycon Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Associated Types

type Rep FTycon :: Type -> Type #

Methods

from :: FTycon -> Rep FTycon x #

to :: Rep FTycon x -> FTycon #

Show FTycon Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Binary FTycon Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

put :: FTycon -> Put #

get :: Get FTycon #

putList :: [FTycon] -> Put #

NFData FTycon Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

rnf :: FTycon -> () #

Eq FTycon Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

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

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

Ord FTycon Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Hashable FTycon Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

hashWithSalt :: Int -> FTycon -> Int #

hash :: FTycon -> Int #

Symbolic FTycon Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

symbol :: FTycon -> Symbol Source #

Fixpoint FTycon Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

PPrint FTycon Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Loc FTycon Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Store FTycon Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

size :: Size FTycon #

poke :: FTycon -> Poke () #

peek :: Peek FTycon #

type Rep FTycon Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

type Rep FTycon

mapFVar :: (Int -> Int) -> Sort -> Sort Source #

intSort :: Sort Source #

Exported Basic Sorts -----------------------------------------------

realSort :: Sort Source #

Exported Basic Sorts -----------------------------------------------

boolSort :: Sort Source #

Exported Basic Sorts -----------------------------------------------

strSort :: Sort Source #

Exported Basic Sorts -----------------------------------------------

funcSort :: Sort Source #

Exported Basic Sorts -----------------------------------------------

charSort :: Sort Source #

Exported Basic Sorts -----------------------------------------------

fApp :: Sort -> [Sort] -> Sort Source #

unFApp :: Sort -> ListNE Sort Source #

fApp' (FApp (FApp Map key) val) ===> [Map, key, val] That is, fApp` is used to split a type application into the FTyCon and its args.

mkSortSubst :: [(Symbol, Sort)] -> SortSubst Source #

sortSubst :: SortSubst -> Sort -> Sort Source #

bkAbs :: Sort -> ([Int], Sort) Source #

User-defined ADTs

data DataField Source #

Constructors

DField 

Fields

Instances

Instances details
Data DataField Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

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

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

toConstr :: DataField -> Constr #

dataTypeOf :: DataField -> DataType #

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

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

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

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

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

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

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

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

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

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

Generic DataField Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Associated Types

type Rep DataField :: Type -> Type #

Show DataField Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

NFData DataField Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

rnf :: DataField -> () #

Eq DataField Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Ord DataField Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Symbolic DataField Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Fixpoint DataField Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

PPrint DataField Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Store DataField Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

type Rep DataField Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

type Rep DataField = D1 ('MetaData "DataField" "Language.Fixpoint.Types.Sorts" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'False) (C1 ('MetaCons "DField" 'PrefixI 'True) (S1 ('MetaSel ('Just "dfName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 LocSymbol) :*: S1 ('MetaSel ('Just "dfSort") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Sort)))

data DataCtor Source #

Constructors

DCtor 

Fields

Instances

Instances details
Data DataCtor Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

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

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

toConstr :: DataCtor -> Constr #

dataTypeOf :: DataCtor -> DataType #

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

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

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

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

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

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

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

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

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

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

Generic DataCtor Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Associated Types

type Rep DataCtor :: Type -> Type #

Methods

from :: DataCtor -> Rep DataCtor x #

to :: Rep DataCtor x -> DataCtor #

Show DataCtor Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

NFData DataCtor Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

rnf :: DataCtor -> () #

Eq DataCtor Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Ord DataCtor Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Symbolic DataCtor Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Fixpoint DataCtor Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

PPrint DataCtor Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Store DataCtor Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

type Rep DataCtor Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

type Rep DataCtor = D1 ('MetaData "DataCtor" "Language.Fixpoint.Types.Sorts" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'False) (C1 ('MetaCons "DCtor" 'PrefixI 'True) (S1 ('MetaSel ('Just "dcName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 LocSymbol) :*: S1 ('MetaSel ('Just "dcFields") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [DataField])))

data DataDecl Source #

Constructors

DDecl 

Fields

Instances

Instances details
Data DataDecl Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

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

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

toConstr :: DataDecl -> Constr #

dataTypeOf :: DataDecl -> DataType #

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

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

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

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

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

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

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

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

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

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

Generic DataDecl Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Associated Types

type Rep DataDecl :: Type -> Type #

Methods

from :: DataDecl -> Rep DataDecl x #

to :: Rep DataDecl x -> DataDecl #

Show DataDecl Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

NFData DataDecl Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

rnf :: DataDecl -> () #

Eq DataDecl Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Ord DataDecl Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Symbolic DataDecl Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Fixpoint DataDecl Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

PPrint DataDecl Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Loc DataDecl Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Store DataDecl Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

type Rep DataDecl Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

type Rep DataDecl = D1 ('MetaData "DataDecl" "Language.Fixpoint.Types.Sorts" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'False) (C1 ('MetaCons "DDecl" 'PrefixI 'True) (S1 ('MetaSel ('Just "ddTyCon") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 FTycon) :*: (S1 ('MetaSel ('Just "ddVars") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Just "ddCtors") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DataCtor]))))

Embedding Source types as Sorts

data TCEmb a Source #

Embedding stuff as Sorts

Instances

Instances details
(Data a, Hashable a) => Data (TCEmb a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

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

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

toConstr :: TCEmb a -> Constr #

dataTypeOf :: TCEmb a -> DataType #

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

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

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

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

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

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

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

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

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

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

(Eq a, Hashable a) => Monoid (TCEmb a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

mempty :: TCEmb a #

mappend :: TCEmb a -> TCEmb a -> TCEmb a #

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

(Eq a, Hashable a) => Semigroup (TCEmb a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

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

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

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

Generic (TCEmb a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Associated Types

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

Methods

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

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

Show a => Show (TCEmb a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

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

show :: TCEmb a -> String #

showList :: [TCEmb a] -> ShowS #

(Eq a, Hashable a, Binary (HashMap a (Sort, TCArgs))) => Binary (TCEmb a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

put :: TCEmb a -> Put #

get :: Get (TCEmb a) #

putList :: [TCEmb a] -> Put #

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

Defined in Language.Fixpoint.Types.Sorts

Methods

rnf :: TCEmb a -> () #

Eq a => Eq (TCEmb a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

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

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

Hashable a => Hashable (TCEmb a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

hashWithSalt :: Int -> TCEmb a -> Int #

hash :: TCEmb a -> Int #

PPrint a => PPrint (TCEmb a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

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

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

type Rep (TCEmb a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

type Rep (TCEmb a) = D1 ('MetaData "TCEmb" "Language.Fixpoint.Types.Sorts" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'True) (C1 ('MetaCons "TCE" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap a (Sort, TCArgs)))))

data TCArgs Source #

Constructors

WithArgs 
NoArgs 

Instances

Instances details
Data TCArgs Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

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

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

toConstr :: TCArgs -> Constr #

dataTypeOf :: TCArgs -> DataType #

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

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

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

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

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

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

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

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

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

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

Monoid TCArgs Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Semigroup TCArgs Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Generic TCArgs Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Associated Types

type Rep TCArgs :: Type -> Type #

Methods

from :: TCArgs -> Rep TCArgs x #

to :: Rep TCArgs x -> TCArgs #

Show TCArgs Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Binary TCArgs Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

put :: TCArgs -> Put #

get :: Get TCArgs #

putList :: [TCArgs] -> Put #

NFData TCArgs Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

rnf :: TCArgs -> () #

Eq TCArgs Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

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

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

Ord TCArgs Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Hashable TCArgs Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

hashWithSalt :: Int -> TCArgs -> Int #

hash :: TCArgs -> Int #

PPrint TCArgs Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Store TCArgs Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

size :: Size TCArgs #

poke :: TCArgs -> Poke () #

peek :: Peek TCArgs #

type Rep TCArgs Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

type Rep TCArgs = D1 ('MetaData "TCArgs" "Language.Fixpoint.Types.Sorts" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'False) (C1 ('MetaCons "WithArgs" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NoArgs" 'PrefixI 'False) (U1 :: Type -> Type))

tceLookup :: (Eq a, Hashable a) => a -> TCEmb a -> Maybe (Sort, TCArgs) Source #

tceFromList :: (Eq a, Hashable a) => [(a, (Sort, TCArgs))] -> TCEmb a Source #

tceToList :: TCEmb a -> [(a, (Sort, TCArgs))] Source #

tceMember :: (Eq a, Hashable a) => a -> TCEmb a -> Bool Source #

tceInsert :: (Eq a, Hashable a) => a -> Sort -> TCArgs -> TCEmb a -> TCEmb a Source #

tceInsertWith :: (Eq a, Hashable a) => (Sort -> Sort -> Sort) -> a -> Sort -> TCArgs -> TCEmb a -> TCEmb a Source #

tceMap :: (Eq b, Hashable b) => (a -> b) -> TCEmb a -> TCEmb b Source #