Skip to content

Instantly share code, notes, and snippets.

@notogawa

notogawa/Sample.hs

Created Feb 11, 2018
Embed
What would you like to do?
for #questions haskell-jp.slack.com
{-# 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