{-# language BangPatterns #-}
{-# language BlockArguments #-}
{-# language DataKinds #-}
{-# language ExplicitNamespaces #-}
{-# language GADTs #-}
{-# language KindSignatures #-}
{-# language MagicHash #-}
{-# language PatternSynonyms #-}
{-# language UnliftedNewtypes #-}
{-# language RankNTypes #-}
{-# language ScopedTypeVariables #-}
{-# language TypeApplications #-}
{-# language TypeOperators #-}
{-# language UnboxedTuples #-}

-- Turn this on when debugging performance.
-- OPTIONS_GHC -ddump-simpl -ddump-to-file -dsuppress-all -ddump-cmm -ddump-asm

module TypeEqVector
  ( equals
  ) where

import Prelude hiding (Bounded,max,min,maximum)

import Type (E,eq)
import Vector (MutableVector(MutableVector),MutableVector#,Vector,Bounded(Bounded),index,write,write#,thaw,read#,unsafeShrinkFreeze,unsafeFreeze)
import GHC.ST (ST(ST),runST)
import Arithmetic.Types (type (<),Fin(Fin),Nat#)
import Arithmetic.Types (type (:=:),type (<=))
import Arithmetic.Types (type (<#),type (<=#))
import Arithmetic.Nat ((<?),(<?#))
import GHC.TypeNats (type (+))
import GHC.Exts (TYPE,State#)
import Data.Unlifted (Bool#,pattern True#,pattern False#)

import qualified GHC.TypeNats as GHC
import qualified Element
import qualified Arithmetic.Lt as Lt
import qualified Arithmetic.Lte as Lte
import qualified Arithmetic.Nat as Nat
import qualified Arithmetic.Fin as Fin
import qualified Vector
import qualified Vector as V

-- | Compare two vectors for equality.
equals :: Nat# n -> Vector n E -> Vector n E -> Bool
equals :: forall (n :: Nat). Nat# n -> Vector n E -> Vector n E -> Bool
equals !Nat# n
n !Vector n E
v0 !Vector n E
v1 = Nat n -> Bool -> (Fin n -> Bool -> Bool) -> Bool
forall a (n :: Nat). Nat n -> a -> (Fin n -> a -> a) -> a
Fin.descend (Nat# n -> Nat n
forall (n :: Nat). Nat# n -> Nat n
Nat.lift Nat# n
n) Bool
True ((Fin n -> Bool -> Bool) -> Bool)
-> (Fin n -> Bool -> Bool) -> Bool
forall a b. (a -> b) -> a -> b
$ \Fin n
fin Bool
acc ->
  E -> E -> Bool
eq (Vector n E -> Fin# n -> E
forall (n :: Nat) (a :: TYPE R). Vector n a -> Fin# n -> a
index Vector n E
v0 (Fin n -> Fin# n
forall (n :: Nat). Fin n -> Fin# n
Fin.unlift Fin n
fin)) (Vector n E -> Fin# n -> E
forall (n :: Nat) (a :: TYPE R). Vector n a -> Fin# n -> a
index Vector n E
v1 (Fin n -> Fin# n
forall (n :: Nat). Fin n -> Fin# n
Fin.unlift Fin n
fin))
  Bool -> Bool -> Bool
&&
  Bool
acc