{-# LANGUAGE KindSignatures, DataKinds, ScopedTypeVariables #-}
module Restklassenring where

import GHC.TypeLits
import Data.Proxy

newtype Restklassenring (n :: Nat) a = Val {getVal :: a}

getIntegral :: (Integral a, KnownNat n) => Proxy n -> a
getIntegral = fromInteger . toInteger . natVal

instance (Integral a, Num a, KnownNat n) => Num (Restklassenring n a) where
  (Val a) + (Val b) = Val $ (a + b) `mod` (getIntegral (Proxy :: Proxy n))
  (Val a) * (Val b) = Val $ (a * b) `mod` (getIntegral (Proxy :: Proxy n))
  signum            = const $ Val $ fromInteger $ 1
  abs               = id
  negate (Val a)    = let
    modulus = toInteger $ natVal (Proxy :: Proxy n)
    a' = toInteger a
    b = modulus - a' in
    fromInteger b
  fromInteger i | i >= 0    = Val $ (fromInteger i) `mod` (getIntegral (Proxy :: Proxy n))
                | otherwise = negate $ fromInteger $ negate i

instance (Show a) => Show (Restklassenring n a) where
  show (Val a) = show a

x :: Restklassenring 7 Integer
x = 13

y :: Restklassenring 7 Integer
y = -2


main :: IO ()
main = do
  print x -- 6
  print y -- 5
  print (x + y) -- 4