liquid-fixpoint-0.9.2.5: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
Safe HaskellSafe-Inferred
LanguageHaskell98

Language.Fixpoint.Types.Theories

Description

This module contains the types defining an SMTLIB2 interface.

Synopsis

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

Instances

Instances details
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 :: forall r r'. (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 #

Generic TheorySymbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Theories

Associated Types

type Rep TheorySymbol :: Type -> Type #

Show TheorySymbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Theories

NFData TheorySymbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Theories

Methods

rnf :: TheorySymbol -> () #

Eq TheorySymbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Theories

Ord TheorySymbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Theories

Fixpoint TheorySymbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Theories

PPrint TheorySymbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Theories

Store TheorySymbol Source # 
Instance details

Defined in Language.Fixpoint.Types.Theories

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.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" '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

Instances details
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 :: forall r r'. (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 #

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 #

Show Sem Source # 
Instance details

Defined in Language.Fixpoint.Types.Theories

Methods

showsPrec :: Int -> Sem -> ShowS #

show :: Sem -> String #

showList :: [Sem] -> ShowS #

NFData Sem Source # 
Instance details

Defined in Language.Fixpoint.Types.Theories

Methods

rnf :: Sem -> () #

Eq Sem Source # 
Instance details

Defined in Language.Fixpoint.Types.Theories

Methods

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

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

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 #

PPrint Sem Source # 
Instance details

Defined in Language.Fixpoint.Types.Theories

Methods

pprintTidy :: Tidy -> Sem -> Doc Source #

pprintPrec :: Int -> Tidy -> Sem -> Doc Source #

Store Sem Source # 
Instance details

Defined in Language.Fixpoint.Types.Theories

Methods

size :: Size Sem #

poke :: Sem -> Poke () #

peek :: Peek Sem #

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.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" '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

Instances

Instances details
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 :: forall r r'. (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 #

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 #

Show SmtSort Source # 
Instance details

Defined in Language.Fixpoint.Types.Theories

NFData SmtSort Source # 
Instance details

Defined in Language.Fixpoint.Types.Theories

Methods

rnf :: SmtSort -> () #

Eq SmtSort Source # 
Instance details

Defined in Language.Fixpoint.Types.Theories

Methods

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

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

Ord SmtSort Source # 
Instance details

Defined in Language.Fixpoint.Types.Theories

Hashable SmtSort Source # 
Instance details

Defined in Language.Fixpoint.Types.Theories

Methods

hashWithSalt :: Int -> SmtSort -> Int #

hash :: SmtSort -> Int #

SMTLIB2 SmtSort Source # 
Instance details

Defined in Language.Fixpoint.Smt.Theories

Methods

smt2 :: SymEnv -> SmtSort -> Builder Source #

PPrint SmtSort Source # 
Instance details

Defined in Language.Fixpoint.Types.Theories

Store SmtSort Source # 
Instance details

Defined in Language.Fixpoint.Types.Theories

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.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" '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.

Symbol Environments

data SymEnv Source #

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

Constructors

SymEnv 

Fields

Instances

Instances details
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 :: forall r r'. (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 #

Monoid SymEnv Source # 
Instance details

Defined in Language.Fixpoint.Types.Theories

Semigroup SymEnv Source # 
Instance details

Defined in Language.Fixpoint.Types.Theories

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 #

Show SymEnv Source # 
Instance details

Defined in Language.Fixpoint.Types.Theories

NFData SymEnv Source # 
Instance details

Defined in Language.Fixpoint.Types.Theories

Methods

rnf :: SymEnv -> () #

Eq SymEnv Source # 
Instance details

Defined in Language.Fixpoint.Types.Theories

Methods

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

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

Store SymEnv Source # 
Instance details

Defined in Language.Fixpoint.Types.Theories

Methods

size :: Size SymEnv #

poke :: SymEnv -> Poke () #

peek :: Peek SymEnv #

type Rep SymEnv Source # 
Instance details

Defined in Language.Fixpoint.Types.Theories

type Rep SymEnv

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