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

{-# OPTIONS_HADDOCK not-home #-}

module Morley.Michelson.Typed.Scope.Internal.WithDeMorganScope
  ( module Morley.Michelson.Typed.Scope.Internal.WithDeMorganScope
  ) where

import Data.Constraint ((\\))
import Data.Singletons (Sing, SingI(..))
import Data.Type.Bool (type (||))

import Data.Type.Equality ((:~:)(..))
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.T (T(..))
import Morley.Util.StubbedProof (stubProof)

-- | Allows using a scope that can be proven true with a De Morgan law.
--
-- Many scopes are defined as @not a@ (or rather @a ~ 'False@) where @a@ is a
-- negative property we want to avoid as a 'Constraint'.
-- The negative constraints are implemented with a type family that for some
-- combination types resolves to itself applied to the type arguments in an @or@,
-- e.g. A @pair l r@ has @x@ if @l@ or @r@ contain @x@.
--
-- Because of the De Morgan laws @not (a or b)@ implies @(not a) and (not b)@
-- or in our case: @pair@ does not contain @x@ -> @a@ and @b@ don't contain @x@.
class WithDeMorganScope (c :: T -> Constraint) t a b where
  withDeMorganScope :: c (t a b) => ((c a, c b) => ret) -> ret

-- | When a class looks like
--
-- @
-- class (SomeTypeFamily t ~ 'False, ...) => TheClass t
-- instance (SomeTypeFamily t ~ 'False, ...) => TheClass t
-- @
--
-- and the additional constraints are satisfied by the instance constraints of
-- the 'WithDeMorganScope' instance for @TheClass@, we can use
-- `simpleWithDeMorgan` to define 'withDeMorganScope' for the instance.
simpleWithDeMorgan
  :: forall a b ret op.
     ((ContainsT op a || ContainsT op b) ~ 'False, SingI a)
  => Sing op
  -> ((ContainsT op a ~ 'False, ContainsT op b ~ 'False) => ret)
  -> ret
-- Note: If we're lucky, GHC might not build `SingI a` and `SingI op` dictionaries.
simpleWithDeMorgan sop = simpleWithDeMorgan' @b sop (sing @a)

simpleWithDeMorgan'
  :: forall b ret op a.
     ((ContainsT op a || ContainsT op b) ~ 'False)
  => Sing op
  -> Sing a
  -> ((ContainsT op a ~ 'False, ContainsT op b ~ 'False) => ret)
  -> ret
simpleWithDeMorgan' sop sa f = f \\
  stubProof @(ContainsT op b) @'False
    case checkTPresence sop sa of
      TAbsent -> Refl

-- | Simpler version of 'withDeMorganScope' for 'ForbidT' constraints.
deMorganForbidT
  :: forall a b r p. (ContainsT p a || ContainsT p b) ~ 'False
  => Sing p
  -> Sing a
  -> Sing b
  -> ((ForbidT p a, ForbidT p b) => r)
  -> r
deMorganForbidT p a _ f = simpleWithDeMorgan' @b p a f

instance (SingI a, SingI p) => WithDeMorganScope (ForbidT p) 'TPair a b where
  withDeMorganScope f = simpleWithDeMorgan @a @b (sing @p) f
instance (SingI a, SingI p) => WithDeMorganScope (ForbidT p) 'TOr a b where
  withDeMorganScope f = simpleWithDeMorgan @a @b (sing @p) f
instance (SingI k, SingI p) => WithDeMorganScope (ForbidT p) 'TMap k v where
  withDeMorganScope f = case sp of
    SPSOp -> simpleWithDeMorgan @k @v sp f
    SPSContract -> simpleWithDeMorgan @k @v sp f
    SPSTicket -> simpleWithDeMorgan @k @v sp f
    SPSBigMap -> simpleWithDeMorgan @k @v sp f
    SPSNestedBigMaps -> simpleWithDeMorgan @k @v sp f
    SPSSaplingState -> simpleWithDeMorgan @k @v sp f
    where sp = sing @p

-- NB: BigMap is special because de Morgan rule not applicable to NestedBigMaps
-- here.
instance (SingI k) => WithDeMorganScope ForbidOp 'TBigMap k v where
  withDeMorganScope f = simpleWithDeMorgan @k @v SPSOp f
instance (SingI k) => WithDeMorganScope ForbidContract 'TBigMap k v where
  withDeMorganScope f = simpleWithDeMorgan @k @v SPSContract f
instance (SingI k) => WithDeMorganScope ForbidTicket 'TBigMap k v where
  withDeMorganScope f = simpleWithDeMorgan @k @v SPSTicket f
instance (SingI k) => WithDeMorganScope ForbidSaplingState 'TBigMap k v where
  withDeMorganScope f = simpleWithDeMorgan @k @v SPSSaplingState f

instance
  ( WithDeMorganScope ForbidOp t a b
  , WithDeMorganScope ForbidNestedBigMaps t a b
  , WellTyped a, WellTyped b
  ) => WithDeMorganScope ParameterScope t a b where
  withDeMorganScope f =
    withDeMorganScope @ForbidOp @t @a @b $
    withDeMorganScope @ForbidNestedBigMaps @t @a @b f

instance
  ( WithDeMorganScope ForbidOp t a b
  , WithDeMorganScope ForbidNestedBigMaps t a b
  , WithDeMorganScope ForbidContract t a b
  , WellTyped a, WellTyped b
  ) => WithDeMorganScope StorageScope t a b where
  withDeMorganScope f =
    withDeMorganScope @ForbidOp @t @a @b $
    withDeMorganScope @ForbidNestedBigMaps @t @a @b $
    withDeMorganScope @ForbidContract @t @a @b f

instance
  ( WithDeMorganScope ForbidOp t a b
  , WithDeMorganScope ForbidBigMap t a b
  , WithDeMorganScope ForbidContract t a b
  , WithDeMorganScope ForbidTicket t a b
  , WithDeMorganScope ForbidSaplingState t a b
  , WellTyped a, WellTyped b
  ) => WithDeMorganScope ConstantScope t a b where
  withDeMorganScope f =
    withDeMorganScope @ForbidOp @t @a @b $
    withDeMorganScope @ForbidBigMap @t @a @b $
    withDeMorganScope @ForbidContract @t @a @b $
    withDeMorganScope @ForbidTicket @t @a @b $
    withDeMorganScope @ForbidSaplingState @t @a @b f

instance
  ( WithDeMorganScope ForbidOp t a b
  , WithDeMorganScope ForbidBigMap t a b
  , WithDeMorganScope ForbidTicket t a b
  , WithDeMorganScope ForbidSaplingState t a b
  , WellTyped a, WellTyped b
  ) => WithDeMorganScope PackedValScope t a b where
  withDeMorganScope f =
    withDeMorganScope @ForbidOp @t @a @b $
    withDeMorganScope @ForbidBigMap @t @a @b $
    withDeMorganScope @ForbidTicket @t @a @b $
    withDeMorganScope @ForbidSaplingState @t @a @b f