{-# 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)
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 = forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero
row Mat x1 'Leaf a
x Mat x2 'Leaf a
y = 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 = forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero
col Mat 'Leaf y1 a
x Mat 'Leaf y2 a
y = 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 = 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 = 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 | forall a. AbelianGroupZ a => a -> Bool
isZero a
x = forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero
      | Bool
otherwise = 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' = 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 forall a (x :: Shape) (y :: Shape).
AbelianGroupZ a =>
Mat x y a -> Mat x y a -> Mat x y a
.+. Mat x1 y1 a
a') (Mat x2 y1 a
b forall a (x :: Shape) (y :: Shape).
AbelianGroupZ a =>
Mat x y a -> Mat x y a -> Mat x y a
.+. Mat x2 y1 a
b') (Mat x1 y2 a
c forall a (x :: Shape) (y :: Shape).
AbelianGroupZ a =>
Mat x y a -> Mat x y a -> Mat x y a
.+. Mat x1 y2 a
c') (Mat x2 y2 a
d forall a (x :: Shape) (y :: Shape).
AbelianGroupZ a =>
Mat x y a -> Mat x y a -> Mat x y a
.+. Mat x2 y2 a
d')
One a
x .+. One a
x' = forall a. AbelianGroupZ a => a -> Mat 'Leaf 'Leaf a
one (a
x 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' = 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 forall a (x :: Shape) (y :: Shape).
AbelianGroupZ a =>
Mat x y a -> Mat x y a -> Mat x y a
.+. Mat x1 'Leaf a
x') (Mat x2 'Leaf a
y forall a (x :: Shape) (y :: Shape).
AbelianGroupZ a =>
Mat x y a -> Mat x y a -> Mat x y 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' = 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 forall a (x :: Shape) (y :: Shape).
AbelianGroupZ a =>
Mat x y a -> Mat x y a -> Mat x y a
.+. Mat 'Leaf y1 a
x') (Mat 'Leaf y2 a
y forall a (x :: Shape) (y :: Shape).
AbelianGroupZ a =>
Mat x y a -> Mat x y a -> Mat x y 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
(+) = 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 = 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 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 = forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero
  Mat x y a
x & Mat z x a
Zero = forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero
  One a
x & One a
x' = forall a. AbelianGroupZ a => a -> Mat 'Leaf 'Leaf a
one (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 = forall (s :: Shape) a (s' :: Shape).
Mat s 'Leaf a -> Mat s' 'Leaf a -> Mat ('Bin s s') 'Leaf a
row (forall a. a -> Mat 'Leaf 'Leaf a
One a
x 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) (forall a. a -> Mat 'Leaf 'Leaf a
One a
x 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 = 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 forall a (x :: Shape) (y :: Shape) (z :: Shape).
RingP a =>
Mat x y a -> Mat z x a -> Mat z y (Pair a)
& forall a. a -> Mat 'Leaf 'Leaf a
One a
x) (Mat 'Leaf y2 a
b forall a (x :: Shape) (y :: Shape) (z :: Shape).
RingP a =>
Mat x y a -> Mat z x a -> Mat z y (Pair 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 'Leaf a
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 y1 a
a' forall a. AbelianGroup a => a -> a -> a
+ Mat x2 'Leaf a
b 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 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' = 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 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 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 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 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' = 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 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 y1 a
a' forall a. AbelianGroup a => a -> a -> a
+ Mat x2 'Leaf a
b 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 y2 a
c') (Mat x1 'Leaf a
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 y1 a
b' forall a. AbelianGroup a => a -> a -> a
+ Mat x2 'Leaf a
b 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 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' = 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 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 y1 a
a' forall a. AbelianGroup a => a -> a -> a
+ Mat x2 y1 a
b 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 y2 a
c') (Mat x1 y2 a
c 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 y1 a
a' forall a. AbelianGroup a => a -> a -> a
+ Mat x2 y2 a
d 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 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' = 
     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 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 y1 a
a' forall a. AbelianGroup a => a -> a -> a
+ Mat x2 y1 a
b 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 y2 a
c') (Mat x1 y1 a
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 y1 a
b' forall a. AbelianGroup a => a -> a -> a
+ Mat x2 y1 a
b 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 y2 a
d')
          (Mat x1 y2 a
c 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 y1 a
a' forall a. AbelianGroup a => a -> a -> a
+ Mat x2 y2 a
d 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 y2 a
c') (Mat x1 y2 a
c 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 y1 a
b' forall a. AbelianGroup a => a -> a -> a
+ Mat x2 y2 a
d 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 y2 a
d')

  Mat x y a
x & Mat z x a
y = forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"mult:" forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"; " [forall (x :: Shape) (y :: Shape) a. Mat x y a -> [Char]
showR Mat x y a
x,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 = forall (f :: * -> *) a. Applicative f => a -> f a
pure 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) = 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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) = forall a. AbelianGroupZ a => a -> Mat 'Leaf 'Leaf a
one 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) = forall (y1 :: Shape) a (y2 :: Shape).
Mat 'Leaf y1 a -> Mat 'Leaf y2 a -> Mat 'Leaf ('Bin y1 y2) a
col forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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) = forall (s :: Shape) a (s' :: Shape).
Mat s 'Leaf a -> Mat s' 'Leaf a -> Mat ('Bin s s') 'Leaf a
row forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 = 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 forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero 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 = 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 = forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero forall a. a -> a -> Pair 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 = 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) = 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pair (Mat x1 x1 a)
x11 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Pair (Mat x2 x1 a)
x12 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Pair (Mat x1 x2 a)
x21 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 = 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 y2 a
a22 Mat x1 y2 (Pair a)
c21 Mat x1 y1 a
b11
                 x11 :: Pair (Mat x1 x1 a)
x11 = 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
a11 (Mat x2 y1 a
a12 forall a (x :: Shape) (y :: Shape) (z :: Shape).
RingP a =>
Mat x y a -> Mat z x a -> Mat z y (Pair a)
& forall a. Pair a -> a
rightOf Pair (Mat x1 x2 a)
x21 forall a. AbelianGroup a => a -> a -> a
+ Mat x1 y1 (Pair a)
c11) Mat x1 y1 a
b11
                 x22 :: Pair (Mat x2 x2 a)
x22 = 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 y2 a
a22 (forall a. Pair a -> a
leftOf  Pair (Mat x1 x2 a)
x21 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 y1 a
b12 forall a. AbelianGroup a => a -> a -> a
+ Mat x2 y2 (Pair a)
c22) Mat x2 y2 a
b22
                 x12 :: Pair (Mat x2 x1 a)
x12 = 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
a11 (Mat x2 y1 a
a12 forall a (x :: Shape) (y :: Shape) (z :: Shape).
RingP a =>
Mat x y a -> Mat z x a -> Mat z y (Pair a)
& forall a. Pair a -> a
rightOf Pair (Mat x2 x2 a)
x22 forall a. AbelianGroup a => a -> a -> a
+ forall a. Pair a -> a
leftOf Pair (Mat x1 x1 a)
x11 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 y1 a
b12 forall a. AbelianGroup a => a -> a -> a
+ Mat x2 y1 (Pair a)
c12) 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) = 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 forall (x :: Shape) (x' :: Shape) (y :: Shape) (y' :: Shape) a.
Mat ('Bin x x') ('Bin y y') a
q0 (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) (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 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 = 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 (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 forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero Mat x2 y2 a
a22) (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) 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) = forall (y1 :: Shape) a (y2 :: Shape).
Mat 'Leaf y1 a -> Mat 'Leaf y2 a -> Mat 'Leaf ('Bin y1 y2) a
col forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pair (Mat 'Leaf x1 a)
x1 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 = 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 y2 a
a22 Mat 'Leaf y2 (Pair a)
c2 forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero
                 x1 :: Pair (Mat 'Leaf x1 a)
x1 = 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
a11 (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 y1 a
a12 (forall a. Pair a -> a
rightOf Pair (Mat 'Leaf x2 a)
x2) forall a. AbelianGroup a => a -> a -> a
+ Mat 'Leaf y1 (Pair a)
c1) 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) = forall (s :: Shape) a (s' :: Shape).
Mat s 'Leaf a -> Mat s' 'Leaf a -> Mat ('Bin s s') 'Leaf a
row forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pair (Mat x1 'Leaf a)
x1 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 = 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 forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero Mat x1 'Leaf (Pair a)
c1 Mat x1 y1 a
b11
                 x2 :: Pair (Mat x2 'Leaf a)
x2 = 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 forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero (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 (forall a. Pair a -> a
leftOf Pair (Mat x1 'Leaf a)
x1) Mat x2 y1 a
b12 forall a. AbelianGroup a => a -> a -> a
+ Mat x2 'Leaf (Pair a)
c2) Mat x2 y2 a
b22
         close Mat x x a
a Mat y x (Pair a)
c Mat y y a
b = forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"closeDisjointP:" forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"; " [forall (x :: Shape) (y :: Shape) a. Mat x y a -> [Char]
showR Mat x x a
a,forall (x :: Shape) (y :: Shape) a. Mat x y a -> [Char]
showR Mat y x (Pair a)
c,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)
(&) = 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]
"("forall a. [a] -> [a] -> [a]
++forall (x :: Shape) (y :: Shape) a. Mat x y a -> [Char]
showR Mat x1 'Leaf a
aforall a. [a] -> [a] -> [a]
++[Char]
"-"forall a. [a] -> [a] -> [a]
++forall (x :: Shape) (y :: Shape) a. Mat x y a -> [Char]
showR Mat x2 'Leaf a
bforall a. [a] -> [a] -> [a]
++[Char]
")"
showR (Col Mat 'Leaf y1 a
a Mat 'Leaf y2 a
b) = [Char]
"("forall a. [a] -> [a] -> [a]
++forall (x :: Shape) (y :: Shape) a. Mat x y a -> [Char]
showR Mat 'Leaf y1 a
aforall a. [a] -> [a] -> [a]
++[Char]
"|"forall a. [a] -> [a] -> [a]
++forall (x :: Shape) (y :: Shape) a. Mat x y a -> [Char]
showR Mat 'Leaf y2 a
bforall 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]
"#("forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"," [forall (x :: Shape) (y :: Shape) a. Mat x y a -> [Char]
showR Mat x1 y1 a
a,forall (x :: Shape) (y :: Shape) a. Mat x y a -> [Char]
showR Mat x2 y1 a
b,forall (x :: Shape) (y :: Shape) a. Mat x y a -> [Char]
showR Mat x1 y2 a
c,forall (x :: Shape) (y :: Shape) a. Mat x y a -> [Char]
showR Mat x2 y2 a
d]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' = forall (s :: Shape) (s' :: Shape).
Int -> Shape' s -> Shape' s' -> Shape' ('Bin s s')
Bin' (forall (s :: Shape). Shape' s -> Int
sz' Shape' s
s forall a. AbelianGroup a => a -> a -> a
+ 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 = forall (s :: Shape). Shape' s -> SomeShape
S (forall (s :: Shape) (s' :: Shape).
Shape' s -> Shape' s' -> Shape' ('Bin s s')
bin' Shape' 'Leaf
Leaf' Shape' 'Leaf
Leaf')
mkShape Int
2 = forall (s :: Shape). Shape' s -> SomeShape
S (forall (s :: Shape) (s' :: Shape).
Shape' s -> Shape' s' -> Shape' ('Bin s s')
bin' (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) -> forall (s :: Shape). Shape' s -> SomeShape
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 forall a. Integral a => a -> a -> a
`div` Int
2
        n'2 :: Int
n'2 = Int
n forall a. Num a => a -> a -> a
- Int
n'1 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 = 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 forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero (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) forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero
mkSing Shape' x
Leaf' Shape' y
Leaf' a
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 = forall (y1 :: Shape) a (y2 :: Shape).
Mat 'Leaf y1 a -> Mat 'Leaf y2 a -> Mat 'Leaf ('Bin y1 y2) a
col forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero (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 = forall (s :: Shape) a (s' :: Shape).
Mat s 'Leaf a -> Mat s' 'Leaf a -> Mat ('Bin s s') 'Leaf a
row (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) 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' = forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero
mkUpDiag [a]
xs (Bin' Int
_ Shape' s
s Shape' s'
s') = 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 (forall a (s :: Shape).
AbelianGroupZ a =>
[a] -> Shape' s -> Mat s s a
mkUpDiag [a]
a Shape' s
s) (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) forall (x :: Shape) (y :: Shape) a. Mat x y a
Zero (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) = forall a. Int -> [a] -> ([a], [a])
splitAt (forall (s :: Shape). Shape' s -> Int
sz' Shape' s
s 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 = forall a. AbelianGroup a => a
zero
close Bool
p (One Pair a
x) = forall a. AbelianGroupZ a => a -> Mat 'Leaf 'Leaf a
one 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) = 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 (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 (forall a. Pair a -> a
leftOf Pair (Mat x1 x1 a)
x11) Mat x2 y1 (Pair a)
a12 (forall a. Pair a -> a
rightOf Pair (Mat x2 x2 a)
x22)) forall a. AbelianGroup a => a
zero Pair (Mat x2 x2 a)
x22
 where x11 :: Pair (Mat x1 x1 a)
x11 = 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 y1 (Pair a)
a11 
       x22 :: Pair (Mat x2 x2 a)
x22 = 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 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 (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Pair a]
xs) of
  S Shape' s
s -> forall (s :: Shape) a. Shape' s -> Pair (Mat s s a) -> SomeTri a
T Shape' s
s (forall a (s :: Shape).
RingP a =>
Bool -> Mat s s (Pair a) -> Pair (Mat s s a)
close Bool
True forall a b. (a -> b) -> a -> b
$ 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 = 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (Mat x1 y1 a)
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f (Mat x2 y1 a)
b forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f (Mat x1 y2 a)
c 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) = forall (s :: Shape) a. Shape' s -> Pair (Mat s s a) -> SomeTri a
T (forall (s :: Shape) (s' :: Shape).
Shape' s -> Shape' s' -> Shape' ('Bin s s')
bin' Shape' s
y Shape' s
x) (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 (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 (forall a. Pair a -> a
leftOf Pair (Mat s s a)
a) Mat s s (Pair a)
c' (forall a. Pair a -> a
rightOf Pair (Mat s s a)
b)) forall a. AbelianGroup a => a
zero Pair (Mat s s a)
b)
  where c' :: Mat s s (Pair a)
c' = 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 = 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) = 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 (forall (s :: Shape) a. Vec s a
Z forall (s :: Shape) a (s' :: Shape).
Vec s a -> Vec s' a -> Vec ('Bin s s') a
:! forall (s :: Shape) a. Vec s a
Z) (Vec s b
a 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 = 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 forall (s :: Shape) a (s' :: Shape).
Vec s a -> Vec s' a -> Vec ('Bin s s') a
:! Vec s' a
b) (forall (s :: Shape) a. Vec s a
Z forall (s :: Shape) a (s' :: Shape).
Vec s a -> Vec s' a -> Vec ('Bin s s') a
:! forall (s :: Shape) a. Vec s a
Z)
zw a -> b -> c
f Vec y a
Z (O b
x) = forall a. a -> Vec 'Leaf a
O forall a b. (a -> b) -> a -> b
$ a -> b -> c
f forall a. AbelianGroup a => a
zero b
x
zw a -> b -> c
f (O a
x) Vec y b
Z = forall a. a -> Vec 'Leaf a
O forall a b. (a -> b) -> a -> b
$ a -> b -> c
f a
x forall a. AbelianGroup a => a
zero
zw a -> b -> c
f (O a
x) (O b
y) = 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') = 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
a' forall (s :: Shape) a (s' :: Shape).
Vec s a -> Vec s' a -> Vec ('Bin s s') 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 -> b -> c
f Vec s' a
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 = 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 forall a. Ord a => a -> a -> Bool
< forall (s :: Shape). Shape' s -> Int
sz' Shape' s
s  = forall a (x :: Shape).
AbelianGroup a =>
Int -> Shape' x -> Vec x a -> a
lk Int
i Shape' s
s Vec s a
x
  | Bool
otherwise = forall a (x :: Shape).
AbelianGroup a =>
Int -> Shape' x -> Vec x a -> a
lk (Int
i forall a. Num a => a -> a -> a
- forall (s :: Shape). Shape' s -> Int
sz' Shape' s
s) Shape' s'
s' 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 = forall (s :: Shape) a. Vec s a
Z
lin' (One a
a) = forall a. a -> Vec 'Leaf a
O (forall a. a -> Vec 'Leaf a
O a
a)
lin' (Row Mat x1 'Leaf a
a Mat x2 'Leaf a
b) = forall a b c (y :: Shape).
(AbelianGroup a, AbelianGroup b) =>
(a -> b -> c) -> Vec y a -> Vec y b -> Vec y c
zw forall (s :: Shape) a (s' :: Shape).
Vec s a -> Vec s' a -> Vec ('Bin s s') a
(:!) (forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Mat x y a -> Vec y (Vec x a)
lin' Mat x1 'Leaf a
a) (forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Mat x y a -> Vec y (Vec x a)
lin' Mat x2 'Leaf a
b)
lin' (Col Mat 'Leaf y1 a
a Mat 'Leaf y2 a
b) = forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Mat x y a -> Vec y (Vec x a)
lin' Mat 'Leaf y1 a
a forall (s :: Shape) a (s' :: Shape).
Vec s a -> Vec s' a -> Vec ('Bin s s') a
:! forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Mat x y a -> Vec y (Vec x a)
lin' 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) = forall a b c (y :: Shape).
(AbelianGroup a, AbelianGroup b) =>
(a -> b -> c) -> Vec y a -> Vec y b -> Vec y c
zw forall (s :: Shape) a (s' :: Shape).
Vec s a -> Vec s' a -> Vec ('Bin s s') a
(:!) (forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Mat x y a -> Vec y (Vec x a)
lin' Mat x1 y1 a
a) (forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Mat x y a -> Vec y (Vec x a)
lin' Mat x2 y1 a
b) forall (s :: Shape) a (s' :: Shape).
Vec s a -> Vec s' a -> Vec ('Bin s s') a
:!forall a b c (y :: Shape).
(AbelianGroup a, AbelianGroup b) =>
(a -> b -> c) -> Vec y a -> Vec y b -> Vec y c
zw forall (s :: Shape) a (s' :: Shape).
Vec s a -> Vec s' a -> Vec ('Bin s s') a
(:!) (forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Mat x y a -> Vec y (Vec x a)
lin' Mat x1 y2 a
c) (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') = forall (x :: Shape) a. Shape' x -> Vec x a -> [(Int, a)]
contents Shape' s
s Vec s a
xs forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (forall {t} {a} {b}. (t -> a) -> (t, b) -> (a, b)
first (forall a. AbelianGroup a => a -> a -> a
+forall (s :: Shape). Shape' s -> Int
sz' Shape' s
s)) (forall (x :: Shape) a. Shape' x -> Vec x a -> [(Int, a)]
contents Shape' s'
s' 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 = forall (s :: Shape) a. Vec s a
Z
  + :: 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 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 =  (forall {t} {b} {a}. (t -> b) -> (a, t) -> (a, b)
second forall (s :: Shape) (s' :: Shape). Path s -> Path ('Bin s' s)
High forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (a, Path x')
y) forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (forall {t} {b} {a}. (t -> b) -> (a, t) -> (a, b)
second forall (s :: Shape) (s' :: Shape). Path s -> Path ('Bin s s')
Low 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 = forall a. Maybe a
Nothing
rightmostOnLine Path y
Here (One a
x) = forall a. a -> Maybe a
Just (a
x,Path 'Leaf
Here)
rightmostOnLine Path y
Here (Row Mat x1 'Leaf a
a Mat x2 'Leaf a
b)    = 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 forall a (x :: Shape) (x' :: Shape).
Maybe (a, Path x)
-> Maybe (a, Path x') -> Maybe (a, Path ('Bin x x'))
<||> 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) = forall (y :: Shape) (x :: Shape) a.
Path y -> Mat x y a -> Maybe (a, Path x)
rightmostOnLine Path s
p Mat 'Leaf y1 a
a
rightmostOnLine (High Path s
p) (Col Mat 'Leaf y1 a
a Mat 'Leaf y2 a
b) = forall (y :: Shape) (x :: Shape) a.
Path y -> Mat x y a -> Maybe (a, Path x)
rightmostOnLine Path s
p 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
_) = forall (y :: Shape) (x :: Shape) a.
Path y -> Mat x y a -> Maybe (a, Path x)
rightmostOnLine Path s
p Mat x1 y1 a
a forall a (x :: Shape) (x' :: Shape).
Maybe (a, Path x)
-> Maybe (a, Path x') -> Maybe (a, Path ('Bin x x'))
<||> forall (y :: Shape) (x :: Shape) a.
Path y -> Mat x y a -> Maybe (a, Path x)
rightmostOnLine Path s
p 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) = forall (y :: Shape) (x :: Shape) a.
Path y -> Mat x y a -> Maybe (a, Path x)
rightmostOnLine Path s
p Mat x1 y2 a
a forall a (x :: Shape) (x' :: Shape).
Maybe (a, Path x)
-> Maybe (a, Path x') -> Maybe (a, Path ('Bin x x'))
<||> forall (y :: Shape) (x :: Shape) a.
Path y -> Mat x y a -> Maybe (a, Path x)
rightmostOnLine Path s
p 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) = 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 | forall (x :: Shape). Path x -> Bool
isRightmost Path y
y = []
             | Bool
otherwise = (Path y
y,a
a,Path y
x) forall a. a -> [a] -> [a]
: 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) = 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')) = [(forall (y :: Shape). Shape' y -> Path y -> Int
fromPath Shape' s
s Path s
x,a
a,forall (y :: Shape). Shape' y -> Path y -> Int
fromPath Shape' s
s Path s
y) | (Path s
x,a
a,Path s
y) <- forall a (y :: Shape).
AbelianGroup a =>
Mat y y a -> Path y -> [(Path y, a, Path y)]
results' (Mat s s a
mforall a. AbelianGroup a => a -> a -> a
+Mat s s a
m') (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 'Leaf
Here
leftMost (Bin' Int
_ Shape' s
s Shape' s'
_) = forall (s :: Shape) (s' :: Shape). Path s -> Path ('Bin s s')
Low forall a b. (a -> b) -> a -> b
$ 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) = forall (y :: Shape). Shape' y -> Path y -> Int
fromPath Shape' s
s Path s
x
fromPath (Bin' Int
_ Shape' s
s Shape' s'
s') (High Path s
x) = forall (s :: Shape). Shape' s -> Int
sz' Shape' s
s forall a. AbelianGroup a => a -> a -> a
+ forall (y :: Shape). Shape' y -> Path y -> Int
fromPath Shape' s'
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 = 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
_) = 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
_) = 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) = 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')) = forall a (x :: Shape) (y :: Shape).
AbelianGroup a =>
Mat x y a -> a
root' Mat s s p
m forall a. AbelianGroup a => a -> a -> a
+ 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 = forall (s :: Shape) a. Shape' s -> Pair (Mat s s a) -> SomeTri a
T Shape' 'Leaf
Leaf' (forall a. AbelianGroupZ a => a -> Mat 'Leaf 'Leaf a
one forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pair a
x)

square2 :: Pair a -> SomeTri a
square2 Pair a
x = forall (s :: Shape) a. Shape' s -> Pair (Mat s s a) -> SomeTri a
T (forall (s :: Shape) (s' :: Shape).
Shape' s -> Shape' s' -> Shape' ('Bin s s')
bin' Shape' 'Leaf
Leaf' Shape' 'Leaf
Leaf') forall a b. (a -> b) -> a -> b
$ 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' forall a. AbelianGroup a => a
zero (forall a. AbelianGroupZ a => a -> Mat 'Leaf 'Leaf a
one forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pair a
x) forall a. AbelianGroup a => a
zero forall a. AbelianGroup a => a
zero

square3 :: Bool -> Pair a -> Pair a -> SomeTri a
square3 Bool
p Pair a
x Pair a
y = forall (s :: Shape) a. Shape' s -> Pair (Mat s s a) -> SomeTri a
T (forall (s :: Shape) (s' :: Shape).
Shape' s -> Shape' s' -> Shape' ('Bin s s')
bin' (forall (s :: Shape) (s' :: Shape).
Shape' s -> Shape' s' -> Shape' ('Bin s s')
bin' Shape' 'Leaf
Leaf' Shape' 'Leaf
Leaf') (Shape' 'Leaf
Leaf')) 
  (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' (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' forall a. AbelianGroup a => a
zero (forall a. AbelianGroupZ a => a -> Mat 'Leaf 'Leaf a
one forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pair a
x) forall a. AbelianGroup a => a
zero forall a. AbelianGroup a => a
zero) (forall (y1 :: Shape) a (y2 :: Shape).
Mat 'Leaf y1 a -> Mat 'Leaf y2 a -> Mat 'Leaf ('Bin y1 y2) a
Col forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a. AbelianGroupZ a => a -> Mat 'Leaf 'Leaf a
one forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. RingP a => Bool -> a -> a -> Pair a
mul Bool
p (forall a. Pair a -> a
leftOf Pair a
x) (forall a. Pair a -> a
rightOf Pair a
y)) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall a. AbelianGroupZ a => a -> Mat 'Leaf 'Leaf a
one forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pair a
y)) forall a. AbelianGroup a => a
zero 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]]
(|+|) = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall 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 = forall a. Int -> a -> [a]
replicate (forall (s :: Shape). Shape' s -> Int
sz' Shape' y
y) forall a b. (a -> b) -> a -> b
$ forall a. Int -> a -> [a]
replicate (forall (s :: Shape). Shape' s -> Int
sz' Shape' x
x) 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) = (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 x1 y1 a
a forall {a}. [[a]] -> [[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 x2 y1 a
b) forall a. [a] -> [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 x1 y2 a
c forall {a}. [[a]] -> [[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 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) = 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 y1 a
a forall a. [a] -> [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 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) = (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 x1 'Leaf a
a) forall {a}. [[a]] -> [[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 x2 'Leaf a
b)

fingerprint :: SomeTri a -> [[Char]]
fingerprint (T Shape' s
s (Mat s s a
m :/: Mat s s a
m')) = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall {a} {a}.
(AbelianGroupZ a, AbelianGroupZ a) =>
a -> a -> Char
c) (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) (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 (forall a. AbelianGroupZ a => a -> Bool
isZero a
x,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'