path: root/src/Lib.hs

{-# LANGUAGE TupleSections #-}
{-# LANGUAGE BangPatterns #-}

module Lib where

import           Data.Char                      ( chr
                                                , ord
                                                )
import qualified Data.List                     as L
import qualified Data.Map                      as M
import           Data.Maybe                     ( fromJust )
import qualified Data.Set                      as S
import           Debug.Trace                    ( traceShowId
                                                , traceShow
                                                )
import           Parser
import qualified Text.Parsec                   as Parsec

mget :: (Ord a) => a -> M.Map a b -> b
mget a m = fromJust $ M.lookup a m

automatizem :: M.Map Addend Int -> Matrix -> DFA [Int] Int
automatizem dir (MEq as bs) =
  eq (fromIntegral $ length dir) (map (`mget` dir) as) (map (`mget` dir) bs)
automatizem dir (MLe  a b) = le (mget a dir) (mget b dir)
automatizem dir (MLt  a b) = lt (mget a dir) (mget b dir)
automatizem dir (MAnd x y) = conj (automatizem dir x) (automatizem dir y)
automatizem dir (MOr  x y) = disj (automatizem dir x) (automatizem dir y)
automatizem dir (MNot x  ) = compl (automatizem dir x)

automatize :: M.Map Addend Int -> QNMFormula -> NFA [Int] Int
automatize dir (QNMFormula [] m) =
  let dfa@( DFA s  _ _ _) = automatizem dir m
      mdfa@(DFA s' _ _ _) = rmdist dfa (fromIntegral (length dir))
      !t                  = (traceShowId $ (length s, length s'))
  in  minimize (fromIntegral $ length dir) $ nondeterminize $ mdfa
automatize dir (QNMFormula (Neg : quas) m) =
  let nfa = automatize dir (QNMFormula quas m)
  in  minimize (fromIntegral (length dir)) (ncompl nfa)
 where
  rmmin d = rmdist d (fromIntegral (length dir))
  ncompl = nondeterminize . compl . rmmin . determinize
automatize dir (QNMFormula (Qua (Exists, v) : quas) m) =
  let nfa = automatize dir (QNMFormula quas m)
  in  case M.lookup (Var v) dir of
        Nothing  -> nfa
        (Just i) -> minimize (fromIntegral $ length dir) $ existentialize i nfa

assign :: S.Set Addend -> M.Map Addend Int
assign xs = M.fromList (zip (S.toList xs) [0 ..])

collect :: Matrix -> S.Set Addend
collect (MEq  as bs) = S.fromList (as ++ bs)
collect (MLe  a  b ) = S.fromList [a, b]
collect (MLt  a  b ) = S.fromList [a, b]
collect (MAnd x  y ) = S.union (collect x) (collect y)
collect (MOr  x  y ) = S.union (collect x) (collect y)
collect (MNot x    ) = collect x

literals :: M.Map Addend Int -> [[Int]]
literals m =
  let
    addends          = L.sortOn snd (M.toList m)
    reversedLiterals = map (\(a, i) -> addendReverseBinary a) addends
    max              = L.maximum (map length reversedLiterals)
    paddedReversed =
      map (\x -> x ++ replicate (max - length x) 0) reversedLiterals
    padded = map reverse paddedReversed
  in
    L.transpose padded

addendReverseBinary :: Addend -> [Int]
addendReverseBinary (Var x) = []
addendReverseBinary (Con n) = reverseBinary n

reverseBinary :: Integer -> [Int]
reverseBinary 0 = []
reverseBinary n = fromIntegral (mod n 2) : reverseBinary (div n 2)

eval :: QNMFormula -> Bool
eval f@(QNMFormula q m) =
  let dir   = (assign $ collect m)
      nfa   = automatize dir f
      input = literals (assign $ collect m)
  in  runNFA nfa input

data State a = S a | Double (State a, State a) | Multi [State a] deriving (Eq, Ord, Show)

data DFA c a = DFA [State a] (State a) [State a] (State a -> c -> State a)

data NFA c a = NFA [State a] [State a] [State a] (State a -> c -> [State a])

runDFA :: (Ord a) => DFA c a -> [c] -> Bool
runDFA (DFA _ start accepts f) cs = foldl f start cs `elem` accepts

minimize :: (Ord a) => Integer -> NFA [Int] a -> NFA [Int] a
minimize n nfa@(NFA _ starts accepts f) = NFA states' starts' accepts' f
 where
  states'  = closure nfa (chars n) starts
  starts'  = starts `L.intersect` states'
  accepts' = accepts `L.intersect` states'


rmdist :: (Ord a, Show a) => DFA [Int] a -> Integer -> DFA [Int] a
rmdist dfa@(DFA states start accepts f) n =
  let
    statecandidates = minimize2 dfa n
    states'         = map head statecandidates
    start' = head $ head $ filter (\c -> L.elem start c) statecandidates
    accepts'        = L.intersect accepts states'
    f' s c =
      let s' = f s c
      in  head $ head $ filter (\c -> L.elem s' c) statecandidates
  in
    DFA states' start' accepts' f'


minimize2 :: (Ord a, Show a) => DFA [Int] a -> Integer -> [[State a]]
minimize2 dfa@(DFA states start accepts f) n =
  let p0 = [states L.\\ accepts, accepts] in minrec dfa n p0

minrec
  :: (Ord a, Show a) => DFA [Int] a -> Integer -> [[State a]] -> [[State a]]
minrec dfa n pklast =
  let next = concatMap (\part -> minimize3 dfa n pklast [] part) pklast
  in  if normpartition next == normpartition pklast
        then next
        else minrec dfa n next

normpartition :: Ord a => [[a]] -> S.Set (S.Set a)
normpartition xs = S.fromList (map S.fromList xs)


minimize3
  :: (Ord a, Show a)
  => DFA [Int] a
  -> Integer
  -> [[State a]]
  -> [[State a]]
  -> [State a]
  -> [[State a]]
minimize3 dfa@(DFA states starts accepts f) n pklast pk [] = pk
minimize3 dfa@(DFA states starts accepts f) n pklast [] (x : xs) =
  minimize3 dfa n pklast [[x]] xs
minimize3 dfa@(DFA states starts accepts f) n pklast pk (x : xs) =
  let ys = filter (\s -> equivall dfa pklast (chars n) (head s) x) pk
  in  if ys == []
        then minimize3 dfa n pklast ([x] : pk) xs
        else
          let coll  = (head ys)
              trunc = L.delete coll pk
              new   = x : coll
              pk'   = new : trunc
          in  minimize3 dfa n pklast pk' xs

equivall
  :: (Eq a)
  => DFA [Int] a
  -> [[State a]]
  -> [[Int]]
  -> (State a)
  -> (State a)
  -> Bool
equivall dfa partition cs x y = all (\c -> not $ dist dfa partition c x y) cs

states = S <$> [0, 1, 2, 3, 4]
start = S 0
accepts = [S 4]
f (S 0) [0] = S 1
f (S 0) [1] = S 2
f (S 1) [0] = S 1
f (S 1) [1] = S 3
f (S 2) [0] = S 1
f (S 2) [1] = S 2
f (S 3) [0] = S 1
f (S 3) [1] = S 4
f (S 4) [0] = S 1
f (S 4) [1] = S 2
dfa = DFA states start accepts f
p0 = [states L.\\ accepts, accepts]
p1 = concatMap (minimize3 dfa 1 p0 []) p0
p2 = concatMap (minimize3 dfa 1 p1 []) p1
minp = minimize2 dfa 1


dist
  :: (Eq a)
  => DFA [Int] a
  -> [[State a]]
  -> [Int]
  -> (State a)
  -> (State a)
  -> Bool
dist (DFA states starts accepts f) partition c x y =
  (findset partition (f x c)) /= (findset partition (f y c))

findset :: (Eq a) => [[State a]] -> State a -> [State a]
findset xs x = head (filter (\s -> L.elem x s) xs)

runNFA :: (Ord a) => NFA c a -> [c] -> Bool
runNFA (NFA _ starts accepts f) cs =
  foldl (\xs c -> L.nub $ concatMap (`f` c) xs) starts cs
    `L.intersect` accepts
    /=            []

reversal :: (Ord a) => NFA c a -> NFA c a
reversal (NFA states starts accepts f) = NFA states accepts starts f'
  where f' s c = filter (\state -> s `elem` f state c) states

eq :: Integer -> [Int] -> [Int] -> DFA [Int] Int
eq n is js = determinize $ minimize n $ reversal $ nondeterminize dfa
 where
  states   = S <$> [-(length js - 1) .. length is - 1 + 1]
  start    = S 0
  accepts  = [S 0]
  rejector = last states
  f :: State Int -> [Int] -> State Int
  f carrystate@(S carry) c = if carrystate == rejector
    then rejector
    else
      let si       = sum (map ((c) !!) (is))
          sj       = sum (map (c !!) (js))
          parityok = mod (carry + si) 2 == mod sj 2
          newcarry = div (carry + si - sj) 2
      in  if parityok then S newcarry else rejector
  dfa = DFA states start accepts f

le :: Int -> Int -> DFA [Int] Int
le = less LessEqual

lt :: Int -> Int -> DFA [Int] Int
lt = less LessThan

data LessType = LessEqual | LessThan deriving (Eq, Ord, Show)

less :: LessType -> Int -> Int -> DFA [Int] Int
less lt i j = DFA [S 0, S 1, S 2] (S 0) accepts f
 where
  accepts = if lt == LessEqual then [S 0, S 2] else [S 2]
  f s c = case (s, (c !! i, c !! j)) of
    (S 0, (1, 1)) -> S 0
    (S 0, (0, 0)) -> S 0
    (S 0, (1, 0)) -> S 1
    (S 0, _     ) -> S 2
    (S 1, _     ) -> S 1
    (_  , _     ) -> S 2

prod :: [a] -> [b] -> [(a, b)]
prod xs       [] = []
prod []       ys = []
prod (x : xs) ys = fmap (x, ) ys ++ prod xs ys

data JunctionType = Conj | Disj deriving (Eq, Ord, Show)

junction :: (Ord a) => JunctionType -> DFA c a -> DFA c a -> DFA c a
junction jt (DFA states1 start1 accepts1 f1) (DFA states2 start2 accepts2 f2) =
  DFA states' start' accepts' f'
 where
  newStates = prod states1 states2
  states'   = Double <$> newStates
  start'    = Double (start1, start2)
  accepts'  = if jt == Conj
    then Double <$> prod accepts1 accepts2
    else
      Double
        <$> filter (\(s, t) -> s `elem` accepts1 || t `elem` accepts2) newStates
  f' (Double (s, t)) c = Double (f1 s c, f2 t c)

conj :: (Ord a) => DFA c a -> DFA c a -> DFA c a
conj = junction Conj

disj :: (Ord a) => DFA c a -> DFA c a -> DFA c a
disj = junction Disj

compl :: (Ord a) => DFA c a -> DFA c a
compl (DFA states start accepts f) = DFA states start (states L.\\ accepts) f

nondeterminize :: (Ord a) => DFA c a -> NFA c a
nondeterminize (DFA states start accepts f) = NFA states [start] accepts f'
  where f' s c = [f s c]

change :: [a] -> Int -> a -> [a]
change xs idx b = take idx xs ++ [b] ++ drop (idx + 1) xs

closure :: (Ord a) => NFA c a -> [c] -> [State a] -> [State a]
closure nfa@(NFA states starts accepts f) cs initstates =
  let new = concatMap (\state -> concatMap (f state) cs) initstates
  in  if L.nub new L.\\ L.nub initstates /= []
        then closure nfa cs (L.nub $ new ++ initstates)
        else L.nub initstates

existentialize :: (Ord a) => Int -> NFA [Int] a -> NFA [Int] a
existentialize idx nfa@(NFA states starts accepts f) = NFA states
                                                           starts'
                                                           accepts
                                                           f'
 where
  zeroer  = replicate 50 0
  oneer   = change zeroer idx 1
  starts' = closure nfa [zeroer, oneer] starts
  f' s c = f s (change c idx 0) ++ f s (change c idx 1)

powerset :: [a] -> [[a]]
powerset []       = [[]]
powerset (x : xs) = let rest = powerset xs in map (x :) rest ++ rest

determinize :: (Ord a) => NFA c a -> DFA c a
determinize (NFA states start accepts f) = DFA states' start' accepts' f'
 where
  newStates = map L.sort $ powerset states
  states'   = Multi <$> newStates
  start'    = Multi $ L.sort start
  accepts' =
    Multi <$> filter (\state' -> state' `L.intersect` accepts /= []) newStates
  f' (Multi s) c = Multi $ L.nub $ L.sort $ concatMap (`f` c) s


chars :: Integer -> [[Int]]
chars 0 = [[]]
chars n = let r = chars (n - 1) in map (1 :) r ++ map (0 :) r