{-# LANGUAGE GADTs, DataKinds, ScopedTypeVariables, KindSignatures #-}

module Data.Matrix.Quad where

import Prelude ()
import Data.List (splitAt,intercalate)
import Control.Applicative
import Algebra.RingUtils hiding (O,concat)
import Data.Traversable
import Data.Foldable

data Shape = Bin Shape Shape | Leaf

data Shape' :: Shape -> * where
  Bin' :: !Int -> Shape' s -> Shape' s' -> Shape' (Bin s s')
  Leaf' :: Shape' Leaf

data SomeShape where
  S :: Shape' s -> SomeShape

data Mat :: Shape -> Shape -> * -> * where
  Quad :: !(Mat x1 y1 a) -> !(Mat x2 y1 a) ->
          !(Mat x1 y2 a) -> !(Mat x2 y2 a) ->
          Mat (Bin x1 x2) (Bin y1 y2) a
  Zero :: Mat x y a
  One :: !a -> Mat Leaf Leaf a
  Row :: Mat x1 Leaf a -> Mat x2 Leaf a -> Mat (Bin x1 x2) Leaf a
  Col :: Mat Leaf y1 a -> Mat Leaf y2 a -> Mat Leaf (Bin y1 y2) a

data Vec :: Shape -> * -> * where
  Z :: Vec s a
  O :: a -> Vec Leaf a
  (:!) :: Vec s a -> Vec s' a -> Vec (Bin s s') a


row :: Mat x1 'Leaf a -> Mat x2 'Leaf a -> Mat ('Bin x1 x2) 'Leaf a
row Mat x1 'Leaf a
Zero Mat x2 'Leaf a
Zero = Mat ('Bin x1 x2) 'Leaf a
forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero
row Mat x1 'Leaf a
x Mat x2 'Leaf a
y = Mat x1 'Leaf a -> Mat x2 'Leaf a -> Mat ('Bin x1 x2) 'Leaf a
forall (s :: Shape) a (s' :: Shape).
Mat s 'Leaf a -> Mat s' 'Leaf a -> Mat ('Bin s s') 'Leaf a
Row Mat x1 'Leaf a
x Mat x2 'Leaf a
y

col :: Mat Leaf y1 a -> Mat Leaf y2 a -> Mat Leaf (Bin y1 y2) a
col :: forall (y1 :: Shape) a (y2 :: Shape).
Mat 'Leaf y1 a -> Mat 'Leaf y2 a -> Mat 'Leaf ('Bin y1 y2) a
col Mat 'Leaf y1 a
Zero Mat 'Leaf y2 a
Zero = Mat 'Leaf ('Bin y1 y2) a
forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero
col Mat 'Leaf y1 a
x Mat 'Leaf y2 a
y = Mat 'Leaf y1 a -> Mat 'Leaf y2 a -> Mat 'Leaf ('Bin y1 y2) a
forall (y1 :: Shape) a (y2 :: Shape).
Mat 'Leaf y1 a -> Mat 'Leaf y2 a -> Mat 'Leaf ('Bin y1 y2) a
Col Mat 'Leaf y1 a
x Mat 'Leaf y2 a
y

quad :: Mat x1 y1 a
-> Mat x2 y1 a
-> Mat x1 y2 a
-> Mat x2 y2 a
-> Mat ('Bin x1 x2) ('Bin y1 y2) a
quad Mat x1 y1 a
Zero Mat x2 y1 a
Zero Mat x1 y2 a
Zero Mat x2 y2 a
Zero = Mat ('Bin x1 x2) ('Bin y1 y2) a
forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero
quad Mat x1 y1 a
a Mat x2 y1 a
b Mat x1 y2 a
c Mat x2 y2 a
d = Mat x1 y1 a
-> Mat x2 y1 a
-> Mat x1 y2 a
-> Mat x2 y2 a
-> Mat ('Bin x1 x2) ('Bin y1 y2) a
forall (s :: Shape) (s' :: Shape) a (x2 :: Shape) (y2 :: Shape).
Mat s s' a
-> Mat x2 s' a
-> Mat s y2 a
-> Mat x2 y2 a
-> Mat ('Bin s x2) ('Bin s' y2) a
Quad Mat x1 y1 a
a Mat x2 y1 a
b Mat x1 y2 a
c Mat x2 y2 a
d

one :: AbelianGroupZ a => a -> Mat Leaf Leaf a
one :: forall a. AbelianGroupZ a => a -> Mat 'Leaf 'Leaf a
one a
x | a -> Bool
forall a. AbelianGroupZ a => a -> Bool
isZero a
x = Mat 'Leaf 'Leaf a
forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero
      | Bool
otherwise = a -> Mat 'Leaf 'Leaf a
forall a. a -> Mat 'Leaf 'Leaf a
One a
x

(.+.) :: AbelianGroupZ a => Mat x y a -> Mat x y a -> Mat x y a
Mat x y a
Zero .+. :: forall a (x :: Shape) (y :: Shape).
AbelianGroupZ a =>
Mat x y a -> Mat x y a -> Mat x y a
.+. Mat x y a
x = Mat x y a
x
Mat x y a
x .+. Mat x y a
Zero = Mat x y a
x
Quad Mat x1 y1 a
a Mat x2 y1 a
b Mat x1 y2 a
c Mat x2 y2 a
d .+. Quad Mat x1 y1 a
a' Mat x2 y1 a
b' Mat x1 y2 a
c' Mat x2 y2 a
d' = Mat x1 y1 a
-> Mat x2 y1 a
-> Mat x1 y2 a
-> Mat x2 y2 a
-> Mat ('Bin x1 x2) ('Bin y1 y2) a
forall (s :: Shape) (s' :: Shape) a (x2 :: Shape) (y2 :: Shape).
Mat s s' a
-> Mat x2 s' a
-> Mat s y2 a
-> Mat x2 y2 a
-> Mat ('Bin s x2) ('Bin s' y2) a
quad (Mat x1 y1 a
a Mat x1 y1 a -> Mat x1 y1 a -> Mat x1 y1 a
forall a (x :: Shape) (y :: Shape).
AbelianGroupZ a =>
Mat x y a -> Mat x y a -> Mat x y a
.+. Mat x1 y1 a
Mat x1 y1 a
a') (Mat x2 y1 a
b Mat x2 y1 a -> Mat x2 y1 a -> Mat x2 y1 a
forall a (x :: Shape) (y :: Shape).
AbelianGroupZ a =>
Mat x y a -> Mat x y a -> Mat x y a
.+. Mat x2 y1 a
Mat x2 y1 a
b') (Mat x1 y2 a
c Mat x1 y2 a -> Mat x1 y2 a -> Mat x1 y2 a
forall a (x :: Shape) (y :: Shape).
AbelianGroupZ a =>
Mat x y a -> Mat x y a -> Mat x y a
.+. Mat x1 y2 a
Mat x1 y2 a
c') (Mat x2 y2 a
d Mat x2 y2 a -> Mat x2 y2 a -> Mat x2 y2 a
forall a (x :: Shape) (y :: Shape).
AbelianGroupZ a =>
Mat x y a -> Mat x y a -> Mat x y a
.+. Mat x2 y2 a
Mat x2 y2 a
d')
One a
x .+. One a
x' = a -> Mat 'Leaf 'Leaf a
forall a. AbelianGroupZ a => a -> Mat 'Leaf 'Leaf a
one (a
x a -> a -> a
forall a. AbelianGroup a => a -> a -> a
+ a
x')
Row Mat x1 'Leaf a
x Mat x2 'Leaf a
y .+. Row Mat x1 'Leaf a
x' Mat x2 'Leaf a
y' = Mat x1 'Leaf a -> Mat x2 'Leaf a -> Mat ('Bin x1 x2) 'Leaf a
forall (s :: Shape) a (s' :: Shape).
Mat s 'Leaf a -> Mat s' 'Leaf a -> Mat ('Bin s s') 'Leaf a
row (Mat x1 'Leaf a
x Mat x1 'Leaf a -> Mat x1 'Leaf a -> Mat x1 'Leaf a
forall a (x :: Shape) (y :: Shape).
AbelianGroupZ a =>
Mat x y a -> Mat x y a -> Mat x y a
.+. Mat x1 'Leaf a
Mat x1 'Leaf a
x') (Mat x2 'Leaf a
y Mat x2 'Leaf a -> Mat x2 'Leaf a -> Mat x2 'Leaf a
forall a (x :: Shape) (y :: Shape).
AbelianGroupZ a =>
Mat x y a -> Mat x y a -> Mat x y a
.+. Mat x2 'Leaf a
Mat x2 'Leaf a
y')
Col Mat 'Leaf y1 a
x Mat 'Leaf y2 a
y .+. Col Mat 'Leaf y1 a
x' Mat 'Leaf y2 a
y' = Mat 'Leaf y1 a -> Mat 'Leaf y2 a -> Mat 'Leaf ('Bin y1 y2) a
forall (y1 :: Shape) a (y2 :: Shape).
Mat 'Leaf y1 a -> Mat 'Leaf y2 a -> Mat 'Leaf ('Bin y1 y2) a
col (Mat 'Leaf y1 a
x Mat 'Leaf y1 a -> Mat 'Leaf y1 a -> Mat 'Leaf y1 a
forall a (x :: Shape) (y :: Shape).
AbelianGroupZ a =>
Mat x y a -> Mat x y a -> Mat x y a
.+. Mat 'Leaf y1 a
Mat 'Leaf y1 a
x') (Mat 'Leaf y2 a
y Mat 'Leaf y2 a -> Mat 'Leaf y2 a -> Mat 'Leaf y2 a
forall a (x :: Shape) (y :: Shape).
AbelianGroupZ a =>
Mat x y a -> Mat x y a -> Mat x y a
.+. Mat 'Leaf y2 a
Mat 'Leaf y2 a
y')

instance AbelianGroupZ a => AbelianGroup (Mat x y a) where
  + :: Mat x y a -> Mat x y a -> Mat x y a
(+) = Mat x y a -> Mat x y a -> Mat x y a
forall a (x :: Shape) (y :: Shape).
AbelianGroupZ a =>
Mat x y a -> Mat x y a -> Mat x y a
(.+.)
  zero :: Mat x y a
zero = Mat x y a
forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero

mult :: RingP a => Bool -> Mat x y a -> Mat z x a -> Mat z y (Pair a)
mult :: forall a (x :: Shape) (y :: Shape) (z :: Shape).
RingP a =>
Bool -> Mat x y a -> Mat z x a -> Mat z y (Pair a)
mult Bool
p Mat x y a
a Mat z x a
b = Mat x y a
a Mat x y a -> Mat z x a -> Mat z y (Pair a)
forall a (x :: Shape) (y :: Shape) (z :: Shape).
RingP a =>
Mat x y a -> Mat z x a -> Mat z y (Pair a)
& Mat z x a
b where
  infixl 7  &
  (&) :: RingP a => Mat x y a -> Mat z x a -> Mat z y (Pair a)
  Mat x y a
Zero & :: forall a (x :: Shape) (y :: Shape) (z :: Shape).
RingP a =>
Mat x y a -> Mat z x a -> Mat z y (Pair a)
& Mat z x a
x = Mat z y (Pair a)
forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero
  Mat x y a
x & Mat z x a
Zero = Mat z y (Pair a)
forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero
  One a
x & One a
x' = Pair a -> Mat 'Leaf 'Leaf (Pair a)
forall a. AbelianGroupZ a => a -> Mat 'Leaf 'Leaf a
one (Bool -> a -> a -> Pair a
forall a. RingP a => Bool -> a -> a -> Pair a
mul Bool
p a
x a
x')
  One a
x & Row Mat x1 'Leaf a
a Mat x2 'Leaf a
b = Mat x1 'Leaf (Pair a)
-> Mat x2 'Leaf (Pair a) -> Mat ('Bin x1 x2) 'Leaf (Pair a)
forall (s :: Shape) a (s' :: Shape).
Mat s 'Leaf a -> Mat s' 'Leaf a -> Mat ('Bin s s') 'Leaf a
row (a -> Mat 'Leaf 'Leaf a
forall a. a -> Mat 'Leaf 'Leaf a
One a
x Mat 'Leaf 'Leaf a -> Mat x1 'Leaf a -> Mat x1 'Leaf (Pair a)
forall a (x :: Shape) (y :: Shape) (z :: Shape).
RingP a =>
Mat x y a -> Mat z x a -> Mat z y (Pair a)
& Mat x1 'Leaf a
a) (a -> Mat 'Leaf 'Leaf a
forall a. a -> Mat 'Leaf 'Leaf a
One a
x Mat 'Leaf 'Leaf a -> Mat x2 'Leaf a -> Mat x2 'Leaf (Pair a)
forall a (x :: Shape) (y :: Shape) (z :: Shape).
RingP a =>
Mat x y a -> Mat z x a -> Mat z y (Pair a)
& Mat x2 'Leaf a
b)
  Col Mat 'Leaf y1 a
a Mat 'Leaf y2 a
b & One a
x = Mat 'Leaf y1 (Pair a)
-> Mat 'Leaf y2 (Pair a) -> Mat 'Leaf ('Bin y1 y2) (Pair a)
forall (y1 :: Shape) a (y2 :: Shape).
Mat 'Leaf y1 a -> Mat 'Leaf y2 a -> Mat 'Leaf ('Bin y1 y2) a
col (Mat 'Leaf y1 a
a Mat 'Leaf y1 a -> Mat 'Leaf 'Leaf a -> Mat 'Leaf y1 (Pair a)
forall a (x :: Shape) (y :: Shape) (z :: Shape).
RingP a =>
Mat x y a -> Mat z x a -> Mat z y (Pair a)
& a -> Mat 'Leaf 'Leaf a
forall a. a -> Mat 'Leaf 'Leaf a
One a
x) (Mat 'Leaf y2 a
b Mat 'Leaf y2 a -> Mat 'Leaf 'Leaf a -> Mat 'Leaf y2 (Pair a)
forall a (x :: Shape) (y :: Shape) (z :: Shape).
RingP a =>
Mat x y a -> Mat z x a -> Mat z y (Pair a)
& a -> Mat 'Leaf 'Leaf a
forall a. a -> Mat 'Leaf 'Leaf a
One a
x)
  Row Mat x1 'Leaf a
a Mat x2 'Leaf a
b & Col Mat 'Leaf y1 a
a' Mat 'Leaf y2 a
b' = Mat x1 y a
Mat x1 'Leaf a
a Mat x1 y a -> Mat z x1 a -> Mat z y (Pair a)
forall a (x :: Shape) (y :: Shape) (z :: Shape).
RingP a =>
Mat x y a -> Mat z x a -> Mat z y (Pair a)
& Mat z x1 a
Mat 'Leaf y1 a
a' Mat z y (Pair a) -> Mat z y (Pair a) -> Mat z y (Pair a)
forall a. AbelianGroup a => a -> a -> a
+ Mat x2 y a
Mat x2 'Leaf a
b Mat x2 y a -> Mat z x2 a -> Mat z y (Pair a)
forall a (x :: Shape) (y :: Shape) (z :: Shape).
RingP a =>
Mat x y a -> Mat z x a -> Mat z y (Pair a)
& Mat z x2 a
Mat 'Leaf y2 a
b'
  Col Mat 'Leaf y1 a
a Mat 'Leaf y2 a
b & Row Mat x1 'Leaf a
a' Mat x2 'Leaf a
b' = Mat x1 y1 (Pair a)
-> Mat x2 y1 (Pair a)
-> Mat x1 y2 (Pair a)
-> Mat x2 y2 (Pair a)
-> Mat ('Bin x1 x2) ('Bin y1 y2) (Pair a)
forall (s :: Shape) (s' :: Shape) a (x2 :: Shape) (y2 :: Shape).
Mat s s' a
-> Mat x2 s' a
-> Mat s y2 a
-> Mat x2 y2 a
-> Mat ('Bin s x2) ('Bin s' y2) a
quad (Mat 'Leaf y1 a
a Mat 'Leaf y1 a -> Mat x1 'Leaf a -> Mat x1 y1 (Pair a)
forall a (x :: Shape) (y :: Shape) (z :: Shape).
RingP a =>
Mat x y a -> Mat z x a -> Mat z y (Pair a)
& Mat x1 'Leaf a
a') (Mat 'Leaf y1 a
a Mat 'Leaf y1 a -> Mat x2 'Leaf a -> Mat x2 y1 (Pair a)
forall a (x :: Shape) (y :: Shape) (z :: Shape).
RingP a =>
Mat x y a -> Mat z x a -> Mat z y (Pair a)
& Mat x2 'Leaf a
b') (Mat 'Leaf y2 a
b Mat 'Leaf y2 a -> Mat x1 'Leaf a -> Mat x1 y2 (Pair a)
forall a (x :: Shape) (y :: Shape) (z :: Shape).
RingP a =>
Mat x y a -> Mat z x a -> Mat z y (Pair a)
& Mat x1 'Leaf a
a') (Mat 'Leaf y2 a
b Mat 'Leaf y2 a -> Mat x2 'Leaf a -> Mat x2 y2 (Pair a)
forall a (x :: Shape) (y :: Shape) (z :: Shape).
RingP a =>
Mat x y a -> Mat z x a -> Mat z y (Pair a)
& Mat x2 'Leaf a
b')
  Row Mat x1 'Leaf a
a Mat x2 'Leaf a
b & Quad Mat x1 y1 a
a' Mat x2 y1 a
b' Mat x1 y2 a
c' Mat x2 y2 a
d' = Mat x1 'Leaf (Pair a)
-> Mat x2 'Leaf (Pair a) -> Mat ('Bin x1 x2) 'Leaf (Pair a)
forall (s :: Shape) a (s' :: Shape).
Mat s 'Leaf a -> Mat s' 'Leaf a -> Mat ('Bin s s') 'Leaf a
row (Mat x1 'Leaf a
a Mat x1 'Leaf a -> Mat x1 x1 a -> Mat x1 'Leaf (Pair a)
forall a (x :: Shape) (y :: Shape) (z :: Shape).
RingP a =>
Mat x y a -> Mat z x a -> Mat z y (Pair a)
& Mat x1 x1 a
Mat x1 y1 a
a' Mat x1 'Leaf (Pair a)
-> Mat x1 'Leaf (Pair a) -> Mat x1 'Leaf (Pair a)
forall a. AbelianGroup a => a -> a -> a
+ Mat x2 'Leaf a
b Mat x2 'Leaf a -> Mat x1 x2 a -> Mat x1 'Leaf (Pair a)
forall a (x :: Shape) (y :: Shape) (z :: Shape).
RingP a =>
Mat x y a -> Mat z x a -> Mat z y (Pair a)
& Mat x1 x2 a
Mat x1 y2 a
c') (Mat x1 'Leaf a
a Mat x1 'Leaf a -> Mat x2 x1 a -> Mat x2 'Leaf (Pair a)
forall a (x :: Shape) (y :: Shape) (z :: Shape).
RingP a =>
Mat x y a -> Mat z x a -> Mat z y (Pair a)
& Mat x2 x1 a
Mat x2 y1 a
b' Mat x2 'Leaf (Pair a)
-> Mat x2 'Leaf (Pair a) -> Mat x2 'Leaf (Pair a)
forall a. AbelianGroup a => a -> a -> a
+ Mat x2 'Leaf a
b Mat x2 'Leaf a -> Mat x2 x2 a -> Mat x2 'Leaf (Pair a)
forall a (x :: Shape) (y :: Shape) (z :: Shape).
RingP a =>
Mat x y a -> Mat z x a -> Mat z y (Pair a)
& Mat x2 x2 a
Mat x2 y2 a
d')
  Quad Mat x1 y1 a
a Mat x2 y1 a
b Mat x1 y2 a
c Mat x2 y2 a
d & Col Mat 'Leaf y1 a
a' Mat 'Leaf y2 a
c' = Mat 'Leaf y1 (Pair a)
-> Mat 'Leaf y2 (Pair a) -> Mat 'Leaf ('Bin y1 y2) (Pair a)
forall (y1 :: Shape) a (y2 :: Shape).
Mat 'Leaf y1 a -> Mat 'Leaf y2 a -> Mat 'Leaf ('Bin y1 y2) a
col (Mat x1 y1 a
a Mat x1 y1 a -> Mat 'Leaf x1 a -> Mat 'Leaf y1 (Pair a)
forall a (x :: Shape) (y :: Shape) (z :: Shape).
RingP a =>
Mat x y a -> Mat z x a -> Mat z y (Pair a)
& Mat 'Leaf x1 a
Mat 'Leaf y1 a
a' Mat 'Leaf y1 (Pair a)
-> Mat 'Leaf y1 (Pair a) -> Mat 'Leaf y1 (Pair a)
forall a. AbelianGroup a => a -> a -> a
+ Mat x2 y1 a
b Mat x2 y1 a -> Mat 'Leaf x2 a -> Mat 'Leaf y1 (Pair a)
forall a (x :: Shape) (y :: Shape) (z :: Shape).
RingP a =>
Mat x y a -> Mat z x a -> Mat z y (Pair a)
& Mat 'Leaf x2 a
Mat 'Leaf y2 a
c') (Mat x1 y2 a
c Mat x1 y2 a -> Mat 'Leaf x1 a -> Mat 'Leaf y2 (Pair a)
forall a (x :: Shape) (y :: Shape) (z :: Shape).
RingP a =>
Mat x y a -> Mat z x a -> Mat z y (Pair a)
& Mat 'Leaf x1 a
Mat 'Leaf y1 a
a' Mat 'Leaf y2 (Pair a)
-> Mat 'Leaf y2 (Pair a) -> Mat 'Leaf y2 (Pair a)
forall a. AbelianGroup a => a -> a -> a
+ Mat x2 y2 a
d Mat x2 y2 a -> Mat 'Leaf x2 a -> Mat 'Leaf y2 (Pair a)
forall a (x :: Shape) (y :: Shape) (z :: Shape).
RingP a =>
Mat x y a -> Mat z x a -> Mat z y (Pair a)
& Mat 'Leaf x2 a
Mat 'Leaf y2 a
c')
  Quad Mat x1 y1 a
a Mat x2 y1 a
b Mat x1 y2 a
c Mat x2 y2 a
d & Quad Mat x1 y1 a
a' Mat x2 y1 a
b' Mat x1 y2 a
c' Mat x2 y2 a
d' =
     Mat x1 y1 (Pair a)
-> Mat x2 y1 (Pair a)
-> Mat x1 y2 (Pair a)
-> Mat x2 y2 (Pair a)
-> Mat ('Bin x1 x2) ('Bin y1 y2) (Pair a)
forall (s :: Shape) (s' :: Shape) a (x2 :: Shape) (y2 :: Shape).
Mat s s' a
-> Mat x2 s' a
-> Mat s y2 a
-> Mat x2 y2 a
-> Mat ('Bin s x2) ('Bin s' y2) a
quad (Mat x1 y1 a
a Mat x1 y1 a -> Mat x1 x1 a -> Mat x1 y1 (Pair a)
forall a (x :: Shape) (y :: Shape) (z :: Shape).
RingP a =>
Mat x y a -> Mat z x a -> Mat z y (Pair a)
& Mat x1 x1 a
Mat x1 y1 a
a' Mat x1 y1 (Pair a) -> Mat x1 y1 (Pair a) -> Mat x1 y1 (Pair a)
forall a. AbelianGroup a => a -> a -> a
+ Mat x2 y1 a
b Mat x2 y1 a -> Mat x1 x2 a -> Mat x1 y1 (Pair a)
forall a (x :: Shape) (y :: Shape) (z :: Shape).
RingP a =>
Mat x y a -> Mat z x a -> Mat z y (Pair a)
& Mat x1 x2 a
Mat x1 y2 a
c') (Mat x1 y1 a
a Mat x1 y1 a -> Mat x2 x1 a -> Mat x2 y1 (Pair a)
forall a (x :: Shape) (y :: Shape) (z :: Shape).
RingP a =>
Mat x y a -> Mat z x a -> Mat z y (Pair a)
& Mat x2 x1 a
Mat x2 y1 a
b' Mat x2 y1 (Pair a) -> Mat x2 y1 (Pair a) -> Mat x2 y1 (Pair a)
forall a. AbelianGroup a => a -> a -> a
+ Mat x2 y1 a
b Mat x2 y1 a -> Mat x2 x2 a -> Mat x2 y1 (Pair a)
forall a (x :: Shape) (y :: Shape) (z :: Shape).
RingP a =>
Mat x y a -> Mat z x a -> Mat z y (Pair a)
& Mat x2 x2 a
Mat x2 y2 a
d')
          (Mat x1 y2 a
c Mat x1 y2 a -> Mat x1 x1 a -> Mat x1 y2 (Pair a)
forall a (x :: Shape) (y :: Shape) (z :: Shape).
RingP a =>
Mat x y a -> Mat z x a -> Mat z y (Pair a)
& Mat x1 x1 a
Mat x1 y1 a
a' Mat x1 y2 (Pair a) -> Mat x1 y2 (Pair a) -> Mat x1 y2 (Pair a)
forall a. AbelianGroup a => a -> a -> a
+ Mat x2 y2 a
d Mat x2 y2 a -> Mat x1 x2 a -> Mat x1 y2 (Pair a)
forall a (x :: Shape) (y :: Shape) (z :: Shape).
RingP a =>
Mat x y a -> Mat z x a -> Mat z y (Pair a)
& Mat x1 x2 a
Mat x1 y2 a
c') (Mat x1 y2 a
c Mat x1 y2 a -> Mat x2 x1 a -> Mat x2 y2 (Pair a)
forall a (x :: Shape) (y :: Shape) (z :: Shape).
RingP a =>
Mat x y a -> Mat z x a -> Mat z y (Pair a)
& Mat x2 x1 a
Mat x2 y1 a
b' Mat x2 y2 (Pair a) -> Mat x2 y2 (Pair a) -> Mat x2 y2 (Pair a)
forall a. AbelianGroup a => a -> a -> a
+ Mat x2 y2 a
d Mat x2 y2 a -> Mat x2 x2 a -> Mat x2 y2 (Pair a)
forall a (x :: Shape) (y :: Shape) (z :: Shape).
RingP a =>
Mat x y a -> Mat z x a -> Mat z y (Pair a)
& Mat x2 x2 a
Mat x2 y2 a
d')

  Mat x y a
x & Mat z x a
y = [Char] -> Mat z y (Pair a)
forall a. HasCallStack => [Char] -> a
error ([Char] -> Mat z y (Pair a)) -> [Char] -> Mat z y (Pair a)
forall a b. (a -> b) -> a -> b
$ [Char]
"mult:" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"; " [Mat x y a -> [Char]
forall (x :: Shape) (y :: Shape) a. Mat x y a -> [Char]
showR Mat x y a
x,Mat z x a -> [Char]
forall (x :: Shape) (y :: Shape) a. Mat x y a -> [Char]
showR Mat z x a
y]

-- a variant of traverse. The constraint prevents to just use traverse.
trav :: AbelianGroupZ a => Mat y x (Pair a) -> Pair (Mat y x a)
trav :: forall a (y :: Shape) (x :: Shape).
AbelianGroupZ a =>
Mat y x (Pair a) -> Pair (Mat y x a)
trav Mat y x (Pair a)
Zero = Mat y x a -> Pair (Mat y x a)
forall a. a -> Pair a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Mat y x a
forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero
trav (Quad Mat x1 y1 (Pair a)
a Mat x2 y1 (Pair a)
b Mat x1 y2 (Pair a)
c Mat x2 y2 (Pair a)
d) = Mat x1 y1 a
-> Mat x2 y1 a -> Mat x1 y2 a -> Mat x2 y2 a -> Mat y x a
Mat x1 y1 a
-> Mat x2 y1 a
-> Mat x1 y2 a
-> Mat x2 y2 a
-> Mat ('Bin x1 x2) ('Bin y1 y2) a
forall (s :: Shape) (s' :: Shape) a (x2 :: Shape) (y2 :: Shape).
Mat s s' a
-> Mat x2 s' a
-> Mat s y2 a
-> Mat x2 y2 a
-> Mat ('Bin s x2) ('Bin s' y2) a
quad (Mat x1 y1 a
 -> Mat x2 y1 a -> Mat x1 y2 a -> Mat x2 y2 a -> Mat y x a)
-> Pair (Mat x1 y1 a)
-> Pair (Mat x2 y1 a -> Mat x1 y2 a -> Mat x2 y2 a -> Mat y x a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Mat x1 y1 (Pair a) -> Pair (Mat x1 y1 a)
forall a (y :: Shape) (x :: Shape).
AbelianGroupZ a =>
Mat y x (Pair a) -> Pair (Mat y x a)
trav Mat x1 y1 (Pair a)
a Pair (Mat x2 y1 a -> Mat x1 y2 a -> Mat x2 y2 a -> Mat y x a)
-> Pair (Mat x2 y1 a)
-> Pair (Mat x1 y2 a -> Mat x2 y2 a -> Mat y x a)
forall a b. Pair (a -> b) -> Pair a -> Pair b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Mat x2 y1 (Pair a) -> Pair (Mat x2 y1 a)
forall a (y :: Shape) (x :: Shape).
AbelianGroupZ a =>
Mat y x (Pair a) -> Pair (Mat y x a)
trav Mat x2 y1 (Pair a)
b Pair (Mat x1 y2 a -> Mat x2 y2 a -> Mat y x a)
-> Pair (Mat x1 y2 a) -> Pair (Mat x2 y2 a -> Mat y x a)
forall a b. Pair (a -> b) -> Pair a -> Pair b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Mat x1 y2 (Pair a) -> Pair (Mat x1 y2 a)
forall a (y :: Shape) (x :: Shape).
AbelianGroupZ a =>
Mat y x (Pair a) -> Pair (Mat y x a)
trav Mat x1 y2 (Pair a)
c Pair (Mat x2 y2 a -> Mat y x a)
-> Pair (Mat x2 y2 a) -> Pair (Mat y x a)
forall a b. Pair (a -> b) -> Pair a -> Pair b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Mat x2 y2 (Pair a) -> Pair (Mat x2 y2 a)
forall a (y :: Shape) (x :: Shape).
AbelianGroupZ a =>
Mat y x (Pair a) -> Pair (Mat y x a)
trav Mat x2 y2 (Pair a)
d
trav (One Pair a
x) = a -> Mat y x a
a -> Mat 'Leaf 'Leaf a
forall a. AbelianGroupZ a => a -> Mat 'Leaf 'Leaf a
one (a -> Mat y x a) -> Pair a -> Pair (Mat y x a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pair a
x
trav (Col Mat 'Leaf y1 (Pair a)
a Mat 'Leaf y2 (Pair a)
b) = Mat 'Leaf y1 a -> Mat 'Leaf y2 a -> Mat y x a
Mat 'Leaf y1 a -> Mat 'Leaf y2 a -> Mat 'Leaf ('Bin y1 y2) a
forall (y1 :: Shape) a (y2 :: Shape).
Mat 'Leaf y1 a -> Mat 'Leaf y2 a -> Mat 'Leaf ('Bin y1 y2) a
col (Mat 'Leaf y1 a -> Mat 'Leaf y2 a -> Mat y x a)
-> Pair (Mat 'Leaf y1 a) -> Pair (Mat 'Leaf y2 a -> Mat y x a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Mat 'Leaf y1 (Pair a) -> Pair (Mat 'Leaf y1 a)
forall a (y :: Shape) (x :: Shape).
AbelianGroupZ a =>
Mat y x (Pair a) -> Pair (Mat y x a)
trav Mat 'Leaf y1 (Pair a)
a Pair (Mat 'Leaf y2 a -> Mat y x a)
-> Pair (Mat 'Leaf y2 a) -> Pair (Mat y x a)
forall a b. Pair (a -> b) -> Pair a -> Pair b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Mat 'Leaf y2 (Pair a) -> Pair (Mat 'Leaf y2 a)
forall a (y :: Shape) (x :: Shape).
AbelianGroupZ a =>
Mat y x (Pair a) -> Pair (Mat y x a)
trav Mat 'Leaf y2 (Pair a)
b
trav (Row Mat x1 'Leaf (Pair a)
a Mat x2 'Leaf (Pair a)
b) = Mat x1 'Leaf a -> Mat x2 'Leaf a -> Mat y x a
Mat x1 'Leaf a -> Mat x2 'Leaf a -> Mat ('Bin x1 x2) 'Leaf a
forall (s :: Shape) a (s' :: Shape).
Mat s 'Leaf a -> Mat s' 'Leaf a -> Mat ('Bin s s') 'Leaf a
row (Mat x1 'Leaf a -> Mat x2 'Leaf a -> Mat y x a)
-> Pair (Mat x1 'Leaf a) -> Pair (Mat x2 'Leaf a -> Mat y x a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Mat x1 'Leaf (Pair a) -> Pair (Mat x1 'Leaf a)
forall a (y :: Shape) (x :: Shape).
AbelianGroupZ a =>
Mat y x (Pair a) -> Pair (Mat y x a)
trav Mat x1 'Leaf (Pair a)
a Pair (Mat x2 'Leaf a -> Mat y x a)
-> Pair (Mat x2 'Leaf a) -> Pair (Mat y x a)
forall a b. Pair (a -> b) -> Pair a -> Pair b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Mat x2 'Leaf (Pair a) -> Pair (Mat x2 'Leaf a)
forall a (y :: Shape) (x :: Shape).
AbelianGroupZ a =>
Mat y x (Pair a) -> Pair (Mat y x a)
trav Mat x2 'Leaf (Pair a)
b

q0 :: Mat (Bin x x') (Bin y y') a
q0 :: forall (x :: Shape) (x' :: Shape) (y :: Shape) (y' :: Shape) a.
Mat ('Bin x x') ('Bin y y') a
q0 = Mat x y a
-> Mat x' y a
-> Mat x y' a
-> Mat x' y' a
-> Mat ('Bin x x') ('Bin y y') a
forall (s :: Shape) (s' :: Shape) a (x2 :: Shape) (y2 :: Shape).
Mat s s' a
-> Mat x2 s' a
-> Mat s y2 a
-> Mat x2 y2 a
-> Mat ('Bin s x2) ('Bin s' y2) a
Quad Mat x y a
forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero Mat x' y a
forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero Mat x y' a
forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero Mat x' y' a
forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero

closeDisjointP :: RingP a => Bool -> Mat x x a -> Mat y x (Pair a) -> Mat y y a -> Pair (Mat y x a)
closeDisjointP :: forall a (x :: Shape) (y :: Shape).
RingP a =>
Bool
-> Mat x x a -> Mat y x (Pair a) -> Mat y y a -> Pair (Mat y x a)
closeDisjointP Bool
p Mat x x a
l Mat y x (Pair a)
c Mat y y a
r = Mat x x a -> Mat y x (Pair a) -> Mat y y a -> Pair (Mat y x a)
forall a (x :: Shape) (y :: Shape).
RingP a =>
Mat x x a -> Mat y x (Pair a) -> Mat y y a -> Pair (Mat y x a)
close Mat x x a
l Mat y x (Pair a)
c Mat y y a
r
  where  close :: RingP a => Mat x x a -> Mat y x (Pair a) -> Mat y y a -> Pair (Mat y x a)
         close :: forall a (x :: Shape) (y :: Shape).
RingP a =>
Mat x x a -> Mat y x (Pair a) -> Mat y y a -> Pair (Mat y x a)
close Mat x x a
l Mat y x (Pair a)
Zero Mat y y a
r = Mat y x a
forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero Mat y x a -> Mat y x a -> Pair (Mat y x a)
forall a. a -> a -> Pair a
:/: Mat y x a
forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero
         close Mat x x a
Zero Mat y x (Pair a)
x Mat y y a
Zero = Mat y x (Pair a) -> Pair (Mat y x a)
forall a (y :: Shape) (x :: Shape).
AbelianGroupZ a =>
Mat y x (Pair a) -> Pair (Mat y x a)
trav Mat y x (Pair a)
x -- if x = One x', we are in this case
         close (Quad Mat x1 y1 a
a11 Mat x2 y1 a
a12 Mat x1 y2 a
Zero Mat x2 y2 a
a22) (Quad Mat x1 y1 (Pair a)
c11 Mat x2 y1 (Pair a)
c12 Mat x1 y2 (Pair a)
c21 Mat x2 y2 (Pair a)
c22) (Quad Mat x1 y1 a
b11 Mat x2 y1 a
b12 Mat x1 y2 a
Zero Mat x2 y2 a
b22) = Mat x1 x1 a
-> Mat x2 x1 a -> Mat x1 x2 a -> Mat x2 x2 a -> Mat y x a
Mat x1 x1 a
-> Mat x2 x1 a
-> Mat x1 x2 a
-> Mat x2 x2 a
-> Mat ('Bin x1 x2) ('Bin x1 x2) a
forall (s :: Shape) (s' :: Shape) a (x2 :: Shape) (y2 :: Shape).
Mat s s' a
-> Mat x2 s' a
-> Mat s y2 a
-> Mat x2 y2 a
-> Mat ('Bin s x2) ('Bin s' y2) a
quad (Mat x1 x1 a
 -> Mat x2 x1 a -> Mat x1 x2 a -> Mat x2 x2 a -> Mat y x a)
-> Pair (Mat x1 x1 a)
-> Pair (Mat x2 x1 a -> Mat x1 x2 a -> Mat x2 x2 a -> Mat y x a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pair (Mat x1 x1 a)
x11 Pair (Mat x2 x1 a -> Mat x1 x2 a -> Mat x2 x2 a -> Mat y x a)
-> Pair (Mat x2 x1 a)
-> Pair (Mat x1 x2 a -> Mat x2 x2 a -> Mat y x a)
forall a b. Pair (a -> b) -> Pair a -> Pair b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Pair (Mat x2 x1 a)
x12 Pair (Mat x1 x2 a -> Mat x2 x2 a -> Mat y x a)
-> Pair (Mat x1 x2 a) -> Pair (Mat x2 x2 a -> Mat y x a)
forall a b. Pair (a -> b) -> Pair a -> Pair b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Pair (Mat x1 x2 a)
x21 Pair (Mat x2 x2 a -> Mat y x a)
-> Pair (Mat x2 x2 a) -> Pair (Mat y x a)
forall a b. Pair (a -> b) -> Pair a -> Pair b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Pair (Mat x2 x2 a)
x22
           where x21 :: Pair (Mat x1 x2 a)
x21 = Mat x2 x2 a
-> Mat x1 x2 (Pair a) -> Mat x1 x1 a -> Pair (Mat x1 x2 a)
forall a (x :: Shape) (y :: Shape).
RingP a =>
Mat x x a -> Mat y x (Pair a) -> Mat y y a -> Pair (Mat y x a)
close Mat x2 x2 a
Mat x2 y2 a
a22 Mat x1 x2 (Pair a)
Mat x1 y2 (Pair a)
c21 Mat x1 x1 a
Mat x1 y1 a
b11
                 x11 :: Pair (Mat x1 x1 a)
x11 = Mat x1 x1 a
-> Mat x1 x1 (Pair a) -> Mat x1 x1 a -> Pair (Mat x1 x1 a)
forall a (x :: Shape) (y :: Shape).
RingP a =>
Mat x x a -> Mat y x (Pair a) -> Mat y y a -> Pair (Mat y x a)
close Mat x1 x1 a
Mat x1 y1 a
a11 (Mat x2 x1 a
Mat x2 y1 a
a12 Mat x2 x1 a -> Mat x1 x2 a -> Mat x1 x1 (Pair a)
forall a (x :: Shape) (y :: Shape) (z :: Shape).
RingP a =>
Mat x y a -> Mat z x a -> Mat z y (Pair a)
& Pair (Mat x1 x2 a) -> Mat x1 x2 a
forall a. Pair a -> a
rightOf Pair (Mat x1 x2 a)
x21 Mat x1 x1 (Pair a) -> Mat x1 x1 (Pair a) -> Mat x1 x1 (Pair a)
forall a. AbelianGroup a => a -> a -> a
+ Mat x1 x1 (Pair a)
Mat x1 y1 (Pair a)
c11) Mat x1 x1 a
Mat x1 y1 a
b11
                 x22 :: Pair (Mat x2 x2 a)
x22 = Mat x2 x2 a
-> Mat x2 x2 (Pair a) -> Mat x2 x2 a -> Pair (Mat x2 x2 a)
forall a (x :: Shape) (y :: Shape).
RingP a =>
Mat x x a -> Mat y x (Pair a) -> Mat y y a -> Pair (Mat y x a)
close Mat x2 x2 a
Mat x2 y2 a
a22 (Pair (Mat x1 x2 a) -> Mat x1 x2 a
forall a. Pair a -> a
leftOf  Pair (Mat x1 x2 a)
x21 Mat x1 x2 a -> Mat x2 x1 a -> Mat x2 x2 (Pair a)
forall a (x :: Shape) (y :: Shape) (z :: Shape).
RingP a =>
Mat x y a -> Mat z x a -> Mat z y (Pair a)
& Mat x2 x1 a
Mat x2 y1 a
b12 Mat x2 x2 (Pair a) -> Mat x2 x2 (Pair a) -> Mat x2 x2 (Pair a)
forall a. AbelianGroup a => a -> a -> a
+ Mat x2 y2 (Pair a)
Mat x2 x2 (Pair a)
c22) Mat x2 x2 a
Mat x2 y2 a
b22
                 x12 :: Pair (Mat x2 x1 a)
x12 = Mat x1 x1 a
-> Mat x2 x1 (Pair a) -> Mat x2 x2 a -> Pair (Mat x2 x1 a)
forall a (x :: Shape) (y :: Shape).
RingP a =>
Mat x x a -> Mat y x (Pair a) -> Mat y y a -> Pair (Mat y x a)
close Mat x1 x1 a
Mat x1 y1 a
a11 (Mat x2 x1 a
Mat x2 y1 a
a12 Mat x2 x1 a -> Mat x2 x2 a -> Mat x2 x1 (Pair a)
forall a (x :: Shape) (y :: Shape) (z :: Shape).
RingP a =>
Mat x y a -> Mat z x a -> Mat z y (Pair a)
& Pair (Mat x2 x2 a) -> Mat x2 x2 a
forall a. Pair a -> a
rightOf Pair (Mat x2 x2 a)
x22 Mat x2 x1 (Pair a) -> Mat x2 x1 (Pair a) -> Mat x2 x1 (Pair a)
forall a. AbelianGroup a => a -> a -> a
+ Pair (Mat x1 x1 a) -> Mat x1 x1 a
forall a. Pair a -> a
leftOf Pair (Mat x1 x1 a)
x11 Mat x1 x1 a -> Mat x2 x1 a -> Mat x2 x1 (Pair a)
forall a (x :: Shape) (y :: Shape) (z :: Shape).
RingP a =>
Mat x y a -> Mat z x a -> Mat z y (Pair a)
& Mat x2 x1 a
Mat x2 y1 a
b12 Mat x2 x1 (Pair a) -> Mat x2 x1 (Pair a) -> Mat x2 x1 (Pair a)
forall a. AbelianGroup a => a -> a -> a
+ Mat x2 y1 (Pair a)
Mat x2 x1 (Pair a)
c12) Mat x2 x2 a
Mat x2 y2 a
b22
         close Mat x x a
Zero (Quad Mat x1 y1 (Pair a)
c11 Mat x2 y1 (Pair a)
c12 Mat x1 y2 (Pair a)
c21 Mat x2 y2 (Pair a)
c22) (Quad Mat x1 y1 a
b11 Mat x2 y1 a
b12 Mat x1 y2 a
Zero Mat x2 y2 a
b22) = Mat x x a -> Mat y x (Pair a) -> Mat y y a -> Pair (Mat y x a)
forall a (x :: Shape) (y :: Shape).
RingP a =>
Mat x x a -> Mat y x (Pair a) -> Mat y y a -> Pair (Mat y x a)
close Mat x x a
Mat ('Bin y1 y2) ('Bin y1 y2) a
forall (x :: Shape) (x' :: Shape) (y :: Shape) (y' :: Shape) a.
Mat ('Bin x x') ('Bin y y') a
q0 (Mat x1 y1 (Pair a)
-> Mat x2 y1 (Pair a)
-> Mat x1 y2 (Pair a)
-> Mat x2 y2 (Pair a)
-> Mat ('Bin x1 x2) ('Bin y1 y2) (Pair a)
forall (s :: Shape) (s' :: Shape) a (x2 :: Shape) (y2 :: Shape).
Mat s s' a
-> Mat x2 s' a
-> Mat s y2 a
-> Mat x2 y2 a
-> Mat ('Bin s x2) ('Bin s' y2) a
Quad Mat x1 y1 (Pair a)
c11 Mat x2 y1 (Pair a)
c12 Mat x1 y2 (Pair a)
c21 Mat x2 y2 (Pair a)
c22) (Mat x1 y1 a
-> Mat x2 y1 a
-> Mat x1 y2 a
-> Mat x2 y2 a
-> Mat ('Bin x1 x2) ('Bin y1 y2) a
forall (s :: Shape) (s' :: Shape) a (x2 :: Shape) (y2 :: Shape).
Mat s s' a
-> Mat x2 s' a
-> Mat s y2 a
-> Mat x2 y2 a
-> Mat ('Bin s x2) ('Bin s' y2) a
Quad Mat x1 y1 a
b11 Mat x2 y1 a
b12 Mat x1 y2 a
forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero Mat x2 y2 a
b22)
         close (Quad Mat x1 y1 a
a11 Mat x2 y1 a
a12 Mat x1 y2 a
Zero Mat x2 y2 a
a22) (Quad Mat x1 y1 (Pair a)
c11 Mat x2 y1 (Pair a)
c12 Mat x1 y2 (Pair a)
c21 Mat x2 y2 (Pair a)
c22) Mat y y a
Zero = Mat x x a -> Mat y x (Pair a) -> Mat y y a -> Pair (Mat y x a)
forall a (x :: Shape) (y :: Shape).
RingP a =>
Mat x x a -> Mat y x (Pair a) -> Mat y y a -> Pair (Mat y x a)
close (Mat x1 y1 a
-> Mat x2 y1 a
-> Mat x1 y2 a
-> Mat x2 y2 a
-> Mat ('Bin x1 x2) ('Bin y1 y2) a
forall (s :: Shape) (s' :: Shape) a (x2 :: Shape) (y2 :: Shape).
Mat s s' a
-> Mat x2 s' a
-> Mat s y2 a
-> Mat x2 y2 a
-> Mat ('Bin s x2) ('Bin s' y2) a
Quad Mat x1 y1 a
a11 Mat x2 y1 a
a12 Mat x1 y2 a
forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero Mat x2 y2 a
a22) (Mat x1 y1 (Pair a)
-> Mat x2 y1 (Pair a)
-> Mat x1 y2 (Pair a)
-> Mat x2 y2 (Pair a)
-> Mat ('Bin x1 x2) ('Bin y1 y2) (Pair a)
forall (s :: Shape) (s' :: Shape) a (x2 :: Shape) (y2 :: Shape).
Mat s s' a
-> Mat x2 s' a
-> Mat s y2 a
-> Mat x2 y2 a
-> Mat ('Bin s x2) ('Bin s' y2) a
Quad Mat x1 y1 (Pair a)
c11 Mat x2 y1 (Pair a)
c12 Mat x1 y2 (Pair a)
c21 Mat x2 y2 (Pair a)
c22) Mat y y a
Mat ('Bin x1 x2) ('Bin x1 x2) a
forall (x :: Shape) (x' :: Shape) (y :: Shape) (y' :: Shape) a.
Mat ('Bin x x') ('Bin y y') a
q0
         close (Quad Mat x1 y1 a
a11 Mat x2 y1 a
a12 Mat x1 y2 a
Zero Mat x2 y2 a
a22) (Col Mat 'Leaf y1 (Pair a)
c1 Mat 'Leaf y2 (Pair a)
c2) (Mat y y a
Zero) = Mat 'Leaf x1 a -> Mat 'Leaf x2 a -> Mat y x a
Mat 'Leaf x1 a -> Mat 'Leaf x2 a -> Mat 'Leaf ('Bin x1 x2) a
forall (y1 :: Shape) a (y2 :: Shape).
Mat 'Leaf y1 a -> Mat 'Leaf y2 a -> Mat 'Leaf ('Bin y1 y2) a
col (Mat 'Leaf x1 a -> Mat 'Leaf x2 a -> Mat y x a)
-> Pair (Mat 'Leaf x1 a) -> Pair (Mat 'Leaf x2 a -> Mat y x a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pair (Mat 'Leaf x1 a)
x1 Pair (Mat 'Leaf x2 a -> Mat y x a)
-> Pair (Mat 'Leaf x2 a) -> Pair (Mat y x a)
forall a b. Pair (a -> b) -> Pair a -> Pair b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Pair (Mat 'Leaf x2 a)
x2
           where x2 :: Pair (Mat 'Leaf x2 a)
x2 = Mat x2 x2 a
-> Mat 'Leaf x2 (Pair a)
-> Mat 'Leaf 'Leaf a
-> Pair (Mat 'Leaf x2 a)
forall a (x :: Shape) (y :: Shape).
RingP a =>
Mat x x a -> Mat y x (Pair a) -> Mat y y a -> Pair (Mat y x a)
close Mat x2 x2 a
Mat x2 y2 a
a22 Mat 'Leaf x2 (Pair a)
Mat 'Leaf y2 (Pair a)
c2 Mat 'Leaf 'Leaf a
forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero
                 x1 :: Pair (Mat 'Leaf x1 a)
x1 = Mat x1 x1 a
-> Mat 'Leaf x1 (Pair a)
-> Mat 'Leaf 'Leaf a
-> Pair (Mat 'Leaf x1 a)
forall a (x :: Shape) (y :: Shape).
RingP a =>
Mat x x a -> Mat y x (Pair a) -> Mat y y a -> Pair (Mat y x a)
close Mat x1 x1 a
Mat x1 y1 a
a11 (Bool -> Mat x2 x1 a -> Mat 'Leaf x2 a -> Mat 'Leaf x1 (Pair a)
forall a (x :: Shape) (y :: Shape) (z :: Shape).
RingP a =>
Bool -> Mat x y a -> Mat z x a -> Mat z y (Pair a)
mult Bool
p Mat x2 x1 a
Mat x2 y1 a
a12 (Pair (Mat 'Leaf x2 a) -> Mat 'Leaf x2 a
forall a. Pair a -> a
rightOf Pair (Mat 'Leaf x2 a)
x2) Mat 'Leaf x1 (Pair a)
-> Mat 'Leaf x1 (Pair a) -> Mat 'Leaf x1 (Pair a)
forall a. AbelianGroup a => a -> a -> a
+ Mat 'Leaf x1 (Pair a)
Mat 'Leaf y1 (Pair a)
c1) Mat 'Leaf 'Leaf a
forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero
         close Mat x x a
Zero (Row Mat x1 'Leaf (Pair a)
c1 Mat x2 'Leaf (Pair a)
c2) (Quad Mat x1 y1 a
b11 Mat x2 y1 a
b12 Mat x1 y2 a
Zero Mat x2 y2 a
b22) = Mat x1 'Leaf a -> Mat x2 'Leaf a -> Mat y x a
Mat x1 'Leaf a -> Mat x2 'Leaf a -> Mat ('Bin x1 x2) 'Leaf a
forall (s :: Shape) a (s' :: Shape).
Mat s 'Leaf a -> Mat s' 'Leaf a -> Mat ('Bin s s') 'Leaf a
row (Mat x1 'Leaf a -> Mat x2 'Leaf a -> Mat y x a)
-> Pair (Mat x1 'Leaf a) -> Pair (Mat x2 'Leaf a -> Mat y x a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pair (Mat x1 'Leaf a)
x1 Pair (Mat x2 'Leaf a -> Mat y x a)
-> Pair (Mat x2 'Leaf a) -> Pair (Mat y x a)
forall a b. Pair (a -> b) -> Pair a -> Pair b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Pair (Mat x2 'Leaf a)
x2
           where x1 :: Pair (Mat x1 'Leaf a)
x1 = Mat 'Leaf 'Leaf a
-> Mat x1 'Leaf (Pair a) -> Mat x1 x1 a -> Pair (Mat x1 'Leaf a)
forall a (x :: Shape) (y :: Shape).
RingP a =>
Mat x x a -> Mat y x (Pair a) -> Mat y y a -> Pair (Mat y x a)
close Mat 'Leaf 'Leaf a
forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero Mat x1 'Leaf (Pair a)
c1 Mat x1 x1 a
Mat x1 y1 a
b11
                 x2 :: Pair (Mat x2 'Leaf a)
x2 = Mat 'Leaf 'Leaf a
-> Mat x2 'Leaf (Pair a) -> Mat x2 x2 a -> Pair (Mat x2 'Leaf a)
forall a (x :: Shape) (y :: Shape).
RingP a =>
Mat x x a -> Mat y x (Pair a) -> Mat y y a -> Pair (Mat y x a)
close Mat 'Leaf 'Leaf a
forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero (Bool -> Mat x1 'Leaf a -> Mat x2 x1 a -> Mat x2 'Leaf (Pair a)
forall a (x :: Shape) (y :: Shape) (z :: Shape).
RingP a =>
Bool -> Mat x y a -> Mat z x a -> Mat z y (Pair a)
mult Bool
p (Pair (Mat x1 'Leaf a) -> Mat x1 'Leaf a
forall a. Pair a -> a
leftOf Pair (Mat x1 'Leaf a)
x1) Mat x2 x1 a
Mat x2 y1 a
b12 Mat x2 'Leaf (Pair a)
-> Mat x2 'Leaf (Pair a) -> Mat x2 'Leaf (Pair a)
forall a. AbelianGroup a => a -> a -> a
+ Mat x2 'Leaf (Pair a)
Mat x2 'Leaf (Pair a)
c2) Mat x2 x2 a
Mat x2 y2 a
b22
         close Mat x x a
a Mat y x (Pair a)
c Mat y y a
b = [Char] -> Pair (Mat y x a)
forall a. HasCallStack => [Char] -> a
error ([Char] -> Pair (Mat y x a)) -> [Char] -> Pair (Mat y x a)
forall a b. (a -> b) -> a -> b
$ [Char]
"closeDisjointP:" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"; " [Mat x x a -> [Char]
forall (x :: Shape) (y :: Shape) a. Mat x y a -> [Char]
showR Mat x x a
a,Mat y x (Pair a) -> [Char]
forall (x :: Shape) (y :: Shape) a. Mat x y a -> [Char]
showR Mat y x (Pair a)
c,Mat y y a -> [Char]
forall (x :: Shape) (y :: Shape) a. Mat x y a -> [Char]
showR Mat y y a
b]
         (&) :: RingP a => Mat x y a -> Mat z x a -> Mat z y (Pair a)
         & :: forall a (x :: Shape) (y :: Shape) (z :: Shape).
RingP a =>
Mat x y a -> Mat z x a -> Mat z y (Pair a)
(&) = Bool -> Mat x y a -> Mat z x a -> Mat z y (Pair a)
forall a (x :: Shape) (y :: Shape) (z :: Shape).
RingP a =>
Bool -> Mat x y a -> Mat z x a -> Mat z y (Pair a)
mult Bool
p

showR :: Mat x y a -> String
showR :: forall (x :: Shape) (y :: Shape) a. Mat x y a -> [Char]
showR Mat x y a
Zero = [Char]
"0"
showR (One a
_) = [Char]
"1"
showR (Row Mat x1 'Leaf a
a Mat x2 'Leaf a
b) = [Char]
"("[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++Mat x1 'Leaf a -> [Char]
forall (x :: Shape) (y :: Shape) a. Mat x y a -> [Char]
showR Mat x1 'Leaf a
a[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++[Char]
"-"[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++Mat x2 'Leaf a -> [Char]
forall (x :: Shape) (y :: Shape) a. Mat x y a -> [Char]
showR Mat x2 'Leaf a
b[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++[Char]
")"
showR (Col Mat 'Leaf y1 a
a Mat 'Leaf y2 a
b) = [Char]
"("[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++Mat 'Leaf y1 a -> [Char]
forall (x :: Shape) (y :: Shape) a. Mat x y a -> [Char]
showR Mat 'Leaf y1 a
a[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++[Char]
"|"[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++Mat 'Leaf y2 a -> [Char]
forall (x :: Shape) (y :: Shape) a. Mat x y a -> [Char]
showR Mat 'Leaf y2 a
b[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++[Char]
")"
showR (Quad Mat x1 y1 a
a Mat x2 y1 a
b Mat x1 y2 a
c Mat x2 y2 a
d) = [Char]
"#("[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"," [Mat x1 y1 a -> [Char]
forall (x :: Shape) (y :: Shape) a. Mat x y a -> [Char]
showR Mat x1 y1 a
a,Mat x2 y1 a -> [Char]
forall (x :: Shape) (y :: Shape) a. Mat x y a -> [Char]
showR Mat x2 y1 a
b,Mat x1 y2 a -> [Char]
forall (x :: Shape) (y :: Shape) a. Mat x y a -> [Char]
showR Mat x1 y2 a
c,Mat x2 y2 a -> [Char]
forall (x :: Shape) (y :: Shape) a. Mat x y a -> [Char]
showR Mat x2 y2 a
d][Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++[Char]
")"

bin' :: Shape' s -> Shape' s' -> Shape' (Bin s s')
bin' :: forall (s :: Shape) (s' :: Shape).
Shape' s -> Shape' s' -> Shape' ('Bin s s')
bin' Shape' s
s Shape' s'
s' = Int -> Shape' s -> Shape' s' -> Shape' ('Bin s s')
forall (s :: Shape) (s' :: Shape).
Int -> Shape' s -> Shape' s' -> Shape' ('Bin s s')
Bin' (Shape' s -> Int
forall (s :: Shape). Shape' s -> Int
sz' Shape' s
s Int -> Int -> Int
forall a. AbelianGroup a => a -> a -> a
+ Shape' s' -> Int
forall (s :: Shape). Shape' s -> Int
sz' Shape' s'
s') Shape' s
s Shape' s'
s'

mkShape :: Int -> SomeShape
mkShape :: Int -> SomeShape
mkShape Int
1 = Shape' ('Bin 'Leaf 'Leaf) -> SomeShape
forall (s :: Shape). Shape' s -> SomeShape
S (Shape' 'Leaf -> Shape' 'Leaf -> Shape' ('Bin 'Leaf 'Leaf)
forall (s :: Shape) (s' :: Shape).
Shape' s -> Shape' s' -> Shape' ('Bin s s')
bin' Shape' 'Leaf
Leaf' Shape' 'Leaf
Leaf')
mkShape Int
2 = Shape' ('Bin ('Bin 'Leaf 'Leaf) 'Leaf) -> SomeShape
forall (s :: Shape). Shape' s -> SomeShape
S (Shape' ('Bin 'Leaf 'Leaf)
-> Shape' 'Leaf -> Shape' ('Bin ('Bin 'Leaf 'Leaf) 'Leaf)
forall (s :: Shape) (s' :: Shape).
Shape' s -> Shape' s' -> Shape' ('Bin s s')
bin' (Shape' 'Leaf -> Shape' 'Leaf -> Shape' ('Bin 'Leaf 'Leaf)
forall (s :: Shape) (s' :: Shape).
Shape' s -> Shape' s' -> Shape' ('Bin s s')
bin' Shape' 'Leaf
Leaf' Shape' 'Leaf
Leaf') Shape' 'Leaf
Leaf')
mkShape Int
n = case (Int -> SomeShape
mkShape Int
n'1, Int -> SomeShape
mkShape Int
n'2) of
  (S Shape' s
x, S Shape' s
y) -> Shape' ('Bin s s) -> SomeShape
forall (s :: Shape). Shape' s -> SomeShape
S (Shape' s -> Shape' s -> Shape' ('Bin s s)
forall (s :: Shape) (s' :: Shape).
Shape' s -> Shape' s' -> Shape' ('Bin s s')
bin' Shape' s
x Shape' s
y)
  where n'1 :: Int
n'1 = Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2
        n'2 :: Int
n'2 = Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n'1 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1

mkSing :: AbelianGroupZ a => Shape' x -> Shape' y -> a -> Mat x y a
mkSing :: forall a (x :: Shape) (y :: Shape).
AbelianGroupZ a =>
Shape' x -> Shape' y -> a -> Mat x y a
mkSing (Bin' Int
_ Shape' s
x1 Shape' s'
x2) (Bin' Int
_ Shape' s
y1 Shape' s'
y2) a
a = Mat s s a
-> Mat s' s a
-> Mat s s' a
-> Mat s' s' a
-> Mat ('Bin s s') ('Bin s s') a
forall (s :: Shape) (s' :: Shape) a (x2 :: Shape) (y2 :: Shape).
Mat s s' a
-> Mat x2 s' a
-> Mat s y2 a
-> Mat x2 y2 a
-> Mat ('Bin s x2) ('Bin s' y2) a
quad Mat s s a
forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero Mat s' s a
forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero (Shape' s -> Shape' s' -> a -> Mat s s' a
forall a (x :: Shape) (y :: Shape).
AbelianGroupZ a =>
Shape' x -> Shape' y -> a -> Mat x y a
mkSing Shape' s
x1 Shape' s'
y2 a
a) Mat s' s' a
forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero
mkSing Shape' x
Leaf' Shape' y
Leaf' a
a = a -> Mat 'Leaf 'Leaf a
forall a. AbelianGroupZ a => a -> Mat 'Leaf 'Leaf a
one a
a
mkSing Shape' x
Leaf' (Bin' Int
_ Shape' s
y1 Shape' s'
y2) a
a = Mat 'Leaf s a -> Mat 'Leaf s' a -> Mat 'Leaf ('Bin s s') a
forall (y1 :: Shape) a (y2 :: Shape).
Mat 'Leaf y1 a -> Mat 'Leaf y2 a -> Mat 'Leaf ('Bin y1 y2) a
col Mat 'Leaf s a
forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero (Shape' 'Leaf -> Shape' s' -> a -> Mat 'Leaf s' a
forall a (x :: Shape) (y :: Shape).
AbelianGroupZ a =>
Shape' x -> Shape' y -> a -> Mat x y a
mkSing Shape' 'Leaf
Leaf' Shape' s'
y2 a
a)
mkSing (Bin' Int
_ Shape' s
x1 Shape' s'
x2) Shape' y
Leaf' a
a = Mat s 'Leaf a -> Mat s' 'Leaf a -> Mat ('Bin s s') 'Leaf a
forall (s :: Shape) a (s' :: Shape).
Mat s 'Leaf a -> Mat s' 'Leaf a -> Mat ('Bin s s') 'Leaf a
row (Shape' s -> Shape' 'Leaf -> a -> Mat s 'Leaf a
forall a (x :: Shape) (y :: Shape).
AbelianGroupZ a =>
Shape' x -> Shape' y -> a -> Mat x y a
mkSing Shape' s
x1 Shape' 'Leaf
Leaf' a
a) Mat s' 'Leaf a
forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero

data SomeTri a where
  T :: Shape' s -> Pair (Mat s s a) -> SomeTri a

type Q a = SomeTri a

mkUpDiag :: AbelianGroupZ a => [a] -> Shape' s -> Mat s s a
mkUpDiag :: forall a (s :: Shape).
AbelianGroupZ a =>
[a] -> Shape' s -> Mat s s a
mkUpDiag [] Shape' s
Leaf' = Mat s s a
forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero
mkUpDiag [a]
xs (Bin' Int
_ Shape' s
s Shape' s'
s') = Mat s s a
-> Mat s' s a
-> Mat s s' a
-> Mat s' s' a
-> Mat ('Bin s s') ('Bin s s') a
forall (s :: Shape) (s' :: Shape) a (x2 :: Shape) (y2 :: Shape).
Mat s s' a
-> Mat x2 s' a
-> Mat s y2 a
-> Mat x2 y2 a
-> Mat ('Bin s x2) ('Bin s' y2) a
Quad ([a] -> Shape' s -> Mat s s a
forall a (s :: Shape).
AbelianGroupZ a =>
[a] -> Shape' s -> Mat s s a
mkUpDiag [a]
a Shape' s
s) (Shape' s' -> Shape' s -> a -> Mat s' s a
forall a (x :: Shape) (y :: Shape).
AbelianGroupZ a =>
Shape' x -> Shape' y -> a -> Mat x y a
mkSing Shape' s'
s' Shape' s
s a
c) Mat s s' a
forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero ([a] -> Shape' s' -> Mat s' s' a
forall a (s :: Shape).
AbelianGroupZ a =>
[a] -> Shape' s -> Mat s s a
mkUpDiag [a]
b Shape' s'
s')
  where ([a]
a,a
c:[a]
b) = Int -> [a] -> ([a], [a])
forall a. Int -> [a] -> ([a], [a])
splitAt (Shape' s -> Int
forall (s :: Shape). Shape' s -> Int
sz' Shape' s
s Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [a]
xs

close :: RingP a => Bool -> Mat s s (Pair a) -> Pair (Mat s s a)
close :: forall a (s :: Shape).
RingP a =>
Bool -> Mat s s (Pair a) -> Pair (Mat s s a)
close Bool
p Mat s s (Pair a)
Zero = Pair (Mat s s a)
forall a. AbelianGroup a => a
zero
close Bool
p (One Pair a
x) = a -> Mat s s a
a -> Mat 'Leaf 'Leaf a
forall a. AbelianGroupZ a => a -> Mat 'Leaf 'Leaf a
one (a -> Mat s s a) -> Pair a -> Pair (Mat s s a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pair a
x
close Bool
p (Quad Mat x1 y1 (Pair a)
a11 Mat x2 y1 (Pair a)
a12 Mat x1 y2 (Pair a)
Zero Mat x2 y2 (Pair a)
a22) = Pair (Mat x1 x1 a)
-> Pair (Mat x2 x1 a)
-> Pair (Mat x1 x2 a)
-> Pair (Mat x2 x2 a)
-> Pair (Mat ('Bin x1 x2) ('Bin x1 x2) a)
forall {f :: * -> *} {x1 :: Shape} {y1 :: Shape} {a} {x2 :: Shape}
       {y2 :: Shape}.
Applicative f =>
f (Mat x1 y1 a)
-> f (Mat x2 y1 a)
-> f (Mat x1 y2 a)
-> f (Mat x2 y2 a)
-> f (Mat ('Bin x1 x2) ('Bin y1 y2) a)
quad' Pair (Mat x1 x1 a)
x11 (Bool
-> Mat x1 x1 a
-> Mat x2 x1 (Pair a)
-> Mat x2 x2 a
-> Pair (Mat x2 x1 a)
forall a (x :: Shape) (y :: Shape).
RingP a =>
Bool
-> Mat x x a -> Mat y x (Pair a) -> Mat y y a -> Pair (Mat y x a)
closeDisjointP Bool
p (Pair (Mat x1 x1 a) -> Mat x1 x1 a
forall a. Pair a -> a
leftOf Pair (Mat x1 x1 a)
x11) Mat x2 x1 (Pair a)
Mat x2 y1 (Pair a)
a12 (Pair (Mat x2 x2 a) -> Mat x2 x2 a
forall a. Pair a -> a
rightOf Pair (Mat x2 x2 a)
x22)) Pair (Mat x1 x2 a)
forall a. AbelianGroup a => a
zero Pair (Mat x2 x2 a)
x22
 where x11 :: Pair (Mat x1 x1 a)
x11 = Bool -> Mat x1 x1 (Pair a) -> Pair (Mat x1 x1 a)
forall a (s :: Shape).
RingP a =>
Bool -> Mat s s (Pair a) -> Pair (Mat s s a)
close (Bool -> Bool
not Bool
p) Mat x1 x1 (Pair a)
Mat x1 y1 (Pair a)
a11
       x22 :: Pair (Mat x2 x2 a)
x22 = Bool -> Mat x2 x2 (Pair a) -> Pair (Mat x2 x2 a)
forall a (s :: Shape).
RingP a =>
Bool -> Mat s s (Pair a) -> Pair (Mat s s a)
close (Bool -> Bool
not Bool
p) Mat x2 x2 (Pair a)
Mat x2 y2 (Pair a)
a22

mkTree :: RingP a => [Pair a] -> SomeTri a
mkTree :: forall a. RingP a => [Pair a] -> SomeTri a
mkTree [Pair a]
xs = case Int -> SomeShape
mkShape ([Pair a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Pair a]
xs) of
  S Shape' s
s -> Shape' s -> Pair (Mat s s a) -> SomeTri a
forall (s :: Shape) a. Shape' s -> Pair (Mat s s a) -> SomeTri a
T Shape' s
s (Bool -> Mat s s (Pair a) -> Pair (Mat s s a)
forall a (s :: Shape).
RingP a =>
Bool -> Mat s s (Pair a) -> Pair (Mat s s a)
close Bool
True (Mat s s (Pair a) -> Pair (Mat s s a))
-> Mat s s (Pair a) -> Pair (Mat s s a)
forall a b. (a -> b) -> a -> b
$ [Pair a] -> Shape' s -> Mat s s (Pair a)
forall a (s :: Shape).
AbelianGroupZ a =>
[a] -> Shape' s -> Mat s s a
mkUpDiag [Pair a]
xs Shape' s
s)

quad' :: f (Mat x1 y1 a)
-> f (Mat x2 y1 a)
-> f (Mat x1 y2 a)
-> f (Mat x2 y2 a)
-> f (Mat ('Bin x1 x2) ('Bin y1 y2) a)
quad' f (Mat x1 y1 a)
a f (Mat x2 y1 a)
b f (Mat x1 y2 a)
c f (Mat x2 y2 a)
d = Mat x1 y1 a
-> Mat x2 y1 a
-> Mat x1 y2 a
-> Mat x2 y2 a
-> Mat ('Bin x1 x2) ('Bin y1 y2) a
forall (s :: Shape) (s' :: Shape) a (x2 :: Shape) (y2 :: Shape).
Mat s s' a
-> Mat x2 s' a
-> Mat s y2 a
-> Mat x2 y2 a
-> Mat ('Bin s x2) ('Bin s' y2) a
quad (Mat x1 y1 a
 -> Mat x2 y1 a
 -> Mat x1 y2 a
 -> Mat x2 y2 a
 -> Mat ('Bin x1 x2) ('Bin y1 y2) a)
-> f (Mat x1 y1 a)
-> f (Mat x2 y1 a
      -> Mat x1 y2 a -> Mat x2 y2 a -> Mat ('Bin x1 x2) ('Bin y1 y2) a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (Mat x1 y1 a)
a f (Mat x2 y1 a
   -> Mat x1 y2 a -> Mat x2 y2 a -> Mat ('Bin x1 x2) ('Bin y1 y2) a)
-> f (Mat x2 y1 a)
-> f (Mat x1 y2 a
      -> Mat x2 y2 a -> Mat ('Bin x1 x2) ('Bin y1 y2) a)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f (Mat x2 y1 a)
b f (Mat x1 y2 a -> Mat x2 y2 a -> Mat ('Bin x1 x2) ('Bin y1 y2) a)
-> f (Mat x1 y2 a)
-> f (Mat x2 y2 a -> Mat ('Bin x1 x2) ('Bin y1 y2) a)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f (Mat x1 y2 a)
c f (Mat x2 y2 a -> Mat ('Bin x1 x2) ('Bin y1 y2) a)
-> f (Mat x2 y2 a) -> f (Mat ('Bin x1 x2) ('Bin y1 y2) a)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f (Mat x2 y2 a)
d

mergein :: RingP a => Bool -> SomeTri a -> Pair a -> SomeTri a -> SomeTri a
mergein :: forall a.
RingP a =>
Bool -> SomeTri a -> Pair a -> SomeTri a -> SomeTri a
mergein Bool
p (T Shape' s
y Pair (Mat s s a)
a) Pair a
c (T Shape' s
x Pair (Mat s s a)
b) = Shape' ('Bin s s)
-> Pair (Mat ('Bin s s) ('Bin s s) a) -> SomeTri a
forall (s :: Shape) a. Shape' s -> Pair (Mat s s a) -> SomeTri a
T (Shape' s -> Shape' s -> Shape' ('Bin s s)
forall (s :: Shape) (s' :: Shape).
Shape' s -> Shape' s' -> Shape' ('Bin s s')
bin' Shape' s
y Shape' s
x) (Pair (Mat s s a)
-> Pair (Mat s s a)
-> Pair (Mat s s a)
-> Pair (Mat s s a)
-> Pair (Mat ('Bin s s) ('Bin s s) a)
forall {f :: * -> *} {x1 :: Shape} {y1 :: Shape} {a} {x2 :: Shape}
       {y2 :: Shape}.
Applicative f =>
f (Mat x1 y1 a)
-> f (Mat x2 y1 a)
-> f (Mat x1 y2 a)
-> f (Mat x2 y2 a)
-> f (Mat ('Bin x1 x2) ('Bin y1 y2) a)
quad' Pair (Mat s s a)
a (Bool
-> Mat s s a -> Mat s s (Pair a) -> Mat s s a -> Pair (Mat s s a)
forall a (x :: Shape) (y :: Shape).
RingP a =>
Bool
-> Mat x x a -> Mat y x (Pair a) -> Mat y y a -> Pair (Mat y x a)
closeDisjointP Bool
p (Pair (Mat s s a) -> Mat s s a
forall a. Pair a -> a
leftOf Pair (Mat s s a)
a) Mat s s (Pair a)
c' (Pair (Mat s s a) -> Mat s s a
forall a. Pair a -> a
rightOf Pair (Mat s s a)
b)) Pair (Mat s s a)
forall a. AbelianGroup a => a
zero Pair (Mat s s a)
b)
  where c' :: Mat s s (Pair a)
c' = Shape' s -> Shape' s -> Pair a -> Mat s s (Pair a)
forall a (x :: Shape) (y :: Shape).
AbelianGroupZ a =>
Shape' x -> Shape' y -> a -> Mat x y a
mkSing Shape' s
x Shape' s
y Pair a
c

-- | A variant of zipWith on vectors
zw :: (AbelianGroup a, AbelianGroup b) => (a -> b -> c) -> Vec y a -> Vec y b -> Vec y c
zw :: forall a b c (y :: Shape).
(AbelianGroup a, AbelianGroup b) =>
(a -> b -> c) -> Vec y a -> Vec y b -> Vec y c
zw a -> b -> c
f Vec y a
Z Vec y b
Z = Vec y c
forall (s :: Shape) a. Vec s a
Z
zw a -> b -> c
f Vec y a
Z (Vec s b
a :! Vec s' b
b) = (a -> b -> c) -> Vec y a -> Vec y b -> Vec y c
forall a b c (y :: Shape).
(AbelianGroup a, AbelianGroup b) =>
(a -> b -> c) -> Vec y a -> Vec y b -> Vec y c
zw a -> b -> c
f (Vec s a
forall (s :: Shape) a. Vec s a
Z Vec s a -> Vec s' a -> Vec ('Bin s s') a
forall (s :: Shape) a (s' :: Shape).
Vec s a -> Vec s' a -> Vec ('Bin s s') a
:! Vec s' a
forall (s :: Shape) a. Vec s a
Z) (Vec s b
a Vec s b -> Vec s' b -> Vec ('Bin s s') b
forall (s :: Shape) a (s' :: Shape).
Vec s a -> Vec s' a -> Vec ('Bin s s') a
:! Vec s' b
b)
zw a -> b -> c
f (Vec s a
a :! Vec s' a
b) Vec y b
Z = (a -> b -> c) -> Vec y a -> Vec y b -> Vec y c
forall a b c (y :: Shape).
(AbelianGroup a, AbelianGroup b) =>
(a -> b -> c) -> Vec y a -> Vec y b -> Vec y c
zw a -> b -> c
f (Vec s a
a Vec s a -> Vec s' a -> Vec ('Bin s s') a
forall (s :: Shape) a (s' :: Shape).
Vec s a -> Vec s' a -> Vec ('Bin s s') a
:! Vec s' a
b) (Vec s b
forall (s :: Shape) a. Vec s a
Z Vec s b -> Vec s' b -> Vec ('Bin s s') b
forall (s :: Shape) a (s' :: Shape).
Vec s a -> Vec s' a -> Vec ('Bin s s') a
:! Vec s' b
forall (s :: Shape) a. Vec s a
Z)
zw a -> b -> c
f Vec y a
Z (O b
x) = c -> Vec 'Leaf c
forall a. a -> Vec 'Leaf a
O (c -> Vec 'Leaf c) -> c -> Vec 'Leaf c
forall a b. (a -> b) -> a -> b
$ a -> b -> c
f a
forall a. AbelianGroup a => a
zero b
x
zw a -> b -> c
f (O a
x) Vec y b
Z = c -> Vec 'Leaf c
forall a. a -> Vec 'Leaf a
O (c -> Vec 'Leaf c) -> c -> Vec 'Leaf c
forall a b. (a -> b) -> a -> b
$ a -> b -> c
f a
x b
forall a. AbelianGroup a => a
zero
zw a -> b -> c
f (O a
x) (O b
y) = c -> Vec 'Leaf c
forall a. a -> Vec 'Leaf a
O (a -> b -> c
f a
x b
y)
zw a -> b -> c
f (Vec s a
a :! Vec s' a
b) (Vec s b
a' :! Vec s' b
b') = (a -> b -> c) -> Vec s a -> Vec s b -> Vec s c
forall a b c (y :: Shape).
(AbelianGroup a, AbelianGroup b) =>
(a -> b -> c) -> Vec y a -> Vec y b -> Vec y c
zw a -> b -> c
f Vec s a
a Vec s b
Vec s b
a' Vec s c -> Vec s' c -> Vec ('Bin s s') c
forall (s :: Shape) a (s' :: Shape).
Vec s a -> Vec s' a -> Vec ('Bin s s') a
:! (a -> b -> c) -> Vec s' a -> Vec s' b -> Vec s' c
forall a b c (y :: Shape).
(AbelianGroup a, AbelianGroup b) =>
(a -> b -> c) -> Vec y a -> Vec y b -> Vec y c
zw a -> b -> c
f Vec s' a
b Vec s' b
Vec s' b
b'

-- | Lookup in a vector
lk :: AbelianGroup a => Int -> Shape' x -> Vec x a -> a
lk :: forall a (x :: Shape).
AbelianGroup a =>
Int -> Shape' x -> Vec x a -> a
lk Int
n Shape' x
_ Vec x a
Z = a
forall a. AbelianGroup a => a
zero
lk Int
0 Shape' x
Leaf' (O a
x) = a
x
lk Int
i (Bin' Int
_ Shape' s
s Shape' s'
s') (Vec s a
x :! Vec s' a
x')
  | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Shape' s -> Int
forall (s :: Shape). Shape' s -> Int
sz' Shape' s
s  = Int -> Shape' s -> Vec s a -> a
forall a (x :: Shape).
AbelianGroup a =>
Int -> Shape' x -> Vec x a -> a
lk Int
i Shape' s
s Vec s a
Vec s a
x
  | Bool
otherwise = Int -> Shape' s' -> Vec s' a -> a
forall a (x :: Shape).
AbelianGroup a =>
Int -> Shape' x -> Vec x a -> a
lk (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Shape' s -> Int
forall (s :: Shape). Shape' s -> Int
sz' Shape' s
s) Shape' s'
s' Vec s' a
Vec s' a
x'

-- | Linearize a matrix
lin' :: AbelianGroup a => Mat x y a -> Vec y (Vec x a)
lin' :: forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Mat x y a -> Vec y (Vec x a)
lin' Mat x y a
Zero = Vec y (Vec x a)
forall (s :: Shape) a. Vec s a
Z
lin' (One a
a) = Vec x a -> Vec 'Leaf (Vec x a)
forall a. a -> Vec 'Leaf a
O (a -> Vec 'Leaf a
forall a. a -> Vec 'Leaf a
O a
a)
lin' (Row Mat x1 'Leaf a
a Mat x2 'Leaf a
b) = (Vec x1 a -> Vec x2 a -> Vec x a)
-> Vec y (Vec x1 a) -> Vec y (Vec x2 a) -> Vec y (Vec x a)
forall a b c (y :: Shape).
(AbelianGroup a, AbelianGroup b) =>
(a -> b -> c) -> Vec y a -> Vec y b -> Vec y c
zw Vec x1 a -> Vec x2 a -> Vec x a
Vec x1 a -> Vec x2 a -> Vec ('Bin x1 x2) a
forall (s :: Shape) a (s' :: Shape).
Vec s a -> Vec s' a -> Vec ('Bin s s') a
(:!) (Mat x1 y a -> Vec y (Vec x1 a)
forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Mat x y a -> Vec y (Vec x a)
lin' Mat x1 y a
Mat x1 'Leaf a
a) (Mat x2 y a -> Vec y (Vec x2 a)
forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Mat x y a -> Vec y (Vec x a)
lin' Mat x2 y a
Mat x2 'Leaf a
b)
lin' (Col Mat 'Leaf y1 a
a Mat 'Leaf y2 a
b) = Mat x y1 a -> Vec y1 (Vec x a)
forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Mat x y a -> Vec y (Vec x a)
lin' Mat x y1 a
Mat 'Leaf y1 a
a Vec y1 (Vec x a) -> Vec y2 (Vec x a) -> Vec ('Bin y1 y2) (Vec x a)
forall (s :: Shape) a (s' :: Shape).
Vec s a -> Vec s' a -> Vec ('Bin s s') a
:! Mat x y2 a -> Vec y2 (Vec x a)
forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Mat x y a -> Vec y (Vec x a)
lin' Mat x y2 a
Mat 'Leaf y2 a
b
lin' (Quad Mat x1 y1 a
a Mat x2 y1 a
b Mat x1 y2 a
c Mat x2 y2 a
d) = (Vec x1 a -> Vec x2 a -> Vec x a)
-> Vec y1 (Vec x1 a) -> Vec y1 (Vec x2 a) -> Vec y1 (Vec x a)
forall a b c (y :: Shape).
(AbelianGroup a, AbelianGroup b) =>
(a -> b -> c) -> Vec y a -> Vec y b -> Vec y c
zw Vec x1 a -> Vec x2 a -> Vec x a
Vec x1 a -> Vec x2 a -> Vec ('Bin x1 x2) a
forall (s :: Shape) a (s' :: Shape).
Vec s a -> Vec s' a -> Vec ('Bin s s') a
(:!) (Mat x1 y1 a -> Vec y1 (Vec x1 a)
forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Mat x y a -> Vec y (Vec x a)
lin' Mat x1 y1 a
a) (Mat x2 y1 a -> Vec y1 (Vec x2 a)
forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Mat x y a -> Vec y (Vec x a)
lin' Mat x2 y1 a
b) Vec y1 (Vec x a) -> Vec y2 (Vec x a) -> Vec ('Bin y1 y2) (Vec x a)
forall (s :: Shape) a (s' :: Shape).
Vec s a -> Vec s' a -> Vec ('Bin s s') a
:!(Vec x1 a -> Vec x2 a -> Vec x a)
-> Vec y2 (Vec x1 a) -> Vec y2 (Vec x2 a) -> Vec y2 (Vec x a)
forall a b c (y :: Shape).
(AbelianGroup a, AbelianGroup b) =>
(a -> b -> c) -> Vec y a -> Vec y b -> Vec y c
zw Vec x1 a -> Vec x2 a -> Vec x a
Vec x1 a -> Vec x2 a -> Vec ('Bin x1 x2) a
forall (s :: Shape) a (s' :: Shape).
Vec s a -> Vec s' a -> Vec ('Bin s s') a
(:!) (Mat x1 y2 a -> Vec y2 (Vec x1 a)
forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Mat x y a -> Vec y (Vec x a)
lin' Mat x1 y2 a
c) (Mat x2 y2 a -> Vec y2 (Vec x2 a)
forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Mat x y a -> Vec y (Vec x a)
lin' Mat x2 y2 a
d)

-- | Contents of a vector
contents :: Shape' x -> Vec x a -> [(Int,a)]
contents :: forall (x :: Shape) a. Shape' x -> Vec x a -> [(Int, a)]
contents Shape' x
s Vec x a
Z = []
contents Shape' x
s (O a
a) = [(Int
0,a
a)]
contents (Bin' Int
_ Shape' s
s Shape' s'
s') (Vec s a
xs :! Vec s' a
xs') = Shape' s -> Vec s a -> [(Int, a)]
forall (x :: Shape) a. Shape' x -> Vec x a -> [(Int, a)]
contents Shape' s
s Vec s a
Vec s a
xs [(Int, a)] -> [(Int, a)] -> [(Int, a)]
forall a. [a] -> [a] -> [a]
++ ((Int, a) -> (Int, a)) -> [(Int, a)] -> [(Int, a)]
forall a b. (a -> b) -> [a] -> [b]
map ((Int -> Int) -> (Int, a) -> (Int, a)
forall {t} {a} {b}. (t -> a) -> (t, b) -> (a, b)
first (Int -> Int -> Int
forall a. AbelianGroup a => a -> a -> a
+Shape' s -> Int
forall (s :: Shape). Shape' s -> Int
sz' Shape' s
s)) (Shape' s' -> Vec s' a -> [(Int, a)]
forall (x :: Shape) a. Shape' x -> Vec x a -> [(Int, a)]
contents Shape' s'
s' Vec s' a
Vec s' a
xs')


first :: (t -> a) -> (t, b) -> (a, b)
first t -> a
f (t
a,b
b) = (t -> a
f t
a,b
b)
second :: (t -> b) -> (a, t) -> (a, b)
second t -> b
f (a
a,t
b) = (a
a,t -> b
f t
b)

instance AbelianGroup a => AbelianGroup (Vec x a) where
  zero :: Vec x a
zero = Vec x a
forall (s :: Shape) a. Vec s a
Z
  + :: Vec x a -> Vec x a -> Vec x a
(+) = (a -> a -> a) -> Vec x a -> Vec x a -> Vec x a
forall a b c (y :: Shape).
(AbelianGroup a, AbelianGroup b) =>
(a -> b -> c) -> Vec y a -> Vec y b -> Vec y c
zw a -> a -> a
forall a. AbelianGroup a => a -> a -> a
(+)

data Path :: Shape -> * where
  Here :: Path Leaf
  Low  :: Path s -> Path (Bin s s')
  High :: Path s -> Path (Bin s' s)

(<||>) :: Maybe (a,Path x) -> Maybe (a,Path x') -> Maybe (a,Path (Bin x x'))
Maybe (a, Path x)
x <||> :: forall a (x :: Shape) (x' :: Shape).
Maybe (a, Path x)
-> Maybe (a, Path x') -> Maybe (a, Path ('Bin x x'))
<||> Maybe (a, Path x')
y =  ((Path x' -> Path ('Bin x x'))
-> (a, Path x') -> (a, Path ('Bin x x'))
forall {t} {b} {a}. (t -> b) -> (a, t) -> (a, b)
second Path x' -> Path ('Bin x x')
forall (s :: Shape) (s' :: Shape). Path s -> Path ('Bin s' s)
High ((a, Path x') -> (a, Path ('Bin x x')))
-> Maybe (a, Path x') -> Maybe (a, Path ('Bin x x'))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (a, Path x')
y) Maybe (a, Path ('Bin x x'))
-> Maybe (a, Path ('Bin x x')) -> Maybe (a, Path ('Bin x x'))
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ((Path x -> Path ('Bin x x'))
-> (a, Path x) -> (a, Path ('Bin x x'))
forall {t} {b} {a}. (t -> b) -> (a, t) -> (a, b)
second Path x -> Path ('Bin x x')
forall (s :: Shape) (s' :: Shape). Path s -> Path ('Bin s s')
Low ((a, Path x) -> (a, Path ('Bin x x')))
-> Maybe (a, Path x) -> Maybe (a, Path ('Bin x x'))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (a, Path x)
x)

-- | What is, and where is the rightmost non-zero element on a given
-- line of the matrix?
rightmostOnLine :: Path y -> Mat x y a -> Maybe (a,Path x)
rightmostOnLine :: forall (y :: Shape) (x :: Shape) a.
Path y -> Mat x y a -> Maybe (a, Path x)
rightmostOnLine Path y
_ Mat x y a
Zero = Maybe (a, Path x)
forall a. Maybe a
Nothing
rightmostOnLine Path y
Here (One a
x) = (a, Path x) -> Maybe (a, Path x)
forall a. a -> Maybe a
Just (a
x,Path x
Path 'Leaf
Here)
rightmostOnLine Path y
Here (Row Mat x1 'Leaf a
a Mat x2 'Leaf a
b)    = Path 'Leaf -> Mat x1 'Leaf a -> Maybe (a, Path x1)
forall (y :: Shape) (x :: Shape) a.
Path y -> Mat x y a -> Maybe (a, Path x)
rightmostOnLine Path 'Leaf
Here Mat x1 'Leaf a
a Maybe (a, Path x1)
-> Maybe (a, Path x2) -> Maybe (a, Path ('Bin x1 x2))
forall a (x :: Shape) (x' :: Shape).
Maybe (a, Path x)
-> Maybe (a, Path x') -> Maybe (a, Path ('Bin x x'))
<||> Path 'Leaf -> Mat x2 'Leaf a -> Maybe (a, Path x2)
forall (y :: Shape) (x :: Shape) a.
Path y -> Mat x y a -> Maybe (a, Path x)
rightmostOnLine Path 'Leaf
Here Mat x2 'Leaf a
b
rightmostOnLine (Low Path s
p) (Col Mat 'Leaf y1 a
a Mat 'Leaf y2 a
b) = Path s -> Mat x s a -> Maybe (a, Path x)
forall (y :: Shape) (x :: Shape) a.
Path y -> Mat x y a -> Maybe (a, Path x)
rightmostOnLine Path s
p Mat x s a
Mat 'Leaf y1 a
a
rightmostOnLine (High Path s
p) (Col Mat 'Leaf y1 a
a Mat 'Leaf y2 a
b) = Path s -> Mat x s a -> Maybe (a, Path x)
forall (y :: Shape) (x :: Shape) a.
Path y -> Mat x y a -> Maybe (a, Path x)
rightmostOnLine Path s
p Mat x s a
Mat 'Leaf y2 a
b
rightmostOnLine (Low Path s
p) (Quad Mat x1 y1 a
a Mat x2 y1 a
b Mat x1 y2 a
_ Mat x2 y2 a
_) = Path s -> Mat x1 s a -> Maybe (a, Path x1)
forall (y :: Shape) (x :: Shape) a.
Path y -> Mat x y a -> Maybe (a, Path x)
rightmostOnLine Path s
p Mat x1 s a
Mat x1 y1 a
a Maybe (a, Path x1)
-> Maybe (a, Path x2) -> Maybe (a, Path ('Bin x1 x2))
forall a (x :: Shape) (x' :: Shape).
Maybe (a, Path x)
-> Maybe (a, Path x') -> Maybe (a, Path ('Bin x x'))
<||> Path s -> Mat x2 s a -> Maybe (a, Path x2)
forall (y :: Shape) (x :: Shape) a.
Path y -> Mat x y a -> Maybe (a, Path x)
rightmostOnLine Path s
p Mat x2 s a
Mat x2 y1 a
b
rightmostOnLine (High Path s
p) (Quad Mat x1 y1 a
_ Mat x2 y1 a
_ Mat x1 y2 a
a Mat x2 y2 a
b) = Path s -> Mat x1 s a -> Maybe (a, Path x1)
forall (y :: Shape) (x :: Shape) a.
Path y -> Mat x y a -> Maybe (a, Path x)
rightmostOnLine Path s
p Mat x1 s a
Mat x1 y2 a
a Maybe (a, Path x1)
-> Maybe (a, Path x2) -> Maybe (a, Path ('Bin x1 x2))
forall a (x :: Shape) (x' :: Shape).
Maybe (a, Path x)
-> Maybe (a, Path x') -> Maybe (a, Path ('Bin x x'))
<||> Path s -> Mat x2 s a -> Maybe (a, Path x2)
forall (y :: Shape) (x :: Shape) a.
Path y -> Mat x y a -> Maybe (a, Path x)
rightmostOnLine Path s
p Mat x2 s a
Mat x2 y2 a
b

-- | Is this the rightmost path?
isRightmost :: Path x -> Bool
isRightmost :: forall (x :: Shape). Path x -> Bool
isRightmost (Low Path s
_) = Bool
False
isRightmost (Path x
Here) = Bool
True
isRightmost (High Path s
x) = Path s -> Bool
forall (x :: Shape). Path x -> Bool
isRightmost Path s
x

results' :: AbelianGroup a => Mat y y a -> Path y -> [(Path y, a, Path y)]
results' :: forall a (y :: Shape).
AbelianGroup a =>
Mat y y a -> Path y -> [(Path y, a, Path y)]
results' Mat y y a
m Path y
y | Path y -> Bool
forall (x :: Shape). Path x -> Bool
isRightmost Path y
y = []
             | Bool
otherwise = (Path y
y,a
a,Path y
x) (Path y, a, Path y)
-> [(Path y, a, Path y)] -> [(Path y, a, Path y)]
forall a. a -> [a] -> [a]
: Mat y y a -> Path y -> [(Path y, a, Path y)]
forall a (y :: Shape).
AbelianGroup a =>
Mat y y a -> Path y -> [(Path y, a, Path y)]
results' Mat y y a
m Path y
x
  where Just (a
a,Path y
x) = Path y -> Mat y y a -> Maybe (a, Path y)
forall (y :: Shape) (x :: Shape) a.
Path y -> Mat x y a -> Maybe (a, Path x)
rightmostOnLine Path y
y Mat y y a
m

results :: AbelianGroupZ a => SomeTri a -> [(Int, a, Int)]
results :: forall a. AbelianGroupZ a => SomeTri a -> [(Int, a, Int)]
results (T Shape' s
s (Mat s s a
m :/: Mat s s a
m')) = [(Shape' s -> Path s -> Int
forall (y :: Shape). Shape' y -> Path y -> Int
fromPath Shape' s
s Path s
x,a
a,Shape' s -> Path s -> Int
forall (y :: Shape). Shape' y -> Path y -> Int
fromPath Shape' s
s Path s
y) | (Path s
x,a
a,Path s
y) <- Mat s s a -> Path s -> [(Path s, a, Path s)]
forall a (y :: Shape).
AbelianGroup a =>
Mat y y a -> Path y -> [(Path y, a, Path y)]
results' (Mat s s a
mMat s s a -> Mat s s a -> Mat s s a
forall a. AbelianGroup a => a -> a -> a
+Mat s s a
m') (Shape' s -> Path s
forall (s :: Shape). Shape' s -> Path s
leftMost Shape' s
s)]

leftMost :: Shape' s -> Path s
leftMost :: forall (s :: Shape). Shape' s -> Path s
leftMost Shape' s
Leaf' = Path s
Path 'Leaf
Here
leftMost (Bin' Int
_ Shape' s
s Shape' s'
_) = Path s -> Path ('Bin s s')
forall (s :: Shape) (s' :: Shape). Path s -> Path ('Bin s s')
Low (Path s -> Path ('Bin s s')) -> Path s -> Path ('Bin s s')
forall a b. (a -> b) -> a -> b
$ Shape' s -> Path s
forall (s :: Shape). Shape' s -> Path s
leftMost Shape' s
s

fromPath :: Shape' y -> Path y -> Int
fromPath :: forall (y :: Shape). Shape' y -> Path y -> Int
fromPath Shape' y
_ Path y
Here =  Int
0
fromPath (Bin' Int
_ Shape' s
s Shape' s'
s') (Low Path s
x) = Shape' s -> Path s -> Int
forall (y :: Shape). Shape' y -> Path y -> Int
fromPath Shape' s
s Path s
Path s
x
fromPath (Bin' Int
_ Shape' s
s Shape' s'
s') (High Path s
x) = Shape' s -> Int
forall (s :: Shape). Shape' s -> Int
sz' Shape' s
s Int -> Int -> Int
forall a. AbelianGroup a => a -> a -> a
+ Shape' s' -> Path s' -> Int
forall (y :: Shape). Shape' y -> Path y -> Int
fromPath Shape' s'
s' Path s'
Path s
x


root' :: AbelianGroup a => Mat x y a -> a
root' :: forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Mat x y a -> a
root' Mat x y a
Zero = a
forall a. AbelianGroup a => a
zero
root' (One a
x) = a
x
root' (Quad Mat x1 y1 a
_ Mat x2 y1 a
a Mat x1 y2 a
_ Mat x2 y2 a
_) = Mat x2 y1 a -> a
forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Mat x y a -> a
root' Mat x2 y1 a
a
root' (Col Mat 'Leaf y1 a
a Mat 'Leaf y2 a
_) = Mat 'Leaf y1 a -> a
forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Mat x y a -> a
root' Mat 'Leaf y1 a
a
root' (Row Mat x1 'Leaf a
_ Mat x2 'Leaf a
a) = Mat x2 'Leaf a -> a
forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Mat x y a -> a
root' Mat x2 'Leaf a
a

root :: SomeTri p -> p
root (T Shape' s
_ (Mat s s p
m :/: Mat s s p
m')) = Mat s s p -> p
forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Mat x y a -> a
root' Mat s s p
m p -> p -> p
forall a. AbelianGroup a => a -> a -> a
+ Mat s s p -> p
forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Mat x y a -> a
root' Mat s s p
m'

single :: Pair a -> SomeTri a
single Pair a
x = Shape' 'Leaf -> Pair (Mat 'Leaf 'Leaf a) -> SomeTri a
forall (s :: Shape) a. Shape' s -> Pair (Mat s s a) -> SomeTri a
T Shape' 'Leaf
Leaf' (a -> Mat 'Leaf 'Leaf a
forall a. AbelianGroupZ a => a -> Mat 'Leaf 'Leaf a
one (a -> Mat 'Leaf 'Leaf a) -> Pair a -> Pair (Mat 'Leaf 'Leaf a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pair a
x)

square2 :: Pair a -> SomeTri a
square2 Pair a
x = Shape' ('Bin 'Leaf 'Leaf)
-> Pair (Mat ('Bin 'Leaf 'Leaf) ('Bin 'Leaf 'Leaf) a) -> SomeTri a
forall (s :: Shape) a. Shape' s -> Pair (Mat s s a) -> SomeTri a
T (Shape' 'Leaf -> Shape' 'Leaf -> Shape' ('Bin 'Leaf 'Leaf)
forall (s :: Shape) (s' :: Shape).
Shape' s -> Shape' s' -> Shape' ('Bin s s')
bin' Shape' 'Leaf
Leaf' Shape' 'Leaf
Leaf') (Pair (Mat ('Bin 'Leaf 'Leaf) ('Bin 'Leaf 'Leaf) a) -> SomeTri a)
-> Pair (Mat ('Bin 'Leaf 'Leaf) ('Bin 'Leaf 'Leaf) a) -> SomeTri a
forall a b. (a -> b) -> a -> b
$ Pair (Mat 'Leaf 'Leaf a)
-> Pair (Mat 'Leaf 'Leaf a)
-> Pair (Mat 'Leaf 'Leaf a)
-> Pair (Mat 'Leaf 'Leaf a)
-> Pair (Mat ('Bin 'Leaf 'Leaf) ('Bin 'Leaf 'Leaf) a)
forall {f :: * -> *} {x1 :: Shape} {y1 :: Shape} {a} {x2 :: Shape}
       {y2 :: Shape}.
Applicative f =>
f (Mat x1 y1 a)
-> f (Mat x2 y1 a)
-> f (Mat x1 y2 a)
-> f (Mat x2 y2 a)
-> f (Mat ('Bin x1 x2) ('Bin y1 y2) a)
quad' Pair (Mat 'Leaf 'Leaf a)
forall a. AbelianGroup a => a
zero (a -> Mat 'Leaf 'Leaf a
forall a. AbelianGroupZ a => a -> Mat 'Leaf 'Leaf a
one (a -> Mat 'Leaf 'Leaf a) -> Pair a -> Pair (Mat 'Leaf 'Leaf a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pair a
x) Pair (Mat 'Leaf 'Leaf a)
forall a. AbelianGroup a => a
zero Pair (Mat 'Leaf 'Leaf a)
forall a. AbelianGroup a => a
zero

square3 :: Bool -> Pair a -> Pair a -> SomeTri a
square3 Bool
p Pair a
x Pair a
y = Shape' ('Bin ('Bin 'Leaf 'Leaf) 'Leaf)
-> Pair
     (Mat
        ('Bin ('Bin 'Leaf 'Leaf) 'Leaf) ('Bin ('Bin 'Leaf 'Leaf) 'Leaf) a)
-> SomeTri a
forall (s :: Shape) a. Shape' s -> Pair (Mat s s a) -> SomeTri a
T (Shape' ('Bin 'Leaf 'Leaf)
-> Shape' 'Leaf -> Shape' ('Bin ('Bin 'Leaf 'Leaf) 'Leaf)
forall (s :: Shape) (s' :: Shape).
Shape' s -> Shape' s' -> Shape' ('Bin s s')
bin' (Shape' 'Leaf -> Shape' 'Leaf -> Shape' ('Bin 'Leaf 'Leaf)
forall (s :: Shape) (s' :: Shape).
Shape' s -> Shape' s' -> Shape' ('Bin s s')
bin' Shape' 'Leaf
Leaf' Shape' 'Leaf
Leaf') (Shape' 'Leaf
Leaf'))
  (Pair (Mat ('Bin 'Leaf 'Leaf) ('Bin 'Leaf 'Leaf) a)
-> Pair (Mat 'Leaf ('Bin 'Leaf 'Leaf) a)
-> Pair (Mat ('Bin 'Leaf 'Leaf) 'Leaf a)
-> Pair (Mat 'Leaf 'Leaf a)
-> Pair
     (Mat
        ('Bin ('Bin 'Leaf 'Leaf) 'Leaf) ('Bin ('Bin 'Leaf 'Leaf) 'Leaf) a)
forall {f :: * -> *} {x1 :: Shape} {y1 :: Shape} {a} {x2 :: Shape}
       {y2 :: Shape}.
Applicative f =>
f (Mat x1 y1 a)
-> f (Mat x2 y1 a)
-> f (Mat x1 y2 a)
-> f (Mat x2 y2 a)
-> f (Mat ('Bin x1 x2) ('Bin y1 y2) a)
quad' (Pair (Mat 'Leaf 'Leaf a)
-> Pair (Mat 'Leaf 'Leaf a)
-> Pair (Mat 'Leaf 'Leaf a)
-> Pair (Mat 'Leaf 'Leaf a)
-> Pair (Mat ('Bin 'Leaf 'Leaf) ('Bin 'Leaf 'Leaf) a)
forall {f :: * -> *} {x1 :: Shape} {y1 :: Shape} {a} {x2 :: Shape}
       {y2 :: Shape}.
Applicative f =>
f (Mat x1 y1 a)
-> f (Mat x2 y1 a)
-> f (Mat x1 y2 a)
-> f (Mat x2 y2 a)
-> f (Mat ('Bin x1 x2) ('Bin y1 y2) a)
quad' Pair (Mat 'Leaf 'Leaf a)
forall a. AbelianGroup a => a
zero (a -> Mat 'Leaf 'Leaf a
forall a. AbelianGroupZ a => a -> Mat 'Leaf 'Leaf a
one (a -> Mat 'Leaf 'Leaf a) -> Pair a -> Pair (Mat 'Leaf 'Leaf a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pair a
x) Pair (Mat 'Leaf 'Leaf a)
forall a. AbelianGroup a => a
zero Pair (Mat 'Leaf 'Leaf a)
forall a. AbelianGroup a => a
zero) (Mat 'Leaf 'Leaf a
-> Mat 'Leaf 'Leaf a -> Mat 'Leaf ('Bin 'Leaf 'Leaf) a
forall (y1 :: Shape) a (y2 :: Shape).
Mat 'Leaf y1 a -> Mat 'Leaf y2 a -> Mat 'Leaf ('Bin y1 y2) a
Col (Mat 'Leaf 'Leaf a
 -> Mat 'Leaf 'Leaf a -> Mat 'Leaf ('Bin 'Leaf 'Leaf) a)
-> Pair (Mat 'Leaf 'Leaf a)
-> Pair (Mat 'Leaf 'Leaf a -> Mat 'Leaf ('Bin 'Leaf 'Leaf) a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> Mat 'Leaf 'Leaf a
forall a. AbelianGroupZ a => a -> Mat 'Leaf 'Leaf a
one (a -> Mat 'Leaf 'Leaf a) -> Pair a -> Pair (Mat 'Leaf 'Leaf a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> a -> a -> Pair a
forall a. RingP a => Bool -> a -> a -> Pair a
mul Bool
p (Pair a -> a
forall a. Pair a -> a
leftOf Pair a
x) (Pair a -> a
forall a. Pair a -> a
rightOf Pair a
y)) Pair (Mat 'Leaf 'Leaf a -> Mat 'Leaf ('Bin 'Leaf 'Leaf) a)
-> Pair (Mat 'Leaf 'Leaf a)
-> Pair (Mat 'Leaf ('Bin 'Leaf 'Leaf) a)
forall a b. Pair (a -> b) -> Pair a -> Pair b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (a -> Mat 'Leaf 'Leaf a
forall a. AbelianGroupZ a => a -> Mat 'Leaf 'Leaf a
one (a -> Mat 'Leaf 'Leaf a) -> Pair a -> Pair (Mat 'Leaf 'Leaf a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pair a
y)) Pair (Mat ('Bin 'Leaf 'Leaf) 'Leaf a)
forall a. AbelianGroup a => a
zero Pair (Mat 'Leaf 'Leaf a)
forall a. AbelianGroup a => a
zero)


sz' :: Shape' s -> Int
sz' :: forall (s :: Shape). Shape' s -> Int
sz' Shape' s
Leaf' = Int
1
sz' (Bin' Int
x Shape' s
l Shape' s'
r) = Int
x -- sz' l + sz' r


|+| :: [[a]] -> [[a]] -> [[a]]
(|+|) = ([a] -> [a] -> [a]) -> [[a]] -> [[a]] -> [[a]]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
(++)
-+- :: [a] -> [a] -> [a]
(-+-) = [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
(++)

-- TODO: reimplement using lin'
lin :: AbelianGroup a => Shape' x -> Shape' y -> Mat x y a -> [[a]]
lin :: forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Shape' x -> Shape' y -> Mat x y a -> [[a]]
lin Shape' x
x Shape' y
y Mat x y a
Zero = Int -> [a] -> [[a]]
forall a. Int -> a -> [a]
replicate (Shape' y -> Int
forall (s :: Shape). Shape' s -> Int
sz' Shape' y
y) ([a] -> [[a]]) -> [a] -> [[a]]
forall a b. (a -> b) -> a -> b
$ Int -> a -> [a]
forall a. Int -> a -> [a]
replicate (Shape' x -> Int
forall (s :: Shape). Shape' s -> Int
sz' Shape' x
x) a
forall a. AbelianGroup a => a
zero
lin Shape' x
_ Shape' y
_ (One a
x) = [[a
x]]
lin (Bin' Int
_ Shape' s
x Shape' s'
x') (Bin' Int
_ Shape' s
y Shape' s'
y') (Quad Mat x1 y1 a
a Mat x2 y1 a
b Mat x1 y2 a
c Mat x2 y2 a
d) = (Shape' s -> Shape' s -> Mat s s a -> [[a]]
forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Shape' x -> Shape' y -> Mat x y a -> [[a]]
lin Shape' s
x Shape' s
y Mat s s a
Mat x1 y1 a
a [[a]] -> [[a]] -> [[a]]
forall {a}. [[a]] -> [[a]] -> [[a]]
|+| Shape' s' -> Shape' s -> Mat s' s a -> [[a]]
forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Shape' x -> Shape' y -> Mat x y a -> [[a]]
lin Shape' s'
x' Shape' s
y Mat s' s a
Mat x2 y1 a
b) [[a]] -> [[a]] -> [[a]]
forall a. [a] -> [a] -> [a]
-+- (Shape' s -> Shape' s' -> Mat s s' a -> [[a]]
forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Shape' x -> Shape' y -> Mat x y a -> [[a]]
lin Shape' s
x Shape' s'
y' Mat s s' a
Mat x1 y2 a
c [[a]] -> [[a]] -> [[a]]
forall {a}. [[a]] -> [[a]] -> [[a]]
|+| Shape' s' -> Shape' s' -> Mat s' s' a -> [[a]]
forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Shape' x -> Shape' y -> Mat x y a -> [[a]]
lin Shape' s'
x' Shape' s'
y' Mat s' s' a
Mat x2 y2 a
d)
lin Shape' x
Leaf' (Bin' Int
_ Shape' s
y Shape' s'
y') (Col Mat 'Leaf y1 a
a Mat 'Leaf y2 a
b) = Shape' 'Leaf -> Shape' s -> Mat 'Leaf s a -> [[a]]
forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Shape' x -> Shape' y -> Mat x y a -> [[a]]
lin Shape' 'Leaf
Leaf' Shape' s
y Mat 'Leaf s a
Mat 'Leaf y1 a
a [[a]] -> [[a]] -> [[a]]
forall a. [a] -> [a] -> [a]
-+- Shape' 'Leaf -> Shape' s' -> Mat 'Leaf s' a -> [[a]]
forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Shape' x -> Shape' y -> Mat x y a -> [[a]]
lin Shape' 'Leaf
Leaf' Shape' s'
y' Mat 'Leaf s' a
Mat 'Leaf y2 a
b
lin (Bin' Int
_ Shape' s
x Shape' s'
x') Shape' y
Leaf' (Row Mat x1 'Leaf a
a Mat x2 'Leaf a
b) = (Shape' s -> Shape' 'Leaf -> Mat s 'Leaf a -> [[a]]
forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Shape' x -> Shape' y -> Mat x y a -> [[a]]
lin Shape' s
x Shape' 'Leaf
Leaf' Mat s 'Leaf a
Mat x1 'Leaf a
a) [[a]] -> [[a]] -> [[a]]
forall {a}. [[a]] -> [[a]] -> [[a]]
|+| (Shape' s' -> Shape' 'Leaf -> Mat s' 'Leaf a -> [[a]]
forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Shape' x -> Shape' y -> Mat x y a -> [[a]]
lin Shape' s'
x' Shape' 'Leaf
Leaf' Mat s' 'Leaf a
Mat x2 'Leaf a
b)

sparse :: AbelianGroup a => Shape' x -> Shape' y -> Mat x y a -> [(Int,Int,a)]
sparse :: forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Shape' x -> Shape' y -> Mat x y a -> [(Int, Int, a)]
sparse Shape' x
x Shape' y
y Mat x y a
Zero = []
sparse Shape' x
_ Shape' y
_ (One a
x) = [(Int
0,Int
0,a
x)]
sparse (Bin' Int
_ Shape' s
x Shape' s'
x') (Bin' Int
_ Shape' s
y Shape' s'
y') (Quad Mat x1 y1 a
a Mat x2 y1 a
b Mat x1 y2 a
c Mat x2 y2 a
d) = Shape' s -> Shape' s -> Mat s s a -> [(Int, Int, a)]
forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Shape' x -> Shape' y -> Mat x y a -> [(Int, Int, a)]
sparse Shape' s
x Shape' s
y Mat s s a
Mat x1 y1 a
a [(Int, Int, a)] -> [(Int, Int, a)] -> [(Int, Int, a)]
forall a. [a] -> [a] -> [a]
++ Shape' s -> [(Int, Int, a)] -> [(Int, Int, a)]
forall {s :: Shape} {b} {c}.
Shape' s -> [(Int, b, c)] -> [(Int, b, c)]
shiftX Shape' s
x (Shape' s' -> Shape' s -> Mat s' s a -> [(Int, Int, a)]
forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Shape' x -> Shape' y -> Mat x y a -> [(Int, Int, a)]
sparse Shape' s'
x' Shape' s
y Mat s' s a
Mat x2 y1 a
b) [(Int, Int, a)] -> [(Int, Int, a)] -> [(Int, Int, a)]
forall a. [a] -> [a] -> [a]
++ Shape' s -> [(Int, Int, a)] -> [(Int, Int, a)]
forall {s :: Shape} {a} {c}.
Shape' s -> [(a, Int, c)] -> [(a, Int, c)]
shiftY Shape' s
y (Shape' s -> Shape' s' -> Mat s s' a -> [(Int, Int, a)]
forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Shape' x -> Shape' y -> Mat x y a -> [(Int, Int, a)]
sparse Shape' s
x Shape' s'
y' Mat s s' a
Mat x1 y2 a
c) [(Int, Int, a)] -> [(Int, Int, a)] -> [(Int, Int, a)]
forall a. [a] -> [a] -> [a]
++ Shape' s -> [(Int, Int, a)] -> [(Int, Int, a)]
forall {s :: Shape} {b} {c}.
Shape' s -> [(Int, b, c)] -> [(Int, b, c)]
shiftX Shape' s
x (Shape' s -> [(Int, Int, a)] -> [(Int, Int, a)]
forall {s :: Shape} {a} {c}.
Shape' s -> [(a, Int, c)] -> [(a, Int, c)]
shiftY Shape' s
y(Shape' s' -> Shape' s' -> Mat s' s' a -> [(Int, Int, a)]
forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Shape' x -> Shape' y -> Mat x y a -> [(Int, Int, a)]
sparse Shape' s'
x' Shape' s'
y' Mat s' s' a
Mat x2 y2 a
d))
sparse Shape' x
Leaf' (Bin' Int
_ Shape' s
y Shape' s'
y') (Col Mat 'Leaf y1 a
a Mat 'Leaf y2 a
b) = Shape' 'Leaf -> Shape' s -> Mat 'Leaf s a -> [(Int, Int, a)]
forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Shape' x -> Shape' y -> Mat x y a -> [(Int, Int, a)]
sparse Shape' 'Leaf
Leaf' Shape' s
y Mat 'Leaf s a
Mat 'Leaf y1 a
a [(Int, Int, a)] -> [(Int, Int, a)] -> [(Int, Int, a)]
forall a. [a] -> [a] -> [a]
++ Shape' s -> [(Int, Int, a)] -> [(Int, Int, a)]
forall {s :: Shape} {a} {c}.
Shape' s -> [(a, Int, c)] -> [(a, Int, c)]
shiftY Shape' s
y (Shape' 'Leaf -> Shape' s' -> Mat 'Leaf s' a -> [(Int, Int, a)]
forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Shape' x -> Shape' y -> Mat x y a -> [(Int, Int, a)]
sparse Shape' 'Leaf
Leaf' Shape' s'
y' Mat 'Leaf s' a
Mat 'Leaf y2 a
b)
sparse (Bin' Int
_ Shape' s
x Shape' s'
x') Shape' y
Leaf' (Row Mat x1 'Leaf a
a Mat x2 'Leaf a
b) = Shape' s -> Shape' 'Leaf -> Mat s 'Leaf a -> [(Int, Int, a)]
forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Shape' x -> Shape' y -> Mat x y a -> [(Int, Int, a)]
sparse Shape' s
x Shape' 'Leaf
Leaf' Mat s 'Leaf a
Mat x1 'Leaf a
a [(Int, Int, a)] -> [(Int, Int, a)] -> [(Int, Int, a)]
forall a. [a] -> [a] -> [a]
++ Shape' s -> [(Int, Int, a)] -> [(Int, Int, a)]
forall {s :: Shape} {b} {c}.
Shape' s -> [(Int, b, c)] -> [(Int, b, c)]
shiftX Shape' s
x (Shape' s' -> Shape' 'Leaf -> Mat s' 'Leaf a -> [(Int, Int, a)]
forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Shape' x -> Shape' y -> Mat x y a -> [(Int, Int, a)]
sparse Shape' s'
x' Shape' 'Leaf
Leaf' Mat s' 'Leaf a
Mat x2 'Leaf a
b)

shiftX :: Shape' s -> [(Int, b, c)] -> [(Int, b, c)]
shiftX Shape' s
x0 [(Int, b, c)]
as = [(Int
xInt -> Int -> Int
forall a. AbelianGroup a => a -> a -> a
+Shape' s -> Int
forall (s :: Shape). Shape' s -> Int
sz' Shape' s
x0,b
y,c
a) | (Int
x,b
y,c
a) <- [(Int, b, c)]
as]
shiftY :: Shape' s -> [(a, Int, c)] -> [(a, Int, c)]
shiftY Shape' s
y0 [(a, Int, c)]
as = [(a
x,Int
yInt -> Int -> Int
forall a. AbelianGroup a => a -> a -> a
+Shape' s -> Int
forall (s :: Shape). Shape' s -> Int
sz' Shape' s
y0,c
a) | (a
x,Int
y,c
a) <- [(a, Int, c)]
as]

fingerprint :: SomeTri a -> [[Char]]
fingerprint (T Shape' s
s (Mat s s a
m :/: Mat s s a
m')) = ([a] -> [a] -> [Char]) -> [[a]] -> [[a]] -> [[Char]]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith ((a -> a -> Char) -> [a] -> [a] -> [Char]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith a -> a -> Char
forall {a} {a}.
(AbelianGroupZ a, AbelianGroupZ a) =>
a -> a -> Char
c) (Shape' s -> Shape' s -> Mat s s a -> [[a]]
forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Shape' x -> Shape' y -> Mat x y a -> [[a]]
lin Shape' s
s Shape' s
s Mat s s a
m) (Shape' s -> Shape' s -> Mat s s a -> [[a]]
forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Shape' x -> Shape' y -> Mat x y a -> [[a]]
lin Shape' s
s Shape' s
s Mat s s a
m')
  where c :: a -> a -> Char
c a
x a
y = case (a -> Bool
forall a. AbelianGroupZ a => a -> Bool
isZero a
x,a -> Bool
forall a. AbelianGroupZ a => a -> Bool
isZero a
y) of
                     (Bool
True  , Bool
True) -> Char
' '
                     (Bool
True  , Bool
False) -> Char
'>'
                     (Bool
False , Bool
True) -> Char
'<'
                     (Bool
False , Bool
False) -> Char
'X'

scatterplot :: SomeTri a -> [Char]
scatterplot (T Shape' s
s (Mat s s a
m :/: Mat s s a
m')) = [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Int -> [Char]
forall a. Show a => a -> [Char]
show Int
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
y [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n" | (Int
x,Int
y,a
_) <- Shape' s -> Shape' s -> Mat s s a -> [(Int, Int, a)]
forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Shape' x -> Shape' y -> Mat x y a -> [(Int, Int, a)]
sparse Shape' s
s Shape' s
s Mat s s a
m [(Int, Int, a)] -> [(Int, Int, a)] -> [(Int, Int, a)]
forall a. [a] -> [a] -> [a]
++ Shape' s -> Shape' s -> Mat s s a -> [(Int, Int, a)]
forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Shape' x -> Shape' y -> Mat x y a -> [(Int, Int, a)]
sparse Shape' s
s Shape' s
s Mat s s a
m']