associativity for -> and <->

1 files changed, 138 insertions, 124 deletions

diff --git a/app/Web.hs b/app/Web.hs
index 7bc233b..a8a38ae 100644
--- a/app/Web.hs
+++ b/app/Web.hs
@@ -9,22 +9,23 @@
 {-# 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
+  ( 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 Lucid
+import Network.Wai.Handler.Warp
 import qualified Parser
-import           Servant                 hiding ( (:.) )
-import           Servant.HTML.Lucid
-import           System.Timeout                 ( timeout )
+import Servant hiding ((:.))
+import Servant.HTML.Lucid
+import System.Timeout (timeout)
 
 data HomeView = HomeDefault | HomeError String String | HomeResult String Bool
 
@@ -41,11 +42,12 @@ 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
@@ -62,7 +64,7 @@ loggify f ex = do
 
 handleArbitraryException :: E.SomeException -> Handler a
 handleArbitraryException _ =
-  throwError err500 { errBody = "500: An unexpected error occurred." }
+  throwError err500 {errBody = "500: An unexpected error occurred."}
 
 data AppException = BadTheorem String | Timeout deriving (Show)
 
@@ -70,14 +72,14 @@ 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 ) = case Parser.parseMFormula f of
-  Left  err     -> return $ HomeError f err
+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
@@ -89,22 +91,22 @@ 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)])
@@ -112,87 +114,96 @@ 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
+          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
-          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"
+          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_ []
-        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"
-        li_ $ span_ [class_ "theorem"] "cx"
-      p_ $ span_ "The following are relations:"
-      ul_ $ do
-        li_ $ span_ [class_ "theorem"] "="
-        li_ $ span_ [class_ "theorem"] "!="
-        li_ $ span_ [class_ "theorem"] "<="
-        li_ $ span_ [class_ "theorem"] "<"
-        li_ $ span_ [class_ "theorem"] ">="
-        li_ $ span_ [class_ "theorem"] ">"
-      p_ $ do
-        span_ "For terms "
-        code_ "a"
-        span_ " and "
-        code_ "b"
-        span_ ", relation "
-        code_ "★"
-        span_ ", and theorems "
-        code_ "φ"
-        span_ " and "
-        code_ "ψ"
-        span_ ", the following are theorems:"
-      ul_ $ do
-        li_ $ span_ [class_ "theorem"] "a+...★b+..."
-        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.φ"
+        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"
+          li_ $ span_ [class_ "theorem"] "cx"
+        p_ $ span_ "The following are relations:"
+        ul_ $ do
+          li_ $ span_ [class_ "theorem"] "="
+          li_ $ span_ [class_ "theorem"] "!="
+          li_ $ span_ [class_ "theorem"] "<="
+          li_ $ span_ [class_ "theorem"] "<"
+          li_ $ span_ [class_ "theorem"] ">="
+          li_ $ span_ [class_ "theorem"] ">"
+        p_ $ span_ "The following are operators:"
+        ul_ $ do
+          li_ $ span_ [class_ "theorem"] "&"
+          li_ $ span_ [class_ "theorem"] "|"
+          li_ $ span_ [class_ "theorem"] "->"
+          li_ $ span_ [class_ "theorem"] "<->"
+        p_ $ do
+          span_ "For terms "
+          code_ "a"
+          span_ " and "
+          code_ "b"
+          span_ ", relation "
+          code_ "★"
+          span_ ", operator "
+          code_ "∗"
+          span_ ", and theorems "
+          code_ "φ"
+          span_ " and "
+          code_ "ψ"
+          span_ ", the following are theorems:"
+        ul_ $ do
+          li_ $ span_ [class_ "theorem"] "a+...★b+..."
+          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,13 +215,16 @@ pageTemplate crumbs body = doctypehtml_ $ do
     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"