{-# LANGUAGE CPP                       #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings         #-}
{-# LANGUAGE UndecidableInstances      #-}
{-# LANGUAGE PatternGuards             #-}
{-# LANGUAGE ViewPatterns              #-}

{-# OPTIONS_GHC -Wno-orphans           #-}

module Language.Fixpoint.Smt.Theories
     (
       -- * Convert theory applications TODO: merge with smt2symbol
       smt2App
       -- * Convert theory sorts
     , sortSmtSort

       -- * Convert theory symbols
     , smt2Symbol

       -- * Preamble to initialize SMT
     , preamble

       -- * Bit Vector Operations
     , sizeBv
       -- , toInt

       -- * Theory Symbols
     , theorySymbols
     , dataDeclSymbols


       -- * Theories
     , setEmpty, setEmp, setCap, setSub, setAdd, setMem
     , setCom, setCup, setDif, setSng

     , mapSel, mapCup, mapSto, mapDef

     , arrConst, arrStore, arrSelect, arrMapNot, arrMapOr, arrMapAnd, arrMapImp

      -- * Query Theories
     , isSmt2App
     , axiomLiterals
     , maxLamArg
     ) where

import           Prelude hiding (map)
import           Data.ByteString.Builder (Builder)
import           Language.Fixpoint.Types.Sorts
import           Language.Fixpoint.Types.Config
import           Language.Fixpoint.Types
import           Language.Fixpoint.Smt.Types
-- import qualified Data.HashMap.Strict      as M
import           Data.Maybe (catMaybes)
-- import           Data.Text.Format
import qualified Data.Text
import           Data.String                 (IsString(..))
import Language.Fixpoint.Utils.Builder

{- | [NOTE:Adding-Theories] To add new (SMTLIB supported) theories to
     liquid-fixpoint and upstream, grep for "Map_default" and then add
     your corresponding symbol in all those places.
     This is currently far more complicated than it needs to be.
 -}

--------------------------------------------------------------------------------
-- | Theory Symbols ------------------------------------------------------------
--------------------------------------------------------------------------------

-- TODO drop all of Set and Map symbols when Map is handled through arrays

-- "set" is currently \"LSet\" instead of just \"Set\" because Z3 has its own
-- \"Set\" since 4.8.5
elt, set, map :: Raw
elt :: Raw
elt  = Raw
"Elt"
set :: Raw
set  = Raw
"LSet"
map :: Raw
map  = Raw
"Map"

sel, sto, mcup, mdef, mprj :: Raw
mToSet, mshift, mmax, mmin :: Raw
sel :: Raw
sel   = Raw
"smt_map_sel"
sto :: Raw
sto   = Raw
"smt_map_sto"
mcup :: Raw
mcup  = Raw
"smt_map_cup"
mmax :: Raw
mmax  = Raw
"smt_map_max"
mmin :: Raw
mmin  = Raw
"smt_map_min"
mdef :: Raw
mdef  = Raw
"smt_map_def"
mprj :: Raw
mprj  = Raw
"smt_map_prj"
mshift :: Raw
mshift = Raw
"smt_map_shift"
mToSet :: Raw
mToSet = Raw
"smt_map_to_set"

---- Size changes
bvConcatName, bvExtractName, bvRepeatName, bvZeroExtName, bvSignExtName :: Symbol
bvConcatName :: Symbol
bvConcatName   = Symbol
"concat"
bvExtractName :: Symbol
bvExtractName  = Symbol
"extract"
bvRepeatName :: Symbol
bvRepeatName   = Symbol
"repeat"
bvZeroExtName :: Symbol
bvZeroExtName  = Symbol
"zero_extend"
bvSignExtName :: Symbol
bvSignExtName  = Symbol
"sign_extend"

-- Unary Logic
bvNotName, bvNegName :: Symbol
bvNotName :: Symbol
bvNotName = Symbol
"bvnot"
bvNegName :: Symbol
bvNegName = Symbol
"bvneg"

-- Binary Logic
bvAndName, bvNandName, bvOrName, bvNorName, bvXorName, bvXnorName :: Symbol
bvAndName :: Symbol
bvAndName  = Symbol
"bvand"
bvNandName :: Symbol
bvNandName = Symbol
"bvnand"
bvOrName :: Symbol
bvOrName   = Symbol
"bvor"
bvNorName :: Symbol
bvNorName  = Symbol
"bvnor"
bvXorName :: Symbol
bvXorName  = Symbol
"bvxor"
bvXnorName :: Symbol
bvXnorName = Symbol
"bvxnor"

-- Shifts
bvShlName, bvLShrName, bvAShrName, bvLRotName, bvRRotName :: Symbol
bvShlName :: Symbol
bvShlName  = Symbol
"bvshl"
bvLShrName :: Symbol
bvLShrName = Symbol
"bvlshr"
bvAShrName :: Symbol
bvAShrName = Symbol
"bvashr"
bvLRotName :: Symbol
bvLRotName = Symbol
"rotate_left"
bvRRotName :: Symbol
bvRRotName = Symbol
"rotate_right"

-- Arithmetic
bvAddName, bvSubName, bvMulName, bvUDivName :: Symbol
bvURemName, bvSDivName, bvSRemName, bvSModName :: Symbol
bvAddName :: Symbol
bvAddName  = Symbol
"bvadd"
bvSubName :: Symbol
bvSubName  = Symbol
"bvsub"
bvMulName :: Symbol
bvMulName  = Symbol
"bvmul"
bvUDivName :: Symbol
bvUDivName = Symbol
"bvudiv"
bvURemName :: Symbol
bvURemName = Symbol
"bvurem"
bvSDivName :: Symbol
bvSDivName = Symbol
"bvsdiv"
bvSRemName :: Symbol
bvSRemName = Symbol
"bvsrem"
bvSModName :: Symbol
bvSModName = Symbol
"bvsmod"

-- Comparisons
bvCompName, bvULtName, bvULeName, bvUGtName, bvUGeName :: Symbol
bvSLtName, bvSLeName, bvSGtName, bvSGeName :: Symbol
bvCompName :: Symbol
bvCompName = Symbol
"bvcomp"
bvULtName :: Symbol
bvULtName  = Symbol
"bvult"
bvULeName :: Symbol
bvULeName  = Symbol
"bvule"
bvUGtName :: Symbol
bvUGtName  = Symbol
"bvugt"
bvUGeName :: Symbol
bvUGeName  = Symbol
"bvuge"
bvSLtName :: Symbol
bvSLtName  = Symbol
"bvslt"
bvSLeName :: Symbol
bvSLeName  = Symbol
"bvsle"
bvSGtName :: Symbol
bvSGtName  = Symbol
"bvsgt"
bvSGeName :: Symbol
bvSGeName  = Symbol
"bvsge"

setEmpty, setEmp, setCap, setSub, setAdd, setMem, setCom, setCup, setDif, setSng :: (IsString a) => a -- Symbol
setEmpty :: forall a. IsString a => a
setEmpty = a
"Set_empty"
setEmp :: forall a. IsString a => a
setEmp   = a
"Set_emp"
setCap :: forall a. IsString a => a
setCap   = a
"Set_cap"
setSub :: forall a. IsString a => a
setSub   = a
"Set_sub"
setAdd :: forall a. IsString a => a
setAdd   = a
"Set_add"
setMem :: forall a. IsString a => a
setMem   = a
"Set_mem"
setCom :: forall a. IsString a => a
setCom   = a
"Set_com"
setCup :: forall a. IsString a => a
setCup   = a
"Set_cup"
setDif :: forall a. IsString a => a
setDif   = a
"Set_dif"
setSng :: forall a. IsString a => a
setSng   = a
"Set_sng"

--- Array operations
arrConst, arrStore, arrSelect, arrMapNot, arrMapOr, arrMapAnd, arrMapImp :: Symbol
arrConst :: Symbol
arrConst  = Symbol
"const"
arrStore :: Symbol
arrStore  = Symbol
"store"
arrSelect :: Symbol
arrSelect = Symbol
"select"
arrMapNot :: Symbol
arrMapNot = Symbol
"arr_map_not"
arrMapOr :: Symbol
arrMapOr  = Symbol
"arr_map_or"
arrMapAnd :: Symbol
arrMapAnd = Symbol
"arr_map_and"
arrMapImp :: Symbol
arrMapImp = Symbol
"arr_map_imp"

mapSel, mapSto, mapCup, mapDef, mapMax, mapMin, mapShift :: Symbol
mapSel :: Symbol
mapSel   = Symbol
"Map_select"
mapSto :: Symbol
mapSto   = Symbol
"Map_store"
mapCup :: Symbol
mapCup   = Symbol
"Map_union"
mapMax :: Symbol
mapMax   = Symbol
"Map_union_max"
mapMin :: Symbol
mapMin   = Symbol
"Map_union_min"
mapDef :: Symbol
mapDef   = Symbol
"Map_default"
mapShift :: Symbol
mapShift = Symbol
"Map_shift" -- See [Map key shift]

-- [Map key shift]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- Function mapShift: Add an integer to all keys in a map. Type signature:
--   mapShift : Int -> Map Int v -> Map Int v
-- Let's call the first argument (the shift amount) N, the second argument K1,
-- and the result K2. For all indices i, we have K2[i] = K1[i - N].
-- This is implemented with Z3's lambda, which lets us construct an array
-- from a function.
--
-- [Map max and min]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- Functions mapMax and mapMin: Union two maps, combining the elements by
-- taking either the greatest (mapMax) or the least (mapMin) of them.
--   mapMax, mapMin : Map v Int -> Map v Int -> Map v Int

mapToSet, mapPrj :: Symbol
mapToSet :: Symbol
mapToSet = Symbol
"Map_to_set"
mapPrj :: Symbol
mapPrj   = Symbol
"Map_project"

-- [Interaction between Map and Set]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- Function mapToSet: Convert a map to a set. The map's key may be of
-- any type and is preserved as the set's element type. More precisely:
--   mapToSet : Map k Int -> Set k
-- The element type must be Int. All non-positive elements are mapped
-- to False, and all positive elements are mapped to True. In practice,
-- negative elements should not exist because Map is intended to be used
-- as a bag, so the element is a non-negative number representing
-- the occurrences of its corresponding key.
--
-- Function mapPrj: Project a subset of a map. Type signature:
--   mapPrj : Set k -> Map k Int -> Map k Int
-- If the key is present in both the argument set and the argument map,
-- then the key (along with its associated value in the map) are preserved
-- in the output. Keys not present in the set are mapped to zero. Keys not
-- present in the set are mapped to zero.

strLen, strSubstr, strConcat :: (IsString a) => a -- Symbol
strLen :: forall a. IsString a => a
strLen    = a
"strLen"
strSubstr :: forall a. IsString a => a
strSubstr = a
"subString"
strConcat :: forall a. IsString a => a
strConcat = a
"concatString"

z3strlen, z3strsubstr, z3strconcat :: Raw
z3strlen :: Raw
z3strlen    = Raw
"str.len"
z3strsubstr :: Raw
z3strsubstr = Raw
"str.substr"
z3strconcat :: Raw
z3strconcat = Raw
"str.++"

strLenSort, substrSort, concatstrSort :: Sort
strLenSort :: Sort
strLenSort    = Sort -> Sort -> Sort
FFunc Sort
strSort Sort
intSort
substrSort :: Sort
substrSort    = Int -> [Sort] -> Sort
mkFFunc Int
0 [Sort
strSort, Sort
intSort, Sort
intSort, Sort
strSort]
concatstrSort :: Sort
concatstrSort = Int -> [Sort] -> Sort
mkFFunc Int
0 [Sort
strSort, Sort
strSort, Sort
strSort]

string :: Raw
string :: Raw
string = Raw
forall a. IsString a => a
strConName

bFun :: Raw -> [(Builder, Builder)] -> Builder -> Builder -> Builder
bFun :: Raw -> [(Builder, Builder)] -> Builder -> Builder -> Builder
bFun Raw
name [(Builder, Builder)]
xts Builder
out Builder
body = Builder -> Builder -> Builder
key Builder
"define-fun" ([Builder] -> Builder
seqs [Raw -> Builder
fromText Raw
name, Builder
args, Builder
out, Builder
body])
  where
    args :: Builder
args = [Builder] -> Builder
parenSeqs [Builder -> Builder
parens (Builder
x Builder -> Builder -> Builder
<+> Builder
t) | (Builder
x, Builder
t) <- [(Builder, Builder)]
xts]

bFun' :: Raw -> [Builder] -> Builder -> Builder
bFun' :: Raw -> [Builder] -> Builder -> Builder
bFun' Raw
name [Builder]
ts Builder
out = Builder -> Builder -> Builder
key Builder
"declare-fun" ([Builder] -> Builder
seqs [Raw -> Builder
fromText Raw
name, Builder
args, Builder
out])
  where
    args :: Builder
args = [Builder] -> Builder
parenSeqs [Builder]
ts

bSort :: Raw -> Builder -> Builder
bSort :: Raw -> Builder -> Builder
bSort Raw
name Builder
def = Builder -> Builder -> Builder
key Builder
"define-sort" (Raw -> Builder
fromText Raw
name Builder -> Builder -> Builder
<+> Builder
"()" Builder -> Builder -> Builder
<+> Builder
def)

z3Preamble :: Config -> [Builder]
z3Preamble :: Config -> [Builder]
z3Preamble Config
u
  = Config -> [Builder]
stringPreamble Config
u [Builder] -> [Builder] -> [Builder]
forall a. [a] -> [a] -> [a]
++
    [ Raw -> Builder -> Builder
bSort Raw
elt
        Builder
"Int"
    , Raw -> Builder -> Builder
bSort Raw
set
        (Builder -> Builder -> Builder -> Builder
key2 Builder
"Array" (Raw -> Builder
fromText Raw
elt) Builder
"Bool")

    -- Maps
    , Raw -> Builder -> Builder
bSort Raw
map
        (Builder -> Builder -> Builder -> Builder
key2 Builder
"Array" (Raw -> Builder
fromText Raw
elt) (Raw -> Builder
fromText Raw
elt))
    , Raw -> [(Builder, Builder)] -> Builder -> Builder -> Builder
bFun Raw
sel
        [(Builder
"m", Raw -> Builder
fromText Raw
map), (Builder
"k", Raw -> Builder
fromText Raw
elt)]
        (Raw -> Builder
fromText Raw
elt)
        Builder
"(select m k)"
    , Raw -> [(Builder, Builder)] -> Builder -> Builder -> Builder
bFun Raw
sto
        [(Builder
"m", Raw -> Builder
fromText Raw
map), (Builder
"k", Raw -> Builder
fromText Raw
elt), (Builder
"v", Raw -> Builder
fromText Raw
elt)]
        (Raw -> Builder
fromText Raw
map)
        Builder
"(store m k v)"
    , Raw -> [(Builder, Builder)] -> Builder -> Builder -> Builder
bFun Raw
mcup
        [(Builder
"m1", Raw -> Builder
fromText Raw
map), (Builder
"m2", Raw -> Builder
fromText Raw
map)]
        (Raw -> Builder
fromText Raw
map)
        (Builder -> Builder -> Builder -> Builder
key2 (Builder -> Builder -> Builder
key Builder
"_ map" (Builder -> Builder -> Builder -> Builder
key2 Builder
"+" (Builder -> Builder
parens (Raw -> Builder
fromText Raw
elt Builder -> Builder -> Builder
<+> Raw -> Builder
fromText Raw
elt)) (Raw -> Builder
fromText Raw
elt))) Builder
"m1" Builder
"m2")
    , Raw -> [(Builder, Builder)] -> Builder -> Builder -> Builder
bFun Raw
mprj -- See [Interaction Between Map and Set]
        [(Builder
"s", Raw -> Builder
fromText Raw
set), (Builder
"m", Raw -> Builder
fromText Raw
map)]
        (Raw -> Builder
fromText Raw
map)
        (Builder -> Builder -> Builder -> Builder -> Builder
key3
          (Builder -> Builder -> Builder
key Builder
"_ map"
            (Builder -> Builder -> Builder -> Builder
key2 Builder
"ite"
              (Builder -> Builder
parens (Builder
"Bool" Builder -> Builder -> Builder
<+> Raw -> Builder
fromText Raw
elt Builder -> Builder -> Builder
<+> Raw -> Builder
fromText Raw
elt))
              (Raw -> Builder
fromText Raw
elt)
            )
          )
          Builder
"s"
          Builder
"m"
          (Builder -> Builder
parens (Builder -> Builder -> Builder
key Builder
"as const" (Builder -> Builder -> Builder -> Builder
key2 Builder
"Array" (Raw -> Builder
fromText Raw
elt) (Raw -> Builder
fromText Raw
elt)) Builder -> Builder -> Builder
<+> Builder
"0"))
        )
    , Raw -> [(Builder, Builder)] -> Builder -> Builder -> Builder
bFun Raw
mToSet -- See [Interaction Between Map and Set]
        [(Builder
"m", Raw -> Builder
fromText Raw
map)]
        (Raw -> Builder
fromText Raw
set)
        (Builder -> Builder -> Builder -> Builder
key2
          (Builder -> Builder -> Builder
key Builder
"_ map"
            (Builder -> Builder -> Builder -> Builder
key2 Builder
">"
              (Builder -> Builder
parens (Raw -> Builder
fromText Raw
elt Builder -> Builder -> Builder
<+> Raw -> Builder
fromText Raw
elt))
              Builder
"Bool"
            )
          )
          Builder
"m"
          (Builder -> Builder
parens (Builder -> Builder -> Builder
key Builder
"as const" (Builder -> Builder -> Builder -> Builder
key2 Builder
"Array" (Raw -> Builder
fromText Raw
elt) (Raw -> Builder
fromText Raw
elt)) Builder -> Builder -> Builder
<+> Builder
"0"))
        )
    , Raw -> [(Builder, Builder)] -> Builder -> Builder -> Builder
bFun Raw
mmax -- See [Map max and min]
        [(Builder
"m1", Raw -> Builder
fromText Raw
map),(Builder
"m2", Raw -> Builder
fromText Raw
map)]
        (Raw -> Builder
fromText Raw
map)
        Builder
"(lambda ((i Int)) (ite (> (select m1 i) (select m2 i)) (select m1 i) (select m2 i)))"
    , Raw -> [(Builder, Builder)] -> Builder -> Builder -> Builder
bFun Raw
mmin -- See [Map max and min]
        [(Builder
"m1", Raw -> Builder
fromText Raw
map),(Builder
"m2", Raw -> Builder
fromText Raw
map)]
        (Raw -> Builder
fromText Raw
map)
        Builder
"(lambda ((i Int)) (ite (< (select m1 i) (select m2 i)) (select m1 i) (select m2 i)))"
    , Raw -> [(Builder, Builder)] -> Builder -> Builder -> Builder
bFun Raw
mshift -- See [Map key shift]
        [(Builder
"n", Builder
"Int"),(Builder
"m", Raw -> Builder
fromText Raw
map)]
        (Raw -> Builder
fromText Raw
map)
        Builder
"(lambda ((i Int)) (select m (- i n)))"
    , Raw -> [(Builder, Builder)] -> Builder -> Builder -> Builder
bFun Raw
mdef
        [(Builder
"v", Raw -> Builder
fromText Raw
elt)]
        (Raw -> Builder
fromText Raw
map)
        (Builder -> Builder -> Builder
key (Builder -> Builder -> Builder
key Builder
"as const" (Builder -> Builder
parens (Raw -> Builder
fromText Raw
map))) Builder
"v")
    , Raw -> [(Builder, Builder)] -> Builder -> Builder -> Builder
bFun Raw
forall a. IsString a => a
boolToIntName
        [(Builder
"b", Builder
"Bool")]
        Builder
"Int"
        Builder
"(ite b 1 0)"

    , Config -> Raw -> Raw -> Builder
uifDef Config
u (Symbol -> Raw
symbolText Symbol
mulFuncName) Raw
"*"
    , Config -> Raw -> Raw -> Builder
uifDef Config
u (Symbol -> Raw
symbolText Symbol
divFuncName) Raw
"div"
    ]

-- RJ: Am changing this to `Int` not `Real` as (1) we usually want `Int` and
-- (2) have very different semantics. TODO: proper overloading, post genEApp
uifDef :: Config -> Data.Text.Text -> Data.Text.Text -> Builder
uifDef :: Config -> Raw -> Raw -> Builder
uifDef Config
cfg Raw
f Raw
op
  | Config -> Bool
linear Config
cfg Bool -> Bool -> Bool
|| SMTSolver
Z3 SMTSolver -> SMTSolver -> Bool
forall a. Eq a => a -> a -> Bool
/= Config -> SMTSolver
solver Config
cfg
  = Raw -> [Builder] -> Builder -> Builder
bFun' Raw
f [Builder
"Int", Builder
"Int"] Builder
"Int"
  | Bool
otherwise
  = Raw -> [(Builder, Builder)] -> Builder -> Builder -> Builder
bFun Raw
f [(Builder
"x", Builder
"Int"), (Builder
"y", Builder
"Int")] Builder
"Int" (Builder -> Builder -> Builder -> Builder
key2 (Raw -> Builder
fromText Raw
op) Builder
"x" Builder
"y")

cvc4Preamble :: Config -> [Builder]
cvc4Preamble :: Config -> [Builder]
cvc4Preamble Config
z
  = [        Builder
"(set-logic ALL_SUPPORTED)"]
  [Builder] -> [Builder] -> [Builder]
forall a. [a] -> [a] -> [a]
++ Config -> [Builder]
commonPreamble Config
z
  [Builder] -> [Builder] -> [Builder]
forall a. [a] -> [a] -> [a]
++ Config -> [Builder]
cvc4MapPreamble Config
z

commonPreamble :: Config -> [Builder]
commonPreamble :: Config -> [Builder]
commonPreamble Config
_ --TODO use uif flag u (see z3Preamble)
  = [ Raw -> Builder -> Builder
bSort Raw
elt    Builder
"Int"
    , Raw -> Builder -> Builder
bSort Raw
set    Builder
"Int"
    , Raw -> Builder -> Builder
bSort Raw
string Builder
"Int"
    , Raw -> [(Builder, Builder)] -> Builder -> Builder -> Builder
bFun Raw
forall a. IsString a => a
boolToIntName [(Builder
"b", Builder
"Bool")] Builder
"Int" Builder
"(ite b 1 0)"
    ]

cvc4MapPreamble :: Config -> [Builder]
cvc4MapPreamble :: Config -> [Builder]
cvc4MapPreamble Config
_ =
    [ Raw -> Builder -> Builder
bSort Raw
map    (Builder -> Builder -> Builder -> Builder
key2 Builder
"Array" (Raw -> Builder
fromText Raw
elt) (Raw -> Builder
fromText Raw
elt))
    , Raw -> [(Builder, Builder)] -> Builder -> Builder -> Builder
bFun Raw
sel [(Builder
"m", Raw -> Builder
fromText Raw
map), (Builder
"k", Raw -> Builder
fromText Raw
elt)]                (Raw -> Builder
fromText Raw
elt) Builder
"(select m k)"
    , Raw -> [(Builder, Builder)] -> Builder -> Builder -> Builder
bFun Raw
sto [(Builder
"m", Raw -> Builder
fromText Raw
map), (Builder
"k", Raw -> Builder
fromText Raw
elt), (Builder
"v", Raw -> Builder
fromText Raw
elt)] (Raw -> Builder
fromText Raw
map) Builder
"(store m k v)"
    ]

smtlibPreamble :: Config -> [Builder]
smtlibPreamble :: Config -> [Builder]
smtlibPreamble Config
z --TODO use uif flag u (see z3Preamble)
  = Config -> [Builder]
commonPreamble Config
z
 [Builder] -> [Builder] -> [Builder]
forall a. [a] -> [a] -> [a]
++ [ Raw -> Builder -> Builder
bSort Raw
map Builder
"Int"
    , Raw -> [Builder] -> Builder -> Builder
bFun' Raw
sel [Raw -> Builder
fromText Raw
map, Raw -> Builder
fromText Raw
elt] (Raw -> Builder
fromText Raw
elt)
    , Raw -> [Builder] -> Builder -> Builder
bFun' Raw
sto [Raw -> Builder
fromText Raw
map, Raw -> Builder
fromText Raw
elt, Raw -> Builder
fromText Raw
elt] (Raw -> Builder
fromText Raw
map)
    ]

stringPreamble :: Config -> [Builder]
stringPreamble :: Config -> [Builder]
stringPreamble Config
cfg | Config -> Bool
stringTheory Config
cfg
  = [ Raw -> Builder -> Builder
bSort Raw
string Builder
"String"
    , Raw -> [(Builder, Builder)] -> Builder -> Builder -> Builder
bFun Raw
forall a. IsString a => a
strLen [(Builder
"s", Raw -> Builder
fromText Raw
string)] Builder
"Int" (Builder -> Builder -> Builder
key (Raw -> Builder
fromText Raw
z3strlen) Builder
"s")
    , Raw -> [(Builder, Builder)] -> Builder -> Builder -> Builder
bFun Raw
forall a. IsString a => a
strSubstr [(Builder
"s", Raw -> Builder
fromText Raw
string), (Builder
"i", Builder
"Int"), (Builder
"j", Builder
"Int")] (Raw -> Builder
fromText Raw
string) (Builder -> Builder -> Builder
key (Raw -> Builder
fromText Raw
z3strsubstr) Builder
"s i j")
    , Raw -> [(Builder, Builder)] -> Builder -> Builder -> Builder
bFun Raw
forall a. IsString a => a
strConcat [(Builder
"x", Raw -> Builder
fromText Raw
string), (Builder
"y", Raw -> Builder
fromText Raw
string)] (Raw -> Builder
fromText Raw
string) (Builder -> Builder -> Builder
key (Raw -> Builder
fromText Raw
z3strconcat) Builder
"x y")
    ]

stringPreamble Config
_
  = [ Raw -> Builder -> Builder
bSort Raw
string Builder
"Int"
    , Raw -> [Builder] -> Builder -> Builder
bFun' Raw
forall a. IsString a => a
strLen [Raw -> Builder
fromText Raw
string] Builder
"Int"
    , Raw -> [Builder] -> Builder -> Builder
bFun' Raw
forall a. IsString a => a
strSubstr [Raw -> Builder
fromText Raw
string, Builder
"Int", Builder
"Int"] (Raw -> Builder
fromText Raw
string)
    , Raw -> [Builder] -> Builder -> Builder
bFun' Raw
forall a. IsString a => a
strConcat [Raw -> Builder
fromText Raw
string, Raw -> Builder
fromText Raw
string] (Raw -> Builder
fromText Raw
string)
    ]

--------------------------------------------------------------------------------
-- | Exported API --------------------------------------------------------------
--------------------------------------------------------------------------------
smt2Symbol :: SymEnv -> Symbol -> Maybe Builder
smt2Symbol :: SymEnv -> Symbol -> Maybe Builder
smt2Symbol SymEnv
env Symbol
x = Raw -> Builder
fromText (Raw -> Builder)
-> (TheorySymbol -> Raw) -> TheorySymbol -> Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TheorySymbol -> Raw
tsRaw (TheorySymbol -> Builder) -> Maybe TheorySymbol -> Maybe Builder
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Symbol -> SymEnv -> Maybe TheorySymbol
symEnvTheory Symbol
x SymEnv
env

instance SMTLIB2 SmtSort where
  smt2 :: SymEnv -> SmtSort -> Builder
smt2 SymEnv
_ = SmtSort -> Builder
smt2SmtSort

smt2SmtSort :: SmtSort -> Builder
smt2SmtSort :: SmtSort -> Builder
smt2SmtSort SmtSort
SInt         = Builder
"Int"
smt2SmtSort SmtSort
SReal        = Builder
"Real"
smt2SmtSort SmtSort
SBool        = Builder
"Bool"
smt2SmtSort SmtSort
SString      = Raw -> Builder
fromText Raw
string
smt2SmtSort SmtSort
SSet         = Raw -> Builder
fromText Raw
set
smt2SmtSort SmtSort
SMap         = Raw -> Builder
fromText Raw
map
smt2SmtSort (SArray SmtSort
a SmtSort
b) = Builder -> Builder -> Builder -> Builder
key2 Builder
"Array" (SmtSort -> Builder
smt2SmtSort SmtSort
a) (SmtSort -> Builder
smt2SmtSort SmtSort
b)
smt2SmtSort (SBitVec Int
n)  = Builder -> Builder -> Builder
key Builder
"_ BitVec" (Int -> Builder
forall a. Show a => a -> Builder
bShow Int
n)
smt2SmtSort (SVar Int
n)     = Builder
"T" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Int -> Builder
forall a. Show a => a -> Builder
bShow Int
n
smt2SmtSort (SData FTycon
c []) = FTycon -> Builder
forall a. Symbolic a => a -> Builder
symbolBuilder FTycon
c
smt2SmtSort (SData FTycon
c [SmtSort]
ts) = [Builder] -> Builder
parenSeqs [FTycon -> Builder
forall a. Symbolic a => a -> Builder
symbolBuilder FTycon
c, [SmtSort] -> Builder
smt2SmtSorts [SmtSort]
ts]

-- smt2SmtSort (SApp ts)    = build "({} {})" (symbolBuilder tyAppName, smt2SmtSorts ts)

smt2SmtSorts :: [SmtSort] -> Builder
smt2SmtSorts :: [SmtSort] -> Builder
smt2SmtSorts = [Builder] -> Builder
seqs ([Builder] -> Builder)
-> ([SmtSort] -> [Builder]) -> [SmtSort] -> Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SmtSort -> Builder) -> [SmtSort] -> [Builder]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SmtSort -> Builder
smt2SmtSort

type VarAs = SymEnv -> Symbol -> Sort -> Builder
--------------------------------------------------------------------------------
smt2App :: VarAs -> SymEnv -> Expr -> [Builder] -> Maybe Builder
--------------------------------------------------------------------------------
smt2App :: VarAs -> SymEnv -> Expr -> [Builder] -> Maybe Builder
smt2App VarAs
_ SymEnv
env ex :: Expr
ex@(Expr -> Expr
dropECst -> EVar Symbol
f) [Builder
d]
  | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
arrConst = Builder -> Maybe Builder
forall a. a -> Maybe a
Just (Builder -> Builder -> Builder
key (Builder -> Builder -> Builder
key Builder
"as const" (Expr -> Builder
getTarget Expr
ex)) Builder
d)
  where
    getTarget :: Expr -> Builder
    -- const is a function, but SMT expects only the output sort
    getTarget :: Expr -> Builder
getTarget (ECst Expr
_ Sort
t) = SmtSort -> Builder
smt2SmtSort (SmtSort -> Builder) -> SmtSort -> Builder
forall a b. (a -> b) -> a -> b
$ Bool -> SEnv DataDecl -> Sort -> SmtSort
sortSmtSort Bool
True (SymEnv -> SEnv DataDecl
seData SymEnv
env) (Sort -> Sort
ffuncOut Sort
t)
    getTarget Expr
e = Expr -> Builder
forall a. Show a => a -> Builder
bShow Expr
e

smt2App VarAs
k SymEnv
env Expr
ex (Builder
builder:[Builder]
builders)
  | Just Builder
fb <- VarAs -> SymEnv -> Expr -> Maybe Builder
smt2AppArg VarAs
k SymEnv
env Expr
ex
  = Builder -> Maybe Builder
forall a. a -> Maybe a
Just (Builder -> Maybe Builder) -> Builder -> Maybe Builder
forall a b. (a -> b) -> a -> b
$ Builder -> Builder -> Builder
key Builder
fb (Builder
builder Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> [Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat [ Builder
" " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
d | Builder
d <- [Builder]
builders])

smt2App VarAs
_ SymEnv
_ Expr
_ [Builder]
_    = Maybe Builder
forall a. Maybe a
Nothing

smt2AppArg :: VarAs -> SymEnv -> Expr -> Maybe Builder
smt2AppArg :: VarAs -> SymEnv -> Expr -> Maybe Builder
smt2AppArg VarAs
k SymEnv
env (ECst (Expr -> Expr
dropECst -> EVar Symbol
f) Sort
t)
  | Just TheorySymbol
fThy <- Symbol -> SymEnv -> Maybe TheorySymbol
symEnvTheory Symbol
f SymEnv
env
  = Builder -> Maybe Builder
forall a. a -> Maybe a
Just (Builder -> Maybe Builder) -> Builder -> Maybe Builder
forall a b. (a -> b) -> a -> b
$ if TheorySymbol -> Sort -> Bool
isPolyCtor TheorySymbol
fThy Sort
t
            then VarAs
k SymEnv
env Symbol
f (Sort -> Sort
ffuncOut Sort
t)
            else Raw -> Builder
fromText (TheorySymbol -> Raw
tsRaw TheorySymbol
fThy)

smt2AppArg VarAs
_ SymEnv
_ Expr
_
  = Maybe Builder
forall a. Maybe a
Nothing

isPolyCtor :: TheorySymbol -> Sort -> Bool
isPolyCtor :: TheorySymbol -> Sort -> Bool
isPolyCtor TheorySymbol
fThy Sort
t = Sort -> Sort -> Bool
isPolyInst (TheorySymbol -> Sort
tsSort TheorySymbol
fThy) Sort
t Bool -> Bool -> Bool
&& TheorySymbol -> Sem
tsInterp TheorySymbol
fThy Sem -> Sem -> Bool
forall a. Eq a => a -> a -> Bool
== Sem
Ctor

ffuncOut :: Sort -> Sort
ffuncOut :: Sort -> Sort
ffuncOut Sort
t = Sort -> ((Int, [Sort]) -> Sort) -> Maybe (Int, [Sort]) -> Sort
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Sort
t ([Sort] -> Sort
forall a. HasCallStack => [a] -> a
last ([Sort] -> Sort)
-> ((Int, [Sort]) -> [Sort]) -> (Int, [Sort]) -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, [Sort]) -> [Sort]
forall a b. (a, b) -> b
snd) (Sort -> Maybe (Int, [Sort])
bkFFunc Sort
t)

--------------------------------------------------------------------------------
isSmt2App :: SEnv TheorySymbol -> Expr -> Maybe Int
--------------------------------------------------------------------------------
isSmt2App :: SEnv TheorySymbol -> Expr -> Maybe Int
isSmt2App SEnv TheorySymbol
g (Expr -> Expr
dropECst -> EVar Symbol
f) = Symbol -> SEnv TheorySymbol -> Maybe TheorySymbol
forall a. Symbol -> SEnv a -> Maybe a
lookupSEnv Symbol
f SEnv TheorySymbol
g Maybe TheorySymbol -> (TheorySymbol -> Maybe Int) -> Maybe Int
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= TheorySymbol -> Maybe Int
thyAppInfo
isSmt2App SEnv TheorySymbol
_  Expr
_                   = Maybe Int
forall a. Maybe a
Nothing

thyAppInfo :: TheorySymbol -> Maybe Int
thyAppInfo :: TheorySymbol -> Maybe Int
thyAppInfo TheorySymbol
ti = case TheorySymbol -> Sem
tsInterp TheorySymbol
ti of
  Sem
Field    -> Int -> Maybe Int
forall a. a -> Maybe a
Just Int
1
  Sem
_        -> Sort -> Maybe Int
sortAppInfo (TheorySymbol -> Sort
tsSort TheorySymbol
ti)

sortAppInfo :: Sort -> Maybe Int
sortAppInfo :: Sort -> Maybe Int
sortAppInfo Sort
t = case Sort -> Maybe (Int, [Sort])
bkFFunc Sort
t of
  Just (Int
_, [Sort]
ts) -> Int -> Maybe Int
forall a. a -> Maybe a
Just ([Sort] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Sort]
ts Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
  Maybe (Int, [Sort])
Nothing      -> Maybe Int
forall a. Maybe a
Nothing

preamble :: Config -> SMTSolver -> [Builder]
preamble :: Config -> SMTSolver -> [Builder]
preamble Config
u SMTSolver
Z3   = Config -> [Builder]
z3Preamble Config
u
preamble Config
u SMTSolver
Cvc4 = Config -> [Builder]
cvc4Preamble Config
u
preamble Config
u SMTSolver
_    = Config -> [Builder]
smtlibPreamble Config
u

--------------------------------------------------------------------------------
-- | Theory Symbols : `uninterpSEnv` should be disjoint from see `interpSEnv`
--   to avoid duplicate SMT definitions.  `uninterpSEnv` is for uninterpreted
--   symbols, and `interpSEnv` is for interpreted symbols.
--------------------------------------------------------------------------------

-- | `theorySymbols` contains the list of ALL SMT symbols with interpretations,
--   i.e. which are given via `define-fun` (as opposed to `declare-fun`)
theorySymbols :: [DataDecl] -> SEnv TheorySymbol -- M.HashMap Symbol TheorySymbol
theorySymbols :: [DataDecl] -> SEnv TheorySymbol
theorySymbols [DataDecl]
ds = [(Symbol, TheorySymbol)] -> SEnv TheorySymbol
forall a. [(Symbol, a)] -> SEnv a
fromListSEnv ([(Symbol, TheorySymbol)] -> SEnv TheorySymbol)
-> [(Symbol, TheorySymbol)] -> SEnv TheorySymbol
forall a b. (a -> b) -> a -> b
$  -- SHIFTLAM uninterpSymbols
                                  [(Symbol, TheorySymbol)]
interpSymbols
                               [(Symbol, TheorySymbol)]
-> [(Symbol, TheorySymbol)] -> [(Symbol, TheorySymbol)]
forall a. [a] -> [a] -> [a]
++ (DataDecl -> [(Symbol, TheorySymbol)])
-> [DataDecl] -> [(Symbol, TheorySymbol)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap DataDecl -> [(Symbol, TheorySymbol)]
dataDeclSymbols [DataDecl]
ds


--------------------------------------------------------------------------------
interpSymbols :: [(Symbol, TheorySymbol)]
--------------------------------------------------------------------------------
interpSymbols :: [(Symbol, TheorySymbol)]
interpSymbols =
  [
  -- TODO we'll probably need two versions of these - one for sets and one for maps
    Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
arrConst  Raw
"const"       (Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
boolSort Sort
setArrSort)
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
arrStore  Raw
"store"       (Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
setArrSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
0) (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
boolSort Sort
setArrSort)
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
arrSelect Raw
"select"      (Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
setArrSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
0) Sort
boolSort)
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
arrMapNot Raw
"(_ map not)" (Sort -> Sort -> Sort
FFunc Sort
setArrSort Sort
setArrSort)
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
arrMapOr  Raw
"(_ map or)"  (Sort -> Sort -> Sort
FFunc Sort
setArrSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
setArrSort Sort
setArrSort)
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
arrMapAnd Raw
"(_ map and)" (Sort -> Sort -> Sort
FFunc Sort
setArrSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
setArrSort Sort
setArrSort)
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
arrMapImp Raw
"(_ map =>)"  (Sort -> Sort -> Sort
FFunc Sort
setArrSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
setArrSort Sort
setArrSort)

  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
setEmp   Raw
forall a. IsString a => a
setEmp   (Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort
setSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort
FVar Int
0) Sort
boolSort)
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
setEmpty Raw
forall a. IsString a => a
setEmpty (Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
intSort (Sort -> Sort
setSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort
FVar Int
0))
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
setSng   Raw
forall a. IsString a => a
setSng   (Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
0) (Sort -> Sort
setSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort
FVar Int
0))
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
setAdd   Raw
forall a. IsString a => a
setAdd   Sort
setAddSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
setCup   Raw
forall a. IsString a => a
setCup   Sort
setBopSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
setCap   Raw
forall a. IsString a => a
setCap   Sort
setBopSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
setMem   Raw
forall a. IsString a => a
setMem   Sort
setMemSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
setDif   Raw
forall a. IsString a => a
setDif   Sort
setBopSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
setSub   Raw
forall a. IsString a => a
setSub   Sort
setCmpSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
setCom   Raw
forall a. IsString a => a
setCom   Sort
setCmpSort

  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
mapSel   Raw
sel   Sort
mapSelSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
mapSto   Raw
sto   Sort
mapStoSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
mapCup   Raw
mcup  Sort
mapCupSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
mapMax   Raw
mmax  Sort
mapMaxSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
mapMin   Raw
mmin  Sort
mapMinSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
mapDef   Raw
mdef  Sort
mapDefSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
mapPrj   Raw
mprj  Sort
mapPrjSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
mapShift Raw
mshift Sort
mapShiftSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
mapToSet Raw
mToSet Sort
mapToSetSort

  -- , interpSym bvOrName  "bvor"  bvBopSort
  -- , interpSym bvAndName "bvand" bvBopSort
  -- , interpSym bvAddName "bvadd" bvBopSort
  -- , interpSym bvSubName "bvsub" bvBopSort

  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
strLen    Raw
forall a. IsString a => a
strLen    Sort
strLenSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
strSubstr Raw
forall a. IsString a => a
strSubstr Sort
substrSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
strConcat Raw
forall a. IsString a => a
strConcat Sort
concatstrSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
boolInt   Raw
forall a. IsString a => a
boolInt   (Sort -> Sort -> Sort
FFunc Sort
boolSort Sort
intSort)

  -- Function mappings for indexed identifier functions
  , Symbol -> Sort -> (Symbol, TheorySymbol)
interpSym' Symbol
"_" Sort
iiSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
"app" Raw
"" Sort
appSort

  , Symbol -> Sort -> (Symbol, TheorySymbol)
interpSym' Symbol
bvConcatName Sort
bvConcatSort
  , Symbol -> Sort -> (Symbol, TheorySymbol)
interpSym' Symbol
bvExtractName (Sort -> Sort -> Sort
FFunc Sort
FInt Sort
bvExtendSort)
  , Symbol -> (Symbol, TheorySymbol)
interpBvExt Symbol
bvRepeatName
  , Symbol -> (Symbol, TheorySymbol)
interpBvExt Symbol
bvZeroExtName
  , Symbol -> (Symbol, TheorySymbol)
interpBvExt Symbol
bvSignExtName

  , Symbol -> (Symbol, TheorySymbol)
interpBvUop Symbol
bvNotName
  , Symbol -> (Symbol, TheorySymbol)
interpBvUop Symbol
bvNegName

  , Symbol -> (Symbol, TheorySymbol)
interpBvBop Symbol
bvAndName
  , Symbol -> (Symbol, TheorySymbol)
interpBvBop Symbol
bvNandName
  , Symbol -> (Symbol, TheorySymbol)
interpBvBop Symbol
bvOrName
  , Symbol -> (Symbol, TheorySymbol)
interpBvBop Symbol
bvNorName
  , Symbol -> (Symbol, TheorySymbol)
interpBvBop Symbol
bvXorName
  , Symbol -> (Symbol, TheorySymbol)
interpBvBop Symbol
bvXnorName

  , Symbol -> (Symbol, TheorySymbol)
interpBvBop Symbol
bvShlName
  , Symbol -> (Symbol, TheorySymbol)
interpBvBop Symbol
bvLShrName
  , Symbol -> (Symbol, TheorySymbol)
interpBvBop Symbol
bvAShrName
  , Symbol -> (Symbol, TheorySymbol)
interpBvRot Symbol
bvLRotName
  , Symbol -> (Symbol, TheorySymbol)
interpBvRot Symbol
bvRRotName

  , Symbol -> (Symbol, TheorySymbol)
interpBvBop Symbol
bvAddName
  , Symbol -> (Symbol, TheorySymbol)
interpBvBop Symbol
bvSubName
  , Symbol -> (Symbol, TheorySymbol)
interpBvBop Symbol
bvMulName
  , Symbol -> (Symbol, TheorySymbol)
interpBvBop Symbol
bvUDivName
  , Symbol -> (Symbol, TheorySymbol)
interpBvBop Symbol
bvURemName
  , Symbol -> (Symbol, TheorySymbol)
interpBvBop Symbol
bvSDivName
  , Symbol -> (Symbol, TheorySymbol)
interpBvBop Symbol
bvSRemName
  , Symbol -> (Symbol, TheorySymbol)
interpBvBop Symbol
bvSModName

  , Symbol -> Sort -> (Symbol, TheorySymbol)
interpSym' Symbol
bvCompName Sort
bvEqSort
  , Symbol -> (Symbol, TheorySymbol)
interpBvCmp Symbol
bvULtName
  , Symbol -> (Symbol, TheorySymbol)
interpBvCmp Symbol
bvULeName
  , Symbol -> (Symbol, TheorySymbol)
interpBvCmp Symbol
bvUGtName
  , Symbol -> (Symbol, TheorySymbol)
interpBvCmp Symbol
bvUGeName
  , Symbol -> (Symbol, TheorySymbol)
interpBvCmp Symbol
bvSLtName
  , Symbol -> (Symbol, TheorySymbol)
interpBvCmp Symbol
bvSLeName
  , Symbol -> (Symbol, TheorySymbol)
interpBvCmp Symbol
bvSGtName
  , Symbol -> (Symbol, TheorySymbol)
interpBvCmp Symbol
bvSGeName

  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
intbv32Name Raw
"(_ int2bv 32)"   (Sort -> Sort -> Sort
FFunc Sort
intSort Sort
bv32)
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
intbv64Name Raw
"(_ int2bv 64)"   (Sort -> Sort -> Sort
FFunc Sort
intSort Sort
bv64)
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
bv32intName  Raw
"(_ bv2int 32)"  (Sort -> Sort -> Sort
FFunc Sort
bv32    Sort
intSort)
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
bv64intName   Raw
"(_ bv2int 64)" (Sort -> Sort -> Sort
FFunc Sort
bv64    Sort
intSort)

  ]
  where
    setArrSort :: Sort
setArrSort = Sort -> Sort -> Sort
arraySort (Int -> Sort
FVar Int
0) Sort
boolSort
    -- (sizedBitVecSort "Size1")
    bv32 :: Sort
bv32       = Symbol -> Sort
sizedBitVecSort Symbol
"Size32"
    bv64 :: Sort
bv64       = Symbol -> Sort
sizedBitVecSort Symbol
"Size64"
    boolInt :: a
boolInt    = a
forall a. IsString a => a
boolToIntName

    setAddSort :: Sort
setAddSort = Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort
setSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort
FVar Int
0) (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
0)           (Sort -> Sort
setSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort
FVar Int
0)
    setBopSort :: Sort
setBopSort = Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort
setSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort
FVar Int
0) (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort
setSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort
FVar Int
0) (Sort -> Sort
setSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort
FVar Int
0)
    setMemSort :: Sort
setMemSort = Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
0) (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort
setSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort
FVar Int
0) Sort
boolSort
    setCmpSort :: Sort
setCmpSort = Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort
setSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort
FVar Int
0) (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort
setSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort
FVar Int
0) Sort
boolSort

    -- select :: forall i a. Map i a -> i -> a
    mapSelSort :: Sort
mapSelSort = Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort -> Sort
FAbs Int
1 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort -> Sort
mapSort (Int -> Sort
FVar Int
0) (Int -> Sort
FVar Int
1))
                                 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
0) (Int -> Sort
FVar Int
1)
    -- cup :: forall i. Map i Int -> Map i Int -> Map i Int
    mapCupSort :: Sort
mapCupSort = Int -> Sort -> Sort
FAbs Int
0          (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort -> Sort
mapSort (Int -> Sort
FVar Int
0) Sort
intSort)
                                 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort -> Sort
mapSort (Int -> Sort
FVar Int
0) Sort
intSort)
                                         (Sort -> Sort -> Sort
mapSort (Int -> Sort
FVar Int
0) Sort
intSort)
    mapMaxSort :: Sort
mapMaxSort = Sort
mapCupSort
    mapMinSort :: Sort
mapMinSort = Sort
mapCupSort
    mapPrjSort :: Sort
mapPrjSort = Int -> Sort -> Sort
FAbs Int
0          (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort
setSort (Int -> Sort
FVar Int
0))
                                 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort -> Sort
mapSort (Int -> Sort
FVar Int
0) Sort
intSort)
                                         (Sort -> Sort -> Sort
mapSort (Int -> Sort
FVar Int
0) Sort
intSort)
    mapShiftSort :: Sort
mapShiftSort = Int -> Sort -> Sort
FAbs Int
0        (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
intSort
                                 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort -> Sort
mapSort Sort
intSort (Int -> Sort
FVar Int
0))
                                         (Sort -> Sort -> Sort
mapSort Sort
intSort (Int -> Sort
FVar Int
0))
    mapToSetSort :: Sort
mapToSetSort = Int -> Sort -> Sort
FAbs Int
0        (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort -> Sort
mapSort (Int -> Sort
FVar Int
0) Sort
intSort) (Sort -> Sort
setSort (Int -> Sort
FVar Int
0))
    -- store :: forall i a. Map i a -> i -> a -> Map i a
    mapStoSort :: Sort
mapStoSort = Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort -> Sort
FAbs Int
1 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort -> Sort
mapSort (Int -> Sort
FVar Int
0) (Int -> Sort
FVar Int
1))
                                 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
0)
                                 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
1)
                                         (Sort -> Sort -> Sort
mapSort (Int -> Sort
FVar Int
0) (Int -> Sort
FVar Int
1))
    mapDefSort :: Sort
mapDefSort = Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort -> Sort
FAbs Int
1 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
1)
                                         (Sort -> Sort -> Sort
mapSort (Int -> Sort
FVar Int
0) (Int -> Sort
FVar Int
1))


interpBvUop :: Symbol -> (Symbol, TheorySymbol)
interpBvUop :: Symbol -> (Symbol, TheorySymbol)
interpBvUop Symbol
name = Symbol -> Sort -> (Symbol, TheorySymbol)
interpSym' Symbol
name Sort
bvUopSort
interpBvBop :: Symbol -> (Symbol, TheorySymbol)
interpBvBop :: Symbol -> (Symbol, TheorySymbol)
interpBvBop Symbol
name = Symbol -> Sort -> (Symbol, TheorySymbol)
interpSym' Symbol
name Sort
bvBopSort
interpBvCmp :: Symbol -> (Symbol, TheorySymbol)
interpBvCmp :: Symbol -> (Symbol, TheorySymbol)
interpBvCmp Symbol
name = Symbol -> Sort -> (Symbol, TheorySymbol)
interpSym' Symbol
name Sort
bvCmpSort
interpBvExt :: Symbol -> (Symbol, TheorySymbol)
interpBvExt :: Symbol -> (Symbol, TheorySymbol)
interpBvExt Symbol
name = Symbol -> Sort -> (Symbol, TheorySymbol)
interpSym' Symbol
name Sort
bvExtendSort
interpBvRot :: Symbol -> (Symbol, TheorySymbol)
interpBvRot :: Symbol -> (Symbol, TheorySymbol)
interpBvRot Symbol
name = Symbol -> Sort -> (Symbol, TheorySymbol)
interpSym' Symbol
name Sort
bvRotSort

interpSym' :: Symbol -> Sort -> (Symbol, TheorySymbol)
interpSym' :: Symbol -> Sort -> (Symbol, TheorySymbol)
interpSym' Symbol
name = Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
name (String -> Raw
Data.Text.pack (String -> Raw) -> String -> Raw
forall a b. (a -> b) -> a -> b
$ Symbol -> String
symbolString Symbol
name)

-- Indexed Identifier sort.
-- Together with 'app', this allows one to write indexed identifier
-- functions (smtlib2 specific functions). (e.g. ((_ sign_extend 1) bv))
--
-- The idea here is that 'app' is elaborated to the empty string,
-- and '_' does the typelit application as it does in smtlib2.
--
-- Then if we write, (app (_ sign_extend 1) bv), LF will elaborate
-- it as ( (_ sign_extend 1) bv). Fitting the smtlib2 format exactly!
--
-- One thing to note, is that any indexed identifier function (like
-- sign_extend) has to have no FAbs in it. Otherwise, they will be
-- elaborated like e.g. ( (_ (as sign_extend Int) 1) bv), which is wrong!
--
-- _ :: forall a b c. (a -> b -> c) -> a -> (b -> c)
iiSort :: Sort
iiSort :: Sort
iiSort = Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort -> Sort
FAbs Int
1 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort -> Sort
FAbs Int
2 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc
               (Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
0) (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
1) (Int -> Sort
FVar Int
2))
               (Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
0) (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
1) (Int -> Sort
FVar Int
2))

-- Simple application, used for indexed identifier function, check '_'.
--
-- app :: forall a b. (a -> b) -> a -> b
appSort :: Sort
appSort :: Sort
appSort = Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort -> Sort
FAbs Int
1 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc
                (Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
0) (Int -> Sort
FVar Int
1))
                (Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
0) (Int -> Sort
FVar Int
1))

-- Indexed identifier operation, purposely didn't place FAbs!
--
-- extend :: Int -> BitVec a -> BitVec b
bvExtendSort :: Sort
bvExtendSort :: Sort
bvExtendSort  = Sort -> Sort -> Sort
FFunc Sort
FInt (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
bitVecSort Int
1) (Int -> Sort
bitVecSort Int
2)

-- Indexed identifier operation, purposely didn't place FAbs!
--
-- rot :: Int -> BitVec a -> BitVec a
bvRotSort :: Sort
bvRotSort :: Sort
bvRotSort  = Sort -> Sort -> Sort
FFunc Sort
FInt (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
bitVecSort Int
0) (Int -> Sort
bitVecSort Int
0)

-- uOp :: forall a. BitVec a -> BitVec a
bvUopSort :: Sort
bvUopSort :: Sort
bvUopSort = Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
bitVecSort Int
0) (Int -> Sort
bitVecSort Int
0)

-- bOp :: forall a. BitVec a -> BitVec a -> BitVec a
bvBopSort :: Sort
bvBopSort :: Sort
bvBopSort = Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
bitVecSort Int
0) (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
bitVecSort Int
0) (Int -> Sort
bitVecSort Int
0)
-- bvBopSort = FAbs 0 $ FFunc (bitVecSort (FVar 0)) (FFunc (bitVecSort (FVar 0)) (bitVecSort (FVar 0)))

-- cmp :: forall a. BitVec a -> BitVec a -> Bool
bvCmpSort :: Sort
bvCmpSort :: Sort
bvCmpSort = Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
bitVecSort Int
0) (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
bitVecSort Int
0) Sort
boolSort

-- eq :: forall a. BitVec a -> BitVec a -> BitVec 1
bvEqSort :: Sort
bvEqSort :: Sort
bvEqSort = Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
bitVecSort Int
0) (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
bitVecSort Int
0) (Symbol -> Sort
sizedBitVecSort Symbol
"Size1")

-- concat :: forall a b c. BitVec a -> BitVec b -> BitVec c
bvConcatSort :: Sort
bvConcatSort :: Sort
bvConcatSort = Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort -> Sort
FAbs Int
1 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort -> Sort
FAbs Int
2 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$
                     Sort -> Sort -> Sort
FFunc (Int -> Sort
bitVecSort Int
0) (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
bitVecSort Int
1) (Int -> Sort
bitVecSort Int
2)

interpSym :: Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym :: Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
x Raw
n Sort
t = (Symbol
x, Symbol -> Raw -> Sort -> Sem -> TheorySymbol
Thy Symbol
x Raw
n Sort
t Sem
Theory)

maxLamArg :: Int
maxLamArg :: Int
maxLamArg = Int
7

axiomLiterals :: [(Symbol, Sort)] -> [Expr]
axiomLiterals :: [(Symbol, Sort)] -> [Expr]
axiomLiterals [(Symbol, Sort)]
lts = [Maybe Expr] -> [Expr]
forall a. [Maybe a] -> [a]
catMaybes [ Symbol -> Int -> Expr
forall {a} {a}. (Expression a, Expression a) => a -> a -> Expr
lenAxiom Symbol
l (Int -> Expr) -> Maybe Int -> Maybe Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Symbol -> Maybe Int
litLen Symbol
l | (Symbol
l, Sort
t) <- [(Symbol, Sort)]
lts, Sort -> Bool
isString Sort
t ]
  where
    lenAxiom :: a -> a -> Expr
lenAxiom a
l a
n  = Expr -> Expr -> Expr
EEq (Expr -> Expr -> Expr
EApp (Symbol -> Expr
forall a. Expression a => a -> Expr
expr (Symbol
forall a. IsString a => a
strLen :: Symbol)) (a -> Expr
forall a. Expression a => a -> Expr
expr a
l)) (a -> Expr
forall a. Expression a => a -> Expr
expr a
n Expr -> Sort -> Expr
`ECst` Sort
intSort)
    litLen :: Symbol -> Maybe Int
litLen        = (Symbol -> Int) -> Maybe Symbol -> Maybe Int
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Raw -> Int
Data.Text.length (Raw -> Int) -> (Symbol -> Raw) -> Symbol -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  Symbol -> Raw
symbolText) (Maybe Symbol -> Maybe Int)
-> (Symbol -> Maybe Symbol) -> Symbol -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Maybe Symbol
unLitSymbol

--------------------------------------------------------------------------------
-- | Constructors, Selectors and Tests from 'DataDecl'arations.
--------------------------------------------------------------------------------
dataDeclSymbols :: DataDecl -> [(Symbol, TheorySymbol)]
dataDeclSymbols :: DataDecl -> [(Symbol, TheorySymbol)]
dataDeclSymbols DataDecl
d = DataDecl -> [(Symbol, TheorySymbol)]
ctorSymbols DataDecl
d [(Symbol, TheorySymbol)]
-> [(Symbol, TheorySymbol)] -> [(Symbol, TheorySymbol)]
forall a. [a] -> [a] -> [a]
++ DataDecl -> [(Symbol, TheorySymbol)]
testSymbols DataDecl
d [(Symbol, TheorySymbol)]
-> [(Symbol, TheorySymbol)] -> [(Symbol, TheorySymbol)]
forall a. [a] -> [a] -> [a]
++ DataDecl -> [(Symbol, TheorySymbol)]
selectSymbols DataDecl
d

-- | 'selfSort d' returns the _self-sort_ of 'd' :: 'DataDecl'.
--   See [NOTE:DataDecl] for details.

selfSort :: DataDecl -> Sort
selfSort :: DataDecl -> Sort
selfSort (DDecl FTycon
c Int
n [DataCtor]
_) = FTycon -> [Sort] -> Sort
fAppTC FTycon
c (Int -> Sort
FVar (Int -> Sort) -> [Int] -> [Sort]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
0..(Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)])

-- | 'fldSort d t' returns the _real-sort_ of 'd' if 't' is the _self-sort_
--   and otherwise returns 't'. See [NOTE:DataDecl] for details.

fldSort :: DataDecl -> Sort -> Sort
fldSort :: DataDecl -> Sort -> Sort
fldSort DataDecl
d (FTC FTycon
c)
  | FTycon
c FTycon -> FTycon -> Bool
forall a. Eq a => a -> a -> Bool
== DataDecl -> FTycon
ddTyCon DataDecl
d = DataDecl -> Sort
selfSort DataDecl
d
fldSort DataDecl
_ Sort
s        = Sort
s

--------------------------------------------------------------------------------
ctorSymbols :: DataDecl -> [(Symbol, TheorySymbol)]
--------------------------------------------------------------------------------
ctorSymbols :: DataDecl -> [(Symbol, TheorySymbol)]
ctorSymbols DataDecl
d = DataDecl -> DataCtor -> (Symbol, TheorySymbol)
ctorSort DataDecl
d (DataCtor -> (Symbol, TheorySymbol))
-> [DataCtor] -> [(Symbol, TheorySymbol)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DataDecl -> [DataCtor]
ddCtors DataDecl
d

ctorSort :: DataDecl -> DataCtor -> (Symbol, TheorySymbol)
ctorSort :: DataDecl -> DataCtor -> (Symbol, TheorySymbol)
ctorSort DataDecl
d DataCtor
ctor = (Symbol
x, Symbol -> Raw -> Sort -> Sem -> TheorySymbol
Thy Symbol
x (Symbol -> Raw
symbolRaw Symbol
x) Sort
t Sem
Ctor)
  where
    x :: Symbol
x           = DataCtor -> Symbol
forall a. Symbolic a => a -> Symbol
symbol DataCtor
ctor
    t :: Sort
t           = Int -> [Sort] -> Sort
mkFFunc Int
n ([Sort]
ts [Sort] -> [Sort] -> [Sort]
forall a. [a] -> [a] -> [a]
++ [DataDecl -> Sort
selfSort DataDecl
d])
    n :: Int
n           = DataDecl -> Int
ddVars DataDecl
d
    ts :: [Sort]
ts          = DataDecl -> Sort -> Sort
fldSort DataDecl
d (Sort -> Sort) -> (DataField -> Sort) -> DataField -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataField -> Sort
dfSort (DataField -> Sort) -> [DataField] -> [Sort]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DataCtor -> [DataField]
dcFields DataCtor
ctor

--------------------------------------------------------------------------------
testSymbols :: DataDecl -> [(Symbol, TheorySymbol)]
--------------------------------------------------------------------------------
testSymbols :: DataDecl -> [(Symbol, TheorySymbol)]
testSymbols DataDecl
d = Sort -> Symbol -> (Symbol, TheorySymbol)
testTheory Sort
t (Symbol -> (Symbol, TheorySymbol))
-> (DataCtor -> Symbol) -> DataCtor -> (Symbol, TheorySymbol)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCtor -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (DataCtor -> (Symbol, TheorySymbol))
-> [DataCtor] -> [(Symbol, TheorySymbol)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DataDecl -> [DataCtor]
ddCtors DataDecl
d
  where
    t :: Sort
t         = Int -> [Sort] -> Sort
mkFFunc (DataDecl -> Int
ddVars DataDecl
d) [DataDecl -> Sort
selfSort DataDecl
d, Sort
boolSort]

testTheory :: Sort -> Symbol -> (Symbol, TheorySymbol)
testTheory :: Sort -> Symbol -> (Symbol, TheorySymbol)
testTheory Sort
t Symbol
x = (Symbol
sx, Symbol -> Raw -> Sort -> Sem -> TheorySymbol
Thy Symbol
sx Raw
raw Sort
t Sem
Test)
  where
    sx :: Symbol
sx         = Symbol -> Symbol
testSymbol Symbol
x
    raw :: Raw
raw        = Raw
"is-" Raw -> Raw -> Raw
forall a. Semigroup a => a -> a -> a
<> Symbol -> Raw
symbolRaw Symbol
x

symbolRaw :: Symbol -> Data.Text.Text
symbolRaw :: Symbol -> Raw
symbolRaw = Symbol -> Raw
symbolSafeText

--------------------------------------------------------------------------------
selectSymbols :: DataDecl -> [(Symbol, TheorySymbol)]
--------------------------------------------------------------------------------
selectSymbols :: DataDecl -> [(Symbol, TheorySymbol)]
selectSymbols DataDecl
d = (Symbol, Sort) -> (Symbol, TheorySymbol)
theorify ((Symbol, Sort) -> (Symbol, TheorySymbol))
-> [(Symbol, Sort)] -> [(Symbol, TheorySymbol)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (DataCtor -> [(Symbol, Sort)]) -> [DataCtor] -> [(Symbol, Sort)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (DataDecl -> DataCtor -> [(Symbol, Sort)]
ctorSelectors DataDecl
d) (DataDecl -> [DataCtor]
ddCtors DataDecl
d)

-- | 'theorify' converts the 'Sort' into a full 'TheorySymbol'
theorify :: (Symbol, Sort) -> (Symbol, TheorySymbol)
theorify :: (Symbol, Sort) -> (Symbol, TheorySymbol)
theorify (Symbol
x, Sort
t) = (Symbol
x, Symbol -> Raw -> Sort -> Sem -> TheorySymbol
Thy Symbol
x (Symbol -> Raw
symbolRaw Symbol
x) Sort
t Sem
Field)

ctorSelectors :: DataDecl -> DataCtor -> [(Symbol, Sort)]
ctorSelectors :: DataDecl -> DataCtor -> [(Symbol, Sort)]
ctorSelectors DataDecl
d DataCtor
ctor = DataDecl -> DataField -> (Symbol, Sort)
fieldSelector DataDecl
d (DataField -> (Symbol, Sort)) -> [DataField] -> [(Symbol, Sort)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DataCtor -> [DataField]
dcFields DataCtor
ctor

fieldSelector :: DataDecl -> DataField -> (Symbol, Sort)
fieldSelector :: DataDecl -> DataField -> (Symbol, Sort)
fieldSelector DataDecl
d DataField
f = (DataField -> Symbol
forall a. Symbolic a => a -> Symbol
symbol DataField
f, Int -> [Sort] -> Sort
mkFFunc Int
n [DataDecl -> Sort
selfSort DataDecl
d, Sort
ft])
  where
    ft :: Sort
ft            = DataDecl -> Sort -> Sort
fldSort DataDecl
d (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ DataField -> Sort
dfSort DataField
f
    n :: Int
n             = DataDecl -> Int
ddVars  DataDecl
d

{- | [NOTE:DataDecl]  This note explains the set of symbols generated
     for the below data-declaration:

  data Vec 1 = [
    | nil  { }
    | cons { vHead : @(0), vTail : Vec}
  ]

We call 'Vec' the _self-sort_ of the data-type, and we want to ensure that
in all constructors, tests and selectors, the _self-sort_ is replaced with
the actual sort, namely, 'Vec @(0)'.

Constructors  // ctor : (fld-sorts) => me

        nil   : func(1, [Vec @(0)])
        cons  : func(1, [@(0); Vec @(0); Vec @(0)])

Tests         // is#ctor : (me) => bool

      is#nil  : func(1, [Vec @(0); bool])
      is#cons : func(1, [Vec @(0); bool])

Selectors     // fld : (me) => fld-sort

      vHead   : func(1, [Vec @(0); @(0)])
      vTail   : func(1, [Vec @(0); Vec @(0)])

-}