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

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

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

import           Prelude hiding (map)
#if !MIN_VERSION_base(4,14,0)
import           Data.Semigroup            (Semigroup (..))
#endif

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 qualified Data.Text.Lazy           as T
import qualified Data.Text.Lazy.Builder   as Builder
import           Data.Text.Format
import qualified Data.Text
import           Data.String                 (IsString(..))


{- | [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 ------------------------------------------------------------
--------------------------------------------------------------------------------

-- "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"

emp, add, cup, cap, mem, dif, sub, com, sel, sto, mcup, mdef :: Raw
emp :: Raw
emp   = Raw
"smt_set_emp"
add :: Raw
add   = Raw
"smt_set_add"
cup :: Raw
cup   = Raw
"smt_set_cup"
cap :: Raw
cap   = Raw
"smt_set_cap"
mem :: Raw
mem   = Raw
"smt_set_mem"
dif :: Raw
dif   = Raw
"smt_set_dif"
sub :: Raw
sub   = Raw
"smt_set_sub"
com :: Raw
com   = Raw
"smt_set_com"
sel :: Raw
sel   = Raw
"smt_map_sel"
sto :: Raw
sto   = Raw
"smt_map_sto"
mcup :: Raw
mcup  = Raw
"smt_map_cup"
mdef :: Raw
mdef  = Raw
"smt_map_def"


setEmpty, setEmp, setCap, setSub, setAdd, setMem, setCom, setCup, setDif, setSng :: Symbol
setEmpty :: Symbol
setEmpty = Symbol
"Set_empty"
setEmp :: Symbol
setEmp   = Symbol
"Set_emp"
setCap :: Symbol
setCap   = Symbol
"Set_cap"
setSub :: Symbol
setSub   = Symbol
"Set_sub"
setAdd :: Symbol
setAdd   = Symbol
"Set_add"
setMem :: Symbol
setMem   = Symbol
"Set_mem"
setCom :: Symbol
setCom   = Symbol
"Set_com"
setCup :: Symbol
setCup   = Symbol
"Set_cup"
setDif :: Symbol
setDif   = Symbol
"Set_dif"
setSng :: Symbol
setSng   = Symbol
"Set_sng"

mapSel, mapSto, mapCup, mapDef :: Symbol
mapSel :: Symbol
mapSel   = Symbol
"Map_select"
mapSto :: Symbol
mapSto   = Symbol
"Map_store"
mapCup :: Symbol
mapCup   = Symbol
"Map_union"
mapDef :: Symbol
mapDef   = Symbol
"Map_default"

strLen, strSubstr, strConcat :: (IsString a) => a -- Symbol
strLen :: a
strLen    = a
"strLen"
strSubstr :: a
strSubstr = a
"subString"
strConcat :: 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

z3Preamble :: Config -> [T.Text]
z3Preamble :: Config -> [Raw]
z3Preamble Config
u
  = Config -> [Raw]
stringPreamble Config
u [Raw] -> [Raw] -> [Raw]
forall a. [a] -> [a] -> [a]
++
    [ Format -> Only Raw -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(define-sort {} () Int)"
        (Raw -> Only Raw
forall a. a -> Only a
Only Raw
elt)
    , Format -> (Raw, Raw) -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(define-sort {} () (Array {} Bool))"
        (Raw
set, Raw
elt)
    , Format -> (Raw, Raw, Raw) -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(define-fun {} () {} ((as const {}) false))"
        (Raw
emp, Raw
set, Raw
set)
    , Format -> (Raw, Raw, Raw) -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(define-fun {} ((x {}) (s {})) Bool (select s x))"
        (Raw
mem, Raw
elt, Raw
set)
    , Format -> (Raw, Raw, Raw, Raw) -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(define-fun {} ((s {}) (x {})) {} (store s x true))"
        (Raw
add, Raw
set, Raw
elt, Raw
set)
    , Format -> (Raw, Raw, Raw, Raw) -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(define-fun {} ((s1 {}) (s2 {})) {} ((_ map or) s1 s2))"
        (Raw
cup, Raw
set, Raw
set, Raw
set)
    , Format -> (Raw, Raw, Raw, Raw) -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(define-fun {} ((s1 {}) (s2 {})) {} ((_ map and) s1 s2))"
        (Raw
cap, Raw
set, Raw
set, Raw
set)
    , Format -> (Raw, Raw, Raw) -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(define-fun {} ((s {})) {} ((_ map not) s))"
        (Raw
com, Raw
set, Raw
set)
    , Format -> (Raw, Raw, Raw, Raw, Raw, Raw) -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(define-fun {} ((s1 {}) (s2 {})) {} ({} s1 ({} s2)))"
        (Raw
dif, Raw
set, Raw
set, Raw
set, Raw
cap, Raw
com)
    , Format -> (Raw, Raw, Raw, Raw, Raw) -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(define-fun {} ((s1 {}) (s2 {})) Bool (= {} ({} s1 s2)))"
        (Raw
sub, Raw
set, Raw
set, Raw
emp, Raw
dif)
    , Format -> (Raw, Raw, Raw) -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(define-sort {} () (Array {} {}))"
        (Raw
map, Raw
elt, Raw
elt)
    , Format -> (Raw, Raw, Raw, Raw) -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(define-fun {} ((m {}) (k {})) {} (select m k))"
        (Raw
sel, Raw
map, Raw
elt, Raw
elt)
    , Format -> (Raw, Raw, Raw, Raw, Raw) -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(define-fun {} ((m {}) (k {}) (v {})) {} (store m k v))"
        (Raw
sto, Raw
map, Raw
elt, Raw
elt, Raw
map)
    , Format -> (Raw, Raw, Raw, Raw, Raw, Raw, Raw) -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(define-fun {} ((m1 {}) (m2 {})) {} ((_ map (+ ({} {}) {})) m1 m2))"
        (Raw
mcup, Raw
map, Raw
map, Raw
map, Raw
elt, Raw
elt, Raw
elt)
    , Format -> (Raw, Raw, Raw, Raw) -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(define-fun {} ((v {})) {} ((as const ({})) v))"
        (Raw
mdef, Raw
elt, Raw
map, Raw
map)
    , Format -> Only Raw -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(define-fun {} ((b Bool)) Int (ite b 1 0))"
        (Raw -> Only Raw
forall a. a -> Only a
Only (Raw
forall a. IsString a => a
boolToIntName :: T.Text))
    , Config -> Text -> Raw -> Raw
uifDef Config
u (Symbol -> Text
symbolText Symbol
mulFuncName) (Raw
"*"   :: T.Text)
    , Config -> Text -> Raw -> Raw
uifDef Config
u (Symbol -> Text
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 -> T.Text -> T.Text
uifDef :: Config -> Text -> Raw -> Raw
uifDef Config
cfg Text
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
  = Format -> Only Text -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(declare-fun {} (Int Int) Int)" (Text -> Only Text
forall a. a -> Only a
Only Text
f)
  | Bool
otherwise
  = Format -> (Text, Raw) -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(define-fun {} ((x Int) (y Int)) Int ({} x y))" (Text
f, Raw
op)

cvc4Preamble :: Config -> [T.Text]
cvc4Preamble :: Config -> [Raw]
cvc4Preamble Config
_ --TODO use uif flag u (see z3Preamble)
  = [        Raw
"(set-logic ALL_SUPPORTED)"
    , Format -> Only Raw -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(define-sort {} () Int)"       (Raw -> Only Raw
forall a. a -> Only a
Only Raw
elt)
    , Format -> Only Raw -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(define-sort {} () Int)"       (Raw -> Only Raw
forall a. a -> Only a
Only Raw
set)
    , Format -> Only Raw -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(define-sort {} () Int)"       (Raw -> Only Raw
forall a. a -> Only a
Only Raw
string)
    , Format -> (Raw, Raw) -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(declare-fun {} () {})"        (Raw
emp, Raw
set)
    , Format -> (Raw, Raw, Raw, Raw) -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(declare-fun {} ({} {}) {})"   (Raw
add, Raw
set, Raw
elt, Raw
set)
    , Format -> (Raw, Raw, Raw, Raw) -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(declare-fun {} ({} {}) {})"   (Raw
cup, Raw
set, Raw
set, Raw
set)
    , Format -> (Raw, Raw, Raw, Raw) -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(declare-fun {} ({} {}) {})"   (Raw
cap, Raw
set, Raw
set, Raw
set)
    , Format -> (Raw, Raw, Raw, Raw) -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(declare-fun {} ({} {}) {})"   (Raw
dif, Raw
set, Raw
set, Raw
set)
    , Format -> (Raw, Raw, Raw) -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(declare-fun {} ({} {}) Bool)" (Raw
sub, Raw
set, Raw
set)
    , Format -> (Raw, Raw, Raw) -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(declare-fun {} ({} {}) Bool)" (Raw
mem, Raw
elt, Raw
set)
    , Format -> (Raw, Raw, Raw) -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(define-sort {} () (Array {} {}))"
        (Raw
map, Raw
elt, Raw
elt)
    , Format -> (Raw, Raw, Raw, Raw) -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(define-fun {} ((m {}) (k {})) {} (select m k))"
        (Raw
sel, Raw
map, Raw
elt, Raw
elt)
    , Format -> (Raw, Raw, Raw, Raw, Raw) -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(define-fun {} ((m {}) (k {}) (v {})) {} (store m k v))"
        (Raw
sto, Raw
map, Raw
elt, Raw
elt, Raw
map)
    , Format -> Only Raw -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(define-fun {} ((b Bool)) Int (ite b 1 0))"
        (Raw -> Only Raw
forall a. a -> Only a
Only (Raw
forall a. IsString a => a
boolToIntName :: Raw))
    ]

smtlibPreamble :: Config -> [T.Text]
smtlibPreamble :: Config -> [Raw]
smtlibPreamble Config
_ --TODO use uif flag u (see z3Preamble)
  = [       --  "(set-logic QF_AUFRIA)",
      Format -> Only Raw -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(define-sort {} () Int)"       (Raw -> Only Raw
forall a. a -> Only a
Only Raw
elt)
    , Format -> Only Raw -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(define-sort {} () Int)"       (Raw -> Only Raw
forall a. a -> Only a
Only Raw
set)
    , Format -> (Raw, Raw) -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(declare-fun {} () {})"        (Raw
emp, Raw
set)
    , Format -> (Raw, Raw, Raw, Raw) -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(declare-fun {} ({} {}) {})"   (Raw
add, Raw
set, Raw
elt, Raw
set)
    , Format -> (Raw, Raw, Raw, Raw) -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(declare-fun {} ({} {}) {})"   (Raw
cup, Raw
set, Raw
set, Raw
set)
    , Format -> (Raw, Raw, Raw, Raw) -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(declare-fun {} ({} {}) {})"   (Raw
cap, Raw
set, Raw
set, Raw
set)
    , Format -> (Raw, Raw, Raw, Raw) -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(declare-fun {} ({} {}) {})"   (Raw
dif, Raw
set, Raw
set, Raw
set)
    , Format -> (Raw, Raw, Raw) -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(declare-fun {} ({} {}) Bool)" (Raw
sub, Raw
set, Raw
set)
    , Format -> (Raw, Raw, Raw) -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(declare-fun {} ({} {}) Bool)" (Raw
mem, Raw
elt, Raw
set)
    , Format -> Only Raw -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(define-sort {} () Int)"       (Raw -> Only Raw
forall a. a -> Only a
Only Raw
map)
    , Format -> (Raw, Raw, Raw, Raw) -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(declare-fun {} ({} {}) {})"    (Raw
sel, Raw
map, Raw
elt, Raw
elt)
    , Format -> (Raw, Raw, Raw, Raw, Raw) -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(declare-fun {} ({} {} {}) {})" (Raw
sto, Raw
map, Raw
elt, Raw
elt, Raw
map)
    , Format -> (Raw, Raw, Raw, Raw, Raw) -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(declare-fun {} ({} {} {}) {})" (Raw
sto, Raw
map, Raw
elt, Raw
elt, Raw
map)
    , Format -> Only Raw -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(define-fun {} ((b Bool)) Int (ite b 1 0))" (Raw -> Only Raw
forall a. a -> Only a
Only (Raw
forall a. IsString a => a
boolToIntName :: Raw))
    ]


stringPreamble :: Config -> [T.Text]
stringPreamble :: Config -> [Raw]
stringPreamble Config
cfg | Config -> Bool
stringTheory Config
cfg
  = [
      Format -> Only Raw -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(define-sort {} () String)" (Raw -> Only Raw
forall a. a -> Only a
Only Raw
string)
    , Format -> (Raw, Raw, Raw) -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(define-fun {} ((s {})) Int ({} s))"
        (Raw
forall a. IsString a => a
strLen :: Raw, Raw
string, Raw
z3strlen)
    , Format -> (Raw, Raw, Raw, Raw) -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(define-fun {} ((s {}) (i Int) (j Int)) {} ({} s i j))"
        (Raw
forall a. IsString a => a
strSubstr :: Raw, Raw
string, Raw
string, Raw
z3strsubstr)
    , Format -> (Raw, Raw, Raw, Raw, Raw) -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(define-fun {} ((x {}) (y {})) {} ({} x y))"
        (Raw
forall a. IsString a => a
strConcat :: Raw, Raw
string, Raw
string, Raw
string, Raw
z3strconcat)
    ]
stringPreamble Config
_
  = [
      Format -> Only Raw -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(define-sort {} () Int)" (Raw -> Only Raw
forall a. a -> Only a
Only Raw
string)
    , Format -> (Raw, Raw) -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(declare-fun {} ({}) Int)"
        (Raw
forall a. IsString a => a
strLen :: Raw, Raw
string)
    , Format -> (Raw, Raw, Raw) -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(declare-fun {} ({} Int Int) {})"
        (Raw
forall a. IsString a => a
strSubstr :: Raw, Raw
string, Raw
string)
    , Format -> (Raw, Raw, Raw, Raw) -> Raw
forall ps. Params ps => Format -> ps -> Raw
format Format
"(declare-fun {} ({} {}) {})"
        (Raw
forall a. IsString a => a
strConcat :: Raw, Raw
string, Raw
string, Raw
string)
    ]



--------------------------------------------------------------------------------
-- | Exported API --------------------------------------------------------------
--------------------------------------------------------------------------------
smt2Symbol :: SymEnv -> Symbol -> Maybe Builder.Builder
smt2Symbol :: SymEnv -> Symbol -> Maybe Builder
smt2Symbol SymEnv
env Symbol
x = Raw -> Builder
Builder.fromLazyText (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.Builder
smt2SmtSort :: SmtSort -> Builder
smt2SmtSort SmtSort
SInt         = Builder
"Int"
smt2SmtSort SmtSort
SReal        = Builder
"Real"
smt2SmtSort SmtSort
SBool        = Builder
"Bool"
smt2SmtSort SmtSort
SString      = Format -> Only Raw -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"{}" (Raw -> Only Raw
forall a. a -> Only a
Only Raw
string)
smt2SmtSort SmtSort
SSet         = Format -> Only Raw -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"{}" (Raw -> Only Raw
forall a. a -> Only a
Only Raw
set)
smt2SmtSort SmtSort
SMap         = Format -> Only Raw -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"{}" (Raw -> Only Raw
forall a. a -> Only a
Only Raw
map)
smt2SmtSort (SBitVec Int
n)  = Format -> Only Int -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"(_ BitVec {})" (Int -> Only Int
forall a. a -> Only a
Only Int
n)
smt2SmtSort (SVar Int
n)     = Format -> Only Int -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"T{}" (Int -> Only Int
forall a. a -> Only a
Only Int
n)
smt2SmtSort (SData FTycon
c []) = FTycon -> Builder
forall a. Symbolic a => a -> Builder
symbolBuilder FTycon
c
smt2SmtSort (SData FTycon
c [SmtSort]
ts) = Format -> (Builder, Builder) -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"({} {})" (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.Builder
smt2SmtSorts :: [SmtSort] -> Builder
smt2SmtSorts = [Builder] -> Builder
buildMany ([Builder] -> Builder)
-> ([SmtSort] -> [Builder]) -> [SmtSort] -> Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SmtSort -> Builder) -> [SmtSort] -> [Builder]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SmtSort -> Builder
smt2SmtSort

type VarAs = SymEnv -> Symbol -> Sort -> Builder.Builder
--------------------------------------------------------------------------------
smt2App :: VarAs -> SymEnv -> Expr -> [Builder.Builder] -> Maybe Builder.Builder
--------------------------------------------------------------------------------
smt2App :: VarAs -> SymEnv -> Expr -> [Builder] -> Maybe Builder
smt2App VarAs
_ SymEnv
_ (ECst (EVar Symbol
f) Sort
_) [Builder
d]
  | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
setEmpty = Builder -> Maybe Builder
forall a. a -> Maybe a
Just (Builder -> Maybe Builder) -> Builder -> Maybe Builder
forall a b. (a -> b) -> a -> b
$ Format -> Only Raw -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"{}"             (Raw -> Only Raw
forall a. a -> Only a
Only Raw
emp)
  | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
setEmp   = Builder -> Maybe Builder
forall a. a -> Maybe a
Just (Builder -> Maybe Builder) -> Builder -> Maybe Builder
forall a b. (a -> b) -> a -> b
$ Format -> (Raw, Builder) -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"(= {} {})"      (Raw
emp, Builder
d)
  | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
setSng   = Builder -> Maybe Builder
forall a. a -> Maybe a
Just (Builder -> Maybe Builder) -> Builder -> Maybe Builder
forall a b. (a -> b) -> a -> b
$ Format -> (Raw, Raw, Builder) -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"({} {} {})"     (Raw
add, Raw
emp, Builder
d)

smt2App VarAs
k SymEnv
env Expr
f (Builder
d:[Builder]
ds)
  | Just Builder
fb <- VarAs -> SymEnv -> Expr -> Maybe Builder
smt2AppArg VarAs
k SymEnv
env Expr
f
  = Builder -> Maybe Builder
forall a. a -> Maybe a
Just (Builder -> Maybe Builder) -> Builder -> Maybe Builder
forall a b. (a -> b) -> a -> b
$ Format -> (Builder, Builder) -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"({} {})" (Builder
fb, Builder
d 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]
ds])

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

smt2AppArg :: VarAs -> SymEnv -> Expr -> Maybe Builder.Builder
smt2AppArg :: VarAs -> SymEnv -> Expr -> Maybe Builder
smt2AppArg VarAs
k SymEnv
env (ECst (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 (Format -> Only Raw -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"{}" (Raw -> Only Raw
forall a. a -> Only a
Only (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. [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  (EVar Symbol
f)
  | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
setEmpty = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
1
  | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
setEmp   = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
1
  | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
setSng   = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
1
  | Bool
otherwise     = 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 (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 (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 -> [T.Text]
preamble :: Config -> SMTSolver -> [Raw]
preamble Config
u SMTSolver
Z3   = Config -> [Raw]
z3Preamble Config
u
preamble Config
u SMTSolver
Cvc4 = Config -> [Raw]
cvc4Preamble Config
u
preamble Config
u SMTSolver
_    = Config -> [Raw]
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 =
  [ Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
setEmp   Raw
emp  (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
setEmpty Raw
emp  (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
setAdd   Raw
add   Sort
setAddSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
setCup   Raw
cup   Sort
setBopSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
setCap   Raw
cap   Sort
setBopSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
setMem   Raw
mem   Sort
setMemSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
setDif   Raw
dif   Sort
setBopSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
setSub   Raw
sub   Sort
setCmpSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
setCom   Raw
com   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
mapDef   Raw
mdef  Sort
mapDefSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
bvOrName Raw
"bvor"   Sort
bvBopSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
bvAndName Raw
"bvand" Sort
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)
  ]
  where
    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
    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)
    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)
    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))

    bvBopSort :: Sort
bvBopSort  = Sort -> Sort -> Sort
FFunc Sort
bitVecSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
bitVecSort Sort
bitVecSort


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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Text -> Int
Data.Text.length (Text -> Int) -> (Symbol -> Text) -> Symbol -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  Symbol -> Text
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 -> T.Text
symbolRaw :: Symbol -> Raw
symbolRaw = Text -> Raw
T.fromStrict (Text -> Raw) -> (Symbol -> Text) -> Symbol -> Raw
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Text
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)])

-}