Created
February 11, 2018 10:33
-
-
Save notogawa/83324a70e35049cd1ddccc005ea1a278 to your computer and use it in GitHub Desktop.
for #questions haskell-jp.slack.com
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE ConstraintKinds #-} | |
{-# LANGUAGE UndecidableInstances #-} | |
{-# LANGUAGE TypeFamilies #-} | |
{-# LANGUAGE DataKinds #-} | |
{-# LANGUAGE TypeOperators #-} | |
import Data.Typeable | |
import Data.Type.Equality | |
import GHC.TypeLits | |
import Data.Constraint (Dict(..)) | |
import Data.Singletons | |
import Data.Singletons.Prelude.Bool | |
import Data.Singletons.Prelude.Eq | |
import Data.Singletons.Prelude.Ord | |
import Data.Singletons.Prelude.Num | |
class FiniteField k where | |
hoge :: k -> String | |
newtype IntResidueClass (n :: Nat) = MkIntResidueClass Integer deriving (Show, Typeable) | |
instance (IsPrime p) => FiniteField (IntResidueClass p) where | |
hoge _ = "hogehoge" | |
type family Mod' (x :: Nat) (y :: Nat) (xGeqY :: Bool) :: Nat where | |
Mod' x y 'True = Mod' (x :- y) y (y :<= (x :- y)) | |
Mod' x y 'False = x | |
sMod' :: Sing x -> Sing y -> Sing xGeqY -> Sing (Mod' x y xGeqY) | |
sMod' sx _ SFalse = sx | |
sMod' sx sy STrue = sMod' (sx %:- sy) sy (sy %:<= (sx %:- sy)) | |
type family Mod (x :: Nat) (y :: Nat) :: Nat where | |
Mod x y = Mod' x y (y :<= x) | |
sMod :: Sing x -> Sing y -> Sing (Mod x y) | |
sMod sx sy = sMod' sx sy (sy %:<= sx) | |
type family IsPrimeB' (p :: Nat) (i :: Nat) (hasFactor :: Bool) (searchEnd :: Bool) where | |
IsPrimeB' _ _ 'True _ = 'False | |
IsPrimeB' _ _ _ 'True = 'True | |
IsPrimeB' p i _ _ = IsPrimeB' p (i :+ 2) (Mod p i :== 0) (Not ((i :+ 2) :* (i :+ 2) :<= p)) | |
s0 :: Sing 0 | |
s0 = sing | |
s1 :: Sing 1 | |
s1 = sing | |
s2 :: Sing 2 | |
s2 = sing | |
s3 :: Sing 3 | |
s3 = sing | |
sIsPrimeB' :: Sing p -> Sing i -> Sing hasFactor -> Sing searchEnd -> Sing (IsPrimeB' p i hasFactor searchEnd) | |
sIsPrimeB' p i hasFactor searchEnd = | |
case hasFactor of | |
STrue -> SFalse | |
SFalse -> case searchEnd of | |
STrue -> STrue | |
SFalse -> sIsPrimeB' p (i %:+ s2) (sMod p i %:== s0) (sNot ((i %:+ s2) %:* (i %:+ s2) %:<= p)) | |
type family IsPrimeB (p :: Nat) (is0 :: Bool) (is1 :: Bool) (is2 :: Bool) :: Bool where | |
IsPrimeB _ 'True 'False 'False = 'False | |
IsPrimeB _ 'False 'True 'False = 'False | |
IsPrimeB _ 'False 'False 'True = 'True | |
IsPrimeB p 'False 'False 'False = IsPrimeB' p 3 (Mod p 2 :== 0) (Not (3 :* 3 :<= p)) | |
sIsPrimeB :: Sing p -> Sing is0 -> Sing is1 -> Sing is2 -> Sing (IsPrimeB p is0 is1 is2) | |
sIsPrimeB _ STrue SFalse SFalse = SFalse | |
sIsPrimeB _ SFalse STrue SFalse = SFalse | |
sIsPrimeB _ SFalse SFalse STrue = STrue | |
sIsPrimeB p SFalse SFalse SFalse = sIsPrimeB' p s3 (sMod p s2 %:== s0) (sNot (s3 %:* s3 %:<= p)) | |
sIsPrimeB _ _ _ _ = error "don't reach this case" | |
type IsPrime p = IsPrimeB p (p :== 0) (p :== 1) (p :== 2) ~ 'True | |
testIsPrime :: Sing p -> Maybe (Dict (IsPrime p)) | |
testIsPrime p = case testEquality (sIsPrimeB p (p %:== s0) (p %:== s1) (p %:== s2)) STrue of | |
Nothing -> Nothing | |
Just eq -> gcastWith eq $ Just Dict | |
mkIntResidueClassFromSing :: Sing p -> Integer -> IntResidueClass p | |
mkIntResidueClassFromSing _ = MkIntResidueClass | |
main :: IO () | |
main = do | |
s <- getLine | |
let i = read s :: Integer | |
withSomeSing i $ \p -> | |
case testIsPrime p of | |
Nothing -> error $ shows i " is not prime" | |
Just Dict -> do | |
let irc = mkIntResidueClassFromSing p 0 | |
print $ hoge irc |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment