Cleanup hopcroft

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