-- 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.Generic
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 (Show, Functor)

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

instance Monoid (ComposeResult a) where
  mempty = ComposeCtorNotFound
  mappend = (<>)

-- | Constraint for 'toTaggedVal' and 'fromTaggedVal'.
type LooseSumC dt =
  ( NiceGeneric dt, GLooseSum (GRep dt)
  )

{- | Decompose Haskell type into constructor name and
data it carries, converting the latter into Michelson 'Value'.

>>> toTaggedVal $ Just ()
("Just",Constrained VUnit)

A custom TypeError is generated if a type doesn't have a 'Generic' instance

>>> data Foo = Foo ()
>>> toTaggedVal $ Foo ()
...
... GHC.Generics.Rep Foo
... is stuck. Likely
... Generic Foo
... instance is missing or out of scope.
...
>>> data Foo = Foo () deriving Generic
>>> toTaggedVal $ Foo ()
("Foo",Constrained VUnit)
-}
toTaggedVal :: LooseSumC dt => dt -> (Text, SomeValue)
toTaggedVal = gToTaggedVal . G.from

{- | Inverse to 'toTaggedVal'.

>>> import Morley.Michelson.Typed

>>> fromTaggedVal @(Maybe ()) ("Just", SomeValue VUnit)
ComposeOk (Just ())

>>> data Foo = Foo () deriving Show
>>> fromTaggedVal @Foo ("Foo", SomeValue VUnit)
...
... GHC.Generics.Rep Foo
... is stuck. Likely
... Generic Foo
... instance is missing or out of scope.
...
>>> data Foo = Foo () deriving (Show, Generic)
>>> fromTaggedVal @Foo ("Foo", SomeValue VUnit)
ComposeOk (Foo ())
-}
fromTaggedVal :: LooseSumC dt => (Text, SomeValue) -> ComposeResult dt
fromTaggedVal = fmap G.to . 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 = gToTaggedVal . G.unM1
  gFromTaggedVal = fmap G.M1 . gFromTaggedVal

instance (GLooseSum x, GLooseSum y) => GLooseSum (x :+: y) where
  gToTaggedVal = \case
    G.L1 x -> gToTaggedVal x
    G.R1 y -> gToTaggedVal y
  gFromTaggedVal v = mconcat
    [ G.L1 <$> gFromTaggedVal v
    , G.R1 <$> gFromTaggedVal v
    ]

instance (GAccessField x, KnownSymbol ctor) =>
         GLooseSum (G.C1 ('G.MetaCons ctor f o) x) where
  gToTaggedVal = (symbolValT' @ctor, ) . gExtractField @x . G.unM1
  gFromTaggedVal (ctor, val)
    | symbolValT' @ctor == ctor = G.M1 <$> gMakeField @x val
    | otherwise = ComposeCtorNotFound

instance GLooseSum G.V1 where
  gToTaggedVal = \case{}
  gFromTaggedVal _ = 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 = gExtractField . G.unM1
  gMakeField v = G.M1 <$> gMakeField @x v

instance IsoValue a =>
         GAccessField (G.Rec0 a) where
  gExtractField = SomeValue . toVal . G.unK1
  gMakeField (SomeValue v) = G.K1 . fromVal <$> composeCast v

instance GAccessField G.U1 where
  gExtractField G.U1 = SomeValue $ toVal ()
  gMakeField (SomeValue v) = G.U1 <$ composeCast @_ @'TUnit v

composeCast :: forall a b. (SingI a, SingI b) => Value a -> ComposeResult (Value b)
composeCast a =
  case castSing a of
    Nothing -> ComposeFieldTypeMismatch (demote @a) (demote @b)
    Just b -> ComposeOk b

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