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

-- | Some derivative constraints.
--
-- They are moved to separate module because they need to lie quite high in
-- modules dependencies graph (unlike "Lorentz.Constraints.Scopes").
module Lorentz.Constraints.Derivative
  ( NiceParameterFull
  , DupableDecision (..)
  , decideOnDupable
  , NiceViews
  , NiceViewsDescriptor
  ) where

import Lorentz.Constraints.Scopes
import Lorentz.Entrypoints.Core
import Lorentz.ViewBase
import Morley.Michelson.Typed.Haskell.Value
import Morley.Michelson.Typed.Scope
import Morley.Util.Type

-- | Constraint applied to a whole parameter type.
type NiceParameterFull cp = (Typeable cp, ParameterDeclaresEntrypoints cp)

-- | Tells whether given type is dupable or not.
data DupableDecision a
  = Dupable a => IsDupable
  | IsNotDupable

-- | Check whether given value is dupable, returning a proof of that when it is.
--
-- This lets defining methods that behave differently depending on whether given
-- value is dupable or not. This may be suitable when for the dupable case you
-- can provide a more efficient implementation, but you also want your
-- implementation to be generic.
--
-- Example:
--
-- @
-- code = case decideOnDupable @a of
--   IsDupable -> do dup; ...
--   IsNotDupable -> ...
-- @
--
decideOnDupable
  :: forall a. (KnownValue a) => DupableDecision a
decideOnDupable :: forall a. KnownValue a => DupableDecision a
decideOnDupable =
  case forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(DupableScope (ToT a)) of
    Right Dict (DupableScope (ToT a))
Dict -> DupableDecision a
forall a. Dupable a => DupableDecision a
IsDupable
    Left BadTypeForScope
_ -> DupableDecision a
forall a. DupableDecision a
IsNotDupable

-- | Require views set to be proper.
type NiceViews vs = RequireAllUnique "view" (ViewsNames vs)

-- | Require views set referred by the given views descriptor to be proper.
type NiceViewsDescriptor vd = NiceViews (RevealViews vd)