module Data.Boltzmann.System.Utils
( isEmptyAtZero
, zeroCoordinates
, wellFoundedAtZero
) where
import Data.Map (Map)
import qualified Data.Map.Strict as M
import Numeric.LinearAlgebra hiding (size)
import Data.Boltzmann.System
(.*) :: (Num a, Eq a) => a -> a -> a
0 .* _ = 0
_ .* 0 = 0
1 .* x = x
x .* 1 = x
x .* y = x * y
isEmptyAtZero :: (Eq a, Num a) => System a -> Bool
isEmptyAtZero sys = all isZeroType ts
where ts = M.toList $ defs sys
isZeroType (_, consL) = all isZeroCons consL
isZeroCons cons = not $ weight cons == 0 && null (args cons)
evalAtZero :: Num a => Arg -> a
evalAtZero (Type _) = 0
evalAtZero (List _) = 1
evalAtZeroL :: (Eq a, Num a) => [Arg] -> a
evalAtZeroL xs = foldl (.*) 1 $ map evalAtZero xs
derivTypeAtZero :: (Eq a, Eq b, Num a, Num b)
=> String -> [Cons b] -> a
derivTypeAtZero dt consL =
sum $ map (derivConsAtZero dt) consL
derivConsAtZero :: (Eq a, Eq b, Num a, Num b)
=> String -> Cons a -> b
derivConsAtZero dt cons
| weight cons /= 0 = 0
| otherwise = derivConsAtZeroL dt (args cons)
derivConsAtZeroL :: (Eq a, Num a)
=> String -> [Arg] -> a
derivConsAtZeroL _ [] = 1
derivConsAtZeroL dt (x:xs) = lhs + rhs
where lhs = evalAtZero x .* derivConsAtZeroL dt xs
rhs = derivAtZero dt x .* evalAtZeroL xs
derivAtZero :: Num a
=> String -> Arg -> a
derivAtZero dt arg
| argName arg /= dt = 0
| otherwise = 1
jacobian :: (Eq a, Num a) => System a -> Matrix Double
jacobian sys = (n><n) [idx i j | i <- [0..n-1], j <- [0..n-1]]
where n = size sys
ts = defs sys
idx i j =
let typ = snd $ M.elemAt i ts
dt = fst $ M.elemAt j ts
in derivTypeAtZero dt typ
isZero :: Matrix Double -> Bool
isZero mat = all (== 0) $ concat (toLists mat)
isNilpotent :: Matrix Double -> Bool
isNilpotent mat = isZero $ power mat m
where m = rows mat
square :: Matrix Double -> Matrix Double
square m = m <> m
power :: Integral a
=> Matrix Double -> a -> Matrix Double
power m 1 = m
power m n
| odd n = m <> square (power m $ n-1)
| otherwise = square (power m $ n `div` 2)
data Coordinate = Zero | Z deriving (Eq)
coord :: Coordinate -> Bool
coord Zero = True
coord Z = False
constrList :: System a -> String -> [Cons a]
constrList sys = (M.!) (defs sys)
zeroCoordinates :: System a -> Bool
zeroCoordinates sys = zeroCoordinates' sys m f
where f = M.fromSet (const Zero) $ types sys
m = size sys
zeroCoordinates' :: (Eq b, Num b)
=> System a -> b -> Map String Coordinate -> Bool
zeroCoordinates' _ 0 f = elem Zero $ M.elems f
zeroCoordinates' sys m f = zeroCoordinates' sys (m-1) f'
where xs = map (\k -> (k, mapF $ constrList sys k)) (M.keys f)
f' = M.fromAscList xs
mapF consL
| all (coord . mapF') consL = Zero
| otherwise = Z
mapF' cons
| any (coord . mapF'') (args cons) = Zero
| otherwise = Z
mapF'' (List _) = Z
mapF'' (Type t) =
case t `M.lookup` f of
Just Zero -> Zero
_ -> Z
wellFoundedAtZero :: (Eq a, Num a)
=> System a -> Bool
wellFoundedAtZero sys
| isNilpotent (jacobian sys) = not $ zeroCoordinates sys
| otherwise = False