init

2 files changed, 232 insertions, 0 deletions

diff --git a/app/Main.hs b/app/Main.hs
new file mode 100644
index 0000000..b69a962
--- /dev/null
+++ b/app/Main.hs
@@ -0,0 +1,6 @@
+module Main where
+
+import Web
+
+main :: IO ()
+main = startApp
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