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

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

Defunc Sort

Methods

defunc :: Sort -> DF Sort

Elaborate (Symbol, Sort)

Methods

elaborate :: String -> SEnv Sort -> (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.6.0.1-5mWt9PUazXkTom8QgdiF2" 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.6.0.1-5mWt9PUazXkTom8QgdiF2" 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

Fixpoint FTycon

Methods

toFix :: FTycon -> Doc

simplify :: FTycon -> FTycon

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

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

isFirstOrder :: Sort -> Bool

mappendFTC :: FTycon -> FTycon -> FTycon

fTyconSymbol :: FTycon -> Located Symbol

symbolFTycon :: LocSymbol -> FTycon

fTyconSort :: FTycon -> Sort

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

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

fApp' :: Sort -> ListNE Sort

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

fObj :: LocSymbol -> 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