-- | Exterior monomials where the variable set 
-- looks like @{x_1, x_2, ... , x_N}@ 
--
-- The internal representation is a bit vector

{-# LANGUAGE 
      CPP, BangPatterns, TypeFamilies, DataKinds, KindSignatures, ScopedTypeVariables,
      FlexibleContexts
  #-}
module Math.Algebra.Polynomial.Monomial.Exterior.Indexed where

--------------------------------------------------------------------------------

import Data.Maybe
import Data.List
import Data.Array.Unboxed 
import Data.Ord
import Data.Bits

import Data.Typeable
import GHC.TypeLits
import Data.Proxy

import Data.Foldable as F 

import qualified Data.Set as Set ; import Data.Set (Set)   -- IntSet and
import qualified Data.Map as Map ; import Data.Map (Map)   -- IntMap would be more efficient

import Math.Algebra.Polynomial.Class
import Math.Algebra.Polynomial.Pretty
import Math.Algebra.Polynomial.Misc

import Math.Algebra.Polynomial.FreeModule ( PartialMonoid(..) )

--------------------------------------------------------------------------------
-- * Exterior monomials

-- | Exterior monomials of the variables @x1,x2,...,xn@. The internal representation is 
-- a bit vector encoded as an @Integer@
newtype Ext (var :: Symbol) (n :: Nat) = Ext Integer deriving (Ext var n -> Ext var n -> Bool
(Ext var n -> Ext var n -> Bool)
-> (Ext var n -> Ext var n -> Bool) -> Eq (Ext var n)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (var :: Symbol) (n :: Nat). Ext var n -> Ext var n -> Bool
/= :: Ext var n -> Ext var n -> Bool
$c/= :: forall (var :: Symbol) (n :: Nat). Ext var n -> Ext var n -> Bool
== :: Ext var n -> Ext var n -> Bool
$c== :: forall (var :: Symbol) (n :: Nat). Ext var n -> Ext var n -> Bool
Eq,Eq (Ext var n)
Eq (Ext var n)
-> (Ext var n -> Ext var n -> Ordering)
-> (Ext var n -> Ext var n -> Bool)
-> (Ext var n -> Ext var n -> Bool)
-> (Ext var n -> Ext var n -> Bool)
-> (Ext var n -> Ext var n -> Bool)
-> (Ext var n -> Ext var n -> Ext var n)
-> (Ext var n -> Ext var n -> Ext var n)
-> Ord (Ext var n)
Ext var n -> Ext var n -> Bool
Ext var n -> Ext var n -> Ordering
Ext var n -> Ext var n -> Ext var n
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall (var :: Symbol) (n :: Nat). Eq (Ext var n)
forall (var :: Symbol) (n :: Nat). Ext var n -> Ext var n -> Bool
forall (var :: Symbol) (n :: Nat).
Ext var n -> Ext var n -> Ordering
forall (var :: Symbol) (n :: Nat).
Ext var n -> Ext var n -> Ext var n
min :: Ext var n -> Ext var n -> Ext var n
$cmin :: forall (var :: Symbol) (n :: Nat).
Ext var n -> Ext var n -> Ext var n
max :: Ext var n -> Ext var n -> Ext var n
$cmax :: forall (var :: Symbol) (n :: Nat).
Ext var n -> Ext var n -> Ext var n
>= :: Ext var n -> Ext var n -> Bool
$c>= :: forall (var :: Symbol) (n :: Nat). Ext var n -> Ext var n -> Bool
> :: Ext var n -> Ext var n -> Bool
$c> :: forall (var :: Symbol) (n :: Nat). Ext var n -> Ext var n -> Bool
<= :: Ext var n -> Ext var n -> Bool
$c<= :: forall (var :: Symbol) (n :: Nat). Ext var n -> Ext var n -> Bool
< :: Ext var n -> Ext var n -> Bool
$c< :: forall (var :: Symbol) (n :: Nat). Ext var n -> Ext var n -> Bool
compare :: Ext var n -> Ext var n -> Ordering
$ccompare :: forall (var :: Symbol) (n :: Nat).
Ext var n -> Ext var n -> Ordering
$cp1Ord :: forall (var :: Symbol) (n :: Nat). Eq (Ext var n)
Ord,Int -> Ext var n -> ShowS
[Ext var n] -> ShowS
Ext var n -> String
(Int -> Ext var n -> ShowS)
-> (Ext var n -> String)
-> ([Ext var n] -> ShowS)
-> Show (Ext var n)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (var :: Symbol) (n :: Nat). Int -> Ext var n -> ShowS
forall (var :: Symbol) (n :: Nat). [Ext var n] -> ShowS
forall (var :: Symbol) (n :: Nat). Ext var n -> String
showList :: [Ext var n] -> ShowS
$cshowList :: forall (var :: Symbol) (n :: Nat). [Ext var n] -> ShowS
show :: Ext var n -> String
$cshow :: forall (var :: Symbol) (n :: Nat). Ext var n -> String
showsPrec :: Int -> Ext var n -> ShowS
$cshowsPrec :: forall (var :: Symbol) (n :: Nat). Int -> Ext var n -> ShowS
Show)

-- | Signed exterior monomial
data SgnExt (var :: Symbol) (n :: Nat) = SgnExt !Sign !(Ext var n) deriving (SgnExt var n -> SgnExt var n -> Bool
(SgnExt var n -> SgnExt var n -> Bool)
-> (SgnExt var n -> SgnExt var n -> Bool) -> Eq (SgnExt var n)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (var :: Symbol) (n :: Nat).
SgnExt var n -> SgnExt var n -> Bool
/= :: SgnExt var n -> SgnExt var n -> Bool
$c/= :: forall (var :: Symbol) (n :: Nat).
SgnExt var n -> SgnExt var n -> Bool
== :: SgnExt var n -> SgnExt var n -> Bool
$c== :: forall (var :: Symbol) (n :: Nat).
SgnExt var n -> SgnExt var n -> Bool
Eq,Eq (SgnExt var n)
Eq (SgnExt var n)
-> (SgnExt var n -> SgnExt var n -> Ordering)
-> (SgnExt var n -> SgnExt var n -> Bool)
-> (SgnExt var n -> SgnExt var n -> Bool)
-> (SgnExt var n -> SgnExt var n -> Bool)
-> (SgnExt var n -> SgnExt var n -> Bool)
-> (SgnExt var n -> SgnExt var n -> SgnExt var n)
-> (SgnExt var n -> SgnExt var n -> SgnExt var n)
-> Ord (SgnExt var n)
SgnExt var n -> SgnExt var n -> Bool
SgnExt var n -> SgnExt var n -> Ordering
SgnExt var n -> SgnExt var n -> SgnExt var n
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall (var :: Symbol) (n :: Nat). Eq (SgnExt var n)
forall (var :: Symbol) (n :: Nat).
SgnExt var n -> SgnExt var n -> Bool
forall (var :: Symbol) (n :: Nat).
SgnExt var n -> SgnExt var n -> Ordering
forall (var :: Symbol) (n :: Nat).
SgnExt var n -> SgnExt var n -> SgnExt var n
min :: SgnExt var n -> SgnExt var n -> SgnExt var n
$cmin :: forall (var :: Symbol) (n :: Nat).
SgnExt var n -> SgnExt var n -> SgnExt var n
max :: SgnExt var n -> SgnExt var n -> SgnExt var n
$cmax :: forall (var :: Symbol) (n :: Nat).
SgnExt var n -> SgnExt var n -> SgnExt var n
>= :: SgnExt var n -> SgnExt var n -> Bool
$c>= :: forall (var :: Symbol) (n :: Nat).
SgnExt var n -> SgnExt var n -> Bool
> :: SgnExt var n -> SgnExt var n -> Bool
$c> :: forall (var :: Symbol) (n :: Nat).
SgnExt var n -> SgnExt var n -> Bool
<= :: SgnExt var n -> SgnExt var n -> Bool
$c<= :: forall (var :: Symbol) (n :: Nat).
SgnExt var n -> SgnExt var n -> Bool
< :: SgnExt var n -> SgnExt var n -> Bool
$c< :: forall (var :: Symbol) (n :: Nat).
SgnExt var n -> SgnExt var n -> Bool
compare :: SgnExt var n -> SgnExt var n -> Ordering
$ccompare :: forall (var :: Symbol) (n :: Nat).
SgnExt var n -> SgnExt var n -> Ordering
$cp1Ord :: forall (var :: Symbol) (n :: Nat). Eq (SgnExt var n)
Ord,Int -> SgnExt var n -> ShowS
[SgnExt var n] -> ShowS
SgnExt var n -> String
(Int -> SgnExt var n -> ShowS)
-> (SgnExt var n -> String)
-> ([SgnExt var n] -> ShowS)
-> Show (SgnExt var n)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (var :: Symbol) (n :: Nat). Int -> SgnExt var n -> ShowS
forall (var :: Symbol) (n :: Nat). [SgnExt var n] -> ShowS
forall (var :: Symbol) (n :: Nat). SgnExt var n -> String
showList :: [SgnExt var n] -> ShowS
$cshowList :: forall (var :: Symbol) (n :: Nat). [SgnExt var n] -> ShowS
show :: SgnExt var n -> String
$cshow :: forall (var :: Symbol) (n :: Nat). SgnExt var n -> String
showsPrec :: Int -> SgnExt var n -> ShowS
$cshowsPrec :: forall (var :: Symbol) (n :: Nat). Int -> SgnExt var n -> ShowS
Show)

unExt :: Ext v n -> Integer
unExt :: Ext v n -> Integer
unExt (Ext Integer
k) = Integer
k

instance KnownNat n => PartialMonoid (SgnExt var n) where
  pmUnit :: SgnExt var n
pmUnit = SgnExt var n
forall (n :: Nat) (var :: Symbol). KnownNat n => SgnExt var n
emptySgnExt
  pmAdd :: SgnExt var n -> SgnExt var n -> Maybe (SgnExt var n)
pmAdd  = SgnExt var n -> SgnExt var n -> Maybe (SgnExt var n)
forall (n :: Nat) (var :: Symbol).
KnownNat n =>
SgnExt var n -> SgnExt var n -> Maybe (SgnExt var n)
mulSgnExt   

instance KnownSymbol var => Pretty (Ext var n) where 
  pretty :: Ext var n -> String
pretty Ext var n
monom =   
    case [ Index -> String
showX Index
i | Index
i <- Ext var n -> [Index]
forall (v :: Symbol) (n :: Nat). Ext v n -> [Index]
extToList Ext var n
monom ] of 
      [] -> String
"(1)"
      [String]
xs -> String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"/\\" [String]
xs
    where
      v :: String
v = Ext var n -> String
forall (var :: Symbol) (n :: Nat).
KnownSymbol var =>
Ext var n -> String
extVar Ext var n
monom
      showX :: Index -> String
showX !(Index Int
i) = String
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i

instance KnownSymbol var => Pretty (SgnExt var n) where 
  pretty :: SgnExt var n -> String
pretty (SgnExt Sign
sgn Ext var n
ext) = case Sign
sgn of
    Sign
Plus  -> Char
'+' Char -> ShowS
forall a. a -> [a] -> [a]
: Ext var n -> String
forall a. Pretty a => a -> String
pretty Ext var n
ext
    Sign
Minus -> Char
'-' Char -> ShowS
forall a. a -> [a] -> [a]
: Ext var n -> String
forall a. Pretty a => a -> String
pretty Ext var n
ext

-- | Name of the variables
extVar :: KnownSymbol var => Ext var n -> String
extVar :: Ext var n -> String
extVar = Proxy var -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (Proxy var -> String)
-> (Ext var n -> Proxy var) -> Ext var n -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ext var n -> Proxy var
forall (var :: Symbol) (n :: Nat). Ext var n -> Proxy var
varProxy where
  varProxy :: Ext var n -> Proxy var
  varProxy :: Ext var n -> Proxy var
varProxy Ext var n
_ = Proxy var
forall k (t :: k). Proxy t
Proxy

-- | Number of variables
nOfExt :: KnownNat n => Ext var n -> Int
nOfExt :: Ext var n -> Int
nOfExt = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> (Ext var n -> Integer) -> Ext var n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n -> Integer)
-> (Ext var n -> Proxy n) -> Ext var n -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ext var n -> Proxy n
forall (var :: Symbol) (n :: Nat). Ext var n -> Proxy n
natProxy where
  natProxy :: Ext var n -> Proxy n
  natProxy :: Ext var n -> Proxy n
natProxy Ext var n
_ = Proxy n
forall k (t :: k). Proxy t
Proxy

nOfMbExt :: KnownNat n => Maybe (Ext var n) -> Int
nOfMbExt :: Maybe (Ext var n) -> Int
nOfMbExt = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int)
-> (Maybe (Ext var n) -> Integer) -> Maybe (Ext var n) -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n -> Integer)
-> (Maybe (Ext var n) -> Proxy n) -> Maybe (Ext var n) -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe (Ext var n) -> Proxy n
forall (var :: Symbol) (n :: Nat). Maybe (Ext var n) -> Proxy n
natProxy where
  natProxy :: Maybe (Ext var n) -> Proxy n
  natProxy :: Maybe (Ext var n) -> Proxy n
natProxy Maybe (Ext var n)
_ = Proxy n
forall k (t :: k). Proxy t
Proxy

nOfSgnExt :: KnownNat n => SgnExt var n -> Int
nOfSgnExt :: SgnExt var n -> Int
nOfSgnExt = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int)
-> (SgnExt var n -> Integer) -> SgnExt var n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n -> Integer)
-> (SgnExt var n -> Proxy n) -> SgnExt var n -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SgnExt var n -> Proxy n
forall (var :: Symbol) (n :: Nat). SgnExt var n -> Proxy n
natProxy where
  natProxy :: SgnExt var n -> Proxy n
  natProxy :: SgnExt var n -> Proxy n
natProxy SgnExt var n
_ = Proxy n
forall k (t :: k). Proxy t
Proxy

nOfMbSgnExt :: KnownNat n => Maybe (SgnExt var n) -> Int
nOfMbSgnExt :: Maybe (SgnExt var n) -> Int
nOfMbSgnExt = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int)
-> (Maybe (SgnExt var n) -> Integer) -> Maybe (SgnExt var n) -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n -> Integer)
-> (Maybe (SgnExt var n) -> Proxy n)
-> Maybe (SgnExt var n)
-> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe (SgnExt var n) -> Proxy n
forall (var :: Symbol) (n :: Nat). Maybe (SgnExt var n) -> Proxy n
natProxy where
  natProxy :: Maybe (SgnExt var n) -> Proxy n
  natProxy :: Maybe (SgnExt var n) -> Proxy n
natProxy Maybe (SgnExt var n)
_ = Proxy n
forall k (t :: k). Proxy t
Proxy

--------------------------------------------------------------------------------
-- * emptyness

emptyExt :: KnownNat n => Ext v n
emptyExt :: Ext v n
emptyExt = Integer -> Ext v n
forall (var :: Symbol) (n :: Nat). Integer -> Ext var n
Ext Integer
0

emptySgnExt :: KnownNat n => SgnExt v n
emptySgnExt :: SgnExt v n
emptySgnExt = Sign -> Ext v n -> SgnExt v n
forall (var :: Symbol) (n :: Nat).
Sign -> Ext var n -> SgnExt var n
SgnExt Sign
Plus (Integer -> Ext v n
forall (var :: Symbol) (n :: Nat). Integer -> Ext var n
Ext Integer
0)

isEmptyExt :: Ext v n -> Bool
isEmptyExt :: Ext v n -> Bool
isEmptyExt (Ext Integer
a) = (Integer
aInteger -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
==Integer
0)

--------------------------------------------------------------------------------
-- * normalization

isNormalExt :: KnownNat n => Ext v n -> Bool
isNormalExt :: Ext v n -> Bool
isNormalExt ext :: Ext v n
ext@(Ext Integer
int) = Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shiftR Integer
int Int
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 where n :: Int
n = Ext v n -> Int
forall (n :: Nat) (var :: Symbol). KnownNat n => Ext var n -> Int
nOfExt Ext v n
ext

--------------------------------------------------------------------------------
-- * conversion

extFromList :: KnownNat n => [Index] -> Maybe (SgnExt v n)
extFromList :: [Index] -> Maybe (SgnExt v n)
extFromList [Index]
list = Maybe (SgnExt v n)
result where
  result :: Maybe (SgnExt v n)
result
    | Map Index Integer -> Bool
forall k a. Map k a -> Bool
Map.null Map Index Integer
multiset                     = SgnExt v n -> Maybe (SgnExt v n)
forall a. a -> Maybe a
Just SgnExt v n
forall (n :: Nat) (var :: Symbol). KnownNat n => SgnExt var n
emptySgnExt
    | (Index, Integer) -> Index
forall a b. (a, b) -> a
fst (Map Index Integer -> (Index, Integer)
forall k a. Map k a -> (k, a)
Map.findMin Map Index Integer
multiset) Index -> Index -> Bool
forall a. Ord a => a -> a -> Bool
< Int -> Index
Index Int
1  = String -> Maybe (SgnExt v n)
forall a. HasCallStack => String -> a
error String
"extFromList: index out of bounds (too small)"
    | (Index, Integer) -> Index
forall a b. (a, b) -> a
fst (Map Index Integer -> (Index, Integer)
forall k a. Map k a -> (k, a)
Map.findMax Map Index Integer
multiset) Index -> Index -> Bool
forall a. Ord a => a -> a -> Bool
> Int -> Index
Index Int
n  = Maybe (SgnExt v n)
forall a. Maybe a
Nothing  -- should this be an error ?
    | (Integer -> Bool) -> [Integer] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>Integer
1) (Map Index Integer -> [Integer]
forall k a. Map k a -> [a]
Map.elems Map Index Integer
multiset)         = Maybe (SgnExt v n)
forall a. Maybe a
Nothing
    | Bool
otherwise                             = SgnExt v n -> Maybe (SgnExt v n)
forall a. a -> Maybe a
Just (Sign -> Ext v n -> SgnExt v n
forall (var :: Symbol) (n :: Nat).
Sign -> Ext var n -> SgnExt var n
SgnExt Sign
sgn (Ext v n -> SgnExt v n) -> Ext v n -> SgnExt v n
forall a b. (a -> b) -> a -> b
$ Integer -> Ext v n
forall (var :: Symbol) (n :: Nat). Integer -> Ext var n
Ext Integer
int)
  n :: Int
n = Maybe (SgnExt v n) -> Int
forall (n :: Nat) (var :: Symbol).
KnownNat n =>
Maybe (SgnExt var n) -> Int
nOfMbSgnExt Maybe (SgnExt v n)
result
  multiset :: Map Index Integer
multiset = (Integer -> Integer -> Integer)
-> [(Index, Integer)] -> Map Index Integer
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) [ (Index
idx,Integer
1) | Index
idx <- [Index]
list ] 
  perm :: Permutation
perm = [Index] -> Permutation
forall a. Ord a => [a] -> Permutation
sortingPermutationAsc [Index]
list
  sgn :: Sign
sgn = if Int -> Bool
forall a. Integral a => a -> Bool
odd (Permutation -> Int
numberOfInversionsMerge Permutation
perm) then Sign
Minus else Sign
Plus
  int :: Integer
int = [Integer] -> Integer
forall a. Num a => [a] -> a
sum' [ Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shiftL Integer
1 (Int
jInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) | Index Int
j <- Map Index Integer -> [Index]
forall k a. Map k a -> [k]
Map.keys Map Index Integer
multiset ]

extToList :: Ext v n -> [Index]
extToList :: Ext v n -> [Index]
extToList (Ext Integer
int) = Int -> Integer -> [Index]
forall a. (Num a, Bits a) => Int -> a -> [Index]
go Int
0 Integer
int where
  go :: Int -> a -> [Index]
go Int
_   a
0 = []
  go !Int
i !a
a = if a -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit a
a Int
0 
    then Int -> Index
Index (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Index -> [Index] -> [Index]
forall a. a -> [a] -> [a]
: Int -> a -> [Index]
go (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (a -> Int -> a
forall a. Bits a => a -> Int -> a
shiftR a
a Int
1)
    else               Int -> a -> [Index]
go (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (a -> Int -> a
forall a. Bits a => a -> Int -> a
shiftR a
a Int
1)

extFromSet :: KnownNat n => Set Index -> Maybe (Ext v n)
extFromSet :: Set Index -> Maybe (Ext v n)
extFromSet Set Index
set = Maybe (Ext v n)
result where
  n :: Int
n = Maybe (Ext v n) -> Int
forall (n :: Nat) (var :: Symbol).
KnownNat n =>
Maybe (Ext var n) -> Int
nOfMbExt Maybe (Ext v n)
result
  result :: Maybe (Ext v n)
result = case Set Index -> Maybe Index
forall a. Set a -> Maybe a
Set.lookupMax Set Index
set of
    Maybe Index
Nothing        -> Ext v n -> Maybe (Ext v n)
forall a. a -> Maybe a
Just Ext v n
forall (n :: Nat) (v :: Symbol). KnownNat n => Ext v n
emptyExt
    Just (Index Int
k) -> if Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
n
      then Maybe (Ext v n)
forall a. Maybe a
Nothing   -- should this be an error ?
      else if (Set Index -> Index
forall a. Set a -> a
Set.findMin Set Index
set Index -> Index -> Bool
forall a. Ord a => a -> a -> Bool
< Int -> Index
Index Int
1)
        then String -> Maybe (Ext v n)
forall a. HasCallStack => String -> a
error String
"extFromSet: index smaller than 1"
        else Ext v n -> Maybe (Ext v n)
forall a. a -> Maybe a
Just (Ext v n -> Maybe (Ext v n)) -> Ext v n -> Maybe (Ext v n)
forall a b. (a -> b) -> a -> b
$ Integer -> Ext v n
forall (var :: Symbol) (n :: Nat). Integer -> Ext var n
Ext (Integer -> Ext v n) -> Integer -> Ext v n
forall a b. (a -> b) -> a -> b
$ [Integer] -> Integer
forall a. Num a => [a] -> a
sum' [ Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shiftL Integer
1 (Int
jInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) | Index Int
j <- Set Index -> [Index]
forall a. Set a -> [a]
Set.toList Set Index
set ]
  
extToSet :: Ext v n -> Set Index
extToSet :: Ext v n -> Set Index
extToSet = [Index] -> Set Index
forall a. Ord a => [a] -> Set a
Set.fromList ([Index] -> Set Index)
-> (Ext v n -> [Index]) -> Ext v n -> Set Index
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ext v n -> [Index]
forall (v :: Symbol) (n :: Nat). Ext v n -> [Index]
extToList

--------------------------------------------------------------------------------
-- * creation

variableExt :: KnownNat n => Index -> Ext v n 
variableExt :: Index -> Ext v n
variableExt (Index Int
idx) = Integer -> Ext v n
forall (var :: Symbol) (n :: Nat). Integer -> Ext var n
Ext (Integer -> Ext v n) -> Integer -> Ext v n
forall a b. (a -> b) -> a -> b
$ Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shiftL Integer
1 (Int
idxInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)

--------------------------------------------------------------------------------
-- * multiplication

mulExt :: KnownNat n => Ext v n -> Ext v n -> Maybe (SgnExt v n)
mulExt :: Ext v n -> Ext v n -> Maybe (SgnExt v n)
mulExt Ext v n
x Ext v n
y = [Index] -> Maybe (SgnExt v n)
forall (n :: Nat) (v :: Symbol).
KnownNat n =>
[Index] -> Maybe (SgnExt v n)
extFromList (Ext v n -> [Index]
forall (v :: Symbol) (n :: Nat). Ext v n -> [Index]
extToList Ext v n
x [Index] -> [Index] -> [Index]
forall a. [a] -> [a] -> [a]
++ Ext v n -> [Index]
forall (v :: Symbol) (n :: Nat). Ext v n -> [Index]
extToList Ext v n
y)

mulExtCoeff :: (Num c, KnownNat n) => Ext v n -> Ext v n -> Maybe (Ext v n, c)
mulExtCoeff :: Ext v n -> Ext v n -> Maybe (Ext v n, c)
mulExtCoeff Ext v n
x Ext v n
y = case Ext v n -> Ext v n -> Maybe (SgnExt v n)
forall (n :: Nat) (v :: Symbol).
KnownNat n =>
Ext v n -> Ext v n -> Maybe (SgnExt v n)
mulExt Ext v n
x Ext v n
y of
  Maybe (SgnExt v n)
Nothing             -> Maybe (Ext v n, c)
forall a. Maybe a
Nothing
  Just (SgnExt Sign
sgn Ext v n
z) -> case Sign
sgn of
    Sign
Plus  -> (Ext v n, c) -> Maybe (Ext v n, c)
forall a. a -> Maybe a
Just (Ext v n
z,  c
1)
    Sign
Minus -> (Ext v n, c) -> Maybe (Ext v n, c)
forall a. a -> Maybe a
Just (Ext v n
z, -c
1)

mulSgnExt :: KnownNat n => SgnExt v n -> SgnExt v n -> Maybe (SgnExt v n)
mulSgnExt :: SgnExt v n -> SgnExt v n -> Maybe (SgnExt v n)
mulSgnExt (SgnExt Sign
s Ext v n
x) (SgnExt Sign
t Ext v n
y) = case Ext v n -> Ext v n -> Maybe (SgnExt v n)
forall (n :: Nat) (v :: Symbol).
KnownNat n =>
Ext v n -> Ext v n -> Maybe (SgnExt v n)
mulExt Ext v n
x Ext v n
y of
  Maybe (SgnExt v n)
Nothing           -> Maybe (SgnExt v n)
forall a. Maybe a
Nothing
  Just (SgnExt Sign
u Ext v n
z) -> SgnExt v n -> Maybe (SgnExt v n)
forall a. a -> Maybe a
Just (SgnExt v n -> Maybe (SgnExt v n))
-> SgnExt v n -> Maybe (SgnExt v n)
forall a b. (a -> b) -> a -> b
$ Sign -> Ext v n -> SgnExt v n
forall (var :: Symbol) (n :: Nat).
Sign -> Ext var n -> SgnExt var n
SgnExt (Sign
s Sign -> Sign -> Sign
forall a. Monoid a => a -> a -> a
`mappend` Sign
t Sign -> Sign -> Sign
forall a. Monoid a => a -> a -> a
`mappend` Sign
u) Ext v n
z

productExt :: (KnownNat n, Foldable f) => f (Ext v n) -> Maybe (SgnExt v n)
productExt :: f (Ext v n) -> Maybe (SgnExt v n)
productExt f (Ext v n)
t = Sign -> [Ext v n] -> Maybe (SgnExt v n)
forall (n :: Nat) (v :: Symbol).
KnownNat n =>
Sign -> [Ext v n] -> Maybe (SgnExt v n)
go Sign
Plus (f (Ext v n) -> [Ext v n]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList f (Ext v n)
t) where
  go :: Sign -> [Ext v n] -> Maybe (SgnExt v n)
go !Sign
sgn [Ext v n]
list = case [Ext v n]
list of
    []         -> SgnExt v n -> Maybe (SgnExt v n)
forall a. a -> Maybe a
Just (Sign -> Ext v n -> SgnExt v n
forall (var :: Symbol) (n :: Nat).
Sign -> Ext var n -> SgnExt var n
SgnExt Sign
sgn Ext v n
forall (n :: Nat) (v :: Symbol). KnownNat n => Ext v n
emptyExt)
    [Ext v n
x]        -> SgnExt v n -> Maybe (SgnExt v n)
forall a. a -> Maybe a
Just (Sign -> Ext v n -> SgnExt v n
forall (var :: Symbol) (n :: Nat).
Sign -> Ext var n -> SgnExt var n
SgnExt Sign
sgn Ext v n
x)
    (Ext v n
x:Ext v n
y:[Ext v n]
rest) -> case Ext v n -> Ext v n -> Maybe (SgnExt v n)
forall (n :: Nat) (v :: Symbol).
KnownNat n =>
Ext v n -> Ext v n -> Maybe (SgnExt v n)
mulExt Ext v n
x Ext v n
y of
      Maybe (SgnExt v n)
Nothing           -> Maybe (SgnExt v n)
forall a. Maybe a
Nothing
      Just (SgnExt Sign
s Ext v n
z) -> Sign -> [Ext v n] -> Maybe (SgnExt v n)
go (Sign
sgn Sign -> Sign -> Sign
forall a. Monoid a => a -> a -> a
`mappend` Sign
s) (Ext v n
zExt v n -> [Ext v n] -> [Ext v n]
forall a. a -> [a] -> [a]
:[Ext v n]
rest) 

--------------------------------------------------------------------------------

[Ext "a" 7
v1,Ext "a" 7
v2,Ext "a" 7
v3,Ext "a" 7
v4,Ext "a" 7
v5,Ext "a" 7
v6] = [ Index -> Ext "a" 7
forall (n :: Nat) (v :: Symbol). KnownNat n => Index -> Ext v n
variableExt (Int -> Index
Index Int
i) | Int
i<-[Int
1..Int
6] ] :: [Ext "a" 7]
Just SgnExt "a" 7
a = [Ext "a" 7] -> Maybe (SgnExt "a" 7)
forall (n :: Nat) (f :: * -> *) (v :: Symbol).
(KnownNat n, Foldable f) =>
f (Ext v n) -> Maybe (SgnExt v n)
productExt [Ext "a" 7
v1,Ext "a" 7
v2,Ext "a" 7
v3]
Just SgnExt "a" 7
b = [Ext "a" 7] -> Maybe (SgnExt "a" 7)
forall (n :: Nat) (f :: * -> *) (v :: Symbol).
(KnownNat n, Foldable f) =>
f (Ext v n) -> Maybe (SgnExt v n)
productExt [Ext "a" 7
v4,Ext "a" 7
v5,Ext "a" 7
v6]

prop_graded_anticomm :: KnownNat n => Ext v n -> Ext v n -> Bool
prop_graded_anticomm :: Ext v n -> Ext v n -> Bool
prop_graded_anticomm Ext v n
x Ext v n
y 
  | Maybe (SgnExt v n) -> Bool
forall a. Maybe a -> Bool
isNothing Maybe (SgnExt v n)
mb1 Bool -> Bool -> Bool
&& Maybe (SgnExt v n) -> Bool
forall a. Maybe a -> Bool
isNothing Maybe (SgnExt v n)
mb2   = Bool
True
  | Maybe (SgnExt v n) -> Bool
forall a. Maybe a -> Bool
isJust    Maybe (SgnExt v n)
mb1 Bool -> Bool -> Bool
&& Maybe (SgnExt v n) -> Bool
forall a. Maybe a -> Bool
isJust    Maybe (SgnExt v n)
mb2   = Ext v n
u Ext v n -> Ext v n -> Bool
forall a. Eq a => a -> a -> Bool
== Ext v n
v Bool -> Bool -> Bool
&& Sign -> Sign
maybeFlip Sign
s Sign -> Sign -> Bool
forall a. Eq a => a -> a -> Bool
== Sign
t
  | Bool
otherwise                        = Bool
False
  where
    mb1 :: Maybe (SgnExt v n)
mb1 = Ext v n
x Ext v n -> Ext v n -> Maybe (SgnExt v n)
forall (n :: Nat) (v :: Symbol).
KnownNat n =>
Ext v n -> Ext v n -> Maybe (SgnExt v n)
`mulExt` Ext v n
y
    mb2 :: Maybe (SgnExt v n)
mb2 = Ext v n
y Ext v n -> Ext v n -> Maybe (SgnExt v n)
forall (n :: Nat) (v :: Symbol).
KnownNat n =>
Ext v n -> Ext v n -> Maybe (SgnExt v n)
`mulExt` Ext v n
x
    Just (SgnExt Sign
s Ext v n
u) = Maybe (SgnExt v n)
mb1
    Just (SgnExt Sign
t Ext v n
v) = Maybe (SgnExt v n)
mb2
    d1 :: Int
d1 = Ext v n -> Int
forall (v :: Symbol) (n :: Nat). Ext v n -> Int
degreeExt Ext v n
x
    d2 :: Int
d2 = Ext v n -> Int
forall (v :: Symbol) (n :: Nat). Ext v n -> Int
degreeExt Ext v n
y
    maybeFlip :: Sign -> Sign
maybeFlip = if Int -> Bool
forall a. Integral a => a -> Bool
odd (Int
d1Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
d2) then Sign -> Sign
oppositeSign else Sign -> Sign
forall a. a -> a
id    

prop_graded_anticomm_sgn :: KnownNat n => SgnExt v n -> SgnExt v n -> Bool
prop_graded_anticomm_sgn :: SgnExt v n -> SgnExt v n -> Bool
prop_graded_anticomm_sgn SgnExt v n
x SgnExt v n
y 
  | Maybe (SgnExt v n) -> Bool
forall a. Maybe a -> Bool
isNothing Maybe (SgnExt v n)
mb1 Bool -> Bool -> Bool
&& Maybe (SgnExt v n) -> Bool
forall a. Maybe a -> Bool
isNothing Maybe (SgnExt v n)
mb2   = Bool
True
  | Maybe (SgnExt v n) -> Bool
forall a. Maybe a -> Bool
isJust    Maybe (SgnExt v n)
mb1 Bool -> Bool -> Bool
&& Maybe (SgnExt v n) -> Bool
forall a. Maybe a -> Bool
isJust    Maybe (SgnExt v n)
mb2   = Ext v n
u Ext v n -> Ext v n -> Bool
forall a. Eq a => a -> a -> Bool
== Ext v n
v Bool -> Bool -> Bool
&& Sign -> Sign
maybeFlip Sign
s Sign -> Sign -> Bool
forall a. Eq a => a -> a -> Bool
== Sign
t
  | Bool
otherwise                        = Bool
False
  where
    mb1 :: Maybe (SgnExt v n)
mb1 = SgnExt v n
x SgnExt v n -> SgnExt v n -> Maybe (SgnExt v n)
forall (n :: Nat) (var :: Symbol).
KnownNat n =>
SgnExt var n -> SgnExt var n -> Maybe (SgnExt var n)
`mulSgnExt` SgnExt v n
y
    mb2 :: Maybe (SgnExt v n)
mb2 = SgnExt v n
y SgnExt v n -> SgnExt v n -> Maybe (SgnExt v n)
forall (n :: Nat) (var :: Symbol).
KnownNat n =>
SgnExt var n -> SgnExt var n -> Maybe (SgnExt var n)
`mulSgnExt` SgnExt v n
x
    Just (SgnExt Sign
s Ext v n
u) = Maybe (SgnExt v n)
mb1
    Just (SgnExt Sign
t Ext v n
v) = Maybe (SgnExt v n)
mb2
    d1 :: Int
d1 = SgnExt v n -> Int
forall (v :: Symbol) (n :: Nat). SgnExt v n -> Int
degreeSgnExt SgnExt v n
x
    d2 :: Int
d2 = SgnExt v n -> Int
forall (v :: Symbol) (n :: Nat). SgnExt v n -> Int
degreeSgnExt SgnExt v n
y
    maybeFlip :: Sign -> Sign
maybeFlip = if Int -> Bool
forall a. Integral a => a -> Bool
odd (Int
d1Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
d2) then Sign -> Sign
oppositeSign else Sign -> Sign
forall a. a -> a
id    

--------------------------------------------------------------------------------
-- * degree

degreeExt :: Ext v n -> Int
degreeExt :: Ext v n -> Int
degreeExt (Ext Integer
k) = Integer -> Int
forall a. Bits a => a -> Int
popCount Integer
k

degreeSgnExt :: SgnExt v n -> Int
degreeSgnExt :: SgnExt v n -> Int
degreeSgnExt (SgnExt Sign
sgn Ext v n
ext) = Ext v n -> Int
forall (v :: Symbol) (n :: Nat). Ext v n -> Int
degreeExt Ext v n
ext

--------------------------------------------------------------------------------
-- * Permutations

--
newtype Permutation = Permutation (UArray Int Int) deriving (Permutation -> Permutation -> Bool
(Permutation -> Permutation -> Bool)
-> (Permutation -> Permutation -> Bool) -> Eq Permutation
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Permutation -> Permutation -> Bool
$c/= :: Permutation -> Permutation -> Bool
== :: Permutation -> Permutation -> Bool
$c== :: Permutation -> Permutation -> Bool
Eq,Eq Permutation
Eq Permutation
-> (Permutation -> Permutation -> Ordering)
-> (Permutation -> Permutation -> Bool)
-> (Permutation -> Permutation -> Bool)
-> (Permutation -> Permutation -> Bool)
-> (Permutation -> Permutation -> Bool)
-> (Permutation -> Permutation -> Permutation)
-> (Permutation -> Permutation -> Permutation)
-> Ord Permutation
Permutation -> Permutation -> Bool
Permutation -> Permutation -> Ordering
Permutation -> Permutation -> Permutation
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Permutation -> Permutation -> Permutation
$cmin :: Permutation -> Permutation -> Permutation
max :: Permutation -> Permutation -> Permutation
$cmax :: Permutation -> Permutation -> Permutation
>= :: Permutation -> Permutation -> Bool
$c>= :: Permutation -> Permutation -> Bool
> :: Permutation -> Permutation -> Bool
$c> :: Permutation -> Permutation -> Bool
<= :: Permutation -> Permutation -> Bool
$c<= :: Permutation -> Permutation -> Bool
< :: Permutation -> Permutation -> Bool
$c< :: Permutation -> Permutation -> Bool
compare :: Permutation -> Permutation -> Ordering
$ccompare :: Permutation -> Permutation -> Ordering
$cp1Ord :: Eq Permutation
Ord)

toPermutationUnsafe :: [Int] -> Permutation
toPermutationUnsafe :: [Int] -> Permutation
toPermutationUnsafe [Int]
xs = UArray Int Int -> Permutation
Permutation UArray Int Int
perm where
  n :: Int
n    = [Int] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
xs
  perm :: UArray Int Int
perm = (Int, Int) -> [Int] -> UArray Int Int
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [e] -> a i e
listArray (Int
1,Int
n) [Int]
xs

sortingPermutationAsc :: Ord a => [a] -> Permutation
sortingPermutationAsc :: [a] -> Permutation
sortingPermutationAsc [a]
xs = [Int] -> Permutation
toPermutationUnsafe (((Int, a) -> Int) -> [(Int, a)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int, a) -> Int
forall a b. (a, b) -> a
fst [(Int, a)]
sorted) where
  sorted :: [(Int, a)]
sorted = ((Int, a) -> (Int, a) -> Ordering) -> [(Int, a)] -> [(Int, a)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (((Int, a) -> a) -> (Int, a) -> (Int, a) -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (Int, a) -> a
forall a b. (a, b) -> b
snd) ([(Int, a)] -> [(Int, a)]) -> [(Int, a)] -> [(Int, a)]
forall a b. (a -> b) -> a -> b
$ [Int] -> [a] -> [(Int, a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
1..] [a]
xs

{-
isEvenPermutation :: Permutation -> Bool
isEvenPermutation (Permutation perm) = res where

  (1,n) = bounds perm
  res = runST $ do
    tag <- newArray (1,n) False 
    cycles <- unfoldM (step tag) 1 
    return $ even (sum cycles)
    
  step :: STUArray s Int Bool -> Int -> ST s (Int,Maybe Int)
  step tag k = do
    cyclen <- worker tag k k 0
    m <- next tag (k+1)
    return (cyclen,m)
    
  next :: STUArray s Int Bool -> Int -> ST s (Maybe Int)
  next tag k = if k > n
    then return Nothing
    else readArray tag k >>= \b -> if b 
      then next tag (k+1)  
      else return (Just k)
      
  worker :: STUArray s Int Bool -> Int -> Int -> Int -> ST s Int
  worker tag k l cyclen = do
    writeArray tag l True
    let m = perm ! l
    if m == k 
      then return cyclen
      else worker tag k m (1+cyclen)      
-}

isEvenPermutation :: Permutation -> Bool
isEvenPermutation :: Permutation -> Bool
isEvenPermutation = Int -> Bool
forall a. Integral a => a -> Bool
even (Int -> Bool) -> (Permutation -> Int) -> Permutation -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Permutation -> Int
numberOfInversionsMerge

-- | Returns the number of inversions, using the merge-sort algorithm.
-- This should be @O(n*log(n))@
--
numberOfInversionsMerge :: Permutation -> Int
numberOfInversionsMerge :: Permutation -> Int
numberOfInversionsMerge (Permutation UArray Int Int
arr) = (Int, [Int]) -> Int
forall a b. (a, b) -> a
fst (Int -> [Int] -> (Int, [Int])
sortCnt Int
n ([Int] -> (Int, [Int])) -> [Int] -> (Int, [Int])
forall a b. (a -> b) -> a -> b
$ UArray Int Int -> [Int]
forall (a :: * -> * -> *) e i. (IArray a e, Ix i) => a i e -> [e]
elems UArray Int Int
arr) where
  (Int
_,Int
n) = UArray Int Int -> (Int, Int)
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds UArray Int Int
arr
                                        
  -- | First argument is length of the list.
  -- Returns also the inversion count.
  sortCnt :: Int -> [Int] -> (Int,[Int])
  sortCnt :: Int -> [Int] -> (Int, [Int])
sortCnt Int
0 [Int]
_     = (Int
0,[] )
  sortCnt Int
1 [Int
x]   = (Int
0,[Int
x])
  sortCnt Int
2 [Int
x,Int
y] = if Int
xInt -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>Int
y then (Int
1,[Int
y,Int
x]) else (Int
0,[Int
x,Int
y])
  sortCnt Int
n [Int]
xs    = (Int, [Int]) -> (Int, [Int]) -> (Int, [Int])
mergeCnt (Int -> [Int] -> (Int, [Int])
sortCnt Int
k [Int]
us) (Int -> [Int] -> (Int, [Int])
sortCnt Int
l [Int]
vs) where
    k :: Int
k = Int -> Int -> Int
forall a. Integral a => a -> a -> a
div Int
n Int
2
    l :: Int
l = Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
k 
    ([Int]
us,[Int]
vs) = Int -> [Int] -> ([Int], [Int])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
k [Int]
xs

  mergeCnt :: (Int,[Int]) -> (Int,[Int]) -> (Int,[Int])
  mergeCnt :: (Int, [Int]) -> (Int, [Int]) -> (Int, [Int])
mergeCnt (!Int
c,[Int]
us) (!Int
d,[Int]
vs) = (Int
cInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
dInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
e,[Int]
ws) where

    (Int
e,[Int]
ws) = Int -> [Int] -> [Int] -> (Int, [Int])
forall a. Ord a => Int -> [a] -> [a] -> (Int, [a])
go Int
0 [Int]
us [Int]
vs 

    go :: Int -> [a] -> [a] -> (Int, [a])
go !Int
k [a]
xs [] = ( Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
*[a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
xs , [a]
xs )
    go Int
_  [] [a]
ys = ( Int
0 , [a]
ys)
    go !Int
k xxs :: [a]
xxs@(a
x:[a]
xs) yys :: [a]
yys@(a
y:[a]
ys) = if a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
y
      then let (Int
a,[a]
zs) = Int -> [a] -> [a] -> (Int, [a])
go  Int
k     [a]
xs [a]
yys in (Int
aInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
k, a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
zs)
      else let (Int
a,[a]
zs) = Int -> [a] -> [a] -> (Int, [a])
go (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) [a]
xxs  [a]
ys in (Int
a  , a
ya -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
zs)

--------------------------------------------------------------------------------