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


    ) where


import           Data.Generics             (Data)
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           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
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
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
SymEnv -> DataType
SymEnv -> Constr
(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)
gmapMo :: 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
gmapMp :: forall (m :: * -> *).
MonadPlus 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
gmapM :: forall (m :: * -> *).
Monad m =>
(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 :: forall u. Int -> (forall d. Data d => d -> u) -> SymEnv -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SymEnv -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> SymEnv -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> SymEnv -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
Data, Typeable, 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 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 forall a. Semigroup a => a -> a -> a
<> SymEnv -> SEnv Sort
seSort   SymEnv
e2
                    , seTheory :: SEnv TheorySymbol
seTheory = SymEnv -> SEnv TheorySymbol
seTheory SymEnv
e1 forall a. Semigroup a => a -> a -> a
<> SymEnv -> SEnv TheorySymbol
seTheory SymEnv
e2
                    , seData :: SEnv DataDecl
seData   = SymEnv -> SEnv DataDecl
seData   SymEnv
e1 forall a. Semigroup a => a -> a -> a
<> SymEnv -> SEnv DataDecl
seData   SymEnv
e2
                    , seLits :: SEnv Sort
seLits   = SymEnv -> SEnv Sort
seLits   SymEnv
e1 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 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 forall a. SEnv a
emptySEnv forall a. SEnv a
emptySEnv forall a. SEnv a
emptySEnv forall a. SEnv a
emptySEnv forall a. Monoid a => a
mempty
  mappend :: SymEnv -> SymEnv -> SymEnv
mappend       = 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'                 = forall a. SEnv a -> HashMap Symbol a -> SEnv a
unionSEnv SEnv Sort
xEnv HashMap Symbol Sort
wiredInEnv
    dEnv :: SEnv DataDecl
dEnv                  = forall a. [(Symbol, a)] -> SEnv a
fromListSEnv [(forall a. Symbolic a => a -> Symbol
symbol DataDecl
d, DataDecl
d) | DataDecl
d <- [DataDecl]
ds]
    sortMap :: HashMap FuncSort Int
sortMap               = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList (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 = 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 forall a b. (a -> b) -> a -> b
$ Int -> Sort -> Sort
FAbs Int
1 forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
0) (Int -> Sort
FVar Int
1))
  ]


-- | '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         = forall a. Ord a => [a] -> [a]
Misc.sortNub forall a b. (a -> b) -> a -> b
$ 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 = 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 = 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 = 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 = 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 -> Raw
symbolAtName Symbol
mkSym SymEnv
env a
e = forall a. PPrint a => Symbol -> SymEnv -> a -> FuncSort -> Raw
symbolAtSmtName Symbol
mkSym SymEnv
env a
e 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 -> Raw
symbolAtSmtName Symbol
mkSym SymEnv
env a
e FuncSort
s =
  -- formerly: intSymbol mkSym . funcSortIndex env e
  Symbol -> Raw -> Raw
appendSymbolText Symbol
mkSym forall a b. (a -> b) -> a -> b
$ String -> Raw
Text.pack (forall a. Show a => a -> String
show (forall a. PPrint a => SymEnv -> a -> FuncSort -> Int
funcSortIndex SymEnv
env a
e FuncSort
s))
{-# SCC symbolAtSmtName #-}

funcSortIndex :: (PPrint a) => SymEnv -> a -> FuncSort -> Int
funcSortIndex :: forall a. PPrint a => SymEnv -> a -> FuncSort -> Int
funcSortIndex SymEnv
env a
e FuncSort
z = forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault forall {a}. a
err FuncSort
z (SymEnv -> HashMap FuncSort Int
seAppls SymEnv
env)
  where
    err :: a
err               = forall a. String -> a
panic (String
"Unknown func-sort: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
showpp FuncSort
z forall a. [a] -> [a] -> [a]
++ String
" for " forall a. [a] -> [a] -> [a]
++ 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 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
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
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
Ord, Int -> TheorySymbol -> ShowS
[TheorySymbol] -> ShowS
TheorySymbol -> String
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
TheorySymbol -> DataType
TheorySymbol -> Constr
(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)
gmapMo :: 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
gmapMp :: forall (m :: * -> *).
MonadPlus 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
gmapM :: forall (m :: * -> *).
Monad m =>
(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 :: forall u. Int -> (forall d. Data d => d -> u) -> TheorySymbol -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TheorySymbol -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> TheorySymbol -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> TheorySymbol -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
Data, Typeable, 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 S.Store TheorySymbol

instance PPrint Sem where
  pprintTidy :: Tidy -> Sem -> Doc
pprintTidy Tidy
_ = String -> Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
<+> forall a. PPrint a => a -> Doc
pprint (Symbol
x, Sort
t) Doc -> Doc -> Doc
<+> Doc -> Doc
parens (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
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (Symbol
x, Sort
t) Doc -> Doc -> Doc
<+> Doc -> Doc
parens (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
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
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
Ord, Int -> Sem -> ShowS
[Sem] -> ShowS
Sem -> String
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
Sem -> DataType
Sem -> Constr
(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)
gmapMo :: 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
gmapMp :: forall (m :: * -> *).
MonadPlus 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
gmapM :: forall (m :: * -> *).
Monad m =>
(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 :: forall u. Int -> (forall d. Data d => d -> u) -> Sem -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Sem -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Sem -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Sem -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
Data, Typeable, 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 S.Store 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
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
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
Ord, Int -> SmtSort -> ShowS
[SmtSort] -> ShowS
SmtSort -> String
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
SmtSort -> DataType
SmtSort -> Constr
(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)
gmapMo :: 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
gmapMp :: forall (m :: * -> *).
MonadPlus 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
gmapM :: forall (m :: * -> *).
Monad m =>
(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 :: forall u. Int -> (forall d. Data d => d -> u) -> SmtSort -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SmtSort -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> SmtSort -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> SmtSort -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
Data, Typeable, 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 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) else id) $ -}  Sort -> SmtSort
go forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort -> Sort
unAbs 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 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 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 = 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]
_
      | Symbol
setConName forall a. Eq a => a -> a -> Bool
== forall a. Symbolic a => a -> Symbol
symbol FTycon
c  = SmtSort
SSet
    go (FTC FTycon
c) [Sort]
_
      | Symbol
mapConName forall a. Eq a => a -> a -> Bool
== forall a. Symbolic a => a -> Symbol
symbol FTycon
c  = SmtSort
SMap
    go (FTC FTycon
bv) [FTC FTycon
s]
      | Symbol
bitVecName forall a. Eq a => a -> a -> Bool
== 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 <- forall x. Symbolic x => x -> SEnv DataDecl -> Maybe Int
tyArgs FTycon
c SEnv DataDecl
env
      , let i :: Int
i = Int
n forall a. Num a => a -> a -> a
- 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Sort -> Sort
FAbs Int
m forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Sort]
ts) 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           = 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Symbol -> SEnv a -> Maybe a
lookupSEnv (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) = forall d. PPrint d => Tidy -> Doc -> [d] -> Doc
ppParens Tidy
k (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 forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> Doc
Misc.intersperse (String -> Doc
text String
"") (Doc
d forall a. a -> [a] -> [a]
: (forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [d]
ds))