summaryrefslogtreecommitdiff
path: root/app
diff options
context:
space:
mode:
Diffstat (limited to 'app')
-rw-r--r--app/Web.hs280
1 files changed, 139 insertions, 141 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