{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies, TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving, GeneralizedNewtypeDeriving #-}
{-# LANGUAGE DataKinds, RankNTypes #-}

-- |

-- Module      : OAlg.AbelianGroup.Definition

-- Description : lifting of abelian homomorphisms.

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

--

-- lifting of abelian homomorphisms.

module OAlg.AbelianGroup.Liftable
  (
    -- * Lifting

    zMatrixLift

    -- * Proposition

  , prpMatrixZJustLiftable
  , prpMatrixZMaybeLiftable
  , prpMatrixZLiftable

    -- * X

  , xLiftable

  ) where

import Control.Monad

import Data.List (zip,(++))
import Data.Foldable (foldr)

import OAlg.Prelude

import OAlg.Data.Canonical

import OAlg.Structure.Oriented
import OAlg.Structure.Multiplicative
import OAlg.Structure.Number
import OAlg.Structure.Exponential

import OAlg.Entity.Slice.Liftable
import OAlg.Entity.Matrix
import OAlg.Entity.Sequence.PSequence

import OAlg.AbelianGroup.Free.SmithNormalForm
import OAlg.AbelianGroup.Euclid

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

-- zMatrixLift -


-- | tries to solve the equation @a '*' x '==' y@.

--

-- __Property__ Let @a@ and @y@ be in @'Matrix' 'Z'@, then holds:

--

-- (1) If @'end' y@ is not equal to @'end' a@ then evaluating @'zMatrixLift' a y@ will end up

-- in a 'NotLiftable'-exception.

--

-- (2) If @'end' y@ is equal to @'end' a@ and there exists an @x@ in @'Matrix' 'Z'@ such that

-- @a '*' x '==' y@ then the result of @'zMatrixLift' a y@ is @'Just' x@ otherwise it

-- will be 'Nothing'. If there exists a non trivial solution, then @x@ will also be non trival.

zMatrixLift :: Matrix Z -> Matrix Z -> Maybe (Matrix Z)
zMatrixLift :: Matrix Z -> Matrix Z -> Maybe (Matrix Z)
zMatrixLift Matrix Z
a Matrix Z
y
  | Matrix Z -> Point (Matrix Z)
forall q. Oriented q => q -> Point q
end Matrix Z
a Dim Z () -> Dim Z () -> Bool
forall a. Eq a => a -> a -> Bool
/= Matrix Z -> Point (Matrix Z)
forall q. Oriented q => q -> Point q
end Matrix Z
y = LiftableException -> String -> Maybe (Matrix Z)
forall a e. Exception e => e -> a
throw LiftableException
NotLiftable String
"end missmatch"
  | Bool
otherwise      = (Matrix Z -> Matrix Z) -> Maybe (Matrix Z) -> Maybe (Matrix Z)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (Matrix Z
rMatrix Z -> Matrix Z -> Matrix Z
forall c. Multiplicative c => c -> c -> c
*) (Maybe (Matrix Z) -> Maybe (Matrix Z))
-> Maybe (Matrix Z) -> Maybe (Matrix Z)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Dim' Z -> [(Z, N)] -> Matrix Z -> Maybe (Matrix Z)
lft (Matrix Z -> Point (Matrix Z)
forall q. Oriented q => q -> Point q
start Matrix Z
a) ([Z]
ds [Z] -> [N] -> [(Z, N)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [N
0..]) (Matrix Z
s Matrix Z -> Matrix Z -> Matrix Z
forall c. Multiplicative c => c -> c -> c
* Matrix Z
y) where
  
  DiagonalForm [Z]
ds (RowTrafo GLT Z
sRT) (ColTrafo GLT Z
rCT) = SmithNormalForm Z -> DiagonalForm Z
forall k. Semiring k => SmithNormalForm k -> DiagonalForm k
snfDiagonalForm (SmithNormalForm Z -> DiagonalForm Z)
-> SmithNormalForm Z -> DiagonalForm Z
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Matrix Z -> SmithNormalForm Z
smithNormalForm Matrix Z
a
  Inv Matrix Z
s Matrix Z
_ = GLApp (GLT Z) (Inv (Matrix Z)) -> GLT Z -> Inv (Matrix Z)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap GLApp (GLT Z) (Inv (Matrix Z))
forall x1. Distributive x1 => GLApp (GLT x1) (Inv (Matrix x1))
GLTGL GLT Z
sRT
  Inv Matrix Z
r Matrix Z
_ = GLApp (GLT Z) (Inv (Matrix Z)) -> GLT Z -> Inv (Matrix Z)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap GLApp (GLT Z) (Inv (Matrix Z))
forall x1. Distributive x1 => GLApp (GLT x1) (Inv (Matrix x1))
GLTGL GLT Z
rCT

  lft :: Dim' Z -> [(Z,N)] -> Matrix Z -> Maybe (Matrix Z)
  lft :: Dim' Z -> [(Z, N)] -> Matrix Z -> Maybe (Matrix Z)
lft Dim' Z
aCls [(Z, N)]
ds (Matrix Dim' Z
_ Dim' Z
yCls Entries N N Z
ys) = do
    Row N (Col N Z)
y'rc <- N -> N -> [(Z, N)] -> Row N (Col N Z) -> Maybe (Row N (Col N Z))
lftCols (Dim Z () -> N
forall x. LengthN x => x -> N
lengthN Dim Z ()
Dim' Z
aCls) (Dim Z () -> N
forall x. LengthN x => x -> N
lengthN Dim Z ()
Dim' Z
yCls) [(Z, N)]
ds (Entries N N Z -> Row N (Col N Z)
forall i j x. (Ord i, Ord j) => Entries i j x -> Row j (Col i x)
etsrc Entries N N Z
ys)
    Matrix Z -> Maybe (Matrix Z)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Dim' Z -> Dim' Z -> Entries N N Z -> Matrix Z
forall x. Dim' x -> Dim' x -> Entries N N x -> Matrix x
Matrix Dim' Z
aCls Dim' Z
yCls (Entries N N Z -> Matrix Z) -> Entries N N Z -> Matrix Z
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Row N (Col N Z) -> Entries N N Z
forall i j x. (Ord i, Ord j) => Row j (Col i x) -> Entries i j x
rcets Row N (Col N Z)
y'rc)

  nonTrivialCol :: N -> N -> Closure N -> N -> [(Col N Z,N)]
  nonTrivialCol :: N -> N -> Closure N -> N -> [(Col N Z, N)]
nonTrivialCol N
r N
aCls Closure N
yClsReached N
yCls
    | N
aCls N -> N -> Bool
forall a. Ord a => a -> a -> Bool
<= N
r = [] -- matrix a is injective

    | N
j' N -> N -> Bool
forall a. Ord a => a -> a -> Bool
< N
yCls = [(PSequence N Z -> Col N Z
forall i x. PSequence i x -> Col i x
Col (PSequence N Z -> Col N Z) -> PSequence N Z -> Col N Z
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(Z, N)] -> PSequence N Z
forall i x. [(x, i)] -> PSequence i x
PSequence [(Z
1,N
r)],N
j')]
    | Bool
otherwise = []
    where j' :: N
j' = case Closure N
yClsReached of
                 Closure N
NegInf -> N
0
                 It N
j   -> N -> N
forall a. Enum a => a -> a
succ N
j


  lftCols :: N -> N -> [(Z,N)] -> Row N (Col N Z) -> Maybe (Row N (Col N Z))
  lftCols :: N -> N -> [(Z, N)] -> Row N (Col N Z) -> Maybe (Row N (Col N Z))
lftCols N
aCls N
yCls [(Z, N)]
ds Row N (Col N Z)
rc = do
    ([(Col N Z, N)]
rc',Closure N
yClsMax) <- ((Col N Z, N)
 -> Maybe ([(Col N Z, N)], Closure N)
 -> Maybe ([(Col N Z, N)], Closure N))
-> Maybe ([(Col N Z, N)], Closure N)
-> [(Col N Z, N)]
-> Maybe ([(Col N Z, N)], Closure N)
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ([(Z, N)]
-> (Col N Z, N)
-> Maybe ([(Col N Z, N)], Closure N)
-> Maybe ([(Col N Z, N)], Closure N)
addLftCol [(Z, N)]
ds) (([(Col N Z, N)], Closure N) -> Maybe ([(Col N Z, N)], Closure N)
forall a. a -> Maybe a
Just ([],Closure N
forall x. Closure x
NegInf)) ([(Col N Z, N)] -> Maybe ([(Col N Z, N)], Closure N))
-> [(Col N Z, N)] -> Maybe ([(Col N Z, N)], Closure N)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Row N (Col N Z) -> [(Col N Z, N)]
forall j x. Row j x -> [(x, j)]
rowxs Row N (Col N Z)
rc
    Row N (Col N Z) -> Maybe (Row N (Col N Z))
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (PSequence N (Col N Z) -> Row N (Col N Z)
forall j x. PSequence j x -> Row j x
Row (PSequence N (Col N Z) -> Row N (Col N Z))
-> PSequence N (Col N Z) -> Row N (Col N Z)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(Col N Z, N)] -> PSequence N (Col N Z)
forall i x. [(x, i)] -> PSequence i x
PSequence ([(Col N Z, N)]
rc' [(Col N Z, N)] -> [(Col N Z, N)] -> [(Col N Z, N)]
forall a. [a] -> [a] -> [a]
++ N -> N -> Closure N -> N -> [(Col N Z, N)]
nonTrivialCol ([(Z, N)] -> N
forall x. LengthN x => x -> N
lengthN [(Z, N)]
ds) N
aCls Closure N
yClsMax N
yCls))

  addLftCol :: [(Z,N)]
    -> (Col N Z,N) -> Maybe ([(Col N Z,N)],Closure N) -> Maybe ([(Col N Z,N)],Closure N)
  addLftCol :: [(Z, N)]
-> (Col N Z, N)
-> Maybe ([(Col N Z, N)], Closure N)
-> Maybe ([(Col N Z, N)], Closure N)
addLftCol [(Z, N)]
ds (Col N Z
yi,N
j) Maybe ([(Col N Z, N)], Closure N)
mCls = do
    ([(Col N Z, N)]
xis,Closure N
jMax) <- Maybe ([(Col N Z, N)], Closure N)
mCls
    [(Z, N)]
xi         <- [(Z, N)] -> [(Z, N)] -> Maybe [(Z, N)]
lftCol [(Z, N)]
ds (Col N Z -> [(Z, N)]
forall i x. Col i x -> [(x, i)]
colxs Col N Z
yi)
    ([(Col N Z, N)], Closure N) -> Maybe ([(Col N Z, N)], Closure N)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ((PSequence N Z -> Col N Z
forall i x. PSequence i x -> Col i x
Col (PSequence N Z -> Col N Z) -> PSequence N Z -> Col N Z
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(Z, N)] -> PSequence N Z
forall i x. [(x, i)] -> PSequence i x
PSequence [(Z, N)]
xi,N
j)(Col N Z, N) -> [(Col N Z, N)] -> [(Col N Z, N)]
forall a. a -> [a] -> [a]
:[(Col N Z, N)]
xis,N -> Closure N
forall x. x -> Closure x
It N
j Closure N -> Closure N -> Closure N
forall a. Ord a => a -> a -> a
`max` Closure N
jMax)

  lftCol :: [(Z,N)] -> [(Z,N)] -> Maybe [(Z,N)]
  lftCol :: [(Z, N)] -> [(Z, N)] -> Maybe [(Z, N)]
lftCol ((Z
d,N
i):[(Z, N)]
dis) yis :: [(Z, N)]
yis@((Z
y,N
i'):[(Z, N)]
yis') = case N
i N -> N -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` N
i' of
    Ordering
LT -> [(Z, N)] -> [(Z, N)] -> Maybe [(Z, N)]
lftCol [(Z, N)]
dis [(Z, N)]
yis
    Ordering
EQ -> let (Z
x,Z
r) = Z -> Z -> (Z, Z)
forall a. Integral a => a -> a -> (a, a)
divMod Z
y Z
d in case Z
r of
        Z
0 -> [(Z, N)] -> [(Z, N)] -> Maybe [(Z, N)]
lftCol [(Z, N)]
dis [(Z, N)]
yis' Maybe [(Z, N)] -> ([(Z, N)] -> Maybe [(Z, N)]) -> Maybe [(Z, N)]
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [(Z, N)] -> Maybe [(Z, N)]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Z, N)] -> Maybe [(Z, N)])
-> ([(Z, N)] -> [(Z, N)]) -> [(Z, N)] -> Maybe [(Z, N)]
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. ((Z
x,N
i)(Z, N) -> [(Z, N)] -> [(Z, N)]
forall a. a -> [a] -> [a]
:)
        Z
_ -> Maybe [(Z, N)]
forall a. Maybe a
Nothing
    -- the case GT should not occure, as the dis are succesive!

  lftCol [] ((Z, N)
_:[(Z, N)]
_) = Maybe [(Z, N)]
forall a. Maybe a
Nothing
  lftCol [(Z, N)]
_ [(Z, N)]
_      = [(Z, N)] -> Maybe [(Z, N)]
forall a. a -> Maybe a
Just []

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

-- xLiftable -


-- | random variable for liftable samples.

xLiftable :: Multiplicative c => XOrtSite To c -> X (c,c)
xLiftable :: forall c. Multiplicative c => XOrtSite 'To c -> X (c, c)
xLiftable XOrtSite 'To c
xTo = (Mltp2 c -> (c, c)) -> X (Mltp2 c) -> X (c, c)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 Mltp2 c -> (c, c)
forall {b}. Multiplicative b => Mltp2 b -> (b, b)
lft (X (Mltp2 c) -> X (c, c)) -> X (Mltp2 c) -> X (c, c)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ XOrtSite 'To c -> X (Mltp2 c)
forall c (d :: Site).
Multiplicative c =>
XOrtSite d c -> X (Mltp2 c)
xMltp2 XOrtSite 'To c
xTo where lft :: Mltp2 b -> (b, b)
lft (Mltp2 b
a b
x) = (b
a,b
ab -> b -> b
forall c. Multiplicative c => c -> c -> c
*b
x)

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

-- prpMatrixZJustLiftable -


-- | validity of 'zMatrixLift' for liftable samples.

prpMatrixZJustLiftable :: XOrtSite To (Matrix Z) -> Statement
prpMatrixZJustLiftable :: XOrtSite 'To (Matrix Z) -> Statement
prpMatrixZJustLiftable XOrtSite 'To (Matrix Z)
xTo = String -> Label
Prp String
"MatrixZJustLiftable" Label -> Statement -> Statement
:<=>:
  X (Matrix Z, Matrix Z)
-> ((Matrix Z, Matrix Z) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall (XOrtSite 'To (Matrix Z) -> X (Matrix Z, Matrix Z)
forall c. Multiplicative c => XOrtSite 'To c -> X (c, c)
xLiftable XOrtSite 'To (Matrix Z)
xTo)
    (\(Matrix Z
a,Matrix Z
y) -> let mx :: Maybe (Matrix Z)
mx = Matrix Z -> Matrix Z -> Maybe (Matrix Z)
zMatrixLift Matrix Z
a Matrix Z
y in
        case Maybe (Matrix Z)
mx of
          Just Matrix Z
x -> String -> Label
Label String
"a * x == y"
                      Label -> Statement -> Statement
:<=>: [Statement] -> Statement
And [ Matrix Z -> Statement
forall a. Validable a => a -> Statement
valid Matrix Z
x
                                , (Matrix Z
a Matrix Z -> Matrix Z -> Matrix Z
forall c. Multiplicative c => c -> c -> c
* Matrix Z
x Matrix Z -> Matrix Z -> Bool
forall a. Eq a => a -> a -> Bool
== Matrix Z
y) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"a"String -> String -> Parameter
:=Matrix Z -> String
forall a. Show a => a -> String
show Matrix Z
a,String
"y"String -> String -> Parameter
:=Matrix Z -> String
forall a. Show a => a -> String
show Matrix Z
y,String
"x"String -> String -> Parameter
:=Matrix Z -> String
forall a. Show a => a -> String
show Matrix Z
x]
                                ]
          Maybe (Matrix Z)
_      -> String -> Label
Label String
"should be liftable"
                      Label -> Statement -> Statement
:<=>: Bool
False Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"a"String -> String -> Parameter
:=Matrix Z -> String
forall a. Show a => a -> String
show Matrix Z
a,String
"y"String -> String -> Parameter
:=Matrix Z -> String
forall a. Show a => a -> String
show Matrix Z
y]
                     
    )

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

-- prpMatrixZMaybeLiftable -


-- | validity of 'zMatrixLift' where liftable and unliftable samples are validated.

prpMatrixZMaybeLiftable :: X Z -> Statement
prpMatrixZMaybeLiftable :: X Z -> Statement
prpMatrixZMaybeLiftable X Z
xz = String -> Label
Prp String
"MatrixZMaybeLiftable" Label -> Statement -> Statement
:<=>: X (Z, Z, Z) -> ((Z, Z, Z) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (Z, Z, Z)
ay (Z, Z, Z) -> Statement
test where
  ay :: X (Z, Z, Z)
ay = do
    Z
a0 <- X Z
xz
    Z
a1 <- X Z
xz
    Z
y  <- X Z
xz
    (Z, Z, Z) -> X (Z, Z, Z)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Z
a0,Z
a1,Z
y)

  test :: (Z, Z, Z) -> Statement
test (Z
a0,Z
a1,Z
y) = case Z
y Z -> Z -> Z
forall a. Integral a => a -> a -> a
`mod` (N -> Z
forall a b. Embeddable a b => a -> b
inj N
g) of
    Z
0 -> String -> Label
Label String
"solvable"
           Label -> Statement -> Statement
:<=>: case Maybe (Matrix Z)
mx of
                   Just Matrix Z
x -> [Statement] -> Statement
And [ Matrix Z -> Statement
forall a. Validable a => a -> Statement
valid Matrix Z
x
                                 , (Matrix Z
a Matrix Z -> Matrix Z -> Matrix Z
forall c. Multiplicative c => c -> c -> c
* Matrix Z
x Matrix Z -> Matrix Z -> Bool
forall a. Eq a => a -> a -> Bool
== Matrix Z
y') Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"a"String -> String -> Parameter
:=Matrix Z -> String
forall a. Show a => a -> String
show Matrix Z
a,String
"y"String -> String -> Parameter
:=Z -> String
forall a. Show a => a -> String
show Z
y,String
"x"String -> String -> Parameter
:=Matrix Z -> String
forall a. Show a => a -> String
show Matrix Z
x]
                                 ]
                   Maybe (Matrix Z)
_      -> String -> Label
Label String
"should be solvable"
                               Label -> Statement -> Statement
:<=>: Bool
False Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"a"String -> String -> Parameter
:=Matrix Z -> String
forall a. Show a => a -> String
show Matrix Z
a,String
"y"String -> String -> Parameter
:=Z -> String
forall a. Show a => a -> String
show Z
y]
    Z
_ -> String -> Label
Label String
"unsolvable"
           Label -> Statement -> Statement
:<=>: case Maybe (Matrix Z)
mx of
                   Maybe (Matrix Z)
Nothing -> Statement
SValid
                   Just Matrix Z
x  -> String -> Label
Label String
"should be unsolvable"
                     Label -> Statement -> Statement
:<=>: Bool
False Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"a"String -> String -> Parameter
:=Matrix Z -> String
forall a. Show a => a -> String
show Matrix Z
a,String
"y"String -> String -> Parameter
:=Z -> String
forall a. Show a => a -> String
show Z
y,String
"x"String -> String -> Parameter
:=Matrix Z -> String
forall a. Show a => a -> String
show Matrix Z
x]
    where (N
g,Z
_,Z
_) = Z -> Z -> (N, Z, Z)
euclid Z
a0 Z
a1
          d :: Dim Z ()
d  = () -> Dim Z ()
forall p x. (Entity p, p ~ Point x) => p -> Dim x p
dim () 
          a :: Matrix Z
a  = Dim Z () -> Dim Z () -> [(Z, N, N)] -> Matrix Z
forall x p.
(Additive x, p ~ Point x) =>
Dim x p -> Dim x p -> [(x, N, N)] -> Matrix x
matrix Dim Z ()
d (Dim Z ()
dDim Z () -> Exponent (Dim Z ()) -> Dim Z ()
forall f. Exponential f => f -> Exponent f -> f
^N
Exponent (Dim Z ())
2) [(Z
a0,N
0,N
0),(Z
a1,N
0,N
1)]
          y' :: Matrix Z
y' = Dim Z () -> Dim Z () -> [(Z, N, N)] -> Matrix Z
forall x p.
(Additive x, p ~ Point x) =>
Dim x p -> Dim x p -> [(x, N, N)] -> Matrix x
matrix Dim Z ()
d Dim Z ()
d [(Z
y,N
0,N
0)]
          mx :: Maybe (Matrix Z)
mx = Matrix Z -> Matrix Z -> Maybe (Matrix Z)
zMatrixLift Matrix Z
a Matrix Z
y'

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

-- prpMatrixZLiftable -


-- | validity of 'zMatrixLift'.

prpMatrixZLiftable :: Statement
prpMatrixZLiftable :: Statement
prpMatrixZLiftable = String -> Label
Prp String
"MatrixZLiftable" Label -> Statement -> Statement
:<=>:
  [Statement] -> Statement
And [ XOrtSite 'To (Matrix Z) -> Statement
prpMatrixZJustLiftable XOrtSite 'To (Matrix Z)
forall (s :: Site) a. XStandardOrtSite s a => XOrtSite s a
xStandardOrtSite
      , X Z -> Statement
prpMatrixZMaybeLiftable (Z -> Z -> X Z
xZB (-Z
1000) Z
1000)
      ]