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

{-# OPTIONS_HADDOCK not-home #-}

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

import Data.Constraint (Dict(..))
import Data.Singletons (SingI(..))

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.Scopes
import Morley.Michelson.Typed.Scope.Internal.WellTyped

-- | Should be present for common scopes.
class CheckScope (c :: Constraint) where
  -- | Check that constraint hold for a given type.
  checkScope :: Either BadTypeForScope (Dict c)

instance SingI t => CheckScope (WellTyped t) where
  checkScope :: Either BadTypeForScope (Dict (WellTyped t))
checkScope = (NotWellTyped -> BadTypeForScope)
-> Either NotWellTyped (Dict (WellTyped t))
-> Either BadTypeForScope (Dict (WellTyped t))
forall a b c. (a -> b) -> Either a c -> Either b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first NotWellTyped -> BadTypeForScope
nwtCause (Either NotWellTyped (Dict (WellTyped t))
 -> Either BadTypeForScope (Dict (WellTyped t)))
-> Either NotWellTyped (Dict (WellTyped t))
-> Either BadTypeForScope (Dict (WellTyped t))
forall a b. (a -> b) -> a -> b
$ forall (t :: T).
SingI t =>
Either NotWellTyped (Dict (WellTyped t))
getWTP @t
instance SingI t => CheckScope (ForbidOp t) where
  checkScope :: Either BadTypeForScope (Dict (ForbidOp t))
checkScope = BadTypeForScope
-> Maybe (Dict (ForbidOp t))
-> Either BadTypeForScope (Dict (ForbidOp t))
forall l r. l -> Maybe r -> Either l r
maybeToRight BadTypeForScope
BtIsOperation (Maybe (Dict (ForbidOp t))
 -> Either BadTypeForScope (Dict (ForbidOp t)))
-> Maybe (Dict (ForbidOp t))
-> Either BadTypeForScope (Dict (ForbidOp t))
forall a b. (a -> b) -> a -> b
$ ((ContainsT 'PSOp t :~: 'False) -> Dict (ForbidOp t))
-> Maybe (ContainsT 'PSOp t :~: 'False)
-> Maybe (Dict (ForbidOp t))
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ContainsT 'PSOp t :~: 'False
Refl -> Dict (ForbidOp t)
forall (a :: Constraint). a => Dict a
Dict) (Maybe (ContainsT 'PSOp t :~: 'False) -> Maybe (Dict (ForbidOp t)))
-> Maybe (ContainsT 'PSOp t :~: 'False)
-> Maybe (Dict (ForbidOp t))
forall a b. (a -> b) -> a -> b
$ Sing 'PSOp -> Sing t -> Maybe (ContainsT 'PSOp t :~: 'False)
forall (p :: TPredicateSym) (t :: T).
Sing p -> Sing t -> Maybe (ContainsT p t :~: 'False)
tAbsence Sing 'PSOp
SingTPredicateSym 'PSOp
SPSOp (Sing t -> Maybe (ContainsT 'PSOp t :~: 'False))
-> Sing t -> Maybe (ContainsT 'PSOp t :~: 'False)
forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k). SingI a => Sing a
forall (a :: T). SingI a => Sing a
sing @t
instance SingI t => CheckScope (ForbidBigMap t) where
  checkScope :: Either BadTypeForScope (Dict (ForbidBigMap t))
checkScope = BadTypeForScope
-> Maybe (Dict (ForbidBigMap t))
-> Either BadTypeForScope (Dict (ForbidBigMap t))
forall l r. l -> Maybe r -> Either l r
maybeToRight BadTypeForScope
BtHasBigMap (Maybe (Dict (ForbidBigMap t))
 -> Either BadTypeForScope (Dict (ForbidBigMap t)))
-> Maybe (Dict (ForbidBigMap t))
-> Either BadTypeForScope (Dict (ForbidBigMap t))
forall a b. (a -> b) -> a -> b
$ ((ContainsT 'PSBigMap t :~: 'False) -> Dict (ForbidBigMap t))
-> Maybe (ContainsT 'PSBigMap t :~: 'False)
-> Maybe (Dict (ForbidBigMap t))
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ContainsT 'PSBigMap t :~: 'False
Refl -> Dict (ForbidBigMap t)
forall (a :: Constraint). a => Dict a
Dict) (Maybe (ContainsT 'PSBigMap t :~: 'False)
 -> Maybe (Dict (ForbidBigMap t)))
-> Maybe (ContainsT 'PSBigMap t :~: 'False)
-> Maybe (Dict (ForbidBigMap t))
forall a b. (a -> b) -> a -> b
$ Sing 'PSBigMap
-> Sing t -> Maybe (ContainsT 'PSBigMap t :~: 'False)
forall (p :: TPredicateSym) (t :: T).
Sing p -> Sing t -> Maybe (ContainsT p t :~: 'False)
tAbsence Sing 'PSBigMap
SingTPredicateSym 'PSBigMap
SPSBigMap (Sing t -> Maybe (ContainsT 'PSBigMap t :~: 'False))
-> Sing t -> Maybe (ContainsT 'PSBigMap t :~: 'False)
forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k). SingI a => Sing a
forall (a :: T). SingI a => Sing a
sing @t
instance SingI t => CheckScope (ForbidNestedBigMaps t) where
  checkScope :: Either BadTypeForScope (Dict (ForbidNestedBigMaps t))
checkScope = BadTypeForScope
-> Maybe (Dict (ForbidNestedBigMaps t))
-> Either BadTypeForScope (Dict (ForbidNestedBigMaps t))
forall l r. l -> Maybe r -> Either l r
maybeToRight BadTypeForScope
BtHasNestedBigMap (Maybe (Dict (ForbidNestedBigMaps t))
 -> Either BadTypeForScope (Dict (ForbidNestedBigMaps t)))
-> Maybe (Dict (ForbidNestedBigMaps t))
-> Either BadTypeForScope (Dict (ForbidNestedBigMaps t))
forall a b. (a -> b) -> a -> b
$ ((ContainsT 'PSNestedBigMaps t :~: 'False)
 -> Dict (ForbidNestedBigMaps t))
-> Maybe (ContainsT 'PSNestedBigMaps t :~: 'False)
-> Maybe (Dict (ForbidNestedBigMaps t))
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ContainsT 'PSNestedBigMaps t :~: 'False
Refl -> Dict (ForbidNestedBigMaps t)
forall (a :: Constraint). a => Dict a
Dict) (Maybe (ContainsT 'PSNestedBigMaps t :~: 'False)
 -> Maybe (Dict (ForbidNestedBigMaps t)))
-> Maybe (ContainsT 'PSNestedBigMaps t :~: 'False)
-> Maybe (Dict (ForbidNestedBigMaps t))
forall a b. (a -> b) -> a -> b
$ Sing 'PSNestedBigMaps
-> Sing t -> Maybe (ContainsT 'PSNestedBigMaps t :~: 'False)
forall (p :: TPredicateSym) (t :: T).
Sing p -> Sing t -> Maybe (ContainsT p t :~: 'False)
tAbsence Sing 'PSNestedBigMaps
SingTPredicateSym 'PSNestedBigMaps
SPSNestedBigMaps (Sing t -> Maybe (ContainsT 'PSNestedBigMaps t :~: 'False))
-> Sing t -> Maybe (ContainsT 'PSNestedBigMaps t :~: 'False)
forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k). SingI a => Sing a
forall (a :: T). SingI a => Sing a
sing @t
instance SingI t => CheckScope (ForbidContract t) where
  checkScope :: Either BadTypeForScope (Dict (ForbidContract t))
checkScope = BadTypeForScope
-> Maybe (Dict (ForbidContract t))
-> Either BadTypeForScope (Dict (ForbidContract t))
forall l r. l -> Maybe r -> Either l r
maybeToRight BadTypeForScope
BtHasContract (Maybe (Dict (ForbidContract t))
 -> Either BadTypeForScope (Dict (ForbidContract t)))
-> Maybe (Dict (ForbidContract t))
-> Either BadTypeForScope (Dict (ForbidContract t))
forall a b. (a -> b) -> a -> b
$ ((ContainsT 'PSContract t :~: 'False) -> Dict (ForbidContract t))
-> Maybe (ContainsT 'PSContract t :~: 'False)
-> Maybe (Dict (ForbidContract t))
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ContainsT 'PSContract t :~: 'False
Refl -> Dict (ForbidContract t)
forall (a :: Constraint). a => Dict a
Dict) (Maybe (ContainsT 'PSContract t :~: 'False)
 -> Maybe (Dict (ForbidContract t)))
-> Maybe (ContainsT 'PSContract t :~: 'False)
-> Maybe (Dict (ForbidContract t))
forall a b. (a -> b) -> a -> b
$ Sing 'PSContract
-> Sing t -> Maybe (ContainsT 'PSContract t :~: 'False)
forall (p :: TPredicateSym) (t :: T).
Sing p -> Sing t -> Maybe (ContainsT p t :~: 'False)
tAbsence Sing 'PSContract
SingTPredicateSym 'PSContract
SPSContract (Sing t -> Maybe (ContainsT 'PSContract t :~: 'False))
-> Sing t -> Maybe (ContainsT 'PSContract t :~: 'False)
forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k). SingI a => Sing a
forall (a :: T). SingI a => Sing a
sing @t
instance SingI t => CheckScope (ForbidTicket t) where
  checkScope :: Either BadTypeForScope (Dict (ForbidTicket t))
checkScope = BadTypeForScope
-> Maybe (Dict (ForbidTicket t))
-> Either BadTypeForScope (Dict (ForbidTicket t))
forall l r. l -> Maybe r -> Either l r
maybeToRight BadTypeForScope
BtHasTicket (Maybe (Dict (ForbidTicket t))
 -> Either BadTypeForScope (Dict (ForbidTicket t)))
-> Maybe (Dict (ForbidTicket t))
-> Either BadTypeForScope (Dict (ForbidTicket t))
forall a b. (a -> b) -> a -> b
$ ((ContainsT 'PSTicket t :~: 'False) -> Dict (ForbidTicket t))
-> Maybe (ContainsT 'PSTicket t :~: 'False)
-> Maybe (Dict (ForbidTicket t))
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ContainsT 'PSTicket t :~: 'False
Refl -> Dict (ForbidTicket t)
forall (a :: Constraint). a => Dict a
Dict) (Maybe (ContainsT 'PSTicket t :~: 'False)
 -> Maybe (Dict (ForbidTicket t)))
-> Maybe (ContainsT 'PSTicket t :~: 'False)
-> Maybe (Dict (ForbidTicket t))
forall a b. (a -> b) -> a -> b
$ Sing 'PSTicket
-> Sing t -> Maybe (ContainsT 'PSTicket t :~: 'False)
forall (p :: TPredicateSym) (t :: T).
Sing p -> Sing t -> Maybe (ContainsT p t :~: 'False)
tAbsence Sing 'PSTicket
SingTPredicateSym 'PSTicket
SPSTicket (Sing t -> Maybe (ContainsT 'PSTicket t :~: 'False))
-> Sing t -> Maybe (ContainsT 'PSTicket t :~: 'False)
forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k). SingI a => Sing a
forall (a :: T). SingI a => Sing a
sing @t
instance SingI t => CheckScope (ForbidSaplingState t) where
  checkScope :: Either BadTypeForScope (Dict (ForbidSaplingState t))
checkScope = BadTypeForScope
-> Maybe (Dict (ForbidSaplingState t))
-> Either BadTypeForScope (Dict (ForbidSaplingState t))
forall l r. l -> Maybe r -> Either l r
maybeToRight BadTypeForScope
BtHasSaplingState (Maybe (Dict (ForbidSaplingState t))
 -> Either BadTypeForScope (Dict (ForbidSaplingState t)))
-> Maybe (Dict (ForbidSaplingState t))
-> Either BadTypeForScope (Dict (ForbidSaplingState t))
forall a b. (a -> b) -> a -> b
$ ((ContainsT 'PSSaplingState t :~: 'False)
 -> Dict (ForbidSaplingState t))
-> Maybe (ContainsT 'PSSaplingState t :~: 'False)
-> Maybe (Dict (ForbidSaplingState t))
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ContainsT 'PSSaplingState t :~: 'False
Refl -> Dict (ForbidSaplingState t)
forall (a :: Constraint). a => Dict a
Dict) (Maybe (ContainsT 'PSSaplingState t :~: 'False)
 -> Maybe (Dict (ForbidSaplingState t)))
-> Maybe (ContainsT 'PSSaplingState t :~: 'False)
-> Maybe (Dict (ForbidSaplingState t))
forall a b. (a -> b) -> a -> b
$ Sing 'PSSaplingState
-> Sing t -> Maybe (ContainsT 'PSSaplingState t :~: 'False)
forall (p :: TPredicateSym) (t :: T).
Sing p -> Sing t -> Maybe (ContainsT p t :~: 'False)
tAbsence Sing 'PSSaplingState
SingTPredicateSym 'PSSaplingState
SPSSaplingState (Sing t -> Maybe (ContainsT 'PSSaplingState t :~: 'False))
-> Sing t -> Maybe (ContainsT 'PSSaplingState t :~: 'False)
forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k). SingI a => Sing a
forall (a :: T). SingI a => Sing a
sing @t
instance SingI t => CheckScope (Comparable t) where
  checkScope :: Either BadTypeForScope (Dict (Comparable t))
checkScope = BadTypeForScope
-> Maybe (Dict (Comparable t))
-> Either BadTypeForScope (Dict (Comparable t))
forall l r. l -> Maybe r -> Either l r
maybeToRight BadTypeForScope
BtNotComparable (Maybe (Dict (Comparable t))
 -> Either BadTypeForScope (Dict (Comparable t)))
-> Maybe (Dict (Comparable t))
-> Either BadTypeForScope (Dict (Comparable t))
forall a b. (a -> b) -> a -> b
$ Sing t -> Maybe (Dict (Comparable t))
forall (t :: T). Sing t -> Maybe (Dict (Comparable t))
comparabilityPresence Sing t
forall {k} (a :: k). SingI a => Sing a
sing

instance SingI t => CheckScope (ParameterScope t) where
  checkScope :: Either BadTypeForScope (Dict (ParameterScope t))
checkScope = do
    Dict (WellTyped t)
Dict <- forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(WellTyped t)
    Dict (ForbidOp t)
Dict <- forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ForbidOp t)
    Dict (ForbidNestedBigMaps t)
Dict <- forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ForbidNestedBigMaps t)
    Dict (ParameterScope t)
-> Either BadTypeForScope (Dict (ParameterScope t))
forall a. a -> Either BadTypeForScope a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Dict (ParameterScope t)
forall (a :: Constraint). a => Dict a
Dict

instance SingI t => CheckScope (StorageScope t) where
  checkScope :: Either BadTypeForScope (Dict (StorageScope t))
checkScope = do
    Dict (WellTyped t)
Dict <- forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(WellTyped t)
    Dict (ForbidOp t)
Dict <- forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ForbidOp t)
    Dict (ForbidNestedBigMaps t)
Dict <- forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ForbidNestedBigMaps t)
    Dict (ForbidContract t)
Dict <- forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ForbidContract t)
    Dict (StorageScope t)
-> Either BadTypeForScope (Dict (StorageScope t))
forall a. a -> Either BadTypeForScope a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Dict (StorageScope t)
forall (a :: Constraint). a => Dict a
Dict

instance SingI t => CheckScope (ConstantScope t) where
  checkScope :: Either BadTypeForScope (Dict (ConstantScope t))
checkScope = do
    Dict (WellTyped t)
Dict <- forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(WellTyped t)
    Dict (ForbidOp t)
Dict <- forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ForbidOp t)
    Dict (ForbidBigMap t)
Dict <- forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ForbidBigMap t)
    Dict (ForbidContract t)
Dict <- forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ForbidContract t)
    Dict (ForbidTicket t)
Dict <- forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ForbidTicket t)
    Dict (ForbidSaplingState t)
Dict <- forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ForbidSaplingState t)
    Dict (ConstantScope t)
-> Either BadTypeForScope (Dict (ConstantScope t))
forall a. a -> Either BadTypeForScope a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Dict (ConstantScope t)
forall (a :: Constraint). a => Dict a
Dict

instance SingI t => CheckScope (DupableScope t) where
  checkScope :: Either BadTypeForScope (Dict (DupableScope t))
checkScope = do
    Dict (ForbidTicket t)
Dict <- forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ForbidTicket t)
    Dict (DupableScope t)
-> Either BadTypeForScope (Dict (DupableScope t))
forall a. a -> Either BadTypeForScope a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Dict (DupableScope t)
forall (a :: Constraint). a => Dict a
Dict

instance SingI t => CheckScope (PackedValScope t) where
  checkScope :: Either BadTypeForScope (Dict (PackedValScope t))
checkScope = do
    Dict (WellTyped t)
Dict <- forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(WellTyped t)
    Dict (ForbidOp t)
Dict <- forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ForbidOp t)
    Dict (ForbidBigMap t)
Dict <- forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ForbidBigMap t)
    Dict (ForbidTicket t)
Dict <- forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ForbidTicket t)
    Dict (ForbidSaplingState t)
Dict <- forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ForbidSaplingState t)
    Dict (PackedValScope t)
-> Either BadTypeForScope (Dict (PackedValScope t))
forall a. a -> Either BadTypeForScope a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Dict (PackedValScope t)
forall (a :: Constraint). a => Dict a
Dict

instance SingI t => CheckScope (UnpackedValScope t) where
  checkScope :: Either BadTypeForScope (Dict (UnpackedValScope t))
checkScope = do
    Dict (ConstantScope t)
Dict <- forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ConstantScope t)
    Dict (UnpackedValScope t)
-> Either BadTypeForScope (Dict (UnpackedValScope t))
forall a. a -> Either BadTypeForScope a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Dict (UnpackedValScope t)
forall (a :: Constraint). a => Dict a
Dict

instance SingI t => CheckScope (ViewableScope t) where
  checkScope :: Either BadTypeForScope (Dict (ViewableScope t))
checkScope = do
    Dict (ForbidOp t)
Dict <- forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ForbidOp t)
    Dict (ForbidBigMap t)
Dict <- forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ForbidBigMap t)
    Dict (ForbidTicket t)
Dict <- forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ForbidTicket t)
    Dict (ViewableScope t)
-> Either BadTypeForScope (Dict (ViewableScope t))
forall a. a -> Either BadTypeForScope a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Dict (ViewableScope t)
forall (a :: Constraint). a => Dict a
Dict

instance SingI t => CheckScope (ComparabilityScope t) where
  checkScope :: Either BadTypeForScope (Dict (ComparabilityScope t))
checkScope = do
    Dict (Comparable t)
Dict <- forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(Comparable t)
    Dict (ComparabilityScope t)
-> Either BadTypeForScope (Dict (ComparabilityScope t))
forall a. a -> Either BadTypeForScope a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Dict (ComparabilityScope t)
forall (a :: Constraint). a => Dict a
Dict

instance (CheckScope a, CheckScope b) => CheckScope (a, b) where
  checkScope :: Either BadTypeForScope (Dict (a, b))
checkScope = do
    Dict a
Dict <- forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @a
    Dict b
Dict <- forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @b
    Dict (a, b) -> Either BadTypeForScope (Dict (a, b))
forall a. a -> Either BadTypeForScope a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Dict (a, b)
forall (a :: Constraint). a => Dict a
Dict