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

{- | Module, containing restrictions imposed by instruction or value scope.

Michelson have multiple restrictions on values, examples:

* @operation@ type cannot appear in parameter.
* @big_map@ type cannot appear in @PUSH@-able constants.
* @contract@ type cannot appear in type we @UNPACK@ to.

Thus we declare multiple "scopes" - constraints applied in corresponding
situations, for instance

* 'ParameterScope';
* 'StorageScope';
* 'ConstantScope'.

Also we separate multiple "classes" of scope-related constraints.

* 'ParameterScope' and similar ones are used within Michelson engine,
they are understandable by GHC and produce human-readable errors.

* Lorentz and other eDSLs may declare their own constraints, in most cases
you should use them. For example see @Lorentz.Constraints@ module.

-}

module Morley.Michelson.Typed.Scope
  ( -- * Scopes
    ConstantScope
  , DupableScope
  , StorageScope
  , PackedValScope
  , ParameterScope
  , UntypedValScope
  , UnpackedValScope
  , ViewableScope
  , ComparabilityScope

  , IsDupableScope

  , BadTypeForScope (..)
  , CheckScope (..)
  , WithDeMorganScope (..)
  , deMorganForbidT
  , Comparable
  , comparableImplies
  , WellTyped
  , NotWellTyped (..)

    -- * Implementation internals
  , ContainsT

  , ForbidT
  , ForbidOp
  , ForbidContract
  , ForbidTicket
  , ForbidBigMap
  , ForbidNestedBigMaps
  , ForbidNonComparable

  , TPresence(..)
  , TPredicateSym(..)
  , SingTPredicateSym(..)
  , checkTPresence
  , tPresence
  , tAbsence

  , Comparability(..)
  , checkComparability
  , comparabilityPresence

  , getWTP
  , getWTP'
    -- * Re-exports
  , withDict
  , SingI (..)
  , (:-)(..)
  ) where

import Data.Constraint (withDict, (:-)(..))
import Data.Singletons (SingI(..))

import Morley.Michelson.Typed.Scope.Internal.CheckScope
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
import Morley.Michelson.Typed.Scope.Internal.WithDeMorganScope