Language.Fixpoint.Types.Sorts

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.

Embedding to 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

Eq Sort

Methods

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

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

Data Sort

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

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

Methods

showsPrec :: Int -> Sort -> ShowS

show :: Sort -> String

showList :: [Sort] -> ShowS

Generic Sort

Associated Types

type Rep Sort :: * -> *

Methods

from :: Sort -> Rep Sort x

to :: Rep Sort x -> Sort

Monoid Sort

Methods

mempty :: Sort

mappend :: Sort -> Sort -> Sort

mconcat :: [Sort] -> Sort

Binary Sort

Methods

put :: Sort -> Put

get :: Get Sort

putList :: [Sort] -> Put

NFData Sort

Methods

rnf :: Sort -> ()

Hashable Sort

Methods

hashWithSalt :: Int -> Sort -> Int

hash :: Sort -> Int

Fixpoint Sort

Methods

toFix :: Sort -> Doc

simplify :: Sort -> Sort

Elaborate Sort

Methods

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

Defunc Sort

Methods

defunc :: Sort -> DF Sort

Elaborate (Symbol, Sort)

Methods

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

Defunc (Symbol, Sort)

Methods

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

type Rep Sort

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

newtype Sub

Constructors

Sub [(Int, Sort)]

Instances

Generic Sub

Associated Types

type Rep Sub :: * -> *

Methods

from :: Sub -> Rep Sub x

to :: Rep Sub x -> Sub

Binary Sub

Methods

put :: Sub -> Put

get :: Get Sub

putList :: [Sub] -> Put

NFData Sub

Methods

rnf :: Sub -> ()

type Rep Sub

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

data FTycon

Instances

Eq FTycon

Methods

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

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

Data FTycon

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

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

Show FTycon

Methods

showsPrec :: Int -> FTycon -> ShowS

show :: FTycon -> String

showList :: [FTycon] -> ShowS

Generic FTycon

Associated Types

type Rep FTycon :: * -> *

Methods

from :: FTycon -> Rep FTycon x

to :: Rep FTycon x -> FTycon

Binary FTycon

Methods

put :: FTycon -> Put

get :: Get FTycon

putList :: [FTycon] -> Put

NFData FTycon

Methods

rnf :: FTycon -> ()

Hashable FTycon

Methods

hashWithSalt :: Int -> FTycon -> Int

hash :: FTycon -> Int

PPrint FTycon

Methods

pprintTidy :: Tidy -> FTycon -> Doc

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

Fixpoint FTycon

Methods

toFix :: FTycon -> Doc

simplify :: FTycon -> FTycon

Loc FTycon

Methods

srcSpan :: FTycon -> SrcSpan

Symbolic FTycon

Methods

symbol :: FTycon -> Symbol

type Rep FTycon

type Rep FTycon

type TCEmb a = HashMap a FTycon

sortFTycon :: Sort -> Maybe FTycon

intFTyCon :: FTycon

boolFTyCon :: FTycon

realFTyCon :: FTycon

numFTyCon :: FTycon

strFTyCon :: FTycon

setFTyCon :: FTycon

mapFTyCon :: FTycon

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

mapSort :: Sort -> Sort -> Sort

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

sortSubst :: HashMap Symbol Sort -> Sort -> Sort

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

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

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

isNumeric :: Sort -> Bool

isReal :: Sort -> Bool

isString :: Sort -> Bool

isPolyInst :: Sort -> Sort -> Bool

User-defined ADTs

data DataField

Constructors

DField

Fields

• dfName :: !LocSymbol

  Field Name

• dfSort :: !Sort

  Field Sort

Instances

Eq DataField

Methods

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

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

Data DataField

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

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

Show DataField

Methods

showsPrec :: Int -> DataField -> ShowS

show :: DataField -> String

showList :: [DataField] -> ShowS

Generic DataField

Associated Types

type Rep DataField :: * -> *

Methods

from :: DataField -> Rep DataField x

to :: Rep DataField x -> DataField

Binary DataField

Methods

put :: DataField -> Put

get :: Get DataField

putList :: [DataField] -> Put

NFData DataField

Methods

rnf :: DataField -> ()

PPrint DataField

Methods

pprintTidy :: Tidy -> DataField -> Doc

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

Fixpoint DataField

Methods

toFix :: DataField -> Doc

simplify :: DataField -> DataField

Symbolic DataField

Methods

symbol :: DataField -> Symbol

type Rep DataField

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

data DataCtor

Constructors

DCtor

Fields

• dcName :: !LocSymbol

  Ctor Name

• dcFields :: ![DataField]

  Ctor Fields

Instances

Eq DataCtor

Methods

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

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

Data DataCtor

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

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

Show DataCtor

Methods

showsPrec :: Int -> DataCtor -> ShowS

show :: DataCtor -> String

showList :: [DataCtor] -> ShowS

Generic DataCtor

Associated Types

type Rep DataCtor :: * -> *

Methods

from :: DataCtor -> Rep DataCtor x

to :: Rep DataCtor x -> DataCtor

Binary DataCtor

Methods

put :: DataCtor -> Put

get :: Get DataCtor

putList :: [DataCtor] -> Put

NFData DataCtor

Methods

rnf :: DataCtor -> ()

PPrint DataCtor

Methods

pprintTidy :: Tidy -> DataCtor -> Doc

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

Fixpoint DataCtor

Methods

toFix :: DataCtor -> Doc

simplify :: DataCtor -> DataCtor

Symbolic DataCtor

Methods

symbol :: DataCtor -> Symbol

type Rep DataCtor

type Rep DataCtor = D1 (MetaData "DataCtor" "Language.Fixpoint.Types.Sorts" "liquid-fixpoint-0.7.0.5-Gva8geyEo6wB3a0li3tGtO" False) (C1 (MetaCons "DCtor" PrefixI True) ((:*:) (S1 (MetaSel (Just Symbol "dcName") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 LocSymbol)) (S1 (MetaSel (Just Symbol "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

Instances

Eq DataDecl

Methods

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

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

Data DataDecl

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

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

Show DataDecl

Methods

showsPrec :: Int -> DataDecl -> ShowS

show :: DataDecl -> String

showList :: [DataDecl] -> ShowS

Generic DataDecl

Associated Types

type Rep DataDecl :: * -> *

Methods

from :: DataDecl -> Rep DataDecl x

to :: Rep DataDecl x -> DataDecl

Binary DataDecl

Methods

put :: DataDecl -> Put

get :: Get DataDecl

putList :: [DataDecl] -> Put

NFData DataDecl

Methods

rnf :: DataDecl -> ()

PPrint DataDecl

Methods

pprintTidy :: Tidy -> DataDecl -> Doc

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

Fixpoint DataDecl

Methods

toFix :: DataDecl -> Doc

simplify :: DataDecl -> DataDecl

Symbolic DataDecl

Methods

symbol :: DataDecl -> Symbol

type Rep DataDecl

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