-- SPDX-FileCopyrightText: 2020 Tocqueville Group
--
-- SPDX-License-Identifier: LicenseRef-MIT-TQ

{-# OPTIONS_GHC -Wno-redundant-constraints #-}

-- | Representation of Haskell sum types via loosy typed Michelson values,
-- useful for e.g. errors and enums.
--
-- In particular, ADT sum can be represented as constructor name + data
-- it carries. Such expression does not have particular type because
-- different constructors may carry different data, and we avoid lifting
-- this data to a union in order to keep only the significant parts
-- (and thus not to confuse the client).
module Michelson.Typed.Haskell.LooseSum
  ( ComposeResult (..)
  , fromTaggedVal
  , toTaggedVal
  , LooseSumC
  ) where

import Data.Singletons
import GHC.Generics ((:*:), (:+:))
import qualified GHC.Generics as G

import Michelson.Typed.Aliases
import Michelson.Typed.Existential
import Michelson.Typed.Haskell.Value
import Michelson.Typed.T
import Util.Sing (castSing)
import Util.TypeLits

-- | Possible outcomes of an attempt to construct a Haskell ADT value
-- from constructor name and relevant data.
data ComposeResult a
  = ComposeOk a
    -- ^ Composed fine.
  | ComposeCtorNotFound
    -- ^ No constructor with such name.
  | ComposeFieldTypeMismatch T T
    -- ^ Found required constructor, but type of data does not correspond
    -- to provided one.
  deriving stock (a -> ComposeResult b -> ComposeResult a
(a -> b) -> ComposeResult a -> ComposeResult b
(forall a b. (a -> b) -> ComposeResult a -> ComposeResult b)
-> (forall a b. a -> ComposeResult b -> ComposeResult a)
-> Functor ComposeResult
forall a b. a -> ComposeResult b -> ComposeResult a
forall a b. (a -> b) -> ComposeResult a -> ComposeResult b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> ComposeResult b -> ComposeResult a
$c<$ :: forall a b. a -> ComposeResult b -> ComposeResult a
fmap :: (a -> b) -> ComposeResult a -> ComposeResult b
$cfmap :: forall a b. (a -> b) -> ComposeResult a -> ComposeResult b
Functor)

instance Semigroup (ComposeResult a) where
  r :: ComposeResult a
r@(ComposeOk a
_) <> :: ComposeResult a -> ComposeResult a -> ComposeResult a
<> ComposeResult a
_ = ComposeResult a
r
  ComposeResult a
_ <> r :: ComposeResult a
r@(ComposeOk a
_) = ComposeResult a
r
  r :: ComposeResult a
r@(ComposeFieldTypeMismatch T
_ T
_) <> ComposeResult a
_ = ComposeResult a
r
  ComposeResult a
_ <> r :: ComposeResult a
r@(ComposeFieldTypeMismatch T
_ T
_) = ComposeResult a
r
  r :: ComposeResult a
r@ComposeResult a
ComposeCtorNotFound <> ComposeResult a
ComposeCtorNotFound = ComposeResult a
r

instance Monoid (ComposeResult a) where
  mempty :: ComposeResult a
mempty = ComposeResult a
forall a. ComposeResult a
ComposeCtorNotFound
  mappend :: ComposeResult a -> ComposeResult a -> ComposeResult a
mappend = ComposeResult a -> ComposeResult a -> ComposeResult a
forall a. Semigroup a => a -> a -> a
(<>)

-- | Constraint for 'hsDecompose' and 'hsCompose'.
type LooseSumC dt =
  ( Generic dt, GLooseSum (G.Rep dt)
  )

-- | Decompose Haskell type into constructor name and
-- data it carries, converting the latter into Michelson 'Value'.
toTaggedVal :: LooseSumC dt => dt -> (Text, SomeValue)
toTaggedVal :: dt -> (Text, SomeValue)
toTaggedVal = Rep dt Any -> (Text, SomeValue)
forall (x :: * -> *) p. GLooseSum x => x p -> (Text, SomeValue)
gToTaggedVal (Rep dt Any -> (Text, SomeValue))
-> (dt -> Rep dt Any) -> dt -> (Text, SomeValue)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. dt -> Rep dt Any
forall a x. Generic a => a -> Rep a x
G.from

-- | Inverse to 'toTaggedVal'.
fromTaggedVal :: LooseSumC dt => (Text, SomeValue) -> ComposeResult dt
fromTaggedVal :: (Text, SomeValue) -> ComposeResult dt
fromTaggedVal = (Rep dt Any -> dt)
-> ComposeResult (Rep dt Any) -> ComposeResult dt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Rep dt Any -> dt
forall a x. Generic a => Rep a x -> a
G.to (ComposeResult (Rep dt Any) -> ComposeResult dt)
-> ((Text, SomeValue) -> ComposeResult (Rep dt Any))
-> (Text, SomeValue)
-> ComposeResult dt
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text, SomeValue) -> ComposeResult (Rep dt Any)
forall (x :: * -> *) p.
GLooseSum x =>
(Text, SomeValue) -> ComposeResult (x p)
gFromTaggedVal

-- | Generic traversal for 'toTaggedVal' and 'fromTaggedVal'.
class GLooseSum (x :: Type -> Type) where
  gToTaggedVal :: x p -> (Text, SomeValue)
  gFromTaggedVal :: (Text, SomeValue) -> ComposeResult (x p)

instance GLooseSum x => GLooseSum (G.D1 i x) where
  gToTaggedVal :: D1 i x p -> (Text, SomeValue)
gToTaggedVal = x p -> (Text, SomeValue)
forall (x :: * -> *) p. GLooseSum x => x p -> (Text, SomeValue)
gToTaggedVal (x p -> (Text, SomeValue))
-> (D1 i x p -> x p) -> D1 i x p -> (Text, SomeValue)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. D1 i x p -> x p
forall i (c :: Meta) k (f :: k -> *) (p :: k). M1 i c f p -> f p
G.unM1
  gFromTaggedVal :: (Text, SomeValue) -> ComposeResult (D1 i x p)
gFromTaggedVal = (x p -> D1 i x p)
-> ComposeResult (x p) -> ComposeResult (D1 i x p)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap x p -> D1 i x p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (ComposeResult (x p) -> ComposeResult (D1 i x p))
-> ((Text, SomeValue) -> ComposeResult (x p))
-> (Text, SomeValue)
-> ComposeResult (D1 i x p)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text, SomeValue) -> ComposeResult (x p)
forall (x :: * -> *) p.
GLooseSum x =>
(Text, SomeValue) -> ComposeResult (x p)
gFromTaggedVal

instance (GLooseSum x, GLooseSum y) => GLooseSum (x :+: y) where
  gToTaggedVal :: (:+:) x y p -> (Text, SomeValue)
gToTaggedVal = \case
    G.L1 x p
x -> x p -> (Text, SomeValue)
forall (x :: * -> *) p. GLooseSum x => x p -> (Text, SomeValue)
gToTaggedVal x p
x
    G.R1 y p
y -> y p -> (Text, SomeValue)
forall (x :: * -> *) p. GLooseSum x => x p -> (Text, SomeValue)
gToTaggedVal y p
y
  gFromTaggedVal :: (Text, SomeValue) -> ComposeResult ((:+:) x y p)
gFromTaggedVal (Text, SomeValue)
v = [ComposeResult ((:+:) x y p)] -> ComposeResult ((:+:) x y p)
forall a. Monoid a => [a] -> a
mconcat
    [ x p -> (:+:) x y p
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
G.L1 (x p -> (:+:) x y p)
-> ComposeResult (x p) -> ComposeResult ((:+:) x y p)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Text, SomeValue) -> ComposeResult (x p)
forall (x :: * -> *) p.
GLooseSum x =>
(Text, SomeValue) -> ComposeResult (x p)
gFromTaggedVal (Text, SomeValue)
v
    , y p -> (:+:) x y p
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
G.R1 (y p -> (:+:) x y p)
-> ComposeResult (y p) -> ComposeResult ((:+:) x y p)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Text, SomeValue) -> ComposeResult (y p)
forall (x :: * -> *) p.
GLooseSum x =>
(Text, SomeValue) -> ComposeResult (x p)
gFromTaggedVal (Text, SomeValue)
v
    ]

instance (GAccessField x, KnownSymbol ctor) =>
         GLooseSum (G.C1 ('G.MetaCons ctor f o) x) where
  gToTaggedVal :: C1 ('MetaCons ctor f o) x p -> (Text, SomeValue)
gToTaggedVal = (KnownSymbol ctor => Text
forall (s :: Symbol). KnownSymbol s => Text
symbolValT' @ctor, ) (SomeValue -> (Text, SomeValue))
-> (C1 ('MetaCons ctor f o) x p -> SomeValue)
-> C1 ('MetaCons ctor f o) x p
-> (Text, SomeValue)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall p. GAccessField x => x p -> SomeValue
forall (x :: * -> *) p. GAccessField x => x p -> SomeValue
gExtractField @x (x p -> SomeValue)
-> (C1 ('MetaCons ctor f o) x p -> x p)
-> C1 ('MetaCons ctor f o) x p
-> SomeValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. C1 ('MetaCons ctor f o) x p -> x p
forall i (c :: Meta) k (f :: k -> *) (p :: k). M1 i c f p -> f p
G.unM1
  gFromTaggedVal :: (Text, SomeValue) -> ComposeResult (C1 ('MetaCons ctor f o) x p)
gFromTaggedVal (Text
ctor, SomeValue
val)
    | KnownSymbol ctor => Text
forall (s :: Symbol). KnownSymbol s => Text
symbolValT' @ctor Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
ctor = x p -> C1 ('MetaCons ctor f o) x p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (x p -> C1 ('MetaCons ctor f o) x p)
-> ComposeResult (x p)
-> ComposeResult (C1 ('MetaCons ctor f o) x p)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SomeValue -> ComposeResult (x p)
forall (x :: * -> *) p.
GAccessField x =>
SomeValue -> ComposeResult (x p)
gMakeField @x SomeValue
val
    | Bool
otherwise = ComposeResult (C1 ('MetaCons ctor f o) x p)
forall a. ComposeResult a
ComposeCtorNotFound

instance GLooseSum G.V1 where
  gToTaggedVal :: V1 p -> (Text, SomeValue)
gToTaggedVal = \case{}
  gFromTaggedVal :: (Text, SomeValue) -> ComposeResult (V1 p)
gFromTaggedVal (Text, SomeValue)
_ = ComposeResult (V1 p)
forall a. Monoid a => a
mempty

-- | Pick a field from constructor with zero or one fields.
class GAccessField (x :: Type -> Type) where
  gExtractField :: x p -> SomeValue
  gMakeField :: SomeValue -> ComposeResult (x p)

instance GAccessField x => GAccessField (G.S1 i x) where
  gExtractField :: S1 i x p -> SomeValue
gExtractField = x p -> SomeValue
forall (x :: * -> *) p. GAccessField x => x p -> SomeValue
gExtractField (x p -> SomeValue) -> (S1 i x p -> x p) -> S1 i x p -> SomeValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. S1 i x p -> x p
forall i (c :: Meta) k (f :: k -> *) (p :: k). M1 i c f p -> f p
G.unM1
  gMakeField :: SomeValue -> ComposeResult (S1 i x p)
gMakeField SomeValue
v = x p -> S1 i x p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (x p -> S1 i x p)
-> ComposeResult (x p) -> ComposeResult (S1 i x p)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SomeValue -> ComposeResult (x p)
forall (x :: * -> *) p.
GAccessField x =>
SomeValue -> ComposeResult (x p)
gMakeField @x SomeValue
v

instance IsoValue a =>
         GAccessField (G.Rec0 a) where
  gExtractField :: Rec0 a p -> SomeValue
gExtractField = Value (ToT a) -> SomeValue
forall (t :: T). SingI t => Value t -> SomeValue
SomeValue (Value (ToT a) -> SomeValue)
-> (Rec0 a p -> Value (ToT a)) -> Rec0 a p -> SomeValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Value (ToT a)
forall a. IsoValue a => a -> Value (ToT a)
toVal (a -> Value (ToT a))
-> (Rec0 a p -> a) -> Rec0 a p -> Value (ToT a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec0 a p -> a
forall i c k (p :: k). K1 i c p -> c
G.unK1
  gMakeField :: SomeValue -> ComposeResult (Rec0 a p)
gMakeField (SomeValue Value t
v) = a -> Rec0 a p
forall k i c (p :: k). c -> K1 i c p
G.K1 (a -> Rec0 a p)
-> (Value (ToT a) -> a) -> Value (ToT a) -> Rec0 a p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value (ToT a) -> a
forall a. IsoValue a => Value (ToT a) -> a
fromVal (Value (ToT a) -> Rec0 a p)
-> ComposeResult (Value (ToT a)) -> ComposeResult (Rec0 a p)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Value t -> ComposeResult (Value (ToT a))
forall (a :: T) (b :: T).
(SingI a, SingI b) =>
Value a -> ComposeResult (Value b)
composeCast Value t
v

instance GAccessField G.U1 where
  gExtractField :: U1 p -> SomeValue
gExtractField U1 p
G.U1 = Value 'TUnit -> SomeValue
forall (t :: T). SingI t => Value t -> SomeValue
SomeValue (Value 'TUnit -> SomeValue) -> Value 'TUnit -> SomeValue
forall a b. (a -> b) -> a -> b
$ () -> Value (ToT ())
forall a. IsoValue a => a -> Value (ToT a)
toVal ()
  gMakeField :: SomeValue -> ComposeResult (U1 p)
gMakeField (SomeValue Value t
v) = U1 p
forall k (p :: k). U1 p
G.U1 U1 p -> ComposeResult (Value 'TUnit) -> ComposeResult (U1 p)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Value t -> ComposeResult (Value 'TUnit)
forall (a :: T) (b :: T).
(SingI a, SingI b) =>
Value a -> ComposeResult (Value b)
composeCast @_ @'TUnit Value t
v

composeCast :: forall a b. (SingI a, SingI b) => Value a -> ComposeResult (Value b)
composeCast :: Value a -> ComposeResult (Value b)
composeCast Value a
a =
  case Value a -> Maybe (Value b)
forall k (a :: k) (b :: k) (t :: k -> *).
(SingI a, SingI b, SDecide k) =>
t a -> Maybe (t b)
castSing Value a
a of
    Maybe (Value b)
Nothing -> T -> T -> ComposeResult (Value b)
forall a. T -> T -> ComposeResult a
ComposeFieldTypeMismatch ((SingKind T, SingI a) => Demote T
forall k (a :: k). (SingKind k, SingI a) => Demote k
demote @a) ((SingKind T, SingI b) => Demote T
forall k (a :: k). (SingKind k, SingI a) => Demote k
demote @b)
    Just Value b
b -> Value b -> ComposeResult (Value b)
forall a. a -> ComposeResult a
ComposeOk Value b
b

instance
  TypeError ('Text "Cannot compose/decompose constructors with more \
             \than one field" ':$$:
             'Text "Consider using tuple instead") =>
  GAccessField (x :*: y) where
  gExtractField :: (:*:) x y p -> SomeValue
gExtractField = Text -> (:*:) x y p -> SomeValue
forall a. HasCallStack => Text -> a
error Text
"impossible"
  gMakeField :: SomeValue -> ComposeResult ((:*:) x y p)
gMakeField = Text -> SomeValue -> ComposeResult ((:*:) x y p)
forall a. HasCallStack => Text -> a
error Text
"impossible"