-- SPDX-FileCopyrightText: 2020 Tocqueville Group
--
-- SPDX-License-Identifier: LicenseRef-MIT-TQ

{-# LANGUAGE UndecidableSuperClasses #-}

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

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

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

  , -- * Re-exports
    withDict
  ) where

import Data.Constraint (evidence, trans, weaken1)

import Lorentz.Annotation (HasAnnotation)
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 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 (HasNoNestedBigMaps (ToT a), IsoValue a) => CanHaveBigMap a
instance (HasNoNestedBigMaps (ToT a), IsoValue a) => CanHaveBigMap a

-- | Constraint applied to any part of parameter type.
--
-- Note that you don't usually apply this constraint to the whole parameter,
-- consider using 'Lorentz.Constraints.Derivative.NiceParameterFull' in such case.
--
-- Using this type is justified e.g. when calling another contract, there
-- you usually supply an entrypoint argument, not the whole parameter.
type NiceParameter a = (ProperParameterBetterErrors (ToT a), KnownValue a)

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

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

type Dupable a = (ProperDupableBetterErrors (ToT a), KnownValue a)

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

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

type NiceFullPackedValue a = (NicePackedValue a, NiceUnpackedValue a)

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

type NiceComparable n = (Comparable (ToT n), KnownValue n)

type NiceNoBigMap n = (KnownValue n, HasNoBigMap (ToT n))

niceParameterEvi :: forall a. NiceParameter a :- ParameterScope (ToT a)
niceParameterEvi :: NiceParameter a :- ParameterScope (ToT a)
niceParameterEvi =
  ProperParameterBetterErrors (ToT a) :- ParameterScope (ToT a)
forall (t :: T). ProperParameterBetterErrors t :- ParameterScope t
properParameterEvi @(ToT a) (ProperParameterBetterErrors (ToT a) :- ParameterScope (ToT a))
-> (NiceParameter a :- ProperParameterBetterErrors (ToT a))
-> NiceParameter a :- ParameterScope (ToT a)
forall (b :: Constraint) (c :: Constraint) (a :: Constraint).
(b :- c) -> (a :- b) -> a :- c
`trans` NiceParameter a :- ProperParameterBetterErrors (ToT a)
forall (a :: Constraint) (b :: Constraint). (a, b) :- a
weaken1

niceStorageEvi :: forall a. NiceStorage a :- StorageScope (ToT a)
niceStorageEvi :: NiceStorage a :- StorageScope (ToT a)
niceStorageEvi =
  (NiceStorage a => Dict (StorageScope (ToT a)))
-> NiceStorage a :- StorageScope (ToT a)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (((SingI (ToT a), FailOnOperationFound (ContainsOp (ToT a)),
  FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT a)),
  FailOnContractFound (ContainsContract (ToT a)))
 :- StorageScope (ToT a))
-> Dict (StorageScope (ToT a))
forall (c :: Constraint) e. HasDict c e => e -> Dict c
evidence (((SingI (ToT a), FailOnOperationFound (ContainsOp (ToT a)),
   FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT a)),
   FailOnContractFound (ContainsContract (ToT a)))
  :- StorageScope (ToT a))
 -> Dict (StorageScope (ToT a)))
-> ((SingI (ToT a), FailOnOperationFound (ContainsOp (ToT a)),
     FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT a)),
     FailOnContractFound (ContainsContract (ToT a)))
    :- StorageScope (ToT a))
-> Dict (StorageScope (ToT a))
forall a b. (a -> b) -> a -> b
$ (SingI (ToT a), FailOnOperationFound (ContainsOp (ToT a)),
 FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT a)),
 FailOnContractFound (ContainsContract (ToT a)))
:- StorageScope (ToT a)
forall (t :: T). ProperStorageBetterErrors t :- StorageScope t
properStorageEvi @(ToT a))

niceConstantEvi :: forall a. NiceConstant a :- ConstantScope (ToT a)
niceConstantEvi :: NiceConstant a :- ConstantScope (ToT a)
niceConstantEvi =
  ProperConstantBetterErrors (ToT a) :- ConstantScope (ToT a)
forall (t :: T). ProperConstantBetterErrors t :- ConstantScope t
properConstantEvi @(ToT a) (ProperConstantBetterErrors (ToT a) :- ConstantScope (ToT a))
-> (NiceConstant a :- ProperConstantBetterErrors (ToT a))
-> NiceConstant a :- ConstantScope (ToT a)
forall (b :: Constraint) (c :: Constraint) (a :: Constraint).
(b :- c) -> (a :- b) -> a :- c
`trans` NiceConstant a :- ProperConstantBetterErrors (ToT a)
forall (a :: Constraint) (b :: Constraint). (a, b) :- a
weaken1

dupableEvi :: forall a. Dupable a :- DupableScope (ToT a)
dupableEvi :: Dupable a :- DupableScope (ToT a)
dupableEvi =
  ProperDupableBetterErrors (ToT a) :- DupableScope (ToT a)
forall (t :: T). ProperDupableBetterErrors t :- DupableScope t
properDupableEvi @(ToT a) (ProperDupableBetterErrors (ToT a) :- DupableScope (ToT a))
-> (Dupable a :- ProperDupableBetterErrors (ToT a))
-> Dupable a :- DupableScope (ToT a)
forall (b :: Constraint) (c :: Constraint) (a :: Constraint).
(b :- c) -> (a :- b) -> a :- c
`trans` Dupable a :- ProperDupableBetterErrors (ToT a)
forall (a :: Constraint) (b :: Constraint). (a, b) :- a
weaken1

nicePackedValueEvi :: forall a. NicePackedValue a :- PackedValScope (ToT a)
nicePackedValueEvi :: NicePackedValue a :- PackedValScope (ToT a)
nicePackedValueEvi =
  ProperPackedValBetterErrors (ToT a) :- PackedValScope (ToT a)
forall (t :: T). ProperPackedValBetterErrors t :- PackedValScope t
properPackedValEvi @(ToT a) (ProperPackedValBetterErrors (ToT a) :- PackedValScope (ToT a))
-> (NicePackedValue a :- ProperPackedValBetterErrors (ToT a))
-> NicePackedValue a :- PackedValScope (ToT a)
forall (b :: Constraint) (c :: Constraint) (a :: Constraint).
(b :- c) -> (a :- b) -> a :- c
`trans` NicePackedValue a :- ProperPackedValBetterErrors (ToT a)
forall (a :: Constraint) (b :: Constraint). (a, b) :- a
weaken1

niceUnpackedValueEvi :: forall a. NiceUnpackedValue a :- UnpackedValScope (ToT a)
niceUnpackedValueEvi :: NiceUnpackedValue a :- UnpackedValScope (ToT a)
niceUnpackedValueEvi =
  ProperUnpackedValBetterErrors (ToT a) :- UnpackedValScope (ToT a)
forall (t :: T).
ProperUnpackedValBetterErrors t :- UnpackedValScope t
properUnpackedValEvi @(ToT a) (ProperUnpackedValBetterErrors (ToT a) :- UnpackedValScope (ToT a))
-> (NiceUnpackedValue a :- ProperUnpackedValBetterErrors (ToT a))
-> NiceUnpackedValue a :- UnpackedValScope (ToT a)
forall (b :: Constraint) (c :: Constraint) (a :: Constraint).
(b :- c) -> (a :- b) -> a :- c
`trans` NiceUnpackedValue a :- ProperUnpackedValBetterErrors (ToT a)
forall (a :: Constraint) (b :: Constraint). (a, b) :- a
weaken1

nicePrintedValueEvi :: forall a. NicePrintedValue a :- PrintedValScope (ToT a)
nicePrintedValueEvi :: NicePrintedValue a :- PrintedValScope (ToT a)
nicePrintedValueEvi =
  ProperPrintedValBetterErrors (ToT a) :- PrintedValScope (ToT a)
forall (t :: T).
ProperPrintedValBetterErrors t :- PrintedValScope t
properPrintedValEvi @(ToT a) (ProperPrintedValBetterErrors (ToT a) :- PrintedValScope (ToT a))
-> (NicePrintedValue a :- ProperPrintedValBetterErrors (ToT a))
-> NicePrintedValue a :- PrintedValScope (ToT a)
forall (b :: Constraint) (c :: Constraint) (a :: Constraint).
(b :- c) -> (a :- b) -> a :- c
`trans` NicePrintedValue a :- ProperPrintedValBetterErrors (ToT a)
forall (a :: Constraint) (b :: Constraint). (a, b) :- a
weaken1