Crypto.Lol.Factored

This module defines types and operations for type-level representation and manipulation of natural numbers, as represented by their prime-power factorizations. It relies on Template Haskell, so parts of the documentation may be difficult to read. See source-level comments for further details.

Factored natural numbers

data Factored

Instances

Eq Factored

Defined in Crypto.Lol.FactoredDefs

Methods

(==) :: Factored -> Factored -> Bool

(/=) :: Factored -> Factored -> Bool

Show Factored

Defined in Crypto.Lol.FactoredDefs

Methods

showsPrec :: Int -> Factored -> ShowS

show :: Factored -> String

showList :: [Factored] -> ShowS

PShow Factored

Defined in Crypto.Lol.FactoredDefs

Associated Types

type ShowsPrec arg arg1 arg2 :: Symbol

type Show_ arg :: Symbol

type ShowList arg arg1 :: Symbol

SShow [PrimePower] => SShow Factored

Defined in Crypto.Lol.FactoredDefs

Methods

sShowsPrec :: Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply ShowsPrecSym0 t1) t2) t3)

sShow_ :: Sing t -> Sing (Apply Show_Sym0 t)

sShowList :: Sing t1 -> Sing t2 -> Sing (Apply (Apply ShowListSym0 t1) t2)

SEq [PrimePower] => SEq Factored

Defined in Crypto.Lol.FactoredDefs

Methods

(%==) :: Sing a -> Sing b -> Sing (a == b)

(%/=) :: Sing a -> Sing b -> Sing (a /= b)

PEq Factored

Defined in Crypto.Lol.FactoredDefs

Associated Types

type x == y :: Bool

type x /= y :: Bool

SDecide [PrimePower] => SDecide Factored

Defined in Crypto.Lol.FactoredDefs

Methods

(%~) :: Sing a -> Sing b -> Decision (a :~: b)

SingKind Factored

Defined in Crypto.Lol.FactoredDefs

Associated Types

type Demote Factored = (r :: Type)

Methods

fromSing :: Sing a -> Demote Factored

toSing :: Demote Factored -> SomeSing Factored

(Fact m, C i) => Reflects (m :: Factored) i

Defined in Crypto.Lol.Reflects

Methods

value :: i

ShowSing [PrimePower] => Show (Sing z)

Defined in Crypto.Lol.FactoredDefs

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

Fact m => Show (ArgType m)

Defined in Crypto.Lol.Utils.ShowType

Methods

showsPrec :: Int -> ArgType m -> ShowS

show :: ArgType m -> String

showList :: [ArgType m] -> ShowS

data Sing (a :: Factored)

Defined in Crypto.Lol.FactoredDefs

data Sing (a :: Factored) where

• SF :: forall (a :: Factored) (n :: [PrimePower]). Sing n -> Sing (F n)

type Demote Factored

Defined in Crypto.Lol.FactoredDefs

type Demote Factored = Factored

type Show_ (arg :: Factored)

Defined in Crypto.Lol.FactoredDefs

type Show_ (arg :: Factored) = Apply (Show__6989586621680262717Sym0 :: TyFun Factored Symbol -> Type) arg

type ShowList (arg :: [Factored]) arg1

Defined in Crypto.Lol.FactoredDefs

type ShowList (arg :: [Factored]) arg1 = Apply (Apply (ShowList_6989586621680262728Sym0 :: TyFun [Factored] (Symbol ~> Symbol) -> Type) arg) arg1

type (x :: Factored) /= (y :: Factored)

Defined in Crypto.Lol.FactoredDefs

type (x :: Factored) /= (y :: Factored) = Not (x == y)

type (a :: Factored) == (b :: Factored)

Defined in Crypto.Lol.FactoredDefs

type (a :: Factored) == (b :: Factored)

type ShowsPrec a1 (a2 :: Factored) a3

Defined in Crypto.Lol.FactoredDefs

type ShowsPrec a1 (a2 :: Factored) a3

type SFactored = (Sing :: Factored -> Type)

type Fact (m :: Factored) = SingI m

Kind-restricted synonym for SingI.

fType :: Int -> TypeQ

Template Haskell splice for the Factored type corresponding to a given positive integer. Factors its argument using a naive trial-division algorithm with primes, so should only be used on small-to-moderate-sized arguments (any reasonable cyclotomic index should be OK).

fDec :: Int -> DecQ

Template Haskell splice that defines the Factored type synonym F\(n\) for a positive integer \(n\).

reifyFact :: Int -> (forall m. SFactored m -> a) -> a

Reify a Factored as a singleton.

reifyFactI :: Int -> (forall m proxy. Fact m => proxy m -> a) -> a

Reify a Factored for a Fact constraint.

intToFact :: Int -> Factored

Converts input to its data-level Factored representation.

Prime powers

newtype PrimePower

Constructors

PP (PrimeBin, Pos)

Instances

Eq PrimePower

Defined in Crypto.Lol.FactoredDefs

Methods

(==) :: PrimePower -> PrimePower -> Bool

(/=) :: PrimePower -> PrimePower -> Bool

Show PrimePower

Defined in Crypto.Lol.FactoredDefs

Methods

showsPrec :: Int -> PrimePower -> ShowS

show :: PrimePower -> String

showList :: [PrimePower] -> ShowS

PShow PrimePower

Defined in Crypto.Lol.FactoredDefs

Associated Types

type ShowsPrec arg arg1 arg2 :: Symbol

type Show_ arg :: Symbol

type ShowList arg arg1 :: Symbol

SShow (PrimeBin, Pos) => SShow PrimePower

Defined in Crypto.Lol.FactoredDefs

Methods

sShowsPrec :: Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply ShowsPrecSym0 t1) t2) t3)

sShow_ :: Sing t -> Sing (Apply Show_Sym0 t)

sShowList :: Sing t1 -> Sing t2 -> Sing (Apply (Apply ShowListSym0 t1) t2)

SEq (PrimeBin, Pos) => SEq PrimePower

Defined in Crypto.Lol.FactoredDefs

Methods

(%==) :: Sing a -> Sing b -> Sing (a == b)

(%/=) :: Sing a -> Sing b -> Sing (a /= b)

PEq PrimePower

Defined in Crypto.Lol.FactoredDefs

Associated Types

type x == y :: Bool

type x /= y :: Bool

SDecide (PrimeBin, Pos) => SDecide PrimePower

Defined in Crypto.Lol.FactoredDefs

Methods

(%~) :: Sing a -> Sing b -> Decision (a :~: b)

SingKind PrimePower

Defined in Crypto.Lol.FactoredDefs

Associated Types

type Demote PrimePower = (r :: Type)

Methods

fromSing :: Sing a -> Demote PrimePower

toSing :: Demote PrimePower -> SomeSing PrimePower

(PPow pp, C i) => Reflects (pp :: PrimePower) i

Defined in Crypto.Lol.Reflects

Methods

value :: i

SingI n => SingI (PP n :: PrimePower)

Defined in Crypto.Lol.FactoredDefs

Methods

sing :: Sing (PP n)

ShowSing (PrimeBin, Pos) => Show (Sing z)

Defined in Crypto.Lol.FactoredDefs

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

SingI (TyCon1 PP)

Defined in Crypto.Lol.FactoredDefs

Methods

sing :: Sing (TyCon1 PP)

data Sing (a :: PrimePower)

Defined in Crypto.Lol.FactoredDefs

data Sing (a :: PrimePower) where

• SPP :: forall (a :: PrimePower) (n :: (PrimeBin, Pos)). Sing n -> Sing (PP n)

type Demote PrimePower

Defined in Crypto.Lol.FactoredDefs

type Demote PrimePower = PrimePower

type Show_ (arg :: PrimePower)

Defined in Crypto.Lol.FactoredDefs

type Show_ (arg :: PrimePower) = Apply (Show__6989586621680262717Sym0 :: TyFun PrimePower Symbol -> Type) arg

type ShowList (arg :: [PrimePower]) arg1

Defined in Crypto.Lol.FactoredDefs

type ShowList (arg :: [PrimePower]) arg1 = Apply (Apply (ShowList_6989586621680262728Sym0 :: TyFun [PrimePower] (Symbol ~> Symbol) -> Type) arg) arg1

type (x :: PrimePower) /= (y :: PrimePower)

Defined in Crypto.Lol.FactoredDefs

type (x :: PrimePower) /= (y :: PrimePower) = Not (x == y)

type (a :: PrimePower) == (b :: PrimePower)

Defined in Crypto.Lol.FactoredDefs

type (a :: PrimePower) == (b :: PrimePower)

type ShowsPrec a1 (a2 :: PrimePower) a3

Defined in Crypto.Lol.FactoredDefs

type ShowsPrec a1 (a2 :: PrimePower) a3

type SPrimePower = (Sing :: PrimePower -> Type)

data family Sing (a :: k) :: Type

The singleton kind-indexed data family.

Instances

ShowSing Pos => Show (Sing z)

Defined in Crypto.Lol.PosBinDefs

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

ShowSing Bin => Show (Sing z)

Defined in Crypto.Lol.PosBinDefs

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

ShowSing Bin => Show (Sing z)

Defined in Crypto.Lol.FactoredDefs

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

ShowSing (PrimeBin, Pos) => Show (Sing z)

Defined in Crypto.Lol.FactoredDefs

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

ShowSing [PrimePower] => Show (Sing z)

Defined in Crypto.Lol.FactoredDefs

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

data Sing (a :: Bool)

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Bool) where

• SFalse :: forall (a :: Bool). Sing False
• STrue :: forall (a :: Bool). Sing True

data Sing (a :: Ordering)

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Ordering) where

• SLT :: forall (a :: Ordering). Sing LT
• SEQ :: forall (a :: Ordering). Sing EQ
• SGT :: forall (a :: Ordering). Sing GT

data Sing (n :: Nat)

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Nat) where

• SNat :: forall (n :: Nat). KnownNat n => Sing n

data Sing (n :: Symbol)

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Symbol) where

• SSym :: forall (n :: Symbol). KnownSymbol n => Sing n

data Sing (a :: ())

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: ()) where

• STuple0 :: forall (a :: ()). Sing ()

data Sing (a :: Pos)

Defined in Crypto.Lol.PosBinDefs

data Sing (a :: Pos) where

• SO :: forall (a :: Pos). Sing O
• SS :: forall (a :: Pos) (n :: Pos). Sing n -> Sing (S n)

data Sing (a :: Bin)

Defined in Crypto.Lol.PosBinDefs

data Sing (a :: Bin) where

• SB1 :: forall (a :: Bin). Sing B1
• SD0 :: forall (a :: Bin) (n :: Bin). Sing n -> Sing (D0 n)
• SD1 :: forall (a :: Bin) (n :: Bin). Sing n -> Sing (D1 n)

data Sing (a :: PrimeBin)

Defined in Crypto.Lol.FactoredDefs

data Sing (a :: PrimeBin) where

• SP :: forall (a :: PrimeBin) (n :: Bin). Sing n -> Sing (P n)

data Sing (a :: PrimePower)

Defined in Crypto.Lol.FactoredDefs

data Sing (a :: PrimePower) where

• SPP :: forall (a :: PrimePower) (n :: (PrimeBin, Pos)). Sing n -> Sing (PP n)

data Sing (a :: Factored)

Defined in Crypto.Lol.FactoredDefs

data Sing (a :: Factored) where

• SF :: forall (a :: Factored) (n :: [PrimePower]). Sing n -> Sing (F n)

data Sing (a :: Void)

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Void)

data Sing (a :: All)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: All) where

• SAll :: forall (a :: All) (n :: Bool). {..} -> Sing (All n)

data Sing (a :: Any)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: Any) where

• SAny :: forall (a :: Any) (n :: Bool). {..} -> Sing (Any n)

data Sing (b :: [a])

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: [a]) where

• SNil :: forall a (b :: [a]). Sing ([] :: [a])
• SCons :: forall a (b :: [a]) (n1 :: a) (n2 :: [a]). Sing n1 -> Sing n2 -> Sing (n1 ': n2)

data Sing (b :: Maybe a)

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: Maybe a) where

• SNothing :: forall a (b :: Maybe a). Sing (Nothing :: Maybe a)
• SJust :: forall a (b :: Maybe a) (n :: a). Sing n -> Sing (Just n)

data Sing (b :: Min a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Min a) where

• SMin :: forall a (b :: Min a) (n :: a). {..} -> Sing (Min n)

data Sing (b :: Max a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Max a) where

• SMax :: forall a (b :: Max a) (n :: a). {..} -> Sing (Max n)

data Sing (b :: First a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: First a) where

• SFirst :: forall a (b :: First a) (n :: a). {..} -> Sing (First n)

data Sing (b :: Last a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Last a) where

• SLast :: forall a (b :: Last a) (n :: a). {..} -> Sing (Last n)

data Sing (a :: WrappedMonoid m)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: WrappedMonoid m) where

• SWrapMonoid :: forall m (a :: WrappedMonoid m) (n :: m). {..} -> Sing (WrapMonoid n)

data Sing (b :: Option a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Option a) where

• SOption :: forall a (b :: Option a) (n :: Maybe a). {..} -> Sing (Option n)

data Sing (b :: Identity a)

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: Identity a) where

• SIdentity :: forall a (b :: Identity a) (n :: a). {..} -> Sing (Identity n)

data Sing (b :: First a)

Defined in Data.Singletons.Prelude.Monoid

data Sing (b :: First a) where

• SFirst :: forall a (b :: First a) (n :: Maybe a). {..} -> Sing (First n)

data Sing (b :: Last a)

Defined in Data.Singletons.Prelude.Monoid

data Sing (b :: Last a) where

• SLast :: forall a (b :: Last a) (n :: Maybe a). {..} -> Sing (Last n)

data Sing (b :: Dual a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Dual a) where

• SDual :: forall a (b :: Dual a) (n :: a). {..} -> Sing (Dual n)

data Sing (b :: Sum a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Sum a) where

• SSum :: forall a (b :: Sum a) (n :: a). {..} -> Sing (Sum n)

data Sing (b :: Product a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Product a) where

• SProduct :: forall a (b :: Product a) (n :: a). {..} -> Sing (Product n)

data Sing (b :: Down a)

Defined in Data.Singletons.Prelude.Ord

data Sing (b :: Down a) where

• SDown :: forall a (b :: Down a) (n :: a). Sing n -> Sing (Down n)

data Sing (b :: NonEmpty a)

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: NonEmpty a) where

• (:%|) :: forall a (b :: NonEmpty a) (n1 :: a) (n2 :: [a]). Sing n1 -> Sing n2 -> Sing (n1 :| n2)

data Sing (b :: Endo a)

Defined in Data.Singletons.Prelude.Foldable

data Sing (b :: Endo a) where

• SEndo :: forall a (b :: Endo a) (x :: a ~> a). Sing x -> Sing (Endo x)

data Sing (b :: MaxInternal a)

Defined in Data.Singletons.Prelude.Foldable

data Sing (b :: MaxInternal a) where

• SMaxInternal :: forall a (b :: MaxInternal a) (x :: Maybe a). Sing x -> Sing (MaxInternal x)

data Sing (b :: MinInternal a)

Defined in Data.Singletons.Prelude.Foldable

data Sing (b :: MinInternal a) where

• SMinInternal :: forall a (b :: MinInternal a) (x :: Maybe a). Sing x -> Sing (MinInternal x)

data Sing (c :: Either a b)

Defined in Data.Singletons.Prelude.Instances

data Sing (c :: Either a b) where

• SLeft :: forall a b (c :: Either a b) (n :: a). Sing n -> Sing (Left n :: Either a b)
• SRight :: forall a b (c :: Either a b) (n :: b). Sing n -> Sing (Right n :: Either a b)

data Sing (c :: (a, b))

Defined in Data.Singletons.Prelude.Instances

data Sing (c :: (a, b)) where

• STuple2 :: forall a b (c :: (a, b)) (n1 :: a) (n2 :: b). Sing n1 -> Sing n2 -> Sing ((,) n1 n2)

data Sing (c :: Arg a b)

Defined in Dat