\import Algebra.Group
\import Algebra.Monoid
\import Algebra.Ordered
\import Algebra.StrictlyOrdered
\import Algebra.Pointed
\import Algebra.Ring
\import Algebra.Solver
\import Arith.Int
\import Data.List

{-
  \func \infixl 7 *n (n : Nat) (a : E) : E \elim n
    | 0 => zro
    | suc n => n *n a + a

  \func \infixl 7 *i (n : Int) (a : E) : E \elim n
    | pos n => n *n a
    | neg (suc n) => suc n *n negative a
 -}

-- TODO[server2]: Finish this
\func LinearSolverModel (A : LinearlyOrderedAbGroup) : SolverModel A \cowith
  | Term => Term Int
  | NF => NF Int
  | normalize => normalize
  | interpret => {?}
  | interpretNF => {?}
  | interpretNF-consistent => {?}
  \where {
    \data Term (C : \Set) (n : Nat)
      | coef C (Term C n)
      | var (Fin n)
      | :zro
      | :negative (Term C n)
      | \infixl  :+ (t s : Term C n)

    \func NF (C : \Set) (n : Nat) => List (\Sigma (Fin n) C)

    \func mulNF {C : Monoid} {n : Nat} (c : C) (l : NF C n) : NF C n
      => map (\lam s => (s., c * s.)) l

    \func normalize {C : Ring} {n : Nat} (t : Term C n) : NF C n \elim t
      | coef c t => mulNF c (normalize t)
      | var v => (v,) :: nil
      | :zro => nil
      | :negative t => mulNF -1 (normalize t)
      | t :+ s => normalize t ++ normalize s

{-
    \func interpret (env : Array A) (t : Term Int env.len) : A \elim t
      | coef c t => c A.*i interpret env t
      | var j => env j
      | :zro => 0
      | :negative t => negative (interpret env t)
      | :+ t s => interpret env t + interpret env s

    \func mulCoef (c : C) (l : List (Fin env.len)) : R \elim l
      | nil => alg c
      | l => \case decideEq c 1 \with {
        | yes _ => MonoidSolverModel.interpretNF env l
        | no _ => alg c * MonoidSolverModel.interpretNF env l
      }

    \func interpretNF (env : Array A) (l : NF Int env.len) : A \elim l
      | nil => 0
      | x :: l => {?}
 -}
  }