{-# 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
data Comparability t where
CanBeCompared :: (Comparable t, ComparabilityImplies t) => Comparability t
CannotBeCompared :: (ContainsT 'PSNonComparable t ~ 'True) => Comparability t
deriving stock instance Show (Comparability t)
type ComparabilityImplies t =
( ForbidOp t
, ForbidNestedBigMaps t
, ForbidTicket t
, ForbidSaplingState t
, ForbidBigMap t
, ForbidContract t
, ForbidNonComparable t
)
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
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
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
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
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