{-
   Copyright 2017, Matthew Danish, Dominic Orchard, Andrew Rice, Mistral Contrastin

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
-}

{-# LANGUAGE TupleSections #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE PatternGuards #-}

module Camfort.Specification.Units.BackendTypes
  ( UnitSet, Dim, Sub, identDim, isIdentDim, dimFromUnitInfo, dimFromUnitInfos, dimToUnitInfo, dimToUnitInfos
  , subFromList, subToList, identSub, applySub, composeSubs, prop_composition, freeDimVars, dimSimplify
  , dimToConstraint, constraintToDim, dimMultiply, dimRaisePow, dimParamEq, dimParamEqCon, normaliseDim, dimFromList )
where

import qualified Data.Map.Strict as M
import qualified Data.Set as S
import Camfort.Specification.Units.Environment (UnitInfo(..), Constraint(..), flattenUnits, foldUnits, unitParamEq)
import Data.List (partition, foldl', foldl1', sortBy, maximumBy)
import Data.Ord (comparing)
import Data.Maybe (fromMaybe)

-- | Set of UnitInfos
type UnitSet = S.Set UnitInfo

-- | Represents a dimension: collection of units raised to a power,
-- multiplied together. Implemented as a map of unit -> power.
type Dim = M.Map UnitInfo Integer

-- | Represents a substitution: map of unit to be replaced ->
-- dimension to replace it with.
type Sub = M.Map UnitInfo Dim

-- Maintain invariant of Dim whereby all units raised to the zeroth
-- power are eliminated from the map.
removeZeroes :: Dim -> Dim
removeZeroes :: Dim -> Dim
removeZeroes = (UnitInfo -> Integer -> Bool) -> Dim -> Dim
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
M.filterWithKey UnitInfo -> Integer -> Bool
forall a. (Eq a, Num a) => UnitInfo -> a -> Bool
f
  where
    f :: UnitInfo -> a -> Bool
f UnitInfo
_ a
0           = Bool
False
    f UnitInfo
UnitlessVar a
_ = Bool
False
    f UnitInfo
UnitlessLit a
_ = Bool
False
    f UnitInfo
_ a
_           = Bool
True

-- Handy function to strip away the UnitPow & return the essence.
getUnitPow :: UnitInfo -> (UnitInfo, Integer)
getUnitPow :: UnitInfo -> (UnitInfo, Integer)
getUnitPow (UnitPow UnitInfo
u Double
p) = (UnitInfo
u', Double -> Integer
forall a b. (RealFrac a, Integral b) => a -> b
floor Double
p Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
p')
  where (UnitInfo
u', Integer
p') = UnitInfo -> (UnitInfo, Integer)
getUnitPow UnitInfo
u
getUnitPow UnitInfo
u = (UnitInfo
u, Integer
1)

-- | The identity Dim: 1.
identDim :: Dim
identDim :: Dim
identDim = Dim
forall k a. Map k a
M.empty

-- | Test for identity.
isIdentDim :: Dim -> Bool
isIdentDim :: Dim -> Bool
isIdentDim = Dim -> Bool
forall k a. Map k a -> Bool
M.null (Dim -> Bool) -> (Dim -> Dim) -> Dim -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dim -> Dim
removeZeroes

-- | Convert from list of implicitly multipled units into a Dim.
dimFromUnitInfos :: [UnitInfo] -> Dim
dimFromUnitInfos :: [UnitInfo] -> Dim
dimFromUnitInfos = [(UnitInfo, Integer)] -> Dim
dimFromList ([(UnitInfo, Integer)] -> Dim)
-> ([UnitInfo] -> [(UnitInfo, Integer)]) -> [UnitInfo] -> Dim
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UnitInfo -> (UnitInfo, Integer))
-> [UnitInfo] -> [(UnitInfo, Integer)]
forall a b. (a -> b) -> [a] -> [b]
map UnitInfo -> (UnitInfo, Integer)
getUnitPow

-- | Convert a UnitInfo to a Dim.
dimFromUnitInfo :: UnitInfo -> Dim
dimFromUnitInfo :: UnitInfo -> Dim
dimFromUnitInfo = [UnitInfo] -> Dim
dimFromUnitInfos ([UnitInfo] -> Dim) -> (UnitInfo -> [UnitInfo]) -> UnitInfo -> Dim
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnitInfo -> [UnitInfo]
flattenUnits

-- | Convert a Dim into an implicitly multipled list of units.
dimToUnitInfos :: Dim -> [UnitInfo]
dimToUnitInfos :: Dim -> [UnitInfo]
dimToUnitInfos = ((UnitInfo, Integer) -> UnitInfo)
-> [(UnitInfo, Integer)] -> [UnitInfo]
forall a b. (a -> b) -> [a] -> [b]
map (\ (UnitInfo
u, Integer
p) -> UnitInfo -> Double -> UnitInfo
UnitPow UnitInfo
u (Integer -> Double
forall a. Num a => Integer -> a
fromInteger Integer
p)) ([(UnitInfo, Integer)] -> [UnitInfo])
-> (Dim -> [(UnitInfo, Integer)]) -> Dim -> [UnitInfo]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dim -> [(UnitInfo, Integer)]
forall k a. Map k a -> [(k, a)]
M.toList

-- | Convert a Dim into a UnitInfo.
dimToUnitInfo :: Dim -> UnitInfo
dimToUnitInfo :: Dim -> UnitInfo
dimToUnitInfo = [UnitInfo] -> UnitInfo
forall (t :: * -> *). Foldable t => t UnitInfo -> UnitInfo
foldUnits ([UnitInfo] -> UnitInfo) -> (Dim -> [UnitInfo]) -> Dim -> UnitInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dim -> [UnitInfo]
dimToUnitInfos

-- | Convert a Constraint into a Dim where lhs/rhs is implicitly equal
-- to 1. Also normalise the powers by dividing by the gcd and making
-- the largest absolute value power be positive.
constraintToDim :: Constraint -> Dim
constraintToDim :: Constraint -> Dim
constraintToDim (ConEq UnitInfo
lhs UnitInfo
rhs) = Dim -> Dim
normaliseDim (UnitInfo -> Dim
dimFromUnitInfo UnitInfo
lhs Dim -> Dim -> Dim
`dimMultiply` Integer -> Dim -> Dim
dimRaisePow (-Integer
1) (UnitInfo -> Dim
dimFromUnitInfo UnitInfo
rhs))
constraintToDim (ConConj [Constraint]
cons)  = (Dim -> Dim -> Dim) -> Dim -> [Dim] -> Dim
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Dim -> Dim -> Dim
dimMultiply Dim
identDim ([Dim] -> Dim) -> [Dim] -> Dim
forall a b. (a -> b) -> a -> b
$ (Constraint -> Dim) -> [Constraint] -> [Dim]
forall a b. (a -> b) -> [a] -> [b]
map Constraint -> Dim
constraintToDim [Constraint]
cons

-- | Divide the powers of a dimension by their collective GCD.
normaliseDim :: Dim -> Dim
normaliseDim :: Dim -> Dim
normaliseDim Dim
dim
  | Dim -> Bool
forall k a. Map k a -> Bool
M.null Dim
dim = Dim
dim
  | Bool
otherwise  = (Integer -> Integer) -> Dim -> Dim
forall a b k. (a -> b) -> Map k a -> Map k b
M.map (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
divisor) Dim
dim
  where
    divisor :: Integer
divisor = (Integer
maxPow Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer -> Integer
forall a. Num a => a -> a
abs(Integer
maxPow)) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* [Integer] -> Integer
forall a. Integral a => [a] -> a
gcds (Dim -> [Integer]
forall k a. Map k a -> [a]
M.elems Dim
dim)
    maxPow :: Integer
maxPow  = (Integer -> Integer -> Ordering) -> [Integer] -> Integer
forall (t :: * -> *) a.
Foldable t =>
(a -> a -> Ordering) -> t a -> a
maximumBy ((Integer -> Integer) -> Integer -> Integer -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing Integer -> Integer
forall a. Num a => a -> a
abs) (Dim -> [Integer]
forall k a. Map k a -> [a]
M.elems Dim
dim)

    gcds :: [a] -> a
gcds []  = a
1
    gcds [a
x] = a
x
    gcds [a]
xs  = (a -> a -> a) -> [a] -> a
forall a. (a -> a -> a) -> [a] -> a
foldl1' a -> a -> a
forall a. Integral a => a -> a -> a
gcd [a]
xs

-- | Multiply two Dims
dimMultiply :: Dim -> Dim -> Dim
dimMultiply :: Dim -> Dim -> Dim
dimMultiply Dim
d1 Dim
d2 = Dim -> Dim
removeZeroes (Dim -> Dim) -> Dim -> Dim
forall a b. (a -> b) -> a -> b
$ (Integer -> Integer -> Integer) -> Dim -> Dim -> Dim
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) Dim
d1 Dim
d2

-- | Raise the dimension to the given power
dimRaisePow :: Integer -> Dim -> Dim
dimRaisePow :: Integer -> Dim -> Dim
dimRaisePow Integer
0 Dim
_ = Dim
identDim
dimRaisePow Integer
k Dim
d = (Integer -> Integer) -> Dim -> Dim
forall a b k. (a -> b) -> Map k a -> Map k b
M.map (Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
k) Dim
d

-- | Compare two Dims, not minding the difference between
-- UnitParam*Abs and UnitParam*Use versions of the polymorphic
-- constructors. Varies from a 'constraint parametric equality'
-- operator because it doesn't assume that dimRaisePow can be used
-- arbitrarily.
dimParamEq :: Dim -> Dim -> Bool
dimParamEq :: Dim -> Dim -> Bool
dimParamEq Dim
d1 Dim
d2 = [(UnitInfo, Integer)] -> [(UnitInfo, Integer)] -> Bool
dimParamEq' (Dim -> [(UnitInfo, Integer)]
forall k a. Map k a -> [(k, a)]
M.toList Dim
d1) (Dim -> [(UnitInfo, Integer)]
forall k a. Map k a -> [(k, a)]
M.toList Dim
d2)

dimParamEq' :: [(UnitInfo, Integer)] -> [(UnitInfo, Integer)] -> Bool
dimParamEq' :: [(UnitInfo, Integer)] -> [(UnitInfo, Integer)] -> Bool
dimParamEq' [] []             = Bool
True
dimParamEq' [] [(UnitInfo, Integer)]
_              = Bool
False
dimParamEq' ((UnitInfo
u1, Integer
p1):[(UnitInfo, Integer)]
d1') [(UnitInfo, Integer)]
d2 = case ((UnitInfo, Integer) -> Bool)
-> [(UnitInfo, Integer)]
-> ([(UnitInfo, Integer)], [(UnitInfo, Integer)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (UnitInfo -> UnitInfo -> Bool
unitParamEq UnitInfo
u1 (UnitInfo -> Bool)
-> ((UnitInfo, Integer) -> UnitInfo) -> (UnitInfo, Integer) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UnitInfo, Integer) -> UnitInfo
forall a b. (a, b) -> a
fst) [(UnitInfo, Integer)]
d2 of
  ((UnitInfo
u2, Integer
p2):[(UnitInfo, Integer)]
d2', [(UnitInfo, Integer)]
d2'') -> [(UnitInfo, Integer)] -> [(UnitInfo, Integer)] -> Bool
dimParamEq' ([(UnitInfo, Integer)]
rem1 [(UnitInfo, Integer)]
-> [(UnitInfo, Integer)] -> [(UnitInfo, Integer)]
forall a. [a] -> [a] -> [a]
++ [(UnitInfo, Integer)]
d1') ([(UnitInfo, Integer)]
rem2 [(UnitInfo, Integer)]
-> [(UnitInfo, Integer)] -> [(UnitInfo, Integer)]
forall a. [a] -> [a] -> [a]
++ [(UnitInfo, Integer)]
d2' [(UnitInfo, Integer)]
-> [(UnitInfo, Integer)] -> [(UnitInfo, Integer)]
forall a. [a] -> [a] -> [a]
++ [(UnitInfo, Integer)]
d2'')
    where
      ([(UnitInfo, Integer)]
rem1, [(UnitInfo, Integer)]
rem2) | Integer
p1 Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
p2  = ([], [])
                   | Integer
p1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
p2   = ([], [(UnitInfo
u2, Integer
p2 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
p1)])
                   | Integer
p1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
p2   = ([(UnitInfo
u1, Integer
p1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
p2)], [])
                   | Bool
otherwise = [Char] -> ([(UnitInfo, Integer)], [(UnitInfo, Integer)])
forall a. HasCallStack => [Char] -> a
error [Char]
"dimParamEq'"
  ([(UnitInfo, Integer)], [(UnitInfo, Integer)])
_ -> Bool
False

-- | Similar to dimParamEq but assume that dimRaisePow can be
-- arbitrarily applied to each of the parameters, because they now
-- represent the unit equation 'd = 1'. In practice this means
-- computing the GCD of the powers and dividing.
dimParamEqCon :: Dim -> Dim -> Bool
dimParamEqCon :: Dim -> Dim -> Bool
dimParamEqCon Dim
d1 Dim
d2 = Dim -> Dim
normaliseDim Dim
d1 Dim -> Dim -> Bool
`dimParamEq` Dim -> Dim
normaliseDim Dim
d2

-- | Create a constraint that the given Dim is equal to the identity unit.
dimToConstraint :: Dim -> Constraint
dimToConstraint :: Dim -> Constraint
dimToConstraint Dim
d = UnitInfo -> UnitInfo -> Constraint
ConEq (Dim -> UnitInfo
dimToUnitInfo Dim
positives) (Dim -> UnitInfo
dimToUnitInfo ((Integer -> Integer) -> Dim -> Dim
forall a b k. (a -> b) -> Map k a -> Map k b
M.map (Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* (-Integer
1)) Dim
negatives))
  where
    (Dim
negatives, Dim
positives) = (Integer -> Bool) -> Dim -> (Dim, Dim)
forall a k. (a -> Bool) -> Map k a -> (Map k a, Map k a)
M.partition (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0) Dim
d

-- | Convert a list of units paired with their corresponding power into a Dim.
dimFromList :: [(UnitInfo, Integer)] -> Dim
dimFromList :: [(UnitInfo, Integer)] -> Dim
dimFromList = Dim -> Dim
removeZeroes (Dim -> Dim)
-> ([(UnitInfo, Integer)] -> Dim) -> [(UnitInfo, Integer)] -> Dim
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer -> Integer -> Integer) -> [(UnitInfo, Integer)] -> Dim
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
M.fromListWith Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+)

-- | Convert a list of units paired with their corresponding
-- substitution (as a Dim) into a Sub. Note that this is equivalent to
-- repeatedly composing substitutions, so earlier substitutions will
-- affect later ones.
subFromList :: [(UnitInfo, Dim)] -> Sub
subFromList :: [(UnitInfo, Dim)] -> Sub
subFromList = (Sub -> Sub -> Sub) -> Sub -> [Sub] -> Sub
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Sub -> Sub -> Sub
composeSubs Sub
identSub ([Sub] -> Sub)
-> ([(UnitInfo, Dim)] -> [Sub]) -> [(UnitInfo, Dim)] -> Sub
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((UnitInfo, Dim) -> Sub) -> [(UnitInfo, Dim)] -> [Sub]
forall a b. (a -> b) -> [a] -> [b]
map ((UnitInfo -> Dim -> Sub) -> (UnitInfo, Dim) -> Sub
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry UnitInfo -> Dim -> Sub
forall k a. k -> a -> Map k a
M.singleton)

-- | Convert a Sub into an association-list format of unit mapped to unit.
subToList :: Sub -> [(UnitInfo, UnitInfo)]
subToList :: Sub -> [(UnitInfo, UnitInfo)]
subToList = ((UnitInfo, Dim) -> (UnitInfo, UnitInfo))
-> [(UnitInfo, Dim)] -> [(UnitInfo, UnitInfo)]
forall a b. (a -> b) -> [a] -> [b]
map ((Dim -> UnitInfo) -> (UnitInfo, Dim) -> (UnitInfo, UnitInfo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Dim -> UnitInfo
dimToUnitInfo) ([(UnitInfo, Dim)] -> [(UnitInfo, UnitInfo)])
-> (Sub -> [(UnitInfo, Dim)]) -> Sub -> [(UnitInfo, UnitInfo)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sub -> [(UnitInfo, Dim)]
forall k a. Map k a -> [(k, a)]
M.toList

-- | Identity substitution (empty).
identSub :: Sub
identSub :: Sub
identSub = Sub
forall k a. Map k a
M.empty

-- | Identity substitution filled out with some identity entries for a
-- certain set of units (useful for when two substitutions have
-- different sets of keys).
identSubWith :: [UnitInfo] -> Sub
identSubWith :: [UnitInfo] -> Sub
identSubWith = [(UnitInfo, Dim)] -> Sub
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(UnitInfo, Dim)] -> Sub)
-> ([UnitInfo] -> [(UnitInfo, Dim)]) -> [UnitInfo] -> Sub
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UnitInfo -> (UnitInfo, Dim)) -> [UnitInfo] -> [(UnitInfo, Dim)]
forall a b. (a -> b) -> [a] -> [b]
map (\ UnitInfo
u -> (UnitInfo
u, [(UnitInfo, Integer)] -> Dim
dimFromList [(UnitInfo
u, Integer
1)]))

-- | Apply a substitution to a dimension.
applySub :: Sub -> Dim -> Dim
applySub :: Sub -> Dim -> Dim
applySub Sub
sub Dim
dim =
  Dim -> Dim
removeZeroes (Dim -> Dim) -> Dim -> Dim
forall a b. (a -> b) -> a -> b
$ (Integer -> Integer -> Integer) -> [Dim] -> Dim
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
M.unionsWith Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) [ (Integer -> Integer) -> Dim -> Dim
forall a b k. (a -> b) -> Map k a -> Map k b
M.map (Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
*Integer
p) (UnitInfo -> Integer -> Dim
forall k a. k -> a -> Map k a
M.singleton UnitInfo
ui Integer
1 Dim -> Maybe Dim -> Dim
forall a. a -> Maybe a -> a
`fromMaybe` UnitInfo -> Sub -> Maybe Dim
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup UnitInfo
ui Sub
sub) | (UnitInfo
ui, Integer
p) <- Dim -> [(UnitInfo, Integer)]
forall k a. Map k a -> [(k, a)]
M.toList Dim
dim ]

-- | Compose two substitutions.
composeSubs :: Sub -> Sub -> Sub
composeSubs :: Sub -> Sub -> Sub
composeSubs Sub
sub1 Sub
sub2 = (Dim -> Dim) -> Sub -> Sub
forall a b k. (a -> b) -> Map k a -> Map k b
M.map (Sub -> Dim -> Dim
applySub Sub
sub1) ((Dim -> Dim -> Dim) -> Sub -> Sub -> Sub
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith (((Dim, Dim) -> Dim) -> Dim -> Dim -> Dim
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (Dim, Dim) -> Dim
forall a b. (a, b) -> b
snd) Sub
ident1 Sub
sub2)
  where
    ident1 :: Sub
ident1 = [UnitInfo] -> Sub
identSubWith (Sub -> [UnitInfo]
forall k a. Map k a -> [k]
M.keys Sub
sub1)

-- | Test the composition property: f (g x) == (f . g) x
prop_composition :: Dim -> Sub -> Sub -> Bool
prop_composition :: Dim -> Sub -> Sub -> Bool
prop_composition Dim
d Sub
s1 Sub
s2 = Sub -> Dim -> Dim
applySub Sub
s1 (Sub -> Dim -> Dim
applySub Sub
s2 Dim
d) Dim -> Dim -> Bool
forall a. Eq a => a -> a -> Bool
== Sub -> Dim -> Dim
applySub (Sub -> Sub -> Sub
composeSubs Sub
s1 Sub
s2) Dim
d

-- | Extract a list of 'free dimension variables' from a given Dim.
freeDimVars :: Dim -> [UnitInfo]
freeDimVars :: Dim -> [UnitInfo]
freeDimVars = (UnitInfo -> Bool) -> [UnitInfo] -> [UnitInfo]
forall a. (a -> Bool) -> [a] -> [a]
filter UnitInfo -> Bool
isVar ([UnitInfo] -> [UnitInfo])
-> (Dim -> [UnitInfo]) -> Dim -> [UnitInfo]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dim -> [UnitInfo]
forall k a. Map k a -> [k]
M.keys
  where
    isVar :: UnitInfo -> Bool
isVar (UnitParamPosAbs {}) = Bool
True
    isVar (UnitParamPosUse {}) = Bool
True
    isVar (UnitParamVarAbs {}) = Bool
True
    isVar (UnitParamVarUse {}) = Bool
True
    isVar (UnitParamLitAbs {}) = Bool
True
    isVar (UnitParamLitUse {}) = Bool
True
    isVar (UnitLiteral {})     = Bool
True
    isVar (UnitVar {})         = Bool
True
    isVar UnitInfo
_                    = Bool
False

-- | The 'dimSimplify' algorithm as shown in Kennedy's technical report Fig 3.4.
dimSimplify :: UnitSet -> Dim -> Sub
dimSimplify :: UnitSet -> Dim -> Sub
dimSimplify UnitSet
excludes Dim
dim
  | [(UnitInfo, Integer)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(UnitInfo, Integer)]
valids = Sub
identSub

  | (UnitInfo
u, Integer
x):[(UnitInfo, Integer)]
_ <- [(UnitInfo, Integer)]
valids, Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0
  , Sub
sub1     <- UnitInfo -> Dim -> Sub
forall k a. k -> a -> Map k a
M.singleton UnitInfo
u (UnitInfo -> Integer -> Dim
forall k a. k -> a -> Map k a
M.singleton UnitInfo
u (-Integer
1))
  , Sub
sub2     <- UnitSet -> Dim -> Sub
dimSimplify UnitSet
excludes (Sub -> Dim -> Dim
applySub Sub
sub1 Dim
dim) = Sub -> Sub -> Sub
composeSubs Sub
sub2 Sub
sub1

  | (UnitInfo
u, Integer
x):[] <- [(UnitInfo, Integer)]
valids = UnitInfo -> Dim -> Sub
forall k a. k -> a -> Map k a
M.singleton UnitInfo
u ([(UnitInfo, Integer)] -> Dim
dimFromList ((UnitInfo
u, Integer
1)(UnitInfo, Integer)
-> [(UnitInfo, Integer)] -> [(UnitInfo, Integer)]
forall a. a -> [a] -> [a]
:[(UnitInfo
v, -Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
div Integer
y Integer
x) | (UnitInfo
v, Integer
y) <- [(UnitInfo, Integer)]
invals]))

  | (UnitInfo
u, Integer
x):[(UnitInfo, Integer)]
_ <- [(UnitInfo, Integer)]
valids
  , Sub
sub1     <- UnitInfo -> Dim -> Sub
forall k a. k -> a -> Map k a
M.singleton UnitInfo
u ([(UnitInfo, Integer)] -> Dim
dimFromList ((UnitInfo
u, Integer
1)(UnitInfo, Integer)
-> [(UnitInfo, Integer)] -> [(UnitInfo, Integer)]
forall a. a -> [a] -> [a]
:[(UnitInfo
v, -Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
div Integer
y Integer
x) | (UnitInfo
v, Integer
y) <- Dim -> [(UnitInfo, Integer)]
forall k a. Map k a -> [(k, a)]
M.toList Dim
dim, UnitInfo
v UnitInfo -> UnitInfo -> Bool
forall a. Eq a => a -> a -> Bool
/= UnitInfo
u]))
  , Sub
sub2     <- UnitSet -> Dim -> Sub
dimSimplify UnitSet
excludes (Sub -> Dim -> Dim
applySub Sub
sub1 Dim
dim) = Sub -> Sub -> Sub
composeSubs Sub
sub2 Sub
sub1
  | Bool
otherwise = [Char] -> Sub
forall a. HasCallStack => [Char] -> a
error [Char]
"dimSimplify"
  where
    valids :: [(UnitInfo, Integer)]
valids   = ((UnitInfo, Integer) -> (UnitInfo, Integer) -> Ordering)
-> [(UnitInfo, Integer)] -> [(UnitInfo, Integer)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (((UnitInfo, Integer) -> Integer)
-> (UnitInfo, Integer) -> (UnitInfo, Integer) -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (Integer -> Integer
forall a. Num a => a -> a
abs (Integer -> Integer)
-> ((UnitInfo, Integer) -> Integer)
-> (UnitInfo, Integer)
-> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UnitInfo, Integer) -> Integer
forall a b. (a, b) -> b
snd)) ([(UnitInfo, Integer)] -> [(UnitInfo, Integer)])
-> ([(UnitInfo, Integer)] -> [(UnitInfo, Integer)])
-> [(UnitInfo, Integer)]
-> [(UnitInfo, Integer)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((UnitInfo, Integer) -> Bool)
-> [(UnitInfo, Integer)] -> [(UnitInfo, Integer)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((UnitInfo -> UnitSet -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.notMember` UnitSet
excludes) (UnitInfo -> Bool)
-> ((UnitInfo, Integer) -> UnitInfo) -> (UnitInfo, Integer) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UnitInfo, Integer) -> UnitInfo
forall a b. (a, b) -> a
fst) ([(UnitInfo, Integer)] -> [(UnitInfo, Integer)])
-> [(UnitInfo, Integer)] -> [(UnitInfo, Integer)]
forall a b. (a -> b) -> a -> b
$ Dim -> [(UnitInfo, Integer)]
forall k a. Map k a -> [(k, a)]
M.toList Dim
dim
    validSet :: UnitSet
validSet = [UnitInfo] -> UnitSet
forall a. Ord a => [a] -> Set a
S.fromList (((UnitInfo, Integer) -> UnitInfo)
-> [(UnitInfo, Integer)] -> [UnitInfo]
forall a b. (a -> b) -> [a] -> [b]
map (UnitInfo, Integer) -> UnitInfo
forall a b. (a, b) -> a
fst [(UnitInfo, Integer)]
valids)
    invals :: [(UnitInfo, Integer)]
invals   = ((UnitInfo, Integer) -> Bool)
-> [(UnitInfo, Integer)] -> [(UnitInfo, Integer)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((UnitInfo -> UnitSet -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.notMember` UnitSet
validSet) (UnitInfo -> Bool)
-> ((UnitInfo, Integer) -> UnitInfo) -> (UnitInfo, Integer) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UnitInfo, Integer) -> UnitInfo
forall a b. (a, b) -> a
fst) ([(UnitInfo, Integer)] -> [(UnitInfo, Integer)])
-> [(UnitInfo, Integer)] -> [(UnitInfo, Integer)]
forall a b. (a -> b) -> a -> b
$ Dim -> [(UnitInfo, Integer)]
forall k a. Map k a -> [(k, a)]
M.toList Dim
dim

-- testVar x = UnitVar (x, x)

-- u0 = testVar "u0"
-- u1 = testVar "u1"
-- u2 = testVar "u2"
-- u3 = testVar "u3"
-- u4 = testVar "u4"

-- dim1 = dimFromList [(u1, 6), (u2, 15), (u3, -7), (u4, 12)]
-- dim2 = dimFromList [(u1, 2), (u2, 15), (u3, -9)]

-- test1 = applySub (dimSimplify (S.fromList [u3,u4]) dim1) dim1 == dimFromList [(u2, 3), (u3, 2)]

-- test2 =  (dimSimplify (S.fromList [u0]) (dimFromList [(u0, 1), (u1, -2)]))