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

-- | 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
    , insertsSymEnv
    , symbolAtName
    , symbolAtSmtName


    ) where


import           Data.Generics             (Data)
#if !MIN_VERSION_base(4,14,0)
import           Data.Semigroup            (Semigroup (..))
#endif

import           Data.Typeable             (Typeable)
import           Data.Hashable
import           GHC.Generics              (Generic)
import           Control.DeepSeq
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 qualified Data.Text.Lazy           as LT
import qualified Data.Binary              as B
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          = LT.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
/= :: SymEnv -> SymEnv -> Bool
$c/= :: SymEnv -> SymEnv -> Bool
== :: SymEnv -> SymEnv -> Bool
$c== :: 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
showList :: [SymEnv] -> ShowS
$cshowList :: [SymEnv] -> ShowS
show :: SymEnv -> String
$cshow :: SymEnv -> String
showsPrec :: Int -> SymEnv -> ShowS
$cshowsPrec :: Int -> SymEnv -> ShowS
Show, Typeable SymEnv
DataType
Constr
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 -> DataType
SymEnv -> Constr
(forall b. Data b => b -> b) -> SymEnv -> SymEnv
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SymEnv -> c SymEnv
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$cSymEnv :: Constr
$tSymEnv :: DataType
gmapMo :: (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
gmapMp :: (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
gmapM :: (forall d. Data d => d -> m d) -> SymEnv -> m SymEnv
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SymEnv -> m SymEnv
gmapQi :: Int -> (forall d. Data d => d -> u) -> SymEnv -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SymEnv -> u
gmapQ :: (forall d. Data d => d -> u) -> SymEnv -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> SymEnv -> [u]
gmapQr :: (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
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SymEnv -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SymEnv -> r
gmapT :: (forall b. Data b => b -> b) -> SymEnv -> SymEnv
$cgmapT :: (forall b. Data b => b -> b) -> SymEnv -> SymEnv
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymEnv)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymEnv)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c SymEnv)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SymEnv)
dataTypeOf :: SymEnv -> DataType
$cdataTypeOf :: SymEnv -> DataType
toConstr :: SymEnv -> Constr
$ctoConstr :: SymEnv -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SymEnv
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SymEnv
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SymEnv -> c SymEnv
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SymEnv -> c SymEnv
$cp1Data :: Typeable 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
$cto :: forall x. Rep SymEnv x -> SymEnv
$cfrom :: forall x. SymEnv -> Rep SymEnv x
Generic)

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

instance NFData   SymEnv
instance B.Binary SymEnv

instance Semigroup SymEnv where
  SymEnv
e1 <> :: SymEnv -> SymEnv -> SymEnv
<> SymEnv
e2 = SymEnv :: SEnv Sort
-> SEnv TheorySymbol
-> SEnv DataDecl
-> SEnv Sort
-> HashMap FuncSort Int
-> SymEnv
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
--   UNININTERPRETED 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])]


-- | 'smtSorts' 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 wierd 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 [ [Sort -> SmtSort
tx Sort
t1, Sort -> SmtSort
tx Sort
t2] | FFunc Sort
t1 Sort
t2 <- [Sort]
ts]
    tx :: Sort -> SmtSort
tx           = SEnv DataDecl -> Sort -> SmtSort
applySmtSort SEnv DataDecl
dEnv


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 :: SEnv Sort
seSort = Symbol -> Sort -> SEnv Sort -> SEnv Sort
forall a. Symbol -> a -> SEnv a -> SEnv a
insertSEnv Symbol
x Sort
t (SymEnv -> SEnv Sort
seSort SymEnv
env) }

insertsSymEnv :: SymEnv -> [(Symbol, Sort)] -> SymEnv
insertsSymEnv :: SymEnv -> [(Symbol, Sort)] -> SymEnv
insertsSymEnv = (SymEnv -> (Symbol, Sort) -> SymEnv)
-> SymEnv -> [(Symbol, Sort)] -> SymEnv
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 -> Symbol
symbolAtName :: Symbol -> SymEnv -> a -> Sort -> Symbol
symbolAtName Symbol
mkSym SymEnv
env a
e = Symbol -> SymEnv -> a -> FuncSort -> Symbol
forall a. PPrint a => Symbol -> SymEnv -> a -> FuncSort -> Symbol
symbolAtSmtName Symbol
mkSym SymEnv
env a
e (FuncSort -> Symbol) -> (Sort -> FuncSort) -> Sort -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymEnv -> Sort -> FuncSort
ffuncSort SymEnv
env

symbolAtSmtName :: (PPrint a) => Symbol -> SymEnv -> a -> FuncSort -> Symbol
symbolAtSmtName :: Symbol -> SymEnv -> a -> FuncSort -> Symbol
symbolAtSmtName Symbol
mkSym SymEnv
env a
e = Symbol -> Int -> Symbol
forall a. Show a => Symbol -> a -> Symbol
intSymbol Symbol
mkSym (Int -> Symbol) -> (FuncSort -> Int) -> FuncSort -> Symbol
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

funcSortIndex :: (PPrint a) => SymEnv -> a -> FuncSort -> Int
funcSortIndex :: SymEnv -> a -> FuncSort -> Int
funcSortIndex SymEnv
env a
e FuncSort
z = 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
z (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. PPrint a => a -> String
showpp FuncSort
z 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 -> Raw
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
/= :: TheorySymbol -> TheorySymbol -> Bool
$c/= :: TheorySymbol -> TheorySymbol -> Bool
== :: TheorySymbol -> TheorySymbol -> Bool
$c== :: 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
min :: TheorySymbol -> TheorySymbol -> TheorySymbol
$cmin :: TheorySymbol -> TheorySymbol -> TheorySymbol
max :: TheorySymbol -> TheorySymbol -> TheorySymbol
$cmax :: TheorySymbol -> TheorySymbol -> TheorySymbol
>= :: TheorySymbol -> TheorySymbol -> Bool
$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
compare :: TheorySymbol -> TheorySymbol -> Ordering
$ccompare :: TheorySymbol -> TheorySymbol -> Ordering
$cp1Ord :: Eq 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
showList :: [TheorySymbol] -> ShowS
$cshowList :: [TheorySymbol] -> ShowS
show :: TheorySymbol -> String
$cshow :: TheorySymbol -> String
showsPrec :: Int -> TheorySymbol -> ShowS
$cshowsPrec :: Int -> TheorySymbol -> ShowS
Show, Typeable TheorySymbol
DataType
Constr
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 -> DataType
TheorySymbol -> Constr
(forall b. Data b => b -> b) -> TheorySymbol -> TheorySymbol
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TheorySymbol -> c TheorySymbol
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$cThy :: Constr
$tTheorySymbol :: DataType
gmapMo :: (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
gmapMp :: (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
gmapM :: (forall d. Data d => d -> m d) -> TheorySymbol -> m TheorySymbol
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TheorySymbol -> m TheorySymbol
gmapQi :: Int -> (forall d. Data d => d -> u) -> TheorySymbol -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TheorySymbol -> u
gmapQ :: (forall d. Data d => d -> u) -> TheorySymbol -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> TheorySymbol -> [u]
gmapQr :: (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
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TheorySymbol -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TheorySymbol -> r
gmapT :: (forall b. Data b => b -> b) -> TheorySymbol -> TheorySymbol
$cgmapT :: (forall b. Data b => b -> b) -> TheorySymbol -> TheorySymbol
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c TheorySymbol)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c TheorySymbol)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c TheorySymbol)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TheorySymbol)
dataTypeOf :: TheorySymbol -> DataType
$cdataTypeOf :: TheorySymbol -> DataType
toConstr :: TheorySymbol -> Constr
$ctoConstr :: TheorySymbol -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TheorySymbol
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TheorySymbol
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TheorySymbol -> c TheorySymbol
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TheorySymbol -> c TheorySymbol
$cp1Data :: Typeable 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
$cto :: forall x. Rep TheorySymbol x -> TheorySymbol
$cfrom :: forall x. TheorySymbol -> Rep TheorySymbol x
Generic)

instance NFData Sem
instance NFData TheorySymbol
instance B.Binary 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 Raw
_ 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 Raw
_ 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
  deriving (Sem -> Sem -> Bool
(Sem -> Sem -> Bool) -> (Sem -> Sem -> Bool) -> Eq Sem
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Sem -> Sem -> Bool
$c/= :: Sem -> Sem -> Bool
== :: Sem -> Sem -> Bool
$c== :: 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
min :: Sem -> Sem -> Sem
$cmin :: Sem -> Sem -> Sem
max :: Sem -> Sem -> Sem
$cmax :: Sem -> Sem -> Sem
>= :: Sem -> Sem -> Bool
$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
compare :: Sem -> Sem -> Ordering
$ccompare :: Sem -> Sem -> Ordering
$cp1Ord :: Eq 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
showList :: [Sem] -> ShowS
$cshowList :: [Sem] -> ShowS
show :: Sem -> String
$cshow :: Sem -> String
showsPrec :: Int -> Sem -> ShowS
$cshowsPrec :: Int -> Sem -> ShowS
Show, Typeable Sem
DataType
Constr
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 -> DataType
Sem -> Constr
(forall b. Data b => b -> b) -> Sem -> Sem
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sem -> c Sem
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$cTheory :: Constr
$cField :: Constr
$cTest :: Constr
$cCtor :: Constr
$cUninterp :: Constr
$tSem :: DataType
gmapMo :: (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
gmapMp :: (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
gmapM :: (forall d. Data d => d -> m d) -> Sem -> m Sem
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Sem -> m Sem
gmapQi :: Int -> (forall d. Data d => d -> u) -> Sem -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Sem -> u
gmapQ :: (forall d. Data d => d -> u) -> Sem -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Sem -> [u]
gmapQr :: (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
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sem -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sem -> r
gmapT :: (forall b. Data b => b -> b) -> Sem -> Sem
$cgmapT :: (forall b. Data b => b -> b) -> Sem -> Sem
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sem)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sem)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Sem)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Sem)
dataTypeOf :: Sem -> DataType
$cdataTypeOf :: Sem -> DataType
toConstr :: Sem -> Constr
$ctoConstr :: Sem -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sem
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Sem
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sem -> c Sem
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Sem -> c Sem
$cp1Data :: Typeable 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
$cto :: forall x. Rep Sem x -> Sem
$cfrom :: forall x. Sem -> Rep Sem x
Generic)

instance B.Binary Sem


--------------------------------------------------------------------------------
-- | A Refinement of 'Sort' that describes SMTLIB Sorts
--------------------------------------------------------------------------------
data SmtSort
  = SInt
  | SBool
  | SReal
  | SString
  | SSet
  | SMap
  | 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
/= :: SmtSort -> SmtSort -> Bool
$c/= :: SmtSort -> SmtSort -> Bool
== :: SmtSort -> SmtSort -> Bool
$c== :: 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
min :: SmtSort -> SmtSort -> SmtSort
$cmin :: SmtSort -> SmtSort -> SmtSort
max :: SmtSort -> SmtSort -> SmtSort
$cmax :: SmtSort -> SmtSort -> SmtSort
>= :: SmtSort -> SmtSort -> Bool
$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
compare :: SmtSort -> SmtSort -> Ordering
$ccompare :: SmtSort -> SmtSort -> Ordering
$cp1Ord :: Eq 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
showList :: [SmtSort] -> ShowS
$cshowList :: [SmtSort] -> ShowS
show :: SmtSort -> String
$cshow :: SmtSort -> String
showsPrec :: Int -> SmtSort -> ShowS
$cshowsPrec :: Int -> SmtSort -> ShowS
Show, Typeable SmtSort
DataType
Constr
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 -> DataType
SmtSort -> Constr
(forall b. Data b => b -> b) -> SmtSort -> SmtSort
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SmtSort -> c SmtSort
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$cSData :: Constr
$cSVar :: Constr
$cSBitVec :: Constr
$cSMap :: Constr
$cSSet :: Constr
$cSString :: Constr
$cSReal :: Constr
$cSBool :: Constr
$cSInt :: Constr
$tSmtSort :: DataType
gmapMo :: (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
gmapMp :: (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
gmapM :: (forall d. Data d => d -> m d) -> SmtSort -> m SmtSort
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SmtSort -> m SmtSort
gmapQi :: Int -> (forall d. Data d => d -> u) -> SmtSort -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SmtSort -> u
gmapQ :: (forall d. Data d => d -> u) -> SmtSort -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> SmtSort -> [u]
gmapQr :: (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
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SmtSort -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SmtSort -> r
gmapT :: (forall b. Data b => b -> b) -> SmtSort -> SmtSort
$cgmapT :: (forall b. Data b => b -> b) -> SmtSort -> SmtSort
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SmtSort)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SmtSort)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c SmtSort)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SmtSort)
dataTypeOf :: SmtSort -> DataType
$cdataTypeOf :: SmtSort -> DataType
toConstr :: SmtSort -> Constr
$ctoConstr :: SmtSort -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SmtSort
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SmtSort
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SmtSort -> c SmtSort
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SmtSort -> c SmtSort
$cp1Data :: Typeable 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
$cto :: forall x. Rep SmtSort x -> SmtSort
$cfrom :: forall x. SmtSort -> Rep SmtSort x
Generic)

instance Hashable SmtSort
instance NFData   SmtSort
instance B.Binary 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) else id) $ -}  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              = Bool -> Int -> SEnv DataDecl -> Sort -> [Sort] -> SmtSort
fappSmtSort Bool
poly Int
m SEnv DataDecl
env Sort
ct [Sort]
ts where (Sort
ct:[Sort]
ts) = Sort -> [Sort]
unFApp Sort
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]
_
      | Symbol
setConName Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== FTycon -> Symbol
forall a. Symbolic a => a -> Symbol
symbol FTycon
c  = SmtSort
SSet
    go (FTC FTycon
c) [Sort]
_
      | Symbol
mapConName Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== FTycon -> Symbol
forall a. Symbolic a => a -> Symbol
symbol FTycon
c  = SmtSort
SMap
    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 (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 :: 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
_ SmtSort
SSet         = String -> Doc
text String
"Set"
  pprintTidy Tidy
_ SmtSort
SMap         = String -> Doc
text String
"Map"
  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 :: 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))