Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell98 |
This module contains the data types, operations and serialization functions for representing Fixpoint's Horn and well-formedness constraints.
Synopsis
- data 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 {}
- data DataCtor = DCtor {}
- data DataDecl = DDecl {}
- muSort :: [DataDecl] -> [DataDecl]
- data TCEmb a
- data TCArgs
- 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
Sorts ---------------------------------------------------------------------
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
Data FTycon Source # | |
Defined in Language.Fixpoint.Types.Sorts 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 # | |
Show FTycon Source # | |
Binary FTycon Source # | |
NFData FTycon Source # | |
Defined in Language.Fixpoint.Types.Sorts | |
Eq FTycon Source # | |
Ord FTycon Source # | |
Hashable FTycon Source # | |
Defined in Language.Fixpoint.Types.Sorts | |
Symbolic FTycon Source # | |
Fixpoint FTycon Source # | |
PPrint FTycon Source # | |
Defined in Language.Fixpoint.Types.Sorts | |
Loc FTycon Source # | |
Store FTycon Source # | |
type Rep FTycon Source # | |
Defined in Language.Fixpoint.Types.Sorts |
boolFTyCon :: FTycon Source #
realFTyCon :: FTycon Source #
basicSorts :: [Sort] Source #
bitVecSort :: Int -> Sort Source #
sizedBitVecSort :: Symbol -> Sort Source #
listFTyCon :: FTycon Source #
isFirstOrder :: Sort -> Bool Source #
symbolFTycon :: LocSymbol -> FTycon Source #
fTyconSort :: FTycon -> Sort Source #
mkSortSubst :: [(Symbol, Sort)] -> SortSubst Source #
User-defined ADTs
Instances
Data DataField Source # | |
Defined in Language.Fixpoint.Types.Sorts 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 :: forall r r'. (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 # | |
Generic DataField Source # | |
Show DataField Source # | |
NFData DataField Source # | |
Defined in Language.Fixpoint.Types.Sorts | |
Eq DataField Source # | |
Ord DataField Source # | |
Defined in Language.Fixpoint.Types.Sorts | |
Symbolic DataField Source # | |
Fixpoint DataField Source # | |
PPrint DataField Source # | |
Defined in Language.Fixpoint.Types.Sorts | |
Store DataField Source # | |
type Rep DataField Source # | |
Defined in Language.Fixpoint.Types.Sorts type Rep DataField = D1 ('MetaData "DataField" "Language.Fixpoint.Types.Sorts" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'False) (C1 ('MetaCons "DField" 'PrefixI 'True) (S1 ('MetaSel ('Just "dfName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 LocSymbol) :*: S1 ('MetaSel ('Just "dfSort") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Sort))) |
Instances
Data DataCtor Source # | |
Defined in Language.Fixpoint.Types.Sorts 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 :: forall r r'. (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 # | |
Generic DataCtor Source # | |
Show DataCtor Source # | |
NFData DataCtor Source # | |
Defined in Language.Fixpoint.Types.Sorts | |
Eq DataCtor Source # | |
Ord DataCtor Source # | |
Defined in Language.Fixpoint.Types.Sorts | |
Symbolic DataCtor Source # | |
Fixpoint DataCtor Source # | |
PPrint DataCtor Source # | |
Defined in Language.Fixpoint.Types.Sorts | |
Store DataCtor Source # | |
type Rep DataCtor Source # | |
Defined in Language.Fixpoint.Types.Sorts type Rep DataCtor = D1 ('MetaData "DataCtor" "Language.Fixpoint.Types.Sorts" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'False) (C1 ('MetaCons "DCtor" 'PrefixI 'True) (S1 ('MetaSel ('Just "dcName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 LocSymbol) :*: S1 ('MetaSel ('Just "dcFields") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [DataField]))) |
Instances
Embedding Source types as Sorts
Embedding stuff as Sorts
Instances
(Data a, Hashable a) => Data (TCEmb a) Source # | |
Defined in Language.Fixpoint.Types.Sorts gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TCEmb a -> c (TCEmb a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (TCEmb a) # toConstr :: TCEmb a -> Constr # dataTypeOf :: TCEmb a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (TCEmb a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (TCEmb a)) # gmapT :: (forall b. Data b => b -> b) -> TCEmb a -> TCEmb a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TCEmb a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TCEmb a -> r # gmapQ :: (forall d. Data d => d -> u) -> TCEmb a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> TCEmb a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> TCEmb a -> m (TCEmb a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TCEmb a -> m (TCEmb a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TCEmb a -> m (TCEmb a) # | |
(Eq a, Hashable a) => Monoid (TCEmb a) Source # | |
(Eq a, Hashable a) => Semigroup (TCEmb a) Source # | |
Generic (TCEmb a) Source # | |
Show a => Show (TCEmb a) Source # | |
(Eq a, Hashable a, Binary (HashMap a (Sort, TCArgs))) => Binary (TCEmb a) Source # | |
NFData a => NFData (TCEmb a) Source # | |
Defined in Language.Fixpoint.Types.Sorts | |
Eq a => Eq (TCEmb a) Source # | |
Hashable a => Hashable (TCEmb a) Source # | |
Defined in Language.Fixpoint.Types.Sorts | |
PPrint a => PPrint (TCEmb a) Source # | |
Defined in Language.Fixpoint.Types.Sorts | |
type Rep (TCEmb a) Source # | |
Defined in Language.Fixpoint.Types.Sorts type Rep (TCEmb a) = D1 ('MetaData "TCEmb" "Language.Fixpoint.Types.Sorts" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'True) (C1 ('MetaCons "TCE" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap a (Sort, TCArgs))))) |
Instances
Data TCArgs Source # | |
Defined in Language.Fixpoint.Types.Sorts gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TCArgs -> c TCArgs # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TCArgs # toConstr :: TCArgs -> Constr # dataTypeOf :: TCArgs -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TCArgs) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TCArgs) # gmapT :: (forall b. Data b => b -> b) -> TCArgs -> TCArgs # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TCArgs -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TCArgs -> r # gmapQ :: (forall d. Data d => d -> u) -> TCArgs -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> TCArgs -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> TCArgs -> m TCArgs # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TCArgs -> m TCArgs # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TCArgs -> m TCArgs # | |
Monoid TCArgs Source # | |
Semigroup TCArgs Source # | |
Generic TCArgs Source # | |
Show TCArgs Source # | |
Binary TCArgs Source # | |
NFData TCArgs Source # | |
Defined in Language.Fixpoint.Types.Sorts | |
Eq TCArgs Source # | |
Ord TCArgs Source # | |
Hashable TCArgs Source # | |
Defined in Language.Fixpoint.Types.Sorts | |
PPrint TCArgs Source # | |
Defined in Language.Fixpoint.Types.Sorts | |
Store TCArgs Source # | |
type Rep TCArgs Source # | |
Defined in Language.Fixpoint.Types.Sorts |