UnifiedFromIntegral.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- |
-- Module      :   Grisette.Internal.Unified.Class.UnifiedFromIntegral
-- 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.Unified.Class.UnifiedFromIntegral
  ( UnifiedFromIntegral (..),
    symFromIntegral,
  )
where

import Data.Type.Bool (If)
import GHC.TypeNats (KnownNat, type (<=))
import Grisette.Internal.Core.Data.Class.SymFromIntegral (SymFromIntegral)
import qualified Grisette.Internal.Core.Data.Class.SymFromIntegral as SymFromIntegral
import Grisette.Internal.SymPrim.AlgReal (AlgReal)
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.FP (FP, ValidFP)
import Grisette.Internal.SymPrim.SymAlgReal (SymAlgReal)
import Grisette.Internal.SymPrim.SymBV (SymIntN, SymWordN)
import Grisette.Internal.SymPrim.SymFP (SymFP)
import Grisette.Internal.SymPrim.SymInteger (SymInteger)
import Grisette.Internal.Unified.EvalModeTag (EvalModeTag (C, S), IsConMode)
import Grisette.Internal.Unified.Util (DecideEvalMode, withMode)

-- | Unified `Grisette.Internal.Core.Data.Class.SymFromIntegral.symFromIntegral`
-- operation.
--
-- This function isn't able to infer the mode, so you need to provide the mode
-- explicitly. For example:
--
-- > symFromIntegral @mode a
symFromIntegral ::
  forall mode a b. (DecideEvalMode mode, UnifiedFromIntegral mode a b) => a -> b
symFromIntegral a =
  withMode @mode
    (withBaseFromIntegral @mode @a @b $ fromIntegral a)
    (withBaseFromIntegral @mode @a @b $ SymFromIntegral.symFromIntegral a)

-- | A class that provides unified conversion from integral types.
--
-- We use this type class to help resolve the constraints for `SymFromIntegral`.
class UnifiedFromIntegral (mode :: EvalModeTag) a b where
  withBaseFromIntegral ::
    ((If (IsConMode mode) (Integral a, Num b) (SymFromIntegral a b)) => r) -> r

instance
  {-# INCOHERENT #-}
  ( DecideEvalMode mode,
    (If (IsConMode mode) (Integral a, Num b) (SymFromIntegral a b))
  ) =>
  UnifiedFromIntegral mode a b
  where
  withBaseFromIntegral r = r

instance UnifiedFromIntegral 'C Integer AlgReal where
  withBaseFromIntegral r = r

instance UnifiedFromIntegral 'C Integer Integer where
  withBaseFromIntegral r = r

instance (KnownNat n, 1 <= n) => UnifiedFromIntegral 'C Integer (IntN n) where
  withBaseFromIntegral r = r

instance
  (KnownNat n, 1 <= n) =>
  UnifiedFromIntegral 'C Integer (WordN n)
  where
  withBaseFromIntegral r = r

instance (ValidFP eb sb) => UnifiedFromIntegral 'C Integer (FP eb sb) where
  withBaseFromIntegral r = r

instance
  (KnownNat n', 1 <= n') =>
  UnifiedFromIntegral 'C (IntN n') AlgReal
  where
  withBaseFromIntegral r = r

instance
  (KnownNat n', 1 <= n') =>
  UnifiedFromIntegral 'C (IntN n') Integer
  where
  withBaseFromIntegral r = r

instance
  (KnownNat n', 1 <= n', KnownNat n, 1 <= n) =>
  UnifiedFromIntegral 'C (IntN n') (IntN n)
  where
  withBaseFromIntegral r = r

instance
  (KnownNat n', 1 <= n', KnownNat n, 1 <= n) =>
  UnifiedFromIntegral 'C (IntN n') (WordN n)
  where
  withBaseFromIntegral r = r

instance
  (KnownNat n', 1 <= n', ValidFP eb sb) =>
  UnifiedFromIntegral 'C (IntN n') (FP eb sb)
  where
  withBaseFromIntegral r = r

instance
  (KnownNat n', 1 <= n') =>
  UnifiedFromIntegral 'C (WordN n') AlgReal
  where
  withBaseFromIntegral r = r

instance
  (KnownNat n', 1 <= n') =>
  UnifiedFromIntegral 'C (WordN n') Integer
  where
  withBaseFromIntegral r = r

instance
  (KnownNat n', 1 <= n', KnownNat n, 1 <= n) =>
  UnifiedFromIntegral 'C (WordN n') (IntN n)
  where
  withBaseFromIntegral r = r

instance
  (KnownNat n', 1 <= n', KnownNat n, 1 <= n) =>
  UnifiedFromIntegral 'C (WordN n') (WordN n)
  where
  withBaseFromIntegral r = r

instance
  (KnownNat n', 1 <= n', ValidFP eb sb) =>
  UnifiedFromIntegral 'C (WordN n') (FP eb sb)
  where
  withBaseFromIntegral r = r

instance UnifiedFromIntegral 'S SymInteger SymAlgReal where
  withBaseFromIntegral r = r

instance UnifiedFromIntegral 'S SymInteger SymInteger where
  withBaseFromIntegral r = r

instance (KnownNat n, 1 <= n) => UnifiedFromIntegral 'S SymInteger (SymIntN n) where
  withBaseFromIntegral r = r

instance
  (KnownNat n, 1 <= n) =>
  UnifiedFromIntegral 'S SymInteger (SymWordN n)
  where
  withBaseFromIntegral r = r

instance (ValidFP eb sb) => UnifiedFromIntegral 'S SymInteger (SymFP eb sb) where
  withBaseFromIntegral r = r

instance
  (KnownNat n', 1 <= n') =>
  UnifiedFromIntegral 'S (SymIntN n') SymAlgReal
  where
  withBaseFromIntegral r = r

instance
  (KnownNat n', 1 <= n') =>
  UnifiedFromIntegral 'S (SymIntN n') SymInteger
  where
  withBaseFromIntegral r = r

instance
  (KnownNat n', 1 <= n', KnownNat n, 1 <= n) =>
  UnifiedFromIntegral 'S (SymIntN n') (SymIntN n)
  where
  withBaseFromIntegral r = r

instance
  (KnownNat n', 1 <= n', KnownNat n, 1 <= n) =>
  UnifiedFromIntegral 'S (SymIntN n') (SymWordN n)
  where
  withBaseFromIntegral r = r

instance
  (KnownNat n', 1 <= n', ValidFP eb sb) =>
  UnifiedFromIntegral 'S (SymIntN n') (SymFP eb sb)
  where
  withBaseFromIntegral r = r

instance
  (KnownNat n', 1 <= n') =>
  UnifiedFromIntegral 'S (SymWordN n') SymAlgReal
  where
  withBaseFromIntegral r = r

instance
  (KnownNat n', 1 <= n') =>
  UnifiedFromIntegral 'S (SymWordN n') SymInteger
  where
  withBaseFromIntegral r = r

instance
  (KnownNat n', 1 <= n', KnownNat n, 1 <= n) =>
  UnifiedFromIntegral 'S (SymWordN n') (SymIntN n)
  where
  withBaseFromIntegral r = r

instance
  (KnownNat n', 1 <= n', KnownNat n, 1 <= n) =>
  UnifiedFromIntegral 'S (SymWordN n') (SymWordN n)
  where
  withBaseFromIntegral r = r

instance
  (KnownNat n', 1 <= n', ValidFP eb sb) =>
  UnifiedFromIntegral 'S (SymWordN n') (SymFP eb sb)
  where
  withBaseFromIntegral r = r