lol-0.2.0.0: A library for lattice cryptography.

Safe HaskellNone
LanguageHaskell2010

Crypto.Lol.PosBin

Contents

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 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 
data Sing Ordering where 
data Sing Nat where 
data Sing Symbol where 
data Sing () where 
data Sing Pos where 
data Sing Bin where 
data Sing Prime where 
data Sing PrimePower where 
data Sing Factored where 
data Sing [a0] where 
data Sing (Maybe a0) where 
data Sing (TyFun k1 k2 -> *) = SLambda {} 
data Sing (Either a0 b0) where 
data Sing ((,) a0 b0) where 
data Sing ((,,) a0 b0 c0) where 
data Sing ((,,,) a0 b0 c0 d0) where 
data Sing ((,,,,) a0 b0 c0 d0 e0) where 
data Sing ((,,,,,) a0 b0 c0 d0 e0 f0) where 
data Sing ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) where 

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.

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) 

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

type SSym1 t = S t 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 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 
data Sing Ordering where 
data Sing Nat where 
data Sing Symbol where 
data Sing () where 
data Sing Pos where 
data Sing Bin where 
data Sing Prime where 
data Sing PrimePower where 
data Sing Factored where 
data Sing [a0] where 
data Sing (Maybe a0) where 
data Sing (TyFun k1 k2 -> *) = SLambda {} 
data Sing (Either a0 b0) where 
data Sing ((,) a0 b0) where 
data Sing ((,,) a0 b0 c0) where 
data Sing ((,,,) a0 b0 c0 d0) where 
data Sing ((,,,,) a0 b0 c0 d0 e0) where 
data Sing ((,,,,,) a0 b0 c0 d0 e0 f0) where 
data Sing ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) where 

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 D0Sym1 t = D0 t 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.

Convenient synonyms for Pos and Bin types

type P1 = O Source

type P2 = S O Source

type P3 = S (S O) Source

type P4 = S (S (S O)) Source

type P5 = S (S (S (S O))) Source

type P6 = S (S (S (S (S O)))) Source

type P7 = S (S (S (S (S (S O))))) Source

type P8 = S (S (S (S (S (S (S O)))))) Source

type P9 = S (S (S (S (S (S (S (S O))))))) Source

type P10 = S (S (S (S (S (S (S (S (S O)))))))) Source

type P11 = S (S (S (S (S (S (S (S (S (S O))))))))) Source

type P12 = S (S (S (S (S (S (S (S (S (S (S O)))))))))) Source

type P13 = S (S (S (S (S (S (S (S (S (S (S (S O))))))))))) Source

type P14 = S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) Source

type P15 = S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))) Source

type P16 = S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))) Source

type B1 = B1 Source

type B2 = D0 B1 Source

type B3 = D1 B1 Source

type B4 = D0 (D0 B1) Source

type B5 = D1 (D0 B1) Source

type B6 = D0 (D1 B1) Source

type B7 = D1 (D1 B1) Source

type B8 = D0 (D0 (D0 B1)) Source

type B9 = D1 (D0 (D0 B1)) Source

type B10 = D0 (D1 (D0 B1)) Source

type B11 = D1 (D1 (D0 B1)) Source

type B12 = D0 (D0 (D1 B1)) Source

type B13 = D1 (D0 (D1 B1)) Source

type B14 = D0 (D1 (D1 B1)) Source

type B15 = D1 (D1 (D1 B1)) Source

type B16 = D0 (D0 (D0 (D0 B1))) Source

type B17 = D1 (D0 (D0 (D0 B1))) Source

type B18 = D0 (D1 (D0 (D0 B1))) Source

type B19 = D1 (D1 (D0 (D0 B1))) Source

type B20 = D0 (D0 (D1 (D0 B1))) Source

type B21 = D1 (D0 (D1 (D0 B1))) Source

type B22 = D0 (D1 (D1 (D0 B1))) Source

type B23 = D1 (D1 (D1 (D0 B1))) Source

type B24 = D0 (D0 (D0 (D1 B1))) Source

type B25 = D1 (D0 (D0 (D1 B1))) Source

type B26 = D0 (D1 (D0 (D1 B1))) Source

type B27 = D1 (D1 (D0 (D1 B1))) Source

type B28 = D0 (D0 (D1 (D1 B1))) Source

type B29 = D1 (D0 (D1 (D1 B1))) Source

type B30 = D0 (D1 (D1 (D1 B1))) Source

type B31 = D1 (D1 (D1 (D1 B1))) Source

type B32 = D0 (D0 (D0 (D0 (D0 B1)))) Source

type B33 = D1 (D0 (D0 (D0 (D0 B1)))) Source

type B34 = D0 (D1 (D0 (D0 (D0 B1)))) Source

type B35 = D1 (D1 (D0 (D0 (D0 B1)))) Source

type B36 = D0 (D0 (D1 (D0 (D0 B1)))) Source

type B37 = D1 (D0 (D1 (D0 (D0 B1)))) Source

type B38 = D0 (D1 (D1 (D0 (D0 B1)))) Source

type B39 = D1 (D1 (D1 (D0 (D0 B1)))) Source

type B40 = D0 (D0 (D0 (D1 (D0 B1)))) Source

type B41 = D1 (D0 (D0 (D1 (D0 B1)))) Source

type B42 = D0 (D1 (D0 (D1 (D0 B1)))) Source

type B43 = D1 (D1 (D0 (D1 (D0 B1)))) Source

type B44 = D0 (D0 (D1 (D1 (D0 B1)))) Source

type B45 = D1 (D0 (D1 (D1 (D0 B1)))) Source

type B46 = D0 (D1 (D1 (D1 (D0 B1)))) Source

type B47 = D1 (D1 (D1 (D1 (D0 B1)))) Source

type B48 = D0 (D0 (D0 (D0 (D1 B1)))) Source

type B49 = D1 (D0 (D0 (D0 (D1 B1)))) Source

type B50 = D0 (D1 (D0 (D0 (D1 B1)))) Source

type B51 = D1 (D1 (D0 (D0 (D1 B1)))) Source

type B52 = D0 (D0 (D1 (D0 (D1 B1)))) Source

type B53 = D1 (D0 (D1 (D0 (D1 B1)))) Source

type B54 = D0 (D1 (D1 (D0 (D1 B1)))) Source

type B55 = D1 (D1 (D1 (D0 (D1 B1)))) Source

type B56 = D0 (D0 (D0 (D1 (D1 B1)))) Source

type B57 = D1 (D0 (D0 (D1 (D1 B1)))) Source

type B58 = D0 (D1 (D0 (D1 (D1 B1)))) Source

type B59 = D1 (D1 (D0 (D1 (D1 B1)))) Source

type B60 = D0 (D0 (D1 (D1 (D1 B1)))) Source

type B61 = D1 (D0 (D1 (D1 (D1 B1)))) Source

type B62 = D0 (D1 (D1 (D1 (D1 B1)))) Source

type B63 = D1 (D1 (D1 (D1 (D1 B1)))) Source

type B64 = D0 (D0 (D0 (D0 (D0 (D0 B1))))) Source

type B65 = D1 (D0 (D0 (D0 (D0 (D0 B1))))) Source

type B66 = D0 (D1 (D0 (D0 (D0 (D0 B1))))) Source

type B67 = D1 (D1 (D0 (D0 (D0 (D0 B1))))) Source

type B68 = D0 (D0 (D1 (D0 (D0 (D0 B1))))) Source

type B69 = D1 (D0 (D1 (D0 (D0 (D0 B1))))) Source

type B70 = D0 (D1 (D1 (D0 (D0 (D0 B1))))) Source

type B71 = D1 (D1 (D1 (D0 (D0 (D0 B1))))) Source

type B72 = D0 (D0 (D0 (D1 (D0 (D0 B1))))) Source

type B73 = D1 (D0 (D0 (D1 (D0 (D0 B1))))) Source

type B74 = D0 (D1 (D0 (D1 (D0 (D0 B1))))) Source

type B75 = D1 (D1 (D0 (D1 (D0 (D0 B1))))) Source

type B76 = D0 (D0 (D1 (D1 (D0 (D0 B1))))) Source

type B77 = D1 (D0 (D1 (D1 (D0 (D0 B1))))) Source

type B78 = D0 (D1 (D1 (D1 (D0 (D0 B1))))) Source

type B79 = D1 (D1 (D1 (D1 (D0 (D0 B1))))) Source

type B80 = D0 (D0 (D0 (D0 (D1 (D0 B1))))) Source

type B81 = D1 (D0 (D0 (D0 (D1 (D0 B1))))) Source

type B82 = D0 (D1 (D0 (D0 (D1 (D0 B1))))) Source

type B83 = D1 (D1 (D0 (D0 (D1 (D0 B1))))) Source

type B84 = D0 (D0 (D1 (D0 (D1 (D0 B1))))) Source

type B85 = D1 (D0 (D1 (D0 (D1 (D0 B1))))) Source

type B86 = D0 (D1 (D1 (D0 (D1 (D0 B1))))) Source

type B87 = D1 (D1 (D1 (D0 (D1 (D0 B1))))) Source

type B88 = D0 (D0 (D0 (D1 (D1 (D0 B1))))) Source

type B89 = D1 (D0 (D0 (D1 (D1 (D0 B1))))) Source

type B90 = D0 (D1 (D0 (D1 (D1 (D0 B1))))) Source

type B91 = D1 (D1 (D0 (D1 (D1 (D0 B1))))) Source

type B92 = D0 (D0 (D1 (D1 (D1 (D0 B1))))) Source

type B93 = D1 (D0 (D1 (D1 (D1 (D0 B1))))) Source

type B94 = D0 (D1 (D1 (D1 (D1 (D0 B1))))) Source

type B95 = D1 (D1 (D1 (D1 (D1 (D0 B1))))) Source

type B96 = D0 (D0 (D0 (D0 (D0 (D1 B1))))) Source

type B97 = D1 (D0 (D0 (D0 (D0 (D1 B1))))) Source

type B98 = D0 (D1 (D0 (D0 (D0 (D1 B1))))) Source

type B99 = D1 (D1 (D0 (D0 (D0 (D1 B1))))) Source

type B100 = D0 (D0 (D1 (D0 (D0 (D1 B1))))) Source

type B101 = D1 (D0 (D1 (D0 (D0 (D1 B1))))) Source

type B102 = D0 (D1 (D1 (D0 (D0 (D1 B1))))) Source

type B103 = D1 (D1 (D1 (D0 (D0 (D1 B1))))) Source

type B104 = D0 (D0 (D0 (D1 (D0 (D1 B1))))) Source

type B105 = D1 (D0 (D0 (D1 (D0 (D1 B1))))) Source

type B106 = D0 (D1 (D0 (D1 (D0 (D1 B1))))) Source

type B107 = D1 (D1 (D0 (D1 (D0 (D1 B1))))) Source

type B108 = D0 (D0 (D1 (D1 (D0 (D1 B1))))) Source

type B109 = D1 (D0 (D1 (D1 (D0 (D1 B1))))) Source

type B110 = D0 (D1 (D1 (D1 (D0 (D1 B1))))) Source

type B111 = D1 (D1 (D1 (D1 (D0 (D1 B1))))) Source

type B112 = D0 (D0 (D0 (D0 (D1 (D1 B1))))) Source

type B113 = D1 (D0 (D0 (D0 (D1 (D1 B1))))) Source

type B114 = D0 (D1 (D0 (D0 (D1 (D1 B1))))) Source

type B115 = D1 (D1 (D0 (D0 (D1 (D1 B1))))) Source

type B116 = D0 (D0 (D1 (D0 (D1 (D1 B1))))) Source

type B117 = D1 (D0 (D1 (D0 (D1 (D1 B1))))) Source

type B118 = D0 (D1 (D1 (D0 (D1 (D1 B1))))) Source

type B119 = D1 (D1 (D1 (D0 (D1 (D1 B1))))) Source

type B120 = D0 (D0 (D0 (D1 (D1 (D1 B1))))) Source

type B121 = D1 (D0 (D0 (D1 (D1 (D1 B1))))) Source

type B122 = D0 (D1 (D0 (D1 (D1 (D1 B1))))) Source

type B123 = D1 (D1 (D0 (D1 (D1 (D1 B1))))) Source

type B124 = D0 (D0 (D1 (D1 (D1 (D1 B1))))) Source

type B125 = D1 (D0 (D1 (D1 (D1 (D1 B1))))) Source

type B126 = D0 (D1 (D1 (D1 (D1 (D1 B1))))) Source

type B127 = D1 (D1 (D1 (D1 (D1 (D1 B1))))) Source

type B128 = D0 (D0 (D0 (D0 (D0 (D0 (D0 B1)))))) Source