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

{-# OPTIONS_HADDOCK not-home #-}

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

import Data.Constraint (Dict(..), (\\))
import Data.Singletons (Sing, SingI(..))
import Data.Type.Equality ((:~:)(..))

import Morley.Michelson.Typed.Scope.Internal.ForbidT
import Morley.Michelson.Typed.Sing (SingT(..))
import Morley.Michelson.Typed.T (T(..))
import Morley.Util.StubbedProof

{- $setup
>>> import Morley.Michelson.Typed
-}

data Comparability t where
  CanBeCompared :: (Comparable t, ComparabilityImplies t) => Comparability t
  CannotBeCompared :: (ContainsT 'PSNonComparable t ~ 'True) => Comparability t
deriving stock instance Show (Comparability t)

-- | Constraints implied by 'Comparable'. This is a little expensive to carry as
-- the superclass of 'Comparable', hence these can be brought into scope on
-- demand using 'comparableImplies'.
type ComparabilityImplies t =
  ( ForbidOp t
  , ForbidNestedBigMaps t
  , ForbidTicket t
  , ForbidSaplingState t
  , ForbidBigMap t
  , ForbidContract t
  , ForbidNonComparable t
  )

-- | Produce 'ComparabilityImplies' on demand. Carrying it as 'Comparable'
-- superclasses turns out to be a little expensive, considering we can produce
-- evidence on demand in O(1).
comparableImplies
  :: forall t proxy. ForbidNonComparable t
  => proxy t -> Dict (ComparabilityImplies t)
comparableImplies :: forall (t :: T) (proxy :: T -> *).
ForbidNonComparable t =>
proxy t -> Dict (ComparabilityImplies t)
comparableImplies proxy t
_ = Dict (ComparabilityImplies t)
(ContainsT 'PSOp t ~ 'False) => Dict (ComparabilityImplies t)
forall (a :: Constraint). a => Dict a
Dict
  ((ContainsT 'PSOp t ~ 'False) => Dict (ComparabilityImplies t))
-> (ContainsT 'PSOp t :~: 'False) -> Dict (ComparabilityImplies t)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing 'PSOp -> ContainsT 'PSOp t :~: 'False
forall (p :: TPredicateSym). Sing p -> ContainsT p t :~: 'False
proofImplOne Sing 'PSOp
SingTPredicateSym 'PSOp
SPSOp
  ((ContainsT 'PSNestedBigMaps t ~ 'False) =>
 Dict (ComparabilityImplies t))
-> (ContainsT 'PSNestedBigMaps t :~: 'False)
-> Dict (ComparabilityImplies t)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing 'PSNestedBigMaps -> ContainsT 'PSNestedBigMaps t :~: 'False
forall (p :: TPredicateSym). Sing p -> ContainsT p t :~: 'False
proofImplOne Sing 'PSNestedBigMaps
SingTPredicateSym 'PSNestedBigMaps
SPSNestedBigMaps
  ((ContainsT 'PSBigMap t ~ 'False) => Dict (ComparabilityImplies t))
-> (ContainsT 'PSBigMap t :~: 'False)
-> Dict (ComparabilityImplies t)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing 'PSBigMap -> ContainsT 'PSBigMap t :~: 'False
forall (p :: TPredicateSym). Sing p -> ContainsT p t :~: 'False
proofImplOne Sing 'PSBigMap
SingTPredicateSym 'PSBigMap
SPSBigMap
  ((ContainsT 'PSTicket t ~ 'False) => Dict (ComparabilityImplies t))
-> (ContainsT 'PSTicket t :~: 'False)
-> Dict (ComparabilityImplies t)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing 'PSTicket -> ContainsT 'PSTicket t :~: 'False
forall (p :: TPredicateSym). Sing p -> ContainsT p t :~: 'False
proofImplOne Sing 'PSTicket
SingTPredicateSym 'PSTicket
SPSTicket
  ((ContainsT 'PSSaplingState t ~ 'False) =>
 Dict (ComparabilityImplies t))
-> (ContainsT 'PSSaplingState t :~: 'False)
-> Dict (ComparabilityImplies t)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing 'PSSaplingState -> ContainsT 'PSSaplingState t :~: 'False
forall (p :: TPredicateSym). Sing p -> ContainsT p t :~: 'False
proofImplOne Sing 'PSSaplingState
SingTPredicateSym 'PSSaplingState
SPSSaplingState
  ((ContainsT 'PSContract t ~ 'False) =>
 Dict (ComparabilityImplies t))
-> (ContainsT 'PSContract t :~: 'False)
-> Dict (ComparabilityImplies t)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Sing 'PSContract -> ContainsT 'PSContract t :~: 'False
forall (p :: TPredicateSym). Sing p -> ContainsT p t :~: 'False
proofImplOne Sing 'PSContract
SingTPredicateSym 'PSContract
SPSContract
  where
    proofImplOne :: Sing p -> ContainsT p t :~: 'False
    proofImplOne :: forall (p :: TPredicateSym). Sing p -> ContainsT p t :~: 'False
proofImplOne Sing p
sp = (Stubbed => ContainsT p t :~: 'False) -> ContainsT p t :~: 'False
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof ((Stubbed => ContainsT p t :~: 'False) -> ContainsT p t :~: 'False)
-> (Stubbed => ContainsT p t :~: 'False)
-> ContainsT p t :~: 'False
forall a b. (a -> b) -> a -> b
$ case Sing t -> Comparability t
forall (t :: T). Sing t -> Comparability t
checkComparability (forall {k} (x :: k). Stubbed => Sing x
forall {k} (x :: k). Sing x
forall (x :: T). Sing x
assumeSing @t) of
      -- NB: using assumeSing isn't strictly safe in the sense that one can get
      -- unsafeCoerce out of an ill-behaved t and assumeSing, but
      -- ForbidNonComparable traverses t. So if it's not stuck, t is
      -- well-behaved enough for our purposes here, and we can get by witout
      -- requiring SingI.
      Comparability t
CanBeCompared -> case Sing p
sp of
        Sing p
SingTPredicateSym p
SPSOp            -> 'False :~: 'False
ContainsT p t :~: 'False
forall {k} (a :: k). a :~: a
Refl
        Sing p
SingTPredicateSym p
SPSContract      -> 'False :~: 'False
ContainsT p t :~: 'False
forall {k} (a :: k). a :~: a
Refl
        Sing p
SingTPredicateSym p
SPSTicket        -> 'False :~: 'False
ContainsT p t :~: 'False
forall {k} (a :: k). a :~: a
Refl
        Sing p
SingTPredicateSym p
SPSBigMap        -> 'False :~: 'False
ContainsT p t :~: 'False
forall {k} (a :: k). a :~: a
Refl
        Sing p
SingTPredicateSym p
SPSNestedBigMaps -> 'False :~: 'False
ContainsT p t :~: 'False
forall {k} (a :: k). a :~: a
Refl
        Sing p
SingTPredicateSym p
SPSSaplingState  -> 'False :~: 'False
ContainsT p t :~: 'False
forall {k} (a :: k). a :~: a
Refl
        Sing p
SingTPredicateSym p
SPSNonComparable -> 'False :~: 'False
ContainsT p t :~: 'False
forall {k} (a :: k). a :~: a
Refl

-- | Enforce recursive superclass constraints.
type RecSuperC :: (T -> Constraint) -> T -> Constraint
type family RecSuperC c t where
  RecSuperC c (_ t1 t2) = (c t1, c t2)
  RecSuperC c (_ t)     = c t
  RecSuperC _ _ = ()

type Comparable :: T -> Constraint
class (SingI t, RecSuperC Comparable t, ForbidNonComparable t) => Comparable t
instance (SingI t, RecSuperC Comparable t, ForbidNonComparable t) => Comparable t

{- | Check if type is comparable or not at runtime. This traverses the
singleton, so it has a considerable runtime cost. If you just need to convince
GHC, you may be looking for 'comparableImplies', or perhaps
@withDeMorganScope@.

>>> checkComparability STOperation
CannotBeCompared
>>> checkComparability STAddress
CanBeCompared
-}
checkComparability :: Sing t -> Comparability t
checkComparability :: forall (t :: T). Sing t -> Comparability t
checkComparability = \case
  STPair Sing n1
a Sing n2
b -> case (Sing n1 -> Comparability n1
forall (t :: T). Sing t -> Comparability t
checkComparability Sing n1
a, Sing n2 -> Comparability n2
forall (t :: T). Sing t -> Comparability t
checkComparability Sing n2
b) of
    (Comparability n1
CanBeCompared, Comparability n2
CanBeCompared) -> Comparability t
forall (t :: T).
(Comparable t, ComparabilityImplies t) =>
Comparability t
CanBeCompared
    (Comparability n1
CannotBeCompared, Comparability n2
_) -> Comparability t
forall (t :: T).
(ContainsT 'PSNonComparable t ~ 'True) =>
Comparability t
CannotBeCompared
    (Comparability n1
_, Comparability n2
CannotBeCompared) -> Comparability t
forall (t :: T).
(ContainsT 'PSNonComparable t ~ 'True) =>
Comparability t
CannotBeCompared
  STOr Sing n1
a Sing n2
b -> case (Sing n1 -> Comparability n1
forall (t :: T). Sing t -> Comparability t
checkComparability Sing n1
a, Sing n2 -> Comparability n2
forall (t :: T). Sing t -> Comparability t
checkComparability Sing n2
b) of
    (Comparability n1
CanBeCompared, Comparability n2
CanBeCompared) -> Comparability t
forall (t :: T).
(Comparable t, ComparabilityImplies t) =>
Comparability t
CanBeCompared
    (Comparability n1
CannotBeCompared, Comparability n2
_) -> Comparability t
forall (t :: T).
(ContainsT 'PSNonComparable t ~ 'True) =>
Comparability t
CannotBeCompared
    (Comparability n1
_, Comparability n2
CannotBeCompared) -> Comparability t
forall (t :: T).
(ContainsT 'PSNonComparable t ~ 'True) =>
Comparability t
CannotBeCompared
  STOption Sing n
t -> case Sing n -> Comparability n
forall (t :: T). Sing t -> Comparability t
checkComparability Sing n
t of
    Comparability n
CanBeCompared -> Comparability t
forall (t :: T).
(Comparable t, ComparabilityImplies t) =>
Comparability t
CanBeCompared
    Comparability n
CannotBeCompared -> Comparability t
forall (t :: T).
(ContainsT 'PSNonComparable t ~ 'True) =>
Comparability t
CannotBeCompared
  STList Sing n
_ -> Comparability t
forall (t :: T).
(ContainsT 'PSNonComparable t ~ 'True) =>
Comparability t
CannotBeCompared
  STSet Sing n
_ -> Comparability t
forall (t :: T).
(ContainsT 'PSNonComparable t ~ 'True) =>
Comparability t
CannotBeCompared
  Sing t
SingT t
STOperation -> Comparability t
forall (t :: T).
(ContainsT 'PSNonComparable t ~ 'True) =>
Comparability t
CannotBeCompared
  STContract Sing n
_ -> Comparability t
forall (t :: T).
(ContainsT 'PSNonComparable t ~ 'True) =>
Comparability t
CannotBeCompared
  STTicket Sing n
_ -> Comparability t
forall (t :: T).
(ContainsT 'PSNonComparable t ~ 'True) =>
Comparability t
CannotBeCompared
  STLambda Sing n1
_ Sing n2
_ -> Comparability t
forall (t :: T).
(ContainsT 'PSNonComparable t ~ 'True) =>
Comparability t
CannotBeCompared
  STMap Sing n1
_ Sing n2
_ -> Comparability t
forall (t :: T).
(ContainsT 'PSNonComparable t ~ 'True) =>
Comparability t
CannotBeCompared
  STBigMap Sing n1
_ Sing n2
_ -> Comparability t
forall (t :: T).
(ContainsT 'PSNonComparable t ~ 'True) =>
Comparability t
CannotBeCompared
  Sing t
SingT t
STNever -> Comparability t
forall (t :: T).
(Comparable t, ComparabilityImplies t) =>
Comparability t
CanBeCompared
  Sing t
SingT t
STUnit -> Comparability t
forall (t :: T).
(Comparable t, ComparabilityImplies t) =>
Comparability t
CanBeCompared
  Sing t
SingT t
STInt -> Comparability t
forall (t :: T).
(Comparable t, ComparabilityImplies t) =>
Comparability t
CanBeCompared
  Sing t
SingT t
STNat -> Comparability t
forall (t :: T).
(Comparable t, ComparabilityImplies t) =>
Comparability t
CanBeCompared
  Sing t
SingT t
STString -> Comparability t
forall (t :: T).
(Comparable t, ComparabilityImplies t) =>
Comparability t
CanBeCompared
  Sing t
SingT t
STBytes -> Comparability t
forall (t :: T).
(Comparable t, ComparabilityImplies t) =>
Comparability t
CanBeCompared
  Sing t
SingT t
STMutez -> Comparability t
forall (t :: T).
(Comparable t, ComparabilityImplies t) =>
Comparability t
CanBeCompared
  Sing t
SingT t
STBool -> Comparability t
forall (t :: T).
(Comparable t, ComparabilityImplies t) =>
Comparability t
CanBeCompared
  Sing t
SingT t
STKeyHash -> Comparability t
forall (t :: T).
(Comparable t, ComparabilityImplies t) =>
Comparability t
CanBeCompared
  Sing t
SingT t
STBls12381Fr -> Comparability t
forall (t :: T).
(ContainsT 'PSNonComparable t ~ 'True) =>
Comparability t
CannotBeCompared
  Sing t
SingT t
STBls12381G1 -> Comparability t
forall (t :: T).
(ContainsT 'PSNonComparable t ~ 'True) =>
Comparability t
CannotBeCompared
  Sing t
SingT t
STBls12381G2 -> Comparability t
forall (t :: T).
(ContainsT 'PSNonComparable t ~ 'True) =>
Comparability t
CannotBeCompared
  Sing t
SingT t
STTimestamp -> Comparability t
forall (t :: T).
(Comparable t, ComparabilityImplies t) =>
Comparability t
CanBeCompared
  Sing t
SingT t
STAddress -> Comparability t
forall (t :: T).
(Comparable t, ComparabilityImplies t) =>
Comparability t
CanBeCompared
  Sing t
SingT t
STKey -> Comparability t
forall (t :: T).
(Comparable t, ComparabilityImplies t) =>
Comparability t
CanBeCompared
  Sing t
SingT t
STSignature -> Comparability t
forall (t :: T).
(Comparable t, ComparabilityImplies t) =>
Comparability t
CanBeCompared
  Sing t
SingT t
STChainId -> Comparability t
forall (t :: T).
(Comparable t, ComparabilityImplies t) =>
Comparability t
CanBeCompared
  Sing t
SingT t
STChest -> Comparability t
forall (t :: T).
(ContainsT 'PSNonComparable t ~ 'True) =>
Comparability t
CannotBeCompared
  Sing t
SingT t
STChestKey -> Comparability t
forall (t :: T).
(ContainsT 'PSNonComparable t ~ 'True) =>
Comparability t
CannotBeCompared
  STSaplingState Sing n
_ -> Comparability t
forall (t :: T).
(ContainsT 'PSNonComparable t ~ 'True) =>
Comparability t
CannotBeCompared
  STSaplingTransaction Sing n
_ -> Comparability t
forall (t :: T).
(ContainsT 'PSNonComparable t ~ 'True) =>
Comparability t
CannotBeCompared

{- | Check if type is comparable or not at runtime. This is a @Dict@ version of
'checkComparability', so the same caveats apply.

>>> comparabilityPresence STOperation
Nothing
>>> comparabilityPresence STAddress
Just Dict
-}
comparabilityPresence :: Sing t -> Maybe (Dict (Comparable t))
comparabilityPresence :: forall (t :: T). Sing t -> Maybe (Dict (Comparable t))
comparabilityPresence Sing t
s = case Sing t -> Comparability t
forall (t :: T). Sing t -> Comparability t
checkComparability Sing t
s of
  Comparability t
CanBeCompared -> Dict (Comparable t) -> Maybe (Dict (Comparable t))
forall a. a -> Maybe a
Just Dict (Comparable t)
forall (a :: Constraint). a => Dict a
Dict
  Comparability t
CannotBeCompared -> Maybe (Dict (Comparable t))
forall a. Maybe a
Nothing