-- SPDX-FileCopyrightText: 2021 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

{-# 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 Morley.Michelson.Typed.Haskell.LooseSum
  ( ComposeResult (..)
  , fromTaggedVal
  , toTaggedVal
  , LooseSumC
  ) where

import Data.Constraint (Bottom(..))
import Data.Singletons (SingI(..), demote)
import GHC.Generics ((:*:), (:+:))
import GHC.Generics qualified as G

import Morley.Michelson.Typed.Aliases
import Morley.Michelson.Typed.Existential
import Morley.Michelson.Typed.Haskell.Value
import Morley.Michelson.Typed.T
import Morley.Util.Sing (castSing)
import Morley.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 ((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
<$ :: forall a b. a -> ComposeResult b -> ComposeResult a
$c<$ :: forall a b. a -> ComposeResult b -> ComposeResult a
fmap :: forall a b. (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 'toTaggedVal' and 'fromTaggedVal'.
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 :: forall dt. LooseSumC dt => 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 :: forall dt. LooseSumC dt => (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 :: forall p. 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))
-> (M1 D i x p -> x p) -> M1 D i x p -> (Text, SomeValue)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1 D i x p -> x p
forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
G.unM1
  gFromTaggedVal :: forall p. (Text, SomeValue) -> ComposeResult (D1 i x p)
gFromTaggedVal = (x p -> M1 D i x p)
-> ComposeResult (x p) -> ComposeResult (M1 D i x p)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap x p -> M1 D 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 (M1 D i x p))
-> ((Text, SomeValue) -> ComposeResult (x p))
-> (Text, SomeValue)
-> ComposeResult (M1 D 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 :: forall p. (:+:) 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 :: forall p. (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 :: forall p. C1 ('MetaCons ctor f o) x p -> (Text, SomeValue)
gToTaggedVal = (forall (s :: Symbol). KnownSymbol s => Text
symbolValT' @ctor, ) (SomeValue -> (Text, SomeValue))
-> (M1 C ('MetaCons ctor f o) x p -> SomeValue)
-> M1 C ('MetaCons ctor f o) x p
-> (Text, SomeValue)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (x :: * -> *) p. GAccessField x => x p -> SomeValue
gExtractField @x (x p -> SomeValue)
-> (M1 C ('MetaCons ctor f o) x p -> x p)
-> M1 C ('MetaCons ctor f o) x p
-> SomeValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1 C ('MetaCons ctor f o) x p -> x p
forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
G.unM1
  gFromTaggedVal :: forall p.
(Text, SomeValue) -> ComposeResult (C1 ('MetaCons ctor f o) x p)
gFromTaggedVal (Text
ctor, SomeValue
val)
    | forall (s :: Symbol). KnownSymbol s => Text
symbolValT' @ctor Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
ctor = x p -> M1 C ('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 -> M1 C ('MetaCons ctor f o) x p)
-> ComposeResult (x p)
-> ComposeResult (M1 C ('MetaCons ctor f o) x p)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (x :: * -> *) p.
GAccessField x =>
SomeValue -> ComposeResult (x p)
gMakeField @x SomeValue
val
    | Bool
otherwise = ComposeResult (M1 C ('MetaCons ctor f o) x p)
forall a. ComposeResult a
ComposeCtorNotFound

instance GLooseSum G.V1 where
  gToTaggedVal :: forall p. V1 p -> (Text, SomeValue)
gToTaggedVal = \case{}
  gFromTaggedVal :: forall p. (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 :: forall p. S1 i x p -> SomeValue
gExtractField = x p -> SomeValue
forall (x :: * -> *) p. GAccessField x => x p -> SomeValue
gExtractField (x p -> SomeValue)
-> (M1 S i x p -> x p) -> M1 S i x p -> SomeValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1 S i x p -> x p
forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
G.unM1
  gMakeField :: forall p. SomeValue -> ComposeResult (S1 i x p)
gMakeField SomeValue
v = x p -> M1 S i x p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (x p -> M1 S i x p)
-> ComposeResult (x p) -> ComposeResult (M1 S i x p)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (x :: * -> *) p.
GAccessField x =>
SomeValue -> ComposeResult (x p)
gMakeField @x SomeValue
v

instance IsoValue a =>
         GAccessField (G.Rec0 a) where
  gExtractField :: forall p. Rec0 a p -> SomeValue
gExtractField = Value (ToT a) -> SomeValue
forall (t :: T). SingI t => Value t -> SomeValue
SomeValue (Value (ToT a) -> SomeValue)
-> (K1 R a p -> Value (ToT a)) -> K1 R 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))
-> (K1 R a p -> a) -> K1 R a p -> Value (ToT a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. K1 R a p -> a
forall k i c (p :: k). K1 i c p -> c
G.unK1
  gMakeField :: forall p. SomeValue -> ComposeResult (Rec0 a p)
gMakeField (SomeValue Value t
v) = a -> K1 R a p
forall k i c (p :: k). c -> K1 i c p
G.K1 (a -> K1 R a p)
-> (Value (ToT a) -> a) -> Value (ToT a) -> K1 R 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) -> K1 R a p)
-> ComposeResult (Value (ToT a)) -> ComposeResult (K1 R 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 :: forall p. 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 :: forall p. 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
<$ 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 :: forall (a :: T) (b :: T).
(SingI a, SingI b) =>
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 (forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: T). (SingKind T, SingI a) => Demote T
demote @a) (forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: T). (SingKind T, SingI a) => Demote T
demote @b)
    Just Value b
b -> Value b -> ComposeResult (Value b)
forall a. a -> ComposeResult a
ComposeOk Value b
b

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