Safe Haskell	Safe-Inferred
Language	Haskell98

Language.Fixpoint.Types.Sorts

Contents

Fixpoint Types
User-defined ADTs
Embedding Source types as Sorts

Description

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

Synopsis

data Sort
- = FInt
- | FReal
- | FNum
- | FFrac
- | FObj !Symbol
- | FVar !Int
- | FFunc !Sort !Sort
- | FAbs !Int !Sort
- | FTC !FTycon
- | FApp !Sort !Sort
newtype Sub = Sub [(Int, Sort)]
data 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
realSort :: Sort
boolSort :: Sort
strSort :: Sort
funcSort :: Sort
setSort :: Sort -> Sort
bitVecSort :: Int -> Sort
sizedBitVecSort :: Symbol -> Sort
mapSort :: Sort -> Sort -> Sort
charSort :: 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
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
isNumeric :: Sort -> Bool
isReal :: Sort -> Bool
isString :: Sort -> Bool
isPolyInst :: Sort -> Sort -> Bool
data DataField = DField {
- dfName :: !LocSymbol
- dfSort :: !Sort
}
data DataCtor = DCtor {
- dcName :: !LocSymbol
- dcFields :: ![DataField]
}
data DataDecl = DDecl {
- ddTyCon :: !FTycon
- ddVars :: !Int
- ddCtors :: [DataCtor]
}
muSort :: [DataDecl] -> [DataDecl]
data TCEmb a
data TCArgs
- = WithArgs
- | NoArgs
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

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

Instances details

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 :: 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 Source #
Instance details Defined in Language.Fixpoint.Types.Sorts Methods mempty :: Sort # mappend :: Sort -> Sort -> Sort # mconcat :: [Sort] -> 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 #
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 #
Show Sort Source #
Instance details Defined in Language.Fixpoint.Types.Sorts Methods showsPrec :: Int -> Sort -> ShowS # show :: Sort -> String # showList :: [Sort] -> ShowS #
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 -> () #
Eq Sort Source #
Instance details Defined in Language.Fixpoint.Types.Sorts Methods (==) :: Sort -> Sort -> Bool # (/=) :: Sort -> Sort -> Bool #
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 #
Hashable Sort Source #
Instance details Defined in Language.Fixpoint.Types.Sorts Methods hashWithSalt :: Int -> Sort -> Int # hash :: Sort -> Int #
Defunc Sort Source #
Instance details Defined in Language.Fixpoint.Defunctionalize Methods defunc :: Sort -> DF Sort Source #
Elaborate Sort Source #
Instance details Defined in Language.Fixpoint.SortCheck Methods elaborate :: Located String -> SymEnv -> Sort -> Sort Source #
Fixpoint Sort Source #
Instance details Defined in Language.Fixpoint.Types.Sorts Methods toFix :: Sort -> Doc Source # simplify :: Sort -> Sort Source #
PPrint Sort Source #
Instance details Defined in Language.Fixpoint.Types.Sorts Methods pprintTidy :: Tidy -> Sort -> Doc Source # pprintPrec :: Int -> Tidy -> Sort -> Doc Source #
Store Sort Source #
Instance details Defined in Language.Fixpoint.Types.Sorts Methods size :: Size Sort # poke :: Sort -> Poke () # peek :: Peek Sort #
Defunc (Symbol, Sort) Source #
Instance details Defined in Language.Fixpoint.Defunctionalize Methods defunc :: (Symbol, Sort) -> DF (Symbol, 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 Methods elaborate :: Located String -> SymEnv -> (Symbol, Sort) -> (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.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" '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

Instances details

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 #
NFData Sub Source #
Instance details Defined in Language.Fixpoint.Types.Sorts Methods rnf :: Sub -> () #
Store Sub Source #
Instance details Defined in Language.Fixpoint.Types.Sorts Methods size :: Size Sub # poke :: Sub -> Poke () # peek :: Peek 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.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'True) (C1 ('MetaCons "Sub" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Int, Sort)])))

data FTycon Source #

Instances

Instances details

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 :: 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 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 #
Show FTycon Source #
Instance details Defined in Language.Fixpoint.Types.Sorts Methods showsPrec :: Int -> FTycon -> ShowS # show :: FTycon -> String # showList :: [FTycon] -> ShowS #
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 -> () #
Eq FTycon Source #
Instance details Defined in Language.Fixpoint.Types.Sorts Methods (==) :: FTycon -> FTycon -> Bool # (/=) :: FTycon -> FTycon -> Bool #
Ord FTycon Source #
Instance details 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 Source #
Instance details Defined in Language.Fixpoint.Types.Sorts Methods hashWithSalt :: Int -> FTycon -> Int # hash :: FTycon -> Int #
Symbolic FTycon Source #
Instance details Defined in Language.Fixpoint.Types.Sorts Methods symbol :: FTycon -> Symbol Source #
Fixpoint FTycon Source #
Instance details Defined in Language.Fixpoint.Types.Sorts Methods toFix :: FTycon -> Doc Source # simplify :: FTycon -> FTycon Source #
PPrint FTycon Source #
Instance details Defined in Language.Fixpoint.Types.Sorts Methods pprintTidy :: Tidy -> FTycon -> Doc Source # pprintPrec :: Int -> Tidy -> FTycon -> Doc Source #
Loc FTycon Source #
Instance details Defined in Language.Fixpoint.Types.Sorts Methods srcSpan :: FTycon -> SrcSpan Source #
Store FTycon Source #
Instance details Defined in Language.Fixpoint.Types.Sorts Methods size :: Size FTycon # poke :: FTycon -> Poke () # peek :: Peek FTycon #
type Rep FTycon Source #
Instance details Defined in Language.Fixpoint.Types.Sorts type Rep FTycon

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 #

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

basicSorts :: [Sort] Source #

intSort :: Sort Source #