{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- |
-- Module      :   Grisette.Internal.Internal.Decl.Core.Data.Class.ToSym
-- Copyright   :   (c) Sirui Lu 2021-2024
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Internal.Internal.Decl.Core.Data.Class.ToSym
  ( -- * Converting to symbolic values
    ToSym (..),
    ToSym1 (..),
    toSym1,
    ToSym2 (..),
    toSym2,

    -- * Generic 'ToSym'
    ToSymArgs (..),
    GToSym (..),
    genericToSym,
    genericLiftToSym,
  )
where

import Data.Kind (Type)
import Generics.Deriving
  ( Default (Default),
    Default1 (Default1),
    Generic (Rep, from, to),
    Generic1 (Rep1, from1, to1),
    K1 (K1),
    M1 (M1),
    Par1 (Par1),
    Rec1 (Rec1),
    U1 (U1),
    V1,
    (:.:) (Comp1),
    type (:*:) ((:*:)),
    type (:+:) (L1, R1),
  )
import Grisette.Internal.Utils.Derive (Arity0, Arity1)

-- $setup
-- >>> import Grisette.SymPrim

-- | Convert a concrete value to symbolic value.
class ToSym a b where
  -- | Convert a concrete value to symbolic value.
  --
  -- >>> toSym False :: SymBool
  -- false
  --
  -- >>> toSym [False, True] :: [SymBool]
  -- [false,true]
  toSym :: a -> b

instance {-# INCOHERENT #-} ToSym a a where
  toSym :: a -> a
toSym = a -> a
forall a. a -> a
id
  {-# INLINE toSym #-}

-- | Lifting of 'ToSym' to unary type constructors.
class
  (forall a b. (ToSym a b) => ToSym (f1 a) (f2 b)) =>
  ToSym1 f1 f2
  where
  -- | Lift a conversion to symbolic function to unary type constructors.
  liftToSym :: (a -> b) -> f1 a -> f2 b

-- | Lift the standard 'toSym' to unary type constructors.
toSym1 :: (ToSym1 f1 f2, ToSym a b) => f1 a -> f2 b
toSym1 :: forall (f1 :: * -> *) (f2 :: * -> *) a b.
(ToSym1 f1 f2, ToSym a b) =>
f1 a -> f2 b
toSym1 = (a -> b) -> f1 a -> f2 b
forall a b. (a -> b) -> f1 a -> f2 b
forall (f1 :: * -> *) (f2 :: * -> *) a b.
ToSym1 f1 f2 =>
(a -> b) -> f1 a -> f2 b
liftToSym a -> b
forall a b. ToSym a b => a -> b
toSym
{-# INLINE toSym1 #-}

-- | Lifting of 'ToSym' to binary type constructors.
class
  (forall a b. (ToSym a b) => ToSym1 (f1 a) (f2 b)) =>
  ToSym2 f1 f2
  where
  -- | Lift conversion to symbolic functions to binary type constructors.
  liftToSym2 :: (a -> b) -> (c -> d) -> f1 a c -> f2 b d

-- | Lift the standard 'toSym' to binary type constructors.
toSym2 :: (ToSym2 f1 f2, ToSym a b, ToSym c d) => f1 a c -> f2 b d
toSym2 :: forall (f1 :: * -> * -> *) (f2 :: * -> * -> *) a b c d.
(ToSym2 f1 f2, ToSym a b, ToSym c d) =>
f1 a c -> f2 b d
toSym2 = (a -> b) -> (c -> d) -> f1 a c -> f2 b d
forall a b c d. (a -> b) -> (c -> d) -> f1 a c -> f2 b d
forall (f1 :: * -> * -> *) (f2 :: * -> * -> *) a b c d.
ToSym2 f1 f2 =>
(a -> b) -> (c -> d) -> f1 a c -> f2 b d
liftToSym2 a -> b
forall a b. ToSym a b => a -> b
toSym c -> d
forall a b. ToSym a b => a -> b
toSym
{-# INLINE toSym2 #-}

-- Derivations

-- | The arguments to the generic 'toSym' function.
data family ToSymArgs arity a b :: Type

data instance ToSymArgs Arity0 _ _ = ToSymArgs0

data instance ToSymArgs Arity1 _ _ where
  ToSymArgs1 :: (a -> b) -> ToSymArgs Arity1 a b

-- | The class of types that can be generically converted to symbolic values.
class GToSym arity f1 f2 where
  gtoSym :: ToSymArgs arity a b -> f1 a -> f2 b

instance GToSym arity V1 V1 where
  gtoSym :: forall a b. ToSymArgs arity a b -> V1 a -> V1 b
gtoSym ToSymArgs arity a b
_ V1 a
_ = [Char] -> V1 b
forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible"
  {-# INLINE gtoSym #-}

instance GToSym arity U1 U1 where
  gtoSym :: forall a b. ToSymArgs arity a b -> U1 a -> U1 b
gtoSym ToSymArgs arity a b
_ U1 a
_ = U1 b
forall k (p :: k). U1 p
U1
  {-# INLINE gtoSym #-}

instance
  (GToSym arity a b, GToSym arity c d) =>
  GToSym arity (a :+: c) (b :+: d)
  where
  gtoSym :: forall a b. ToSymArgs arity a b -> (:+:) a c a -> (:+:) b d b
gtoSym ToSymArgs arity a b
args (L1 a a
a) = b b -> (:+:) b d b
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (b b -> (:+:) b d b) -> b b -> (:+:) b d b
forall a b. (a -> b) -> a -> b
$ ToSymArgs arity a b -> a a -> b b
forall a b. ToSymArgs arity a b -> a a -> b b
forall arity (f1 :: * -> *) (f2 :: * -> *) a b.
GToSym arity f1 f2 =>
ToSymArgs arity a b -> f1 a -> f2 b
gtoSym ToSymArgs arity a b
args a a
a
  gtoSym ToSymArgs arity a b
args (R1 c a
b) = d b -> (:+:) b d b
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (d b -> (:+:) b d b) -> d b -> (:+:) b d b
forall a b. (a -> b) -> a -> b
$ ToSymArgs arity a b -> c a -> d b
forall a b. ToSymArgs arity a b -> c a -> d b
forall arity (f1 :: * -> *) (f2 :: * -> *) a b.
GToSym arity f1 f2 =>
ToSymArgs arity a b -> f1 a -> f2 b
gtoSym ToSymArgs arity a b
args c a
b
  {-# INLINE gtoSym #-}

instance
  (GToSym arity a b, GToSym arity c d) =>
  GToSym arity (a :*: c) (b :*: d)
  where
  gtoSym :: forall a b. ToSymArgs arity a b -> (:*:) a c a -> (:*:) b d b
gtoSym ToSymArgs arity a b
args (a a
a :*: c a
c) = ToSymArgs arity a b -> a a -> b b
forall a b. ToSymArgs arity a b -> a a -> b b
forall arity (f1 :: * -> *) (f2 :: * -> *) a b.
GToSym arity f1 f2 =>
ToSymArgs arity a b -> f1 a -> f2 b
gtoSym ToSymArgs arity a b
args a a
a b b -> d b -> (:*:) b d b
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: ToSymArgs arity a b -> c a -> d b
forall a b. ToSymArgs arity a b -> c a -> d b
forall arity (f1 :: * -> *) (f2 :: * -> *) a b.
GToSym arity f1 f2 =>
ToSymArgs arity a b -> f1 a -> f2 b
gtoSym ToSymArgs arity a b
args c a
c
  {-# INLINE gtoSym #-}

instance (ToSym a b) => GToSym arity (K1 i a) (K1 i b) where
  gtoSym :: forall a b. ToSymArgs arity a b -> K1 i a a -> K1 i b b
gtoSym ToSymArgs arity a b
_ (K1 a
a) = b -> K1 i b b
forall k i c (p :: k). c -> K1 i c p
K1 (b -> K1 i b b) -> b -> K1 i b b
forall a b. (a -> b) -> a -> b
$ a -> b
forall a b. ToSym a b => a -> b
toSym a
a
  {-# INLINE gtoSym #-}

instance (GToSym arity f1 f2) => GToSym arity (M1 i c1 f1) (M1 i c2 f2) where
  gtoSym :: forall a b. ToSymArgs arity a b -> M1 i c1 f1 a -> M1 i c2 f2 b
gtoSym ToSymArgs arity a b
args (M1 f1 a
a) = f2 b -> M1 i c2 f2 b
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (f2 b -> M1 i c2 f2 b) -> f2 b -> M1 i c2 f2 b
forall a b. (a -> b) -> a -> b
$ ToSymArgs arity a b -> f1 a -> f2 b
forall a b. ToSymArgs arity a b -> f1 a -> f2 b
forall arity (f1 :: * -> *) (f2 :: * -> *) a b.
GToSym arity f1 f2 =>
ToSymArgs arity a b -> f1 a -> f2 b
gtoSym ToSymArgs arity a b
args f1 a
a
  {-# INLINE gtoSym #-}

instance GToSym Arity1 Par1 Par1 where
  gtoSym :: forall a b. ToSymArgs Arity1 a b -> Par1 a -> Par1 b
gtoSym (ToSymArgs1 a -> b
f) (Par1 a
a) = b -> Par1 b
forall p. p -> Par1 p
Par1 (b -> Par1 b) -> b -> Par1 b
forall a b. (a -> b) -> a -> b
$ a -> b
f a
a
  {-# INLINE gtoSym #-}

instance (ToSym1 f1 f2) => GToSym Arity1 (Rec1 f1) (Rec1 f2) where
  gtoSym :: forall a b. ToSymArgs Arity1 a b -> Rec1 f1 a -> Rec1 f2 b
gtoSym (ToSymArgs1 a -> b
f) (Rec1 f1 a
a) = f2 b -> Rec1 f2 b
forall k (f :: k -> *) (p :: k). f p -> Rec1 f p
Rec1 (f2 b -> Rec1 f2 b) -> f2 b -> Rec1 f2 b
forall a b. (a -> b) -> a -> b
$ (a -> b) -> f1 a -> f2 b
forall a b. (a -> b) -> f1 a -> f2 b
forall (f1 :: * -> *) (f2 :: * -> *) a b.
ToSym1 f1 f2 =>
(a -> b) -> f1 a -> f2 b
liftToSym a -> b
f f1 a
a
  {-# INLINE gtoSym #-}

instance
  (ToSym1 f1 f2, GToSym Arity1 g1 g2) =>
  GToSym Arity1 (f1 :.: g1) (f2 :.: g2)
  where
  gtoSym :: forall a b. ToSymArgs Arity1 a b -> (:.:) f1 g1 a -> (:.:) f2 g2 b
gtoSym targs :: ToSymArgs Arity1 a b
targs@ToSymArgs1 {} (Comp1 f1 (g1 a)
a) = f2 (g2 b) -> (:.:) f2 g2 b
forall k2 k1 (f :: k2 -> *) (g :: k1 -> k2) (p :: k1).
f (g p) -> (:.:) f g p
Comp1 (f2 (g2 b) -> (:.:) f2 g2 b) -> f2 (g2 b) -> (:.:) f2 g2 b
forall a b. (a -> b) -> a -> b
$ (g1 a -> g2 b) -> f1 (g1 a) -> f2 (g2 b)
forall a b. (a -> b) -> f1 a -> f2 b
forall (f1 :: * -> *) (f2 :: * -> *) a b.
ToSym1 f1 f2 =>
(a -> b) -> f1 a -> f2 b
liftToSym (ToSymArgs Arity1 a b -> g1 a -> g2 b
forall a b. ToSymArgs Arity1 a b -> g1 a -> g2 b
forall arity (f1 :: * -> *) (f2 :: * -> *) a b.
GToSym arity f1 f2 =>
ToSymArgs arity a b -> f1 a -> f2 b
gtoSym ToSymArgs Arity1 a b
targs) f1 (g1 a)
a
  {-# INLINE gtoSym #-}

-- | Generic 'toSym' function.
genericToSym ::
  (Generic a, Generic b, GToSym Arity0 (Rep a) (Rep b)) =>
  a ->
  b
genericToSym :: forall a b.
(Generic a, Generic b, GToSym Arity0 (Rep a) (Rep b)) =>
a -> b
genericToSym = Rep b Any -> b
forall a x. Generic a => Rep a x -> a
forall x. Rep b x -> b
to (Rep b Any -> b) -> (a -> Rep b Any) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ToSymArgs Arity0 Any Any -> Rep a Any -> Rep b Any
forall a b. ToSymArgs Arity0 a b -> Rep a a -> Rep b b
forall arity (f1 :: * -> *) (f2 :: * -> *) a b.
GToSym arity f1 f2 =>
ToSymArgs arity a b -> f1 a -> f2 b
gtoSym ToSymArgs Arity0 Any Any
forall _ _. ToSymArgs Arity0 _ _
ToSymArgs0 (Rep a Any -> Rep b Any) -> (a -> Rep a Any) -> a -> Rep b Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from
{-# INLINE genericToSym #-}

-- | Generic 'liftToSym' function.
genericLiftToSym ::
  (Generic1 f1, Generic1 f2, GToSym Arity1 (Rep1 f1) (Rep1 f2)) =>
  (a -> b) ->
  f1 a ->
  f2 b
genericLiftToSym :: forall (f1 :: * -> *) (f2 :: * -> *) a b.
(Generic1 f1, Generic1 f2, GToSym Arity1 (Rep1 f1) (Rep1 f2)) =>
(a -> b) -> f1 a -> f2 b
genericLiftToSym a -> b
f = Rep1 f2 b -> f2 b
forall a. Rep1 f2 a -> f2 a
forall k (f :: k -> *) (a :: k). Generic1 f => Rep1 f a -> f a
to1 (Rep1 f2 b -> f2 b) -> (f1 a -> Rep1 f2 b) -> f1 a -> f2 b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ToSymArgs Arity1 a b -> Rep1 f1 a -> Rep1 f2 b
forall a b. ToSymArgs Arity1 a b -> Rep1 f1 a -> Rep1 f2 b
forall arity (f1 :: * -> *) (f2 :: * -> *) a b.
GToSym arity f1 f2 =>
ToSymArgs arity a b -> f1 a -> f2 b
gtoSym ((a -> b) -> ToSymArgs Arity1 a b
forall a b. (a -> b) -> ToSymArgs Arity1 a b
ToSymArgs1 a -> b
f) (Rep1 f1 a -> Rep1 f2 b)
-> (f1 a -> Rep1 f1 a) -> f1 a -> Rep1 f2 b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f1 a -> Rep1 f1 a
forall a. f1 a -> Rep1 f1 a
forall k (f :: k -> *) (a :: k). Generic1 f => f a -> Rep1 f a
from1
{-# INLINE genericLiftToSym #-}

instance
  ( Generic a,
    Generic b,
    GToSym Arity0 (Rep a) (Rep b)
  ) =>
  ToSym a (Default b)
  where
  toSym :: a -> Default b
toSym = b -> Default b
forall a. a -> Default a
Default (b -> Default b) -> (a -> b) -> a -> Default b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
forall a b.
(Generic a, Generic b, GToSym Arity0 (Rep a) (Rep b)) =>
a -> b
genericToSym
  {-# INLINE toSym #-}

instance
  ( Generic1 f1,
    Generic1 f2,
    GToSym Arity1 (Rep1 f1) (Rep1 f2),
    ToSym a b
  ) =>
  ToSym (f1 a) (Default1 f2 b)
  where
  toSym :: f1 a -> Default1 f2 b
toSym = f1 a -> Default1 f2 b
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(ToSym1 f1 f2, ToSym a b) =>
f1 a -> f2 b
toSym1

instance
  ( Generic1 f1,
    Generic1 f2,
    GToSym Arity1 (Rep1 f1) (Rep1 f2)
  ) =>
  ToSym1 f1 (Default1 f2)
  where
  liftToSym :: forall a b. (a -> b) -> f1 a -> Default1 f2 b
liftToSym a -> b
f = f2 b -> Default1 f2 b
forall (f :: * -> *) a. f a -> Default1 f a
Default1 (f2 b -> Default1 f2 b) -> (f1 a -> f2 b) -> f1 a -> Default1 f2 b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b) -> f1 a -> f2 b
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(Generic1 f1, Generic1 f2, GToSym Arity1 (Rep1 f1) (Rep1 f2)) =>
(a -> b) -> f1 a -> f2 b
genericLiftToSym a -> b
f
  {-# INLINE liftToSym #-}