-- 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 :: forall (p :: TPredicateSym) (ty :: T).
Sing p -> Sing ty -> TPresence p ty
checkTPresence Sing p
sp = \case
  STOption Sing n
t -> case Sing p -> Sing n -> TPresence p n
forall (p :: TPredicateSym) (ty :: T).
Sing p -> Sing ty -> TPresence p ty
checkTPresence Sing p
sp Sing n
t of
    TPresence p n
TPresent -> TPresence p ty
forall (p :: TPredicateSym) (t :: T).
(ContainsT p t ~ 'True) =>
TPresence p t
TPresent
    TPresence p n
TAbsent -> TPresence p ty
forall (p :: TPredicateSym) (t :: T).
(ContainsT p t ~ 'False) =>
TPresence p t
TAbsent
  STList Sing n
t -> $(byTPredicateSymCases [|sp|]
    [ ('SPSNonComparable, [|TPresent|]) ]
    [|case checkTPresence sp t of
        TPresent -> TPresent
        TAbsent -> TAbsent
    |])
  STSet Sing n
t -> $(byTPredicateSymCases [|sp|]
    [ ('SPSNonComparable, [|TPresent|]) ]
    [|case checkTPresence sp t of
        TPresent -> TPresent
        TAbsent -> TAbsent
    |])
  STTicket Sing n
t -> $(byTPredicateSymCases [|sp|]
    [ ('SPSTicket, [|TPresent|])
    , ('SPSNonComparable, [|TPresent|])
    ]
    [|case checkTPresence sp t of
        TPresent -> TPresent
        TAbsent -> TAbsent
    |]
    )
  STPair Sing n1
a Sing n2
b -> case Sing p -> Sing n1 -> TPresence p n1
forall (p :: TPredicateSym) (ty :: T).
Sing p -> Sing ty -> TPresence p ty
checkTPresence Sing p
sp Sing n1
a of
    TPresence p n1
TPresent -> TPresence p ty
forall (p :: TPredicateSym) (t :: T).
(ContainsT p t ~ 'True) =>
TPresence p t
TPresent
    TPresence p n1
TAbsent -> case Sing p -> Sing n2 -> TPresence p n2
forall (p :: TPredicateSym) (ty :: T).
Sing p -> Sing ty -> TPresence p ty
checkTPresence Sing p
sp Sing n2
b of
      TPresence p n2
TPresent -> TPresence p ty
forall (p :: TPredicateSym) (t :: T).
(ContainsT p t ~ 'True) =>
TPresence p t
TPresent
      TPresence p n2
TAbsent -> TPresence p ty
forall (p :: TPredicateSym) (t :: T).
(ContainsT p t ~ 'False) =>
TPresence p t
TAbsent
  STOr Sing n1
a Sing n2
b -> case Sing p -> Sing n1 -> TPresence p n1
forall (p :: TPredicateSym) (ty :: T).
Sing p -> Sing ty -> TPresence p ty
checkTPresence Sing p
sp Sing n1
a of
    TPresence p n1
TPresent -> TPresence p ty
forall (p :: TPredicateSym) (t :: T).
(ContainsT p t ~ 'True) =>
TPresence p t
TPresent
    TPresence p n1
TAbsent -> case Sing p -> Sing n2 -> TPresence p n2
forall (p :: TPredicateSym) (ty :: T).
Sing p -> Sing ty -> TPresence p ty
checkTPresence Sing p
sp Sing n2
b of
      TPresence p n2
TPresent -> TPresence p ty
forall (p :: TPredicateSym) (t :: T).
(ContainsT p t ~ 'True) =>
TPresence p t
TPresent
      TPresence p n2
TAbsent -> TPresence p ty
forall (p :: TPredicateSym) (t :: T).
(ContainsT p t ~ 'False) =>
TPresence p t
TAbsent
  STMap Sing n1
a Sing n2
b -> $(byTPredicateSymCases [|sp|]
    [ ('SPSNonComparable, [|TPresent|])]
    [|case checkTPresence sp a of
        TPresent -> TPresent
        TAbsent -> case checkTPresence sp b of
          TPresent -> TPresent
          TAbsent -> TAbsent
    |])
  STBigMap Sing n1
a Sing n2
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
  Sing ty
SingT ty
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
  Sing ty
SingT ty
STKey -> TPresence p ty
forall (p :: TPredicateSym) (t :: T).
(ContainsT p t ~ 'False) =>
TPresence p t
TAbsent
  Sing ty
SingT ty
STUnit -> TPresence p ty
forall (p :: TPredicateSym) (t :: T).
(ContainsT p t ~ 'False) =>
TPresence p t
TAbsent
  Sing ty
SingT ty
STSignature -> TPresence p ty
forall (p :: TPredicateSym) (t :: T).
(ContainsT p t ~ 'False) =>
TPresence p t
TAbsent
  Sing ty
SingT ty
STChainId -> TPresence p ty
forall (p :: TPredicateSym) (t :: T).
(ContainsT p t ~ 'False) =>
TPresence p t
TAbsent
  Sing ty
SingT ty
STInt -> TPresence p ty
forall (p :: TPredicateSym) (t :: T).
(ContainsT p t ~ 'False) =>
TPresence p t
TAbsent
  Sing ty
SingT ty
STNat -> TPresence p ty
forall (p :: TPredicateSym) (t :: T).
(ContainsT p t ~ 'False) =>
TPresence p t
TAbsent
  Sing ty
SingT ty
STString -> TPresence p ty
forall (p :: TPredicateSym) (t :: T).
(ContainsT p t ~ 'False) =>
TPresence p t
TAbsent
  Sing ty
SingT ty
STBytes -> TPresence p ty
forall (p :: TPredicateSym) (t :: T).
(ContainsT p t ~ 'False) =>
TPresence p t
TAbsent
  Sing ty
SingT ty
STMutez -> TPresence p ty
forall (p :: TPredicateSym) (t :: T).
(ContainsT p t ~ 'False) =>
TPresence p t
TAbsent
  Sing ty
SingT ty
STBool -> TPresence p ty
forall (p :: TPredicateSym) (t :: T).
(ContainsT p t ~ 'False) =>
TPresence p t
TAbsent
  Sing ty
SingT ty
STKeyHash -> TPresence p ty
forall (p :: TPredicateSym) (t :: T).
(ContainsT p t ~ 'False) =>
TPresence p t
TAbsent
  Sing ty
SingT ty
STBls12381Fr -> $(byTPredicateSymCases [|sp|] [('SPSNonComparable, [|TPresent|])] [|TAbsent|])
  Sing ty
SingT ty
STBls12381G1 -> $(byTPredicateSymCases [|sp|] [('SPSNonComparable, [|TPresent|])] [|TAbsent|])
  Sing ty
SingT ty
STBls12381G2 -> $(byTPredicateSymCases [|sp|] [('SPSNonComparable, [|TPresent|])] [|TAbsent|])
  Sing ty
SingT ty
STTimestamp -> TPresence p ty
forall (p :: TPredicateSym) (t :: T).
(ContainsT p t ~ 'False) =>
TPresence p t
TAbsent
  Sing ty
SingT ty
STAddress -> TPresence p ty
forall (p :: TPredicateSym) (t :: T).
(ContainsT p t ~ 'False) =>
TPresence p t
TAbsent
  Sing ty
SingT ty
STChest -> $(byTPredicateSymCases [|sp|] [('SPSNonComparable, [|TPresent|])] [|TAbsent|])
  Sing ty
SingT ty
STChestKey -> $(byTPredicateSymCases [|sp|] [('SPSNonComparable, [|TPresent|])] [|TAbsent|])
  STSaplingTransaction Sing n
_ ->
    $(byTPredicateSymCases [|sp|] [('SPSNonComparable, [|TPresent|])] [|TAbsent|])
  Sing ty
SingT ty
STNever -> TPresence p ty
forall (p :: TPredicateSym) (t :: T).
(ContainsT p t ~ 'False) =>
TPresence p t
TAbsent
  STLambda{} -> $(byTPredicateSymCases [|sp|] [('SPSNonComparable, [|TPresent|])] [|TAbsent|])

tPresence :: Sing p -> Sing t -> Maybe (ContainsT p t :~: 'True)
tPresence :: forall (p :: TPredicateSym) (t :: T).
Sing p -> Sing t -> Maybe (ContainsT p t :~: 'True)
tPresence Sing p
p Sing t
t = case Sing p -> Sing t -> TPresence p t
forall (p :: TPredicateSym) (ty :: T).
Sing p -> Sing ty -> TPresence p ty
checkTPresence Sing p
p Sing t
t of
  TPresence p t
TPresent -> ('True :~: 'True) -> Maybe ('True :~: 'True)
forall a. a -> Maybe a
Just 'True :~: 'True
forall {k} (a :: k). a :~: a
Refl
  TPresence p t
TAbsent -> Maybe ('False :~: 'True)
Maybe (ContainsT p t :~: 'True)
forall a. Maybe a
Nothing

tAbsence :: Sing p -> Sing t -> Maybe (ContainsT p t :~: 'False)
tAbsence :: forall (p :: TPredicateSym) (t :: T).
Sing p -> Sing t -> Maybe (ContainsT p t :~: 'False)
tAbsence Sing p
p Sing t
t = case Sing p -> Sing t -> TPresence p t
forall (p :: TPredicateSym) (ty :: T).
Sing p -> Sing ty -> TPresence p ty
checkTPresence Sing p
p Sing t
t of
  TPresence p t
TPresent -> Maybe ('True :~: 'False)
Maybe (ContainsT p t :~: 'False)
forall a. Maybe a
Nothing
  TPresence p t
TAbsent -> ('False :~: 'False) -> Maybe ('False :~: 'False)
forall a. a -> Maybe a
Just 'False :~: 'False
forall {k} (a :: k). a :~: a
Refl