diff options
| -rw-r--r-- | app/Web.hs | 280 | ||||
| -rw-r--r-- | src/Lib.hs | 379 | ||||
| -rw-r--r-- | src/Parser.hs | 189 |
3 files changed, 389 insertions, 459 deletions
@@ -1,33 +1,30 @@ {-# LANGUAGE DataKinds #-} -{-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE GeneralizedNewtypeDeriving #-} -{-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} -module Web (startApp) where +module Web + ( startApp + ) where -import qualified Control.Exception as E -import qualified Control.Exception.Safe as CES -import Control.Monad.IO.Class -import qualified Data.ByteString.Lazy.UTF8 as BLU -import qualified Data.List as L -import qualified Data.Text as T +import qualified Control.Exception as E +import qualified Control.Exception.Safe as CES +import Control.Monad.IO.Class +import qualified Data.ByteString.Lazy.UTF8 as BLU +import qualified Data.List as L +import qualified Data.Text as T import qualified Lib -import Lucid -import Network.Wai.Handler.Warp +import Lucid +import Network.Wai.Handler.Warp import qualified Parser -import Servant hiding ((:.)) -import Servant.HTML.Lucid -import System.Timeout (timeout) -import Web.HttpApiData +import Servant hiding ( (:.) ) +import Servant.HTML.Lucid +import System.Timeout ( timeout ) data HomeView = HomeDefault | HomeError String String | HomeResult String Bool @@ -44,12 +41,11 @@ app :: Application app = serve api $ hoistServer api handleErrors server handleErrors :: Handler a -> Handler a -handleErrors f = - CES.catches - f - [ CES.Handler (loggify handleAppException), - CES.Handler (loggify handleArbitraryException) - ] +handleErrors f = CES.catches + f + [ CES.Handler (loggify handleAppException) + , CES.Handler (loggify handleArbitraryException) + ] api :: Proxy API api = Proxy @@ -65,7 +61,8 @@ loggify f ex = do f ex handleArbitraryException :: E.SomeException -> Handler a -handleArbitraryException _ = throwError err500 {errBody = "500: An unexpected error occurred."} +handleArbitraryException _ = + throwError err500 { errBody = "500: An unexpected error occurred." } data AppException = BadTheorem String | Timeout deriving (Show) @@ -73,129 +70,132 @@ instance E.Exception AppException handleAppException :: AppException -> Handler a handleAppException (BadTheorem s) = - throwError err400 {errBody = "400: bad theorem: " <> BLU.fromString s} -handleAppException Timeout = - throwError err400 {errBody = "400: timeout"} + throwError err400 { errBody = "400: bad theorem: " <> BLU.fromString s } +handleAppException Timeout = throwError err400 { errBody = "400: timeout" } handleHome :: Maybe String -> Handler HomeView -handleHome Nothing = return HomeDefault +handleHome Nothing = return HomeDefault handleHome (Just "") = return HomeDefault -handleHome (Just f) = do - case Parser.parseMFormula f of - Left err -> return $ HomeError f err - Right theorem -> do - ret <- liftIO $ timeout 2000000 (pure $! Lib.eval theorem) - case ret of - Just ok -> return $ HomeResult f ok - Nothing -> return $ HomeError f "Timeout." +handleHome (Just f ) = case Parser.parseMFormula f of + Left err -> return $ HomeError f err + Right theorem -> do + ret <- liftIO $ timeout 2000000 (pure $! Lib.eval theorem) + case ret of + Just ok -> return $ HomeResult f ok + Nothing -> return $ HomeError f "Timeout." homeURI :: Maybe String -> T.Text homeURI f = "/" <> toUrlPiece (safeLink api (Proxy :: Proxy HomeAPI) f :: Link) examples :: [(String, String)] examples = - [ ("1+1=2", "one plus one equals two."), - ("Ax.Ay.x+y=y+x", "addition is commutative."), - ("Ex.Ay.x>y", "there exists a largest natural."), - ("Ee.Ae'.(Ax.e'+x=x <-> e=e')", "the additive identity exists and is unique."), - ("Ax.Ey.2y=x", "every natural is even."), - ("Ax.Ey.(2y=x | 2y+1=x)", "every natural is either even or odd."), - ("Ax.Ay.Az.((x=y & y=z) -> x=z)", "equality is transitive."), - ("Ax.Ay.(x<=y <-> y<=x)", "less-than-or-equal-to is symmetric."), - ("Ax.Ay.((x<=y & y<=x) -> x=y)", "less-than-or-equal-to is antisymmetric."), - ("Ax.Ay.(x+1=y+1 -> x=y)", "the successor function is injective.") + [ ("1+1=2" , "one plus one equals two.") + , ("Ax.Ay.x+y=y+x", "addition is commutative.") + , ("Ex.Ay.x>y" , "there exists a largest natural.") + , ( "Ee.Ae'.(Ax.e'+x=x <-> e=e')" + , "the additive identity exists and is unique." + ) + , ("Ax.Ey.2y=x" , "every natural is even.") + , ("Ax.Ey.(2y=x | 2y+1=x)" , "every natural is either even or odd.") + , ("Ax.Ay.Az.((x=y & y=z) -> x=z)", "equality is transitive.") + , ("Ax.Ay.(x<=y <-> y<=x)" , "less-than-or-equal-to is symmetric.") + , ("Ax.Ay.((x<=y & y<=x) -> x=y)" , "less-than-or-equal-to is antisymmetric.") + , ("Ax.Ay.(x+1=y+1 -> x=y)" , "the successor function is injective.") ] styles :: HomeView -> (String, String, [Attribute]) -styles HomeDefault = ("", "", []) +styles HomeDefault = ("", "", []) styles (HomeError f err) = ("error", "Error. " <> err, [value_ (T.pack f)]) -styles (HomeResult f True) = ("valid", "The theorem is valid.", [value_ (T.pack f)]) -styles (HomeResult f False) = ("invalid", "The theorem is invalid.", [value_ (T.pack f)]) +styles (HomeResult f True) = + ("valid", "The theorem is valid.", [value_ (T.pack f)]) +styles (HomeResult f False) = + ("invalid", "The theorem is invalid.", [value_ (T.pack f)]) instance ToHtml HomeView where - toHtml view = - pageTemplate - [a_ [href_ "https://git.cyfraeviolae.org/sumcheck", class_ "nonbreaking"] "source code"] - homeBody - where - (formclass, formtxt, inpval) = styles view - homeBody = div_ [class_ "narrow"] $ do - p_ $ do - span_ - "The diagonalizing sorcerer Roseacrucis has \ + toHtml view = pageTemplate + [ a_ [href_ "https://git.cyfraeviolae.org/sumcheck", class_ "nonbreaking"] + "source code" + ] + homeBody + where + (formclass, formtxt, inpval) = styles view + homeBody = div_ [class_ "narrow"] $ do + p_ $ do + span_ + "The diagonalizing sorcerer Roseacrucis has \ \resurrected the Sumcheck Sphinx; it blocks the entrance to the \ \Library. To defeat it, you must answer its many riddles, all of which \ \happen to consist of deciding the validity of theorems in the " - a_ - [href_ "https://en.wikipedia.org/wiki/Presburger_arithmetic"] - "first-order theory of the natural numbers with addition" - span_ "." - form_ [method_ "get", action_ "/", class_ (T.pack formclass)] $ do - p_ $ do - label_ [class_ "focus"] "theorem:" - input_ ([type_ "text", name_ "theorem"] ++ inpval) - p_ $ do - button_ [type_ "submit"] "Decide" - span_ [class_ "validity"] (toHtml formtxt) + a_ [href_ "https://en.wikipedia.org/wiki/Presburger_arithmetic"] + "first-order theory of the natural numbers with addition" + span_ "." + form_ [method_ "get", action_ "/", class_ (T.pack formclass)] $ do p_ $ do - span_ "The Sphinx asks its riddles in rapidfire succession, but accompanied by your faithful " - a_ - [href_ "http://t-yuyama.jp/pdfs/Decidability-of-Presburger-Arithmetic-via-Finite-Automata.pdf"] - "addition automaton" - span_ ", they are all summarily decided." - ul_ $ - mapM_ - ( \(theorem, description) -> li_ $ do - a_ [href_ (homeURI (Just theorem)), class_ "theorem"] (toHtml theorem) - span_ (toHtml $ ": " <> description) - ) - examples - br_ [] - p_ $ do - code_ "C-h p addition-automaton" - br_ [] - span_ "For constant " - code_ "c" - span_ " and variable " - code_ "x" - span_ ", the following are terms:" - ul_ $ do - li_ $ span_ [class_ "theorem"] "c" - li_ $ span_ [class_ "theorem"] "x" + label_ [class_ "focus"] "theorem:" + input_ ([type_ "text", name_ "theorem"] ++ inpval) p_ $ do - span_ "The following are addends:" - ul_ $ do - li_ $ span_ [class_ "theorem"] "c" - li_ $ span_ [class_ "theorem"] "x" - li_ $ span_ [class_ "theorem"] "cx" - p_ $ do - span_ "For addends " - code_ "a" - span_ " and " - code_ "b" - span_ ", terms " - code_ "t" - span_ " and " - code_ "r" - span_ ", and theorems " - code_ "φ" - span_ " and " - code_ "ψ" - span_ ", the following are theorems:" - ul_ $ do - li_ $ span_ [class_ "theorem"] "a+...=b+..." - li_ $ span_ [class_ "theorem"] "a+...!=b+..." - li_ $ span_ [class_ "theorem"] "t<=r" - li_ $ span_ [class_ "theorem"] "t<r" - li_ $ span_ [class_ "theorem"] "t>=r" - li_ $ span_ [class_ "theorem"] "t>r" - li_ $ span_ [class_ "theorem"] "(φ & ψ & ...)" - li_ $ span_ [class_ "theorem"] "(φ | ψ | ...)" - li_ $ span_ [class_ "theorem"] "(φ -> ψ)" - li_ $ span_ [class_ "theorem"] "(φ <-> ψ)" - li_ $ span_ [class_ "theorem"] "~φ" - li_ $ span_ [class_ "theorem"] "Ax.φ" - li_ $ span_ [class_ "theorem"] "Ex.φ" + button_ [type_ "submit"] "Decide" + span_ [class_ "validity"] (toHtml formtxt) + p_ $ do + span_ + "The Sphinx asks its riddles in rapidfire succession, but accompanied by your faithful " + a_ + [ href_ + "http://t-yuyama.jp/pdfs/Decidability-of-Presburger-Arithmetic-via-Finite-Automata.pdf" + ] + "addition automaton" + span_ ", they are all summarily decided." + ul_ $ mapM_ + (\(theorem, description) -> li_ $ do + a_ [href_ (homeURI (Just theorem)), class_ "theorem"] (toHtml theorem) + span_ (toHtml $ ": " <> description) + ) + examples + br_ [] + p_ $ do + code_ "C-h p addition-automaton" + br_ [] + span_ "For constant " + code_ "c" + span_ " and variable " + code_ "x" + span_ ", the following are terms:" + ul_ $ do + li_ $ span_ [class_ "theorem"] "c" + li_ $ span_ [class_ "theorem"] "x" + p_ $ span_ "The following are addends:" + ul_ $ do + li_ $ span_ [class_ "theorem"] "c" + li_ $ span_ [class_ "theorem"] "x" + li_ $ span_ [class_ "theorem"] "cx" + p_ $ do + span_ "For addends " + code_ "a" + span_ " and " + code_ "b" + span_ ", terms " + code_ "t" + span_ " and " + code_ "r" + span_ ", and theorems " + code_ "φ" + span_ " and " + code_ "ψ" + span_ ", the following are theorems:" + ul_ $ do + li_ $ span_ [class_ "theorem"] "a+...=b+..." + li_ $ span_ [class_ "theorem"] "a+...!=b+..." + li_ $ span_ [class_ "theorem"] "t<=r" + li_ $ span_ [class_ "theorem"] "t<r" + li_ $ span_ [class_ "theorem"] "t>=r" + li_ $ span_ [class_ "theorem"] "t>r" + li_ $ span_ [class_ "theorem"] "(φ & ψ & ...)" + li_ $ span_ [class_ "theorem"] "(φ | ψ | ...)" + li_ $ span_ [class_ "theorem"] "(φ -> ψ)" + li_ $ span_ [class_ "theorem"] "(φ <-> ψ)" + li_ $ span_ [class_ "theorem"] "~φ" + li_ $ span_ [class_ "theorem"] "Ax.φ" + li_ $ span_ [class_ "theorem"] "Ex.φ" toHtmlRaw = toHtml pageTemplate :: Monad m => [HtmlT m ()] -> HtmlT m () -> HtmlT m () @@ -204,21 +204,19 @@ pageTemplate crumbs body = doctypehtml_ $ do title_ "Sumcheck" meta_ [charset_ "utf-8"] meta_ [name_ "viewport", content_ "width=device-width, initial-scale=1.0"] - link_ [rel_ "shortcut icon", type_ "image/x-icon", href_ "/static/favicon.ico"] + link_ + [rel_ "shortcut icon", type_ "image/x-icon", href_ "/static/favicon.ico"] link_ [rel_ "stylesheet", type_ "text/css", href_ "/static/style.css"] - body_ $ - div_ [class_ "container"] $ do - div_ [class_ "row navbar"] $ - sequence_ $ - L.intersperse - (span_ [class_ "sep"] (toHtmlRaw (T.pack " | "))) - (crumb : crumbs) - body - where - crumb = span_ [class_ "ico"] $ do - a_ [href_ (homeURI Nothing), class_ "title"] (strong_ "Sumcheck") - span_ "@" - a_ [href_ "https://cyfraeviolae.org"] "cyfraeviolae.org" + body_ $ div_ [class_ "container"] $ do + div_ [class_ "row navbar"] $ sequence_ $ L.intersperse + (span_ [class_ "sep"] (toHtmlRaw (T.pack " | "))) + (crumb : crumbs) + body + where + crumb = span_ [class_ "ico"] $ do + a_ [href_ (homeURI Nothing), class_ "title"] (strong_ "Sumcheck") + span_ "@" + a_ [href_ "https://cyfraeviolae.org"] "cyfraeviolae.org" tshow :: Show a => a -> T.Text tshow = T.pack . show @@ -1,88 +1,85 @@ {-# 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 +import qualified Data.List as L +import qualified Data.Map as M +import Data.Maybe (fromJust) +import qualified Data.Set as S +import Parser + ( Addend (..), + Matrix (..), + QN (Neg, Qua), + QNMFormula (..), + Quantifier (Exists, ForAll), + ) 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) + eq (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) +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 + let dfa = automatizem dir m + mdfa = minDistinguishability dfa (length dir) + in minReachability (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 + in minReachability (length dir) (ncompl nfa) + where + md dfa = minDistinguishability dfa (length dir) + ncompl = nondeterminize . compl . md . 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 + in case M.lookup (Var v) dir of + Nothing -> nfa + (Just i) -> minReachability (length dir) $ existentialize i nfa +automatize _ (QNMFormula (Qua (ForAll, _) : _) _) = + error "should be universal-free" 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 +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 + let addends = L.sortOn snd (M.toList m) + reversedLiterals = map (\(a, _) -> addendReverseBinary a) addends + padTo = L.maximum (map length reversedLiterals) + paddedReversed = + map (\x -> x ++ replicate (padTo - length x) 0) reversedLiterals + padded = map reverse paddedReversed + in L.transpose padded addendReverseBinary :: Addend -> [Int] -addendReverseBinary (Var x) = [] +addendReverseBinary (Var _) = [] addendReverseBinary (Con n) = reverseBinary n -reverseBinary :: Integer -> [Int] +reverseBinary :: Int -> [Int] reverseBinary 0 = [] -reverseBinary n = fromIntegral (mod n 2) : reverseBinary (div n 2) +reverseBinary n = mod n 2 : reverseBinary (div n 2) eval :: QNMFormula -> Bool -eval f@(QNMFormula q m) = - let dir = (assign $ collect m) - nfa = automatize dir f +eval f@(QNMFormula _ m) = + let dir = (assign $ collect m) + nfa = automatize dir f input = literals (assign $ collect m) - in runNFA nfa input + in runNFA nfa input data State a = S a | Double (State a, State a) | Multi [State a] deriving (Eq, Ord, Show) @@ -93,137 +90,76 @@ 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) +minReachability :: (Ord a) => Int -> NFA [Int] a -> NFA [Int] a +minReachability 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' + +minDistinguishability :: (Ord a, Show a) => DFA [Int] a -> Int -> DFA [Int] a +minDistinguishability dfa@(DFA _ start accepts f) n = + let partition = hopcroftPartitionRefinement dfa n + states' = map head partition + start' = head $ head $ filter (L.elem start) partition + accepts' = L.intersect accepts states' + f' s c = let s' = f s c in head $ head $ filter (L.elem s') partition + in DFA states' start' accepts' f' + +hopcroftPartitionRefinement :: + (Ord a, Show a) => DFA [Int] a -> Int -> [[State a]] +hopcroftPartitionRefinement (DFA states _ accepts f) n = + let p0 = [states L.\\ accepts, accepts] in recurse p0 + where + sigma = chars n + normalizePartition partition = S.fromList (map S.fromList partition) + findInPartition xs x = fromJust $ L.find (L.elem x) xs + equalUnder partition x y = + findInPartition partition x == findInPartition partition y + indistinguishable partition x y = + all (\c -> equalUnder partition (f x c) (f y c)) sigma + partialRefine _ pk [] = pk + partialRefine pkPrev [] (x : xs) = partialRefine pkPrev [[x]] xs + partialRefine pkPrev pk (x : xs) = + case filter (\s -> indistinguishable pkPrev (head s) x) pk of + [] -> partialRefine pkPrev ([x] : pk) xs + [match] -> partialRefine pkPrev ((x : match) : L.delete match pk) xs + _ -> error "should be unreachable" + recurse pkPrev = + let pk = concatMap (partialRefine pkPrev []) pkPrev + in if normalizePartition pk == normalizePartition pkPrev + then pk + else recurse pk 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 + where + f' s c = filter (\state -> s `elem` f state c) states + +eq :: Int -> [Int] -> [Int] -> DFA [Int] Int +eq n is js = determinize $ minReachability 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 @@ -234,37 +170,38 @@ 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 +less op i j = DFA [S 0, S 1, S 2] (S 0) accepts f + where + accepts = if op == 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 +prod _ [] = [] +prod [] _ = [] +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) + 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 @@ -277,44 +214,46 @@ 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] + 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 = +closure nfa@(NFA _ _ _ f) cs initstates = let new = concatMap (\state -> concatMap (f state) cs) initstates - in if L.nub new L.\\ L.nub 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) +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 [] = [[]] 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]] + 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 :: Int -> [[Int]] chars 0 = [[]] chars n = let r = chars (n - 1) in map (1 :) r ++ map (0 :) r diff --git a/src/Parser.hs b/src/Parser.hs index 2d0798f..77cde09 100644 --- a/src/Parser.hs +++ b/src/Parser.hs @@ -3,29 +3,24 @@ 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 +import Control.Applicative +import qualified Data.Either.Combinators as E +import Data.Functor.Identity +import qualified Data.Set as S +import qualified Text.Parsec as Parsec + +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 +type Natural = Int data Addend = Var Symbol | Con Natural deriving (Show, Eq, Ord) @@ -49,7 +44,7 @@ data Formula pSymbol :: Parser Symbol pSymbol = Parsec.many1 (Parsec.oneOf $ ['a' .. 'z'] ++ ['\'']) -pNatural :: Parser Integer +pNatural :: Parser Int pNatural = read <$> Parsec.many1 Parsec.digit pAddend :: Parser Addend @@ -67,32 +62,35 @@ singleton a = [a] pSums :: String -> ([Addend] -> [Addend] -> a) -> Parser a pSums s op = do as <- f - Parsec.string s + _ <- 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 '+') + 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 + _ <- 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) + 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 + _ <- Parsec.space + _ <- Parsec.string s + _ <- Parsec.space y <- pFormulaInner return $ op x y @@ -117,13 +115,13 @@ pFormulaInner = <|> Parsec.try (pBinOp ">" Gt) <|> Parsec.try pNot <|> Parsec.between - (Parsec.char '(') - (Parsec.char ')') - ( Parsec.try (pMultiMatOp "&" And) + (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 @@ -141,60 +139,59 @@ data Matrix | MOr Matrix Matrix deriving (Eq, Show) -data MFormula = MFormula [(Quantifier, Symbol)] 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 (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 (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') + in MFormula [] (MAnd x' y') split (Or x y) = let MFormula [] x' = split x MFormula [] y' = split y - in MFormula [] (MOr x' y') + in MFormula [] (MOr x' y') renameAddend :: (Symbol -> Symbol) -> Addend -> Addend renameAddend f (Var x) = Var (f x) -renameAddend f x = 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) +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 (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 (Or x y) = pull (Or (prenex x) (prenex y)) prenex (Q q v x) = Q q v (prenex x) -prenex f = f +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 (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')) @@ -206,12 +203,12 @@ 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) +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) @@ -220,67 +217,63 @@ 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') + 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 +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 (Not x ) = boundvars x boundvars (And x y) = boundvars x ++ boundvars y -boundvars (Or x y) = boundvars x ++ boundvars y +boundvars (Or x y) = boundvars x ++ boundvars y boundvars (Q _ v f) = v : boundvars f -boundvars x = [] +boundvars _ = [] filtervars :: [Addend] -> [Symbol] -filtervars as = - concatMap - ( \case - (Var x) -> [x] - (Con x) -> [] - ) - as +filtervars = concatMap + (\case + (Var x) -> [x] + (Con _) -> [] + ) data QN = Qua (Quantifier, Symbol) | Neg deriving (Eq, Show) -data QNMFormula = QNMFormula [QN] Matrix 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 + in if q == ForAll then [Neg, qua, Neg] ++ ret else qua : ret simplifyNegsQua :: [QN] -> [QN] -simplifyNegsQua [] = [] +simplifyNegsQua [] = [] simplifyNegsQua (Neg : Neg : quas) = quas -simplifyNegsQua (qua : quas) = qua : simplifyNegsQua quas +simplifyNegsQua (qua : quas) = qua : simplifyNegsQua quas simplifyNegs :: MFormula -> QNMFormula simplifyNegs (MFormula quas m) = let quas' = (simplifyNegsQua . eliminateUniversals) quas - in QNMFormula quas' m + in QNMFormula quas' m anyUnboundVars :: Formula -> Bool -anyUnboundVars f = not $ S.null (S.fromList (vars f) S.\\ S.fromList (boundvars f)) +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) + 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 |