summaryrefslogtreecommitdiff
path: root/app/Web.hs
diff options
context:
space:
mode:
Diffstat (limited to 'app/Web.hs')
-rw-r--r--app/Web.hs226
1 files changed, 226 insertions, 0 deletions
diff --git a/app/Web.hs b/app/Web.hs
new file mode 100644
index 0000000..7f7c2ba
--- /dev/null
+++ b/app/Web.hs
@@ -0,0 +1,226 @@
+{-# 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
+
+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 qualified Parser
+import Servant hiding ((:.))
+import Servant.HTML.Lucid
+import System.Timeout (timeout)
+import Web.HttpApiData
+
+data HomeView = HomeDefault | HomeError String String | HomeResult String Bool
+
+type HomeAPI =
+ QueryParam "theorem" String
+ :> Get '[HTML] HomeView
+
+type API = HomeAPI :<|> "static" :> Raw
+
+startApp :: IO ()
+startApp = run 9000 app
+
+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)
+ ]
+
+api :: Proxy API
+api = Proxy
+
+server :: Server API
+server = handleHome :<|> serveDirectoryWebApp "static/"
+
+------------------------------
+
+loggify :: E.Exception b => (b -> Handler a) -> b -> Handler a
+loggify f ex = do
+ liftIO $ print ex
+ f ex
+
+handleArbitraryException :: E.SomeException -> Handler a
+handleArbitraryException _ = throwError err500 {errBody = "500: An unexpected error occurred."}
+
+data AppException = BadTheorem String | Timeout deriving (Show)
+
+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"}
+
+handleHome :: Maybe String -> Handler HomeView
+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."
+
+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.Ax'.x+x'=x'+x", "addition is commutative."),
+ ("Ee.Ax.x+e=x", "there exists an additive identity."),
+ ("Ex.Ay.x>y", "there exists a largest natural."),
+ ("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."),
+ ("Ax.x+1!=0", "there is no natural whose successor is zero."),
+ ("(Ax.x=x & Ex.x=0 & Ex.x=1)", "the Sphinx is not an acolyte of prenex normal form.")
+ ]
+
+styles :: HomeView -> (String, String, [Attribute])
+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)])
+
+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 \
+ \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)
+ 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_ $ 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.φ"
+ toHtmlRaw = toHtml
+
+pageTemplate :: Monad m => [HtmlT m ()] -> HtmlT m () -> HtmlT m ()
+pageTemplate crumbs body = doctypehtml_ $ do
+ head_ $ 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_ "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"
+
+tshow :: Show a => a -> T.Text
+tshow = T.pack . show
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-16 23:26:38 +0000