Language.Fixpoint.Types.Sorts

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

Fixpoint Types

data Sort

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

FromJSON Sort

Defined in Language.Fixpoint.Types.Sorts

Methods

parseJSON :: Value -> Parser Sort

parseJSONList :: Value -> Parser [Sort]

omittedField :: Maybe Sort

ToJSON Sort

Defined in Language.Fixpoint.Types.Sorts

Methods

toJSON :: Sort -> Value

toEncoding :: Sort -> Encoding

toJSONList :: [Sort] -> Value

toEncodingList :: [Sort] -> Encoding

omitField :: Sort -> Bool

Data Sort

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

Defined in Language.Fixpoint.Types.Sorts

Methods

mempty :: Sort

mappend :: Sort -> Sort -> Sort

mconcat :: [Sort] -> Sort

Semigroup Sort

Defined in Language.Fixpoint.Types.Sorts

Methods

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

sconcat :: NonEmpty Sort -> Sort

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

Generic Sort

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

Defined in Language.Fixpoint.Types.Sorts

Methods

showsPrec :: Int -> Sort -> ShowS

show :: Sort -> String

showList :: [Sort] -> ShowS

Binary Sort

Defined in Language.Fixpoint.Types.Sorts

Methods

put :: Sort -> Put

get :: Get Sort

putList :: [Sort] -> Put

NFData Sort

Defined in Language.Fixpoint.Types.Sorts

Methods

rnf :: Sort -> ()

Eq Sort

Defined in Language.Fixpoint.Types.Sorts

Methods

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

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

Ord Sort

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

Defined in Language.Fixpoint.Types.Sorts

Methods

hashWithSalt :: Int -> Sort -> Int

hash :: Sort -> Int

Defunc Sort

Defined in Language.Fixpoint.Defunctionalize

Methods

defunc :: Sort -> DF Sort

ToHornSMT Sort

Defined in Language.Fixpoint.Horn.Types

Methods

toHornSMT :: Sort -> Doc

Elaborate Sort

Defined in Language.Fixpoint.SortCheck

Methods

elaborate :: Located String -> SymEnv -> Sort -> Sort

Fixpoint Sort

Defined in Language.Fixpoint.Types.Sorts

Methods

toFix :: Sort -> Doc

simplify :: Sort -> Sort

PPrint Sort

Defined in Language.Fixpoint.Types.Sorts

Methods

pprintTidy :: Tidy -> Sort -> Doc

pprintPrec :: Int -> Tidy -> Sort -> Doc

Store Sort

Defined in Language.Fixpoint.Types.Sorts

Methods

size :: Size Sort

poke :: Sort -> Poke ()

peek :: Peek Sort

Defunc (Symbol, Sort)

Defined in Language.Fixpoint.Defunctionalize

Methods

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

SMTLIB2 (Symbol, Sort)

Defined in Language.Fixpoint.Smt.Serialize

Methods

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

Elaborate (Symbol, Sort)

Defined in Language.Fixpoint.SortCheck

Methods

elaborate :: Located String -> SymEnv -> (Symbol, Sort) -> (Symbol, Sort)

type Rep Sort

Defined in Language.Fixpoint.Types.Sorts

type Rep Sort = D1 ('MetaData "Sort" "Language.Fixpoint.Types.Sorts" "liquid-fixpoint-0.9.6.3.1-BCIWdTkZFz53NySssdlA6L" '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

Constructors

Sub [(Int, Sort)]

Instances

Generic Sub

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

Defined in Language.Fixpoint.Types.Sorts

Methods

rnf :: Sub -> ()

Store Sub

Defined in Language.Fixpoint.Types.Sorts

Methods

size :: Size Sub

poke :: Sub -> Poke ()

peek :: Peek Sub

type Rep Sub

Defined in Language.Fixpoint.Types.Sorts

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

data FTycon

Instances

FromJSON FTycon

Defined in Language.Fixpoint.Types.Sorts

Methods

parseJSON :: Value -> Parser FTycon

parseJSONList :: Value -> Parser [FTycon]

omittedField :: Maybe FTycon

ToJSON FTycon

Defined in Language.Fixpoint.Types.Sorts

Methods

toJSON :: FTycon -> Value

toEncoding :: FTycon -> Encoding

toJSONList :: [FTycon] -> Value

toEncodingList :: [FTycon] -> Encoding

omitField :: FTycon -> Bool

Data FTycon

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

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

Defined in Language.Fixpoint.Types.Sorts

Methods

showsPrec :: Int -> FTycon -> ShowS

show :: FTycon -> String

showList :: [FTycon] -> ShowS

Binary FTycon

Defined in Language.Fixpoint.Types.Sorts

Methods

put :: FTycon -> Put

get :: Get FTycon

putList :: [FTycon] -> Put

NFData FTycon

Defined in Language.Fixpoint.Types.Sorts

Methods

rnf :: FTycon -> ()

Eq FTycon

Defined in Language.Fixpoint.Types.Sorts

Methods

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

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

Ord FTycon

Defined in Language.Fixpoint.Types.Sorts

Methods

compare :: FTycon -> FTycon -> Ordering

(<) :: FTycon -> FTycon -> Bool

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

(>) :: FTycon -> FTycon -> Bool

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

max :: FTycon -> FTycon -> FTycon

min :: FTycon -> FTycon -> FTycon

Hashable FTycon

Defined in Language.Fixpoint.Types.Sorts

Methods

hashWithSalt :: Int -> FTycon -> Int

hash :: FTycon -> Int

ToHornSMT FTycon

Defined in Language.Fixpoint.Horn.Types

Methods

toHornSMT :: FTycon -> Doc

Symbolic FTycon

Defined in Language.Fixpoint.Types.Sorts

Methods

symbol :: FTycon -> Symbol

Fixpoint FTycon

Defined in Language.Fixpoint.Types.Sorts

Methods

toFix :: FTycon -> Doc

simplify :: FTycon -> FTycon

PPrint FTycon

Defined in Language.Fixpoint.Types.Sorts

Methods

pprintTidy :: Tidy -> FTycon -> Doc

pprintPrec :: Int -> Tidy -> FTycon -> Doc

Loc FTycon

Defined in Language.Fixpoint.Types.Sorts

Methods

srcSpan :: FTycon -> SrcSpan

Store FTycon

Defined in Language.Fixpoint.Types.Sorts

Methods

size :: Size FTycon

poke :: FTycon -> Poke ()

peek :: Peek FTycon

type Rep FTycon

Defined in Language.Fixpoint.Types.Sorts

type Rep FTycon

sortFTycon :: Sort -> Maybe FTycon

intFTyCon :: FTycon

boolFTyCon :: FTycon

realFTyCon :: FTycon

numFTyCon :: FTycon

strFTyCon :: FTycon

setFTyCon :: FTycon

mapFTyCon :: FTycon

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

basicSorts :: [Sort]

intSort :: Sort

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

realSort :: Sort

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

boolSort :: Sort

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

strSort :: Sort

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

funcSort :: Sort

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

setSort :: Sort -> Sort

bitVecSort :: Int -> Sort

arraySort :: Sort -> Sort -> Sort

sizedBitVecSort :: Symbol -> Sort

mapSort :: Sort -> Sort -> Sort

charSort :: Sort

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

listFTyCon :: FTycon

isListTC :: FTycon -> Bool

sizeBv :: FTycon -> Maybe Int

isFirstOrder :: Sort -> Bool

mappendFTC :: FTycon -> FTycon -> FTycon

fTyconSymbol :: FTycon -> Located Symbol

symbolFTycon :: LocSymbol -> FTycon

fTyconSort :: FTycon -> Sort

symbolNumInfoFTyCon :: LocSymbol -> Bool -> Bool -> FTycon

fTyconSelfSort :: FTycon -> Int -> Sort

fApp :: Sort -> [Sort] -> Sort

fAppTC :: FTycon -> [Sort] -> Sort

fObj :: LocSymbol -> Sort

unFApp :: Sort -> ListNE Sort

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.

unAbs :: Sort -> Sort

sortAbs :: Sort -> Int

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

sortSubst :: SortSubst -> Sort -> Sort

functionSort :: Sort -> Maybe ([Int], [Sort], Sort)

mkFFunc :: Int -> [Sort] -> Sort

bkFFunc :: Sort -> Maybe (Int, [Sort])

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

mkPoly :: Int -> Sort -> Sort

sortSymbols :: Sort -> HashSet Symbol

substSort :: (Symbol -> Sort) -> Sort -> Sort

isBool :: Sort -> Bool

isNumeric :: Sort -> Bool

isReal :: Sort -> Bool

isString :: Sort -> Bool

isSet :: Sort -> Bool

isArray :: Sort -> Bool

isPolyInst :: Sort -> Sort -> Bool

User-defined ADTs

data DataField

Constructors

DField

Fields

• dfName :: !LocSymbol

  Field Name

• dfSort :: !Sort

  Field Sort

Instances

FromJSON DataField

Defined in Language.Fixpoint.Types.Sorts

Methods

parseJSON :: Value -> Parser DataField

parseJSONList :: Value -> Parser [DataField]

omittedField :: Maybe DataField

ToJSON DataField

Defined in Language.Fixpoint.Types.Sorts

Methods

toJSON :: DataField -> Value

toEncoding :: DataField -> Encoding

toJSONList :: [DataField] -> Value

toEncodingList :: [DataField] -> Encoding

omitField :: DataField -> Bool

Data DataField

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

Defined in Language.Fixpoint.Types.Sorts

Associated Types

type Rep DataField :: Type -> Type

Methods

from :: DataField -> Rep DataField x

to :: Rep DataField x -> DataField

Show DataField

Defined in Language.Fixpoint.Types.Sorts

Methods

showsPrec :: Int -> DataField -> ShowS

show :: DataField -> String

showList :: [DataField] -> ShowS

NFData DataField

Defined in Language.Fixpoint.Types.Sorts

Methods

rnf :: DataField -> ()

Eq DataField

Defined in Language.Fixpoint.Types.Sorts

Methods

(==) :: DataField -> DataField -> Bool

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

Ord DataField

Defined in Language.Fixpoint.Types.Sorts

Methods

compare :: DataField -> DataField -> Ordering

(<) :: DataField -> DataField -> Bool

(<=) :: DataField -> DataField -> Bool

(>) :: DataField -> DataField -> Bool

(>=) :: DataField -> DataField -> Bool

max :: DataField -> DataField -> DataField

min :: DataField -> DataField -> DataField

ToHornSMT DataField

Defined in Language.Fixpoint.Horn.Types

Methods

toHornSMT :: DataField -> Doc

Symbolic DataField

Defined in Language.Fixpoint.Types.Sorts

Methods

symbol :: DataField -> Symbol

Fixpoint DataField

Defined in Language.Fixpoint.Types.Sorts

Methods

toFix :: DataField -> Doc

simplify :: DataField -> DataField

PPrint DataField

Defined in Language.Fixpoint.Types.Sorts

Methods

pprintTidy :: Tidy -> DataField -> Doc

pprintPrec :: Int -> Tidy -> DataField -> Doc

Store DataField

Defined in Language.Fixpoint.Types.Sorts

Methods

size :: Size DataField

poke :: DataField -> Poke ()

peek :: Peek DataField

type Rep DataField

Defined in Language.Fixpoint.Types.Sorts

type Rep DataField = D1 ('MetaData "DataField" "Language.Fixpoint.Types.Sorts" "liquid-fixpoint-0.9.6.3.1-BCIWdTkZFz53NySssdlA6L" '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

Constructors

DCtor

Fields

• dcName :: !LocSymbol

  Ctor Name

• dcFields :: ![DataField]

  Ctor Fields

Instances

FromJSON DataCtor

Defined in Language.Fixpoint.Types.Sorts

Methods

parseJSON :: Value -> Parser DataCtor

parseJSONList :: Value -> Parser [DataCtor]

omittedField :: Maybe DataCtor

ToJSON DataCtor

Defined in Language.Fixpoint.Types.Sorts

Methods

toJSON :: DataCtor -> Value

toEncoding :: DataCtor -> Encoding

toJSONList :: [DataCtor] -> Value

toEncodingList :: [DataCtor] -> Encoding

omitField :: DataCtor -> Bool

Data DataCtor

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

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

Defined in Language.Fixpoint.Types.Sorts

Methods

showsPrec :: Int -> DataCtor -> ShowS

show :: DataCtor -> String

showList :: [DataCtor] -> ShowS

NFData DataCtor

Defined in Language.Fixpoint.Types.Sorts

Methods

rnf :: DataCtor -> ()

Eq DataCtor

Defined in Language.Fixpoint.Types.Sorts

Methods

(==) :: DataCtor -> DataCtor -> Bool

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

Ord DataCtor

Defined in Language.Fixpoint.Types.Sorts

Methods

compare :: DataCtor -> DataCtor -> Ordering

(<) :: DataCtor -> DataCtor -> Bool

(<=) :: DataCtor -> DataCtor -> Bool

(>) :: DataCtor -> DataCtor -> Bool

(>=) :: DataCtor -> DataCtor -> Bool

max :: DataCtor -> DataCtor -> DataCtor

min :: DataCtor -> DataCtor -> DataCtor

ToHornSMT DataCtor

Defined in Language.Fixpoint.Horn.Types

Methods

toHornSMT :: DataCtor -> Doc

Symbolic DataCtor

Defined in Language.Fixpoint.Types.Sorts

Methods

symbol :: DataCtor -> Symbol

Fixpoint DataCtor

Defined in Language.Fixpoint.Types.Sorts

Methods

toFix :: DataCtor -> Doc

simplify :: DataCtor -> DataCtor

PPrint DataCtor

Defined in Language.Fixpoint.Types.Sorts

Methods

pprintTidy :: Tidy -> DataCtor -> Doc

pprintPrec :: Int -> Tidy -> DataCtor -> Doc

Store DataCtor

Defined in Language.Fixpoint.Types.Sorts

Methods

size :: Size DataCtor

poke :: DataCtor -> Poke ()

peek :: Peek DataCtor

type Rep DataCtor

Defined in Language.Fixpoint.Types.Sorts

type Rep DataCtor = D1 ('MetaData "DataCtor" "Language.Fixpoint.Types.Sorts" "liquid-fixpoint-0.9.6.3.1-BCIWdTkZFz53NySssdlA6L" '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

Constructors

DDecl

Fields

• ddTyCon :: !FTycon

  Name of defined datatype

• ddVars :: !Int

  Number of type variables

• ddCtors :: [DataCtor]

  Datatype Ctors. Invariant: type variables bound in ctors are greater than ddVars

Instances

FromJSON DataDecl

Defined in Language.Fixpoint.Types.Sorts

Methods

parseJSON :: Value -> Parser DataDecl

parseJSONList :: Value -> Parser [DataDecl]

omittedField :: Maybe DataDecl

ToJSON DataDecl

Defined in Language.Fixpoint.Types.Sorts

Methods

toJSON :: DataDecl -> Value

toEncoding :: DataDecl -> Encoding

toJSONList :: [DataDecl] -> Value

toEncodingList :: [DataDecl] -> Encoding

omitField :: DataDecl -> Bool

Data DataDecl

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

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

Defined in Language.Fixpoint.Types.Sorts

Methods

showsPrec :: Int -> DataDecl -> ShowS

show :: DataDecl -> String

showList :: [DataDecl] -> ShowS

NFData DataDecl

Defined in Language.Fixpoint.Types.Sorts

Methods

rnf :: DataDecl -> ()

Eq DataDecl

Defined in Language.Fixpoint.Types.Sorts

Methods

(==) :: DataDecl -> DataDecl -> Bool

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

Ord DataDecl

Defined in Language.Fixpoint.Types.Sorts

Methods

compare :: DataDecl -> DataDecl -> Ordering

(<) :: DataDecl -> DataDecl -> Bool

(<=) :: DataDecl -> DataDecl -> Bool

(>) :: DataDecl -> DataDecl -> Bool

(>=) :: DataDecl -> DataDecl -> Bool

max :: DataDecl -> DataDecl -> DataDecl

min :: DataDecl -> DataDecl -> DataDecl

ToHornSMT DataDecl

Defined in Language.Fixpoint.Horn.Types

Methods

toHornSMT :: DataDecl -> Doc

Symbolic DataDecl

Defined in Language.Fixpoint.Types.Sorts

Methods

symbol :: DataDecl -> Symbol

Fixpoint DataDecl

Defined in Language.Fixpoint.Types.Sorts

Methods

toFix :: DataDecl -> Doc

simplify :: DataDecl -> DataDecl

PPrint DataDecl

Defined in Language.Fixpoint.Types.Sorts

Methods

pprintTidy :: Tidy -> DataDecl -> Doc

pprintPrec :: Int -> Tidy -> DataDecl -> Doc

Loc DataDecl

Defined in Language.Fixpoint.Types.Sorts

Methods

srcSpan :: DataDecl -> SrcSpan

Store DataDecl

Defined in Language.Fixpoint.Types.Sorts

Methods

size :: Size DataDecl

poke :: DataDecl -> Poke ()

peek :: Peek DataDecl

type Rep DataDecl

Defined in Language.Fixpoint.Types.Sorts

type Rep DataDecl = D1 ('MetaData "DataDecl" "Language.Fixpoint.Types.Sorts" "liquid-fixpoint-0.9.6.3.1-BCIWdTkZFz53NySssdlA6L" '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]))))

muSort :: [DataDecl] -> [DataDecl]

Embedding Source types as Sorts

data TCEmb a

Embedding stuff as Sorts

Instances

(Data a, Hashable a) => Data (TCEmb a)

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)

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)

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)

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)

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)

Defined in Language.Fixpoint.Types.Sorts

Methods

put :: TCEmb a -> Put

get :: Get (TCEmb a)

putList :: [TCEmb a] -> Put

NFData a => NFData (TCEmb a)

Defined in Language.Fixpoint.Types.Sorts

Methods

rnf :: TCEmb a -> ()

Eq a => Eq (TCEmb a)

Defined in Language.Fixpoint.Types.Sorts

Methods

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

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

Hashable a => Hashable (TCEmb a)

Defined in Language.Fixpoint.Types.Sorts

Methods

hashWithSalt :: Int -> TCEmb a -> Int

hash :: TCEmb a -> Int

PPrint a => PPrint (TCEmb a)

Defined in Language.Fixpoint.Types.Sorts

Methods

pprintTidy :: Tidy -> TCEmb a -> Doc

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

type Rep (TCEmb a)

Defined in Language.Fixpoint.Types.Sorts

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

data TCArgs

Constructors

WithArgs

NoArgs

Instances

Data TCArgs

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

Defined in Language.Fixpoint.Types.Sorts

Methods

mempty :: TCArgs

mappend :: TCArgs -> TCArgs -> TCArgs

mconcat :: [TCArgs] -> TCArgs

Semigroup TCArgs

Defined in Language.Fixpoint.Types.Sorts

Methods

(<>) :: TCArgs -> TCArgs -> TCArgs

sconcat :: NonEmpty TCArgs -> TCArgs

stimes :: Integral b => b -> TCArgs -> TCArgs

Generic TCArgs

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

Defined in Language.Fixpoint.Types.Sorts

Methods

showsPrec :: Int -> TCArgs -> ShowS

show :: TCArgs -> String

showList :: [TCArgs] -> ShowS

Binary TCArgs

Defined in Language.Fixpoint.Types.Sorts

Methods

put :: TCArgs -> Put

get :: Get TCArgs

putList :: [TCArgs] -> Put

NFData TCArgs

Defined in Language.Fixpoint.Types.Sorts

Methods

rnf :: TCArgs -> ()

Eq TCArgs

Defined in Language.Fixpoint.Types.Sorts

Methods

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

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

Ord TCArgs

Defined in Language.Fixpoint.Types.Sorts

Methods

compare :: TCArgs -> TCArgs -> Ordering

(<) :: TCArgs -> TCArgs -> Bool

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

(>) :: TCArgs -> TCArgs -> Bool

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

max :: TCArgs -> TCArgs -> TCArgs

min :: TCArgs -> TCArgs -> TCArgs

Hashable TCArgs

Defined in Language.Fixpoint.Types.Sorts

Methods

hashWithSalt :: Int -> TCArgs -> Int

hash :: TCArgs -> Int

PPrint TCArgs

Defined in Language.Fixpoint.Types.Sorts

Methods

pprintTidy :: Tidy -> TCArgs -> Doc

pprintPrec :: Int -> Tidy -> TCArgs -> Doc

Store TCArgs

Defined in Language.Fixpoint.Types.Sorts

Methods

size :: Size TCArgs

poke :: TCArgs -> Poke ()

peek :: Peek TCArgs

type Rep TCArgs

Defined in Language.Fixpoint.Types.Sorts

type Rep TCArgs = D1 ('MetaData "TCArgs" "Language.Fixpoint.Types.Sorts" "liquid-fixpoint-0.9.6.3.1-BCIWdTkZFz53NySssdlA6L" '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)

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

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

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

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

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

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

Sort coercion for SMT theory encoding

coerceSetToArray :: Sort -> Sort

Sort coercion for SMT theory encoding