{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# 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)

data HomeView = HomeDefault | HomeError String String | HomeResult String Bool

type HomeAPI =
  "sumcheck" :>
  QueryParam "theorem" String
    :> Get '[HTML] HomeView

type StaticAPI = "sumcheck" :> "static" :> Raw

type API = HomeAPI :<|> StaticAPI

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) = 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.")
  ]

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://cyfraeviolae.org/git/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_ "/sumcheck", 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"
          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 ()
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_ "/sumcheck/static/favicon.ico"]
    link_ [rel_ "stylesheet", type_ "text/css", href_ "/sumcheck/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"