{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- |
-- Module      :   Grisette.Internal.Unified.BVBVConversion
-- 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.BVBVConversion
  ( UnifiedBVBVConversion,
    AllUnifiedBVBVConversion,
  )
where

import GHC.TypeNats (KnownNat, Nat, type (<=))
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.SymBV (SymIntN, SymWordN)
import Grisette.Internal.Unified.Class.UnifiedFromIntegral (UnifiedFromIntegral)
import Grisette.Internal.Unified.EvalModeTag (EvalModeTag (C, S))
import Grisette.Internal.Unified.UnifiedBV (UnifiedBVImpl (GetIntN, GetWordN))

class
  ( bv0 ~ bvn0 n0,
    bv1 ~ bvn1 n1,
    UnifiedFromIntegral mode bv0 bv1
  ) =>
  UnifiedBVBVConversionImpl
    (mode :: EvalModeTag)
    bvn0
    bvn1
    (n0 :: Nat)
    (n1 :: Nat)
    bv0
    bv1
    | bvn0 n0 -> bv0,
      bvn1 n1 -> bv1,
      bv0 -> bvn0 n0,
      bv1 -> bvn1 n1

#define QUOTE() '

#define CONINSTANCE(ty0, ty1) \
instance \
  (KnownNat n0, 1 <= n0, KnownNat n1, 1 <= n1) => \
  UnifiedBVBVConversionImpl QUOTE()C ty0 ty1 n0 n1 (ty0 n0) (ty1 n1)

#define SYMINSTANCE(ty0, ty1) \
instance \
  (KnownNat n0, 1 <= n0, KnownNat n1, 1 <= n1) => \
  UnifiedBVBVConversionImpl QUOTE()S ty0 ty1 n0 n1 (ty0 n0) (ty1 n1)

#if 1
CONINSTANCE(WordN, WordN)
CONINSTANCE(WordN, IntN)
CONINSTANCE(IntN, WordN)
CONINSTANCE(IntN, IntN)
SYMINSTANCE(SymWordN, SymWordN)
SYMINSTANCE(SymWordN, SymIntN)
SYMINSTANCE(SymIntN, SymWordN)
SYMINSTANCE(SymIntN, SymIntN)
#endif

-- | Unified constraints for conversion between bit-vectors.
class
  ( UnifiedBVBVConversionImpl
      mode
      (GetWordN mode)
      (GetWordN mode)
      n0
      n1
      (GetWordN mode n0)
      (GetWordN mode n1),
    UnifiedBVBVConversionImpl
      mode
      (GetWordN mode)
      (GetIntN mode)
      n0
      n1
      (GetWordN mode n0)
      (GetIntN mode n1),
    UnifiedBVBVConversionImpl
      mode
      (GetIntN mode)
      (GetWordN mode)
      n0
      n1
      (GetIntN mode n0)
      (GetWordN mode n1),
    UnifiedBVBVConversionImpl
      mode
      (GetIntN mode)
      (GetIntN mode)
      n0
      n1
      (GetIntN mode n0)
      (GetIntN mode n1)
  ) =>
  UnifiedBVBVConversion (mode :: EvalModeTag) n0 n1

instance
  ( UnifiedBVBVConversionImpl
      mode
      (GetWordN mode)
      (GetWordN mode)
      n0
      n1
      (GetWordN mode n0)
      (GetWordN mode n1),
    UnifiedBVBVConversionImpl
      mode
      (GetWordN mode)
      (GetIntN mode)
      n0
      n1
      (GetWordN mode n0)
      (GetIntN mode n1),
    UnifiedBVBVConversionImpl
      mode
      (GetIntN mode)
      (GetWordN mode)
      n0
      n1
      (GetIntN mode n0)
      (GetWordN mode n1),
    UnifiedBVBVConversionImpl
      mode
      (GetIntN mode)
      (GetIntN mode)
      n0
      n1
      (GetIntN mode n0)
      (GetIntN mode n1)
  ) =>
  UnifiedBVBVConversion (mode :: EvalModeTag) n0 n1

-- | Evaluation mode with unified conversion from bit-vectors to bit-vectors.
class
  ( forall n0 n1.
    (KnownNat n0, KnownNat n1, 1 <= n0, 1 <= n1) =>
    UnifiedBVBVConversion mode n0 n1
  ) =>
  AllUnifiedBVBVConversion mode

instance
  ( forall n0 n1.
    (KnownNat n0, KnownNat n1, 1 <= n0, 1 <= n1) =>
    UnifiedBVBVConversion mode n0 n1
  ) =>
  AllUnifiedBVBVConversion mode