{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}

module Hermod.ReCon.Integer.Polynomial.Value (
    IntTermNF(..)
  , zero
  , plus
  , minus
  , mul
  , nullify
  , eval
  , quote
  , normalise
  ) where

import           Hermod.ReCon.Integer.Polynomial.Term (VariableIdentifier, IntTerm (..), IntValue)

import qualified Data.List as List
import           Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map

-- | c + k₀ · x₀ + k₁ · x₁ + ... + kₙ · xₙ
data IntTermNF = IntTermNF {
  -- | Invariant: the coefficients must be non-zero.
  IntTermNF -> Map VariableIdentifier IntValue
coeff    :: Map VariableIdentifier IntValue,
  IntTermNF -> IntValue
constant :: IntValue
} deriving (Int -> IntTermNF -> ShowS
[IntTermNF] -> ShowS
IntTermNF -> String
(Int -> IntTermNF -> ShowS)
-> (IntTermNF -> String)
-> ([IntTermNF] -> ShowS)
-> Show IntTermNF
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> IntTermNF -> ShowS
showsPrec :: Int -> IntTermNF -> ShowS
$cshow :: IntTermNF -> String
show :: IntTermNF -> String
$cshowList :: [IntTermNF] -> ShowS
showList :: [IntTermNF] -> ShowS
Show, IntTermNF -> IntTermNF -> Bool
(IntTermNF -> IntTermNF -> Bool)
-> (IntTermNF -> IntTermNF -> Bool) -> Eq IntTermNF
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: IntTermNF -> IntTermNF -> Bool
== :: IntTermNF -> IntTermNF -> Bool
$c/= :: IntTermNF -> IntTermNF -> Bool
/= :: IntTermNF -> IntTermNF -> Bool
Eq, Eq IntTermNF
Eq IntTermNF =>
(IntTermNF -> IntTermNF -> Ordering)
-> (IntTermNF -> IntTermNF -> Bool)
-> (IntTermNF -> IntTermNF -> Bool)
-> (IntTermNF -> IntTermNF -> Bool)
-> (IntTermNF -> IntTermNF -> Bool)
-> (IntTermNF -> IntTermNF -> IntTermNF)
-> (IntTermNF -> IntTermNF -> IntTermNF)
-> Ord IntTermNF
IntTermNF -> IntTermNF -> Bool
IntTermNF -> IntTermNF -> Ordering
IntTermNF -> IntTermNF -> IntTermNF
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
$ccompare :: IntTermNF -> IntTermNF -> Ordering
compare :: IntTermNF -> IntTermNF -> Ordering
$c< :: IntTermNF -> IntTermNF -> Bool
< :: IntTermNF -> IntTermNF -> Bool
$c<= :: IntTermNF -> IntTermNF -> Bool
<= :: IntTermNF -> IntTermNF -> Bool
$c> :: IntTermNF -> IntTermNF -> Bool
> :: IntTermNF -> IntTermNF -> Bool
$c>= :: IntTermNF -> IntTermNF -> Bool
>= :: IntTermNF -> IntTermNF -> Bool
$cmax :: IntTermNF -> IntTermNF -> IntTermNF
max :: IntTermNF -> IntTermNF -> IntTermNF
$cmin :: IntTermNF -> IntTermNF -> IntTermNF
min :: IntTermNF -> IntTermNF -> IntTermNF
Ord)

-- 0 + 0 · x₀ + ... + 0 · xₙ
zero :: IntTermNF
zero :: IntTermNF
zero = IntTermNF{coeff :: Map VariableIdentifier IntValue
coeff = Map VariableIdentifier IntValue
forall k a. Map k a
Map.empty, constant :: IntValue
constant = IntValue
0}

-- | (c + k₀ · x₀ + k₁ · x₁ + ... + kₙ · xₙ) + (c' + k₀' · x₀ + k₁' · x₁ + ... + kₙ' · xₙ)
--   =
--   ((c + c') + (k₀ + k₀') · x₀ + (k₁ + k₁') · x₁ + ... + (kₙ + kₙ') · xₙ)
plus :: IntTermNF -> IntTermNF -> IntTermNF
plus :: IntTermNF -> IntTermNF -> IntTermNF
plus IntTermNF{Map VariableIdentifier IntValue
coeff :: IntTermNF -> Map VariableIdentifier IntValue
coeff :: Map VariableIdentifier IntValue
coeff, IntValue
constant :: IntTermNF -> IntValue
constant :: IntValue
constant} IntTermNF{coeff :: IntTermNF -> Map VariableIdentifier IntValue
coeff = Map VariableIdentifier IntValue
coeff', constant :: IntTermNF -> IntValue
constant = IntValue
constant'} =
  IntTermNF{coeff :: Map VariableIdentifier IntValue
coeff = (IntValue -> Bool)
-> Map VariableIdentifier IntValue
-> Map VariableIdentifier IntValue
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (IntValue -> IntValue -> Bool
forall a. Eq a => a -> a -> Bool
/= IntValue
0) (Map VariableIdentifier IntValue
 -> Map VariableIdentifier IntValue)
-> Map VariableIdentifier IntValue
-> Map VariableIdentifier IntValue
forall a b. (a -> b) -> a -> b
$ (IntValue -> IntValue -> IntValue)
-> Map VariableIdentifier IntValue
-> Map VariableIdentifier IntValue
-> Map VariableIdentifier IntValue
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith IntValue -> IntValue -> IntValue
forall a. Num a => a -> a -> a
(+) Map VariableIdentifier IntValue
coeff Map VariableIdentifier IntValue
coeff', constant :: IntValue
constant = IntValue
constant IntValue -> IntValue -> IntValue
forall a. Num a => a -> a -> a
+ IntValue
constant'}

minus :: IntTermNF -> IntTermNF -> IntTermNF
minus :: IntTermNF -> IntTermNF -> IntTermNF
minus IntTermNF{Map VariableIdentifier IntValue
coeff :: IntTermNF -> Map VariableIdentifier IntValue
coeff :: Map VariableIdentifier IntValue
coeff, IntValue
constant :: IntTermNF -> IntValue
constant :: IntValue
constant} IntTermNF{coeff :: IntTermNF -> Map VariableIdentifier IntValue
coeff = Map VariableIdentifier IntValue
coeff', constant :: IntTermNF -> IntValue
constant = IntValue
constant'} =
  IntTermNF{coeff :: Map VariableIdentifier IntValue
coeff = (IntValue -> Bool)
-> Map VariableIdentifier IntValue
-> Map VariableIdentifier IntValue
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (IntValue -> IntValue -> Bool
forall a. Eq a => a -> a -> Bool
/= IntValue
0) (Map VariableIdentifier IntValue
 -> Map VariableIdentifier IntValue)
-> Map VariableIdentifier IntValue
-> Map VariableIdentifier IntValue
forall a b. (a -> b) -> a -> b
$ (IntValue -> IntValue -> IntValue)
-> Map VariableIdentifier IntValue
-> Map VariableIdentifier IntValue
-> Map VariableIdentifier IntValue
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith (-) Map VariableIdentifier IntValue
coeff Map VariableIdentifier IntValue
coeff', constant :: IntValue
constant = IntValue
constant IntValue -> IntValue -> IntValue
forall a. Num a => a -> a -> a
- IntValue
constant'}

-- | k * (c + k₀ · x₀ + k₁ · x₁ + ... + kₙ · xₙ)
--   =
--   ((k * c) + (k * k₀) · x₀ + (k * k₁) · x₁ + ... + (k * kₙ) · xₙ)
mul :: IntValue -> IntTermNF -> IntTermNF
mul :: IntValue -> IntTermNF -> IntTermNF
mul IntValue
k IntTermNF{IntValue
Map VariableIdentifier IntValue
coeff :: IntTermNF -> Map VariableIdentifier IntValue
constant :: IntTermNF -> IntValue
coeff :: Map VariableIdentifier IntValue
constant :: IntValue
..} = IntTermNF{constant :: IntValue
constant = IntValue
k IntValue -> IntValue -> IntValue
forall a. Num a => a -> a -> a
* IntValue
constant, coeff :: Map VariableIdentifier IntValue
coeff = (IntValue -> Bool)
-> Map VariableIdentifier IntValue
-> Map VariableIdentifier IntValue
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (IntValue -> IntValue -> Bool
forall a. Eq a => a -> a -> Bool
/= IntValue
0) (Map VariableIdentifier IntValue
 -> Map VariableIdentifier IntValue)
-> Map VariableIdentifier IntValue
-> Map VariableIdentifier IntValue
forall a b. (a -> b) -> a -> b
$ (IntValue -> IntValue)
-> Map VariableIdentifier IntValue
-> Map VariableIdentifier IntValue
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (IntValue -> IntValue -> IntValue
forall a. Num a => a -> a -> a
* IntValue
k) Map VariableIdentifier IntValue
coeff}

setCoeff :: IntValue -> VariableIdentifier -> IntTermNF -> IntTermNF
setCoeff :: IntValue -> VariableIdentifier -> IntTermNF -> IntTermNF
setCoeff IntValue
k VariableIdentifier
x IntTermNF{IntValue
Map VariableIdentifier IntValue
coeff :: IntTermNF -> Map VariableIdentifier IntValue
constant :: IntTermNF -> IntValue
coeff :: Map VariableIdentifier IntValue
constant :: IntValue
..} = IntTermNF{coeff :: Map VariableIdentifier IntValue
coeff = (IntValue -> Bool)
-> Map VariableIdentifier IntValue
-> Map VariableIdentifier IntValue
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (IntValue -> IntValue -> Bool
forall a. Eq a => a -> a -> Bool
/= IntValue
0) (Map VariableIdentifier IntValue
 -> Map VariableIdentifier IntValue)
-> Map VariableIdentifier IntValue
-> Map VariableIdentifier IntValue
forall a b. (a -> b) -> a -> b
$ VariableIdentifier
-> IntValue
-> Map VariableIdentifier IntValue
-> Map VariableIdentifier IntValue
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert VariableIdentifier
x IntValue
k Map VariableIdentifier IntValue
coeff, IntValue
constant :: IntValue
constant :: IntValue
constant}

nullify :: VariableIdentifier -> IntTermNF -> IntTermNF
nullify :: VariableIdentifier -> IntTermNF -> IntTermNF
nullify = IntValue -> VariableIdentifier -> IntTermNF -> IntTermNF
setCoeff IntValue
0

eval :: IntTerm -> IntTermNF
eval :: IntTerm -> IntTermNF
eval (IntConst IntValue
k)  = IntTermNF {coeff :: Map VariableIdentifier IntValue
coeff = Map VariableIdentifier IntValue
forall k a. Map k a
Map.empty, constant :: IntValue
constant = IntValue
k}
eval (IntVar IntValue
k VariableIdentifier
x)  = IntTermNF {coeff :: Map VariableIdentifier IntValue
coeff = (IntValue -> Bool)
-> Map VariableIdentifier IntValue
-> Map VariableIdentifier IntValue
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (IntValue -> IntValue -> Bool
forall a. Eq a => a -> a -> Bool
/= IntValue
0) (VariableIdentifier -> IntValue -> Map VariableIdentifier IntValue
forall k a. k -> a -> Map k a
Map.singleton VariableIdentifier
x IntValue
k), constant :: IntValue
constant = IntValue
0}
eval (IntSum IntTerm
a IntTerm
b)  = IntTerm -> IntTermNF
eval IntTerm
a IntTermNF -> IntTermNF -> IntTermNF
`plus` IntTerm -> IntTermNF
eval IntTerm
b

quote :: IntTermNF -> IntTerm
quote :: IntTermNF -> IntTerm
quote IntTermNF{IntValue
Map VariableIdentifier IntValue
coeff :: IntTermNF -> Map VariableIdentifier IntValue
constant :: IntTermNF -> IntValue
coeff :: Map VariableIdentifier IntValue
constant :: IntValue
..} | Map VariableIdentifier IntValue -> Bool
forall a. Map VariableIdentifier a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Map VariableIdentifier IntValue
coeff = IntValue -> IntTerm
IntConst IntValue
constant
quote IntTermNF{IntValue
Map VariableIdentifier IntValue
coeff :: IntTermNF -> Map VariableIdentifier IntValue
constant :: IntTermNF -> IntValue
coeff :: Map VariableIdentifier IntValue
constant :: IntValue
..} = IntTerm -> IntTerm -> IntTerm
IntSum (IntValue -> IntTerm
IntConst IntValue
constant) IntTerm
vars where
  -- [] case is impossible here due to the clause above
  (VariableIdentifier
x0, IntValue
k0) : [(VariableIdentifier, IntValue)]
rest = Map VariableIdentifier IntValue -> [(VariableIdentifier, IntValue)]
forall k a. Map k a -> [(k, a)]
Map.toList Map VariableIdentifier IntValue
coeff
  vars :: IntTerm
vars            = (IntTerm -> (VariableIdentifier, IntValue) -> IntTerm)
-> IntTerm -> [(VariableIdentifier, IntValue)] -> IntTerm
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' IntTerm -> (VariableIdentifier, IntValue) -> IntTerm
go (IntValue -> VariableIdentifier -> IntTerm
IntVar IntValue
k0 VariableIdentifier
x0) [(VariableIdentifier, IntValue)]
rest
  go :: IntTerm -> (VariableIdentifier, IntValue) -> IntTerm
go IntTerm
acc (VariableIdentifier
x, IntValue
k)   = IntTerm -> IntTerm -> IntTerm
IntSum IntTerm
acc (IntValue -> VariableIdentifier -> IntTerm
IntVar IntValue
k VariableIdentifier
x)

normalise :: IntTerm -> IntTerm
normalise :: IntTerm -> IntTerm
normalise = IntTermNF -> IntTerm
quote (IntTermNF -> IntTerm)
-> (IntTerm -> IntTermNF) -> IntTerm -> IntTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntTerm -> IntTermNF
eval