{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- |
-- Module      :   Grisette.Internal.Core.Data.Class.SymFromIntegral
-- 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.Core.Data.Class.SymFromIntegral
  ( SymFromIntegral (..),
  )
where

import GHC.TypeLits (KnownNat, type (<=))
import Grisette.Internal.SymPrim.FP (ValidFP)
import Grisette.Internal.SymPrim.Prim.Internal.Term
  ( PEvalFromIntegralTerm (pevalFromIntegralTerm),
  )
import Grisette.Internal.SymPrim.SymAlgReal (SymAlgReal (SymAlgReal))
import Grisette.Internal.SymPrim.SymBV (SymIntN (SymIntN), SymWordN (SymWordN))
import Grisette.Internal.SymPrim.SymFP (SymFP (SymFP))
import Grisette.Internal.SymPrim.SymInteger (SymInteger (SymInteger))

-- | Conversion from a symbolic integral type.
class SymFromIntegral from to where
  symFromIntegral :: from -> to

instance SymFromIntegral SymInteger SymInteger where
  symFromIntegral :: SymInteger -> SymInteger
symFromIntegral = SymInteger -> SymInteger
forall a. a -> a
id
  {-# INLINE symFromIntegral #-}

instance SymFromIntegral SymInteger SymAlgReal where
  symFromIntegral :: SymInteger -> SymAlgReal
symFromIntegral (SymInteger Term Integer
x) = Term AlgReal -> SymAlgReal
SymAlgReal (Term AlgReal -> SymAlgReal) -> Term AlgReal -> SymAlgReal
forall a b. (a -> b) -> a -> b
$ Term Integer -> Term AlgReal
forall a b. PEvalFromIntegralTerm a b => Term a -> Term b
pevalFromIntegralTerm Term Integer
x
  {-# INLINE symFromIntegral #-}

instance (KnownNat n, 1 <= n) => SymFromIntegral SymInteger (SymWordN n) where
  symFromIntegral :: SymInteger -> SymWordN n
symFromIntegral (SymInteger Term Integer
x) = Term (WordN n) -> SymWordN n
forall (n :: Nat). Term (WordN n) -> SymWordN n
SymWordN (Term (WordN n) -> SymWordN n) -> Term (WordN n) -> SymWordN n
forall a b. (a -> b) -> a -> b
$ Term Integer -> Term (WordN n)
forall a b. PEvalFromIntegralTerm a b => Term a -> Term b
pevalFromIntegralTerm Term Integer
x
  {-# INLINE symFromIntegral #-}

instance (KnownNat n, 1 <= n) => SymFromIntegral SymInteger (SymIntN n) where
  symFromIntegral :: SymInteger -> SymIntN n
symFromIntegral (SymInteger Term Integer
x) = Term (IntN n) -> SymIntN n
forall (n :: Nat). Term (IntN n) -> SymIntN n
SymIntN (Term (IntN n) -> SymIntN n) -> Term (IntN n) -> SymIntN n
forall a b. (a -> b) -> a -> b
$ Term Integer -> Term (IntN n)
forall a b. PEvalFromIntegralTerm a b => Term a -> Term b
pevalFromIntegralTerm Term Integer
x
  {-# INLINE symFromIntegral #-}

instance (ValidFP eb sb) => SymFromIntegral SymInteger (SymFP eb sb) where
  symFromIntegral :: SymInteger -> SymFP eb sb
symFromIntegral (SymInteger Term Integer
x) = Term (FP eb sb) -> SymFP eb sb
forall (eb :: Nat) (sb :: Nat). Term (FP eb sb) -> SymFP eb sb
SymFP (Term (FP eb sb) -> SymFP eb sb) -> Term (FP eb sb) -> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ Term Integer -> Term (FP eb sb)
forall a b. PEvalFromIntegralTerm a b => Term a -> Term b
pevalFromIntegralTerm Term Integer
x
  {-# INLINE symFromIntegral #-}

instance (KnownNat n, 1 <= n) => SymFromIntegral (SymWordN n) SymInteger where
  symFromIntegral :: SymWordN n -> SymInteger
symFromIntegral (SymWordN Term (WordN n)
x) = Term Integer -> SymInteger
SymInteger (Term Integer -> SymInteger) -> Term Integer -> SymInteger
forall a b. (a -> b) -> a -> b
$ Term (WordN n) -> Term Integer
forall a b. PEvalFromIntegralTerm a b => Term a -> Term b
pevalFromIntegralTerm Term (WordN n)
x
  {-# INLINE symFromIntegral #-}

instance
  (KnownNat n, KnownNat m, 1 <= n, 1 <= m) =>
  SymFromIntegral (SymWordN n) (SymWordN m)
  where
  symFromIntegral :: SymWordN n -> SymWordN m
symFromIntegral (SymWordN Term (WordN n)
x) = Term (WordN m) -> SymWordN m
forall (n :: Nat). Term (WordN n) -> SymWordN n
SymWordN (Term (WordN m) -> SymWordN m) -> Term (WordN m) -> SymWordN m
forall a b. (a -> b) -> a -> b
$ Term (WordN n) -> Term (WordN m)
forall a b. PEvalFromIntegralTerm a b => Term a -> Term b
pevalFromIntegralTerm Term (WordN n)
x
  {-# INLINE symFromIntegral #-}

instance (KnownNat n, 1 <= n) => SymFromIntegral (SymWordN n) SymAlgReal where
  symFromIntegral :: SymWordN n -> SymAlgReal
symFromIntegral (SymWordN Term (WordN n)
x) = Term AlgReal -> SymAlgReal
SymAlgReal (Term AlgReal -> SymAlgReal) -> Term AlgReal -> SymAlgReal
forall a b. (a -> b) -> a -> b
$ Term (WordN n) -> Term AlgReal
forall a b. PEvalFromIntegralTerm a b => Term a -> Term b
pevalFromIntegralTerm Term (WordN n)
x
  {-# INLINE symFromIntegral #-}

instance
  (KnownNat n, KnownNat m, 1 <= n, 1 <= m) =>
  SymFromIntegral (SymWordN n) (SymIntN m)
  where
  symFromIntegral :: SymWordN n -> SymIntN m
symFromIntegral (SymWordN Term (WordN n)
x) = Term (IntN m) -> SymIntN m
forall (n :: Nat). Term (IntN n) -> SymIntN n
SymIntN (Term (IntN m) -> SymIntN m) -> Term (IntN m) -> SymIntN m
forall a b. (a -> b) -> a -> b
$ Term (WordN n) -> Term (IntN m)
forall a b. PEvalFromIntegralTerm a b => Term a -> Term b
pevalFromIntegralTerm Term (WordN n)
x
  {-# INLINE symFromIntegral #-}

instance
  (KnownNat n, 1 <= n, ValidFP eb sb) =>
  SymFromIntegral (SymWordN n) (SymFP eb sb)
  where
  symFromIntegral :: SymWordN n -> SymFP eb sb
symFromIntegral (SymWordN Term (WordN n)
x) = Term (FP eb sb) -> SymFP eb sb
forall (eb :: Nat) (sb :: Nat). Term (FP eb sb) -> SymFP eb sb
SymFP (Term (FP eb sb) -> SymFP eb sb) -> Term (FP eb sb) -> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ Term (WordN n) -> Term (FP eb sb)
forall a b. PEvalFromIntegralTerm a b => Term a -> Term b
pevalFromIntegralTerm Term (WordN n)
x
  {-# INLINE symFromIntegral #-}

instance (KnownNat n, 1 <= n) => SymFromIntegral (SymIntN n) SymInteger where
  symFromIntegral :: SymIntN n -> SymInteger
symFromIntegral (SymIntN Term (IntN n)
x) = Term Integer -> SymInteger
SymInteger (Term Integer -> SymInteger) -> Term Integer -> SymInteger
forall a b. (a -> b) -> a -> b
$ Term (IntN n) -> Term Integer
forall a b. PEvalFromIntegralTerm a b => Term a -> Term b
pevalFromIntegralTerm Term (IntN n)
x
  {-# INLINE symFromIntegral #-}

instance
  (KnownNat n, KnownNat m, 1 <= n, 1 <= m) =>
  SymFromIntegral (SymIntN n) (SymWordN m)
  where
  symFromIntegral :: SymIntN n -> SymWordN m
symFromIntegral (SymIntN Term (IntN n)
x) = Term (WordN m) -> SymWordN m
forall (n :: Nat). Term (WordN n) -> SymWordN n
SymWordN (Term (WordN m) -> SymWordN m) -> Term (WordN m) -> SymWordN m
forall a b. (a -> b) -> a -> b
$ Term (IntN n) -> Term (WordN m)
forall a b. PEvalFromIntegralTerm a b => Term a -> Term b
pevalFromIntegralTerm Term (IntN n)
x
  {-# INLINE symFromIntegral #-}

instance (KnownNat n, 1 <= n) => SymFromIntegral (SymIntN n) SymAlgReal where
  symFromIntegral :: SymIntN n -> SymAlgReal
symFromIntegral (SymIntN Term (IntN n)
x) = Term AlgReal -> SymAlgReal
SymAlgReal (Term AlgReal -> SymAlgReal) -> Term AlgReal -> SymAlgReal
forall a b. (a -> b) -> a -> b
$ Term (IntN n) -> Term AlgReal
forall a b. PEvalFromIntegralTerm a b => Term a -> Term b
pevalFromIntegralTerm Term (IntN n)
x
  {-# INLINE symFromIntegral #-}

instance
  (KnownNat n, KnownNat m, 1 <= n, 1 <= m) =>
  SymFromIntegral (SymIntN n) (SymIntN m)
  where
  symFromIntegral :: SymIntN n -> SymIntN m
symFromIntegral (SymIntN Term (IntN n)
x) = Term (IntN m) -> SymIntN m
forall (n :: Nat). Term (IntN n) -> SymIntN n
SymIntN (Term (IntN m) -> SymIntN m) -> Term (IntN m) -> SymIntN m
forall a b. (a -> b) -> a -> b
$ Term (IntN n) -> Term (IntN m)
forall a b. PEvalFromIntegralTerm a b => Term a -> Term b
pevalFromIntegralTerm Term (IntN n)
x
  {-# INLINE symFromIntegral #-}

instance
  (KnownNat n, 1 <= n, ValidFP eb sb) =>
  SymFromIntegral (SymIntN n) (SymFP eb sb)
  where
  symFromIntegral :: SymIntN n -> SymFP eb sb
symFromIntegral (SymIntN Term (IntN n)
x) = Term (FP eb sb) -> SymFP eb sb
forall (eb :: Nat) (sb :: Nat). Term (FP eb sb) -> SymFP eb sb
SymFP (Term (FP eb sb) -> SymFP eb sb) -> Term (FP eb sb) -> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ Term (IntN n) -> Term (FP eb sb)
forall a b. PEvalFromIntegralTerm a b => Term a -> Term b
pevalFromIntegralTerm Term (IntN n)
x
  {-# INLINE symFromIntegral #-}