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

{-# OPTIONS_HADDOCK not-home #-}

module Morley.Michelson.Typed.Scope.Internal.Deprecated
  ( module Morley.Michelson.Typed.Scope.Internal.Deprecated
  ) where

import Data.Constraint (Dict(..), (\\))
import Data.Singletons (Sing, SingI(..))
import Data.Type.Bool (Not)
import Data.Type.Equality ((:~:)(..))

import Morley.Michelson.Typed.Scope.Internal.Comparable
import Morley.Michelson.Typed.Scope.Internal.ForbidT
import Morley.Michelson.Typed.Scope.Internal.Presence
import Morley.Michelson.Typed.Scope.Internal.WellTyped
import Morley.Michelson.Typed.Sing (SingT(..))
import Morley.Michelson.Typed.T (T(..))
import Morley.Util.StubbedProof (stubProof)

-- | Whether a value of this type _may_ contain an operation.
--
-- In some scopes (constants, parameters, storage) appearing for operation type
-- is prohibited.
-- Operations in input/output of lambdas are allowed without limits though.
type ContainsOp t = ContainsT 'PSOp t

-- | Whether a value of this type _may_ contain a @contract@ value.
--
-- In some scopes (constants, storage) appearing for contract type
-- is prohibited.
-- Contracts in input/output of lambdas are allowed without limits though.
type ContainsContract t = ContainsT 'PSContract t

-- | Whether a value of this type _may_ contain a @ticket@ value.
type ContainsTicket t = ContainsT 'PSTicket t

-- | Whether a value of this type _may_ contain a @big_map@ value.
type ContainsBigMap t = ContainsT 'PSBigMap t

-- | Whether a value of this type _may_ contain nested @big_map@s.
--
-- Nested big_maps (i.e. big_map which contains another big_map inside of it's value type) are
-- prohibited in all contexts. Some context such as PUSH, APPLY, PACK/UNPACK instructions are more
-- strict because they don't work with big_map at all.
type ContainsNestedBigMaps t = ContainsT 'PSNestedBigMaps t

-- | Whether a value of this type _may_ contain a @samping_state@ value.
type ContainsSaplingState t = ContainsT 'PSSaplingState t

{-# DEPRECATED
  ContainsOp
  , ContainsContract
  , ContainsTicket
  , ContainsBigMap
  , ContainsNestedBigMaps
  , ContainsSaplingState
  "Use 'ContainsT' with the corresponding type marker, e.g. \
  \'ContainsT PSOp', 'ContainsT PSTicket', etc"
  #-}


-- | Constraint which ensures that a value of type @t@ does not contain operations.
--
-- Not just a type alias in order to be able to partially apply it
-- (e.g. in 'Each').
class (ContainsOp t ~ 'False) => HasNoOp t
instance (ContainsOp t ~ 'False) => HasNoOp t

-- | Constraint which ensures that a value of type @t@ does not contain @contract@ values.
class (ContainsContract t ~ 'False) => HasNoContract t
instance (ContainsContract t ~ 'False) => HasNoContract t

-- | Constraint which ensures that a value of type @t@ does not contain @ticket@ values.
class (ContainsTicket t ~ 'False) => HasNoTicket t
instance (ContainsTicket t ~ 'False) => HasNoTicket t

-- | Constraint which ensures that a value of type @t@ does not contain @big_map@ values.
class (ContainsBigMap t ~ 'False) => HasNoBigMap t
instance (ContainsBigMap t ~ 'False) => HasNoBigMap t

-- | Constraint which ensures that a value of type @t@ does not contain @sapling_state@ values.
class (ContainsSaplingState t ~ 'False) => HasNoSaplingState t
instance (ContainsSaplingState t ~ 'False) => HasNoSaplingState t

-- | Constraint which ensures that there are no nested bigmaps.
class (ContainsNestedBigMaps t ~ 'False) => HasNoNestedBigMaps t
instance (ContainsNestedBigMaps t ~ 'False) => HasNoNestedBigMaps t

{-# DEPRECATED HasNoOp, HasNoContract, HasNoTicket, HasNoBigMap, HasNoSaplingState, HasNoNestedBigMaps
  "Use Forbid* instead" #-}


-- | Whether a value of this type _may_ contain an operation.
type OpPresence (t :: T) = TPresence 'PSOp t
pattern OpPresent :: () => ContainsOp t ~ 'True => OpPresence t
pattern OpPresent = TPresent
pattern OpAbsent :: () => ContainsOp t ~ 'False => OpPresence t
pattern OpAbsent = TAbsent
{-# COMPLETE OpPresent, OpAbsent #-}

-- | Whether a value of this type _may_ contain a @contract@ value.
type ContractPresence (t :: T) = TPresence 'PSContract t
pattern ContractPresent :: () => ContainsContract t ~ 'True => ContractPresence t
pattern ContractPresent = TPresent
pattern ContractAbsent :: () => ContainsContract t ~ 'False => ContractPresence t
pattern ContractAbsent = TAbsent
{-# COMPLETE ContractPresent, ContractAbsent #-}

-- | Whether a value of this type _may_ contain a @ticket@ value.
type TicketPresence (t :: T) = TPresence 'PSTicket t
pattern TicketPresent :: () => ContainsTicket t ~ 'True => TicketPresence t
pattern TicketPresent = TPresent
pattern TicketAbsent :: () => ContainsTicket t ~ 'False => TicketPresence t
pattern TicketAbsent = TAbsent
{-# COMPLETE TicketPresent, TicketAbsent #-}

-- | Whether a value of this type _may_ contain a @big_map@ value.
type BigMapPresence (t :: T) = TPresence 'PSBigMap t
pattern BigMapPresent :: () => ContainsBigMap t ~ 'True => BigMapPresence t
pattern BigMapPresent = TPresent
pattern BigMapAbsent :: () => ContainsBigMap t ~ 'False => BigMapPresence t
pattern BigMapAbsent = TAbsent
{-# COMPLETE BigMapPresent, BigMapAbsent #-}

-- | Whether a value of this type _may_ contain nested @big_map@s.
type NestedBigMapsPresence (t :: T) = TPresence 'PSNestedBigMaps t
pattern NestedBigMapsPresent :: () => ContainsNestedBigMaps t ~ 'True => NestedBigMapsPresence t
pattern NestedBigMapsPresent = TPresent
pattern NestedBigMapsAbsent :: () => ContainsNestedBigMaps t ~ 'False => NestedBigMapsPresence t
pattern NestedBigMapsAbsent = TAbsent
{-# COMPLETE NestedBigMapsPresent, NestedBigMapsAbsent #-}

-- | Whether a value of this type _may_ contain a @sapling_state@ value.
type SaplingStatePresence (t :: T) = TPresence 'PSSaplingState t
pattern SaplingStatePresent :: () => ContainsSaplingState t ~ 'True => SaplingStatePresence t
pattern SaplingStatePresent = TPresent
pattern SaplingStateAbsent :: () => ContainsSaplingState t ~ 'False => SaplingStatePresence t
pattern SaplingStateAbsent = TAbsent
{-# COMPLETE SaplingStatePresent, SaplingStateAbsent #-}

{-# DEPRECATED
  OpPresence, OpPresent, OpAbsent
  , ContractPresence, ContractPresent, ContractAbsent
  , TicketPresence, TicketPresent, TicketAbsent
  , BigMapPresence, BigMapPresent, BigMapAbsent
  , NestedBigMapsPresence, NestedBigMapsPresent, NestedBigMapsAbsent
  , SaplingStatePresence, SaplingStatePresent, SaplingStateAbsent
  "Use TPresence instead" #-}

type ProperParameterBetterErrors t =
  (SingI t, WellTyped t, ForbidOp t, ForbidNestedBigMaps t)

type ProperStorageBetterErrors t =
  (SingI t, WellTyped t, ForbidOp t, ForbidNestedBigMaps t, ForbidContract t)

type ProperConstantBetterErrors t =
  (SingI t, WellTyped t, ForbidOp t, ForbidBigMap t, ForbidContract t, ForbidTicket t, ForbidSaplingState t)

type ProperDupableBetterErrors t =
  (SingI t, ForbidTicket t)

type ProperPackedValBetterErrors t =
  (SingI t, WellTyped t, ForbidOp t, ForbidBigMap t, ForbidTicket t, ForbidSaplingState t)

type ProperUnpackedValBetterErrors t =
  (ProperPackedValBetterErrors t, ProperConstantBetterErrors t)

type ProperViewableBetterErrors t =
  (SingI t, ForbidOp t, ForbidBigMap t, ForbidTicket t)

type ProperUntypedValBetterErrors t =
  (SingI t, ForbidOp t)

type ProperNonComparableValBetterErrors t =
  (SingI t, ForbidNonComparable t)

{-# DEPRECATED ProperParameterBetterErrors
  , ProperStorageBetterErrors
  , ProperConstantBetterErrors
  , ProperDupableBetterErrors
  , ProperPackedValBetterErrors
  , ProperUnpackedValBetterErrors
  , ProperViewableBetterErrors
  , ProperUntypedValBetterErrors
  , ProperNonComparableValBetterErrors
  "Use *Scope instead"
  #-}

-- | Check at runtime whether a value of the given type _may_ contain an operation.
checkOpPresence :: Sing (ty :: T) -> TPresence 'PSOp ty
checkOpPresence = checkTPresence SPSOp

-- | Check at runtime whether a value of the given type _may_ contain a @contract@ value.
checkContractTypePresence :: Sing (ty :: T) -> TPresence 'PSContract ty
checkContractTypePresence = checkTPresence SPSContract

-- | Check at runtime whether a value of the given type _may_ contain a @ticket@ value.
checkTicketPresence :: Sing (ty :: T) -> TPresence 'PSTicket ty
checkTicketPresence = checkTPresence SPSTicket

-- | Check at runtime whether a value of the given type _may_ contain a @big_map@ value.
checkBigMapPresence :: Sing (ty :: T) -> TPresence 'PSBigMap ty
checkBigMapPresence = checkTPresence SPSBigMap

-- | Check at runtime whether a value of the given type _may_ contain nested @big_map@s.
checkNestedBigMapsPresence :: Sing (ty :: T) -> TPresence 'PSNestedBigMaps ty
checkNestedBigMapsPresence = checkTPresence SPSNestedBigMaps

{-# DEPRECATED checkOpPresence, checkContractTypePresence, checkTicketPresence, checkBigMapPresence, checkNestedBigMapsPresence
  "Use checkTPresence instead" #-}

-- | Check at runtime that a value of the given type cannot contain operations.
opAbsense :: Sing (t :: T) -> Maybe (Dict $ ForbidOp t)
opAbsense = fmap (\Refl -> Dict) . tAbsence SPSOp

-- | Check at runtime that a value of the given type cannot contain @contract@ values.
contractTypeAbsense :: Sing (t :: T) -> Maybe (Dict $ ForbidContract t)
contractTypeAbsense = fmap (\Refl -> Dict) . tAbsence SPSContract

-- | Check at runtime that a value of the given type cannot containt @big_map@ values
bigMapAbsense :: Sing (t :: T) -> Maybe (Dict $ ForbidBigMap t)
bigMapAbsense = fmap (\Refl -> Dict) . tAbsence SPSBigMap

-- | Check at runtime that a value of the given type cannot contain nested @big_map@s.
nestedBigMapsAbsense :: Sing (t :: T) -> Maybe (Dict $ ForbidNestedBigMaps t)
nestedBigMapsAbsense = fmap (\Refl -> Dict) . tAbsence SPSNestedBigMaps

{-# DEPRECATED opAbsense, contractTypeAbsense, bigMapAbsense, nestedBigMapsAbsense
  "Use tAbsence instead"
 #-}

-- | Inductive proof that 'Comparable' implies 'HasNoNestedBigMaps'. This is
-- stubbed with an @unsafeCoerce Refl@ at runtime to avoid runtime traversals.
comparabilityImpliesNoNestedBigMaps
  :: forall t. (SingI t, IsComparable t ~ 'True) => ContainsNestedBigMaps t :~: 'False
comparabilityImpliesNoNestedBigMaps = stubProof $ go (sing @t)
  where
    go :: IsComparable a ~ 'True => Sing a -> ContainsNestedBigMaps a :~: 'False
    go = \case
      STPair (a :: Sing a) (b :: Sing b) -> case (checkComparability a, checkComparability b) of
        (CanBeCompared, CanBeCompared) -> Refl \\ go a \\ go b
      STOr a b -> case (checkComparability a, checkComparability b) of
        (CanBeCompared, CanBeCompared) -> Refl \\ go a \\ go b
      STOption t -> Refl \\ go t
      STNever -> Refl
      STUnit -> Refl
      STInt -> Refl
      STNat -> Refl
      STString -> Refl
      STBytes -> Refl
      STMutez -> Refl
      STBool -> Refl
      STKeyHash -> Refl
      STTimestamp -> Refl
      STAddress -> Refl
      STKey -> Refl
      STSignature -> Refl
      STChainId -> Refl

-- | Inductive proof that 'Comparable' implies 'HasNoOp'. This is
-- stubbed with an @unsafeCoerce Refl@ at runtime to avoid runtime traversals.
comparabilityImpliesNoOp
  :: forall t. (SingI t, IsComparable t ~ 'True) => ContainsOp t :~: 'False
comparabilityImpliesNoOp = stubProof $ go (sing @t)
  where
    go :: IsComparable a ~ 'True => Sing a -> ContainsOp a :~: 'False
    go = \case
      STPair (a :: Sing a) (b :: Sing b) -> case (checkComparability a, checkComparability b) of
        (CanBeCompared, CanBeCompared) -> Refl \\ go a \\ go b
      STOr a b -> case (checkComparability a, checkComparability b) of
        (CanBeCompared, CanBeCompared) -> Refl \\ go a \\ go b
      STOption t -> Refl \\ go t
      STNever -> Refl
      STUnit -> Refl
      STInt -> Refl
      STNat -> Refl
      STString -> Refl
      STBytes -> Refl
      STMutez -> Refl
      STBool -> Refl
      STKeyHash -> Refl
      STTimestamp -> Refl
      STAddress -> Refl
      STKey -> Refl
      STSignature -> Refl
      STChainId -> Refl

{-# DEPRECATED comparabilityImpliesNoNestedBigMaps, comparabilityImpliesNoOp
  "Already implied by Comparable constraint" #-}

getComparableProofS :: Sing (a :: T) -> Maybe (Dict (Comparable a))
getComparableProofS = comparabilityPresence
{-# DEPRECATED getComparableProofS "Use comparabilityPresence" #-}

type IsComparable t = Not (ContainsT 'PSNonComparable t)
{-# DEPRECATED IsComparable "Use 'Not (ContainsT PSNonComparable t)' instead" #-}