summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorcyfraeviolae <cyfraeviolae>2021-05-29 21:55:25 -0400
committercyfraeviolae <cyfraeviolae>2021-05-29 21:55:25 -0400
commit1f5e25758603870cbc8261935850ec9a922469f5 (patch)
treea06838f94e8c065336ab7c2c984b7bec0a5750f6
parentb76ffcb6e2bab640f6896dcdaaef2732edfd1617 (diff)
Cleanup hopcroft
-rw-r--r--app/Web.hs280
-rw-r--r--src/Lib.hs379
-rw-r--r--src/Parser.hs189
3 files changed, 389 insertions, 459 deletions
diff --git a/app/Web.hs b/app/Web.hs
index 89b6ac5..60b3120 100644
--- a/app/Web.hs
+++ b/app/Web.hs
@@ -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
diff --git a/src/Lib.hs b/src/Lib.hs
index 0e093e3..7bd27d2 100644
--- a/src/Lib.hs
+++ b/src/Lib.hs
@@ -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