summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Lib.hs214
-rw-r--r--src/Parser.hs288
2 files changed, 502 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
diff --git a/src/Parser.hs b/src/Parser.hs
new file mode 100644
index 0000000..c61cd79
--- /dev/null
+++ b/src/Parser.hs
@@ -0,0 +1,288 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE LambdaCase #-}
+
+module Parser where
+
+import Control.Applicative
+import qualified Data.Bifunctor
+import qualified Data.Either.Combinators as E
+import Data.Functor.Identity
+import qualified Data.List as L
+import qualified Data.Set as S
+import Text.Parsec ((<?>))
+import qualified Text.Parsec as Parsec
+import Text.Parsec.Language (haskellDef)
+import qualified Text.Parsec.Token as P
+
+pparse ::
+ Parsec.Stream s Data.Functor.Identity.Identity t =>
+ Parsec.Parsec s () a ->
+ s ->
+ Either Parsec.ParseError a
+pparse rule = Parsec.parse rule ""
+
+type Parser a = Parsec.Parsec String () a
+
+type Symbol = String
+
+type Natural = Integer
+
+data Addend = Var Symbol | Con Natural deriving (Show, Eq, Ord)
+
+data Quantifier = ForAll | Exists deriving (Show, Eq, Ord)
+
+data Formula
+ = Eq [Addend] [Addend]
+ | Ne [Addend] [Addend]
+ | Le Addend Addend
+ | Lt Addend Addend
+ | Ge Addend Addend
+ | Gt Addend Addend
+ | Not Formula
+ | And Formula Formula
+ | Or Formula Formula
+ | Imp Formula Formula
+ | Iff Formula Formula
+ | Q Quantifier Symbol Formula
+ deriving (Show)
+
+pSymbol :: Parser Symbol
+pSymbol = Parsec.many1 (Parsec.oneOf $ ['a' .. 'z'] ++ ['\''])
+
+pNatural :: Parser Integer
+pNatural = read <$> Parsec.many1 Parsec.digit
+
+pAddend :: Parser Addend
+pAddend = Var <$> pSymbol <|> Con <$> pNatural
+
+pTerm :: Parser [Addend]
+pTerm = do
+ c <- Parsec.option 1 pNatural
+ a <- pSymbol
+ return $ replicate (fromIntegral c) (Var a)
+
+singleton :: a -> [a]
+singleton a = [a]
+
+pSums :: String -> ([Addend] -> [Addend] -> a) -> Parser a
+pSums s op = do
+ as <- f
+ Parsec.string s
+ bs <- f
+ return $ op (concat as) (concat bs)
+ where
+ f = Parsec.sepBy1 (Parsec.try pTerm <|> Parsec.try (singleton . Con <$> pNatural)) (Parsec.char '+')
+
+pBinOp :: String -> (Addend -> Addend -> a) -> Parser a
+pBinOp s op = do
+ a <- pAddend
+ Parsec.string s
+ b <- pAddend
+ return $ op a b
+
+pMultiMatOp :: String -> (Formula -> Formula -> Formula) -> Parser Formula
+pMultiMatOp s op = do
+ term <- pFormulaInner
+ Parsec.space *> Parsec.string s *> Parsec.space
+ terms <- Parsec.sepBy1 pFormulaInner (Parsec.space *> Parsec.string s *> Parsec.space)
+ return $ foldl1 op (term : terms)
+
+pBinMatOp :: String -> (Formula -> Formula -> Formula) -> Parser Formula
+pBinMatOp s op = do
+ x <- pFormulaInner
+ Parsec.space
+ Parsec.string s
+ Parsec.space
+ y <- pFormulaInner
+ return $ op x y
+
+pNot :: Parser Formula
+pNot = Not <$> (Parsec.char '~' *> pFormulaInner)
+
+pQuantifier :: Parser Formula
+pQuantifier = do
+ q <- Parsec.oneOf ['A', 'E']
+ c <- pSymbol
+ Parsec.char '.'
+ f <- pFormulaInner
+ return $ Q (if q == 'A' then ForAll else Exists) c f
+
+pFormulaInner :: Parser Formula
+pFormulaInner =
+ Parsec.try (pSums "=" Eq)
+ <|> Parsec.try (pSums "!=" Ne)
+ <|> Parsec.try (pBinOp "<=" Le)
+ <|> Parsec.try (pBinOp "<" Lt)
+ <|> Parsec.try (pBinOp ">=" Ge)
+ <|> Parsec.try (pBinOp ">" Gt)
+ <|> Parsec.try pNot
+ <|> Parsec.between
+ (Parsec.char '(')
+ (Parsec.char ')')
+ ( Parsec.try (pMultiMatOp "&" And)
+ <|> Parsec.try (pMultiMatOp "|" Or)
+ <|> Parsec.try (pBinMatOp "<->" Iff)
+ <|> Parsec.try (pBinMatOp "->" Imp)
+ )
+ <|> Parsec.try pQuantifier
+
+pFormula :: Parser Formula
+pFormula = do
+ p <- pFormulaInner
+ Parsec.eof
+ return p
+
+data Matrix
+ = MEq [Addend] [Addend]
+ | MLe Addend Addend
+ | MLt Addend Addend
+ | MNot Matrix
+ | MAnd Matrix Matrix
+ | MOr Matrix Matrix
+ deriving (Eq, Show)
+
+data MFormula = MFormula [(Quantifier, Symbol)] Matrix deriving (Eq, Show)
+
+-- assumes simplified, pnf
+split :: Formula -> MFormula
+split (Q q v x) =
+ let (MFormula p m) = split x
+ in MFormula ((q, v) : p) m
+split (Eq as bs) = MFormula [] (MEq as bs)
+split (Le a b) = MFormula [] (MLe a b)
+split (Lt a b) = MFormula [] (MLt a b)
+split (Not x) =
+ let MFormula [] x' = split x
+ in MFormula [] (MNot x')
+split (And x y) =
+ let MFormula [] x' = split x
+ MFormula [] y' = split y
+ in MFormula [] (MAnd x' y')
+split (Or x y) =
+ let MFormula [] x' = split x
+ MFormula [] y' = split y
+ in MFormula [] (MOr x' y')
+
+(&) = And
+
+renameAddend :: (Symbol -> Symbol) -> Addend -> Addend
+renameAddend f (Var x) = Var (f x)
+renameAddend f x = x
+
+-- TODO restrict type?
+simplify :: Formula -> Formula
+simplify x@(Eq as bs) = x
+simplify (Ne as bs) = Not (Eq as bs)
+simplify x@(Le a b) = x
+simplify x@(Lt a b) = x
+simplify (Ge a b) = Le b a
+simplify (Gt a b) = Lt b a
+simplify (Not x) = Not (simplify x)
+simplify (And x y) = And (simplify x) (simplify y)
+simplify (Or x y) = Or (simplify x) (simplify y)
+simplify (Imp x y) = simplify (Or (Not x) y)
+simplify (Iff x y) = simplify (And (Imp x y) (Imp y x))
+simplify (Q q v f) = Q q v (simplify f)
+
+prenex :: Formula -> Formula
+prenex (Not x) = pull $ Not (prenex x)
+prenex (And x y) = pull (And (prenex x) (prenex y))
+prenex (Or x y) = pull (Or (prenex x) (prenex y))
+prenex (Q q v x) = Q q v (prenex x)
+prenex f = f
+
+pull :: Formula -> Formula
+pull (Not (Q ForAll x f)) = Q Exists x (pull (Not f))
+pull (Not (Q Exists x f)) = Q ForAll x (pull (Not f))
+pull (Not f) = Not f
+pull (And (Q q v x) y) = let (v', x') = fixup v x y in Q q v' (pull (And x' y))
+pull (And y (Q q v x)) = let (v', x') = fixup v x y in Q q v' (pull (And y x'))
+pull (And x y) = And x y
+pull (Or (Q q v x) y) = let (v', x') = fixup v x y in Q q v' (pull (Or x' y))
+pull (Or y (Q q v x)) = let (v', x') = fixup v x y in Q q v' (pull (Or y x'))
+pull (Or x y) = Or x y
+pull x = x
+
+newname :: Symbol -> [Symbol] -> Symbol
+newname x seen = if x `elem` seen then newname (x <> "'") seen else x
+
+rename :: (Symbol -> Symbol) -> Formula -> Formula
+rename f (Eq as bs) = Eq (renameAddend f <$> as) (renameAddend f <$> bs)
+rename f (Le a b) = Le (renameAddend f a) (renameAddend f b)
+rename f (Lt a b) = Lt (renameAddend f a) (renameAddend f b)
+rename f (Not x) = Not (rename f x)
+rename f (And x y) = And (rename f x) (rename f y)
+rename f (Or x y) = Or (rename f x) (rename f y)
+rename f (Q q v x) = Q q (f v) (rename f x)
+
+-- v is bound in x, other formula is y
+-- if v is either bound or free in y, then rename v in x (avoiding collisions in x or y)
+-- otherwise, leave as is
+fixup :: Symbol -> Formula -> Formula -> (Symbol, Formula)
+fixup v x y =
+ let xvars = vars x
+ yvars = vars y
+ v' =
+ if v `elem` yvars
+ then newname v (xvars ++ yvars)
+ else v
+ x' = rename (\z -> if z == v then v' else z) x
+ in (v', x')
+
+vars :: Formula -> [Symbol]
+vars (Eq as bs) = filtervars as ++ filtervars bs
+vars (Le a b) = filtervars [a, b]
+vars (Lt a b) = filtervars [a, b]
+vars (Not x) = vars x
+vars (And x y) = vars x ++ vars y
+vars (Or x y) = vars x ++ vars y
+vars (Q _ x f) = x : vars f
+
+boundvars :: Formula -> [Symbol]
+boundvars (Not x) = boundvars x
+boundvars (And x y) = boundvars x ++ boundvars y
+boundvars (Or x y) = boundvars x ++ boundvars y
+boundvars (Q _ v f) = v : boundvars f
+boundvars x = []
+
+filtervars :: [Addend] -> [Symbol]
+filtervars as =
+ concatMap
+ ( \case
+ (Var x) -> [x]
+ (Con x) -> []
+ )
+ as
+
+data QN = Qua (Quantifier, Symbol) | Neg deriving (Eq, Show)
+
+data QNMFormula = QNMFormula [QN] Matrix deriving (Eq, Show)
+
+eliminateUniversals :: [(Quantifier, Symbol)] -> [QN]
+eliminateUniversals [] = []
+eliminateUniversals ((q, v) : quas) =
+ let ret = eliminateUniversals quas
+ qua = Qua (Exists, v)
+ in if q == ForAll
+ then [Neg, qua, Neg] ++ ret
+ else qua : ret
+
+simplifyNegsQua :: [QN] -> [QN]
+simplifyNegsQua [] = []
+simplifyNegsQua (Neg : Neg : quas) = quas
+simplifyNegsQua (qua : quas) = qua : simplifyNegsQua quas
+
+simplifyNegs :: MFormula -> QNMFormula
+simplifyNegs (MFormula quas m) =
+ let quas' = (simplifyNegsQua . eliminateUniversals) quas
+ in QNMFormula quas' m
+
+anyUnboundVars :: Formula -> Bool
+anyUnboundVars f = not $ S.null (S.fromList (vars f) S.\\ S.fromList (boundvars f))
+
+parseMFormula :: String -> Either String QNMFormula
+parseMFormula s = do
+ formula <- E.mapLeft (flip (<>) "." . show) (prenex . simplify <$> pparse pFormula s)
+ if anyUnboundVars formula
+ then Left "All variables must be bound."
+ else Right $ simplifyNegs $ split formula