Safe Haskell	Safe-Inferred
Language	Haskell2010

Morley.Michelson.Typed.Scope.Internal.WithDeMorganScope

Synopsis

class WithDeMorganScope (c :: T -> Constraint) t a b where
- withDeMorganScope :: c (t a b) => ((c a, c b) => ret) -> ret
deMorganForbidT :: forall a b r p. (ContainsT p a || ContainsT p b) ~ 'False => Sing p -> Sing a -> Sing b -> ((ForbidT p a, ForbidT p b) => r) -> r
simpleWithDeMorgan :: forall a b ret op. ((ContainsT op a || ContainsT op b) ~ 'False, SingI a) => Sing op -> ((ContainsT op a ~ 'False, ContainsT op b ~ 'False) => ret) -> ret
simpleWithDeMorgan' :: forall b ret op a. (ContainsT op a || ContainsT op b) ~ 'False => Sing op -> Sing a -> ((ContainsT op a ~ 'False, ContainsT op b ~ 'False) => ret) -> ret

Documentation

class WithDeMorganScope (c :: T -> Constraint) t a b where Source #

Allows using a scope that can be proven true with a De Morgan law.

Many scopes are defined as not a (or rather a ~ 'False) where a is a negative property we want to avoid as a Constraint. The negative constraints are implemented with a type family that for some combination types resolves to itself applied to the type arguments in an or, e.g. A pair l r has x if l or r contain x.

Because of the De Morgan laws not (a or b) implies (not a) and (not b) or in our case: pair does not contain x -> a and b don't contain x.

Methods

withDeMorganScope :: c (t a b) => ((c a, c b) => ret) -> ret Source #

Instances

Instances details

SingI k => WithDeMorganScope ForbidContract 'TBigMap k v Source #
Instance details Defined in Morley.Michelson.Typed.Scope.Internal.WithDeMorganScope Methods withDeMorganScope :: ForbidContract ('TBigMap k v) => ((ForbidContract k, ForbidContract v) => ret) -> ret Source #
SingI k => WithDeMorganScope ForbidOp 'TBigMap k v Source #
Instance details Defined in Morley.Michelson.Typed.Scope.Internal.WithDeMorganScope Methods withDeMorganScope :: ForbidOp ('TBigMap k v) => ((ForbidOp k, ForbidOp v) => ret) -> ret Source #
SingI k => WithDeMorganScope ForbidSaplingState 'TBigMap k v Source #
Instance details Defined in Morley.Michelson.Typed.Scope.Internal.WithDeMorganScope Methods withDeMorganScope :: ForbidSaplingState ('TBigMap k v) => ((ForbidSaplingState k, ForbidSaplingState v) => ret) -> ret Source #
SingI k => WithDeMorganScope ForbidTicket 'TBigMap k v Source #
Instance details Defined in Morley.Michelson.Typed.Scope.Internal.WithDeMorganScope Methods withDeMorganScope :: ForbidTicket ('TBigMap k v) => ((ForbidTicket k, ForbidTicket v) => ret) -> ret Source #
(WithDeMorganScope ForbidOp t a b, WithDeMorganScope ForbidBigMap t a b, WithDeMorganScope ForbidContract t a b, WithDeMorganScope ForbidTicket t a b, WithDeMorganScope ForbidSaplingState t a b, WellTyped a, WellTyped b) => WithDeMorganScope ConstantScope t a b Source #
Instance details Defined in Morley.Michelson.Typed.Scope.Internal.WithDeMorganScope Methods withDeMorganScope :: ConstantScope (t a b) => ((ConstantScope a, ConstantScope b) => ret) -> ret Source #
(WithDeMorganScope ForbidOp t a b, WithDeMorganScope ForbidBigMap t a b, WithDeMorganScope ForbidTicket t a b, WithDeMorganScope ForbidSaplingState t a b, WellTyped a, WellTyped b) => WithDeMorganScope PackedValScope t a b Source #
Instance details Defined in Morley.Michelson.Typed.Scope.Internal.WithDeMorganScope Methods withDeMorganScope :: PackedValScope (t a b) => ((PackedValScope a, PackedValScope b) => ret) -> ret Source #
(WithDeMorganScope ForbidOp t a b, WithDeMorganScope ForbidNestedBigMaps t a b, WellTyped a, WellTyped b) => WithDeMorganScope ParameterScope t a b Source #
Instance details Defined in Morley.Michelson.Typed.Scope.Internal.WithDeMorganScope Methods withDeMorganScope :: ParameterScope (t a b) => ((ParameterScope a, ParameterScope b) => ret) -> ret Source #
(WithDeMorganScope ForbidOp t a b, WithDeMorganScope ForbidNestedBigMaps t a b, WithDeMorganScope ForbidContract t a b, WellTyped a, WellTyped b) => WithDeMorganScope StorageScope t a b Source #
Instance details Defined in Morley.Michelson.Typed.Scope.Internal.WithDeMorganScope Methods withDeMorganScope :: StorageScope (t a b) => ((StorageScope a, StorageScope b) => ret) -> ret Source #
(SingI k, SingI p) => WithDeMorganScope (ForbidT p) 'TMap k v Source #
Instance details Defined in Morley.Michelson.Typed.Scope.Internal.WithDeMorganScope Methods withDeMorganScope :: ForbidT p ('TMap k v) => ((ForbidT p k, ForbidT p v) => ret) -> ret Source #
(SingI a, SingI p) => WithDeMorganScope (ForbidT p) 'TOr a b Source #
Instance details Defined in Morley.Michelson.Typed.Scope.Internal.WithDeMorganScope Methods withDeMorganScope :: ForbidT p ('TOr a b) => ((ForbidT p a, ForbidT p b) => ret) -> ret Source #
(SingI a, SingI p) => WithDeMorganScope (ForbidT p) 'TPair a b Source #
Instance details Defined in Morley.Michelson.Typed.Scope.Internal.WithDeMorganScope Methods withDeMorganScope :: ForbidT p ('TPair a b) => ((ForbidT p a, ForbidT p b) => ret) -> ret Source #

deMorganForbidT :: forall a b r p. (ContainsT p a || ContainsT p b) ~ 'False => Sing p -> Sing a -> Sing b -> ((ForbidT p a, ForbidT p b) => r) -> r Source #

Simpler version of withDeMorganScope for ForbidT constraints.

simpleWithDeMorgan :: forall a b ret op. ((ContainsT op a || ContainsT op b) ~ 'False, SingI a) => Sing op -> ((ContainsT op a ~ 'False, ContainsT op b ~ 'False) => ret) -> ret Source #

When a class looks like

class (SomeTypeFamily t ~ 'False, ...) => TheClass t
instance (SomeTypeFamily t ~ 'False, ...) => TheClass t

and the additional constraints are satisfied by the instance constraints of the WithDeMorganScope instance for TheClass, we can use simpleWithDeMorgan to define withDeMorganScope for the instance.

simpleWithDeMorgan' :: forall b ret op a. (ContainsT op a || ContainsT op b) ~ 'False => Sing op -> Sing a -> ((ContainsT op a ~ 'False, ContainsT op b ~ 'False) => ret) -> ret Source #