    -- Copyright (c) David Amos, 2008. All rights reserved.

    module Math.Algebra.NonCommutative.GSBasis where

    import Data.List as L

    import Math.Algebra.NonCommutative.NCPoly

    -- given two monomials f g, find if possible a,b,c with f=ab g=bc

    findOverlap :: Monomial a
    -> Monomial a -> Maybe (Monomial a, Monomial a, Monomial a)
    findOverlap (M xs :: [a]
    xs) (M ys :: [a]
    ys) = [a] -> [a] -> [a] -> Maybe (Monomial a, Monomial a, Monomial a)
    forall a.
    Eq a =>
    [a] -> [a] -> [a] -> Maybe (Monomial a, Monomial a, Monomial a)
    findOverlap' [] [a]
    xs [a]
    ys where
        findOverlap' :: [a] -> [a] -> [a] -> Maybe (Monomial a, Monomial a, Monomial a)
    findOverlap' as :: [a]
    as [] cs :: [a]
    cs = Maybe (Monomial a, Monomial a, Monomial a)
    forall a. Maybe a
    Nothing -- (reverse as, [], cs)

        findOverlap' as :: [a]
    as (b :: a
    b:bs :: [a]
    bs) cs :: [a]
    cs =
            if (a
    ba -> [a] -> [a]
    forall a. a -> [a] -> [a]
    :[a]
    bs) [a] -> [a] -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `L.isPrefixOf` [a]
    cs
            then (Monomial a, Monomial a, Monomial a)
    -> Maybe (Monomial a, Monomial a, Monomial a)
    forall a. a -> Maybe a
    Just ([a] -> Monomial a
    forall v. [v] -> Monomial v
    M ([a] -> Monomial a) -> [a] -> Monomial a
    forall a b. (a -> b) -> a -> b
    $ [a] -> [a]
    forall a. [a] -> [a]
    reverse [a]
    as, [a] -> Monomial a
    forall v. [v] -> Monomial v
    M ([a] -> Monomial a) -> [a] -> Monomial a
    forall a b. (a -> b) -> a -> b
    $ a
    ba -> [a] -> [a]
    forall a. a -> [a] -> [a]
    :[a]
    bs, [a] -> Monomial a
    forall v. [v] -> Monomial v
    M ([a] -> Monomial a) -> [a] -> Monomial a
    forall a b. (a -> b) -> a -> b
    $ Int -> [a] -> [a]
    forall a. Int -> [a] -> [a]
    drop ([a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length (a
    ba -> [a] -> [a]
    forall a. a -> [a] -> [a]
    :[a]
    bs)) [a]
    cs)
            else [a] -> [a] -> [a] -> Maybe (Monomial a, Monomial a, Monomial a)
    findOverlap' (a
    ba -> [a] -> [a]
    forall a. a -> [a] -> [a]
    :[a]
    as) [a]
    bs [a]
    cs

    -- given two monomials f g, find if possible l,r with g = lfr

    -- findInclusion (M xs) (M ys) = findInclusion'

    sPoly :: NPoly r v -> NPoly r v -> NPoly r v
    sPoly f :: NPoly r v
    f@(NP ((xs :: Monomial v
    xs,c :: r
    c):_)) g :: NPoly r v
    g@(NP ((ys :: Monomial v
    ys,d :: r
    d):_)) =
        case Monomial v
    -> Monomial v -> Maybe (Monomial v, Monomial v, Monomial v)
    forall a.
    Eq a =>
    Monomial a
    -> Monomial a -> Maybe (Monomial a, Monomial a, Monomial a)
    findOverlap Monomial v
    xs Monomial v
    ys of
        Just (l :: Monomial v
    l,m :: Monomial v
    m,r :: Monomial v
    r) -> NPoly r v
    f NPoly r v -> NPoly r v -> NPoly r v
    forall a. Num a => a -> a -> a
    * [(Monomial v, r)] -> NPoly r v
    forall r v. [(Monomial v, r)] -> NPoly r v
    NP [(Monomial v
    r,r
    d)] NPoly r v -> NPoly r v -> NPoly r v
    forall a. Num a => a -> a -> a
    - [(Monomial v, r)] -> NPoly r v
    forall r v. [(Monomial v, r)] -> NPoly r v
    NP [(Monomial v
    l,r
    c)] NPoly r v -> NPoly r v -> NPoly r v
    forall a. Num a => a -> a -> a
    * NPoly r v
    g
        Nothing -> 0
    sPoly _ _ = 0 -- !! shouldn't reach this

    -- The point about the s-poly is that it cancels out the leading terms of the two polys, exposing their second terms

    gb1 :: [NPoly r v] -> [NPoly r v]
    gb1 fs :: [NPoly r v]
    fs = [NPoly r v] -> [NPoly r v] -> [NPoly r v]
    forall v r.
    (Fractional r, Ord v, Show v, Eq r) =>
    [NPoly r v] -> [NPoly r v] -> [NPoly r v]
    gb' [NPoly r v]
    fs [NPoly r v -> NPoly r v -> NPoly r v
    forall v r.
    (Eq r, Num r, Ord v, Show v) =>
    NPoly r v -> NPoly r v -> NPoly r v
    sPoly NPoly r v
    fi NPoly r v
    fj | NPoly r v
    fi <- [NPoly r v]
    fs, NPoly r v
    fj <- [NPoly r v]
    fs, NPoly r v
    fi NPoly r v -> NPoly r v -> Bool
    forall a. Eq a => a -> a -> Bool
    /= NPoly r v
    fj] where -- unlike the commutative case, we take sPolys both ways round

        gb' :: [NPoly r v] -> [NPoly r v] -> [NPoly r v]
    gb' gs :: [NPoly r v]
    gs (h :: NPoly r v
    h:hs :: [NPoly r v]
    hs) = let h' :: NPoly r v
    h' = NPoly r v
    h NPoly r v -> [NPoly r v] -> NPoly r v
    forall r v.
    (Fractional r, Ord v, Show v, Eq r) =>
    NPoly r v -> [NPoly r v] -> NPoly r v
    %% [NPoly r v]
    gs in
                        if NPoly r v
    h' NPoly r v -> NPoly r v -> Bool
    forall a. Eq a => a -> a -> Bool
    == 0 then [NPoly r v] -> [NPoly r v] -> [NPoly r v]
    gb' [NPoly r v]
    gs [NPoly r v]
    hs else [NPoly r v] -> [NPoly r v] -> [NPoly r v]
    gb' (NPoly r v
    h'NPoly r v -> [NPoly r v] -> [NPoly r v]
    forall a. a -> [a] -> [a]
    :[NPoly r v]
    gs) ([NPoly r v]
    hs [NPoly r v] -> [NPoly r v] -> [NPoly r v]
    forall a. [a] -> [a] -> [a]
    ++ [NPoly r v -> NPoly r v -> NPoly r v
    forall v r.
    (Eq r, Num r, Ord v, Show v) =>
    NPoly r v -> NPoly r v -> NPoly r v
    sPoly NPoly r v
    h' NPoly r v
    g | NPoly r v
    g <- [NPoly r v]
    gs] [NPoly r v] -> [NPoly r v] -> [NPoly r v]
    forall a. [a] -> [a] -> [a]
    ++ [NPoly r v -> NPoly r v -> NPoly r v
    forall v r.
    (Eq r, Num r, Ord v, Show v) =>
    NPoly r v -> NPoly r v -> NPoly r v
    sPoly NPoly r v
    g NPoly r v
    h' | NPoly r v
    g <- [NPoly r v]
    gs])
        gb' gs :: [NPoly r v]
    gs [] = [NPoly r v]
    gs

    reduce :: [NPoly r v] -> [NPoly r v]
    reduce gs :: [NPoly r v]
    gs = [NPoly r v] -> [NPoly r v] -> [NPoly r v]
    forall v r.
    (Ord r, Fractional r, Ord v, Show v) =>
    [NPoly r v] -> [NPoly r v] -> [NPoly r v]
    reduce' [] [NPoly r v]
    gs where
        reduce' :: [NPoly r v] -> [NPoly r v] -> [NPoly r v]
    reduce' gs' :: [NPoly r v]
    gs' (g :: NPoly r v
    g:gs :: [NPoly r v]
    gs) | NPoly r v
    g' NPoly r v -> NPoly r v -> Bool
    forall a. Eq a => a -> a -> Bool
    == 0   = [NPoly r v] -> [NPoly r v] -> [NPoly r v]
    reduce' [NPoly r v]
    gs' [NPoly r v]
    gs
                           | Bool
    otherwise = [NPoly r v] -> [NPoly r v] -> [NPoly r v]
    reduce' (NPoly r v
    g'NPoly r v -> [NPoly r v] -> [NPoly r v]
    forall a. a -> [a] -> [a]
    :[NPoly r v]
    gs') [NPoly r v]
    gs
                           where g' :: NPoly r v
    g' = NPoly r v
    g NPoly r v -> [NPoly r v] -> NPoly r v
    forall r v.
    (Fractional r, Ord v, Show v, Eq r) =>
    NPoly r v -> [NPoly r v] -> NPoly r v
    %% ([NPoly r v]
    gs'[NPoly r v] -> [NPoly r v] -> [NPoly r v]
    forall a. [a] -> [a] -> [a]
    ++[NPoly r v]
    gs)
        reduce' gs' :: [NPoly r v]
    gs' [] = [NPoly r v] -> [NPoly r v]
    forall a. [a] -> [a]
    reverse ([NPoly r v] -> [NPoly r v]) -> [NPoly r v] -> [NPoly r v]
    forall a b. (a -> b) -> a -> b
    $ [NPoly r v] -> [NPoly r v]
    forall a. Ord a => [a] -> [a]
    sort ([NPoly r v] -> [NPoly r v]) -> [NPoly r v] -> [NPoly r v]
    forall a b. (a -> b) -> a -> b
    $ [NPoly r v]
    gs'

    gb :: [NPoly r v] -> [NPoly r v]
    gb fs :: [NPoly r v]
    fs = (NPoly r v -> NPoly r v) -> [NPoly r v] -> [NPoly r v]
    forall a b. (a -> b) -> [a] -> [b]
    map NPoly r v -> NPoly r v
    forall v r.
    (Eq r, Ord v, Show v, Fractional r) =>
    NPoly r v -> NPoly r v
    toMonic ([NPoly r v] -> [NPoly r v]) -> [NPoly r v] -> [NPoly r v]
    forall a b. (a -> b) -> a -> b
    $ [NPoly r v] -> [NPoly r v]
    forall r v.
    (Fractional r, Ord r, Ord v, Show v) =>
    [NPoly r v] -> [NPoly r v]
    reduce ([NPoly r v] -> [NPoly r v]) -> [NPoly r v] -> [NPoly r v]
    forall a b. (a -> b) -> a -> b
    $ [NPoly r v] -> [NPoly r v]
    forall r v.
    (Fractional r, Ord v, Show v, Eq r) =>
    [NPoly r v] -> [NPoly r v]
    gb1 [NPoly r v]
    fs

    gb' :: [NPoly r v] -> [NPoly r v]
    gb' fs :: [NPoly r v]
    fs = [NPoly r v] -> [NPoly r v]
    forall r v.
    (Fractional r, Ord r, Ord v, Show v) =>
    [NPoly r v] -> [NPoly r v]
    reduce ([NPoly r v] -> [NPoly r v]) -> [NPoly r v] -> [NPoly r v]
    forall a b. (a -> b) -> a -> b
    $ [NPoly r v] -> [NPoly r v]
    forall r v.
    (Fractional r, Ord v, Show v, Eq r) =>
    [NPoly r v] -> [NPoly r v]
    gb1 [NPoly r v]
    fs

    gb2 :: [NPoly r v] -> [NPoly r v]
    gb2 fs :: [NPoly r v]
    fs = [NPoly r v] -> [(NPoly r v, NPoly r v)] -> [NPoly r v]
    forall v r.
    (Fractional r, Ord v, Show v, Eq r) =>
    [NPoly r v] -> [(NPoly r v, NPoly r v)] -> [NPoly r v]
    gb' [NPoly r v]
    fs [(NPoly r v
    fi,NPoly r v
    fj) | NPoly r v
    fi <- [NPoly r v]
    fs, NPoly r v
    fj <- [NPoly r v]
    fs, NPoly r v
    fi NPoly r v -> NPoly r v -> Bool
    forall a. Eq a => a -> a -> Bool
    /= NPoly r v
    fj] where -- unlike the commutative case, we take sPolys both ways round

        gb' :: [NPoly r v] -> [(NPoly r v, NPoly r v)] -> [NPoly r v]
    gb' gs :: [NPoly r v]
    gs ((fi :: NPoly r v
    fi,fj :: NPoly r v
    fj):pairs :: [(NPoly r v, NPoly r v)]
    pairs) =
            let h :: NPoly r v
    h = NPoly r v -> NPoly r v -> NPoly r v
    forall v r.
    (Eq r, Num r, Ord v, Show v) =>
    NPoly r v -> NPoly r v -> NPoly r v
    sPoly NPoly r v
    fi NPoly r v
    fj NPoly r v -> [NPoly r v] -> NPoly r v
    forall r v.
    (Fractional r, Ord v, Show v, Eq r) =>
    NPoly r v -> [NPoly r v] -> NPoly r v
    %% [NPoly r v]
    gs in
            if NPoly r v
    h NPoly r v -> NPoly r v -> Bool
    forall a. Eq a => a -> a -> Bool
    == 0 then [NPoly r v] -> [(NPoly r v, NPoly r v)] -> [NPoly r v]
    gb' [NPoly r v]
    gs [(NPoly r v, NPoly r v)]
    pairs else [NPoly r v] -> [(NPoly r v, NPoly r v)] -> [NPoly r v]
    gb' (NPoly r v
    hNPoly r v -> [NPoly r v] -> [NPoly r v]
    forall a. a -> [a] -> [a]
    :[NPoly r v]
    gs) ([(NPoly r v, NPoly r v)]
    pairs [(NPoly r v, NPoly r v)]
    -> [(NPoly r v, NPoly r v)] -> [(NPoly r v, NPoly r v)]
    forall a. [a] -> [a] -> [a]
    ++ [(NPoly r v
    h,NPoly r v
    g) | NPoly r v
    g <- [NPoly r v]
    gs] [(NPoly r v, NPoly r v)]
    -> [(NPoly r v, NPoly r v)] -> [(NPoly r v, NPoly r v)]
    forall a. [a] -> [a] -> [a]
    ++ [(NPoly r v
    g,NPoly r v
    h) | NPoly r v
    g <- [NPoly r v]
    gs])
        gb' gs :: [NPoly r v]
    gs [] = [NPoly r v]
    gs

    gb2' :: [NPoly r v] -> [(NPoly r v, NPoly r v, NPoly r v, NPoly r v)]
    gb2' fs :: [NPoly r v]
    fs = [NPoly r v]
    -> [(NPoly r v, NPoly r v)]
    -> [(NPoly r v, NPoly r v, NPoly r v, NPoly r v)]
    forall v r.
    (Fractional r, Ord v, Show v, Eq r) =>
    [NPoly r v]
    -> [(NPoly r v, NPoly r v)]
    -> [(NPoly r v, NPoly r v, NPoly r v, NPoly r v)]
    gb' [NPoly r v]
    fs [(NPoly r v
    fi,NPoly r v
    fj) | NPoly r v
    fi <- [NPoly r v]
    fs, NPoly r v
    fj <- [NPoly r v]
    fs, NPoly r v
    fi NPoly r v -> NPoly r v -> Bool
    forall a. Eq a => a -> a -> Bool
    /= NPoly r v
    fj] where -- unlike the commutative case, we take sPolys both ways round

        gb' :: [NPoly r v]
    -> [(NPoly r v, NPoly r v)]
    -> [(NPoly r v, NPoly r v, NPoly r v, NPoly r v)]
    gb' gs :: [NPoly r v]
    gs ((fi :: NPoly r v
    fi,fj :: NPoly r v
    fj):pairs :: [(NPoly r v, NPoly r v)]
    pairs) =
            let h :: NPoly r v
    h = NPoly r v -> NPoly r v -> NPoly r v
    forall v r.
    (Eq r, Num r, Ord v, Show v) =>
    NPoly r v -> NPoly r v -> NPoly r v
    sPoly NPoly r v
    fi NPoly r v
    fj NPoly r v -> [NPoly r v] -> NPoly r v
    forall r v.
    (Fractional r, Ord v, Show v, Eq r) =>
    NPoly r v -> [NPoly r v] -> NPoly r v
    %% [NPoly r v]
    gs in
            if NPoly r v
    h NPoly r v -> NPoly r v -> Bool
    forall a. Eq a => a -> a -> Bool
    == 0 then [NPoly r v]
    -> [(NPoly r v, NPoly r v)]
    -> [(NPoly r v, NPoly r v, NPoly r v, NPoly r v)]
    gb' [NPoly r v]
    gs [(NPoly r v, NPoly r v)]
    pairs else (NPoly r v
    fi,NPoly r v
    fj,NPoly r v -> NPoly r v -> NPoly r v
    forall v r.
    (Eq r, Num r, Ord v, Show v) =>
    NPoly r v -> NPoly r v -> NPoly r v
    sPoly NPoly r v
    fi NPoly r v
    fj,NPoly r v
    h) (NPoly r v, NPoly r v, NPoly r v, NPoly r v)
    -> [(NPoly r v, NPoly r v, NPoly r v, NPoly r v)]
    -> [(NPoly r v, NPoly r v, NPoly r v, NPoly r v)]
    forall a. a -> [a] -> [a]
    : [NPoly r v]
    -> [(NPoly r v, NPoly r v)]
    -> [(NPoly r v, NPoly r v, NPoly r v, NPoly r v)]
    gb' (NPoly r v
    hNPoly r v -> [NPoly r v] -> [NPoly r v]
    forall a. a -> [a] -> [a]
    :[NPoly r v]
    gs) ([(NPoly r v, NPoly r v)]
    pairs [(NPoly r v, NPoly r v)]
    -> [(NPoly r v, NPoly r v)] -> [(NPoly r v, NPoly r v)]
    forall a. [a] -> [a] -> [a]
    ++ [(NPoly r v
    h,NPoly r v
    g) | NPoly r v
    g <- [NPoly r v]
    gs] [(NPoly r v, NPoly r v)]
    -> [(NPoly r v, NPoly r v)] -> [(NPoly r v, NPoly r v)]
    forall a. [a] -> [a] -> [a]
    ++ [(NPoly r v
    g,NPoly r v
    h) | NPoly r v
    g <- [NPoly r v]
    gs])
        gb' gs :: [NPoly r v]
    gs [] = [] -- gs

    -- Monomial basis for the quotient algebra, where gs are the generators, rs the relations

    mbasisQA :: [NPoly r v] -> [NPoly r v] -> [NPoly r v]
    mbasisQA gs :: [NPoly r v]
    gs rs :: [NPoly r v]
    rs = [NPoly r v] -> [NPoly r v]
    mbasisQA' [1] where
        mbasisQA' :: [NPoly r v] -> [NPoly r v]
    mbasisQA' [] = [] -- the quotient ring has a finite monomial basis

        mbasisQA' ms :: [NPoly r v]
    ms = let ms' :: [NPoly r v]
    ms' = [NPoly r v
    gNPoly r v -> NPoly r v -> NPoly r v
    forall a. Num a => a -> a -> a
    *NPoly r v
    m | NPoly r v
    g <- [NPoly r v]
    gs, NPoly r v
    m <- [NPoly r v]
    ms, NPoly r v
    gNPoly r v -> NPoly r v -> NPoly r v
    forall a. Num a => a -> a -> a
    *NPoly r v
    m NPoly r v -> [NPoly r v] -> NPoly r v
    forall r v.
    (Fractional r, Ord v, Show v, Eq r) =>
    NPoly r v -> [NPoly r v] -> NPoly r v
    %% [NPoly r v]
    rs NPoly r v -> NPoly r v -> Bool
    forall a. Eq a => a -> a -> Bool
    == NPoly r v
    gNPoly r v -> NPoly r v -> NPoly r v
    forall a. Num a => a -> a -> a
    *NPoly r v
    m] -- ie, not reducible

                       in [NPoly r v]
    ms [NPoly r v] -> [NPoly r v] -> [NPoly r v]
    forall a. [a] -> [a] -> [a]
    ++ [NPoly r v] -> [NPoly r v]
    mbasisQA' [NPoly r v]
    ms'
    {-
    isGB fs = all (\h -> h %% fs == 0) (pairWith sPoly fs)
    -}