liquid-fixpoint-0.8.10.1: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver

Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Types.Sorts

Contents

Description

This module contains the data types, operations and serialization functions for representing Fixpoint's implication (i.e. subtyping) and well-formedness constraints in Haskell. The actual constraint solving is done by the `fixpoint.native` which is written in Ocaml.

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
Eq Sort Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

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

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

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 :: (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 #

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 #

Show Sort Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

showsPrec :: Int -> Sort -> ShowS #

show :: Sort -> String #

showList :: [Sort] -> ShowS #

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 #

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 #

Monoid Sort Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

mempty :: Sort #

mappend :: Sort -> Sort -> Sort #

mconcat :: [Sort] -> Sort #

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 -> () #

Hashable Sort Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

hashWithSalt :: Int -> Sort -> Int #

hash :: Sort -> Int #

PPrint Sort Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

Fixpoint Sort Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Elaborate Sort Source # 
Instance details

Defined in Language.Fixpoint.SortCheck

Defunc Sort Source # 
Instance details

Defined in Language.Fixpoint.Defunctionalize

Methods

defunc :: Sort -> DF 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

Defunc (Symbol, Sort) Source # 
Instance details

Defined in Language.Fixpoint.Defunctionalize

Methods

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

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.8.10.1-GurPN6vmwrs4cBOYBbkvBH" 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
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 #

Binary Sub Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

put :: Sub -> Put #

get :: Get Sub #

putList :: [Sub] -> Put #

NFData Sub Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

rnf :: 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.8.10.1-GurPN6vmwrs4cBOYBbkvBH" True) (C1 (MetaCons "Sub" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [(Int, Sort)])))

data FTycon Source #

Instances
Eq FTycon Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

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

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

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 :: (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 #

Ord FTycon Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Show FTycon Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

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 #

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 -> () #

Hashable FTycon Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

hashWithSalt :: Int -> FTycon -> Int #

hash :: FTycon -> Int #

PPrint FTycon Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Fixpoint FTycon Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Loc FTycon Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Symbolic FTycon Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

symbol :: FTycon -> Symbol Source #

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 #

User-defined ADTs

data DataField Source #

Constructors

DField 

Fields

Instances
Eq DataField Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

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 :: (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 #

Ord DataField Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Show DataField Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Generic DataField Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Associated Types

type Rep DataField :: Type -> Type #

Binary DataField Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

NFData DataField Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

rnf :: DataField -> () #

PPrint DataField Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Fixpoint DataField Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Symbolic 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.8.10.1-GurPN6vmwrs4cBOYBbkvBH" 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
Eq DataCtor Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

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 :: (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 #

Ord DataCtor Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Show DataCtor Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

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 #

Binary DataCtor Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

put :: DataCtor -> Put #

get :: Get DataCtor #

putList :: [DataCtor] -> Put #

NFData DataCtor Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

rnf :: DataCtor -> () #

PPrint DataCtor Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Fixpoint DataCtor Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Symbolic 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.8.10.1-GurPN6vmwrs4cBOYBbkvBH" 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
Eq DataDecl Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

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 :: (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 #

Ord DataDecl Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Show DataDecl Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

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 #

Binary DataDecl Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

put :: DataDecl -> Put #

get :: Get DataDecl #

putList :: [DataDecl] -> Put #

NFData DataDecl Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

rnf :: DataDecl -> () #

PPrint DataDecl Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Fixpoint DataDecl Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Loc DataDecl Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Symbolic 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.8.10.1-GurPN6vmwrs4cBOYBbkvBH" 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
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 #

(Data a, Eq 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 :: (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) #

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 #

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 #

(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 #

(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, Binary a) => Binary (TCEmb a) Source # 
Instance details

Defined in Language.Fixpoint.Types.Refinements

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 -> () #

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.Refinements

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.8.10.1-GurPN6vmwrs4cBOYBbkvBH" 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
Eq TCArgs Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Methods

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

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

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 :: (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 #

Ord TCArgs Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Show 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 #

Semigroup TCArgs Source # 
Instance details

Defined in Language.Fixpoint.Types.Sorts

Monoid 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 -> () #

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

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.8.10.1-GurPN6vmwrs4cBOYBbkvBH" 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 #