content: {-# LANGUAGE ConstraintKinds, DataKinds, GADTs, KindSignatures     #-}
  {-# LANGUAGE MultiParamTypeClasses, NoImplicitPrelude              #-}
  {-# LANGUAGE NoMonomorphismRestriction, QuasiQuotes, TypeOperators #-}
  module Main where
  import Algebra.Algorithms.Groebner
  import Algebra.Field.Finite
  import Algebra.Prelude
  import Data.Type.Ordinal
  
  -- | 0-th variable of polynomial ring with at least one variable.
  -- Variables are 0-origin.
  x :: (KnownNat n, CoeffRing r, IsMonomialOrder n order, (0 < n) ~ 'True)
    => OrderedPolynomial r order n
  x = var [od|0|]
  
  -- | 1-st variable of polynomial ring with at least two variable.
  y :: (KnownNat n, CoeffRing r, IsMonomialOrder n order, (1 < n) ~ 'True)
    => OrderedPolynomial r order n
  y = var [od|1|]
  
  -- | The last variable of
  z :: Polynomial Rational 3
  z = var [od|2|]
  
  -- | f in QQ[x,y,z]
  f :: OrderedPolynomial Rational Grevlex 3
  f = 1%2*x*y^2 + y^2
  
  -- | map f to the F_5[x,y,z], where F_5 = ZZ/5ZZ
  f' :: Polynomial (F 5) 3
  f' = mapCoeff (\r -> fromInteger (numerator r) / fromInteger (denominator r) ) f
  
  -- | ideal of QQ[x,y,a,b,c,s]
  heron :: Ideal (OrderedPolynomial Rational Lex 6)
  heron = toIdeal [ 2 * s - a * y
                  , b^2 - (x^2 + y^2)
                  , c^2 - ((a - x)^2 + y^2)
                  ]
    where
      -- | Get the last four variables of QQ[x,y,a,b,c,s]
      [_, _, a, b, c, s] = vars
  
  main :: IO ()
  main = act
  
  act = do
    print f
    print f'
    print $ x * f'^2
    print $ calcGroebnerBasis heron
    -- print $ f' * 5 + f -- ^ Type error!
  