diff options
| -rw-r--r-- | app/Web.hs | 262 | ||||
| -rw-r--r-- | src/Parser.hs | 17 |
2 files changed, 143 insertions, 136 deletions
@@ -9,22 +9,23 @@ {-# LANGUAGE UndecidableInstances #-} 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 + ( 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 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 Servant hiding ((:.)) +import Servant.HTML.Lucid +import System.Timeout (timeout) data HomeView = HomeDefault | HomeError String String | HomeResult String Bool @@ -41,11 +42,12 @@ 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 @@ -62,7 +64,7 @@ loggify f ex = do handleArbitraryException :: E.SomeException -> Handler a handleArbitraryException _ = - throwError err500 { errBody = "500: An unexpected error occurred." } + throwError err500 {errBody = "500: An unexpected error occurred."} data AppException = BadTheorem String | Timeout deriving (Show) @@ -70,14 +72,14 @@ 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 ) = case Parser.parseMFormula f of - Left err -> return $ HomeError f err +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 @@ -89,22 +91,22 @@ 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)]) @@ -112,87 +114,96 @@ 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 + 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) p_ $ do - label_ [class_ "focus"] "theorem:" - input_ ([type_ "text", name_ "theorem"] ++ inpval) - p_ $ do - 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" + 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_ [] - 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" - li_ $ span_ [class_ "theorem"] "cx" - p_ $ span_ "The following are relations:" - ul_ $ do - li_ $ span_ [class_ "theorem"] "=" - li_ $ span_ [class_ "theorem"] "!=" - li_ $ span_ [class_ "theorem"] "<=" - li_ $ span_ [class_ "theorem"] "<" - li_ $ span_ [class_ "theorem"] ">=" - li_ $ span_ [class_ "theorem"] ">" - p_ $ do - span_ "For terms " - code_ "a" - span_ " and " - code_ "b" - span_ ", relation " - code_ "★" - span_ ", and theorems " - code_ "φ" - span_ " and " - code_ "ψ" - span_ ", the following are theorems:" - ul_ $ do - li_ $ span_ [class_ "theorem"] "a+...★b+..." - 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.φ" + 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" + li_ $ span_ [class_ "theorem"] "cx" + p_ $ span_ "The following are relations:" + ul_ $ do + li_ $ span_ [class_ "theorem"] "=" + li_ $ span_ [class_ "theorem"] "!=" + li_ $ span_ [class_ "theorem"] "<=" + li_ $ span_ [class_ "theorem"] "<" + li_ $ span_ [class_ "theorem"] ">=" + li_ $ span_ [class_ "theorem"] ">" + p_ $ span_ "The following are operators:" + ul_ $ do + li_ $ span_ [class_ "theorem"] "&" + li_ $ span_ [class_ "theorem"] "|" + li_ $ span_ [class_ "theorem"] "->" + li_ $ span_ [class_ "theorem"] "<->" + p_ $ do + span_ "For terms " + code_ "a" + span_ " and " + code_ "b" + span_ ", relation " + code_ "★" + span_ ", operator " + code_ "∗" + span_ ", and theorems " + code_ "φ" + span_ " and " + code_ "ψ" + span_ ", the following are theorems:" + ul_ $ do + li_ $ span_ [class_ "theorem"] "a+...★b+..." + 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,13 +215,16 @@ pageTemplate crumbs body = doctypehtml_ $ do 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" diff --git a/src/Parser.hs b/src/Parser.hs index e328b6e..0891481 100644 --- a/src/Parser.hs +++ b/src/Parser.hs @@ -79,16 +79,9 @@ pMultiMatOp s op = do 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 + -- Imp is right-associative, whereas And/Or/Iff can be either, so + -- use right-associative for everything. + return $ foldr1 op (term : terms) pNot :: Parser Formula pNot = Not <$> (Parsec.char '~' *> pFormulaInner) @@ -115,8 +108,8 @@ pFormulaInner = (Parsec.char ')') ( Parsec.try (pMultiMatOp "&" And) <|> Parsec.try (pMultiMatOp "|" Or) - <|> Parsec.try (pBinMatOp "<->" Iff) - <|> Parsec.try (pBinMatOp "->" Imp) + <|> Parsec.try (pMultiMatOp "<->" Iff) + <|> Parsec.try (pMultiMatOp "->" Imp) ) <|> Parsec.try pQuantifier |