{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}

-- |
-- Module      :   Grisette.Internal.SymPrim.SymInteger
-- Copyright   :   (c) Sirui Lu 2024
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Internal.SymPrim.SymInteger (SymInteger (SymInteger)) where

import Control.DeepSeq (NFData)
import Data.Hashable (Hashable (hashWithSalt))
import Data.String (IsString (fromString))
import GHC.Generics (Generic)
import Grisette.Internal.Core.Data.Class.Function (Apply (FunType, apply))
import Grisette.Internal.Core.Data.Class.Solvable (Solvable (con, conView, ssym, sym))
import Grisette.Internal.SymPrim.AllSyms (AllSyms (allSymsS), SomeSym (SomeSym))
import Grisette.Internal.SymPrim.Prim.Term
  ( ConRep (ConType),
    LinkedRep (underlyingTerm, wrapTerm),
    PEvalNumTerm
      ( pevalAbsNumTerm,
        pevalAddNumTerm,
        pevalMulNumTerm,
        pevalNegNumTerm,
        pevalSignumNumTerm
      ),
    SymRep (SymType),
    Term (ConTerm),
    conTerm,
    pevalSubNumTerm,
    pformat,
    symTerm,
  )
import Language.Haskell.TH.Syntax (Lift)

-- $setup
-- >>> import Grisette.Core
-- >>> import Grisette.SymPrim
-- >>> import Grisette.Backend
-- >>> import Data.Proxy

-- | Symbolic (unbounded, mathematical) integer type.
--
-- >>> "a" + 1 :: SymInteger
-- (+ 1 a)
--
-- More symbolic operations are available. Please refer to the documentation
-- for the type class instances.
newtype SymInteger = SymInteger {SymInteger -> Term Integer
underlyingIntegerTerm :: Term Integer}
  deriving ((forall (m :: * -> *). Quote m => SymInteger -> m Exp)
-> (forall (m :: * -> *).
    Quote m =>
    SymInteger -> Code m SymInteger)
-> Lift SymInteger
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => SymInteger -> m Exp
forall (m :: * -> *). Quote m => SymInteger -> Code m SymInteger
$clift :: forall (m :: * -> *). Quote m => SymInteger -> m Exp
lift :: forall (m :: * -> *). Quote m => SymInteger -> m Exp
$cliftTyped :: forall (m :: * -> *). Quote m => SymInteger -> Code m SymInteger
liftTyped :: forall (m :: * -> *). Quote m => SymInteger -> Code m SymInteger
Lift, SymInteger -> ()
(SymInteger -> ()) -> NFData SymInteger
forall a. (a -> ()) -> NFData a
$crnf :: SymInteger -> ()
rnf :: SymInteger -> ()
NFData, (forall x. SymInteger -> Rep SymInteger x)
-> (forall x. Rep SymInteger x -> SymInteger) -> Generic SymInteger
forall x. Rep SymInteger x -> SymInteger
forall x. SymInteger -> Rep SymInteger x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. SymInteger -> Rep SymInteger x
from :: forall x. SymInteger -> Rep SymInteger x
$cto :: forall x. Rep SymInteger x -> SymInteger
to :: forall x. Rep SymInteger x -> SymInteger
Generic)

instance ConRep SymInteger where
  type ConType SymInteger = Integer

instance SymRep Integer where
  type SymType Integer = SymInteger

instance LinkedRep Integer SymInteger where
  underlyingTerm :: SymInteger -> Term Integer
underlyingTerm (SymInteger Term Integer
a) = Term Integer
a
  wrapTerm :: Term Integer -> SymInteger
wrapTerm = Term Integer -> SymInteger
SymInteger

instance Apply SymInteger where
  type FunType SymInteger = SymInteger
  apply :: SymInteger -> FunType SymInteger
apply = SymInteger -> FunType SymInteger
SymInteger -> SymInteger
forall a. a -> a
id

instance Num SymInteger where
  (SymInteger Term Integer
l) + :: SymInteger -> SymInteger -> SymInteger
+ (SymInteger Term Integer
r) = Term Integer -> SymInteger
SymInteger (Term Integer -> SymInteger) -> Term Integer -> SymInteger
forall a b. (a -> b) -> a -> b
$ Term Integer -> Term Integer -> Term Integer
forall t. PEvalNumTerm t => Term t -> Term t -> Term t
pevalAddNumTerm Term Integer
l Term Integer
r
  (SymInteger Term Integer
l) - :: SymInteger -> SymInteger -> SymInteger
- (SymInteger Term Integer
r) = Term Integer -> SymInteger
SymInteger (Term Integer -> SymInteger) -> Term Integer -> SymInteger
forall a b. (a -> b) -> a -> b
$ Term Integer -> Term Integer -> Term Integer
forall t. PEvalNumTerm t => Term t -> Term t -> Term t
pevalSubNumTerm Term Integer
l Term Integer
r
  (SymInteger Term Integer
l) * :: SymInteger -> SymInteger -> SymInteger
* (SymInteger Term Integer
r) = Term Integer -> SymInteger
SymInteger (Term Integer -> SymInteger) -> Term Integer -> SymInteger
forall a b. (a -> b) -> a -> b
$ Term Integer -> Term Integer -> Term Integer
forall t. PEvalNumTerm t => Term t -> Term t -> Term t
pevalMulNumTerm Term Integer
l Term Integer
r
  negate :: SymInteger -> SymInteger
negate (SymInteger Term Integer
v) = Term Integer -> SymInteger
SymInteger (Term Integer -> SymInteger) -> Term Integer -> SymInteger
forall a b. (a -> b) -> a -> b
$ Term Integer -> Term Integer
forall t. PEvalNumTerm t => Term t -> Term t
pevalNegNumTerm Term Integer
v
  abs :: SymInteger -> SymInteger
abs (SymInteger Term Integer
v) = Term Integer -> SymInteger
SymInteger (Term Integer -> SymInteger) -> Term Integer -> SymInteger
forall a b. (a -> b) -> a -> b
$ Term Integer -> Term Integer
forall t. PEvalNumTerm t => Term t -> Term t
pevalAbsNumTerm Term Integer
v
  signum :: SymInteger -> SymInteger
signum (SymInteger Term Integer
v) = Term Integer -> SymInteger
SymInteger (Term Integer -> SymInteger) -> Term Integer -> SymInteger
forall a b. (a -> b) -> a -> b
$ Term Integer -> Term Integer
forall t. PEvalNumTerm t => Term t -> Term t
pevalSignumNumTerm Term Integer
v
  fromInteger :: Integer -> SymInteger
fromInteger = Integer -> SymInteger
forall c t. Solvable c t => c -> t
con

instance Eq SymInteger where
  SymInteger Term Integer
l == :: SymInteger -> SymInteger -> Bool
== SymInteger Term Integer
r = Term Integer
l Term Integer -> Term Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Term Integer
r

instance Hashable SymInteger where
  hashWithSalt :: Int -> SymInteger -> Int
hashWithSalt Int
s (SymInteger Term Integer
v) = Int
s Int -> Term Integer -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Term Integer
v

instance Solvable Integer SymInteger where
  con :: Integer -> SymInteger
con = Term Integer -> SymInteger
SymInteger (Term Integer -> SymInteger)
-> (Integer -> Term Integer) -> Integer -> SymInteger
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Term Integer
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm
  sym :: Symbol -> SymInteger
sym = Term Integer -> SymInteger
SymInteger (Term Integer -> SymInteger)
-> (Symbol -> Term Integer) -> Symbol -> SymInteger
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Term Integer
forall t. (SupportedPrim t, Typeable t) => Symbol -> Term t
symTerm
  conView :: SymInteger -> Maybe Integer
conView (SymInteger (ConTerm Int
_ Integer
t)) = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
t
  conView SymInteger
_ = Maybe Integer
forall a. Maybe a
Nothing

instance IsString SymInteger where
  fromString :: String -> SymInteger
fromString = Identifier -> SymInteger
forall c t. Solvable c t => Identifier -> t
ssym (Identifier -> SymInteger)
-> (String -> Identifier) -> String -> SymInteger
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Identifier
forall a. IsString a => String -> a
fromString

instance Show SymInteger where
  show :: SymInteger -> String
show (SymInteger Term Integer
t) = Term Integer -> String
forall t. SupportedPrim t => Term t -> String
pformat Term Integer
t

instance AllSyms SymInteger where
  allSymsS :: SymInteger -> [SomeSym] -> [SomeSym]
allSymsS SymInteger
v = (SymInteger -> SomeSym
forall con sym. LinkedRep con sym => sym -> SomeSym
SomeSym SymInteger
v SomeSym -> [SomeSym] -> [SomeSym]
forall a. a -> [a] -> [a]
:)