Safe Haskell	None
Language	Haskell98

Language.Fixpoint.Types.Theories

Contents

Serialized Representation
Theory Symbol
Theory Sorts
Symbol Environments
Coercing sorts in 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
- | Defined
data SmtSort
- = SInt
- | SBool
- | SReal
- | SString
- | SSet !SmtSort
- | SBag !SmtSort
- | SFFld !Integer
- | SArray !SmtSort !SmtSort
- | SBitVec !Int
- | SVar !Int
- | SData !FTycon ![SmtSort]
type FuncSort = (SmtSort, SmtSort)
sortSmtSort :: Bool -> SEnv DataDecl -> Sort -> SmtSort
isIntSmtSort :: SEnv DataDecl -> Sort -> Bool
mergeTopAppls :: HashMap FuncSort Int -> Appls -> Appls
pushAppls :: Appls -> Appls
popAppls :: Appls -> Appls
peekAppls :: Appls -> Maybe (HashMap FuncSort Int)
data SymEnv = SymEnv {
- seSort :: !(SEnv Sort)
- seTheory :: !(SEnv TheorySymbol)
- seData :: !(SEnv DataDecl)
- seLits :: !(SEnv Sort)
- seAppls :: !Appls
- seApplsCur :: !(HashMap FuncSort Int)
- seIx :: !Int
}
type SymM a = State SymEnv a
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
deleteSymEnv :: Symbol -> SymEnv -> SymEnv
insertsSymEnv :: SymEnv -> [(Symbol, Sort)] -> SymEnv
symbolAtName :: Symbol -> Sort -> SymM Text
symbolAtSortIndex :: Symbol -> Int -> Text
coerceSort :: ElabFlags -> Sort -> Sort
coerceEnv :: ElabFlags -> SymEnv -> SymEnv
coerceSortEnv :: ElabFlags -> SEnv Sort -> SEnv Sort
class TheorySymbols a where
- theorySymbols :: a -> SEnv TheorySymbol

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

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

Instance details

Defined in Language.Fixpoint.Types.Theories

type Rep TheorySymbol = D1 ('MetaData "TheorySymbol" "Language.Fixpoint.Types.Theories" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" '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))))

Methods

from :: TheorySymbol -> Rep TheorySymbol x #

to :: Rep TheorySymbol x -> TheorySymbol #

Show TheorySymbol Source #

Instance details

Defined in Language.Fixpoint.Types.Theories

Methods

showsPrec :: Int -> TheorySymbol -> ShowS #

show :: TheorySymbol -> String #

showList :: [TheorySymbol] -> ShowS #

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

Methods

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

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

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 #

Fixpoint TheorySymbol Source #

Instance details

Defined in Language.Fixpoint.Types.Theories

Methods

toFix :: TheorySymbol -> Doc Source #

simplify :: TheorySymbol -> TheorySymbol Source #

PPrint TheorySymbol Source #

Instance details

Defined in Language.Fixpoint.Types.Theories

Methods

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

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

Store TheorySymbol Source #

Instance details

Defined in Language.Fixpoint.Types.Theories

Methods

size :: Size TheorySymbol #

poke :: TheorySymbol -> Poke () #

peek :: Peek TheorySymbol #

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.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" '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
Defined	for user-defined `define-fun`

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

Instance details

Defined in Language.Fixpoint.Types.Theories

type Rep Sem = D1 ('MetaData "Sem" "Language.Fixpoint.Types.Theories" "liquid-fixpoint-0.9.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" '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) :+: C1 ('MetaCons "Defined" 'PrefixI 'False) (U1 :: 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.6.3.4-CmH5CYTDh7gFBJNG3w2uNw" '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) :+: C1 ('MetaCons "Defined" 'PrefixI 'False) (U1 :: Type -> Type))))

Theory Sorts

data SmtSort Source #

A Refinement of Sort that describes SMTLIB Sorts

Constructors

SInt
SBool
SReal
SString
SSet !SmtSort
SBag !SmtSort
SFFld !Integer
SArray !SmtSort !SmtSort
SBitVec !Int
SVar !Int
SData !FTycon ![SmtSort]

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

Instance details

Defined in Language.Fixpoint.Types.Theories

Methods

from :: SmtSort -> Rep SmtSort x #

to :: Rep SmtSort x -> SmtSort #

Show SmtSort Source #

Instance details

Defined in Language.Fixpoint.Types.Theories

Methods

showsPrec :: Int -> SmtSort -> ShowS #

show :: SmtSort -> String #

showList :: [SmtSort] -> ShowS #

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

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 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 :: SmtSort -> SymM Builder Source #

PPrint SmtSort Source #

Instance details

Defined in Language.Fixpoint.Types.Theories

Methods

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

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

Store SmtSort Source #

Instance details

Defined in Language.Fixpoint.Types.Theories

Methods

size :: Size SmtSort #

poke :: SmtSort -> Poke () #

peek :: Peek SmtSort #

type Rep SmtSort Source #

Instance details

Defined in Language.Fixpoint.Types.Theories

type FuncSort = (SmtSort, SmtSort) Source #

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 #

mergeTopAppls :: HashMap FuncSort Int -> Appls -> Appls Source #

pushAppls :: Appls -> Appls Source #

popAppls :: Appls -> Appls Source #

peekAppls :: Appls -> Maybe (HashMap FuncSort Int) Source #

Symbol Environments

data SymEnv Source #

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 :: !Appls
Apply tags already declared in the SMT solver.
This is inspected when serializing applications of functions to determine if a new tag needs to be created for a given function sort (funcSortIndex).
seApplsCur :: !(HashMap FuncSort Int)
Apply tags that have been created while serializing expressions for the SMT solver, but which have not been used to declare apply symbols yet in the SMT solver.
The apply symbols using the tags are declared whenever we need to send the serialized expressions to the SMT solver (using funcSortVars). At this point, the contents of this map are merged into the top of the seAppls stack, and seApplsCur is cleared.
seIx :: !Int
Largest unused index for sorts

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

Methods

mempty :: SymEnv #

mappend :: SymEnv -> SymEnv -> SymEnv #

mconcat :: [SymEnv] -> 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 #

Generic SymEnv Source #

Instance details

Defined in Language.Fixpoint.Types.Theories

Associated Types

type Rep SymEnv
Instance details Defined in Language.Fixpoint.Types.Theories type Rep SymEnv

Methods

from :: SymEnv -> Rep SymEnv x #

to :: Rep SymEnv x -> SymEnv #

Show SymEnv Source #

Instance details

Defined in Language.Fixpoint.Types.Theories

Methods

showsPrec :: Int -> SymEnv -> ShowS #

show :: SymEnv -> String #

showList :: [SymEnv] -> ShowS #

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

type SymM a = State SymEnv a Source #

Generating SMT expressions is a stateful process because new symbols (apply, coerce, smt_lambda and lam_arg) need to be emitted with unique ids for each newly encountered function sort. The SymM monad carries the SymEnv state required to track the ids. The state updates are performed in Serialize (functions smt2App, smt2Coerc, smt2Lam and smtLamArg, correspondingly).

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 #

deleteSymEnv :: Symbol -> SymEnv -> SymEnv Source #

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

symbolAtName :: Symbol -> Sort -> SymM Text Source #

symbolAtSortIndex :: Symbol -> Int -> Text Source #

Coercing sorts in environments

coerceSort :: ElabFlags -> Sort -> Sort Source #

coerceEnv :: ElabFlags -> SymEnv -> SymEnv Source #

coerceSortEnv :: ElabFlags -> SEnv Sort -> SEnv Sort Source #

Coercing sorts inside environments for SMT theory encoding

class TheorySymbols a where Source #

Methods

theorySymbols :: a -> SEnv TheorySymbol Source #

Instances

Instances details

TheorySymbols SMTSolver Source #	Theory Symbols : `uninterpSEnv` should be disjoint from see `interpSEnv` to avoid duplicate SMT definitions. `uninterpSEnv` is for uninterpreted symbols, and `interpSEnv` is for interpreted symbols.
Instance details Defined in Language.Fixpoint.Smt.Theories Methods theorySymbols :: SMTSolver -> SEnv TheorySymbol Source #
TheorySymbols DefinedFuns Source #
Instance details Defined in Language.Fixpoint.Smt.Theories Methods theorySymbols :: DefinedFuns -> SEnv TheorySymbol Source #
TheorySymbols [Equation] Source #
Instance details Defined in Language.Fixpoint.Smt.Theories Methods theorySymbols :: [Equation] -> SEnv TheorySymbol Source #
TheorySymbols [DataDecl] Source #
Instance details Defined in Language.Fixpoint.Smt.Theories Methods theorySymbols :: [DataDecl] -> SEnv TheorySymbol Source #