Safe Haskell	None
Language	Haskell98

Language.Fixpoint.Types.Theories

Contents

Serialized Representation
Theory Symbol
Theory Sorts
Symbol Environments

Description

This module contains the types defining an SMTLIB2 interface.

Synopsis

type Raw = Text
data TheorySymbol = Thy {
- tsSym :: !Symbol
- tsRaw :: !Raw
- tsSort :: !Sort
- tsInterp :: !Sem
}
data Sem
- = Uninterp
- | Ctor
- | Test
- | Field
- | Theory
data SmtSort
- = SInt
- | SBool
- | SReal
- | SString
- | SSet
- | SMap
- | SBitVec !Int
- | SVar !Int
- | SData !FTycon ![SmtSort]
sortSmtSort :: Bool -> SEnv DataDecl -> Sort -> SmtSort
isIntSmtSort :: SEnv DataDecl -> Sort -> Bool
data SymEnv = SymEnv {
- seSort :: !(SEnv Sort)
- seTheory :: !(SEnv TheorySymbol)
- seData :: !(SEnv DataDecl)
- seLits :: !(SEnv Sort)
- seAppls :: !(HashMap FuncSort Int)
}
symEnv :: SEnv Sort -> SEnv TheorySymbol -> [DataDecl] -> SEnv Sort -> [Sort] -> SymEnv
symEnvSort :: Symbol -> SymEnv -> Maybe Sort
symEnvTheory :: Symbol -> SymEnv -> Maybe TheorySymbol
insertSymEnv :: Symbol -> Sort -> SymEnv -> SymEnv
insertsSymEnv :: SymEnv -> [(Symbol, Sort)] -> SymEnv
symbolAtName :: PPrint a => Symbol -> SymEnv -> a -> Sort -> Symbol
symbolAtSmtName :: PPrint a => Symbol -> SymEnv -> a -> FuncSort -> Symbol

Serialized Representation

type Raw = Text Source #

Raw is the low-level representation for SMT values

Theory Symbol

data TheorySymbol Source #

TheorySymbol represents the information about each interpreted Symbol

Constructors

Thy
Fields tsSym :: !Symbol name tsRaw :: !Raw serialized SMTLIB2 name tsSort :: !Sort sort tsInterp :: !Sem TRUE = defined (interpreted), FALSE = declared (uninterpreted)

Instances

Eq TheorySymbol Source #
Instance details Defined in Language.Fixpoint.Types.Theories Methods (==) :: TheorySymbol -> TheorySymbol -> Bool # (/=) :: TheorySymbol -> TheorySymbol -> Bool #
Data TheorySymbol Source #
Instance details Defined in Language.Fixpoint.Types.Theories Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TheorySymbol -> c TheorySymbol # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TheorySymbol # toConstr :: TheorySymbol -> Constr # dataTypeOf :: TheorySymbol -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TheorySymbol) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TheorySymbol) # gmapT :: (forall b. Data b => b -> b) -> TheorySymbol -> TheorySymbol # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TheorySymbol -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TheorySymbol -> r # gmapQ :: (forall d. Data d => d -> u) -> TheorySymbol -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> TheorySymbol -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> TheorySymbol -> m TheorySymbol # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TheorySymbol -> m TheorySymbol # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TheorySymbol -> m TheorySymbol #
Ord TheorySymbol Source #
Instance details Defined in Language.Fixpoint.Types.Theories Methods compare :: TheorySymbol -> TheorySymbol -> Ordering # (<) :: TheorySymbol -> TheorySymbol -> Bool # (<=) :: TheorySymbol -> TheorySymbol -> Bool # (>) :: TheorySymbol -> TheorySymbol -> Bool # (>=) :: TheorySymbol -> TheorySymbol -> Bool # max :: TheorySymbol -> TheorySymbol -> TheorySymbol # min :: TheorySymbol -> TheorySymbol -> TheorySymbol #
Show TheorySymbol Source #
Instance details Defined in Language.Fixpoint.Types.Theories Methods showsPrec :: Int -> TheorySymbol -> ShowS # show :: TheorySymbol -> String # showList :: [TheorySymbol] -> ShowS #
Generic TheorySymbol Source #
Instance details Defined in Language.Fixpoint.Types.Theories Associated Types type Rep TheorySymbol :: Type -> Type # Methods from :: TheorySymbol -> Rep TheorySymbol x # to :: Rep TheorySymbol x -> TheorySymbol #
Binary TheorySymbol Source #
Instance details Defined in Language.Fixpoint.Types.Theories Methods put :: TheorySymbol -> Put # get :: Get TheorySymbol # putList :: [TheorySymbol] -> Put #
NFData TheorySymbol Source #
Instance details Defined in Language.Fixpoint.Types.Theories Methods rnf :: TheorySymbol -> () #
PPrint TheorySymbol Source #
Instance details Defined in Language.Fixpoint.Types.Theories Methods pprintTidy :: Tidy -> TheorySymbol -> Doc Source # pprintPrec :: Int -> Tidy -> TheorySymbol -> Doc Source #
Fixpoint TheorySymbol Source #
Instance details Defined in Language.Fixpoint.Types.Theories Methods toFix :: TheorySymbol -> Doc Source # simplify :: TheorySymbol -> TheorySymbol Source #
type Rep TheorySymbol Source #
Instance details Defined in Language.Fixpoint.Types.Theories type Rep TheorySymbol = D1 (MetaData "TheorySymbol" "Language.Fixpoint.Types.Theories" "liquid-fixpoint-0.8.0.2-EGSzGwrlcJrCaUaEYLNzOY" False) (C1 (MetaCons "Thy" PrefixI True) ((S1 (MetaSel (Just "tsSym") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Symbol) :: S1 (MetaSel (Just "tsRaw") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Raw)) :: (S1 (MetaSel (Just "tsSort") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Sort) :*: S1 (MetaSel (Just "tsInterp") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Sem))))

data Sem Source #

Sem describes the SMT semantics for a given symbol

Constructors

Uninterp	for UDF: `len`, `height`, `append`
Ctor	for ADT constructor and tests: `cons`, `nil`
Test	for ADT tests : `is$cons`
Field	for ADT field: `hd`, `tl`
Theory	for theory ops: mem, cup, select

Instances

Eq Sem Source #
Instance details Defined in Language.Fixpoint.Types.Theories Methods (==) :: Sem -> Sem -> Bool # (/=) :: Sem -> Sem -> Bool #
Data Sem Source #
Instance details Defined in Language.Fixpoint.Types.Theories Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Sem -> c Sem # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Sem # toConstr :: Sem -> Constr # dataTypeOf :: Sem -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Sem) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sem) # gmapT :: (forall b. Data b => b -> b) -> Sem -> Sem # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sem -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sem -> r # gmapQ :: (forall d. Data d => d -> u) -> Sem -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Sem -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Sem -> m Sem # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Sem -> m Sem # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Sem -> m Sem #
Ord Sem Source #
Instance details Defined in Language.Fixpoint.Types.Theories Methods compare :: Sem -> Sem -> Ordering # (<) :: Sem -> Sem -> Bool # (<=) :: Sem -> Sem -> Bool # (>) :: Sem -> Sem -> Bool # (>=) :: Sem -> Sem -> Bool # max :: Sem -> Sem -> Sem # min :: Sem -> Sem -> Sem #
Show Sem Source #
Instance details Defined in Language.Fixpoint.Types.Theories Methods showsPrec :: Int -> Sem -> ShowS # show :: Sem -> String # showList :: [Sem] -> ShowS #
Generic Sem Source #
Instance details Defined in Language.Fixpoint.Types.Theories Associated Types type Rep Sem :: Type -> Type # Methods from :: Sem -> Rep Sem x # to :: Rep Sem x -> Sem #
Binary Sem Source #
Instance details Defined in Language.Fixpoint.Types.Theories Methods put :: Sem -> Put # get :: Get Sem # putList :: [Sem] -> Put #
NFData Sem Source #
Instance details Defined in Language.Fixpoint.Types.Theories Methods rnf :: Sem -> () #
PPrint Sem Source #
Instance details Defined in Language.Fixpoint.Types.Theories Methods pprintTidy :: Tidy -> Sem -> Doc Source # pprintPrec :: Int -> Tidy -> Sem -> Doc Source #
type Rep Sem Source #
Instance details Defined in Language.Fixpoint.Types.Theories type Rep Sem = D1 (MetaData "Sem" "Language.Fixpoint.Types.Theories" "liquid-fixpoint-0.8.0.2-EGSzGwrlcJrCaUaEYLNzOY" False) ((C1 (MetaCons "Uninterp" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Ctor" PrefixI False) (U1 :: Type -> Type)) :+: (C1 (MetaCons "Test" PrefixI False) (U1 :: Type -> Type) :+: (C1 (MetaCons "Field" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "Theory" PrefixI False) (U1 :: Type -> Type))))

Theory Sorts

data SmtSort Source #

A Refinement of Sort that describes SMTLIB Sorts

Constructors

SInt
SBool
SReal
SString
SSet
SMap
SBitVec !Int
SVar !Int
SData !FTycon ![SmtSort]

Instances

Eq SmtSort Source #
Instance details Defined in Language.Fixpoint.Types.Theories Methods (==) :: SmtSort -> SmtSort -> Bool # (/=) :: SmtSort -> SmtSort -> Bool #
Data SmtSort Source #
Instance details Defined in Language.Fixpoint.Types.Theories Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SmtSort -> c SmtSort # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SmtSort # toConstr :: SmtSort -> Constr # dataTypeOf :: SmtSort -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SmtSort) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SmtSort) # gmapT :: (forall b. Data b => b -> b) -> SmtSort -> SmtSort # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SmtSort -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SmtSort -> r # gmapQ :: (forall d. Data d => d -> u) -> SmtSort -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> SmtSort -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> SmtSort -> m SmtSort # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SmtSort -> m SmtSort # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SmtSort -> m SmtSort #
Ord SmtSort Source #
Instance details Defined in Language.Fixpoint.Types.Theories Methods compare :: SmtSort -> SmtSort -> Ordering # (<) :: SmtSort -> SmtSort -> Bool # (<=) :: SmtSort -> SmtSort -> Bool # (>) :: SmtSort -> SmtSort -> Bool # (>=) :: SmtSort -> SmtSort -> Bool # max :: SmtSort -> SmtSort -> SmtSort # min :: SmtSort -> SmtSort -> SmtSort #
Show SmtSort Source #
Instance details Defined in Language.Fixpoint.Types.Theories Methods showsPrec :: Int -> SmtSort -> ShowS # show :: SmtSort -> String # showList :: [SmtSort] -> ShowS #
Generic SmtSort Source #
Instance details Defined in Language.Fixpoint.Types.Theories Associated Types type Rep SmtSort :: Type -> Type # Methods from :: SmtSort -> Rep SmtSort x # to :: Rep SmtSort x -> SmtSort #
Binary SmtSort Source #
Instance details Defined in Language.Fixpoint.Types.Theories Methods put :: SmtSort -> Put # get :: Get SmtSort # putList :: [SmtSort] -> Put #
NFData SmtSort Source #
Instance details Defined in Language.Fixpoint.Types.Theories Methods rnf :: SmtSort -> () #
Hashable SmtSort Source #
Instance details Defined in Language.Fixpoint.Types.Theories Methods hashWithSalt :: Int -> SmtSort -> Int # hash :: SmtSort -> Int #
PPrint SmtSort Source #
Instance details Defined in Language.Fixpoint.Types.Theories Methods pprintTidy :: Tidy -> SmtSort -> Doc Source # pprintPrec :: Int -> Tidy -> SmtSort -> Doc Source #
SMTLIB2 SmtSort Source #
Instance details Defined in Language.Fixpoint.Smt.Theories Methods smt2 :: SymEnv -> SmtSort -> Builder Source #
type Rep SmtSort Source #
Instance details Defined in Language.Fixpoint.Types.Theories type Rep SmtSort = D1 (MetaData "SmtSort" "Language.Fixpoint.Types.Theories" "liquid-fixpoint-0.8.0.2-EGSzGwrlcJrCaUaEYLNzOY" False) (((C1 (MetaCons "SInt" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "SBool" PrefixI False) (U1 :: Type -> Type)) :+: (C1 (MetaCons "SReal" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "SString" PrefixI False) (U1 :: Type -> Type))) :+: ((C1 (MetaCons "SSet" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "SMap" PrefixI False) (U1 :: Type -> Type)) :+: (C1 (MetaCons "SBitVec" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Int)) :+: (C1 (MetaCons "SVar" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Int)) :+: C1 (MetaCons "SData" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 FTycon) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [SmtSort]))))))

sortSmtSort :: Bool -> SEnv DataDecl -> Sort -> SmtSort Source #

The poly parameter is True when we are *declaring* sorts, and so we need to leave the top type variables be; it is False when we are declaring variables etc., and there, we serialize them using Int (though really, there SHOULD BE NO floating tyVars... 'smtSort True msg t' serializes a sort t using type variables, 'smtSort False msg t' serializes a sort t using Int instead of tyvars.

isIntSmtSort :: SEnv DataDecl -> Sort -> Bool Source #

Symbol Environments

data SymEnv Source #

SymEnv is used to resolve the Sort and Sem of each Symbol

Constructors

SymEnv
Fields seSort :: !(SEnv Sort) Sorts of all defined symbols seTheory :: !(SEnv TheorySymbol) Information about theory-specific Symbols seData :: !(SEnv DataDecl) User-defined data-declarations seLits :: !(SEnv Sort) Distinct Constant symbols seAppls :: !(HashMap FuncSort Int) Types at which `apply` was used; see [NOTE:apply-monomorphization]

Instances

Eq SymEnv Source #
Instance details Defined in Language.Fixpoint.Types.Theories Methods (==) :: SymEnv -> SymEnv -> Bool # (/=) :: SymEnv -> SymEnv -> Bool #
Data SymEnv Source #
Instance details Defined in Language.Fixpoint.Types.Theories Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SymEnv -> c SymEnv # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SymEnv # toConstr :: SymEnv -> Constr # dataTypeOf :: SymEnv -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SymEnv) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymEnv) # gmapT :: (forall b. Data b => b -> b) -> SymEnv -> SymEnv # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SymEnv -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SymEnv -> r # gmapQ :: (forall d. Data d => d -> u) -> SymEnv -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> SymEnv -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> SymEnv -> m SymEnv # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SymEnv -> m SymEnv # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SymEnv -> m SymEnv #
Show SymEnv Source #
Instance details Defined in Language.Fixpoint.Types.Theories Methods showsPrec :: Int -> SymEnv -> ShowS # show :: SymEnv -> String # showList :: [SymEnv] -> ShowS #
Generic SymEnv Source #
Instance details Defined in Language.Fixpoint.Types.Theories Associated Types type Rep SymEnv :: Type -> Type # Methods from :: SymEnv -> Rep SymEnv x # to :: Rep SymEnv x -> SymEnv #
Semigroup SymEnv Source #
Instance details Defined in Language.Fixpoint.Types.Theories Methods (<>) :: SymEnv -> SymEnv -> SymEnv # sconcat :: NonEmpty SymEnv -> SymEnv # stimes :: Integral b => b -> SymEnv -> SymEnv #
Monoid SymEnv Source #
Instance details Defined in Language.Fixpoint.Types.Theories Methods mempty :: SymEnv # mappend :: SymEnv -> SymEnv -> SymEnv # mconcat :: [SymEnv] -> SymEnv #
Binary SymEnv Source #
Instance details Defined in Language.Fixpoint.Types.Theories Methods put :: SymEnv -> Put # get :: Get SymEnv # putList :: [SymEnv] -> Put #
NFData SymEnv Source #
Instance details Defined in Language.Fixpoint.Types.Theories Methods rnf :: SymEnv -> () #
type Rep SymEnv Source #
Instance details Defined in Language.Fixpoint.Types.Theories type Rep SymEnv

symEnv :: SEnv Sort -> SEnv TheorySymbol -> [DataDecl] -> SEnv Sort -> [Sort] -> SymEnv Source #

symEnvSort :: Symbol -> SymEnv -> Maybe Sort Source #

symEnvTheory :: Symbol -> SymEnv -> Maybe TheorySymbol Source #

insertSymEnv :: Symbol -> Sort -> SymEnv -> SymEnv Source #

insertsSymEnv :: SymEnv -> [(Symbol, Sort)] -> SymEnv Source #

symbolAtName :: PPrint a => Symbol -> SymEnv -> a -> Sort -> Symbol Source #

symbolAtSmtName :: PPrint a => Symbol -> SymEnv -> a -> FuncSort -> Symbol Source #