{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE OverloadedStrings #-}

-----------------------------------------------------------------------------
{-|
Module      : Math.Tensor.Basic.Epsilon
Description : Definitions of epsilon tensor densities.
Copyright   : (c) Nils Alex, 2020
License     : MIT
Maintainer  : nils.alex@fau.de

Definitions of covariant and contravariant epsilon tensor densities
like \(\epsilon_{abc}\).
-}
-----------------------------------------------------------------------------
module Math.Tensor.Basic.Epsilon
  ( -- * Epsilon tensor densities
    epsilon'
  , someEpsilon
  , epsilonInv'
  , someEpsilonInv
  , -- * Internals
    permSign
  ) where

import Math.Tensor
import Math.Tensor.Safe
import Math.Tensor.Safe.TH
import Math.Tensor.Basic.TH

import Data.Singletons
  ( Sing
  , SingI (sing)
  , Demote
  , withSomeSing
  , withSingI
  , fromSing
  )
import Data.Singletons.Prelude
import Data.Singletons.Decide
  ( (:~:) (Refl)
  , Decision (Proved)
  , (%~)
  )
import Data.Singletons.TypeLits
  ( Symbol
  , Nat
  , KnownNat
  , withKnownNat
  )

import Data.List (sort,permutations)
import qualified Data.List.NonEmpty as NE (NonEmpty((:|)),sort)

import Control.Monad.Except (MonadError, throwError)

-- |Sign of a permutation:
--
-- @
--   permSign [1,2,3] = 1
--   permSign [2,1,3] = -1
-- @
permSign :: (Num v, Ord a) => [a] -> v
permSign :: [a] -> v
permSign (a
x:[a]
xs)
    | Int -> Bool
forall a. Integral a => a -> Bool
even ([a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [a]
defects) = [a] -> v
forall v a. (Num v, Ord a) => [a] -> v
permSign [a]
xs
    | Int -> Bool
forall a. Integral a => a -> Bool
odd ([a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [a]
defects)  = (-v
1) v -> v -> v
forall a. Num a => a -> a -> a
* [a] -> v
forall v a. (Num v, Ord a) => [a] -> v
permSign [a]
xs
  where
    defects :: [a]
defects = (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
filter (a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<a
x) [a]
xs
permSign [a]
_ = v
1

-- |Totally antisymmetric covariant tensor density of weight -1
-- such that
--
-- \[ \epsilon_{12\dots n} = 1. \]
--
-- Vector space label, vector space dimension and index labels
-- are passed as singletons.
epsilon' :: forall (id :: Symbol) (n :: Nat) (is :: NE.NonEmpty Symbol) (r :: Rank) v.
              (
               KnownNat n,
               Num v,
               EpsilonRank id n is ~ 'Just r,
               SingI r
              ) =>
              Sing id -> Sing n -> Sing is -> Tensor r v
epsilon' :: Sing id -> Sing n -> Sing is -> Tensor r v
epsilon' Sing id
_ Sing n
sn Sing is
_ =
    case Sing r -> Sing (Apply LengthRSym0 r)
forall s n (t :: [(VSpace s n, IList s)]).
Sing t -> Sing (Apply LengthRSym0 t)
sLengthR Sing r
sr Sing (LengthR r)
-> Sing (Case_6989586621679113968 n (DefaultEq n 0))
-> Decision
     (LengthR r :~: Case_6989586621679113968 n (DefaultEq n 0))
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing (Case_6989586621679113968 n (DefaultEq n 0))
Sing (Apply FromNatSym0 n)
sn' of
      Proved LengthR r :~: Case_6989586621679113968 n (DefaultEq n 0)
Refl ->
        case Sing r -> Sing (Apply SaneSym0 r)
forall a b (t :: [(VSpace a b, IList a)]).
(SOrd a, SOrd b) =>
Sing t -> Sing (Apply SaneSym0 t)
sSane Sing r
sr Sing (Sane r) -> Sing 'True -> Decision (Sane r :~: 'True)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ SBool 'True
Sing 'True
STrue of
          Proved Sane r :~: 'True
Refl -> [(Vec (Case_6989586621679113968 n (DefaultEq n 0)) Int, v)]
-> Tensor r v
forall (r :: [(VSpace Symbol Nat, IList Symbol)]) v (n :: N).
(SingI r, Sane r ~ 'True, LengthR r ~ n) =>
[(Vec n Int, v)] -> Tensor r v
fromList [(Vec (Case_6989586621679113968 n (DefaultEq n 0)) Int, v)]
xs
  where
    sr :: Sing r
sr = Sing r
forall k (a :: k). SingI a => Sing a
sing :: Sing r
    sn' :: Sing (Apply FromNatSym0 n)
sn' = Sing n -> Sing (Apply FromNatSym0 n)
forall (t :: Nat). Sing t -> Sing (Apply FromNatSym0 t)
sFromNat Sing n
sn
    n :: Demote Nat
n = Sing n -> Demote Nat
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing n
sn
    perms :: [[Int]]
perms = [[Int]] -> [[Int]]
forall a. Ord a => [a] -> [a]
sort ([[Int]] -> [[Int]]) -> [[Int]] -> [[Int]]
forall a b. (a -> b) -> a -> b
$ [Int] -> [[Int]]
forall a. [a] -> [[a]]
permutations ([Int] -> [[Int]]) -> [Int] -> [[Int]]
forall a b. (a -> b) -> a -> b
$ Int -> [Int] -> [Int]
forall a. Int -> [a] -> [a]
take (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
Demote Nat
n) [(Int
0 :: Int)..]
    xs :: [(Vec (Case_6989586621679113968 n (DefaultEq n 0)) Int, v)]
xs = ([Int]
 -> (Vec (Case_6989586621679113968 n (DefaultEq n 0)) Int, v))
-> [[Int]]
-> [(Vec (Case_6989586621679113968 n (DefaultEq n 0)) Int, v)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (\[Int]
p -> (Sing (Case_6989586621679113968 n (DefaultEq n 0))
-> [Int] -> Vec (Case_6989586621679113968 n (DefaultEq n 0)) Int
forall (n :: N) a. Sing n -> [a] -> Vec n a
vecFromListUnsafe Sing (Case_6989586621679113968 n (DefaultEq n 0))
Sing (Apply FromNatSym0 n)
sn' [Int]
p, [Int] -> v
forall v a. (Num v, Ord a) => [a] -> v
permSign [Int]
p :: v)) [[Int]]
perms

-- |Totally antisymmetric contravariant tensor density of weight +1
-- such that
--
-- \[ \epsilon^{12\dots n} = 1. \]
--
-- Vector space label, vector space dimension and index labels
-- are passed as singletons.
epsilonInv' :: forall (id :: Symbol) (n :: Nat) (is :: NE.NonEmpty Symbol) (r :: Rank) v.
              (
               KnownNat n,
               Num v,
               EpsilonInvRank id n is ~ 'Just r,
               SingI r
              ) =>
              Sing id -> Sing n -> Sing is -> Tensor r v
epsilonInv' :: Sing id -> Sing n -> Sing is -> Tensor r v
epsilonInv' Sing id
_ Sing n
sn Sing is
_ =
    case Sing r -> Sing (Apply LengthRSym0 r)
forall s n (t :: [(VSpace s n, IList s)]).
Sing t -> Sing (Apply LengthRSym0 t)
sLengthR Sing r
sr Sing (LengthR r)
-> Sing (Case_6989586621679113968 n (DefaultEq n 0))
-> Decision
     (LengthR r :~: Case_6989586621679113968 n (DefaultEq n 0))
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing (Case_6989586621679113968 n (DefaultEq n 0))
Sing (Apply FromNatSym0 n)
sn' of
      Proved LengthR r :~: Case_6989586621679113968 n (DefaultEq n 0)
Refl ->
        case Sing r -> Sing (Apply SaneSym0 r)
forall a b (t :: [(VSpace a b, IList a)]).
(SOrd a, SOrd b) =>
Sing t -> Sing (Apply SaneSym0 t)
sSane Sing r
sr Sing (Sane r) -> Sing 'True -> Decision (Sane r :~: 'True)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ SBool 'True
Sing 'True
STrue of
          Proved Sane r :~: 'True
Refl -> [(Vec (Case_6989586621679113968 n (DefaultEq n 0)) Int, v)]
-> Tensor r v
forall (r :: [(VSpace Symbol Nat, IList Symbol)]) v (n :: N).
(SingI r, Sane r ~ 'True, LengthR r ~ n) =>
[(Vec n Int, v)] -> Tensor r v
fromList [(Vec (Case_6989586621679113968 n (DefaultEq n 0)) Int, v)]
xs
  where
    sr :: Sing r
sr = Sing r
forall k (a :: k). SingI a => Sing a
sing :: Sing r
    sn' :: Sing (Apply FromNatSym0 n)
sn' = Sing n -> Sing (Apply FromNatSym0 n)
forall (t :: Nat). Sing t -> Sing (Apply FromNatSym0 t)
sFromNat Sing n
sn
    n :: Demote Nat
n = Sing n -> Demote Nat
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing n
sn
    perms :: [[Int]]
perms = [[Int]] -> [[Int]]
forall a. Ord a => [a] -> [a]
sort ([[Int]] -> [[Int]]) -> [[Int]] -> [[Int]]
forall a b. (a -> b) -> a -> b
$ [Int] -> [[Int]]
forall a. [a] -> [[a]]
permutations ([Int] -> [[Int]]) -> [Int] -> [[Int]]
forall a b. (a -> b) -> a -> b
$ Int -> [Int] -> [Int]
forall a. Int -> [a] -> [a]
take (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
Demote Nat
n) [(Int
0 :: Int)..]
    xs :: [(Vec (Case_6989586621679113968 n (DefaultEq n 0)) Int, v)]
xs = ([Int]
 -> (Vec (Case_6989586621679113968 n (DefaultEq n 0)) Int, v))
-> [[Int]]
-> [(Vec (Case_6989586621679113968 n (DefaultEq n 0)) Int, v)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (\[Int]
p -> (Sing (Case_6989586621679113968 n (DefaultEq n 0))
-> [Int] -> Vec (Case_6989586621679113968 n (DefaultEq n 0)) Int
forall (n :: N) a. Sing n -> [a] -> Vec n a
vecFromListUnsafe Sing (Case_6989586621679113968 n (DefaultEq n 0))
Sing (Apply FromNatSym0 n)
sn' [Int]
p, [Int] -> v
forall v a. (Num v, Ord a) => [a] -> v
permSign [Int]
p :: v)) [[Int]]
perms

-- |Totally antisymmetric covariant tensor density of weight -1
-- such that
--
-- \[ \epsilon_{12\dots n} = 1. \]
--
-- Vector space label, vector space dimension and index labels
-- are passed as values. Result is existentially quantified.
someEpsilon :: forall v m.(Num v, MonadError String m) =>
               Demote Symbol -> Demote Nat -> [Demote Symbol] ->
               m (T v)
someEpsilon :: Demote Symbol -> Demote Nat -> [Demote Symbol] -> m (T v)
someEpsilon Demote Symbol
_ Demote Nat
_ [] = String -> m (T v)
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError String
"Empty index list!"
someEpsilon Demote Symbol
vid Demote Nat
vdim (Demote Symbol
i:[Demote Symbol]
is) =
  let sign :: v
sign = [Text] -> v
forall v a. (Num v, Ord a) => [a] -> v
permSign (Text
Demote Symbol
iText -> [Text] -> [Text]
forall a. a -> [a] -> [a]
:[Text]
[Demote Symbol]
is) :: v
  in Demote Symbol
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (T v)
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Symbol
vid ((forall (a :: Symbol). Sing a -> m (T v)) -> m (T v))
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
svid ->
     Demote Nat -> (forall (a :: Nat). Sing a -> m (T v)) -> m (T v)
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Nat
vdim ((forall (a :: Nat). Sing a -> m (T v)) -> m (T v))
-> (forall (a :: Nat). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
svdim ->
     Demote (NonEmpty Symbol)
-> (forall (a :: NonEmpty Symbol). Sing a -> m (T v)) -> m (T v)
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing (NonEmpty Text -> NonEmpty Text
forall a. Ord a => NonEmpty a -> NonEmpty a
NE.sort (Text
Demote Symbol
i Text -> [Text] -> NonEmpty Text
forall a. a -> [a] -> NonEmpty a
NE.:| [Text]
[Demote Symbol]
is)) ((forall (a :: NonEmpty Symbol). Sing a -> m (T v)) -> m (T v))
-> (forall (a :: NonEmpty Symbol). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
sis ->
     Sing a -> (KnownNat a => m (T v)) -> m (T v)
forall (n :: Nat) r. Sing n -> (KnownNat n => r) -> r
withKnownNat Sing a
svdim ((KnownNat a => m (T v)) -> m (T v))
-> (KnownNat a => m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$
     case Sing a
-> Sing a
-> Sing a
-> Sing (Apply (Apply (Apply EpsilonRankSym0 a) a) a)
forall (t1 :: Symbol) (t2 :: Nat) (t3 :: NonEmpty Symbol).
Sing t1
-> Sing t2
-> Sing t3
-> Sing (Apply (Apply (Apply EpsilonRankSym0 t1) t2) t3)
sEpsilonRank Sing a
svid Sing a
svdim Sing a
sis of
       SJust sr ->
         Sing n -> (SingI n => m (T v)) -> m (T v)
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
sr ((SingI n => m (T v)) -> m (T v))
-> (SingI n => m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$
         T v -> m (T v)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (T v -> m (T v)) -> T v -> m (T v)
forall a b. (a -> b) -> a -> b
$ Tensor n v -> T v
forall (r :: [(VSpace Symbol Nat, IList Symbol)]) v.
SingI r =>
Tensor r v -> T v
T (Tensor n v -> T v) -> Tensor n v -> T v
forall a b. (a -> b) -> a -> b
$ (v -> v -> v
forall a. Num a => a -> a -> a
* v
sign) (v -> v) -> Tensor n v -> Tensor n v
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Sing a -> Sing a -> Sing a -> Tensor n v
forall (id :: Symbol) (n :: Nat) (is :: NonEmpty Symbol)
       (r :: [(VSpace Symbol Nat, IList Symbol)]) v.
(KnownNat n, Num v, EpsilonRank id n is ~ 'Just r, SingI r) =>
Sing id -> Sing n -> Sing is -> Tensor r v
epsilon' Sing a
svid Sing a
svdim Sing a
sis
       Sing (Apply (Apply (Apply EpsilonRankSym0 a) a) a)
SNothing -> String -> m (T v)
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (String -> m (T v)) -> String -> m (T v)
forall a b. (a -> b) -> a -> b
$ String
"Illegal index list " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Text] -> String
forall a. Show a => a -> String
show (Text
Demote Symbol
iText -> [Text] -> [Text]
forall a. a -> [a] -> [a]
:[Text]
[Demote Symbol]
is) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"!"

-- |Totally antisymmetric contravariant tensor density of weight +1
-- such that
--
-- \[ \epsilon^{12\dots n} = 1. \]
--
-- Vector space label, vector space dimension and index labels
-- are passed as values. Result is existentially quantified.
someEpsilonInv :: forall v m.(Num v, MonadError String m) =>
                  Demote Symbol -> Demote Nat -> [Demote Symbol] ->
                  m (T v)
someEpsilonInv :: Demote Symbol -> Demote Nat -> [Demote Symbol] -> m (T v)
someEpsilonInv Demote Symbol
_ Demote Nat
_ [] = String -> m (T v)
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError String
"Empty index list!"
someEpsilonInv Demote Symbol
vid Demote Nat
vdim (Demote Symbol
i:[Demote Symbol]
is) =
  let sign :: v
sign = [Text] -> v
forall v a. (Num v, Ord a) => [a] -> v
permSign (Text
Demote Symbol
iText -> [Text] -> [Text]
forall a. a -> [a] -> [a]
:[Text]
[Demote Symbol]
is) :: v
  in Demote Symbol
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (T v)
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Symbol
vid ((forall (a :: Symbol). Sing a -> m (T v)) -> m (T v))
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
svid ->
     Demote Nat -> (forall (a :: Nat). Sing a -> m (T v)) -> m (T v)
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Nat
vdim ((forall (a :: Nat). Sing a -> m (T v)) -> m (T v))
-> (forall (a :: Nat). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
svdim ->
     Demote (NonEmpty Symbol)
-> (forall (a :: NonEmpty Symbol). Sing a -> m (T v)) -> m (T v)
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing (NonEmpty Text -> NonEmpty Text
forall a. Ord a => NonEmpty a -> NonEmpty a
NE.sort (Text
Demote Symbol
i Text -> [Text] -> NonEmpty Text
forall a. a -> [a] -> NonEmpty a
NE.:| [Text]
[Demote Symbol]
is)) ((forall (a :: NonEmpty Symbol). Sing a -> m (T v)) -> m (T v))
-> (forall (a :: NonEmpty Symbol). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
sis ->
     Sing a -> (KnownNat a => m (T v)) -> m (T v)
forall (n :: Nat) r. Sing n -> (KnownNat n => r) -> r
withKnownNat Sing a
svdim ((KnownNat a => m (T v)) -> m (T v))
-> (KnownNat a => m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$
     case Sing a
-> Sing a
-> Sing a
-> Sing (Apply (Apply (Apply EpsilonInvRankSym0 a) a) a)
forall (t1 :: Symbol) (t2 :: Nat) (t3 :: NonEmpty Symbol).
Sing t1
-> Sing t2
-> Sing t3
-> Sing (Apply (Apply (Apply EpsilonInvRankSym0 t1) t2) t3)
sEpsilonInvRank Sing a
svid Sing a
svdim Sing a
sis of
       SJust sr ->
         Sing n -> (SingI n => m (T v)) -> m (T v)
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
sr ((SingI n => m (T v)) -> m (T v))
-> (SingI n => m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$
         T v -> m (T v)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (T v -> m (T v)) -> T v -> m (T v)
forall a b. (a -> b) -> a -> b
$ Tensor n v -> T v
forall (r :: [(VSpace Symbol Nat, IList Symbol)]) v.
SingI r =>
Tensor r v -> T v
T (Tensor n v -> T v) -> Tensor n v -> T v
forall a b. (a -> b) -> a -> b
$ (v -> v -> v
forall a. Num a => a -> a -> a
* v
sign) (v -> v) -> Tensor n v -> Tensor n v
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Sing a -> Sing a -> Sing a -> Tensor n v
forall (id :: Symbol) (n :: Nat) (is :: NonEmpty Symbol)
       (r :: [(VSpace Symbol Nat, IList Symbol)]) v.
(KnownNat n, Num v, EpsilonInvRank id n is ~ 'Just r, SingI r) =>
Sing id -> Sing n -> Sing is -> Tensor r v
epsilonInv' Sing a
svid Sing a
svdim Sing a
sis
       Sing (Apply (Apply (Apply EpsilonInvRankSym0 a) a) a)
SNothing -> String -> m (T v)
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (String -> m (T v)) -> String -> m (T v)
forall a b. (a -> b) -> a -> b
$ String
"Illegal index list " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Text] -> String
forall a. Show a => a -> String
show (Text
Demote Symbol
iText -> [Text] -> [Text]
forall a. a -> [a] -> [a]
:[Text]
[Demote Symbol]
is) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"!"