diff options
Diffstat (limited to 'app')
| -rw-r--r-- | app/Web.hs | 280 |
1 files changed, 139 insertions, 141 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 |