{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ViewPatterns #-}

module Language.Hasmtlib.Type.Expr
 ( SMTSort(..)
 , SMTVar(..), varId
 , HaskellType
 , Value(..), unwrapValue, wrapValue
 , SSMTSort(..), KnownSMTSort(..), sortSing', SomeSMTSort(..), SomeKnownSMTSort, AllC
 , Expr
 , equal, distinct
 , bvShL, bvLShR, bvConcat, bvRotL, bvRotR
 , for_all , exists
 , select, store
 )
where

import Language.Hasmtlib.Internal.Expr
import Language.Hasmtlib.Internal.Expr.Num ()
import Language.Hasmtlib.Boolean
import Data.Proxy
import Data.List (genericLength)
import Data.Foldable (toList)
import qualified Data.Vector.Sized as V
import GHC.TypeNats

-- | Test multiple expressions on equality within in the 'SMT'-Problem.
equal :: (Eq (HaskellType t), KnownSMTSort t, Foldable f) => f (Expr t) -> Expr BoolSort
equal :: forall (t :: SMTSort) (f :: * -> *).
(Eq (HaskellType t), KnownSMTSort t, Foldable f) =>
f (Expr t) -> Expr 'BoolSort
equal (f (Expr t) -> [Expr t]
forall a. f a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList -> (Expr t
a:Expr t
b:[Expr t]
xs)) = case Natural -> SomeNat
someNatVal ([Expr t] -> Natural
forall i a. Num i => [a] -> i
genericLength [Expr t]
xs) of
  SomeNat Proxy n
n -> case Proxy n -> [Expr t] -> Maybe (Vector n (Expr t))
forall (n :: Natural) a (p :: Natural -> *).
KnownNat n =>
p n -> [a] -> Maybe (Vector n a)
V.fromListN' Proxy n
n [Expr t]
xs of
    Maybe (Vector n (Expr t))
Nothing  -> Vector (0 + 2) (Expr t) -> Expr 'BoolSort
forall (t1 :: SMTSort) (n :: Natural).
(Eq (HaskellType t1), KnownSMTSort t1, KnownNat n) =>
Vector (n + 2) (Expr t1) -> Expr 'BoolSort
EQU (Vector (0 + 2) (Expr t) -> Expr 'BoolSort)
-> Vector (0 + 2) (Expr t) -> Expr 'BoolSort
forall a b. (a -> b) -> a -> b
$ (Expr t, Expr t) -> Vector (0 + 2) (Expr t)
forall input (length :: Natural) ty.
(IndexedListLiterals input length ty, KnownNat length) =>
input -> Vector length ty
V.fromTuple (Expr t
a,Expr t
b)
    Just Vector n (Expr t)
xs' -> Vector (n + 2) (Expr t) -> Expr 'BoolSort
forall (t1 :: SMTSort) (n :: Natural).
(Eq (HaskellType t1), KnownSMTSort t1, KnownNat n) =>
Vector (n + 2) (Expr t1) -> Expr 'BoolSort
EQU (Vector (n + 2) (Expr t) -> Expr 'BoolSort)
-> Vector (n + 2) (Expr t) -> Expr 'BoolSort
forall a b. (a -> b) -> a -> b
$ Vector n (Expr t)
xs' Vector n (Expr t) -> Vector 2 (Expr t) -> Vector (n + 2) (Expr t)
forall (n :: Natural) (m :: Natural) a.
Vector n a -> Vector m a -> Vector (n + m) a
V.++ (Expr t, Expr t) -> Vector 2 (Expr t)
forall input (length :: Natural) ty.
(IndexedListLiterals input length ty, KnownNat length) =>
input -> Vector length ty
V.fromTuple (Expr t
a,Expr t
b)
equal (f (Expr t) -> [Expr t]
forall a. f a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList -> [Expr t]
_)        = Expr 'BoolSort
forall b. Boolean b => b
true

-- | Test multiple expressions on distinctness within in the 'SMT'-Problem.
distinct :: (Eq (HaskellType t), KnownSMTSort t, Foldable f) => f (Expr t) -> Expr BoolSort
distinct :: forall (t :: SMTSort) (f :: * -> *).
(Eq (HaskellType t), KnownSMTSort t, Foldable f) =>
f (Expr t) -> Expr 'BoolSort
distinct (f (Expr t) -> [Expr t]
forall a. f a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList -> (Expr t
a:Expr t
b:[Expr t]
xs)) = case Natural -> SomeNat
someNatVal ([Expr t] -> Natural
forall i a. Num i => [a] -> i
genericLength [Expr t]
xs) of
  SomeNat Proxy n
n -> case Proxy n -> [Expr t] -> Maybe (Vector n (Expr t))
forall (n :: Natural) a (p :: Natural -> *).
KnownNat n =>
p n -> [a] -> Maybe (Vector n a)
V.fromListN' Proxy n
n [Expr t]
xs of
    Maybe (Vector n (Expr t))
Nothing  -> Vector (0 + 2) (Expr t) -> Expr 'BoolSort
forall (t1 :: SMTSort) (n :: Natural).
(Eq (HaskellType t1), KnownSMTSort t1, KnownNat n) =>
Vector (n + 2) (Expr t1) -> Expr 'BoolSort
Distinct (Vector (0 + 2) (Expr t) -> Expr 'BoolSort)
-> Vector (0 + 2) (Expr t) -> Expr 'BoolSort
forall a b. (a -> b) -> a -> b
$ (Expr t, Expr t) -> Vector (0 + 2) (Expr t)
forall input (length :: Natural) ty.
(IndexedListLiterals input length ty, KnownNat length) =>
input -> Vector length ty
V.fromTuple (Expr t
a,Expr t
b)
    Just Vector n (Expr t)
xs' -> Vector (n + 2) (Expr t) -> Expr 'BoolSort
forall (t1 :: SMTSort) (n :: Natural).
(Eq (HaskellType t1), KnownSMTSort t1, KnownNat n) =>
Vector (n + 2) (Expr t1) -> Expr 'BoolSort
Distinct (Vector (n + 2) (Expr t) -> Expr 'BoolSort)
-> Vector (n + 2) (Expr t) -> Expr 'BoolSort
forall a b. (a -> b) -> a -> b
$ Vector n (Expr t)
xs' Vector n (Expr t) -> Vector 2 (Expr t) -> Vector (n + 2) (Expr t)
forall (n :: Natural) (m :: Natural) a.
Vector n a -> Vector m a -> Vector (n + m) a
V.++ (Expr t, Expr t) -> Vector 2 (Expr t)
forall input (length :: Natural) ty.
(IndexedListLiterals input length ty, KnownNat length) =>
input -> Vector length ty
V.fromTuple (Expr t
a,Expr t
b)
distinct (f (Expr t) -> [Expr t]
forall a. f a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList -> [Expr t]
_)        = Expr 'BoolSort
forall b. Boolean b => b
true

-- | A universal quantification for any specific 'SMTSort'.
--   If the type cannot be inferred, apply a type-annotation.
--   Nested quantifiers are also supported.
--
--   Usage:
--
--   @
--   assert $
--      for_all @IntSort $ \x ->
--         x + 0 === x && 0 + x === x
--   @
--
--   The lambdas 'x' is all-quantified here.
--   It will only be scoped for the lambdas body.
for_all :: forall t. KnownSMTSort t => (Expr t -> Expr BoolSort) -> Expr BoolSort
for_all :: forall (t :: SMTSort).
KnownSMTSort t =>
(Expr t -> Expr 'BoolSort) -> Expr 'BoolSort
for_all = Maybe (SMTVar t) -> (Expr t -> Expr 'BoolSort) -> Expr 'BoolSort
forall (t1 :: SMTSort).
KnownSMTSort t1 =>
Maybe (SMTVar t1) -> (Expr t1 -> Expr 'BoolSort) -> Expr 'BoolSort
ForAll Maybe (SMTVar t)
forall a. Maybe a
Nothing

-- | An existential quantification for any specific 'SMTSort'
--   If the type cannot be inferred, apply a type-annotation.
--   Nested quantifiers are also supported.
--
--   Usage:
--
--   @
--   assert $
--      for_all @(BvSort 8) $ \x ->
--          exists $ \y ->
--            x - y === 0
--   @
--
--   The lambdas 'y' is existentially quantified here.
--   It will only be scoped for the lambdas body.
exists :: forall t. KnownSMTSort t => (Expr t -> Expr BoolSort) -> Expr BoolSort
exists :: forall (t :: SMTSort).
KnownSMTSort t =>
(Expr t -> Expr 'BoolSort) -> Expr 'BoolSort
exists = Maybe (SMTVar t) -> (Expr t -> Expr 'BoolSort) -> Expr 'BoolSort
forall (t1 :: SMTSort).
KnownSMTSort t1 =>
Maybe (SMTVar t1) -> (Expr t1 -> Expr 'BoolSort) -> Expr 'BoolSort
Exists Maybe (SMTVar t)
forall a. Maybe a
Nothing

-- | Select a value from an array.
select :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Expr (ArraySort k v) -> Expr k -> Expr v
select :: forall (k :: SMTSort) (v :: SMTSort).
(KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) =>
Expr ('ArraySort k v) -> Expr k -> Expr v
select = Expr ('ArraySort k v) -> Expr k -> Expr v
forall (k :: SMTSort) (v :: SMTSort).
(KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) =>
Expr ('ArraySort k v) -> Expr k -> Expr v
ArrSelect

-- | Store a value in an array.
store :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Expr (ArraySort k v) -> Expr k -> Expr v -> Expr (ArraySort k v)
store :: forall (k :: SMTSort) (v :: SMTSort).
(KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) =>
Expr ('ArraySort k v) -> Expr k -> Expr v -> Expr ('ArraySort k v)
store = Expr ('ArraySort k v) -> Expr k -> Expr v -> Expr ('ArraySort k v)
forall (k :: SMTSort) (v :: SMTSort).
(KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) =>
Expr ('ArraySort k v) -> Expr k -> Expr v -> Expr ('ArraySort k v)
ArrStore

-- | Bitvector shift left
bvShL    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
bvShL :: forall (n :: Natural).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
bvShL    = Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Natural).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvShL
{-# INLINE bvShL #-}

-- | Bitvector logical shift right
bvLShR   :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
bvLShR :: forall (n :: Natural).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
bvLShR   = Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Natural).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvLShR
{-# INLINE bvLShR #-}

-- | Concat two bitvectors
bvConcat :: (KnownNat n, KnownNat m) => Expr (BvSort n) -> Expr (BvSort m) -> Expr (BvSort (n + m))
bvConcat :: forall (n :: Natural) (m :: Natural).
(KnownNat n, KnownNat m) =>
Expr ('BvSort n) -> Expr ('BvSort m) -> Expr ('BvSort (n + m))
bvConcat = Expr ('BvSort n) -> Expr ('BvSort m) -> Expr ('BvSort (n + m))
forall (n :: Natural) (m :: Natural).
(KnownNat n, KnownNat m) =>
Expr ('BvSort n) -> Expr ('BvSort m) -> Expr ('BvSort (n + m))
BvConcat
{-# INLINE bvConcat #-}

-- | Rotate bitvector left
bvRotL   :: (KnownNat n, KnownNat i, KnownNat (Mod i n)) => Proxy i -> Expr (BvSort n) -> Expr (BvSort n)
bvRotL :: forall (n :: Natural) (i :: Natural).
(KnownNat n, KnownNat i, KnownNat (Mod i n)) =>
Proxy i -> Expr ('BvSort n) -> Expr ('BvSort n)
bvRotL   = Proxy i -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Natural) (i :: Natural).
(KnownNat n, KnownNat i, KnownNat (Mod i n)) =>
Proxy i -> Expr ('BvSort n) -> Expr ('BvSort n)
BvRotL
{-# INLINE bvRotL #-}

-- | Rotate bitvector right
bvRotR   :: (KnownNat n, KnownNat i, KnownNat (Mod i n)) => Proxy i -> Expr (BvSort n) -> Expr (BvSort n)
bvRotR :: forall (n :: Natural) (i :: Natural).
(KnownNat n, KnownNat i, KnownNat (Mod i n)) =>
Proxy i -> Expr ('BvSort n) -> Expr ('BvSort n)
bvRotR   = Proxy i -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Natural) (i :: Natural).
(KnownNat n, KnownNat i, KnownNat (Mod i n)) =>
Proxy i -> Expr ('BvSort n) -> Expr ('BvSort n)
BvRotR
{-# INLINE bvRotR #-}