1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
|
{-# 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
[]
homeBody
where
(formclass, formtxt, inpval) = styles view
homeBody = div_ $ 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_ "."
br_ []
form_ [method_ "get", action_ "/sumcheck", class_ (T.pack formclass)] $ do
p_ $ do
label_ $ strong_ "theorem:"
input_ ([type_ "text", name_ "theorem"] ++ inpval)
p_ $ do
button_ [type_ "submit"] "Decide"
span_ [class_ "validity"] (toHtml formtxt)
br_ []
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_ "/static/styles.css"]
link_ [rel_ "stylesheet", type_ "text/css", href_ "/sumcheck/static/styles.css"]
body_ $
div_ [class_ "container"] $ do
div_ $ do
div_ [class_ "home"] $ do
a_ [href_ (homeURI Nothing), class_ "home-title"] (strong_ "Sumcheck")
span_ " at "
a_ [class_ "site", href_ "/"] "cyfraeviolae.org"
a_ [class_ "source", href_ "/git/sumcheck"] "[src]"
div_ [class_ "crumbs"] $ sequence_ $ L.intersperse
(span_ [class_ "sep"] (toHtmlRaw (T.pack " · ")))
crumbs
body
|
