-- 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 = first nwtCause $ getWTP @t
instance SingI t => CheckScope (ForbidOp t) where
  checkScope = maybeToRight BtIsOperation $ fmap (\Refl -> Dict) $ tAbsence SPSOp $ sing @t
instance SingI t => CheckScope (ForbidBigMap t) where
  checkScope = maybeToRight BtHasBigMap $ fmap (\Refl -> Dict) $ tAbsence SPSBigMap $ sing @t
instance SingI t => CheckScope (ForbidNestedBigMaps t) where
  checkScope = maybeToRight BtHasNestedBigMap $ fmap (\Refl -> Dict) $ tAbsence SPSNestedBigMaps $ sing @t
instance SingI t => CheckScope (ForbidContract t) where
  checkScope = maybeToRight BtHasContract $ fmap (\Refl -> Dict) $ tAbsence SPSContract $ sing @t
instance SingI t => CheckScope (ForbidTicket t) where
  checkScope = maybeToRight BtHasTicket $ fmap (\Refl -> Dict) $ tAbsence SPSTicket $ sing @t
instance SingI t => CheckScope (ForbidSaplingState t) where
  checkScope = maybeToRight BtHasSaplingState $ fmap (\Refl -> Dict) $ tAbsence SPSSaplingState $ sing @t
instance SingI t => CheckScope (Comparable t) where
  checkScope = maybeToRight BtNotComparable $ comparabilityPresence sing

instance SingI t => CheckScope (ParameterScope t) where
  checkScope = do
    Dict <- checkScope @(WellTyped t)
    Dict <- checkScope @(ForbidOp t)
    Dict <- checkScope @(ForbidNestedBigMaps t)
    pure Dict

instance SingI t => CheckScope (StorageScope t) where
  checkScope = do
    Dict <- checkScope @(WellTyped t)
    Dict <- checkScope @(ForbidOp t)
    Dict <- checkScope @(ForbidNestedBigMaps t)
    Dict <- checkScope @(ForbidContract t)
    pure Dict

instance SingI t => CheckScope (ConstantScope t) where
  checkScope = do
    Dict <- checkScope @(WellTyped t)
    Dict <- checkScope @(ForbidOp t)
    Dict <- checkScope @(ForbidBigMap t)
    Dict <- checkScope @(ForbidContract t)
    Dict <- checkScope @(ForbidTicket t)
    Dict <- checkScope @(ForbidSaplingState t)
    pure Dict

instance SingI t => CheckScope (DupableScope t) where
  checkScope = do
    Dict <- checkScope @(ForbidTicket t)
    pure Dict

instance SingI t => CheckScope (PackedValScope t) where
  checkScope = do
    Dict <- checkScope @(WellTyped t)
    Dict <- checkScope @(ForbidOp t)
    Dict <- checkScope @(ForbidBigMap t)
    Dict <- checkScope @(ForbidTicket t)
    Dict <- checkScope @(ForbidSaplingState t)
    pure Dict

instance SingI t => CheckScope (UnpackedValScope t) where
  checkScope = do
    Dict <- checkScope @(ConstantScope t)
    pure Dict

instance SingI t => CheckScope (ViewableScope t) where
  checkScope = do
    Dict <- checkScope @(ForbidOp t)
    Dict <- checkScope @(ForbidBigMap t)
    Dict <- checkScope @(ForbidTicket t)
    pure Dict

instance SingI t => CheckScope (ComparabilityScope t) where
  checkScope = do
    Dict <- checkScope @(Comparable t)
    pure Dict

instance (CheckScope a, CheckScope b) => CheckScope (a, b) where
  checkScope = do
    Dict <- checkScope @a
    Dict <- checkScope @b
    pure Dict