module Noether.Algebra.Vector.Boxed where
import qualified Prelude as P
import qualified Data.Vector as V
import Noether.Lemmata.Prelude
import Noether.Lemmata.TypeFu
import Noether.Algebra.Actions
import Noether.Algebra.Linear
import Noether.Algebra.Single
import Noether.Algebra.Tags
import Noether.Algebra.Vector.Generic
import Noether.Algebra.Vector.Tags
newtype BVector (n :: k) v =
BVector (V.Vector v)
deriving (Show)
unsafeFromList :: [a] -> BVector n a
unsafeFromList as = BVector (V.fromList as)
unsafeChangeDimension
:: forall k l (m :: k) (n :: l) a.
BVector m a -> BVector n a
unsafeChangeDimension (BVector as) = BVector as
instance (MagmaK op v s) =>
MagmaK op (BVector n v) (MagmaTagged BVectorLift s) where
binaryOpK o _ = gBinaryOpK @V.Vector @v @s o
instance (KnownNat n, NeutralK op v s) =>
NeutralK op (BVector n v) (NeutralTagged BVectorLift s) where
neutralK o _ = gNeutralK @n @V.Vector @v @s o
instance (CancellativeK op v s) =>
CancellativeK op (BVector n v) (CancellativeTagged BVectorLift s) where
cancelK o _ = gCancelK @V.Vector @v @s o
instance (ActsK lr op a b s) =>
ActsK lr op a (BVector n b) (ActsTagged BVectorLift s) where
actK o _ _ = gActK @V.Vector @a @b @s @lr o
type instance MagmaS (op :: BinaryNumeric) (BVector n a) = DeriveMagma_Tagged BVectorLift op a
type instance NeutralS (op :: BinaryNumeric) (BVector n a) = DeriveNeutral_Tagged BVectorLift op a
type instance CommutativeS (op :: BinaryNumeric) (BVector n a) = DeriveCommutative_Tagged BVectorLift op a
type instance CancellativeS Add (BVector n a) = DeriveCancellative_Tagged BVectorLift Add a
type instance SemigroupS (op :: BinaryNumeric) (BVector n a) = DeriveSemigroup_Magma op (BVector n a)
type instance MonoidS (op :: BinaryNumeric) (BVector n a) = DeriveMonoid_Semigroup_Neutral op (BVector n a)
type instance GroupS Add (BVector n a) = DeriveGroup_Monoid_Cancellative Add (BVector n a)
type instance AbelianGroupS Add (BVector n a) = DeriveAbelianGroup_Commutative_Group Add (BVector n a)
type instance ActsS lr Mul a (BVector n b) = DeriveActs_Tagged BVectorLift lr Mul a b
type instance CompatibleS lr Mul Mul a (BVector n b) = DeriveCompatible_Acts_Semigroup lr Mul Mul a (BVector n b)
type instance ActorLinearS lr Mul Add a Add (BVector n a) =
DeriveActorLinearActs_Acts_Semigroup_Semigroup lr Mul Add a Add (BVector n a)
type instance ActeeLinearS lr Mul a Add (BVector n a) =
DeriveActeeLinearActs_Acts_Semigroup lr Mul a Add (BVector n a)