{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}

-- | Complex multiplication as a structure-constant contraction in
-- @Circuit.Mat@.
--
-- A complex number is a vector @(F 2 -> s)@: slot 0 is real, slot 1 is
-- imaginary.  The product is the contraction of the outer product against the
-- structure-constant tensor of @R[x]/(x² + 1)@.
module Circuit.Mat.Complex
  ( complexSMul,
    structureConst,
  )
where

import Circuit.Mat (Finite, Mat (..), runMat)
import Circuit.Mat.Harpie (F (..), fromF)
import Harpie.Shape (fromFin)
import NumHask.Algebra.Additive (Additive (..), Subtractive (..))
import NumHask.Algebra.Multiplicative (Multiplicative (..))
import Prelude hiding (id, negate, sum, (*), (+), (-))

-- | Structure-constant tensor for @ℂ = R[x]/(x² + 1)@.
--
-- @c k i j@ is the coefficient of @a[i] * b[j]@ in output component @k@.
structureConst ::
  (Additive s, Multiplicative s, Subtractive s) =>
  F 2 ->
  F 2 ->
  F 2 ->
  s
structureConst :: forall s.
(Additive s, Multiplicative s, Subtractive s) =>
F 2 -> F 2 -> F 2 -> s
structureConst F 2
i F 2
j F 2
k =
  case (F 2 -> Int
forall {s :: Nat}. F s -> Int
ix F 2
i, F 2 -> Int
forall {s :: Nat}. F s -> Int
ix F 2
j, F 2 -> Int
forall {s :: Nat}. F s -> Int
ix F 2
k) of
    (Int
0, Int
0, Int
0) -> s
forall a. Multiplicative a => a
one
    (Int
1, Int
1, Int
0) -> s
forall a. Additive a => a
zero s -> s -> s
forall a. Subtractive a => a -> a -> a
- s
forall a. Multiplicative a => a
one
    (Int
0, Int
1, Int
1) -> s
forall a. Multiplicative a => a
one
    (Int
1, Int
0, Int
1) -> s
forall a. Multiplicative a => a
one
    (Int, Int, Int)
_ -> s
forall a. Additive a => a
zero
  where
    ix :: F s -> Int
ix = Fin s -> Int
forall {k} (s :: k). Fin s -> Int
fromFin (Fin s -> Int) -> (F s -> Fin s) -> F s -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. F s -> Fin s
forall (n :: Nat). F n -> Fin n
fromF

-- | Complex multiplication as a @Mat@ contraction.
--
-- @complexSMul a b k@ returns component @k@ of the product of the two complex
-- numbers @a@ and @b@.
complexSMul ::
  (Additive s, Multiplicative s, Subtractive s, Eq (F 2), Eq (F 2, F 2), Finite (F 2, F 2)) =>
  (F 2 -> s) ->
  (F 2 -> s) ->
  F 2 ->
  s
complexSMul :: forall s.
(Additive s, Multiplicative s, Subtractive s, Eq (F 2),
 Eq (F 2, F 2), Finite (F 2, F 2)) =>
(F 2 -> s) -> (F 2 -> s) -> F 2 -> s
complexSMul F 2 -> s
a F 2 -> s
b = Mat s () (F 2) -> () -> F 2 -> s
forall s j i.
(Additive s, Multiplicative s, Eq j) =>
Mat s i j -> i -> j -> s
runMat (Mat s (F 2, F 2) (F 2)
cMat Mat s (F 2, F 2) (F 2) -> Mat s () (F 2, F 2) -> Mat s () (F 2)
forall s j1 j i. Mat s j1 j -> Mat s i j1 -> Mat s i j
`Comp` Mat s () (F 2, F 2)
outerProd) ()
  where
    outerProd :: Mat s () (F 2, F 2)
outerProd = (() -> (F 2, F 2) -> s) -> Mat s () (F 2, F 2)
forall i j s. (Finite i, Finite j) => (i -> j -> s) -> Mat s i j
Mat ((() -> (F 2, F 2) -> s) -> Mat s () (F 2, F 2))
-> (() -> (F 2, F 2) -> s) -> Mat s () (F 2, F 2)
forall a b. (a -> b) -> a -> b
$ \() (F 2
i, F 2
j) -> F 2 -> s
a F 2
i s -> s -> s
forall a. Multiplicative a => a -> a -> a
* F 2 -> s
b F 2
j
    cMat :: Mat s (F 2, F 2) (F 2)
cMat = ((F 2, F 2) -> F 2 -> s) -> Mat s (F 2, F 2) (F 2)
forall i j s. (Finite i, Finite j) => (i -> j -> s) -> Mat s i j
Mat (((F 2, F 2) -> F 2 -> s) -> Mat s (F 2, F 2) (F 2))
-> ((F 2, F 2) -> F 2 -> s) -> Mat s (F 2, F 2) (F 2)
forall a b. (a -> b) -> a -> b
$ \(F 2
i, F 2
j) F 2
k -> F 2 -> F 2 -> F 2 -> s
forall s.
(Additive s, Multiplicative s, Subtractive s) =>
F 2 -> F 2 -> F 2 -> s
structureConst F 2
i F 2
j F 2
k