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

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

module Lorentz.UParam
  ( UParam (..)
  , EntrypointKind
  , type (?:)

    -- * Construction
  , mkUParam

    -- * Deconstruction
  , ConstrainedSome (..)
  , UnpackUParam
  , unpackUParam

    -- * Casting to homomorphic value
  , SomeInterface
  , UParam_

    -- * Pattern-matching
  , EntrypointsImpl
  , UParamFallback
  , EntrypointLookupError (..)
  , CaseUParam
  , caseUParam
  , caseUParamT
  , uparamFallbackFail

    -- * Constraints
  , LookupEntrypoint
  , RequireUniqueEntrypoints

    -- * Conversion from ADT
  , uparamFromAdt
  , UParamLinearize
  , UParamLinearized

    -- * Documentation
  , pbsUParam

    -- * Internals used for entrypoint-wise migrations
  , unwrapUParam
  ) where

import Data.Constraint ((\\))
import qualified Data.Kind as Kind
import qualified Fcf
import Fmt (Buildable(..))
import GHC.Generics ((:*:)(..), (:+:)(..))
import qualified GHC.Generics as G
import qualified Text.Show

import Lorentz.ADT
import Lorentz.Annotation (HasAnnotation)
import Lorentz.Base
import Lorentz.Coercions
import Lorentz.Constraints
import Lorentz.Entrypoints.Doc
import Lorentz.Errors
import Lorentz.Instr as L
import Lorentz.Macro
import Lorentz.Pack
import Michelson.Text
import Michelson.Typed
import Util.Label (Label)
import Util.Markdown
import Util.Type
import Util.TypeLits
import Util.TypeTuple

-- | An entrypoint is described by two types: its name and type of argument.
type EntrypointKind = (Symbol, Kind.Type)

-- | A convenient alias for type-level name-something pair.
type (n :: Symbol) ?: (a :: k) = '(n, a)

-- | Encapsulates parameter for one of entry points.
-- It keeps entrypoint name and corresponding argument serialized.
--
-- In Haskell world, we keep an invariant of that contained value relates
-- to one of entry points from @entries@ list.
newtype UParam (entries :: [EntrypointKind]) = UParamUnsafe (MText, ByteString)
  deriving stock (Generic, Eq, Show)
  deriving anyclass (IsoValue, HasAnnotation, Wrappable)

-- Casting to homomorphic value
----------------------------------------------------------------------------

-- | Pseudo value for 'UParam' type variable.
type SomeInterface = '[ '("SomeEntrypoints", Void) ]

-- | Homomorphic version of 'UParam', forgets the exact interface.
type UParam_ = UParam SomeInterface

-- | Allows casts only between 'UParam_' and 'UParam'.
instance SameEntries entries1 entries2 =>
         UParam entries1 `CanCastTo` UParam entries2

type family SameEntries (es1 :: [EntrypointKind]) (es :: [EntrypointKind])
              :: Constraint where
  SameEntries e e = ()
  SameEntries SomeInterface _ = ()
  SameEntries _ SomeInterface = ()
  SameEntries e1 e2 = (e1 ~ e2)

----------------------------------------------------------------------------
-- Common type-level stuff
----------------------------------------------------------------------------

-- | Get type of entrypoint argument by its name.
type family LookupEntrypoint (name :: Symbol) (entries :: [EntrypointKind])
             :: Kind.Type where
  LookupEntrypoint name ('(name, a) ': _) = a
  LookupEntrypoint name (_ ': entries) = LookupEntrypoint name entries
  LookupEntrypoint name '[] =
    TypeError ('Text "Entry point " ':<>: 'ShowType name ':<>:
               'Text " in not in the entry points list")

-- | Ensure that given entry points do no contain duplicated names.
type family RequireUniqueEntrypoints (entries :: [EntrypointKind])
             :: Constraint where
  RequireUniqueEntrypoints entries =
    RequireAllUnique "entrypoint" (Fcf.Eval (Fcf.Map Fcf.Fst entries))

----------------------------------------------------------------------------
-- Construction
----------------------------------------------------------------------------

-- | Construct a 'UParam' safely.
mkUParam
  :: ( NicePackedValue a
     , LookupEntrypoint name entries ~ a
     , RequireUniqueEntrypoints entries
     )
  => Label name -> a -> UParam entries
mkUParam label (a :: a) =
  UParamUnsafe (labelToMText label, lPackValue a)
    \\ nicePackedValueEvi @a

-- Example
----------------------------------------------------------------------------

type MyEntrypoints =
  [ "add" ?: Integer
  , "reset" ?: ()
  ]

_mkParamSample1 :: UParam MyEntrypoints
_mkParamSample1 = mkUParam #add 5

----------------------------------------------------------------------------
-- Deconstruction
----------------------------------------------------------------------------

-- | This type can store any value that satisfies a certain constraint.
data ConstrainedSome (c :: Kind.Type -> Constraint) where
  ConstrainedSome :: c a => a -> ConstrainedSome c

instance Show (ConstrainedSome Show) where
  show (ConstrainedSome a) = show a

instance Buildable (ConstrainedSome Buildable) where
  build (ConstrainedSome a) = build a

-- | This class is needed to implement `unpackUParam`.
class UnpackUParam (c :: Kind.Type -> Constraint) entries where
  -- | Turn 'UParam' into a Haskell value.
  -- Since we don't know its type in compile time, we have to erase it using
  -- 'ConstrainedSome'. The user of this function can require arbitrary
  -- constraint to hold (depending on how they want to use the result).
  unpackUParam ::
    UParam entries -> Either EntrypointLookupError (MText, ConstrainedSome c)

instance UnpackUParam c '[] where
  unpackUParam (UParamUnsafe (name, _)) = Left (NoSuchEntrypoint name)

instance
  ( KnownSymbol name
  , UnpackUParam c entries
  , NiceUnpackedValue arg
  , c arg
  ) => UnpackUParam c ((name ?: arg) ': entries) where
  unpackUParam (UParamUnsafe (name, bytes))
    | name == symbolToMText @name =
      fmap (name,) .
      first (const ArgumentUnpackFailed) .
      fmap ConstrainedSome .
      lUnpackValue @arg $
      bytes
    | otherwise = unpackUParam @c @entries (UParamUnsafe (name, bytes))

----------------------------------------------------------------------------
-- Pattern-matching
----------------------------------------------------------------------------

-- | Helper instruction which extracts content of 'UParam'.
unwrapUParam :: UParam entries : s :-> (MText, ByteString) : s
unwrapUParam = coerceUnwrap

-- | Wrapper for a single "case" branch.
data CaseClauseU inp out (entry :: EntrypointKind) where
  CaseClauseU :: (arg : inp) :-> out -> CaseClauseU inp out '(name, arg)

instance (name ~ name', body ~ ((arg : inp) :-> out)) =>
         CaseArrow name' body (CaseClauseU inp out '(name, arg)) where
  (/->) _ = CaseClauseU

data EntrypointLookupError
  = NoSuchEntrypoint MText
  | ArgumentUnpackFailed
  deriving stock (Generic, Eq, Show)

instance Buildable EntrypointLookupError where
  build =
    \case
      NoSuchEntrypoint name -> "No such entrypoint: " <> build name
      ArgumentUnpackFailed -> "UNPACK failed"

type instance ErrorArg "uparamNoSuchEntrypoint" = MText
type instance ErrorArg "uparamArgumentUnpackFailed" = ()

instance Buildable (CustomError "uparamNoSuchEntrypoint") where
  build (CustomError _ name) = "No such entrypoint: " <> build name

instance Buildable (CustomError "uparamArgumentUnpackFailed") where
  build (CustomError _ ()) = "UNPACK failed"

instance CustomErrorHasDoc "uparamNoSuchEntrypoint" where
  customErrClass = ErrClassBadArgument
  customErrDocMdCause = "Entrypoint with given name does not exist."

instance CustomErrorHasDoc "uparamArgumentUnpackFailed" where
  customErrClass = ErrClassBadArgument
  customErrDocMdCause = "Argument of wrong type is provided to the entrypoint."

-- | Implementations of some entry points.
--
-- Note that this thing inherits properties of 'Rec', e.g. you can
-- @Data.Vinyl.Core.rappend@ implementations for two entrypoint sets
-- when assembling scattered parts of a contract.
type EntrypointsImpl inp out entries =
  Rec (CaseClauseU inp out) entries

-- | An action invoked when user-provided entrypoint is not found.
type UParamFallback inp out = ((MText, ByteString) : inp) :-> out

-- | Default implementation for 'UParamFallback', simply reports an error.
uparamFallbackFail :: UParamFallback inp out
uparamFallbackFail =
  car # failCustom #uparamNoSuchEntrypoint

-- | Make up a "case" over entry points.
class CaseUParam (entries :: [EntrypointKind]) where
  -- | Pattern-match on given @UParam entries@.
  --
  -- You have to provide all case branches and a fallback action on case
  -- when entrypoint is not found.
  --
  -- This function is unsafe because it does not make sure at type-level
  -- that entry points' names do not repeat.
  caseUParamUnsafe
    :: Rec (CaseClauseU inp out) entries
    -> UParamFallback inp out
    -> (UParam entries : inp) :-> out

instance CaseUParam '[] where
  caseUParamUnsafe RNil fallback = unwrapUParam # fallback

instance ( KnownSymbol name
         , CaseUParam entries
         , NiceUnpackedValue arg
         ) =>
         CaseUParam ((name ?: arg) ': entries) where
  caseUParamUnsafe (CaseClauseU clause :& clauses) fallback =
    dup # unwrapUParam # car #
    push (mkMTextUnsafe $ symbolValT' @name) # eq #
    if_ (unwrapUParam # cdr # unpack #
         ifSome nop (failCustom_ #uparamArgumentUnpackFailed) # clause)
        (cutUParamEntry # caseUParamUnsafe clauses fallback)
    where
      cutUParamEntry :: UParam (e : es) : s :-> UParam es : s
      cutUParamEntry = forcedCoerce_

-- | Pattern-match on given @UParam entries@.
--
-- You have to provide all case branches and a fallback action on case
-- when entrypoint is not found.
caseUParam
  :: (CaseUParam entries, RequireUniqueEntrypoints entries)
  => Rec (CaseClauseU inp out) entries
  -> UParamFallback inp out
  -> (UParam entries : inp) :-> out
caseUParam = caseUParamUnsafe

-- | Like 'caseUParam', but accepts a tuple of clauses, not a 'Rec'.
caseUParamT
  :: forall entries inp out clauses.
     ( clauses ~ Rec (CaseClauseU inp out) entries
     , RecFromTuple clauses
     , CaseUParam entries
     )
  => IsoRecTuple clauses
  -> UParamFallback inp out
  -> (UParam entries : inp) :-> out
caseUParamT clauses fallback = caseUParamUnsafe (recFromTuple clauses) fallback

-- Example
----------------------------------------------------------------------------

_caseSample :: UParam MyEntrypoints : s :-> Integer : s
_caseSample = caseUParamT
  ( #add /-> nop
  , #reset /-> L.drop @() # push 0
  ) uparamFallbackFail

----------------------------------------------------------------------------
-- ADT conversion
----------------------------------------------------------------------------

{- @martoon: I actually hope no one will use this capability,
   it's here primarily because in other places we also use Generic stuff.

   Representation with type-level list and a datatype made polymorhpic over
   it seems more powerful than Generics.
   1. It's simpler to implement features for it. No extra boilerplate.
   2. 'Data.Vinyl' provides many useful utilities to work with such things.
   3. You are not such constrained in selecting names of entry points as when
      they come from constructor names.
-}

-- | Make up 'UParam' from ADT sum.
--
-- Entry points template will consist of
-- @(constructorName, constructorFieldType)@ pairs.
-- Each constructor is expected to have exactly one field.
uparamFromAdt
  :: UParamLinearize up
  => up -> UParam (UParamLinearized up)
uparamFromAdt = adtToRec . G.from

-- | Constraint required by 'uparamFromAdt'.
type UParamLinearize p = (Generic p, GUParamLinearize (G.Rep p))

-- | Entry points template derived from given ADT sum.
type UParamLinearized p = GUParamLinearized (G.Rep p)

-- | Generic traversal for conversion between ADT sum and 'UParam'.
class GUParamLinearize (x :: Kind.Type -> Kind.Type) where
  type GUParamLinearized x :: [(Symbol, Kind.Type)]
  adtToRec :: x p -> UParam (GUParamLinearized x)

instance GUParamLinearize x => GUParamLinearize (G.D1 i x) where
  type GUParamLinearized (G.D1 i x) = GUParamLinearized x
  adtToRec = adtToRec . G.unM1

instance (GUParamLinearize x, GUParamLinearize y) => GUParamLinearize (x :+: y) where
  type GUParamLinearized (x :+: y) = GUParamLinearized x ++ GUParamLinearized y
  adtToRec = \case
    G.L1 x -> let UParamUnsafe up = adtToRec x in UParamUnsafe up
    G.R1 y -> let UParamUnsafe up = adtToRec y in UParamUnsafe up

instance (KnownSymbol name, NicePackedValue a) =>
         GUParamLinearize (G.C1 ('G.MetaCons name _1 _2) (G.S1 si (G.Rec0 a))) where
  type GUParamLinearized (G.C1 ('G.MetaCons name _1 _2) (G.S1 si (G.Rec0 a))) =
    '[ '(name, a) ]

  adtToRec (G.M1 (G.M1 (G.K1 a))) = UParamUnsafe
    ( symbolToMText @name
    , lPackValue a
    )

instance
    TypeError ('Text "UParam linearization requires exactly one field \
                    \in each constructor") =>
    GUParamLinearize (G.C1 i G.U1) where
  type GUParamLinearized (G.C1 i G.U1) =
    TypeError ('Text "Bad linearized ADT")
  adtToRec = error "impossible"

instance
    TypeError ('Text "UParam linearization requires exactly one field \
                    \in each constructor") =>
    GUParamLinearize (G.C1 i (x :*: y)) where
  type GUParamLinearized (G.C1 i (x :*: y)) =
    TypeError ('Text "Bad linearized ADT")
  adtToRec = error "impossible"

----------------------------------------------------------------------------
-- Documentation
----------------------------------------------------------------------------

instance Typeable interface => TypeHasDoc (UParam interface) where
  typeDocName _ = "Upgradable parameter"
  typeDocMdReference p = customTypeDocMdReference ("UParam", DType p) []
  typeDocMdDescription =
    "This type encapsulates parameter for one of entry points. \
    \It keeps entry point name and corresponding argument serialized."
  typeDocHaskellRep = homomorphicTypeDocHaskellRep
  typeDocMichelsonRep = homomorphicTypeDocMichelsonRep

-- | Note that calling given entrypoints involves constructing 'UParam'.
pbsUParam :: forall ctorName. KnownSymbol ctorName => ParamBuildingStep
pbsUParam =
  let ctor = build $ symbolValT' @ctorName
  in PbsCustom ParamBuildingDesc
      { pbdEnglish =
          "Wrap into *UParam* as " <> mdTicked ctor <> " entrypoint."
      , pbdHaskell = ParamBuilder $
          \a -> "mkUParam #" <> ctor <> " (" <> a <> ")"
      , pbdMichelson = ParamBuilder $
          \a -> "Pair \"" <> ctor <> "\" (pack (" <> a <> "))"
      }