{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE CPP                        #-}
{-# LANGUAGE DeriveGeneric              #-}
{-# LANGUAGE PatternGuards              #-}
{-# LANGUAGE DeriveDataTypeable         #-}

{-# OPTIONS_GHC -Wno-orphans            #-}
{-# OPTIONS_GHC -Wno-name-shadowing     #-}

-- | This module contains the types defining an SMTLIB2 interface.

module Language.Fixpoint.Types.Theories (

    -- * Serialized Representation
      Raw

    -- * Theory Symbol
    , TheorySymbol (..)
    , Sem (..)

    -- * Theory Sorts
    , SmtSort (..)
    , FuncSort
    , sortSmtSort
    , isIntSmtSort

    , mergeTopAppls
    , pushAppls
    , popAppls
    , peekAppls

    -- * Symbol Environments
    , SymEnv (..)
    , SymM
    , symEnv
    , symEnvSort
    , symEnvTheory
    , insertSymEnv
    , deleteSymEnv
    , insertsSymEnv
    , symbolAtName
    , symbolAtSortIndex

    -- * Coercing sorts in environments
    , coerceSort
    , coerceEnv
    , coerceSortEnv
    , TheorySymbols(..)
    ) where


import           Data.Generics             (Data)
import           Data.Typeable             (Typeable)
import           Data.Hashable
import           GHC.Generics              (Generic)
import           Control.Applicative
import           Control.Monad.State
import           Control.DeepSeq
import           Language.Fixpoint.Types.Config
import           Language.Fixpoint.Types.PrettyPrint
import           Language.Fixpoint.Types.Names
import           Language.Fixpoint.Types.Sorts
import           Language.Fixpoint.Types.Environments

import           Text.PrettyPrint.HughesPJ.Compat
import qualified Data.List                as L
import           Data.Text (Text)
import qualified Data.Text                as Text
import qualified Data.Store              as S
import qualified Data.HashMap.Strict      as M
import qualified Language.Fixpoint.Misc   as Misc

--------------------------------------------------------------------------------
-- | 'Raw' is the low-level representation for SMT values
--------------------------------------------------------------------------------
type Raw = Text

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

-- | Apply tags already used to declare @apply@ symbols in the SMT solver.
--
-- The tags are organized in a stack because every time we pop the SMT solver
-- state, it forgets the tags declared since the last push.
--
-- Each entry in the stack describes the integer tag corresponding to a
-- particular function sort. Every time we issue a `push` a new level
-- is added to the stack, and correspondingly, a `pop` removes a level.
--
-- See 'seApplsCur' in 'SymEnv' for details about actually declaring the
-- tags to the SMT solver.
type Appls = [M.HashMap FuncSort Int]

lookupAppls :: FuncSort -> Appls -> Maybe Int
lookupAppls :: FuncSort -> Appls -> Maybe Int
lookupAppls FuncSort
fs = (HashMap FuncSort Int -> Maybe Int -> Maybe Int)
-> Maybe Int -> Appls -> Maybe Int
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\HashMap FuncSort Int
hm Maybe Int
acc -> Maybe Int
acc Maybe Int -> Maybe Int -> Maybe Int
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> FuncSort -> HashMap FuncSort Int -> Maybe Int
forall k v. Hashable k => k -> HashMap k v -> Maybe v
M.lookup FuncSort
fs HashMap FuncSort Int
hm) Maybe Int
forall a. Maybe a
Nothing

mergeTopAppls :: M.HashMap FuncSort Int -> Appls -> Appls
mergeTopAppls :: HashMap FuncSort Int -> Appls -> Appls
mergeTopAppls HashMap FuncSort Int
m (HashMap FuncSort Int
top : Appls
rest) = (HashMap FuncSort Int
top HashMap FuncSort Int
-> HashMap FuncSort Int -> HashMap FuncSort Int
forall a. Semigroup a => a -> a -> a
<> HashMap FuncSort Int
m) HashMap FuncSort Int -> Appls -> Appls
forall a. a -> [a] -> [a]
: Appls
rest
mergeTopAppls HashMap FuncSort Int
m [] = [HashMap FuncSort Int
m]

pushAppls :: Appls -> Appls
pushAppls :: Appls -> Appls
pushAppls Appls
aps = HashMap FuncSort Int
forall k v. HashMap k v
M.empty HashMap FuncSort Int -> Appls -> Appls
forall a. a -> [a] -> [a]
: Appls
aps

popAppls :: Appls -> Appls
popAppls :: Appls -> Appls
popAppls [] = []
popAppls (HashMap FuncSort Int
_:Appls
xs) = Appls
xs

peekAppls :: Appls -> Maybe (M.HashMap FuncSort Int)
peekAppls :: Appls -> Maybe (HashMap FuncSort Int)
peekAppls [] = Maybe (HashMap FuncSort Int)
forall a. Maybe a
Nothing
peekAppls (HashMap FuncSort Int
x:Appls
_) = HashMap FuncSort Int -> Maybe (HashMap FuncSort Int)
forall a. a -> Maybe a
Just HashMap FuncSort Int
x

data SymEnv = SymEnv
  { SymEnv -> SEnv Sort
seSort     :: !(SEnv Sort)              -- ^ Sorts of *all* defined symbols
  , SymEnv -> SEnv TheorySymbol
seTheory   :: !(SEnv TheorySymbol)      -- ^ Information about theory-specific Symbols
  , SymEnv -> SEnv DataDecl
seData     :: !(SEnv DataDecl)          -- ^ User-defined data-declarations
  , SymEnv -> SEnv Sort
seLits     :: !(SEnv Sort)              -- ^ Distinct Constant symbols

    -- | 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@).
  , SymEnv -> Appls
seAppls    :: !Appls

    -- | 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.
  , SymEnv -> HashMap FuncSort Int
seApplsCur :: !(M.HashMap FuncSort Int)
  , SymEnv -> Int
seIx       :: !Int                      -- ^ Largest unused index for sorts
  }
  deriving (SymEnv -> SymEnv -> Bool
(SymEnv -> SymEnv -> Bool)
-> (SymEnv -> SymEnv -> Bool) -> Eq SymEnv
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SymEnv -> SymEnv -> Bool
== :: SymEnv -> SymEnv -> Bool
$c/= :: SymEnv -> SymEnv -> Bool
/= :: SymEnv -> SymEnv -> Bool
Eq, Int -> SymEnv -> ShowS
[SymEnv] -> ShowS
SymEnv -> String
(Int -> SymEnv -> ShowS)
-> (SymEnv -> String) -> ([SymEnv] -> ShowS) -> Show SymEnv
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SymEnv -> ShowS
showsPrec :: Int -> SymEnv -> ShowS
$cshow :: SymEnv -> String
show :: SymEnv -> String
$cshowList :: [SymEnv] -> ShowS
showList :: [SymEnv] -> ShowS
Show, Typeable SymEnv
Typeable SymEnv =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> SymEnv -> c SymEnv)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c SymEnv)
-> (SymEnv -> Constr)
-> (SymEnv -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c SymEnv))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymEnv))
-> ((forall b. Data b => b -> b) -> SymEnv -> SymEnv)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> SymEnv -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> SymEnv -> r)
-> (forall u. (forall d. Data d => d -> u) -> SymEnv -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> SymEnv -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> SymEnv -> m SymEnv)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SymEnv -> m SymEnv)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SymEnv -> m SymEnv)
-> Data SymEnv
SymEnv -> Constr
SymEnv -> DataType
(forall b. Data b => b -> b) -> SymEnv -> SymEnv
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> SymEnv -> u
forall u. (forall d. Data d => d -> u) -> SymEnv -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SymEnv -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SymEnv -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SymEnv -> m SymEnv
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SymEnv -> m SymEnv
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SymEnv
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SymEnv -> c SymEnv
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SymEnv)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymEnv)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SymEnv -> c SymEnv
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SymEnv -> c SymEnv
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SymEnv
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SymEnv
$ctoConstr :: SymEnv -> Constr
toConstr :: SymEnv -> Constr
$cdataTypeOf :: SymEnv -> DataType
dataTypeOf :: SymEnv -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SymEnv)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SymEnv)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymEnv)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymEnv)
$cgmapT :: (forall b. Data b => b -> b) -> SymEnv -> SymEnv
gmapT :: (forall b. Data b => b -> b) -> SymEnv -> SymEnv
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SymEnv -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SymEnv -> r
$cgmapQr :: forall r r'.
(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
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> SymEnv -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> SymEnv -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SymEnv -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SymEnv -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SymEnv -> m SymEnv
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SymEnv -> m SymEnv
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SymEnv -> m SymEnv
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SymEnv -> m SymEnv
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SymEnv -> m SymEnv
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SymEnv -> m SymEnv
Data, Typeable, (forall x. SymEnv -> Rep SymEnv x)
-> (forall x. Rep SymEnv x -> SymEnv) -> Generic SymEnv
forall x. Rep SymEnv x -> SymEnv
forall x. SymEnv -> Rep SymEnv x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. SymEnv -> Rep SymEnv x
from :: forall x. SymEnv -> Rep SymEnv x
$cto :: forall x. Rep SymEnv x -> SymEnv
to :: forall x. Rep SymEnv x -> SymEnv
Generic)

{- type FuncSort = {v:Sort | isFFunc v} @-}
type FuncSort = (SmtSort, SmtSort)

-- | 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 `L.F.Smt.Serialize` (functions `smt2App`, `smt2Coerc`,
--   `smt2Lam` and `smtLamArg`, correspondingly).
type SymM a = State SymEnv a

instance NFData   SymEnv
instance S.Store SymEnv

instance Semigroup SymEnv where
  SymEnv
e1 <> :: SymEnv -> SymEnv -> SymEnv
<> SymEnv
e2 = SymEnv { seSort :: SEnv Sort
seSort     = SymEnv -> SEnv Sort
seSort     SymEnv
e1 SEnv Sort -> SEnv Sort -> SEnv Sort
forall a. Semigroup a => a -> a -> a
<> SymEnv -> SEnv Sort
seSort     SymEnv
e2
                    , seTheory :: SEnv TheorySymbol
seTheory   = SymEnv -> SEnv TheorySymbol
seTheory   SymEnv
e1 SEnv TheorySymbol -> SEnv TheorySymbol -> SEnv TheorySymbol
forall a. Semigroup a => a -> a -> a
<> SymEnv -> SEnv TheorySymbol
seTheory   SymEnv
e2
                    , seData :: SEnv DataDecl
seData     = SymEnv -> SEnv DataDecl
seData     SymEnv
e1 SEnv DataDecl -> SEnv DataDecl -> SEnv DataDecl
forall a. Semigroup a => a -> a -> a
<> SymEnv -> SEnv DataDecl
seData     SymEnv
e2
                    , seLits :: SEnv Sort
seLits     = SymEnv -> SEnv Sort
seLits     SymEnv
e1 SEnv Sort -> SEnv Sort -> SEnv Sort
forall a. Semigroup a => a -> a -> a
<> SymEnv -> SEnv Sort
seLits     SymEnv
e2
                    , seAppls :: Appls
seAppls    = (HashMap FuncSort Int
 -> HashMap FuncSort Int -> HashMap FuncSort Int)
-> Appls -> Appls -> Appls
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith HashMap FuncSort Int
-> HashMap FuncSort Int -> HashMap FuncSort Int
forall a. Semigroup a => a -> a -> a
(<>) (SymEnv -> Appls
seAppls SymEnv
e1) (SymEnv -> Appls
seAppls SymEnv
e2)
                    , seApplsCur :: HashMap FuncSort Int
seApplsCur = SymEnv -> HashMap FuncSort Int
seApplsCur SymEnv
e1 HashMap FuncSort Int
-> HashMap FuncSort Int -> HashMap FuncSort Int
forall a. Semigroup a => a -> a -> a
<> SymEnv -> HashMap FuncSort Int
seApplsCur SymEnv
e2
                    , seIx :: Int
seIx       = SymEnv -> Int
seIx       SymEnv
e1 Int -> Int -> Int
forall a. Ord a => a -> a -> a
`max` SymEnv -> Int
seIx    SymEnv
e2
                    }

instance Monoid SymEnv where
  mempty :: SymEnv
mempty        = SEnv Sort
-> SEnv TheorySymbol
-> SEnv DataDecl
-> SEnv Sort
-> Appls
-> HashMap FuncSort Int
-> Int
-> SymEnv
SymEnv SEnv Sort
forall a. SEnv a
emptySEnv SEnv TheorySymbol
forall a. SEnv a
emptySEnv SEnv DataDecl
forall a. SEnv a
emptySEnv SEnv Sort
forall a. SEnv a
emptySEnv [] HashMap FuncSort Int
forall a. Monoid a => a
mempty Int
0
  mappend :: SymEnv -> SymEnv -> SymEnv
mappend       = SymEnv -> SymEnv -> SymEnv
forall a. Semigroup a => a -> a -> a
(<>)

symEnv :: SEnv Sort -> SEnv TheorySymbol -> [DataDecl] -> SEnv Sort -> [Sort] -> SymEnv
symEnv :: SEnv Sort
-> SEnv TheorySymbol -> [DataDecl] -> SEnv Sort -> [Sort] -> SymEnv
symEnv SEnv Sort
xEnv SEnv TheorySymbol
fEnv [DataDecl]
ds SEnv Sort
ls [Sort]
_ = SEnv Sort
-> SEnv TheorySymbol
-> SEnv DataDecl
-> SEnv Sort
-> Appls
-> HashMap FuncSort Int
-> Int
-> SymEnv
SymEnv SEnv Sort
xEnv' SEnv TheorySymbol
fEnv SEnv DataDecl
dEnv SEnv Sort
ls [] HashMap FuncSort Int
forall a. Monoid a => a
mempty Int
0
  where
    xEnv' :: SEnv Sort
xEnv'   = SEnv Sort -> HashMap Symbol Sort -> SEnv Sort
forall a. SEnv a -> HashMap Symbol a -> SEnv a
unionSEnv SEnv Sort
xEnv HashMap Symbol Sort
wiredInEnv
    dEnv :: SEnv DataDecl
dEnv    = [(Symbol, DataDecl)] -> SEnv DataDecl
forall a. [(Symbol, a)] -> SEnv a
fromListSEnv [(DataDecl -> Symbol
forall a. Symbolic a => a -> Symbol
symbol DataDecl
d, DataDecl
d) | DataDecl
d <- [DataDecl]
ds]

-- | These are "BUILT-in" polymorphic functions which are
--   UNINTERPRETED but POLYMORPHIC, hence need to go through
--   the apply-defunc stuff.
wiredInEnv :: M.HashMap Symbol Sort
wiredInEnv :: HashMap Symbol Sort
wiredInEnv = [(Symbol, Sort)] -> HashMap Symbol Sort
forall k v. Hashable k => [(k, v)] -> HashMap k v
M.fromList
  [ (Symbol
toIntName, Int -> [Sort] -> Sort
mkFFunc Int
1 [Int -> Sort
FVar Int
0, Sort
FInt])
  , (Symbol
tyCastName, Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort -> Sort
FAbs Int
1 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
0) (Int -> Sort
FVar Int
1))
  ]

symEnvTheory :: Symbol -> SymEnv -> Maybe TheorySymbol
symEnvTheory :: Symbol -> SymEnv -> Maybe TheorySymbol
symEnvTheory Symbol
x SymEnv
env = Symbol -> SEnv TheorySymbol -> Maybe TheorySymbol
forall a. Symbol -> SEnv a -> Maybe a
lookupSEnv Symbol
x (SymEnv -> SEnv TheorySymbol
seTheory SymEnv
env)

symEnvSort :: Symbol -> SymEnv -> Maybe Sort
symEnvSort :: Symbol -> SymEnv -> Maybe Sort
symEnvSort   Symbol
x SymEnv
env = Symbol -> SEnv Sort -> Maybe Sort
forall a. Symbol -> SEnv a -> Maybe a
lookupSEnv Symbol
x (SymEnv -> SEnv Sort
seSort SymEnv
env)

insertSymEnv :: Symbol -> Sort -> SymEnv -> SymEnv
insertSymEnv :: Symbol -> Sort -> SymEnv -> SymEnv
insertSymEnv Symbol
x Sort
t SymEnv
env = SymEnv
env { seSort = insertSEnv x t (seSort env) }

deleteSymEnv :: Symbol -> SymEnv -> SymEnv
deleteSymEnv :: Symbol -> SymEnv -> SymEnv
deleteSymEnv Symbol
x SymEnv
env = SymEnv
env { seSort = deleteSEnv x (seSort env) }

insertsSymEnv :: SymEnv -> [(Symbol, Sort)] -> SymEnv
insertsSymEnv :: SymEnv -> [(Symbol, Sort)] -> SymEnv
insertsSymEnv = (SymEnv -> (Symbol, Sort) -> SymEnv)
-> SymEnv -> [(Symbol, Sort)] -> SymEnv
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' (\SymEnv
env (Symbol
x, Sort
s) -> Symbol -> Sort -> SymEnv -> SymEnv
insertSymEnv Symbol
x Sort
s SymEnv
env)

symbolAtSortIndex :: Symbol -> Int -> Text
symbolAtSortIndex :: Symbol -> Int -> Text
symbolAtSortIndex Symbol
mkSym Int
si = Symbol -> Text -> Text
appendSymbolText Symbol
mkSym (Text -> Text) -> (Int -> Text) -> Int -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
Text.pack (String -> Text) -> (Int -> String) -> Int -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String
forall a. Show a => a -> String
show (Int -> Text) -> Int -> Text
forall a b. (a -> b) -> a -> b
$ Int
si

symbolAtName :: Symbol -> Sort -> SymM Text
symbolAtName :: Symbol -> Sort -> SymM Text
symbolAtName Symbol
mkSym Sort
s =
  do SymEnv
env <- StateT SymEnv Identity SymEnv
forall s (m :: * -> *). MonadState s m => m s
get
     Int
fsi <- FuncSort -> SymM Int
funcSortIndex (SymEnv -> Sort -> FuncSort
ffuncSort SymEnv
env Sort
s)
     Text -> SymM Text
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Text -> SymM Text) -> Text -> SymM Text
forall a b. (a -> b) -> a -> b
$ Symbol -> Int -> Text
symbolAtSortIndex Symbol
mkSym Int
fsi
{-# SCC symbolAtName #-}

-- See 'seAppls' and 'seApplsCur' in 'SymEnv' for explanation.
funcSortIndex :: FuncSort -> SymM Int
funcSortIndex :: FuncSort -> SymM Int
funcSortIndex FuncSort
fs =
  do SymEnv
env <- StateT SymEnv Identity SymEnv
forall s (m :: * -> *). MonadState s m => m s
get
     let aps :: Appls
aps = SymEnv -> Appls
seAppls SymEnv
env
     let apsc :: HashMap FuncSort Int
apsc = SymEnv -> HashMap FuncSort Int
seApplsCur SymEnv
env
     case FuncSort -> Appls -> Maybe Int
lookupAppls FuncSort
fs Appls
aps of
      Just Int
i  -> Int -> SymM Int
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
i
      Maybe Int
Nothing ->
        case FuncSort -> HashMap FuncSort Int -> Maybe Int
forall k v. Hashable k => k -> HashMap k v -> Maybe v
M.lookup FuncSort
fs HashMap FuncSort Int
apsc of
          Just Int
i  -> Int -> SymM Int
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
i
          Maybe Int
Nothing ->
           do let i :: Int
i = SymEnv -> Int
seIx SymEnv
env
              (SymEnv -> SymEnv) -> StateT SymEnv Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\SymEnv
env -> SymEnv
env { seApplsCur = M.insert fs i apsc , seIx = 1 + i })
              Int -> SymM Int
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
i

ffuncSort :: SymEnv -> Sort -> FuncSort
ffuncSort :: SymEnv -> Sort -> FuncSort
ffuncSort SymEnv
env Sort
t      = {- tracepp ("ffuncSort " ++ showpp (t1,t2)) -} (Sort -> SmtSort
tx Sort
t1, Sort -> SmtSort
tx Sort
t2)
  where
    tx :: Sort -> SmtSort
tx               = SEnv DataDecl -> Sort -> SmtSort
applySmtSort (SymEnv -> SEnv DataDecl
seData SymEnv
env)
    (Sort
t1, Sort
t2)         = Sort -> (Sort, Sort)
args Sort
t
    args :: Sort -> (Sort, Sort)
args (FFunc Sort
a Sort
b) = (Sort
a, Sort
b)
    args Sort
_           = (Sort
FInt, Sort
FInt)

applySmtSort :: SEnv DataDecl -> Sort -> SmtSort
applySmtSort :: SEnv DataDecl -> Sort -> SmtSort
applySmtSort = Bool -> SEnv DataDecl -> Sort -> SmtSort
sortSmtSort Bool
False

isIntSmtSort :: SEnv DataDecl -> Sort -> Bool
isIntSmtSort :: SEnv DataDecl -> Sort -> Bool
isIntSmtSort SEnv DataDecl
env Sort
s = SmtSort
SInt SmtSort -> SmtSort -> Bool
forall a. Eq a => a -> a -> Bool
== SEnv DataDecl -> Sort -> SmtSort
applySmtSort SEnv DataDecl
env Sort
s

--------------------------------------------------------------------------------
-- | 'TheorySymbol' represents the information about each interpreted 'Symbol'
--------------------------------------------------------------------------------
data TheorySymbol  = Thy
  { TheorySymbol -> Symbol
tsSym    :: !Symbol          -- ^ name
  , TheorySymbol -> Text
tsRaw    :: !Raw             -- ^ serialized SMTLIB2 name
  , TheorySymbol -> Sort
tsSort   :: !Sort            -- ^ sort
  , TheorySymbol -> Sem
tsInterp :: !Sem             -- ^ TRUE = defined (interpreted), FALSE = declared (uninterpreted)
  }
  deriving (TheorySymbol -> TheorySymbol -> Bool
(TheorySymbol -> TheorySymbol -> Bool)
-> (TheorySymbol -> TheorySymbol -> Bool) -> Eq TheorySymbol
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TheorySymbol -> TheorySymbol -> Bool
== :: TheorySymbol -> TheorySymbol -> Bool
$c/= :: TheorySymbol -> TheorySymbol -> Bool
/= :: TheorySymbol -> TheorySymbol -> Bool
Eq, Eq TheorySymbol
Eq TheorySymbol =>
(TheorySymbol -> TheorySymbol -> Ordering)
-> (TheorySymbol -> TheorySymbol -> Bool)
-> (TheorySymbol -> TheorySymbol -> Bool)
-> (TheorySymbol -> TheorySymbol -> Bool)
-> (TheorySymbol -> TheorySymbol -> Bool)
-> (TheorySymbol -> TheorySymbol -> TheorySymbol)
-> (TheorySymbol -> TheorySymbol -> TheorySymbol)
-> Ord TheorySymbol
TheorySymbol -> TheorySymbol -> Bool
TheorySymbol -> TheorySymbol -> Ordering
TheorySymbol -> TheorySymbol -> TheorySymbol
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: TheorySymbol -> TheorySymbol -> Ordering
compare :: TheorySymbol -> TheorySymbol -> Ordering
$c< :: TheorySymbol -> TheorySymbol -> Bool
< :: TheorySymbol -> TheorySymbol -> Bool
$c<= :: TheorySymbol -> TheorySymbol -> Bool
<= :: TheorySymbol -> TheorySymbol -> Bool
$c> :: TheorySymbol -> TheorySymbol -> Bool
> :: TheorySymbol -> TheorySymbol -> Bool
$c>= :: TheorySymbol -> TheorySymbol -> Bool
>= :: TheorySymbol -> TheorySymbol -> Bool
$cmax :: TheorySymbol -> TheorySymbol -> TheorySymbol
max :: TheorySymbol -> TheorySymbol -> TheorySymbol
$cmin :: TheorySymbol -> TheorySymbol -> TheorySymbol
min :: TheorySymbol -> TheorySymbol -> TheorySymbol
Ord, Int -> TheorySymbol -> ShowS
[TheorySymbol] -> ShowS
TheorySymbol -> String
(Int -> TheorySymbol -> ShowS)
-> (TheorySymbol -> String)
-> ([TheorySymbol] -> ShowS)
-> Show TheorySymbol
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TheorySymbol -> ShowS
showsPrec :: Int -> TheorySymbol -> ShowS
$cshow :: TheorySymbol -> String
show :: TheorySymbol -> String
$cshowList :: [TheorySymbol] -> ShowS
showList :: [TheorySymbol] -> ShowS
Show, Typeable TheorySymbol
Typeable TheorySymbol =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> TheorySymbol -> c TheorySymbol)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c TheorySymbol)
-> (TheorySymbol -> Constr)
-> (TheorySymbol -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c TheorySymbol))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c TheorySymbol))
-> ((forall b. Data b => b -> b) -> TheorySymbol -> TheorySymbol)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> TheorySymbol -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> TheorySymbol -> r)
-> (forall u. (forall d. Data d => d -> u) -> TheorySymbol -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> TheorySymbol -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> TheorySymbol -> m TheorySymbol)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TheorySymbol -> m TheorySymbol)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TheorySymbol -> m TheorySymbol)
-> Data TheorySymbol
TheorySymbol -> Constr
TheorySymbol -> DataType
(forall b. Data b => b -> b) -> TheorySymbol -> TheorySymbol
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> TheorySymbol -> u
forall u. (forall d. Data d => d -> u) -> TheorySymbol -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TheorySymbol -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TheorySymbol -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TheorySymbol -> m TheorySymbol
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TheorySymbol -> m TheorySymbol
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TheorySymbol
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TheorySymbol -> c TheorySymbol
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TheorySymbol)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c TheorySymbol)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TheorySymbol -> c TheorySymbol
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TheorySymbol -> c TheorySymbol
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TheorySymbol
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TheorySymbol
$ctoConstr :: TheorySymbol -> Constr
toConstr :: TheorySymbol -> Constr
$cdataTypeOf :: TheorySymbol -> DataType
dataTypeOf :: TheorySymbol -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TheorySymbol)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TheorySymbol)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c TheorySymbol)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c TheorySymbol)
$cgmapT :: (forall b. Data b => b -> b) -> TheorySymbol -> TheorySymbol
gmapT :: (forall b. Data b => b -> b) -> TheorySymbol -> TheorySymbol
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TheorySymbol -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TheorySymbol -> r
$cgmapQr :: forall r r'.
(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
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> TheorySymbol -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> TheorySymbol -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TheorySymbol -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TheorySymbol -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TheorySymbol -> m TheorySymbol
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TheorySymbol -> m TheorySymbol
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TheorySymbol -> m TheorySymbol
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TheorySymbol -> m TheorySymbol
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TheorySymbol -> m TheorySymbol
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TheorySymbol -> m TheorySymbol
Data, Typeable, (forall x. TheorySymbol -> Rep TheorySymbol x)
-> (forall x. Rep TheorySymbol x -> TheorySymbol)
-> Generic TheorySymbol
forall x. Rep TheorySymbol x -> TheorySymbol
forall x. TheorySymbol -> Rep TheorySymbol x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. TheorySymbol -> Rep TheorySymbol x
from :: forall x. TheorySymbol -> Rep TheorySymbol x
$cto :: forall x. Rep TheorySymbol x -> TheorySymbol
to :: forall x. Rep TheorySymbol x -> TheorySymbol
Generic)


class TheorySymbols a where
  theorySymbols :: a ->  SEnv TheorySymbol

instance NFData Sem
instance NFData TheorySymbol
instance S.Store TheorySymbol

instance PPrint Sem where
  pprintTidy :: Tidy -> Sem -> Doc
pprintTidy Tidy
_ = String -> Doc
text (String -> Doc) -> (Sem -> String) -> Sem -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem -> String
forall a. Show a => a -> String
show

instance Fixpoint TheorySymbol where
  toFix :: TheorySymbol -> Doc
toFix (Thy Symbol
x Text
_ Sort
t Sem
d) = String -> Doc
text String
"TheorySymbol" Doc -> Doc -> Doc
<+> (Symbol, Sort) -> Doc
forall a. PPrint a => a -> Doc
pprint (Symbol
x, Sort
t) Doc -> Doc -> Doc
<+> Doc -> Doc
parens (Sem -> Doc
forall a. PPrint a => a -> Doc
pprint Sem
d)

instance PPrint TheorySymbol where
  pprintTidy :: Tidy -> TheorySymbol -> Doc
pprintTidy Tidy
k (Thy Symbol
x Text
_ Sort
t Sem
d) = String -> Doc
text String
"TheorySymbol" Doc -> Doc -> Doc
<+> Tidy -> (Symbol, Sort) -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (Symbol
x, Sort
t) Doc -> Doc -> Doc
<+> Doc -> Doc
parens (Sem -> Doc
forall a. PPrint a => a -> Doc
pprint Sem
d)

--------------------------------------------------------------------------------
-- | 'Sem' describes the SMT semantics for a given symbol
--------------------------------------------------------------------------------

data Sem
  = 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`
  deriving (Sem -> Sem -> Bool
(Sem -> Sem -> Bool) -> (Sem -> Sem -> Bool) -> Eq Sem
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Sem -> Sem -> Bool
== :: Sem -> Sem -> Bool
$c/= :: Sem -> Sem -> Bool
/= :: Sem -> Sem -> Bool
Eq, Eq Sem
Eq Sem =>
(Sem -> Sem -> Ordering)
-> (Sem -> Sem -> Bool)
-> (Sem -> Sem -> Bool)
-> (Sem -> Sem -> Bool)
-> (Sem -> Sem -> Bool)
-> (Sem -> Sem -> Sem)
-> (Sem -> Sem -> Sem)
-> Ord Sem
Sem -> Sem -> Bool
Sem -> Sem -> Ordering
Sem -> Sem -> Sem
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Sem -> Sem -> Ordering
compare :: Sem -> Sem -> Ordering
$c< :: Sem -> Sem -> Bool
< :: Sem -> Sem -> Bool
$c<= :: Sem -> Sem -> Bool
<= :: Sem -> Sem -> Bool
$c> :: Sem -> Sem -> Bool
> :: Sem -> Sem -> Bool
$c>= :: Sem -> Sem -> Bool
>= :: Sem -> Sem -> Bool
$cmax :: Sem -> Sem -> Sem
max :: Sem -> Sem -> Sem
$cmin :: Sem -> Sem -> Sem
min :: Sem -> Sem -> Sem
Ord, Int -> Sem -> ShowS
[Sem] -> ShowS
Sem -> String
(Int -> Sem -> ShowS)
-> (Sem -> String) -> ([Sem] -> ShowS) -> Show Sem
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Sem -> ShowS
showsPrec :: Int -> Sem -> ShowS
$cshow :: Sem -> String
show :: Sem -> String
$cshowList :: [Sem] -> ShowS
showList :: [Sem] -> ShowS
Show, Typeable Sem
Typeable Sem =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Sem -> c Sem)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Sem)
-> (Sem -> Constr)
-> (Sem -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Sem))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sem))
-> ((forall b. Data b => b -> b) -> Sem -> Sem)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sem -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sem -> r)
-> (forall u. (forall d. Data d => d -> u) -> Sem -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Sem -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Sem -> m Sem)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Sem -> m Sem)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Sem -> m Sem)
-> Data Sem
Sem -> Constr
Sem -> DataType
(forall b. Data b => b -> b) -> Sem -> Sem
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Sem -> u
forall u. (forall d. Data d => d -> u) -> Sem -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sem -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sem -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Sem -> m Sem
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sem -> m Sem
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sem
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sem -> c Sem
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Sem)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sem)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sem -> c Sem
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sem -> c Sem
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sem
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sem
$ctoConstr :: Sem -> Constr
toConstr :: Sem -> Constr
$cdataTypeOf :: Sem -> DataType
dataTypeOf :: Sem -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Sem)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Sem)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sem)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sem)
$cgmapT :: (forall b. Data b => b -> b) -> Sem -> Sem
gmapT :: (forall b. Data b => b -> b) -> Sem -> Sem
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sem -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sem -> r
$cgmapQr :: forall r r'.
(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
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Sem -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Sem -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Sem -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Sem -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Sem -> m Sem
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Sem -> m Sem
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sem -> m Sem
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sem -> m Sem
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sem -> m Sem
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Sem -> m Sem
Data, Typeable, (forall x. Sem -> Rep Sem x)
-> (forall x. Rep Sem x -> Sem) -> Generic Sem
forall x. Rep Sem x -> Sem
forall x. Sem -> Rep Sem x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Sem -> Rep Sem x
from :: forall x. Sem -> Rep Sem x
$cto :: forall x. Rep Sem x -> Sem
to :: forall x. Rep Sem x -> Sem
Generic)

instance S.Store Sem


--------------------------------------------------------------------------------
-- | A Refinement of 'Sort' that describes SMTLIB Sorts
--------------------------------------------------------------------------------
data SmtSort
  = SInt
  | SBool
  | SReal
  | SString
  --- CVC(5) only
  | SSet !SmtSort
  | SBag !SmtSort
  | SFFld !Integer
  ---
  | SArray !SmtSort !SmtSort
  | SBitVec !Int
  | SVar    !Int
  | SData   !FTycon ![SmtSort]
  -- HKT | SApp            ![SmtSort]           -- ^ Representing HKT
  deriving (SmtSort -> SmtSort -> Bool
(SmtSort -> SmtSort -> Bool)
-> (SmtSort -> SmtSort -> Bool) -> Eq SmtSort
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SmtSort -> SmtSort -> Bool
== :: SmtSort -> SmtSort -> Bool
$c/= :: SmtSort -> SmtSort -> Bool
/= :: SmtSort -> SmtSort -> Bool
Eq, Eq SmtSort
Eq SmtSort =>
(SmtSort -> SmtSort -> Ordering)
-> (SmtSort -> SmtSort -> Bool)
-> (SmtSort -> SmtSort -> Bool)
-> (SmtSort -> SmtSort -> Bool)
-> (SmtSort -> SmtSort -> Bool)
-> (SmtSort -> SmtSort -> SmtSort)
-> (SmtSort -> SmtSort -> SmtSort)
-> Ord SmtSort
SmtSort -> SmtSort -> Bool
SmtSort -> SmtSort -> Ordering
SmtSort -> SmtSort -> SmtSort
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: SmtSort -> SmtSort -> Ordering
compare :: SmtSort -> SmtSort -> Ordering
$c< :: SmtSort -> SmtSort -> Bool
< :: SmtSort -> SmtSort -> Bool
$c<= :: SmtSort -> SmtSort -> Bool
<= :: SmtSort -> SmtSort -> Bool
$c> :: SmtSort -> SmtSort -> Bool
> :: SmtSort -> SmtSort -> Bool
$c>= :: SmtSort -> SmtSort -> Bool
>= :: SmtSort -> SmtSort -> Bool
$cmax :: SmtSort -> SmtSort -> SmtSort
max :: SmtSort -> SmtSort -> SmtSort
$cmin :: SmtSort -> SmtSort -> SmtSort
min :: SmtSort -> SmtSort -> SmtSort
Ord, Int -> SmtSort -> ShowS
[SmtSort] -> ShowS
SmtSort -> String
(Int -> SmtSort -> ShowS)
-> (SmtSort -> String) -> ([SmtSort] -> ShowS) -> Show SmtSort
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SmtSort -> ShowS
showsPrec :: Int -> SmtSort -> ShowS
$cshow :: SmtSort -> String
show :: SmtSort -> String
$cshowList :: [SmtSort] -> ShowS
showList :: [SmtSort] -> ShowS
Show, Typeable SmtSort
Typeable SmtSort =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> SmtSort -> c SmtSort)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c SmtSort)
-> (SmtSort -> Constr)
-> (SmtSort -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c SmtSort))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SmtSort))
-> ((forall b. Data b => b -> b) -> SmtSort -> SmtSort)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> SmtSort -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> SmtSort -> r)
-> (forall u. (forall d. Data d => d -> u) -> SmtSort -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> SmtSort -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> SmtSort -> m SmtSort)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SmtSort -> m SmtSort)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SmtSort -> m SmtSort)
-> Data SmtSort
SmtSort -> Constr
SmtSort -> DataType
(forall b. Data b => b -> b) -> SmtSort -> SmtSort
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> SmtSort -> u
forall u. (forall d. Data d => d -> u) -> SmtSort -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SmtSort -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SmtSort -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SmtSort -> m SmtSort
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SmtSort -> m SmtSort
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SmtSort
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SmtSort -> c SmtSort
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SmtSort)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SmtSort)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SmtSort -> c SmtSort
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SmtSort -> c SmtSort
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SmtSort
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SmtSort
$ctoConstr :: SmtSort -> Constr
toConstr :: SmtSort -> Constr
$cdataTypeOf :: SmtSort -> DataType
dataTypeOf :: SmtSort -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SmtSort)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SmtSort)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SmtSort)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SmtSort)
$cgmapT :: (forall b. Data b => b -> b) -> SmtSort -> SmtSort
gmapT :: (forall b. Data b => b -> b) -> SmtSort -> SmtSort
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SmtSort -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SmtSort -> r
$cgmapQr :: forall r r'.
(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
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> SmtSort -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> SmtSort -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SmtSort -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SmtSort -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SmtSort -> m SmtSort
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SmtSort -> m SmtSort
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SmtSort -> m SmtSort
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SmtSort -> m SmtSort
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SmtSort -> m SmtSort
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SmtSort -> m SmtSort
Data, Typeable, (forall x. SmtSort -> Rep SmtSort x)
-> (forall x. Rep SmtSort x -> SmtSort) -> Generic SmtSort
forall x. Rep SmtSort x -> SmtSort
forall x. SmtSort -> Rep SmtSort x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. SmtSort -> Rep SmtSort x
from :: forall x. SmtSort -> Rep SmtSort x
$cto :: forall x. Rep SmtSort x -> SmtSort
to :: forall x. Rep SmtSort x -> SmtSort
Generic)

instance Hashable SmtSort
instance NFData   SmtSort
instance S.Store 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.
sortSmtSort :: Bool -> SEnv DataDecl -> Sort -> SmtSort
sortSmtSort :: Bool -> SEnv DataDecl -> Sort -> SmtSort
sortSmtSort Bool
poly SEnv DataDecl
env Sort
t = {- tracepp ("sortSmtSort: " ++ showpp t) $ -} Sort -> SmtSort
go (Sort -> SmtSort) -> (Sort -> Sort) -> Sort -> SmtSort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort -> Sort
unAbs (Sort -> SmtSort) -> Sort -> SmtSort
forall a b. (a -> b) -> a -> b
$ Sort
t
  where
    m :: Int
m = Sort -> Int
sortAbs Sort
t
    go :: Sort -> SmtSort
go (FFunc Sort
_ Sort
_)    = SmtSort
SInt
    go Sort
FInt           = SmtSort
SInt
    go Sort
FReal          = SmtSort
SReal
    go Sort
t
      | Sort
t Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
boolSort = SmtSort
SBool
      | Sort -> Bool
isString Sort
t    = SmtSort
SString
    go (FVar Int
i)
      | Bool
poly, Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
m   = Int -> SmtSort
SVar Int
i
      | Bool
otherwise     = SmtSort
SInt
    go Sort
t
      | (Sort
ct:[Sort]
ts) <- Sort -> [Sort]
unFApp Sort
t = Bool -> Int -> SEnv DataDecl -> Sort -> [Sort] -> SmtSort
fappSmtSort Bool
poly Int
m SEnv DataDecl
env Sort
ct [Sort]
ts
      | Bool
otherwise = String -> SmtSort
forall a. HasCallStack => String -> a
error String
"Unexpected empty 'unFApp t'"

fappSmtSort :: Bool -> Int -> SEnv DataDecl -> Sort -> [Sort] -> SmtSort
fappSmtSort :: Bool -> Int -> SEnv DataDecl -> Sort -> [Sort] -> SmtSort
fappSmtSort Bool
poly Int
m SEnv DataDecl
env = Sort -> [Sort] -> SmtSort
go
  where
-- HKT    go t@(FVar _) ts            = SApp (sortSmtSort poly env <$> (t:ts))

    go :: Sort -> [Sort] -> SmtSort
go (FTC FTycon
c) [Sort
a]
      | Symbol
setConName Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== FTycon -> Symbol
forall a. Symbolic a => a -> Symbol
symbol FTycon
c   = SmtSort -> SmtSort
SSet (Bool -> SEnv DataDecl -> Sort -> SmtSort
sortSmtSort Bool
poly SEnv DataDecl
env Sort
a)
    go (FTC FTycon
c) [Sort
a]
      | Symbol
bagConName Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== FTycon -> Symbol
forall a. Symbolic a => a -> Symbol
symbol FTycon
c   = SmtSort -> SmtSort
SBag (Bool -> SEnv DataDecl -> Sort -> SmtSort
sortSmtSort Bool
poly SEnv DataDecl
env Sort
a)
    go (FTC FTycon
c) [FNatNum Integer
n]
      | Symbol
ffldConName Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== FTycon -> Symbol
forall a. Symbolic a => a -> Symbol
symbol FTycon
c  = Integer -> SmtSort
SFFld Integer
n
    go (FTC FTycon
c) [Sort
a, Sort
b]
      | Symbol
arrayConName Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== FTycon -> Symbol
forall a. Symbolic a => a -> Symbol
symbol FTycon
c = SmtSort -> SmtSort -> SmtSort
SArray (Bool -> SEnv DataDecl -> Sort -> SmtSort
sortSmtSort Bool
poly SEnv DataDecl
env Sort
a) (Bool -> SEnv DataDecl -> Sort -> SmtSort
sortSmtSort Bool
poly SEnv DataDecl
env Sort
b)
    go (FTC FTycon
bv) [FTC FTycon
s]
      | Symbol
bitVecName Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== FTycon -> Symbol
forall a. Symbolic a => a -> Symbol
symbol FTycon
bv
      , Just Int
n <- FTycon -> Maybe Int
sizeBv FTycon
s      = Int -> SmtSort
SBitVec Int
n
    go Sort
s []
      | Sort -> Bool
isString Sort
s              = SmtSort
SString
    go (FTC FTycon
c) [Sort]
ts
      | Just Int
n <- FTycon -> SEnv DataDecl -> Maybe Int
forall x. Symbolic x => x -> SEnv DataDecl -> Maybe Int
tyArgs FTycon
c SEnv DataDecl
env
      , let i :: Int
i = Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- [Sort] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Sort]
ts   = FTycon -> [SmtSort] -> SmtSort
SData FTycon
c ((Bool -> SEnv DataDecl -> Sort -> SmtSort
sortSmtSort Bool
poly SEnv DataDecl
env (Sort -> SmtSort) -> (Sort -> Sort) -> Sort -> SmtSort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Sort -> Sort
FAbs Int
m (Sort -> SmtSort) -> [Sort] -> [SmtSort]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Sort]
ts) [SmtSort] -> [SmtSort] -> [SmtSort]
forall a. [a] -> [a] -> [a]
++ Int -> [SmtSort]
pad Int
i)
    go Sort
_ [Sort]
_                      = SmtSort
SInt

    pad :: Int -> [SmtSort]
pad Int
i | Bool
poly                = []
          | Bool
otherwise           = Int -> SmtSort -> [SmtSort]
forall a. Int -> a -> [a]
replicate Int
i SmtSort
SInt

tyArgs :: (Symbolic x) => x -> SEnv DataDecl -> Maybe Int
tyArgs :: forall x. Symbolic x => x -> SEnv DataDecl -> Maybe Int
tyArgs x
x SEnv DataDecl
env = DataDecl -> Int
ddVars (DataDecl -> Int) -> Maybe DataDecl -> Maybe Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Symbol -> SEnv DataDecl -> Maybe DataDecl
forall a. Symbol -> SEnv a -> Maybe a
lookupSEnv (x -> Symbol
forall a. Symbolic a => a -> Symbol
symbol x
x) SEnv DataDecl
env

instance PPrint SmtSort where
  pprintTidy :: Tidy -> SmtSort -> Doc
pprintTidy Tidy
_ SmtSort
SInt         = String -> Doc
text String
"Int"
  pprintTidy Tidy
_ SmtSort
SBool        = String -> Doc
text String
"Bool"
  pprintTidy Tidy
_ SmtSort
SReal        = String -> Doc
text String
"Real"
  pprintTidy Tidy
_ SmtSort
SString      = String -> Doc
text String
"Str"
  pprintTidy Tidy
k (SSet SmtSort
a)     = Tidy -> Doc -> [SmtSort] -> Doc
forall d. PPrint d => Tidy -> Doc -> [d] -> Doc
ppParens Tidy
k (String -> Doc
text String
"Set") [SmtSort
a]
  pprintTidy Tidy
k (SBag SmtSort
a)     = Tidy -> Doc -> [SmtSort] -> Doc
forall d. PPrint d => Tidy -> Doc -> [d] -> Doc
ppParens Tidy
k (String -> Doc
text String
"Bag") [SmtSort
a]
  pprintTidy Tidy
_ (SFFld Integer
n)    = String -> Doc
text String
"FiniteField" Doc -> Doc -> Doc
<+> Integer -> Doc
integer Integer
n
  pprintTidy Tidy
k (SArray SmtSort
a SmtSort
b) = Tidy -> Doc -> [SmtSort] -> Doc
forall d. PPrint d => Tidy -> Doc -> [d] -> Doc
ppParens Tidy
k (String -> Doc
text String
"Array") [SmtSort
a, SmtSort
b]
  pprintTidy Tidy
_ (SBitVec Int
n)  = String -> Doc
text String
"BitVec" Doc -> Doc -> Doc
<+> Int -> Doc
int Int
n
  pprintTidy Tidy
_ (SVar Int
i)     = String -> Doc
text String
"@" Doc -> Doc -> Doc
<-> Int -> Doc
int Int
i
--  HKT pprintTidy k (SApp ts)    = ppParens k (pprintTidy k tyAppName) ts
  pprintTidy Tidy
k (SData FTycon
c [SmtSort]
ts) = Tidy -> Doc -> [SmtSort] -> Doc
forall d. PPrint d => Tidy -> Doc -> [d] -> Doc
ppParens Tidy
k (Tidy -> FTycon -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k FTycon
c)         [SmtSort]
ts

ppParens :: (PPrint d) => Tidy -> Doc -> [d] -> Doc
ppParens :: forall d. PPrint d => Tidy -> Doc -> [d] -> Doc
ppParens Tidy
k Doc
d [d]
ds = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> Doc
Misc.intersperse (String -> Doc
text String
"") (Doc
d Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: (Tidy -> d -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (d -> Doc) -> [d] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [d]
ds))

--------------------------------------------------------------------------------
-- | Coercing sorts inside environments for SMT theory encoding
--------------------------------------------------------------------------------

coerceSortEnv :: ElabFlags -> SEnv Sort -> SEnv Sort
coerceSortEnv :: ElabFlags -> SEnv Sort -> SEnv Sort
coerceSortEnv ElabFlags
ef SEnv Sort
ss = ElabFlags -> Sort -> Sort
coerceSort ElabFlags
ef (Sort -> Sort) -> SEnv Sort -> SEnv Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEnv Sort
ss

coerceSort :: ElabFlags -> Sort -> Sort
coerceSort :: ElabFlags -> Sort -> Sort
coerceSort ElabFlags
ef = (if ElabFlags -> Bool
elabSetBag ElabFlags
ef then Sort -> Sort
coerceSetBagToArray else Sort -> Sort
forall a. a -> a
id) (Sort -> Sort) -> (Sort -> Sort) -> Sort -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort -> Sort
coerceMapToArray

coerceEnv :: ElabFlags -> SymEnv -> SymEnv
coerceEnv :: ElabFlags -> SymEnv -> SymEnv
coerceEnv ElabFlags
slv SymEnv
env =
  SymEnv { seSort :: SEnv Sort
seSort     = ElabFlags -> SEnv Sort -> SEnv Sort
coerceSortEnv ElabFlags
slv (SymEnv -> SEnv Sort
seSort SymEnv
env)
         , seTheory :: SEnv TheorySymbol
seTheory   = SymEnv -> SEnv TheorySymbol
seTheory SymEnv
env
         , seData :: SEnv DataDecl
seData     = SymEnv -> SEnv DataDecl
seData   SymEnv
env
         , seLits :: SEnv Sort
seLits     = SymEnv -> SEnv Sort
seLits   SymEnv
env
         , seAppls :: Appls
seAppls    = SymEnv -> Appls
seAppls  SymEnv
env
         , seApplsCur :: HashMap FuncSort Int
seApplsCur = SymEnv -> HashMap FuncSort Int
seApplsCur SymEnv
env
         , seIx :: Int
seIx       = SymEnv -> Int
seIx     SymEnv
env
         }