{-# LANGUAGE UndecidableSuperClasses #-}

-- | Scope-related constraints used in Lorentz.
module Lorentz.Constraints
  ( -- * Grouped constraints
    NiceParameter
  , NiceStorage
  , NiceConstant
  , NicePackedValue
  , NiceUnpackedValue
  , NiceFullPackedValue
  , NicePrintedValue

  , niceParameterEvi
  , niceStorageEvi
  , niceConstantEvi
  , nicePackedValueEvi
  , niceUnpackedValueEvi
  , nicePrintedValueEvi

    -- * Individual constraints (internals)
  , CanHaveBigMap
  , KnownValue
  , KnownCValue
  , NoOperation
  , NoContractType
  , NoBigMap

  , -- * Re-exports
    withDict
  ) where

import Data.Constraint (trans, weaken2)
import Data.Singletons (SingI)

import Michelson.Typed

-- We write these constraints as class + instance, rather than
-- type aliases, in order to allow their partial application.

-- | Gathers constraints, commonly required for values.
class (IsoValue a, Typeable (ToT a), SingI (ToT a)) => KnownValue a
instance (IsoValue a, Typeable (ToT a), SingI (ToT a)) => KnownValue a

class (IsoValue a, Typeable (ToCT a), SingI (ToCT a)) => KnownCValue a
instance (IsoValue a, Typeable (ToCT a), SingI (ToCT a)) => KnownCValue a

-- | Ensure given type does not contain "operation".
class (IsoValue a, ForbidOp (ToT a)) => NoOperation a
instance (IsoValue a, ForbidOp (ToT a)) => NoOperation a

class (IsoValue a, ForbidContract (ToT a)) => NoContractType a
instance (IsoValue a, ForbidContract (ToT a)) => NoContractType a

class (IsoValue a, ForbidBigMap (ToT a)) => NoBigMap a
instance (IsoValue a, ForbidBigMap (ToT a)) => NoBigMap a

class (IsoValue a, HasNoNestedBigMaps (ToT a)) => CanHaveBigMap a
instance (IsoValue a, HasNoNestedBigMaps (ToT a)) => CanHaveBigMap a

-- | Constraint applied to parameter type.
type NiceParameter a = (KnownValue a, ProperParameterBetterErrors (ToT a))

type NiceStorage a = (KnownValue a, ProperStorageBetterErrors (ToT a))

type NiceConstant a = (KnownValue a, ProperConstantBetterErrors (ToT a))

type NicePackedValue a = (KnownValue a, ProperPackedValBetterErrors (ToT a))

type NiceUnpackedValue a = (KnownValue a, ProperUnpackedValBetterErrors (ToT a))

type NiceFullPackedValue a = (NicePackedValue a, NiceUnpackedValue a)

type NicePrintedValue a = (KnownValue a, ProperPrintedValBetterErrors (ToT a))

niceParameterEvi :: forall a. NiceParameter a :- ParameterScope (ToT a)
niceParameterEvi =
  properParameterEvi @(ToT a) `trans` weaken2

niceStorageEvi :: forall a. NiceStorage a :- StorageScope (ToT a)
niceStorageEvi =
  properStorageEvi @(ToT a) `trans` weaken2

niceConstantEvi :: forall a. NiceConstant a :- ConstantScope (ToT a)
niceConstantEvi =
  properConstantEvi @(ToT a) `trans` weaken2

nicePackedValueEvi :: forall a. NicePackedValue a :- PackedValScope (ToT a)
nicePackedValueEvi =
  properPackedValEvi @(ToT a) `trans` weaken2

niceUnpackedValueEvi :: forall a. NiceUnpackedValue a :- UnpackedValScope (ToT a)
niceUnpackedValueEvi =
  properUnpackedValEvi @(ToT a) `trans` weaken2

nicePrintedValueEvi :: forall a. NicePrintedValue a :- PrintedValScope (ToT a)
nicePrintedValueEvi =
  properPrintedValEvi @(ToT a) `trans` weaken2