{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wincomplete-patterns -Wno-orphans #-}
{-# OPTIONS_GHC -fplugin Data.Type.Natural.Presburger.MinMaxSolver #-}

#if __GLASGOW_HASKELL__ >= 806
{-# LANGUAGE NoStarIsType #-}
#endif
module Algebra.Internal
  ( (:~:) (..),
    withRefl,
    module Data.Proxy,
    module Algebra.Internal,
    module Data.Type.Ordinal,
  )
where

import Algebra.Instances ()
import AlgebraicPrelude
import qualified Data.Foldable as F
import Data.Kind (Type)
import Data.Proxy (KProxy (..), Proxy (..), asProxyTypeOf)
import qualified Data.Sequence as Seq
#if MIN_VERSION_singletons(3,0,0)
import Data.Singletons as Algebra.Internal
  ( Sing,
    SingI (..),
    SingKind (..),
    SomeSing (..),
    withSingI,
  )
import qualified GHC.TypeLits.Singletons as Sing
#else
import Data.Singletons.Prelude as Algebra.Internal
  ( Sing,
    SingI (..),
    SingKind (..),
    SomeSing (..),
    withSingI,
  )
import qualified Data.Singletons.TypeLits as Sing
#endif

import Data.Sized as Algebra.Internal
  ( generate,
    sIndex,
    singleton,
    unsafeFromList,
    unsafeFromList',
    zipWithSame,
    pattern Nil,
    pattern (:<),
    pattern (:>),
  )
import qualified Data.Sized as S
import qualified Data.Sized.Flipped as Flipped (Flipped (..))
import Data.Type.Equality (gcastWith, (:~:) (..))
import Data.Type.Natural as Algebra.Internal hiding ((%~))
import Data.Type.Natural.Lemma.Arithmetic (plusComm)
import Data.Type.Natural.Lemma.Order (geqToMax, leqToMax, minusPlus, notLeqToLeq)
import Data.Type.Ordinal
import qualified Data.Vector as DV
import qualified Data.Vector.Unboxed as UV
import Proof.Equational (coerce, withRefl)
import Proof.Equational as Algebra.Internal
  ( because,
    coerce,
    start,
    (===),
    (=~=),
  )
import Proof.Propositional as Algebra.Internal
  ( IsTrue (..),
    withWitness,
  )

toProxy :: a -> Proxy a
toProxy :: a -> Proxy a
toProxy a
_ = Proxy a
forall k (t :: k). Proxy t
Proxy

type USized n a = S.Sized UV.Vector n a

type Sized n a = S.Sized DV.Vector n a

type Sized' n a = S.Sized Seq.Seq n a

sNatToSingleton :: SNat n -> Sing n
sNatToSingleton :: SNat n -> Sing n
sNatToSingleton SNat n
sn = SNat n -> (KnownNat n => SNat n) -> SNat n
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n
sn KnownNat n => SNat n
forall k (a :: k). SingI a => Sing a
sing

singToSNat :: Sing n -> SNat n
singToSNat :: Sing n -> SNat n
singToSNat Sing n
sn = Sing n -> (KnownNat n => SNat n) -> SNat n
forall (n :: Nat) r. Sing n -> (KnownNat n => r) -> r
Sing.withKnownNat Sing n
sn KnownNat n => SNat n
forall (n :: Nat). KnownNat n => SNat n
sNat

coerceLength :: n :~: m -> S.Sized f n a -> S.Sized f m a
{-# ANN coerceLength "HLint: ignore Avoid lambda" #-}
{-# ANN coerceLength "HLint: ignore Redundant lambda" #-}
coerceLength :: (n :~: m) -> Sized f n a -> Sized f m a
coerceLength = \n :~: m
eql Sized f n a
x -> (n :~: m) -> ((n ~ m) => Sized f m a) -> Sized f m a
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith n :~: m
eql Sized f n a
(n ~ m) => Sized f m a
x

sizedLength :: (KnownNat n, S.DomC f a) => S.Sized f n a -> SNat n
sizedLength :: Sized f n a -> SNat n
sizedLength = Sized f n a -> SNat n
forall (f :: Type -> Type) (n :: Nat) a.
(Dom f a, KnownNat n) =>
Sized f n a -> SNat n
S.sLength

padVecs ::
  forall a n m.
  (Unbox a, KnownNat n, KnownNat m) =>
  a ->
  USized n a ->
  USized m a ->
  (SNat (Max n m), USized (Max n m) a, USized (Max n m) a)
padVecs :: a
-> USized n a
-> USized m a
-> (SNat (Max n m), USized (Max n m) a, USized (Max n m) a)
padVecs a
d USized n a
xs USized m a
ys =
  let (SNat n
n, SNat m
m) = (USized n a -> SNat n
forall (f :: Type -> Type) (n :: Nat) a.
(Dom f a, KnownNat n) =>
Sized f n a -> SNat n
S.sLength USized n a
xs, USized m a -> SNat m
forall (f :: Type -> Type) (n :: Nat) a.
(Dom f a, KnownNat n) =>
Sized f n a -> SNat n
S.sLength USized m a
ys)
      l :: SNat (Max n m)
l = SNat n -> SNat m -> SNat (Max n m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Max n m)
sMax SNat n
n SNat m
m
   in case SNat n
n SNat n -> SNat m -> SBool (n <=? m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n <=? m)
%<=? SNat m
m of
        SBool (n <=? m)
STrue ->
          let maxISm :: Max n m :~: m
maxISm = SNat n -> SNat m -> IsTrue (n <=? m) -> Max n m :~: m
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? m) -> Max n m :~: m
leqToMax SNat n
n SNat m
m IsTrue (n <=? m)
IsTrue 'True
Witness
              k :: SNat (m - n)
k = SNat m
m SNat m -> SNat n -> SNat (m - n)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m)
%- SNat n
n
              nPLUSk :: (n + (m - n)) :~: m
nPLUSk =
                SNat (n + (m - n)) -> (n + (m - n)) :~: (n + (m - n))
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat n
n SNat n -> SNat (m - n) -> SNat (n + (m - n))
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ (SNat m
m SNat m -> SNat n -> SNat (m - n)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m)
%- SNat n
n))
                  ((n + (m - n)) :~: (n + (m - n)))
-> Reason (:~:) (n + (m - n)) ((m - n) + n)
-> (n + (m - n)) :~: ((m - n) + n)
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat m
m SNat m -> SNat n -> SNat (m - n)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m)
%- SNat n
n SNat (m - n) -> SNat n -> SNat ((m - n) + n)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat n
n SNat ((m - n) + n)
-> ((n + (m - n)) :~: ((m - n) + n))
-> Reason (:~:) (n + (m - n)) ((m - n) + n)
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
       (eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat n -> SNat (m - n) -> (n + (m - n)) :~: ((m - n) + n)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n + m) :~: (m + n)
plusComm SNat n
n (SNat m
m SNat m -> SNat n -> SNat (m - n)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m)
%- SNat n
n)
                  ((n + (m - n)) :~: ((m - n) + n))
-> Reason (:~:) ((m - n) + n) m -> (n + (m - n)) :~: m
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat m
m SNat m -> (((m - n) + n) :~: m) -> Reason (:~:) ((m - n) + n) m
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
       (eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat m -> SNat n -> IsTrue (n <=? m) -> ((m - n) + n) :~: m
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (m <=? n) -> ((n - m) + m) :~: n
minusPlus SNat m
m SNat n
n IsTrue (n <=? m)
IsTrue 'True
Witness
                  ((n + (m - n)) :~: m) -> Reason (:~:) m m -> (n + (m - n)) :~: m
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat n -> SNat m -> SNat (Max n m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Max n m)
sMax SNat n
n SNat m
m SNat m -> (m :~: m) -> Reason (:~:) m m
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
       (eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` m :~: m
Max n m :~: m
maxISm
           in ( SNat (Max n m)
l
              , ((n + (m - n)) :~: m) -> Sized Vector (n + (m - n)) a -> USized m a
forall (n :: Nat) (m :: Nat) (f :: Type -> Type) a.
(n :~: m) -> Sized f n a -> Sized f m a
coerceLength (n + (m - n)) :~: m
nPLUSk (USized n a
xs USized n a
-> Sized Vector (m - n) a -> Sized Vector (n + (m - n)) a
forall (f :: Type -> Type) (n :: Nat) (m :: Nat) a.
(CFreeMonoid f, Dom f a) =>
Sized f n a -> Sized f m a -> Sized f (n + m) a
S.++ SNat (m - n) -> a -> Sized Vector (m - n) a
forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> a -> Sized f n a
S.replicate SNat (m - n)
k a
d)
              , (m :~: m) -> USized m a -> USized m a
forall (n :: Nat) (m :: Nat) (f :: Type -> Type) a.
(n :~: m) -> Sized f n a -> Sized f m a
coerceLength m :~: m
Max n m :~: m
maxISm USized m a
ys
              )
        SBool (n <=? m)
SFalse ->
          IsTrue (m <=? n)
-> (((m <=? n) ~ 'True) =>
    (SNat (Max n m), USized (Max n m) a, USized (Max n m) a))
-> (SNat (Max n m), USized (Max n m) a, USized (Max n m) a)
forall (b :: Bool) r. IsTrue b -> ((b ~ 'True) => r) -> r
withWitness (SNat n -> SNat m -> IsTrue (m <=? n)
forall (n :: Nat) (m :: Nat).
((n <=? m) ~ 'False) =>
SNat n -> SNat m -> IsTrue (m <=? n)
notLeqToLeq SNat n
n SNat m
m) ((((m <=? n) ~ 'True) =>
  (SNat (Max n m), USized (Max n m) a, USized (Max n m) a))
 -> (SNat (Max n m), USized (Max n m) a, USized (Max n m) a))
-> (((m <=? n) ~ 'True) =>
    (SNat (Max n m), USized (Max n m) a, USized (Max n m) a))
-> (SNat (Max n m), USized (Max n m) a, USized (Max n m) a)
forall a b. (a -> b) -> a -> b
$
            let maxISn :: Max n m :~: n
maxISn = SNat n -> SNat m -> IsTrue (m <=? n) -> Max n m :~: n
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (m <=? n) -> Max n m :~: n
geqToMax SNat n
n SNat m
m IsTrue (m <=? n)
IsTrue 'True
Witness
                mPLUSk :: m + (n - m) :~: Max n m
                mPLUSk :: (m + (n - m)) :~: Max n m
mPLUSk =
                  SNat (m + (n - m)) -> (m + (n - m)) :~: (m + (n - m))
forall k (eq :: k -> k -> Type) (proxy :: k -> Type) (a :: k).
Preorder eq =>
proxy a -> eq a a
start (SNat m
m SNat m -> SNat (n - m) -> SNat (m + (n - m))
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ (SNat n
n SNat n -> SNat m -> SNat (n - m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m)
%- SNat m
m))
                    ((m + (n - m)) :~: (m + (n - m)))
-> Reason (:~:) (m + (n - m)) ((n - m) + m)
-> (m + (n - m)) :~: ((n - m) + m)
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat n
n SNat n -> SNat m -> SNat (n - m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m)
%- SNat m
m SNat (n - m) -> SNat m -> SNat ((n - m) + m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
m SNat ((n - m) + m)
-> ((m + (n - m)) :~: ((n - m) + m))
-> Reason (:~:) (m + (n - m)) ((n - m) + m)
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
       (eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat m -> SNat (n - m) -> (m + (n - m)) :~: ((n - m) + m)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n + m) :~: (m + n)
plusComm SNat m
m (SNat n
n SNat n -> SNat m -> SNat (n - m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m)
%- SNat m
m)
                    ((m + (n - m)) :~: ((n - m) + m))
-> Reason (:~:) ((n - m) + m) n -> (m + (n - m)) :~: n
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat n
n SNat n -> (((n - m) + m) :~: n) -> Reason (:~:) ((n - m) + m) n
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
       (eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` SNat n -> SNat m -> IsTrue (m <=? n) -> ((n - m) + m) :~: n
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (m <=? n) -> ((n - m) + m) :~: n
minusPlus SNat n
n SNat m
m IsTrue (m <=? n)
IsTrue 'True
Witness
                    ((m + (n - m)) :~: n) -> Reason (:~:) n n -> (m + (n - m)) :~: n
forall k (eq :: k -> k -> Type) (x :: k) (y :: k) (z :: k).
Equality eq =>
eq x y -> Reason eq y z -> eq x z
=== SNat n -> SNat m -> SNat (Max n m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Max n m)
sMax SNat n
n SNat m
m SNat n -> (n :~: n) -> Reason (:~:) n n
forall k1 k2 (proxy :: k1 -> Type) (y :: k1)
       (eq :: k2 -> k1 -> Type) (x :: k2).
proxy y -> eq x y -> Reason eq x y
`because` n :~: n
Max n m :~: n
maxISn
             in ( SNat n
SNat (Max n m)
l
                , (n :~: n) -> USized n a -> USized n a
forall (n :: Nat) (m :: Nat) (f :: Type -> Type) a.
(n :~: m) -> Sized f n a -> Sized f m a
coerceLength n :~: n
Max n m :~: n
maxISn USized n a
xs
                , ((m + (n - m)) :~: n) -> Sized Vector (m + (n - m)) a -> USized n a
forall (n :: Nat) (m :: Nat) (f :: Type -> Type) a.
(n :~: m) -> Sized f n a -> Sized f m a
coerceLength (m + (n - m)) :~: n
(m + (n - m)) :~: Max n m
mPLUSk (Sized Vector (m + (n - m)) a -> USized n a)
-> Sized Vector (m + (n - m)) a -> USized n a
forall a b. (a -> b) -> a -> b
$ USized m a
ys USized m a
-> Sized Vector (n - m) a -> Sized Vector (m + (n - m)) a
forall (f :: Type -> Type) (n :: Nat) (m :: Nat) a.
(CFreeMonoid f, Dom f a) =>
Sized f n a -> Sized f m a -> Sized f (n + m) a
S.++ SNat (n - m) -> a -> Sized Vector (n - m) a
forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> a -> Sized f n a
S.replicate (SNat n
n SNat n -> SNat m -> SNat (n - m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m)
%- SNat m
m) a
d
                )

type family Flipped f a :: Nat -> Type where
  Flipped f a = Flipped.Flipped f a

pattern Flipped :: S.Sized f n a -> Flipped f a n
pattern $bFlipped :: Sized f n a -> Flipped f a n
$mFlipped :: forall r (f :: Type -> Type) (n :: Nat) a.
Flipped f a n -> (Sized f n a -> r) -> (Void# -> r) -> r
Flipped xs = Flipped.Flipped xs

sNatToInt :: SNat n -> Int
sNatToInt :: SNat n -> Int
sNatToInt = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> (SNat n -> Natural) -> SNat n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SNat n -> Natural
forall (n :: Nat). SNat n -> Natural
toNatural

#if !MIN_VERSION_hashable(1,3,4)
instance Hashable a => Hashable (Seq.Seq a) where
  hashWithSalt :: Int -> Seq a -> Int
hashWithSalt Int
d = Int -> [a] -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
d ([a] -> Int) -> (Seq a -> [a]) -> Seq a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Seq a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
F.toList
#endif