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

{-# OPTIONS_HADDOCK not-home #-}

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

import Data.Singletons (Sing)

import Data.Type.Equality ((:~:)(..))
import Morley.Michelson.Typed.Scope.Internal.ForbidT
import Morley.Michelson.Typed.Scope.Internal.TH
import Morley.Michelson.Typed.Sing (SingT(..))
import Morley.Michelson.Typed.T (T(..))

{- $setup
>>> import Morley.Michelson.Typed (T(..), SingT(..), SingTPredicateSym(..))
>>> import Morley.Util.Peano (pattern S, pattern Z)
>>> import Data.Type.Equality ((:~:)(..))
-}

-- | Whether a value of this type _may_ contain a type defined by 'TPredicateSym'.
type TPresence :: TPredicateSym -> T -> Type
data TPresence p t where
  TPresent :: ContainsT p t ~ 'True => TPresence p t
  TAbsent :: ContainsT p t ~ 'False => TPresence p t

deriving stock instance Show (TPresence t p)

{- | Check for presence of type defined by 'TPredicateSym' at runtime. Use
'TPredicateSym' singletons (i.e. 'SingTPredicateSym') as the first parameter,
e.g.:

>>> checkTPresence SPSOp STOperation
TPresent
>>> checkTPresence SPSOp STUnit
TAbsent

To only prove absence of some type, it is more efficient to use
@deMorganForbidT@ or @withDeMorganScope@.
-}
checkTPresence
  :: forall p ty. Sing p
  -> Sing ty
  -> TPresence p ty
checkTPresence sp = \case
  STOption t -> case checkTPresence sp t of
    TPresent -> TPresent
    TAbsent -> TAbsent
  STList t -> $(byTPredicateSymCases [|sp|]
    [ ('SPSNonComparable, [|TPresent|]) ]
    [|case checkTPresence sp t of
        TPresent -> TPresent
        TAbsent -> TAbsent
    |])
  STSet t -> $(byTPredicateSymCases [|sp|]
    [ ('SPSNonComparable, [|TPresent|]) ]
    [|case checkTPresence sp t of
        TPresent -> TPresent
        TAbsent -> TAbsent
    |])
  STTicket t -> $(byTPredicateSymCases [|sp|]
    [ ('SPSTicket, [|TPresent|])
    , ('SPSNonComparable, [|TPresent|])
    ]
    [|case checkTPresence sp t of
        TPresent -> TPresent
        TAbsent -> TAbsent
    |]
    )
  STPair a b -> case checkTPresence sp a of
    TPresent -> TPresent
    TAbsent -> case checkTPresence sp b of
      TPresent -> TPresent
      TAbsent -> TAbsent
  STOr a b -> case checkTPresence sp a of
    TPresent -> TPresent
    TAbsent -> case checkTPresence sp b of
      TPresent -> TPresent
      TAbsent -> TAbsent
  STMap a b -> $(byTPredicateSymCases [|sp|]
    [ ('SPSNonComparable, [|TPresent|])]
    [|case checkTPresence sp a of
        TPresent -> TPresent
        TAbsent -> case checkTPresence sp b of
          TPresent -> TPresent
          TAbsent -> TAbsent
    |])
  STBigMap a b -> $(byTPredicateSymCases [|sp|]
    [ ('SPSBigMap, [|TPresent|])
    , ('SPSNonComparable, [|TPresent|])
    , ('SPSNestedBigMaps, [|
          case checkTPresence SPSBigMap b of
            TPresent -> TPresent
            TAbsent -> TAbsent
          |])
    ]
    [|case checkTPresence sp a of
        TPresent -> TPresent
        TAbsent -> case checkTPresence sp b of
          TPresent -> TPresent
          TAbsent -> TAbsent
    |]
    )
  -- special cases
  STOperation ->
    $(byTPredicateSymCases [|sp|]
      [('SPSOp, [|TPresent|]), ('SPSNonComparable, [|TPresent|])]
      [|TAbsent|])
  STContract{} ->
    $(byTPredicateSymCases [|sp|]
      [('SPSContract, [|TPresent|]), ('SPSNonComparable, [|TPresent|])]
      [|TAbsent|])
  STSaplingState{} ->
    $(byTPredicateSymCases [|sp|]
      [('SPSSaplingState, [|TPresent|]), ('SPSNonComparable, [|TPresent|])]
      [|TAbsent|])
  -- rest
  STKey -> TAbsent
  STUnit -> TAbsent
  STSignature -> TAbsent
  STChainId -> TAbsent
  STInt -> TAbsent
  STNat -> TAbsent
  STString -> TAbsent
  STBytes -> TAbsent
  STMutez -> TAbsent
  STBool -> TAbsent
  STKeyHash -> TAbsent
  STBls12381Fr -> $(byTPredicateSymCases [|sp|] [('SPSNonComparable, [|TPresent|])] [|TAbsent|])
  STBls12381G1 -> $(byTPredicateSymCases [|sp|] [('SPSNonComparable, [|TPresent|])] [|TAbsent|])
  STBls12381G2 -> $(byTPredicateSymCases [|sp|] [('SPSNonComparable, [|TPresent|])] [|TAbsent|])
  STTimestamp -> TAbsent
  STAddress -> TAbsent
  STChest -> $(byTPredicateSymCases [|sp|] [('SPSNonComparable, [|TPresent|])] [|TAbsent|])
  STChestKey -> $(byTPredicateSymCases [|sp|] [('SPSNonComparable, [|TPresent|])] [|TAbsent|])
  STSaplingTransaction _ ->
    $(byTPredicateSymCases [|sp|] [('SPSNonComparable, [|TPresent|])] [|TAbsent|])
  STNever -> TAbsent
  STLambda{} -> $(byTPredicateSymCases [|sp|] [('SPSNonComparable, [|TPresent|])] [|TAbsent|])

tPresence :: Sing p -> Sing t -> Maybe (ContainsT p t :~: 'True)
tPresence p t = case checkTPresence p t of
  TPresent -> Just Refl
  TAbsent -> Nothing

tAbsence :: Sing p -> Sing t -> Maybe (ContainsT p t :~: 'False)
tAbsence p t = case checkTPresence p t of
  TPresent -> Nothing
  TAbsent -> Just Refl