#if __GLASGOW_HASKELL__ >= 800
#endif
module Crypto.Lol.FactoredDefs
(
reifyFact, reifyFactI
, Factored, SFactored, Fact, fType, fDec
, reifyPPow, reifyPPowI
, PrimePower, SPrimePower, Sing(SPP), PPow, ppType, ppDec
, reifyPrime, reifyPrimeI
, PrimeBin, SPrimeBin, Prime, pType, pDec
, pToPP, sPToPP, PToPP, ppToF, sPpToF, PpToF, pToF, sPToF, PToF
, unF, sUnF, UnF, unPP, sUnPP, UnPP, primePP, PrimePP, exponentPP, ExponentPP
, fPPMul, FPPMul, fMul, FMul, type (*)
, fDivides, FDivides, Divides, fDiv, FDiv, type (/)
, fGCD, FGCD, fLCM, FLCM, Coprime
, fOddRadical, FOddRadical
, pFree, PFree
, ppsFact, valueFact, totientFact, valueHatFact, radicalFact, oddRadicalFact
, ppPPow, primePPow, exponentPPow, valuePPow, totientPPow
, valuePrime
, transDivides, gcdDivides, lcmDivides, lcm2Divides
, pSplitTheorems, pFreeDivides
, (\\)
, valueHat
, PP, ppToPP, valuePP, totientPP, radicalPP, oddRadicalPP
, valuePPs, totientPPs, radicalPPs, oddRadicalPPs
, module Crypto.Lol.PosBin
) where
import Crypto.Lol.PosBin
import Control.Arrow
import Data.Constraint hiding ((***), (&&&))
import Data.Functor.Trans.Tagged
import Data.List hiding ((\\))
import Data.Singletons.Prelude hiding ((:-))
import Data.Singletons.TH
import Language.Haskell.TH
import Unsafe.Coerce
singletons [d|
newtype PrimeBin = P Bin deriving (Eq,Ord,Show)
newtype PrimePower = PP (PrimeBin,Pos) deriving (Eq,Show)
newtype Factored = F [PrimePower] deriving (Eq,Show)
unP :: PrimeBin -> Bin
unP (P p) = p
unPP :: PrimePower -> (PrimeBin,Pos)
unPP (PP pp) = pp
unF :: Factored -> [PrimePower]
unF (F pps) = pps
primePP :: PrimePower -> PrimeBin
primePP = fst . unPP
exponentPP :: PrimePower -> Pos
exponentPP = snd . unPP
|]
type F1 = 'F '[]
singletons [d|
fPPMul :: PrimePower -> Factored -> Factored
fMul :: Factored -> Factored -> Factored
fPPMul pp (F pps) = F (ppMul pp pps)
fMul (F pps1) (F pps2) = F (ppsMul pps1 pps2)
ppMul :: PrimePower -> [PrimePower] -> [PrimePower]
ppMul x [] = [x]
ppMul pp'@(PP (p',e')) pps@(pp@(PP (p,e)):pps') =
case compare p' p of
EQ -> PP (p, addPos e e') : pps'
LT -> pp' : pps
GT -> pp : ppMul pp' pps'
ppsMul :: [PrimePower] -> [PrimePower] -> [PrimePower]
ppsMul [] ys = ys
ppsMul (pp:pps) ys = ppsMul pps (ppMul pp ys)
|]
singletons [d|
pToPP :: PrimeBin -> PrimePower
pToPP p = PP (p, O)
ppToF :: PrimePower -> Factored
ppToF pp = F [pp]
pToF :: PrimeBin -> Factored
pToF = ppToF . pToPP
fGCD, fLCM :: Factored -> Factored -> Factored
fDivides :: Factored -> Factored -> Bool
fDiv :: Factored -> Factored -> Factored
fOddRadical :: Factored -> Factored
fGCD (F pps1) (F pps2) = F (ppsGCD pps1 pps2)
fLCM (F pps1) (F pps2) = F (ppsLCM pps1 pps2)
fDivides (F pps1) (F pps2) = ppsDivides pps1 pps2
fDiv (F pps1) (F pps2) = F (ppsDiv pps1 pps2)
fOddRadical (F pps) = F (ppsOddRad pps)
ppsGCD :: [PrimePower] -> [PrimePower] -> [PrimePower]
ppsGCD [] _ = []
ppsGCD (_:_) [] = []
ppsGCD xs@(PP (p,e) : xs') ys@(PP (p',e') : ys') =
case compare p p' of
EQ -> PP (p, min e e') : ppsGCD xs' ys'
LT -> ppsGCD xs' ys
GT -> ppsGCD xs ys'
ppsLCM :: [PrimePower] -> [PrimePower] -> [PrimePower]
ppsLCM [] ys = ys
ppsLCM xs@(_:_) [] = xs
ppsLCM xs@(pp@(PP (p,e)) : xs') ys@(pp'@(PP (p',e')) : ys') =
case compare p p' of
EQ -> PP (p, max e e') : ppsLCM xs' ys'
LT -> pp : ppsLCM xs' ys
GT -> pp' : ppsLCM xs ys'
ppsDivides :: [PrimePower] -> [PrimePower] -> Bool
ppsDivides [] _ = True
ppsDivides (_:_) [] = False
ppsDivides xs@(PP (p,e) : xs') (PP (p',e') : ys') =
if p == p' then (e <= e') && ppsDivides xs' ys'
else (p > p') && ppsDivides xs ys'
ppsDiv :: [PrimePower] -> [PrimePower] -> [PrimePower]
ppsDiv xs [] = xs
ppsDiv (pp@(PP (p,e)) : xs') ys@(PP (p',e') : ys') =
if p == p' && e' == e then ppsDiv xs' ys'
else if p == p' && e' <= e then PP (p, subPos e e') : ppsDiv xs' ys'
else if p <= p' then pp : ppsDiv xs' ys
else error "invalid call to ppsDiv"
ppsOddRad :: [PrimePower] -> [PrimePower]
ppsOddRad [] = []
ppsOddRad (PP (p, _) : xs') =
if p == P (D0 B1) then ppsOddRad xs'
else PP (p,O) : ppsOddRad xs'
|]
singletons [d|
pFree :: PrimeBin -> Factored -> Factored
pFree p (F pps) = F (go pps)
where go [] = []
go (pp@(PP (p',_)) : ps) =
if p == p' then ps
else pp : (go ps)
|]
type a / b = FDiv a b
type a * b = FMul a b
type Prime (p :: PrimeBin) = SingI p
type PPow (pp :: PrimePower) = SingI pp
type Fact (m :: Factored) = SingI m
reifyPrime :: Int -> (forall p . SPrimeBin p -> a) -> a
reifyPrime x _ | not $ prime x = error $ "reifyPrime: non-prime x = " ++ show x
reifyPrime x k = reifyBin x (k . SP)
reifyPrimeI :: Int -> (forall p proxy. Prime p => proxy p -> a) -> a
reifyPrimeI n k =
reifyPrime n (\(p::SPrimeBin p) -> withSingI p $ k (Proxy::Proxy p))
reifyPPow :: (Int,Int) -> (forall pp . SPrimePower pp -> a) -> a
reifyPPow (p,e) k = reifyPrime p (\sp -> reifyPos e (k . SPP . STuple2 sp))
reifyPPowI :: (Int,Int) -> (forall pp proxy. PPow pp => proxy pp -> a) -> a
reifyPPowI pp k =
reifyPPow pp $ (\(p::SPrimePower p) -> withSingI p $ k (Proxy::Proxy p))
reifyFact :: Int -> (forall m . SFactored m -> a) -> a
reifyFact m k = let pps = factorize m in reifyPPs pps $ k . SF
where reifyPPs :: [(Int,Int)]
-> (forall (pps :: [PrimePower]) . Sing pps -> a) -> a
reifyPPs [] c = c SNil
reifyPPs (pp:pps) c =
reifyPPow pp (\spp -> reifyPPs pps (\sm' -> c $ SCons spp sm'))
reifyFactI :: Int -> (forall m proxy. Fact m => proxy m -> a) -> a
reifyFactI pps k =
reifyFact pps $ (\(m::SFactored m) -> withSingI m $ k (Proxy::Proxy m))
type Divides m m' = (Fact m, Fact m', FDivides m m' ~ 'True)
type Coprime m m' = (FGCD m m' ~ F1)
coerceFDivs :: p m -> p' m' -> (() :- (FDivides m m' ~ 'True))
coerceFDivs _ _ = Sub $ unsafeCoerce (Dict :: Dict ())
coerceGCD :: p a -> p' a' -> p'' a'' -> (() :- (FGCD a a' ~ a''))
coerceGCD _ _ _ = Sub $ unsafeCoerce (Dict :: Dict ())
transDivides :: forall k l m . Proxy k -> Proxy l -> Proxy m ->
((k `Divides` l, l `Divides` m) :- (k `Divides` m))
transDivides k _ m = Sub Dict \\ coerceFDivs k m
gcdDivides :: forall m1 m2 g . Proxy m1 -> Proxy m2 ->
((Fact m1, Fact m2, g ~ FGCD m1 m2) :-
(g `Divides` m1, g `Divides` m2))
gcdDivides m1 m2 =
Sub $ withSingI (sFGCD (sing :: SFactored m1) (sing :: SFactored m2))
Dict \\ coerceFDivs (Proxy::Proxy g) m1
\\ coerceFDivs (Proxy::Proxy g) m2
lcmDivides :: forall m1 m2 l . Proxy m1 -> Proxy m2 ->
((Fact m1, Fact m2, l ~ FLCM m1 m2) :-
(m1 `Divides` l, m2 `Divides` l))
lcmDivides m1 m2 =
Sub $ withSingI (sFLCM (sing :: SFactored m1) (sing :: SFactored m2))
Dict \\ coerceFDivs m1 (Proxy::Proxy l)
\\ coerceFDivs m2 (Proxy::Proxy l)
lcm2Divides :: forall m1 m2 l m . Proxy m1 -> Proxy m2 -> Proxy m ->
((m1 `Divides` m, m2 `Divides` m, l ~ FLCM m1 m2) :-
(m1 `Divides` l, m2 `Divides` l, (FLCM m1 m2) `Divides` m))
lcm2Divides m1 m2 m =
Sub $ withSingI (sFLCM (sing :: SFactored m1) (sing :: SFactored m2))
Dict \\ coerceFDivs (Proxy::Proxy (FLCM m1 m2)) m \\ lcmDivides m1 m2
pSplitTheorems :: forall p m f . Proxy p -> Proxy m ->
((Prime p, Fact m, f ~ PFree p m) :-
(f `Divides` m, Coprime (PToF p) f))
pSplitTheorems _ m =
Sub $ withSingI (sPFree (sing :: SPrimeBin p) (sing :: SFactored m))
Dict \\ coerceFDivs (Proxy::Proxy f) m
\\ coerceGCD (Proxy::Proxy (PToF p)) (Proxy::Proxy f) (Proxy::Proxy F1)
pFreeDivides :: forall p m m' . Proxy p -> Proxy m -> Proxy m' ->
((Prime p, m `Divides` m') :-
((PFree p m) `Divides` (PFree p m')))
pFreeDivides _ _ _ =
Sub $ withSingI (sPFree (sing :: SPrimeBin p) (sing :: SFactored m)) $
withSingI (sPFree (sing :: SPrimeBin p) (sing :: SFactored m')) $
Dict \\ coerceFDivs (Proxy::Proxy (PFree p m)) (Proxy::Proxy (PFree p m'))
type PP = (Int, Int)
ppsFact :: forall m . Fact m => Tagged m [PP]
ppsFact = tag $ map ppToPP $ unF $ fromSing (sing :: SFactored m)
valueFact, totientFact, valueHatFact, radicalFact, oddRadicalFact ::
Fact m => Tagged m Int
valueFact = valuePPs <$> ppsFact
totientFact = totientPPs <$> ppsFact
valueHatFact = valueHat <$> valueFact
radicalFact = radicalPPs <$> ppsFact
oddRadicalFact = oddRadicalPPs <$> ppsFact
ppPPow :: forall pp . PPow pp => Tagged pp PP
ppPPow = tag $ ppToPP $ fromSing (sing :: SPrimePower pp)
primePPow, exponentPPow, valuePPow, totientPPow :: PPow pp => Tagged pp Int
primePPow = fst <$> ppPPow
exponentPPow = snd <$> ppPPow
valuePPow = valuePP <$> ppPPow
totientPPow = totientPP <$> ppPPow
valuePrime :: forall p . Prime p => Tagged p Int
valuePrime = tag $ binToInt $ unP $ fromSing (sing :: SPrimeBin p)
valueHat :: Integral i => i -> i
valueHat m = if m `mod` 2 == 0 then m `div` 2 else m
ppToPP :: PrimePower -> PP
ppToPP = (binToInt . unP *** posToInt) . unPP
valuePP, totientPP, radicalPP, oddRadicalPP :: PP -> Int
valuePP (p,e) = p^e
totientPP (_,0) = 1
totientPP (p,e) = (p1)*(p^(e1))
radicalPP (_,0) = 1
radicalPP (p,_) = p
oddRadicalPP (2,_) = 1
oddRadicalPP (p,_) = p
valuePPs, totientPPs, radicalPPs, oddRadicalPPs :: [PP] -> Int
valuePPs = product . map valuePP
totientPPs = product . map totientPP
radicalPPs = product . map radicalPP
oddRadicalPPs = product . map oddRadicalPP
pType :: Int -> TypeQ
pType p
| prime p = conT 'P `appT` binType p
| otherwise = fail $ "pType : non-prime p " ++ show p
ppType :: PP -> TypeQ
ppType (p,e) = conT 'PP `appT`
(promotedTupleT 2 `appT` pType p `appT` posType e)
fType :: Int -> TypeQ
fType n = conT 'F `appT` (foldr (\pp -> appT (promotedConsT `appT` ppType pp))
promotedNilT $ factorize n)
pDec :: Int -> DecQ
pDec p = tySynD (mkName $ "Prime" ++ show p) [] $ pType p
ppDec :: PP -> DecQ
ppDec pp@(p,e) = tySynD (mkName $ "PP" ++ show (p^e)) [] $ ppType pp
fDec :: Int -> DecQ
fDec n = tySynD (mkName $ 'F' : show n) [] $ fType n
factorize' :: [Int] -> Int -> [Int]
factorize' _ 1 = []
factorize' ds@(d:ds') n
| n > 1 = if d * d > n then [n]
else let (q,r) = n `divMod` d
in if r == 0 then d : factorize' ds q
else factorize' ds' n
factorize' _ n = error $ "can't factorize non-positive n = " ++ show n
factorize :: Int -> [(Int,Int)]
factorize = map (head &&& length) . group . factorize' primes