Safe Haskell	None
Language	Haskell2010

Crypto.Lol.PosBin

Contents

Positive naturals in Peano representation
Positive naturals in binary representation
Miscellaneous
Convenient synonyms for Pos and Bin types

Description

Positive naturals in Peano and binary representations, singletonized and promoted to the type level. This module relies on Template Haskell, so parts of the documentation may be difficult to read. See source-level comments for further details.

Synopsis

Positive naturals in Peano representation

data Pos Source

Constructors

O
S Pos

Instances

Eq Pos Source
Ord Pos Source
Show Pos Source
SingI Pos O Source
POrd Pos (KProxy Pos) Source
SOrd Pos (KProxy Pos) Source
SEq Pos (KProxy Pos) Source
PEq Pos (KProxy Pos) Source
SDecide Pos (KProxy Pos) Source
SingI Pos n0 => SingI Pos (S n) Source
SingKind Pos (KProxy Pos) Source
SuppressUnusedWarnings (Pos -> TyFun Pos Pos -> *) AddPosSym1 Source
SuppressUnusedWarnings (Pos -> TyFun Pos Pos -> *) SubPosSym1 Source
SuppressUnusedWarnings (TyFun Pos (TyFun Pos Pos -> ) -> ) AddPosSym0 Source
SuppressUnusedWarnings (TyFun Pos (TyFun Pos Pos -> ) -> ) SubPosSym0 Source
SuppressUnusedWarnings (TyFun Pos Pos -> *) SSym0 Source
data Sing Pos where SO :: (~) Pos z O => Sing Pos z SS :: (~) Pos z (S n) => Sing Pos n -> Sing Pos z Source
type Min Pos arg0 arg1 = Apply Pos Pos (Apply (TyFun Pos Pos -> *) Pos (Min_1627641717Sym0 Pos) arg0) arg1
type Max Pos arg0 arg1 = Apply Pos Pos (Apply (TyFun Pos Pos -> *) Pos (Max_1627641684Sym0 Pos) arg0) arg1
type (:>=) Pos arg0 arg1 = Apply Bool Pos (Apply (TyFun Pos Bool -> *) Pos (TFHelper_1627641651Sym0 Pos) arg0) arg1
type (:>) Pos arg0 arg1 = Apply Bool Pos (Apply (TyFun Pos Bool -> *) Pos (TFHelper_1627641618Sym0 Pos) arg0) arg1
type (:<=) Pos arg0 arg1 = Apply Bool Pos (Apply (TyFun Pos Bool -> *) Pos (TFHelper_1627641585Sym0 Pos) arg0) arg1
type (:<) Pos arg0 arg1 = Apply Bool Pos (Apply (TyFun Pos Bool -> *) Pos (TFHelper_1627641552Sym0 Pos) arg0) arg1
type Compare Pos a0 a1 Source
type (:/=) Pos x y = Not ((:==) Pos x y)
type (:==) Pos a0 b0 Source
type Apply Pos Pos SSym0 l0 = SSym1 l0 Source
type Apply Pos Pos (AddPosSym1 l1) l0 Source
type Apply Pos Pos (SubPosSym1 l1) l0 Source
type DemoteRep Pos (KProxy Pos) = Pos Source
type Apply (TyFun Pos Pos -> *) Pos AddPosSym0 l0 = AddPosSym1 l0 Source
type Apply (TyFun Pos Pos -> *) Pos SubPosSym0 l0 = SubPosSym1 l0 Source

data family Sing a

The singleton kind-indexed data family.

Instances

data Sing Bool where SFalse :: (~) Bool z0 False => Sing Bool z0 STrue :: (~) Bool z0 True => Sing Bool z0
data Sing Ordering where SLT :: (~) Ordering z0 LT => Sing Ordering z0 SEQ :: (~) Ordering z0 EQ => Sing Ordering z0 SGT :: (~) Ordering z0 GT => Sing Ordering z0
data Sing Nat where SNat :: KnownNat n => Sing Nat n
data Sing Symbol where SSym :: KnownSymbol n => Sing Symbol n
data Sing () where STuple0 :: (~) () z0 () => Sing () z0
data Sing Pos where SO :: (~) Pos z O => Sing Pos z SS :: (~) Pos z (S n) => Sing Pos n -> Sing Pos z
data Sing Bin where SB1 :: (~) Bin z B1 => Sing Bin z SD0 :: (~) Bin z (D0 n) => Sing Bin n -> Sing Bin z SD1 :: (~) Bin z (D1 n) => Sing Bin n -> Sing Bin z
data Sing Prime where SP :: (~) Prime z (P n) => Sing Bin n -> Sing Prime z
data Sing PrimePower where SPP :: (~) PrimePower z (PP n) => Sing ((,) Prime Pos) n -> Sing PrimePower z
data Sing Factored where SF :: (~) Factored z (F n) => Sing [PrimePower] n -> Sing Factored z
data Sing [a0] where SNil :: (~) [a0] z0 ([] a0) => Sing [a0] z0 SCons :: (~) [a0] z0 ((:) a0 n0 n1) => Sing a0 n0 -> Sing [a0] n1 -> Sing [a0] z0
data Sing (Maybe a0) where SNothing :: (~) (Maybe a0) z0 (Nothing a0) => Sing (Maybe a0) z0 SJust :: (~) (Maybe a0) z0 (Just a0 n0) => Sing a0 n0 -> Sing (Maybe a0) z0
data Sing (TyFun k1 k2 -> *) = SLambda { applySing :: forall t. Sing k1 t -> Sing k2 ((@@) k2 k1 f t) }
data Sing (Either a0 b0) where SLeft :: (~) (Either a0 b0) z0 (Left a0 b0 n0) => Sing a0 n0 -> Sing (Either a0 b0) z0 SRight :: (~) (Either a0 b0) z0 (Right a0 b0 n0) => Sing b0 n0 -> Sing (Either a0 b0) z0
data Sing ((,) a0 b0) where STuple2 :: (~) ((,) a0 b0) z0 ((,) a0 b0 n0 n1) => Sing a0 n0 -> Sing b0 n1 -> Sing ((,) a0 b0) z0
data Sing ((,,) a0 b0 c0) where STuple3 :: (~) ((,,) a0 b0 c0) z0 ((,,) a0 b0 c0 n0 n1 n2) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing ((,,) a0 b0 c0) z0
data Sing ((,,,) a0 b0 c0 d0) where STuple4 :: (~) ((,,,) a0 b0 c0 d0) z0 ((,,,) a0 b0 c0 d0 n0 n1 n2 n3) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing d0 n3 -> Sing ((,,,) a0 b0 c0 d0) z0
data Sing ((,,,,) a0 b0 c0 d0 e0) where STuple5 :: (~) ((,,,,) a0 b0 c0 d0 e0) z0 ((,,,,) a0 b0 c0 d0 e0 n0 n1 n2 n3 n4) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing d0 n3 -> Sing e0 n4 -> Sing ((,,,,) a0 b0 c0 d0 e0) z0
data Sing ((,,,,,) a0 b0 c0 d0 e0 f0) where STuple6 :: (~) ((,,,,,) a0 b0 c0 d0 e0 f0) z0 ((,,,,,) a0 b0 c0 d0 e0 f0 n0 n1 n2 n3 n4 n5) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing d0 n3 -> Sing e0 n4 -> Sing f0 n5 -> Sing ((,,,,,) a0 b0 c0 d0 e0 f0) z0
data Sing ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) where STuple7 :: (~) ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) z0 ((,,,,,,) a0 b0 c0 d0 e0 f0 g0 n0 n1 n2 n3 n4 n5 n6) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing d0 n3 -> Sing e0 n4 -> Sing f0 n5 -> Sing g0 n6 -> Sing ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) z0

type SPos = (Sing :: Pos -> *) Source

type PosC p = SingI p Source

Kind-restricted synonym for SingI.

posToInt :: C z => Pos -> z Source

Convert a Pos to an integral type.

addPos :: Pos -> Pos -> Pos Source

sAddPos :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply AddPosSym0 t) t :: Pos) Source

type family AddPos a a :: Pos Source

Equations

AddPos O b = Apply SSym0 b
AddPos (S a) b = Apply (Apply ($$) SSym0) (Apply (Apply AddPosSym0 a) b)

subPos :: Pos -> Pos -> Pos Source

sSubPos :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply SubPosSym0 t) t :: Pos) Source

type family SubPos a a :: Pos Source

Equations

SubPos (S a) O = a
SubPos (S a) (S b) = Apply (Apply SubPosSym0 a) b
SubPos O _z_1627499864 = Apply ErrorSym0 "Invalid call to subPos: a <= b"

posType :: Int -> TypeQ Source

Template Haskell splice for the Pos type representing a given Int, e.g., $(posType 8).

posDec :: Int -> DecQ Source

Template Haskell splice that defines the Pos type synonym Pn.

type OSym0 = O Source

data SSym0 l Source

Instances

SuppressUnusedWarnings (TyFun Pos Pos -> *) SSym0 Source
type Apply Pos Pos SSym0 l0 = SSym1 l0 Source

type SSym1 t = S t Source

data AddPosSym0 l Source

Instances

SuppressUnusedWarnings (TyFun Pos (TyFun Pos Pos -> ) -> ) AddPosSym0 Source
type Apply (TyFun Pos Pos -> *) Pos AddPosSym0 l0 = AddPosSym1 l0 Source

data AddPosSym1 l l Source

Instances

SuppressUnusedWarnings (Pos -> TyFun Pos Pos -> *) AddPosSym1 Source
type Apply Pos Pos (AddPosSym1 l1) l0 Source

data SubPosSym0 l Source

Instances

SuppressUnusedWarnings (TyFun Pos (TyFun Pos Pos -> ) -> ) SubPosSym0 Source
type Apply (TyFun Pos Pos -> *) Pos SubPosSym0 l0 = SubPosSym1 l0 Source

data SubPosSym1 l l Source

Instances

SuppressUnusedWarnings (Pos -> TyFun Pos Pos -> *) SubPosSym1 Source
type Apply Pos Pos (SubPosSym1 l1) l0 Source

Positive naturals in binary representation

data Bin Source

Constructors

B1
D0 Bin
D1 Bin

Instances

Eq Bin Source
Ord Bin Source
Show Bin Source
SingI Bin B1 Source
POrd Bin (KProxy Bin) Source
SOrd Bin (KProxy Bin) Source
SEq Bin (KProxy Bin) Source
PEq Bin (KProxy Bin) Source
SDecide Bin (KProxy Bin) Source
SingI Bin n0 => SingI Bin (D0 n) Source
SingI Bin n0 => SingI Bin (D1 n) Source
SingKind Bin (KProxy Bin) Source
SuppressUnusedWarnings (TyFun Bin Bin -> *) D1Sym0 Source
SuppressUnusedWarnings (TyFun Bin Bin -> *) D0Sym0 Source
data Sing Bin where SB1 :: (~) Bin z B1 => Sing Bin z SD0 :: (~) Bin z (D0 n) => Sing Bin n -> Sing Bin z SD1 :: (~) Bin z (D1 n) => Sing Bin n -> Sing Bin z Source
type Min Bin arg0 arg1 = Apply Bin Bin (Apply (TyFun Bin Bin -> *) Bin (Min_1627641717Sym0 Bin) arg0) arg1
type Max Bin arg0 arg1 = Apply Bin Bin (Apply (TyFun Bin Bin -> *) Bin (Max_1627641684Sym0 Bin) arg0) arg1
type (:>=) Bin arg0 arg1 = Apply Bool Bin (Apply (TyFun Bin Bool -> *) Bin (TFHelper_1627641651Sym0 Bin) arg0) arg1
type (:>) Bin arg0 arg1 = Apply Bool Bin (Apply (TyFun Bin Bool -> *) Bin (TFHelper_1627641618Sym0 Bin) arg0) arg1
type (:<=) Bin arg0 arg1 = Apply Bool Bin (Apply (TyFun Bin Bool -> *) Bin (TFHelper_1627641585Sym0 Bin) arg0) arg1
type (:<) Bin arg0 arg1 = Apply Bool Bin (Apply (TyFun Bin Bool -> *) Bin (TFHelper_1627641552Sym0 Bin) arg0) arg1
type Compare Bin a0 a1 Source
type (:/=) Bin x y = Not ((:==) Bin x y)
type (:==) Bin a0 b0 Source
type Apply Bin Bin D1Sym0 l0 = D1Sym1 l0 Source
type Apply Bin Bin D0Sym0 l0 = D0Sym1 l0 Source
type DemoteRep Bin (KProxy Bin) = Bin Source

data family Sing a

The singleton kind-indexed data family.

Instances

data Sing Bool where SFalse :: (~) Bool z0 False => Sing Bool z0 STrue :: (~) Bool z0 True => Sing Bool z0
data Sing Ordering where SLT :: (~) Ordering z0 LT => Sing Ordering z0 SEQ :: (~) Ordering z0 EQ => Sing Ordering z0 SGT :: (~) Ordering z0 GT => Sing Ordering z0
data Sing Nat where SNat :: KnownNat n => Sing Nat n
data Sing Symbol where SSym :: KnownSymbol n => Sing Symbol n
data Sing () where STuple0 :: (~) () z0 () => Sing () z0
data Sing Pos where SO :: (~) Pos z O => Sing Pos z SS :: (~) Pos z (S n) => Sing Pos n -> Sing Pos z
data Sing Bin where SB1 :: (~) Bin z B1 => Sing Bin z SD0 :: (~) Bin z (D0 n) => Sing Bin n -> Sing Bin z SD1 :: (~) Bin z (D1 n) => Sing Bin n -> Sing Bin z
data Sing Prime where SP :: (~) Prime z (P n) => Sing Bin n -> Sing Prime z
data Sing PrimePower where SPP :: (~) PrimePower z (PP n) => Sing ((,) Prime Pos) n -> Sing PrimePower z
data Sing Factored where SF :: (~) Factored z (F n) => Sing [PrimePower] n -> Sing Factored z
data Sing [a0] where SNil :: (~) [a0] z0 ([] a0) => Sing [a0] z0 SCons :: (~) [a0] z0 ((:) a0 n0 n1) => Sing a0 n0 -> Sing [a0] n1 -> Sing [a0] z0
data Sing (Maybe a0) where SNothing :: (~) (Maybe a0) z0 (Nothing a0) => Sing (Maybe a0) z0 SJust :: (~) (Maybe a0) z0 (Just a0 n0) => Sing a0 n0 -> Sing (Maybe a0) z0
data Sing (TyFun k1 k2 -> *) = SLambda { applySing :: forall t. Sing k1 t -> Sing k2 ((@@) k2 k1 f t) }
data Sing (Either a0 b0) where SLeft :: (~) (Either a0 b0) z0 (Left a0 b0 n0) => Sing a0 n0 -> Sing (Either a0 b0) z0 SRight :: (~) (Either a0 b0) z0 (Right a0 b0 n0) => Sing b0 n0 -> Sing (Either a0 b0) z0
data Sing ((,) a0 b0) where STuple2 :: (~) ((,) a0 b0) z0 ((,) a0 b0 n0 n1) => Sing a0 n0 -> Sing b0 n1 -> Sing ((,) a0 b0) z0
data Sing ((,,) a0 b0 c0) where STuple3 :: (~) ((,,) a0 b0 c0) z0 ((,,) a0 b0 c0 n0 n1 n2) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing ((,,) a0 b0 c0) z0
data Sing ((,,,) a0 b0 c0 d0) where STuple4 :: (~) ((,,,) a0 b0 c0 d0) z0 ((,,,) a0 b0 c0 d0 n0 n1 n2 n3) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing d0 n3 -> Sing ((,,,) a0 b0 c0 d0) z0
data Sing ((,,,,) a0 b0 c0 d0 e0) where STuple5 :: (~) ((,,,,) a0 b0 c0 d0 e0) z0 ((,,,,) a0 b0 c0 d0 e0 n0 n1 n2 n3 n4) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing d0 n3 -> Sing e0 n4 -> Sing ((,,,,) a0 b0 c0 d0 e0) z0
data Sing ((,,,,,) a0 b0 c0 d0 e0 f0) where STuple6 :: (~) ((,,,,,) a0 b0 c0 d0 e0 f0) z0 ((,,,,,) a0 b0 c0 d0 e0 f0 n0 n1 n2 n3 n4 n5) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing d0 n3 -> Sing e0 n4 -> Sing f0 n5 -> Sing ((,,,,,) a0 b0 c0 d0 e0 f0) z0
data Sing ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) where STuple7 :: (~) ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) z0 ((,,,,,,) a0 b0 c0 d0 e0 f0 g0 n0 n1 n2 n3 n4 n5 n6) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing d0 n3 -> Sing e0 n4 -> Sing f0 n5 -> Sing g0 n6 -> Sing ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) z0

type SBin = (Sing :: Bin -> *) Source

type BinC b = SingI b Source

Kind-restricted synonym for SingI.

binToInt :: C z => Bin -> z Source

Convert a Bin to an integral type.

binType :: Int -> TypeQ Source

Template Haskell splice for the Bin type representing a given Int, e.g., $(binType 89).

binDec :: Int -> DecQ Source

Template Haskell splice that defines the Bin type synonym Bn.

type B1Sym0 = B1 Source

data D0Sym0 l Source

Instances

SuppressUnusedWarnings (TyFun Bin Bin -> *) D0Sym0 Source
type Apply Bin Bin D0Sym0 l0 = D0Sym1 l0 Source

type D0Sym1 t = D0 t Source

data D1Sym0 l Source

Instances

SuppressUnusedWarnings (TyFun Bin Bin -> *) D1Sym0 Source
type Apply Bin Bin D1Sym0 l0 = D1Sym1 l0 Source

type D1Sym1 t = D1 t Source

Miscellaneous

intDec Source

Arguments

:: String	pfx
-> (Int -> TypeQ)	f
-> Int	n
-> DecQ

Template Haskell splice that declares a type synonym pfxn as the type f n.

primes :: [Int] Source

Infinite list of primes, built using Sieve of Erastothenes.

prime :: Int -> Bool Source

Search for the argument in primes. This is not particularly fast, but works well enough for moderate-sized numbers that would appear as (divisors of) cyclotomic indices of interest.