{-# 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(..))
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)
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
|]
)
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|])
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