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

-- |
-- Module      :   Grisette.Internal.Internal.Decl.Core.Data.Class.ToCon
-- 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.ToCon
  ( -- * Converting to concrete values
    ToCon (..),
    ToCon1 (..),
    toCon1,
    ToCon2 (..),
    toCon2,

    -- * Generic 'ToCon'
    ToConArgs (..),
    GToCon (..),
    genericToCon,
    genericLiftToCon,
  )
where

import Data.Kind (Type)
import GHC.Generics
  ( 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 Generics.Deriving (Default (Default), Default1 (Default1))
import Generics.Deriving.Instances ()
import Grisette.Internal.Core.Data.Class.Solvable (Solvable (conView))
import Grisette.Internal.SymPrim.SymBool (SymBool)
import Grisette.Internal.Utils.Derive (Arity0, Arity1)

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

-- | Convert a symbolic value to concrete value if possible.
class ToCon a b where
  -- | Convert a symbolic value to concrete value if possible.
  -- If the symbolic value cannot be converted to concrete, the result will be 'Nothing'.
  --
  -- >>> toCon (ssym "a" :: SymInteger) :: Maybe Integer
  -- Nothing
  --
  -- >>> toCon (con 1 :: SymInteger) :: Maybe Integer
  -- Just 1
  --
  -- 'toCon' works on complex types too.
  --
  -- >>> toCon ([con 1, con 2] :: [SymInteger]) :: Maybe [Integer]
  -- Just [1,2]
  --
  -- >>> toCon ([con 1, ssym "a"] :: [SymInteger]) :: Maybe [Integer]
  -- Nothing
  toCon :: a -> Maybe b

instance {-# INCOHERENT #-} ToCon v v where
  toCon :: v -> Maybe v
toCon = v -> Maybe v
forall v. v -> Maybe v
Just

-- | Lifting of 'ToCon' to unary type constructors.
class (forall a b. (ToCon a b) => ToCon (f1 a) (f2 b)) => ToCon1 f1 f2 where
  -- | Lift a conversion to concrete function to unary type constructors.
  liftToCon :: (a -> Maybe b) -> f1 a -> Maybe (f2 b)

-- | Lift the standard 'toCon' to unary type constructors.
toCon1 :: (ToCon1 f1 f2, ToCon a b) => f1 a -> Maybe (f2 b)
toCon1 :: forall (f1 :: * -> *) (f2 :: * -> *) a b.
(ToCon1 f1 f2, ToCon a b) =>
f1 a -> Maybe (f2 b)
toCon1 = (a -> Maybe b) -> f1 a -> Maybe (f2 b)
forall a b. (a -> Maybe b) -> f1 a -> Maybe (f2 b)
forall (f1 :: * -> *) (f2 :: * -> *) a b.
ToCon1 f1 f2 =>
(a -> Maybe b) -> f1 a -> Maybe (f2 b)
liftToCon a -> Maybe b
forall a b. ToCon a b => a -> Maybe b
toCon
{-# INLINE toCon1 #-}

-- | Lifting of 'ToCon' to binary type constructors.
class (forall a b. (ToCon a b) => ToCon1 (f1 a) (f2 b)) => ToCon2 f1 f2 where
  -- | Lift conversion to concrete functions to binary type constructors.
  liftToCon2 :: (a -> Maybe b) -> (c -> Maybe d) -> f1 a c -> Maybe (f2 b d)

-- | Lift the standard 'toCon' to binary type constructors.
toCon2 :: (ToCon2 f1 f2, ToCon a b, ToCon c d) => f1 a c -> Maybe (f2 b d)
toCon2 :: forall (f1 :: * -> * -> *) (f2 :: * -> * -> *) a b c d.
(ToCon2 f1 f2, ToCon a b, ToCon c d) =>
f1 a c -> Maybe (f2 b d)
toCon2 = (a -> Maybe b) -> (c -> Maybe d) -> f1 a c -> Maybe (f2 b d)
forall a b c d.
(a -> Maybe b) -> (c -> Maybe d) -> f1 a c -> Maybe (f2 b d)
forall (f1 :: * -> * -> *) (f2 :: * -> * -> *) a b c d.
ToCon2 f1 f2 =>
(a -> Maybe b) -> (c -> Maybe d) -> f1 a c -> Maybe (f2 b d)
liftToCon2 a -> Maybe b
forall a b. ToCon a b => a -> Maybe b
toCon c -> Maybe d
forall a b. ToCon a b => a -> Maybe b
toCon
{-# INLINE toCon2 #-}

-- Derivations

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

data instance ToConArgs Arity0 _ _ = ToConArgs0

newtype instance ToConArgs Arity1 a b
  = ToConArgs1 (a -> Maybe b)

-- | The class of types that can be generically converted to concrete values.
class GToCon arity f1 f2 where
  gtoCon :: ToConArgs arity a b -> f1 a -> Maybe (f2 b)

instance GToCon arity V1 V1 where
  gtoCon :: forall a b. ToConArgs arity a b -> V1 a -> Maybe (V1 b)
gtoCon ToConArgs arity a b
_ V1 a
_ = [Char] -> Maybe (V1 b)
forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible"
  {-# INLINE gtoCon #-}

instance GToCon arity U1 U1 where
  gtoCon :: forall a b. ToConArgs arity a b -> U1 a -> Maybe (U1 b)
gtoCon ToConArgs arity a b
_ U1 a
_ = U1 b -> Maybe (U1 b)
forall v. v -> Maybe v
Just U1 b
forall k (p :: k). U1 p
U1
  {-# INLINE gtoCon #-}

instance
  (GToCon arity a b, GToCon arity c d) =>
  GToCon arity (a :*: c) (b :*: d)
  where
  gtoCon :: forall a b.
ToConArgs arity a b -> (:*:) a c a -> Maybe ((:*:) b d b)
gtoCon ToConArgs arity a b
args (a a
a :*: c a
c) = do
    b b
a' <- ToConArgs arity a b -> a a -> Maybe (b b)
forall a b. ToConArgs arity a b -> a a -> Maybe (b b)
forall arity (f1 :: * -> *) (f2 :: * -> *) a b.
GToCon arity f1 f2 =>
ToConArgs arity a b -> f1 a -> Maybe (f2 b)
gtoCon ToConArgs arity a b
args a a
a
    d b
c' <- ToConArgs arity a b -> c a -> Maybe (d b)
forall a b. ToConArgs arity a b -> c a -> Maybe (d b)
forall arity (f1 :: * -> *) (f2 :: * -> *) a b.
GToCon arity f1 f2 =>
ToConArgs arity a b -> f1 a -> Maybe (f2 b)
gtoCon ToConArgs arity a b
args c a
c
    (:*:) b d b -> Maybe ((:*:) b d b)
forall v. v -> Maybe v
forall (m :: * -> *) a. Monad m => a -> m a
return ((:*:) b d b -> Maybe ((:*:) b d b))
-> (:*:) b d b -> Maybe ((:*:) b d b)
forall a b. (a -> b) -> a -> b
$ b b
a' b b -> d b -> (:*:) b d b
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: d b
c'
  {-# INLINE gtoCon #-}

instance
  (GToCon arity a b, GToCon arity c d) =>
  GToCon arity (a :+: c) (b :+: d)
  where
  gtoCon :: forall a b.
ToConArgs arity a b -> (:+:) a c a -> Maybe ((:+:) b d b)
gtoCon ToConArgs 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) -> Maybe (b b) -> Maybe ((:+:) b d b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ToConArgs arity a b -> a a -> Maybe (b b)
forall a b. ToConArgs arity a b -> a a -> Maybe (b b)
forall arity (f1 :: * -> *) (f2 :: * -> *) a b.
GToCon arity f1 f2 =>
ToConArgs arity a b -> f1 a -> Maybe (f2 b)
gtoCon ToConArgs arity a b
args a a
a
  gtoCon ToConArgs arity a b
args (R1 c a
a) = d b -> (:+:) b d b
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (d b -> (:+:) b d b) -> Maybe (d b) -> Maybe ((:+:) b d b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ToConArgs arity a b -> c a -> Maybe (d b)
forall a b. ToConArgs arity a b -> c a -> Maybe (d b)
forall arity (f1 :: * -> *) (f2 :: * -> *) a b.
GToCon arity f1 f2 =>
ToConArgs arity a b -> f1 a -> Maybe (f2 b)
gtoCon ToConArgs arity a b
args c a
a
  {-# INLINE gtoCon #-}

instance (GToCon arity a b) => GToCon arity (M1 i c1 a) (M1 i c2 b) where
  gtoCon :: forall a b.
ToConArgs arity a b -> M1 i c1 a a -> Maybe (M1 i c2 b b)
gtoCon ToConArgs arity a b
args (M1 a a
a) = b b -> M1 i c2 b b
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (b b -> M1 i c2 b b) -> Maybe (b b) -> Maybe (M1 i c2 b b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ToConArgs arity a b -> a a -> Maybe (b b)
forall a b. ToConArgs arity a b -> a a -> Maybe (b b)
forall arity (f1 :: * -> *) (f2 :: * -> *) a b.
GToCon arity f1 f2 =>
ToConArgs arity a b -> f1 a -> Maybe (f2 b)
gtoCon ToConArgs arity a b
args a a
a
  {-# INLINE gtoCon #-}

instance (ToCon a b) => GToCon arity (K1 i a) (K1 i b) where
  gtoCon :: forall a b. ToConArgs arity a b -> K1 i a a -> Maybe (K1 i b b)
gtoCon ToConArgs 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) -> Maybe b -> Maybe (K1 i b b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> Maybe b
forall a b. ToCon a b => a -> Maybe b
toCon a
a
  {-# INLINE gtoCon #-}

instance GToCon Arity1 Par1 Par1 where
  gtoCon :: forall a b. ToConArgs Arity1 a b -> Par1 a -> Maybe (Par1 b)
gtoCon (ToConArgs1 a -> Maybe b
f) (Par1 a
a) = b -> Par1 b
forall p. p -> Par1 p
Par1 (b -> Par1 b) -> Maybe b -> Maybe (Par1 b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> Maybe b
f a
a
  {-# INLINE gtoCon #-}

instance (ToCon1 f1 f2) => GToCon Arity1 (Rec1 f1) (Rec1 f2) where
  gtoCon :: forall a b. ToConArgs Arity1 a b -> Rec1 f1 a -> Maybe (Rec1 f2 b)
gtoCon (ToConArgs1 a -> Maybe 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) -> Maybe (f2 b) -> Maybe (Rec1 f2 b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> Maybe b) -> f1 a -> Maybe (f2 b)
forall a b. (a -> Maybe b) -> f1 a -> Maybe (f2 b)
forall (f1 :: * -> *) (f2 :: * -> *) a b.
ToCon1 f1 f2 =>
(a -> Maybe b) -> f1 a -> Maybe (f2 b)
liftToCon a -> Maybe b
f f1 a
a
  {-# INLINE gtoCon #-}

instance
  (ToCon1 f1 f2, GToCon Arity1 g1 g2) =>
  GToCon Arity1 (f1 :.: g1) (f2 :.: g2)
  where
  gtoCon :: forall a b.
ToConArgs Arity1 a b -> (:.:) f1 g1 a -> Maybe ((:.:) f2 g2 b)
gtoCon ToConArgs Arity1 a b
targs (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)
-> Maybe (f2 (g2 b)) -> Maybe ((:.:) f2 g2 b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (g1 a -> Maybe (g2 b)) -> f1 (g1 a) -> Maybe (f2 (g2 b))
forall a b. (a -> Maybe b) -> f1 a -> Maybe (f2 b)
forall (f1 :: * -> *) (f2 :: * -> *) a b.
ToCon1 f1 f2 =>
(a -> Maybe b) -> f1 a -> Maybe (f2 b)
liftToCon (ToConArgs Arity1 a b -> g1 a -> Maybe (g2 b)
forall a b. ToConArgs Arity1 a b -> g1 a -> Maybe (g2 b)
forall arity (f1 :: * -> *) (f2 :: * -> *) a b.
GToCon arity f1 f2 =>
ToConArgs arity a b -> f1 a -> Maybe (f2 b)
gtoCon ToConArgs Arity1 a b
targs) f1 (g1 a)
a
  {-# INLINE gtoCon #-}

-- | Generic 'toCon' function.
genericToCon ::
  (Generic a, Generic b, GToCon Arity0 (Rep a) (Rep b)) =>
  a ->
  Maybe b
genericToCon :: forall a b.
(Generic a, Generic b, GToCon Arity0 (Rep a) (Rep b)) =>
a -> Maybe b
genericToCon = (Rep b Any -> b) -> Maybe (Rep b Any) -> Maybe b
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Rep b Any -> b
forall a x. Generic a => Rep a x -> a
forall x. Rep b x -> b
to (Maybe (Rep b Any) -> Maybe b)
-> (a -> Maybe (Rep b Any)) -> a -> Maybe b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ToConArgs Arity0 Any Any -> Rep a Any -> Maybe (Rep b Any)
forall a b. ToConArgs Arity0 a b -> Rep a a -> Maybe (Rep b b)
forall arity (f1 :: * -> *) (f2 :: * -> *) a b.
GToCon arity f1 f2 =>
ToConArgs arity a b -> f1 a -> Maybe (f2 b)
gtoCon ToConArgs Arity0 Any Any
forall _ _. ToConArgs Arity0 _ _
ToConArgs0 (Rep a Any -> Maybe (Rep b Any))
-> (a -> Rep a Any) -> a -> Maybe (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 genericToCon #-}

-- | Generic 'liftToCon' function.
genericLiftToCon ::
  (Generic1 f1, Generic1 f2, GToCon Arity1 (Rep1 f1) (Rep1 f2)) =>
  (a -> Maybe b) ->
  f1 a ->
  Maybe (f2 b)
genericLiftToCon :: forall (f1 :: * -> *) (f2 :: * -> *) a b.
(Generic1 f1, Generic1 f2, GToCon Arity1 (Rep1 f1) (Rep1 f2)) =>
(a -> Maybe b) -> f1 a -> Maybe (f2 b)
genericLiftToCon a -> Maybe b
f = (Rep1 f2 b -> f2 b) -> Maybe (Rep1 f2 b) -> Maybe (f2 b)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap 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 (Maybe (Rep1 f2 b) -> Maybe (f2 b))
-> (f1 a -> Maybe (Rep1 f2 b)) -> f1 a -> Maybe (f2 b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ToConArgs Arity1 a b -> Rep1 f1 a -> Maybe (Rep1 f2 b)
forall a b. ToConArgs Arity1 a b -> Rep1 f1 a -> Maybe (Rep1 f2 b)
forall arity (f1 :: * -> *) (f2 :: * -> *) a b.
GToCon arity f1 f2 =>
ToConArgs arity a b -> f1 a -> Maybe (f2 b)
gtoCon ((a -> Maybe b) -> ToConArgs Arity1 a b
forall a b. (a -> Maybe b) -> ToConArgs Arity1 a b
ToConArgs1 a -> Maybe b
f) (Rep1 f1 a -> Maybe (Rep1 f2 b))
-> (f1 a -> Rep1 f1 a) -> f1 a -> Maybe (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 genericLiftToCon #-}

instance
  (Generic a, Generic b, GToCon Arity0 (Rep a) (Rep b)) =>
  ToCon a (Default b)
  where
  toCon :: a -> Maybe (Default b)
toCon = (b -> Default b) -> Maybe b -> Maybe (Default b)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> Default b
forall a. a -> Default a
Default (Maybe b -> Maybe (Default b))
-> (a -> Maybe b) -> a -> Maybe (Default b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe b
forall a b.
(Generic a, Generic b, GToCon Arity0 (Rep a) (Rep b)) =>
a -> Maybe b
genericToCon
  {-# INLINE toCon #-}

instance
  (Generic1 f1, Generic1 f2, GToCon Arity1 (Rep1 f1) (Rep1 f2), ToCon a b) =>
  ToCon (f1 a) (Default1 f2 b)
  where
  toCon :: f1 a -> Maybe (Default1 f2 b)
toCon = f1 a -> Maybe (Default1 f2 b)
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(ToCon1 f1 f2, ToCon a b) =>
f1 a -> Maybe (f2 b)
toCon1

instance
  (Generic1 f1, Generic1 f2, GToCon Arity1 (Rep1 f1) (Rep1 f2)) =>
  ToCon1 f1 (Default1 f2)
  where
  liftToCon :: forall a b. (a -> Maybe b) -> f1 a -> Maybe (Default1 f2 b)
liftToCon a -> Maybe b
f = (f2 b -> Default1 f2 b) -> Maybe (f2 b) -> Maybe (Default1 f2 b)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f2 b -> Default1 f2 b
forall (f :: * -> *) a. f a -> Default1 f a
Default1 (Maybe (f2 b) -> Maybe (Default1 f2 b))
-> (f1 a -> Maybe (f2 b)) -> f1 a -> Maybe (Default1 f2 b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Maybe b) -> f1 a -> Maybe (f2 b)
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(Generic1 f1, Generic1 f2, GToCon Arity1 (Rep1 f1) (Rep1 f2)) =>
(a -> Maybe b) -> f1 a -> Maybe (f2 b)
genericLiftToCon a -> Maybe b
f
  {-# INLINE liftToCon #-}

instance ToCon SymBool Bool where
  toCon :: SymBool -> Maybe Bool
toCon = SymBool -> Maybe Bool
forall c t. Solvable c t => t -> Maybe c
conView