{-# 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