-- 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 :: forall (a :: T) (b :: T) ret (op :: TPredicateSym).
((ContainsT op a || ContainsT op b) ~ 'False, SingI a) =>
Sing op
-> ((ContainsT op a ~ 'False, ContainsT op b ~ 'False) => ret)
-> ret
simpleWithDeMorgan Sing op
sop = forall (b :: T) ret (op :: TPredicateSym) (a :: T).
((ContainsT op a || ContainsT op b) ~ 'False) =>
Sing op
-> Sing a
-> ((ContainsT op a ~ 'False, ContainsT op b ~ 'False) => ret)
-> ret
simpleWithDeMorgan' @b Sing op
sop (forall {k} (a :: k). SingI a => Sing a
forall (a :: T). SingI a => Sing a
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' :: forall (b :: T) ret (op :: TPredicateSym) (a :: T).
((ContainsT op a || ContainsT op b) ~ 'False) =>
Sing op
-> Sing a
-> ((ContainsT op a ~ 'False, ContainsT op b ~ 'False) => ret)
-> ret
simpleWithDeMorgan' Sing op
sop Sing a
sa (ContainsT op a ~ 'False, ContainsT op b ~ 'False) => ret
f = ret
(ContainsT op b ~ 'False) => ret
(ContainsT op a ~ 'False, ContainsT op b ~ 'False) => ret
f ((ContainsT op b ~ 'False) => ret)
-> (ContainsT op b :~: 'False) -> ret
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\
  forall (a :: Bool) (b :: Bool). (Stubbed => a :~: b) -> a :~: b
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof @(ContainsT op b) @'False
    case Sing op -> Sing a -> TPresence op a
forall (p :: TPredicateSym) (ty :: T).
Sing p -> Sing ty -> TPresence p ty
checkTPresence Sing op
sop Sing a
sa of
      TPresence op a
TAbsent -> 'False :~: 'False
ContainsT op b :~: 'False
forall {k} (a :: k). a :~: a
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 :: forall (a :: T) (b :: T) r (p :: TPredicateSym).
((ContainsT p a || ContainsT p b) ~ 'False) =>
Sing p
-> Sing a -> Sing b -> ((ForbidT p a, ForbidT p b) => r) -> r
deMorganForbidT Sing p
p Sing a
a Sing b
_ (ForbidT p a, ForbidT p b) => r
f = forall (b :: T) ret (op :: TPredicateSym) (a :: T).
((ContainsT op a || ContainsT op b) ~ 'False) =>
Sing op
-> Sing a
-> ((ContainsT op a ~ 'False, ContainsT op b ~ 'False) => ret)
-> ret
simpleWithDeMorgan' @b Sing p
p Sing a
a r
(ContainsT p a ~ 'False, ContainsT p b ~ 'False) => r
(ForbidT p a, ForbidT p b) => r
f

instance (SingI a, SingI p) => WithDeMorganScope (ForbidT p) 'TPair a b where
  withDeMorganScope :: forall ret.
ForbidT p ('TPair a b) =>
((ForbidT p a, ForbidT p b) => ret) -> ret
withDeMorganScope (ForbidT p a, ForbidT p b) => ret
f = forall (a :: T) (b :: T) ret (op :: TPredicateSym).
((ContainsT op a || ContainsT op b) ~ 'False, SingI a) =>
Sing op
-> ((ContainsT op a ~ 'False, ContainsT op b ~ 'False) => ret)
-> ret
simpleWithDeMorgan @a @b (forall {k} (a :: k). SingI a => Sing a
forall (a :: TPredicateSym). SingI a => Sing a
sing @p) ret
(ContainsT p a ~ 'False, ContainsT p b ~ 'False) => ret
(ForbidT p a, ForbidT p b) => ret
f
instance (SingI a, SingI p) => WithDeMorganScope (ForbidT p) 'TOr a b where
  withDeMorganScope :: forall ret.
ForbidT p ('TOr a b) =>
((ForbidT p a, ForbidT p b) => ret) -> ret
withDeMorganScope (ForbidT p a, ForbidT p b) => ret
f = forall (a :: T) (b :: T) ret (op :: TPredicateSym).
((ContainsT op a || ContainsT op b) ~ 'False, SingI a) =>
Sing op
-> ((ContainsT op a ~ 'False, ContainsT op b ~ 'False) => ret)
-> ret
simpleWithDeMorgan @a @b (forall {k} (a :: k). SingI a => Sing a
forall (a :: TPredicateSym). SingI a => Sing a
sing @p) ret
(ContainsT p a ~ 'False, ContainsT p b ~ 'False) => ret
(ForbidT p a, ForbidT p b) => ret
f
instance (SingI k, SingI p) => WithDeMorganScope (ForbidT p) 'TMap k v where
  withDeMorganScope :: forall ret.
ForbidT p ('TMap k v) =>
((ForbidT p k, ForbidT p v) => ret) -> ret
withDeMorganScope (ForbidT p k, ForbidT p v) => ret
f = case Sing p
sp of
    Sing p
SingTPredicateSym p
SPSOp -> forall (a :: T) (b :: T) ret (op :: TPredicateSym).
((ContainsT op a || ContainsT op b) ~ 'False, SingI a) =>
Sing op
-> ((ContainsT op a ~ 'False, ContainsT op b ~ 'False) => ret)
-> ret
simpleWithDeMorgan @k @v Sing p
Sing 'PSOp
sp ret
(ContainsT 'PSOp k ~ 'False, ContainsT 'PSOp v ~ 'False) => ret
(ForbidT p k, ForbidT p v) => ret
f
    Sing p
SingTPredicateSym p
SPSContract -> forall (a :: T) (b :: T) ret (op :: TPredicateSym).
((ContainsT op a || ContainsT op b) ~ 'False, SingI a) =>
Sing op
-> ((ContainsT op a ~ 'False, ContainsT op b ~ 'False) => ret)
-> ret
simpleWithDeMorgan @k @v Sing p
Sing 'PSContract
sp ret
(ContainsT 'PSContract k ~ 'False,
 ContainsT 'PSContract v ~ 'False) =>
ret
(ForbidT p k, ForbidT p v) => ret
f
    Sing p
SingTPredicateSym p
SPSTicket -> forall (a :: T) (b :: T) ret (op :: TPredicateSym).
((ContainsT op a || ContainsT op b) ~ 'False, SingI a) =>
Sing op
-> ((ContainsT op a ~ 'False, ContainsT op b ~ 'False) => ret)
-> ret
simpleWithDeMorgan @k @v Sing p
Sing 'PSTicket
sp ret
(ContainsT 'PSTicket k ~ 'False, ContainsT 'PSTicket v ~ 'False) =>
ret
(ForbidT p k, ForbidT p v) => ret
f
    Sing p
SingTPredicateSym p
SPSBigMap -> forall (a :: T) (b :: T) ret (op :: TPredicateSym).
((ContainsT op a || ContainsT op b) ~ 'False, SingI a) =>
Sing op
-> ((ContainsT op a ~ 'False, ContainsT op b ~ 'False) => ret)
-> ret
simpleWithDeMorgan @k @v Sing p
Sing 'PSBigMap
sp ret
(ContainsT 'PSBigMap k ~ 'False, ContainsT 'PSBigMap v ~ 'False) =>
ret
(ForbidT p k, ForbidT p v) => ret
f
    Sing p
SingTPredicateSym p
SPSNestedBigMaps -> forall (a :: T) (b :: T) ret (op :: TPredicateSym).
((ContainsT op a || ContainsT op b) ~ 'False, SingI a) =>
Sing op
-> ((ContainsT op a ~ 'False, ContainsT op b ~ 'False) => ret)
-> ret
simpleWithDeMorgan @k @v Sing p
Sing 'PSNestedBigMaps
sp ret
(ContainsT 'PSNestedBigMaps k ~ 'False,
 ContainsT 'PSNestedBigMaps v ~ 'False) =>
ret
(ForbidT p k, ForbidT p v) => ret
f
    Sing p
SingTPredicateSym p
SPSSaplingState -> forall (a :: T) (b :: T) ret (op :: TPredicateSym).
((ContainsT op a || ContainsT op b) ~ 'False, SingI a) =>
Sing op
-> ((ContainsT op a ~ 'False, ContainsT op b ~ 'False) => ret)
-> ret
simpleWithDeMorgan @k @v Sing p
Sing 'PSSaplingState
sp ret
(ContainsT 'PSSaplingState k ~ 'False,
 ContainsT 'PSSaplingState v ~ 'False) =>
ret
(ForbidT p k, ForbidT p v) => ret
f
    where sp :: Sing p
sp = forall {k} (a :: k). SingI a => Sing a
forall (a :: TPredicateSym). SingI a => Sing a
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 :: forall ret.
ForbidOp ('TBigMap k v) =>
((ForbidOp k, ForbidOp v) => ret) -> ret
withDeMorganScope (ForbidOp k, ForbidOp v) => ret
f = forall (a :: T) (b :: T) ret (op :: TPredicateSym).
((ContainsT op a || ContainsT op b) ~ 'False, SingI a) =>
Sing op
-> ((ContainsT op a ~ 'False, ContainsT op b ~ 'False) => ret)
-> ret
simpleWithDeMorgan @k @v Sing 'PSOp
SingTPredicateSym 'PSOp
SPSOp ret
(ContainsT 'PSOp k ~ 'False, ContainsT 'PSOp v ~ 'False) => ret
(ForbidOp k, ForbidOp v) => ret
f
instance (SingI k) => WithDeMorganScope ForbidContract 'TBigMap k v where
  withDeMorganScope :: forall ret.
ForbidContract ('TBigMap k v) =>
((ForbidContract k, ForbidContract v) => ret) -> ret
withDeMorganScope (ForbidContract k, ForbidContract v) => ret
f = forall (a :: T) (b :: T) ret (op :: TPredicateSym).
((ContainsT op a || ContainsT op b) ~ 'False, SingI a) =>
Sing op
-> ((ContainsT op a ~ 'False, ContainsT op b ~ 'False) => ret)
-> ret
simpleWithDeMorgan @k @v Sing 'PSContract
SingTPredicateSym 'PSContract
SPSContract ret
(ContainsT 'PSContract k ~ 'False,
 ContainsT 'PSContract v ~ 'False) =>
ret
(ForbidContract k, ForbidContract v) => ret
f
instance (SingI k) => WithDeMorganScope ForbidTicket 'TBigMap k v where
  withDeMorganScope :: forall ret.
ForbidTicket ('TBigMap k v) =>
((ForbidTicket k, ForbidTicket v) => ret) -> ret
withDeMorganScope (ForbidTicket k, ForbidTicket v) => ret
f = forall (a :: T) (b :: T) ret (op :: TPredicateSym).
((ContainsT op a || ContainsT op b) ~ 'False, SingI a) =>
Sing op
-> ((ContainsT op a ~ 'False, ContainsT op b ~ 'False) => ret)
-> ret
simpleWithDeMorgan @k @v Sing 'PSTicket
SingTPredicateSym 'PSTicket
SPSTicket ret
(ContainsT 'PSTicket k ~ 'False, ContainsT 'PSTicket v ~ 'False) =>
ret
(ForbidTicket k, ForbidTicket v) => ret
f
instance (SingI k) => WithDeMorganScope ForbidSaplingState 'TBigMap k v where
  withDeMorganScope :: forall ret.
ForbidSaplingState ('TBigMap k v) =>
((ForbidSaplingState k, ForbidSaplingState v) => ret) -> ret
withDeMorganScope (ForbidSaplingState k, ForbidSaplingState v) => ret
f = forall (a :: T) (b :: T) ret (op :: TPredicateSym).
((ContainsT op a || ContainsT op b) ~ 'False, SingI a) =>
Sing op
-> ((ContainsT op a ~ 'False, ContainsT op b ~ 'False) => ret)
-> ret
simpleWithDeMorgan @k @v Sing 'PSSaplingState
SingTPredicateSym 'PSSaplingState
SPSSaplingState ret
(ContainsT 'PSSaplingState k ~ 'False,
 ContainsT 'PSSaplingState v ~ 'False) =>
ret
(ForbidSaplingState k, ForbidSaplingState v) => ret
f

instance
  ( WithDeMorganScope ForbidOp t a b
  , WithDeMorganScope ForbidNestedBigMaps t a b
  , WellTyped a, WellTyped b
  ) => WithDeMorganScope ParameterScope t a b where
  withDeMorganScope :: forall ret.
ParameterScope (t a b) =>
((ParameterScope a, ParameterScope b) => ret) -> ret
withDeMorganScope (ParameterScope a, ParameterScope b) => ret
f =
    forall (c :: T -> Constraint) (t :: T -> T -> T) (a :: T) (b :: T)
       ret.
(WithDeMorganScope c t a b, c (t a b)) =>
((c a, c b) => ret) -> ret
withDeMorganScope @ForbidOp @t @a @b (((ForbidOp a, ForbidOp b) => ret) -> ret)
-> ((ForbidOp a, ForbidOp b) => ret) -> ret
forall a b. (a -> b) -> a -> b
$
    forall (c :: T -> Constraint) (t :: T -> T -> T) (a :: T) (b :: T)
       ret.
(WithDeMorganScope c t a b, c (t a b)) =>
((c a, c b) => ret) -> ret
withDeMorganScope @ForbidNestedBigMaps @t @a @b ret
(ForbidNestedBigMaps a, ForbidNestedBigMaps b) => ret
(ParameterScope a, ParameterScope b) => ret
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 :: forall ret.
StorageScope (t a b) =>
((StorageScope a, StorageScope b) => ret) -> ret
withDeMorganScope (StorageScope a, StorageScope b) => ret
f =
    forall (c :: T -> Constraint) (t :: T -> T -> T) (a :: T) (b :: T)
       ret.
(WithDeMorganScope c t a b, c (t a b)) =>
((c a, c b) => ret) -> ret
withDeMorganScope @ForbidOp @t @a @b (((ForbidOp a, ForbidOp b) => ret) -> ret)
-> ((ForbidOp a, ForbidOp b) => ret) -> ret
forall a b. (a -> b) -> a -> b
$
    forall (c :: T -> Constraint) (t :: T -> T -> T) (a :: T) (b :: T)
       ret.
(WithDeMorganScope c t a b, c (t a b)) =>
((c a, c b) => ret) -> ret
withDeMorganScope @ForbidNestedBigMaps @t @a @b (((ForbidNestedBigMaps a, ForbidNestedBigMaps b) => ret) -> ret)
-> ((ForbidNestedBigMaps a, ForbidNestedBigMaps b) => ret) -> ret
forall a b. (a -> b) -> a -> b
$
    forall (c :: T -> Constraint) (t :: T -> T -> T) (a :: T) (b :: T)
       ret.
(WithDeMorganScope c t a b, c (t a b)) =>
((c a, c b) => ret) -> ret
withDeMorganScope @ForbidContract @t @a @b ret
(ForbidContract a, ForbidContract b) => ret
(StorageScope a, StorageScope b) => ret
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 :: forall ret.
ConstantScope (t a b) =>
((ConstantScope a, ConstantScope b) => ret) -> ret
withDeMorganScope (ConstantScope a, ConstantScope b) => ret
f =
    forall (c :: T -> Constraint) (t :: T -> T -> T) (a :: T) (b :: T)
       ret.
(WithDeMorganScope c t a b, c (t a b)) =>
((c a, c b) => ret) -> ret
withDeMorganScope @ForbidOp @t @a @b (((ForbidOp a, ForbidOp b) => ret) -> ret)
-> ((ForbidOp a, ForbidOp b) => ret) -> ret
forall a b. (a -> b) -> a -> b
$
    forall (c :: T -> Constraint) (t :: T -> T -> T) (a :: T) (b :: T)
       ret.
(WithDeMorganScope c t a b, c (t a b)) =>
((c a, c b) => ret) -> ret
withDeMorganScope @ForbidBigMap @t @a @b (((ForbidBigMap a, ForbidBigMap b) => ret) -> ret)
-> ((ForbidBigMap a, ForbidBigMap b) => ret) -> ret
forall a b. (a -> b) -> a -> b
$
    forall (c :: T -> Constraint) (t :: T -> T -> T) (a :: T) (b :: T)
       ret.
(WithDeMorganScope c t a b, c (t a b)) =>
((c a, c b) => ret) -> ret
withDeMorganScope @ForbidContract @t @a @b (((ForbidContract a, ForbidContract b) => ret) -> ret)
-> ((ForbidContract a, ForbidContract b) => ret) -> ret
forall a b. (a -> b) -> a -> b
$
    forall (c :: T -> Constraint) (t :: T -> T -> T) (a :: T) (b :: T)
       ret.
(WithDeMorganScope c t a b, c (t a b)) =>
((c a, c b) => ret) -> ret
withDeMorganScope @ForbidTicket @t @a @b (((ForbidTicket a, ForbidTicket b) => ret) -> ret)
-> ((ForbidTicket a, ForbidTicket b) => ret) -> ret
forall a b. (a -> b) -> a -> b
$
    forall (c :: T -> Constraint) (t :: T -> T -> T) (a :: T) (b :: T)
       ret.
(WithDeMorganScope c t a b, c (t a b)) =>
((c a, c b) => ret) -> ret
withDeMorganScope @ForbidSaplingState @t @a @b ret
(ForbidSaplingState a, ForbidSaplingState b) => ret
(ConstantScope a, ConstantScope b) => ret
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 :: forall ret.
PackedValScope (t a b) =>
((PackedValScope a, PackedValScope b) => ret) -> ret
withDeMorganScope (PackedValScope a, PackedValScope b) => ret
f =
    forall (c :: T -> Constraint) (t :: T -> T -> T) (a :: T) (b :: T)
       ret.
(WithDeMorganScope c t a b, c (t a b)) =>
((c a, c b) => ret) -> ret
withDeMorganScope @ForbidOp @t @a @b (((ForbidOp a, ForbidOp b) => ret) -> ret)
-> ((ForbidOp a, ForbidOp b) => ret) -> ret
forall a b. (a -> b) -> a -> b
$
    forall (c :: T -> Constraint) (t :: T -> T -> T) (a :: T) (b :: T)
       ret.
(WithDeMorganScope c t a b, c (t a b)) =>
((c a, c b) => ret) -> ret
withDeMorganScope @ForbidBigMap @t @a @b (((ForbidBigMap a, ForbidBigMap b) => ret) -> ret)
-> ((ForbidBigMap a, ForbidBigMap b) => ret) -> ret
forall a b. (a -> b) -> a -> b
$
    forall (c :: T -> Constraint) (t :: T -> T -> T) (a :: T) (b :: T)
       ret.
(WithDeMorganScope c t a b, c (t a b)) =>
((c a, c b) => ret) -> ret
withDeMorganScope @ForbidTicket @t @a @b (((ForbidTicket a, ForbidTicket b) => ret) -> ret)
-> ((ForbidTicket a, ForbidTicket b) => ret) -> ret
forall a b. (a -> b) -> a -> b
$
    forall (c :: T -> Constraint) (t :: T -> T -> T) (a :: T) (b :: T)
       ret.
(WithDeMorganScope c t a b, c (t a b)) =>
((c a, c b) => ret) -> ret
withDeMorganScope @ForbidSaplingState @t @a @b ret
(ForbidSaplingState a, ForbidSaplingState b) => ret
(PackedValScope a, PackedValScope b) => ret
f