liquid-fixpoint-0.7.0.2: 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

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

Methods

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

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

Data Sort Source # 

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 # 

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 # 

Methods

showsPrec :: Int -> Sort -> ShowS #

show :: Sort -> String #

showList :: [Sort] -> ShowS #

Generic Sort Source # 

Associated Types

type Rep Sort :: * -> * #

Methods

from :: Sort -> Rep Sort x #

to :: Rep Sort x -> Sort #

Monoid Sort Source # 

Methods

mempty :: Sort #

mappend :: Sort -> Sort -> Sort #

mconcat :: [Sort] -> Sort #

Binary Sort Source # 

Methods

put :: Sort -> Put #

get :: Get Sort #

putList :: [Sort] -> Put #

NFData Sort Source # 

Methods

rnf :: Sort -> () #

Hashable Sort Source # 

Methods

hashWithSalt :: Int -> Sort -> Int #

hash :: Sort -> Int #

Fixpoint Sort Source # 
Elaborate Sort Source # 

Methods

elaborate :: String -> SymEnv -> Sort -> Sort Source #

Defunc Sort Source # 

Methods

defunc :: Sort -> DF Sort Source #

Elaborate (Symbol, Sort) Source # 

Methods

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

Defunc (Symbol, Sort) Source # 

Methods

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

type Rep Sort Source # 

newtype Sub Source #

Constructors

Sub [(Int, Sort)] 

Instances

Generic Sub Source # 

Associated Types

type Rep Sub :: * -> * #

Methods

from :: Sub -> Rep Sub x #

to :: Rep Sub x -> Sub #

Binary Sub Source # 

Methods

put :: Sub -> Put #

get :: Get Sub #

putList :: [Sub] -> Put #

NFData Sub Source # 

Methods

rnf :: Sub -> () #

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

data FTycon Source #

Instances

Eq FTycon Source # 

Methods

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

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

Data FTycon Source # 

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 # 
Show FTycon Source # 
Generic FTycon Source # 

Associated Types

type Rep FTycon :: * -> * #

Methods

from :: FTycon -> Rep FTycon x #

to :: Rep FTycon x -> FTycon #

Binary FTycon Source # 

Methods

put :: FTycon -> Put #

get :: Get FTycon #

putList :: [FTycon] -> Put #

NFData FTycon Source # 

Methods

rnf :: FTycon -> () #

Hashable FTycon Source # 

Methods

hashWithSalt :: Int -> FTycon -> Int #

hash :: FTycon -> Int #

PPrint FTycon Source # 
Fixpoint FTycon Source # 
Symbolic FTycon Source # 

Methods

symbol :: FTycon -> Symbol Source #

type Rep FTycon Source # 
type Rep FTycon

type TCEmb a = HashMap a FTycon Source #

sortFTycon :: Sort -> Maybe FTycon Source #

intFTyCon :: FTycon Source #

boolFTyCon :: FTycon Source #

realFTyCon :: FTycon Source #

numFTyCon :: FTycon Source #

strFTyCon :: FTycon Source #

setFTyCon :: FTycon Source #

mapFTyCon :: FTycon Source #

basicSorts :: [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 -----------------------------------------------

setSort :: Sort -> Sort Source #

bitVecSort :: Sort Source #

mapSort :: Sort -> Sort -> Sort Source #

listFTyCon :: FTycon Source #

isListTC :: FTycon -> Bool Source #

sizeBv :: FTycon -> Maybe Int Source #

isFirstOrder :: Sort -> Bool Source #

mappendFTC :: FTycon -> FTycon -> FTycon Source #

fTyconSymbol :: FTycon -> Located Symbol Source #

symbolFTycon :: LocSymbol -> FTycon Source #

fTyconSort :: FTycon -> Sort Source #

symbolNumInfoFTyCon :: LocSymbol -> Bool -> Bool -> FTycon Source #

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

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

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

unAbs :: Sort -> Sort Source #

sortSubst :: HashMap Symbol Sort -> Sort -> Sort Source #

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

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

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

isNumeric :: Sort -> Bool Source #

isReal :: Sort -> Bool Source #

isString :: Sort -> Bool Source #

User-defined ADTs

data DataField Source #

Constructors

DField 

Fields

Instances

Eq DataField Source # 
Data DataField Source # 

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 # 
Show DataField Source # 
Generic DataField Source # 

Associated Types

type Rep DataField :: * -> * #

Methods

from :: DataField -> Rep DataField x #

to :: Rep DataField x -> DataField #

Binary DataField Source # 
NFData DataField Source # 

Methods

rnf :: DataField -> () #

PPrint DataField Source # 
Fixpoint DataField Source # 
Symbolic DataField Source # 
type Rep DataField Source # 
type Rep DataField = D1 (MetaData "DataField" "Language.Fixpoint.Types.Sorts" "liquid-fixpoint-0.7.0.2-3repHVQ2bkqGganvJ6cFNP" 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 Source #

Constructors

DCtor 

Fields

Instances

Eq DataCtor Source # 
Data DataCtor Source # 

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 # 
Show DataCtor Source # 
Generic DataCtor Source # 

Associated Types

type Rep DataCtor :: * -> * #

Methods

from :: DataCtor -> Rep DataCtor x #

to :: Rep DataCtor x -> DataCtor #

Binary DataCtor Source # 

Methods

put :: DataCtor -> Put #

get :: Get DataCtor #

putList :: [DataCtor] -> Put #

NFData DataCtor Source # 

Methods

rnf :: DataCtor -> () #

PPrint DataCtor Source # 
Fixpoint DataCtor Source # 
Symbolic DataCtor Source # 
type Rep DataCtor Source # 
type Rep DataCtor = D1 (MetaData "DataCtor" "Language.Fixpoint.Types.Sorts" "liquid-fixpoint-0.7.0.2-3repHVQ2bkqGganvJ6cFNP" 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 Source #

Constructors

DDecl 

Fields

Instances

Eq DataDecl Source # 
Data DataDecl Source # 

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 # 
Show DataDecl Source # 
Generic DataDecl Source # 

Associated Types

type Rep DataDecl :: * -> * #

Methods

from :: DataDecl -> Rep DataDecl x #

to :: Rep DataDecl x -> DataDecl #

Binary DataDecl Source # 

Methods

put :: DataDecl -> Put #

get :: Get DataDecl #

putList :: [DataDecl] -> Put #

NFData DataDecl Source # 

Methods

rnf :: DataDecl -> () #

PPrint DataDecl Source # 
Fixpoint DataDecl Source # 
Symbolic DataDecl Source # 
type Rep DataDecl Source # 
type Rep DataDecl = D1 (MetaData "DataDecl" "Language.Fixpoint.Types.Sorts" "liquid-fixpoint-0.7.0.2-3repHVQ2bkqGganvJ6cFNP" 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])))))