{-# LANGUAGE DataKinds, FlexibleInstances, GADTs, KindSignatures,
             MultiParamTypeClasses, ScopedTypeVariables,
             TypeApplications, TypeFamilies, TypeOperators,
             UndecidableInstances,
             CPP #-}

{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_GHC -Wno-orphans #-}

-- | Some type families to be used with GHC.KnownNat.Solver

module ConCat.KnownNatOps where

import GHC.TypeLits
import GHC.TypeLits.KnownNat
import Data.Proxy

-- When the plugin works with GHC 8.4 (base 4.11.0.0), get Div and Mod from
-- GHC.TypeNat instead of declaring here.
type family Div (m :: Nat) (n :: Nat) :: Nat
type family Mod (m :: Nat) (n :: Nat) :: Nat

instance (KnownNat a, KnownNat b) => KnownNat2 "Div" a b where
  natSing2 :: SNatKn "Div"
natSing2 = Nat -> SNatKn "Div"
forall (f :: Symbol). Nat -> SNatKn f
SNatKn (Nat -> SNatKn "Div") -> Nat -> SNatKn "Div"
forall a b. (a -> b) -> a -> b
$ Integer -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Nat) -> Integer -> Nat
forall a b. (a -> b) -> a -> b
$ (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
div (Proxy a -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy a
forall {k} (t :: k). Proxy t
Proxy ::  Proxy a)) (Proxy b -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy b
forall {k} (t :: k). Proxy t
Proxy :: Proxy b)))
  {-# INLINE natSing2 #-}

instance (KnownNat a, KnownNat b) => KnownNat2 "Mod" a b where
  natSing2 :: SNatKn "Mod"
natSing2 = Nat -> SNatKn "Mod"
forall (f :: Symbol). Nat -> SNatKn f
SNatKn (Nat -> SNatKn "Mod") -> Nat -> SNatKn "Mod"
forall a b. (a -> b) -> a -> b
$  Integer -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Nat) -> Integer -> Nat
forall a b. (a -> b) -> a -> b
$ (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
mod (Proxy a -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy a
forall {k} (t :: k). Proxy t
Proxy ::  Proxy a)) (Proxy b -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy b
forall {k} (t :: k). Proxy t
Proxy :: Proxy b)))
  {-# INLINE natSing2 #-}