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

{-# LANGUAGE UndecidableSuperClasses #-}

-- | Scope-related constraints used in Lorentz.
--
-- This contains constraints from "Morley.Michelson.Typed.Scope" modified for use
-- in Lorentz.
module Lorentz.Constraints.Scopes
  ( -- * Grouped constraints
    NiceComparable
  , NiceConstant
  , Dupable
  , NiceFullPackedValue
  , NicePackedValue
  , NiceParameter
  , NiceUntypedValue
  , NiceStorage
  , NiceStorageFull
  , NiceUnpackedValue
  , NiceViewable
  , NiceNoBigMap

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

  , -- * Re-exports
    withDict
  ) where

import Lorentz.Annotation (HasAnnotation)
import Morley.Michelson.Typed
import Morley.Michelson.Typed.Scope.Internal.ForbidT
import Morley.Michelson.Typed.Scope.Internal.Scopes

{- $setup
>>> import Lorentz
>>> import Morley.Michelson.Typed
>>> import Fmt (pretty)
-}

-- 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 a) => KnownValue a
instance (IsoValue a, Typeable a) => KnownValue a

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

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

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

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

-- For NiceSomething we use type classes to display user-friendly error messages
-- on ambiguous and polymorphic types. We use SomethingScopeC instead of
-- SomethingScope for the same reason.

{- | Constraint applied to any part of a parameter type.

Use t'Lorentz.Constraints.Derivative.NiceParameterFull' instead
when you need to know the contract's entrypoints at compile-time.

Shows human-readable errors:

>>> epAddressToContract @Operation
...
... Type `operation` found in
... 'TOperation
... is not allowed in this scope
...

Also on ambiguity:

>>> epAddressToContract
...
... Can't check if type
... ToT p0
... contains `operation` or nested `big_map`s. Perhaps you need to add
... NiceParameter p0
... constraint? You can also try adding a type annotation.
...
-}
class (ParameterScopeC (NiceParameter a) (ToT a), KnownValue a) => NiceParameter a
instance (ParameterScopeC (NiceParameter a) (ToT a), KnownValue a) => NiceParameter a

class (StorageScopeC (NiceStorage a) (ToT a), KnownValue a) => NiceStorage a
instance (StorageScopeC (NiceStorage a) (ToT a), KnownValue a) => NiceStorage a

type NiceStorageFull a = (NiceStorage a, HasAnnotation a)

{- | Constraint applied to constants.

Shows human-readable errors on ambiguity:

>>> push undefined
...
... Can't check if type
... ToT t0
... contains `operation`, `big_map`, `contract`, `ticket` or `sapling_state`. Perhaps you need to add
... NiceConstant t0
... constraint? You can also try adding a type annotation.
...

>>> pretty $ push (1 :: Integer)
[PUSH int 1]
-}
class (ConstantScopeC (NiceConstant a) (ToT a), KnownValue a) => NiceConstant a
instance (ConstantScopeC (NiceConstant a) (ToT a), KnownValue a) => NiceConstant a

{- | Constraint applied to constants.

Shows human-readable errors:

>>> ticket # dup
...
... Type `ticket` found in
... 'TOption ('TTicket (ToT a))
... is not allowed in this scope
...

Also on ambiguity:

>>> dup
...
... Can't check if type
... ToT a0
... contains `ticket`. Perhaps you need to add
... Dupable a0
... constraint? You can also try adding a type annotation.
...

>>> pretty $ dup @Integer
[DUP]
-}
class (DupableScopeC (Dupable a) (ToT a), KnownValue a) => Dupable a
instance (DupableScopeC (Dupable a) (ToT a), KnownValue a) => Dupable a

{- | Constraint applied to a value being packed.

Shows human-readable errors:

>>> pack @Operation
...
... Type `operation` found in
... 'TOperation
... is not allowed in this scope
...

Also on ambiguity:

>>> pack
...
... Can't check if type
... ToT a0
... contains `operation`, `big_map`, `ticket` or `sapling_state`. Perhaps you need to add
... NicePackedValue a0
... constraint? You can also try adding a type annotation.
...
-}
class (PackedValScopeC (NicePackedValue a) (ToT a), KnownValue a) => NicePackedValue a
instance (PackedValScopeC (NicePackedValue a) (ToT a), KnownValue a) => NicePackedValue a

{- | Constraint applied to a value being unpacked.

Shows human-readable errors:

>>> unpack @Operation
...
... Type `operation` found in
... 'TOperation
... is not allowed in this scope
...

Also on ambiguity:

>>> unpack
...
... Can't check if type
... ToT a0
... contains `operation`, `big_map`, `contract`, `ticket` or `sapling_state`. Perhaps you need to add
... NiceUnpackedValue a0
... constraint? You can also try adding a type annotation.
...
-}
class (UnpackedValScopeC (NiceUnpackedValue a) (ToT a), KnownValue a) => NiceUnpackedValue a
instance (UnpackedValScopeC (NiceUnpackedValue a) (ToT a), KnownValue a) => NiceUnpackedValue a

type NiceFullPackedValue a = (NicePackedValue a, NiceUnpackedValue a)

class (UntypedValScopeC (NiceUntypedValue a) (ToT a), KnownValue a) => NiceUntypedValue a
instance (UntypedValScopeC (NiceUntypedValue a) (ToT a), KnownValue a) => NiceUntypedValue a

{- | Constraint applied to a value returned from a view.

Shows human-readable errors:

>>> view' @"SomeView" @Operation
...
... Type `operation` found in
... 'TOperation
... is not allowed in this scope
...

Also on ambiguity:

>>> view' @"SomeView"
...
... Can't check if type
... ToT ret0
... contains `operation`, `big_map` or `ticket`. Perhaps you need to add
... NiceViewable ret0
... constraint? You can also try adding a type annotation.
...
-}
class (ViewableScopeC (NiceViewable a) (ToT a), KnownValue a) => NiceViewable a
instance (ViewableScopeC (NiceViewable a) (ToT a), KnownValue a) => NiceViewable a

{- | Constraint applied to any type, to check if Michelson representation (if exists) of this
type is Comparable. In case it is not prints human-readable error message

>>> emptySet @[Integer]
...
... Non-comparable type
... 'TList 'TInt
... is not allowed in this scope
...

>>> emptySet
...
... Can't check if type
... ToT e0
... contains non-comparable types. Perhaps you need to add
... NiceComparable e0
... constraint? You can also try adding a type annotation.
...
-}
class (ComparabilityScopeC (NiceComparable n) (ToT n), KnownValue n) => NiceComparable n
instance (ComparabilityScopeC (NiceComparable n) (ToT n), KnownValue n) => NiceComparable n

{- | Constraint applied to a @big_map@ value type.

Shows human-readable errors:

>>> emptyBigMap @Integer @(BigMap Integer Integer)
...
... Type `big_map` found in
... 'TBigMap 'TInt 'TInt
... is not allowed in this scope
...

Also on ambiguity:

>>> emptyBigMap @Integer
...
... Can't check if type
... ToT v0
... contains `big_map`. Perhaps you need to add
... NiceNoBigMap v0
... constraint? You can also try adding a type annotation.
...
-}
class (KnownValue n, ForbidManyT (NiceNoBigMap n) '[ 'PSBigMap] (ToT n)) => NiceNoBigMap n
instance (KnownValue n, ForbidManyT (NiceNoBigMap n) '[ 'PSBigMap] (ToT n)) => NiceNoBigMap n