1 files changed, 214 insertions, 0 deletions
diff --git a/src/Lib.hs b/src/Lib.hs
new file mode 100644
index 0000000..13dc4ac
--- /dev/null
+++ b/src/Lib.hs
@@ -0,0 +1,214 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TupleSections #-}
+
+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 ()
+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) = minimize (fromIntegral $ length dir) $ nondeterminize $ automatizem dir m
+automatize dir (QNMFormula (Neg : quas) m) =
+  let nfa = automatize dir (QNMFormula quas m)
+   in minimize (fromIntegral (length dir)) (ncompl nfa)
+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 = Single 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
+
+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 = Single <$> [- (length js - 1) .. length is - 1 + 1]
+    start = Single 0
+    accepts = [Single 0]
+    rejector = last states
+    f :: State Int -> [Int] -> State Int
+    f carrystate@(Single 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 Single 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 [Single 0, Single 1, Single 2] (Single 0) accepts f
+  where
+    accepts = if lt == LessEqual then [Single 0, Single 2] else [Single 2]
+    f s c = case (s, (c !! i, c !! j)) of
+      (Single 0, (1, 1)) -> Single 0
+      (Single 0, (0, 0)) -> Single 0
+      (Single 0, (1, 0)) -> Single 1
+      (Single 0, _) -> Single 2
+      (Single 1, _) -> Single 1
+      (_, _) -> Single 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
+
+ncompl :: (Ord a) => NFA c a -> NFA c a
+ncompl = nondeterminize . compl . determinize
+
+chars :: Integer -> [[Int]]
+chars 0 = [[]]
+chars n =
+  let r = chars (n -1)
+   in map (1 :) r ++ map (0 :) r
+
+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