Language.Fixpoint.Types.Theories

This module contains the types defining an SMTLIB2 interface.

Serialized Representation

type Raw = Text

Raw is the low-level representation for SMT values

Theory Symbol

data TheorySymbol

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

Data TheorySymbol

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

Defined in Language.Fixpoint.Types.Theories

Associated Types

type Rep TheorySymbol :: Type -> Type

Methods

from :: TheorySymbol -> Rep TheorySymbol x

to :: Rep TheorySymbol x -> TheorySymbol

Show TheorySymbol

Defined in Language.Fixpoint.Types.Theories

Methods

showsPrec :: Int -> TheorySymbol -> ShowS

show :: TheorySymbol -> String

showList :: [TheorySymbol] -> ShowS

NFData TheorySymbol

Defined in Language.Fixpoint.Types.Theories

Methods

rnf :: TheorySymbol -> ()

Eq TheorySymbol

Defined in Language.Fixpoint.Types.Theories

Methods

(==) :: TheorySymbol -> TheorySymbol -> Bool

(/=) :: TheorySymbol -> TheorySymbol -> Bool

Ord TheorySymbol

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

Fixpoint TheorySymbol

Defined in Language.Fixpoint.Types.Theories

Methods

toFix :: TheorySymbol -> Doc

simplify :: TheorySymbol -> TheorySymbol

PPrint TheorySymbol

Defined in Language.Fixpoint.Types.Theories

Methods

pprintTidy :: Tidy -> TheorySymbol -> Doc

pprintPrec :: Int -> Tidy -> TheorySymbol -> Doc

Store TheorySymbol

Defined in Language.Fixpoint.Types.Theories

Methods

size :: Size TheorySymbol

poke :: TheorySymbol -> Poke ()

peek :: Peek TheorySymbol

type Rep TheorySymbol

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

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

Data Sem

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

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

Defined in Language.Fixpoint.Types.Theories

Methods

showsPrec :: Int -> Sem -> ShowS

show :: Sem -> String

showList :: [Sem] -> ShowS

NFData Sem

Defined in Language.Fixpoint.Types.Theories

Methods

rnf :: Sem -> ()

Eq Sem

Defined in Language.Fixpoint.Types.Theories

Methods

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

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

Ord Sem

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

Defined in Language.Fixpoint.Types.Theories

Methods

pprintTidy :: Tidy -> Sem -> Doc

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

Store Sem

Defined in Language.Fixpoint.Types.Theories

Methods

size :: Size Sem

poke :: Sem -> Poke ()

peek :: Peek Sem

type Rep Sem

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

A Refinement of Sort that describes SMTLIB Sorts

Constructors

SInt

SBool

SReal

SString

SSet

SMap

SBitVec !Int

SVar !Int

SData !FTycon ![SmtSort]

Instances

Data SmtSort

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

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

Defined in Language.Fixpoint.Types.Theories

Methods

showsPrec :: Int -> SmtSort -> ShowS

show :: SmtSort -> String

showList :: [SmtSort] -> ShowS

NFData SmtSort

Defined in Language.Fixpoint.Types.Theories

Methods

rnf :: SmtSort -> ()

Eq SmtSort

Defined in Language.Fixpoint.Types.Theories

Methods

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

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

Ord SmtSort

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

Hashable SmtSort

Defined in Language.Fixpoint.Types.Theories

Methods

hashWithSalt :: Int -> SmtSort -> Int

hash :: SmtSort -> Int

SMTLIB2 SmtSort

Defined in Language.Fixpoint.Smt.Theories

Methods

smt2 :: SymEnv -> SmtSort -> Builder

PPrint SmtSort

Defined in Language.Fixpoint.Types.Theories

Methods

pprintTidy :: Tidy -> SmtSort -> Doc

pprintPrec :: Int -> Tidy -> SmtSort -> Doc

Store SmtSort

Defined in Language.Fixpoint.Types.Theories

Methods

size :: Size SmtSort

poke :: SmtSort -> Poke ()

peek :: Peek SmtSort

type Rep SmtSort

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

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

Symbol Environments

data SymEnv

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

Data SymEnv

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

Defined in Language.Fixpoint.Types.Theories

Methods

mempty :: SymEnv

mappend :: SymEnv -> SymEnv -> SymEnv

mconcat :: [SymEnv] -> SymEnv

Semigroup SymEnv

Defined in Language.Fixpoint.Types.Theories

Methods

(<>) :: SymEnv -> SymEnv -> SymEnv

sconcat :: NonEmpty SymEnv -> SymEnv

stimes :: Integral b => b -> SymEnv -> SymEnv

Generic SymEnv

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

Defined in Language.Fixpoint.Types.Theories

Methods

showsPrec :: Int -> SymEnv -> ShowS

show :: SymEnv -> String

showList :: [SymEnv] -> ShowS

NFData SymEnv

Defined in Language.Fixpoint.Types.Theories

Methods

rnf :: SymEnv -> ()

Eq SymEnv

Defined in Language.Fixpoint.Types.Theories

Methods

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

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

Store SymEnv

Defined in Language.Fixpoint.Types.Theories

Methods

size :: Size SymEnv

poke :: SymEnv -> Poke ()

peek :: Peek SymEnv

type Rep SymEnv

Defined in Language.Fixpoint.Types.Theories

type Rep SymEnv

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 -> Text

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