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

-- | 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
  ) where

import Lorentz.Constraints.Scopes
import Lorentz.Entrypoints.Core
import Michelson.Typed.Haskell.Value
import Michelson.Typed.Scope

-- | 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 =
  case checkScope @(DupableScope (ToT a)) of
    Right Dict -> IsDupable
    Left _ -> IsNotDupable