{-# 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 (..)
    , sortSmtSort
    , isIntSmtSort

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

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


import           Data.Generics             (Data)
import           Data.Typeable             (Typeable)
import           Data.Hashable
import           GHC.Generics              (Generic)
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.Errors
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'
--------------------------------------------------------------------------------
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
  , SymEnv -> HashMap FuncSort Int
seAppls  :: !(M.HashMap FuncSort Int) -- ^ Types at which `apply` was used;
                                           --   see [NOTE:apply-monomorphization]
  }
  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)

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 :: HashMap FuncSort Int
seAppls  = SymEnv -> HashMap FuncSort Int
seAppls  SymEnv
e1 HashMap FuncSort Int
-> HashMap FuncSort Int -> HashMap FuncSort Int
forall a. Semigroup a => a -> a -> a
<> SymEnv -> HashMap FuncSort Int
seAppls  SymEnv
e2
                    }

instance Monoid SymEnv where
  mempty :: SymEnv
mempty        = SEnv Sort
-> SEnv TheorySymbol
-> SEnv DataDecl
-> SEnv Sort
-> HashMap FuncSort 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
  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]
ts = SEnv Sort
-> SEnv TheorySymbol
-> SEnv DataDecl
-> SEnv Sort
-> HashMap FuncSort Int
-> SymEnv
SymEnv SEnv Sort
xEnv' SEnv TheorySymbol
fEnv SEnv DataDecl
dEnv SEnv Sort
ls HashMap FuncSort Int
sortMap
  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]
    sortMap :: HashMap FuncSort Int
sortMap = [(FuncSort, Int)] -> HashMap FuncSort Int
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([FuncSort] -> [Int] -> [(FuncSort, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [FuncSort]
smts [Int
0..])
    smts :: [FuncSort]
smts    = SEnv DataDecl -> [Sort] -> [FuncSort]
funcSorts SEnv DataDecl
dEnv [Sort]
ts

-- | 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. (Eq k, 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))
  ]


-- | 'funcSorts' attempts to compute a list of all the input-output sorts
--   at which applications occur. This is a gross hack; as during unfolding
--   we may create _new_ terms with weird new sorts. Ideally, we MUST allow
--   for EXTENDING the apply-sorts with those newly created terms.
--   the solution is perhaps to *preface* each VC query of the form
--
--      push
--      assert p
--      check-sat
--      pop
--
--   with the declarations needed to make 'p' well-sorted under SMT, i.e.
--   change the above to
--
--      declare apply-sorts
--      push
--      assert p
--      check-sat
--      pop
--
--   such a strategy would NUKE the entire apply-sort machinery from the CODE base.
--   [TODO]: dynamic-apply-declaration

funcSorts :: SEnv DataDecl -> [Sort] -> [FuncSort]
funcSorts :: SEnv DataDecl -> [Sort] -> [FuncSort]
funcSorts SEnv DataDecl
dEnv [Sort]
ts = [ (SmtSort
t1, SmtSort
t2) | SmtSort
t1 <- [SmtSort]
smts, SmtSort
t2 <- [SmtSort]
smts]
  where
    smts :: [SmtSort]
smts = [SmtSort] -> [SmtSort]
forall a. Ord a => [a] -> [a]
Misc.sortNub ([SmtSort] -> [SmtSort]) -> [SmtSort] -> [SmtSort]
forall a b. (a -> b) -> a -> b
$ [[SmtSort]] -> [SmtSort]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[SmtSort]] -> [SmtSort]) -> [[SmtSort]] -> [SmtSort]
forall a b. (a -> b) -> a -> b
$ [ Sort -> [SmtSort]
tx Sort
t1 [SmtSort] -> [SmtSort] -> [SmtSort]
forall a. [a] -> [a] -> [a]
++ Sort -> [SmtSort]
tx Sort
t2 | FFunc Sort
t1 Sort
t2 <- [Sort]
ts ]
    tx :: Sort -> [SmtSort]
tx   = Bool -> SEnv DataDecl -> Sort -> [SmtSort]
inlineArrSetBag Bool
False SEnv DataDecl
dEnv

-- Related to the above, after merging #688, we now allow types other than
-- Int to which Arrays/Sets/Bags can be applied.
-- However, the `sortSmtSort` function below, previously used in `funcSorts`,
-- only instantiates type variables at Ints. This causes the solver to crash
-- when PLE generates apply queries for polymorphic sets (see
-- https://github.com/ucsd-progsys/liquidhaskell/issues/2438). The following
-- pair of functions is a temporary fix for this - it generates additional
-- array/set/bag sorts instantiated at all user types for a "polymorphic depth 1"
-- (i.e., `Array (Foo Int) Int` but not `Array (Foo (Foo Int)) Int`, to keep
-- the applys table from blowing up exponentially). Ultimately, a general
-- solution should be implemented for generating ad-hoc sets of applys on the
-- fly, as described above.

inlineArrSetBag :: Bool -> SEnv DataDecl -> Sort -> [SmtSort]
inlineArrSetBag :: Bool -> SEnv DataDecl -> Sort -> [SmtSort]
inlineArrSetBag Bool
isASB SEnv DataDecl
env Sort
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
_)
      | Bool
isASB     = SmtSort
SInt SmtSort -> [SmtSort] -> [SmtSort]
forall a. a -> [a] -> [a]
: ((Symbol, DataDecl) -> SmtSort)
-> [(Symbol, DataDecl)] -> [SmtSort]
forall a b. (a -> b) -> [a] -> [b]
map (\(Symbol, DataDecl)
q -> let dd :: DataDecl
dd = (Symbol, DataDecl) -> DataDecl
forall a b. (a, b) -> b
snd (Symbol, DataDecl)
q in
                                      FTycon -> [SmtSort] -> SmtSort
SData (DataDecl -> FTycon
ddTyCon DataDecl
dd) (Int -> SmtSort -> [SmtSort]
forall a. Int -> a -> [a]
replicate (DataDecl -> Int
ddVars DataDecl
dd) SmtSort
SInt))
                               (HashMap Symbol DataDecl -> [(Symbol, DataDecl)]
forall k v. HashMap k v -> [(k, v)]
M.toList (HashMap Symbol DataDecl -> [(Symbol, DataDecl)])
-> HashMap Symbol DataDecl -> [(Symbol, DataDecl)]
forall a b. (a -> b) -> a -> b
$ SEnv DataDecl -> HashMap Symbol DataDecl
forall a. SEnv a -> HashMap Symbol a
seBinds SEnv DataDecl
env)
      | Bool
otherwise = [SmtSort
SInt]
    go Sort
t
      | (Sort
ct:[Sort]
ts) <- Sort -> [Sort]
unFApp Sort
t = Int -> SEnv DataDecl -> Sort -> [Sort] -> [SmtSort]
inlineArrSetBagFApp Int
m SEnv DataDecl
env Sort
ct [Sort]
ts
      | Bool
otherwise = String -> [SmtSort]
forall a. HasCallStack => String -> a
error String
"Unexpected empty 'unFApp t'"

inlineArrSetBagFApp :: Int -> SEnv DataDecl -> Sort -> [Sort] -> [SmtSort]
inlineArrSetBagFApp :: Int -> SEnv DataDecl -> Sort -> [Sort] -> [SmtSort]
inlineArrSetBagFApp Int
m SEnv DataDecl
env = Sort -> [Sort] -> [SmtSort]
go
  where
    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 (SmtSort -> SmtSort) -> [SmtSort] -> [SmtSort]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> SEnv DataDecl -> Sort -> [SmtSort]
inlineArrSetBag Bool
True 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 (SmtSort -> SmtSort) -> [SmtSort] -> [SmtSort]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> SEnv DataDecl -> Sort -> [SmtSort]
inlineArrSetBag Bool
True SEnv DataDecl
env Sort
a
    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 (SmtSort -> SmtSort -> SmtSort)
-> [SmtSort] -> [SmtSort -> SmtSort]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> SEnv DataDecl -> Sort -> [SmtSort]
inlineArrSetBag Bool
True SEnv DataDecl
env Sort
a [SmtSort -> SmtSort] -> [SmtSort] -> [SmtSort]
forall a b. [a -> b] -> [a] -> [b]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Bool -> SEnv DataDecl -> Sort -> [SmtSort]
inlineArrSetBag Bool
True 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]
inlineArrSetBag Bool
False 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 (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Sort]
ts) [SmtSort] -> [SmtSort] -> [SmtSort]
forall a. [a] -> [a] -> [a]
++ Int -> SmtSort -> [SmtSort]
forall a. Int -> a -> [a]
replicate Int
i SmtSort
SInt)]
    go Sort
_ [Sort]
_                      = [SmtSort
SInt]


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)

symbolAtName :: (PPrint a) => Symbol -> SymEnv -> a -> Sort -> Text
symbolAtName :: forall a. PPrint a => Symbol -> SymEnv -> a -> Sort -> Text
symbolAtName Symbol
mkSym SymEnv
env a
e = Symbol -> SymEnv -> a -> FuncSort -> Text
forall a. PPrint a => Symbol -> SymEnv -> a -> FuncSort -> Text
symbolAtSmtName Symbol
mkSym SymEnv
env a
e (FuncSort -> Text) -> (Sort -> FuncSort) -> Sort -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymEnv -> Sort -> FuncSort
ffuncSort SymEnv
env
{-# SCC symbolAtName #-}

symbolAtSmtName :: (PPrint a) => Symbol -> SymEnv -> a -> FuncSort -> Text
symbolAtSmtName :: forall a. PPrint a => Symbol -> SymEnv -> a -> FuncSort -> Text
symbolAtSmtName Symbol
mkSym SymEnv
env a
e =
  -- formerly: intSymbol mkSym . funcSortIndex env e
  Symbol -> Text -> Text
appendSymbolText Symbol
mkSym (Text -> Text) -> (FuncSort -> Text) -> FuncSort -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
Text.pack (String -> Text) -> (FuncSort -> String) -> FuncSort -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String
forall a. Show a => a -> String
show (Int -> String) -> (FuncSort -> Int) -> FuncSort -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymEnv -> a -> FuncSort -> Int
forall a. PPrint a => SymEnv -> a -> FuncSort -> Int
funcSortIndex SymEnv
env a
e
{-# SCC symbolAtSmtName #-}

funcSortIndex :: (PPrint a) => SymEnv -> a -> FuncSort -> Int
funcSortIndex :: forall a. PPrint a => SymEnv -> a -> FuncSort -> Int
funcSortIndex SymEnv
env a
e FuncSort
fs = Int -> FuncSort -> HashMap FuncSort Int -> Int
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault Int
forall {a}. a
err FuncSort
fs (SymEnv -> HashMap FuncSort Int
seAppls SymEnv
env)
  where
    err :: a
err = String -> a
forall a. String -> a
panic (String
"Unknown func-sort: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ FuncSort -> String
forall a. Show a => a -> String
show FuncSort
fs String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. PPrint a => a -> String
showpp a
e)

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
  | SSet !SmtSort
  | SBag !SmtSort
  | 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) [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
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 = (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 (Sort -> Sort) -> SEnv Sort -> SEnv Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEnv Sort
ss

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 :: HashMap FuncSort Int
seAppls  = SymEnv -> HashMap FuncSort Int
seAppls  SymEnv
env
         }