-- 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 _ = Dict
  \\ proofImplOne SPSOp
  \\ proofImplOne SPSNestedBigMaps
  \\ proofImplOne SPSBigMap
  \\ proofImplOne SPSTicket
  \\ proofImplOne SPSSaplingState
  \\ proofImplOne SPSContract
  where
    proofImplOne :: Sing p -> ContainsT p t :~: 'False
    proofImplOne sp = stubProof $ case checkComparability (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.
      CanBeCompared -> case sp of
        SPSOp            -> Refl
        SPSContract      -> Refl
        SPSTicket        -> Refl
        SPSBigMap        -> Refl
        SPSNestedBigMaps -> Refl
        SPSSaplingState  -> Refl
        SPSNonComparable -> 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 = \case
  STPair a b -> case (checkComparability a, checkComparability b) of
    (CanBeCompared, CanBeCompared) -> CanBeCompared
    (CannotBeCompared, _) -> CannotBeCompared
    (_, CannotBeCompared) -> CannotBeCompared
  STOr a b -> case (checkComparability a, checkComparability b) of
    (CanBeCompared, CanBeCompared) -> CanBeCompared
    (CannotBeCompared, _) -> CannotBeCompared
    (_, CannotBeCompared) -> CannotBeCompared
  STOption t -> case checkComparability t of
    CanBeCompared -> CanBeCompared
    CannotBeCompared -> CannotBeCompared
  STList _ -> CannotBeCompared
  STSet _ -> CannotBeCompared
  STOperation -> CannotBeCompared
  STContract _ -> CannotBeCompared
  STTicket _ -> CannotBeCompared
  STLambda _ _ -> CannotBeCompared
  STMap _ _ -> CannotBeCompared
  STBigMap _ _ -> CannotBeCompared
  STNever -> CanBeCompared
  STUnit -> CanBeCompared
  STInt -> CanBeCompared
  STNat -> CanBeCompared
  STString -> CanBeCompared
  STBytes -> CanBeCompared
  STMutez -> CanBeCompared
  STBool -> CanBeCompared
  STKeyHash -> CanBeCompared
  STBls12381Fr -> CannotBeCompared
  STBls12381G1 -> CannotBeCompared
  STBls12381G2 -> CannotBeCompared
  STTimestamp -> CanBeCompared
  STAddress -> CanBeCompared
  STKey -> CanBeCompared
  STSignature -> CanBeCompared
  STChainId -> CanBeCompared
  STChest -> CannotBeCompared
  STChestKey -> CannotBeCompared
  STSaplingState _ -> CannotBeCompared
  STSaplingTransaction _ -> 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 s = case checkComparability s of
  CanBeCompared -> Just Dict
  CannotBeCompared -> Nothing