From 1da9b25ff814d681afc3b741739bffbca7cc45e8 Mon Sep 17 00:00:00 2001 From: cyfraeviolae Date: Sun, 16 May 2021 18:22:49 -0400 Subject: init --- src/Lib.hs | 214 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 214 insertions(+) create mode 100644 src/Lib.hs (limited to 'src/Lib.hs') 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 -- cgit v1.2.3