Safe Haskell	None
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 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

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 :: 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])
mkPoly :: Int -> 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

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

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 #
Binary Sub Source #
Instance details Defined in Language.Fixpoint.Types.Sorts Methods put :: Sub -> Put # get :: Get Sub # putList :: [Sub] -> Put #
NFData Sub Source #
Instance details Defined in Language.Fixpoint.Types.Sorts Methods rnf :: 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.8.0.2-EGSzGwrlcJrCaUaEYLNzOY" True) (C1 (MetaCons "Sub" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [(Int, Sort)])))

data FTycon Source #

Instances

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