module Algebra.Internal
( (:~:)(..), withRefl,
module Data.Proxy,
module Algebra.Internal) where
import Algebra.Instances ()
import AlgebraicPrelude
import Control.Lens ((%~), _Unwrapping)
import Data.Proxy
import Data.Singletons.Prelude as Algebra.Internal (PNum (..),
POrd (..),
SNum (..),
SOrd (..),
Sing (SFalse, STrue),
SingI (..),
SingKind (..),
SomeSing (..),
withSingI)
import Data.Singletons.Prelude.Enum as Algebra.Internal (PEnum (..),
SEnum (..))
import Data.Singletons.TypeLits as Algebra.Internal (KnownNat,
withKnownNat)
import Data.Sized.Builtin as Algebra.Internal (pattern (:<),
pattern (:>),
pattern NilL,
pattern NilR,
sIndex,generate,
singleton,
unsafeFromList,
unsafeFromList',
zipWithSame)
import qualified Data.Sized.Builtin as S
import qualified Data.Sized.Flipped as Flipped (Flipped (..))
import Data.Type.Equality ((:~:) (..))
import Data.Type.Natural.Class as Algebra.Internal
import qualified Data.Type.Ordinal as O
import qualified Data.Vector as DV
import GHC.TypeLits as Algebra.Internal
import Proof.Equational (coerce, withRefl)
import Proof.Equational as Algebra.Internal (because,
coerce,
start, (===),
(=~=))
import Proof.Propositional as Algebra.Internal (IsTrue (..),
withWitness)
import qualified Data.Foldable as F
import qualified Data.Sequence as Seq
import Data.Kind (Type)
toProxy :: a -> Proxy a
toProxy _ = Proxy
type Sized n a = S.Sized DV.Vector n a
type Sized' n a = S.Sized Seq.Seq n a
coerceLength :: n :~: m -> S.Sized f n a -> S.Sized f m a
coerceLength eql = _Unwrapping Flipped.Flipped %~ coerce eql
type SNat (n :: Nat) = Sing n
sizedLength f = (S.sLength f)
padVecs :: forall a n m. a -> Sized' n a -> Sized' m a
-> (SNat (Max n m), Sized' (Max n m) a, Sized' (Max n m) a)
padVecs d xs ys
= let (n, m) = (S.sLength xs, S.sLength ys)
l = sMax n m
in case n %:<= m of
STrue ->
let maxISm = leqToMax n m Witness
k = m %:- n
nPLUSk = start (n %:+ (m %:- n))
=== m %:- n %:+ n `because` plusComm n (m %:- n)
=== m `because` minusPlus m n Witness
=== sMax n m `because` maxISm
in (l,
coerceLength nPLUSk (xs S.++ S.replicate k d),
coerceLength maxISm ys)
SFalse -> withWitness (notLeqToLeq n m) $
let maxISn = geqToMax n m Witness
mPLUSk :: m :+ (n :- m) :~: Max n m
mPLUSk = start (m %:+ (n %:- m))
=== n %:- m %:+ m `because` plusComm m (n %:- m)
=== n `because` minusPlus n m Witness
=== sMax n m `because` maxISn
in (l,
coerceLength maxISn xs,
coerceLength mPLUSk $ ys S.++ S.replicate (n %:- m) 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 Flipped xs = Flipped.Flipped xs
pattern OLt :: forall (t :: Nat). ()
=> forall (n1 :: Nat).
((n1 :< t) ~ 'True)
=> Sing n1 -> O.Ordinal t
pattern OLt n = O.OLt n
sNatToInt :: SNat n -> Int
sNatToInt = fromInteger . fromSing
instance Hashable a => Hashable (Seq.Seq a) where
hashWithSalt d = hashWithSalt d . F.toList