{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExplicitNamespaces #-}

-- |
-- Module      : Data.Rhythm.Binary.Christoffel
-- Description : Binary Christoffel words
-- Copyright   : (c) Eric Bailey, 2025
--
-- License     : MIT
-- Maintainer  : eric@ericb.me
-- Stability   : stable
-- Portability : POSIX
--
-- Binary Christoffel words.
module Data.Rhythm.Binary.Christoffel
  ( -- * Ergonomic
    christoffelWord,

    -- * Safe
    christoffelWord',
  )
where

import Control.Arrow (first, second)
import Data.Bool (bool)
import Data.Finite (Finite, getFinite)
import Data.Proxy (Proxy (..))
import Data.Ratio (denominator, numerator)
import Data.Rhythm.Internal (cycleVector)
import Data.Vector.Sized (Vector)
import Data.Vector.Sized qualified as VS
import GHC.TypeLits.Witnesses (SNat (..), (%+), (%-))
import GHC.TypeNats (KnownNat, SomeNat (..), natVal, someNatVal, type (+), type (-))

-- $setup
-- >>> import Data.Finite (getFinite)
-- >>> import Data.Ratio ((%))

-- | See 'christoffelWord''.
--
-- >>> christoffelWord False (3 % 7) 10
-- [0,0,0,1,0,0,1,0,0,1]
--
-- >>> christoffelWord True (3 % 7) 10
-- [1,0,0,1,0,0,1,0,0,0]
--
-- >>> christoffelWord True (3 % 7) 20
-- [1,0,0,1,0,0,1,0,0,0,1,0,0,1,0,0,1,0,0,0]
christoffelWord :: Bool -> Rational -> Int -> [Integer]
christoffelWord :: Bool -> Rational -> Int -> [Integer]
christoffelWord Bool
isUpperWord Rational
slope Int
nTerms =
  case (Natural -> SomeNat
someNatVal (Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
nTerms), Natural -> SomeNat
someNatVal Natural
n, Natural -> SomeNat
someNatVal Natural
d) of
    (SomeNat (Proxy n
_ :: Proxy k), SomeNat (Proxy n
_ :: Proxy n), SomeNat (Proxy n
_ :: Proxy d)) ->
      Vector n Integer -> [Integer]
forall (n :: Natural) a. Vector n a -> [a]
VS.toList (Vector n Integer -> [Integer]) -> Vector n Integer -> [Integer]
forall a b. (a -> b) -> a -> b
$
        (Finite 2 -> Integer) -> Vector n (Finite 2) -> Vector n Integer
forall a b (n :: Natural). (a -> b) -> Vector n a -> Vector n b
VS.map Finite 2 -> Integer
forall (n :: Natural). Finite n -> Integer
getFinite (Vector n (Finite 2) -> Vector n Integer)
-> Vector n (Finite 2) -> Vector n Integer
forall a b. (a -> b) -> a -> b
$
          forall (m :: Natural) (n :: Natural) (d :: Natural).
(KnownNat m, KnownNat n, KnownNat d) =>
Bool -> Vector m (Finite 2)
christoffelWord' @k @n @d Bool
isUpperWord
  where
    (Natural
n, Natural
d) = (Integer -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
slope), Integer -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Rational -> Integer
forall a. Ratio a -> a
denominator Rational
slope))

-- | Generate the upper or lower Christoffel word for a given slope with a given
-- number of terms.
--
-- >>> map getFinite $ VS.toList $ christoffelWord' @10 @3 @7 False
-- [0,0,0,1,0,0,1,0,0,1]
--
-- >>> map getFinite $ VS.toList $ christoffelWord' @10 @3 @7 True
-- [1,0,0,1,0,0,1,0,0,0]
--
-- >>> map getFinite $ VS.toList $ christoffelWord' @20 @3 @7 True
-- [1,0,0,1,0,0,1,0,0,0,1,0,0,1,0,0,1,0,0,0]
christoffelWord' ::
  forall m n d.
  (KnownNat m, KnownNat n, KnownNat d) =>
  Bool ->
  Vector m (Finite 2)
christoffelWord' :: forall (m :: Natural) (n :: Natural) (d :: Natural).
(KnownNat m, KnownNat n, KnownNat d) =>
Bool -> Vector m (Finite 2)
christoffelWord' Bool
isUpperWord =
  case (SNat n
forall (n :: Natural). KnownNat n => SNat n
SNat :: SNat n) SNat n -> SNat (d - 1) -> SNat (n + (d - 1))
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n + m)
%+ ((SNat d
forall (n :: Natural). KnownNat n => SNat n
SNat :: SNat d) SNat d -> SNat 1 -> SNat (d - 1)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n - m)
%- (SNat 1
forall (n :: Natural). KnownNat n => SNat n
SNat :: SNat 1)) of
    SNat (n + (d - 1))
SNat ->
      case (SNat 1
forall (n :: Natural). KnownNat n => SNat n
SNat :: SNat 1) SNat 1 -> SNat (n + (d - 1)) -> SNat (1 + (n + (d - 1)))
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n + m)
%+ ((SNat n
forall (n :: Natural). KnownNat n => SNat n
SNat :: SNat n) SNat n -> SNat (d - 1) -> SNat (n + (d - 1))
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n + m)
%+ ((SNat d
forall (n :: Natural). KnownNat n => SNat n
SNat :: SNat d) SNat d -> SNat 1 -> SNat (d - 1)
forall (n :: Natural) (m :: Natural).
SNat n -> SNat m -> SNat (n - m)
%- (SNat 1
forall (n :: Natural). KnownNat n => SNat n
SNat :: SNat 1))) of
        SNat (1 + (n + (d - 1)))
SNat ->
          Vector (1 + (n + (d - 1))) (Finite 2) -> Vector m (Finite 2)
forall (m :: Natural) (n :: Natural) a.
(KnownNat m, KnownNat n) =>
Vector n a -> Vector m a
cycleVector (Vector (1 + (n + (d - 1))) (Finite 2) -> Vector m (Finite 2))
-> Vector (1 + (n + (d - 1))) (Finite 2) -> Vector m (Finite 2)
forall a b. (a -> b) -> a -> b
$
            Finite 2
-> Vector (n + (d - 1)) (Finite 2)
-> Vector (1 + (n + (d - 1))) (Finite 2)
forall (n :: Natural) a. a -> Vector n a -> Vector (1 + n) a
VS.cons (Finite 2 -> Finite 2 -> Bool -> Finite 2
forall a. a -> a -> Bool -> a
bool Finite 2
0 Finite 2
1 Bool
isUpperWord) (Vector (n + (d - 1)) (Finite 2)
 -> Vector (1 + (n + (d - 1))) (Finite 2))
-> Vector (n + (d - 1)) (Finite 2)
-> Vector (1 + (n + (d - 1))) (Finite 2)
forall a b. (a -> b) -> a -> b
$
              forall (n :: Natural) a b.
KnownNat n =>
(b -> (a, b)) -> b -> Vector n a
VS.unfoldrN @(n + (d - 1)) (Integer, Integer) -> (Finite 2, (Integer, Integer))
forall {a}. Num a => (Integer, Integer) -> (a, (Integer, Integer))
go (Integer
n, Integer
d)
  where
    go :: (Integer, Integer) -> (a, (Integer, Integer))
go (Integer, Integer)
slope = case (Integer -> Integer -> Ordering) -> (Integer, Integer) -> Ordering
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Integer, Integer)
slope of
      Ordering
GT -> (a
1, (Integer -> Integer) -> (Integer, Integer) -> (Integer, Integer)
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
d) (Integer, Integer)
slope)
      Ordering
EQ -> (a -> a -> Bool -> a
forall a. a -> a -> Bool -> a
bool a
1 a
0 Bool
isUpperWord, (Integer
n, Integer
d))
      Ordering
LT -> (a
0, (Integer -> Integer) -> (Integer, Integer) -> (Integer, Integer)
forall b c d. (b -> c) -> (b, d) -> (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
n) (Integer, Integer)
slope)
    n, d :: Integer
    n :: Integer
n = Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Natural
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n))
    d :: Integer
d = Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy d -> Natural
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @d))