init

20 files changed, 1227 insertions, 0 deletions

diff --git a/LICENSE b/LICENSE
new file mode 100644
index 0000000..fe9baac
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,16 @@
+Sumcheck
+Copyright (C) 2020 cyfraeviolae.org
+
+This program is free software: you can redistribute it and/or modify
+it under the terms of the GNU Affero General Public License as
+published by the Free Software Foundation, either version 3 of the
+License, or (at your option) any later version.
+
+This program is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+GNU Affero General Public License for more details.
+
+You should have received a copy of the GNU Affero General Public License
+along with this program.  If not, see <https://www.gnu.org/licenses/>.
+
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..0292749
--- /dev/null
+++ b/README.md
@@ -0,0 +1,10 @@
+# sumcheck
+
+A decider for Presburger arithmetic using automata.
+
+- parsec.try correct?
+- parsec.expr
+- integers support
+- tests
+- gadt
+- more flexible parser (associativity, parens...)
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
index 0000000..9a994af
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
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
diff --git a/deploy b/deploy
new file mode 100755
index 0000000..3b3c728
--- /dev/null
+++ b/deploy
@@ -0,0 +1,6 @@
+#!/usr/bin/env bash
+set -euo pipefail
+stack install
+rsync ~/.local/bin/sumcheck-exe vps:/srv/sumcheck/staging
+rsync sumcheck.service vps:/srv/sumcheck/staging
+rsync -az static vps:/srv/sumcheck/staging
diff --git a/package.yaml b/package.yaml
new file mode 100644
index 0000000..f954c47
--- /dev/null
+++ b/package.yaml
@@ -0,0 +1,62 @@
+name:                sumcheck
+version:             0.1.0.0
+license:             AGPL
+author:              "cyfraeviolae"
+maintainer:          "cyfraeviolae"
+copyright:           "2021 cyfraeviolae.org"
+
+extra-source-files:
+- README.md
+
+# Metadata used when publishing your package
+# synopsis:            Short description of your package
+# category:            Web
+
+# To avoid duplicated efforts in documentation and dealing with the
+# complications of embedding Haddock markup inside cabal files, it is
+# common to point users to the README.md file.
+description:         Please see the README on GitHub at <https://github.com/githubuser/sumcheck#readme>
+
+dependencies:
+- base >= 4.7 && < 5
+- parsec
+- containers
+- either
+
+library:
+  source-dirs: src
+
+executables:
+  sumcheck-exe:
+    main:                Main.hs
+    source-dirs:         app
+    ghc-options:
+    - -threaded
+    - -rtsopts
+    - -with-rtsopts=-N
+    dependencies:
+    - sumcheck
+    - servant-server
+    - lucid
+    - text
+    - http-api-data
+    - servant-lucid
+    - safe-exceptions
+    - wai
+    - warp
+    - bytestring
+    - utf8-string
+
+tests:
+  sumcheck-test:
+    main:                Spec.hs
+    source-dirs:         test
+    ghc-options:
+    - -threaded
+    - -rtsopts
+    - -with-rtsopts=-N
+    dependencies:
+    - sumcheck
+    - tasty
+    - tasty-hunit
+    - tasty-quickcheck
diff --git a/src/Lib.hs b/src/Lib.hs
new file mode 100644
index 0000000..13dc4ac
--- /dev/null
+++ b/src/Lib.hs
@@ -0,0 +1,214 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TupleSections #-}
+
+module Lib where
+
+import Data.Char (chr, ord)
+import qualified Data.List as L
+import qualified Data.Map as M
+import Data.Maybe (fromJust)
+import qualified Data.Set as S
+import Debug.Trace ()
+import Parser
+import qualified Text.Parsec as Parsec
+
+mget :: (Ord a) => a -> M.Map a b -> b
+mget a m = fromJust $ M.lookup a m
+
+automatizem :: M.Map Addend Int -> Matrix -> DFA [Int] Int
+automatizem dir (MEq as bs) = eq (fromIntegral $ length dir) (map (`mget` dir) as) (map (`mget` dir) bs)
+automatizem dir (MLe a b) = le (mget a dir) (mget b dir)
+automatizem dir (MLt a b) = lt (mget a dir) (mget b dir)
+automatizem dir (MAnd x y) = conj (automatizem dir x) (automatizem dir y)
+automatizem dir (MOr x y) = disj (automatizem dir x) (automatizem dir y)
+automatizem dir (MNot x) = compl (automatizem dir x)
+
+automatize :: M.Map Addend Int -> QNMFormula -> NFA [Int] Int
+automatize dir (QNMFormula [] m) = minimize (fromIntegral $ length dir) $ nondeterminize $ automatizem dir m
+automatize dir (QNMFormula (Neg : quas) m) =
+  let nfa = automatize dir (QNMFormula quas m)
+   in minimize (fromIntegral (length dir)) (ncompl nfa)
+automatize dir (QNMFormula (Qua (Exists, v) : quas) m) =
+  let nfa = automatize dir (QNMFormula quas m)
+   in case M.lookup (Var v) dir of
+        Nothing -> nfa
+        (Just i) -> minimize (fromIntegral $ length dir) $ existentialize i nfa
+
+assign :: S.Set Addend -> M.Map Addend Int
+assign xs = M.fromList (zip (S.toList xs) [0 ..])
+
+collect :: Matrix -> S.Set Addend
+collect (MEq as bs) = S.fromList (as ++ bs)
+collect (MLe a b) = S.fromList [a, b]
+collect (MLt a b) = S.fromList [a, b]
+collect (MAnd x y) = S.union (collect x) (collect y)
+collect (MOr x y) = S.union (collect x) (collect y)
+collect (MNot x) = collect x
+
+literals :: M.Map Addend Int -> [[Int]]
+literals m =
+  let addends = L.sortOn snd (M.toList m)
+      reversedLiterals = map (\(a, i) -> addendReverseBinary a) addends
+      max = L.maximum (map length reversedLiterals)
+      paddedReversed = map (\x -> x ++ replicate (max - length x) 0) reversedLiterals
+      padded = map reverse paddedReversed
+   in L.transpose padded
+
+addendReverseBinary :: Addend -> [Int]
+addendReverseBinary (Var x) = []
+addendReverseBinary (Con n) = reverseBinary n
+
+reverseBinary :: Integer -> [Int]
+reverseBinary 0 = []
+reverseBinary n = fromIntegral (mod n 2) : reverseBinary (div n 2)
+
+eval :: QNMFormula -> Bool
+eval f@(QNMFormula q m) =
+  let dir = (assign $ collect m)
+      nfa = automatize dir f
+      input = literals (assign $ collect m)
+   in runNFA nfa input
+
+data State a = Single a | Double (State a, State a) | Multi [State a] deriving (Eq, Ord, Show)
+
+data DFA c a = DFA [State a] (State a) [State a] (State a -> c -> State a)
+
+data NFA c a = NFA [State a] [State a] [State a] (State a -> c -> [State a])
+
+runDFA :: (Ord a) => DFA c a -> [c] -> Bool
+runDFA (DFA _ start accepts f) cs = foldl f start cs `elem` accepts
+
+runNFA :: (Ord a) => NFA c a -> [c] -> Bool
+runNFA (NFA _ starts accepts f) cs =
+  foldl (\xs c -> L.nub $ concatMap (`f` c) xs) starts cs `L.intersect` accepts /= []
+
+reversal :: (Ord a) => NFA c a -> NFA c a
+reversal (NFA states starts accepts f) = NFA states accepts starts f'
+  where
+    f' s c = filter (\state -> s `elem` f state c) states
+
+eq :: Integer -> [Int] -> [Int] -> DFA [Int] Int
+eq n is js = determinize $ minimize n $ reversal $ nondeterminize dfa
+  where
+    states = Single <$> [- (length js - 1) .. length is - 1 + 1]
+    start = Single 0
+    accepts = [Single 0]
+    rejector = last states
+    f :: State Int -> [Int] -> State Int
+    f carrystate@(Single carry) c =
+      if carrystate == rejector
+        then rejector
+        else
+          let si = sum (map (c !!) is)
+              sj = sum (map (c !!) js)
+              parityok = mod (carry + si) 2 == mod sj 2
+              newcarry = div (carry + si - sj) 2
+           in if parityok
+                then Single newcarry
+                else rejector
+    dfa = DFA states start accepts f
+
+le :: Int -> Int -> DFA [Int] Int
+le = less LessEqual
+
+lt :: Int -> Int -> DFA [Int] Int
+lt = less LessThan
+
+data LessType = LessEqual | LessThan deriving (Eq, Ord, Show)
+
+less :: LessType -> Int -> Int -> DFA [Int] Int
+less lt i j = DFA [Single 0, Single 1, Single 2] (Single 0) accepts f
+  where
+    accepts = if lt == LessEqual then [Single 0, Single 2] else [Single 2]
+    f s c = case (s, (c !! i, c !! j)) of
+      (Single 0, (1, 1)) -> Single 0
+      (Single 0, (0, 0)) -> Single 0
+      (Single 0, (1, 0)) -> Single 1
+      (Single 0, _) -> Single 2
+      (Single 1, _) -> Single 1
+      (_, _) -> Single 2
+
+prod :: [a] -> [b] -> [(a, b)]
+prod xs [] = []
+prod [] ys = []
+prod (x : xs) ys = fmap (x,) ys ++ prod xs ys
+
+data JunctionType = Conj | Disj deriving (Eq, Ord, Show)
+
+junction :: (Ord a) => JunctionType -> DFA c a -> DFA c a -> DFA c a
+junction jt (DFA states1 start1 accepts1 f1) (DFA states2 start2 accepts2 f2) =
+  DFA states' start' accepts' f'
+  where
+    newStates = prod states1 states2
+    states' = Double <$> newStates
+    start' = Double (start1, start2)
+    accepts' =
+      if jt == Conj
+        then Double <$> prod accepts1 accepts2
+        else Double <$> filter (\(s, t) -> s `elem` accepts1 || t `elem` accepts2) newStates
+    f' (Double (s, t)) c = Double (f1 s c, f2 t c)
+
+conj :: (Ord a) => DFA c a -> DFA c a -> DFA c a
+conj = junction Conj
+
+disj :: (Ord a) => DFA c a -> DFA c a -> DFA c a
+disj = junction Disj
+
+compl :: (Ord a) => DFA c a -> DFA c a
+compl (DFA states start accepts f) =
+  DFA states start (states L.\\ accepts) f
+
+nondeterminize :: (Ord a) => DFA c a -> NFA c a
+nondeterminize (DFA states start accepts f) =
+  NFA states [start] accepts f'
+  where
+    f' s c = [f s c]
+
+change :: [a] -> Int -> a -> [a]
+change xs idx b = take idx xs ++ [b] ++ drop (idx + 1) xs
+
+closure :: (Ord a) => NFA c a -> [c] -> [State a] -> [State a]
+closure nfa@(NFA states starts accepts f) cs initstates =
+  let new = concatMap (\state -> concatMap (f state) cs) initstates
+   in if L.nub new L.\\ L.nub initstates /= []
+        then closure nfa cs (L.nub $ new ++ initstates)
+        else L.nub initstates
+
+existentialize :: (Ord a) => Int -> NFA [Int] a -> NFA [Int] a
+existentialize idx nfa@(NFA states starts accepts f) =
+  NFA states starts' accepts f'
+  where
+    zeroer = replicate 50 0
+    oneer = change zeroer idx 1
+    starts' = closure nfa [zeroer, oneer] starts
+    f' s c = f s (change c idx 0) ++ f s (change c idx 1)
+
+powerset :: [a] -> [[a]]
+powerset [] = [[]]
+powerset (x : xs) = let rest = powerset xs in map (x :) rest ++ rest
+
+determinize :: (Ord a) => NFA c a -> DFA c a
+determinize (NFA states start accepts f) =
+  DFA states' start' accepts' f'
+  where
+    newStates = map L.sort $ powerset states
+    states' = Multi <$> newStates
+    start' = Multi $ L.sort start
+    accepts' = Multi <$> filter (\state' -> state' `L.intersect` accepts /= []) newStates
+    f' (Multi s) c = Multi $ L.nub $ L.sort $ concatMap (`f` c) s
+
+ncompl :: (Ord a) => NFA c a -> NFA c a
+ncompl = nondeterminize . compl . determinize
+
+chars :: Integer -> [[Int]]
+chars 0 = [[]]
+chars n =
+  let r = chars (n -1)
+   in map (1 :) r ++ map (0 :) r
+
+minimize :: (Ord a) => Integer -> NFA [Int] a -> NFA [Int] a
+minimize n nfa@(NFA _ starts accepts f) = NFA states' starts accepts f
+  where
+    states' = closure nfa (chars n) starts
diff --git a/src/Parser.hs b/src/Parser.hs
new file mode 100644
index 0000000..c61cd79
--- /dev/null
+++ b/src/Parser.hs
@@ -0,0 +1,288 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE LambdaCase #-}
+
+module Parser where
+
+import Control.Applicative
+import qualified Data.Bifunctor
+import qualified Data.Either.Combinators as E
+import Data.Functor.Identity
+import qualified Data.List as L
+import qualified Data.Set as S
+import Text.Parsec ((<?>))
+import qualified Text.Parsec as Parsec
+import Text.Parsec.Language (haskellDef)
+import qualified Text.Parsec.Token as P
+
+pparse ::
+  Parsec.Stream s Data.Functor.Identity.Identity t =>
+  Parsec.Parsec s () a ->
+  s ->
+  Either Parsec.ParseError a
+pparse rule = Parsec.parse rule ""
+
+type Parser a = Parsec.Parsec String () a
+
+type Symbol = String
+
+type Natural = Integer
+
+data Addend = Var Symbol | Con Natural deriving (Show, Eq, Ord)
+
+data Quantifier = ForAll | Exists deriving (Show, Eq, Ord)
+
+data Formula
+  = Eq [Addend] [Addend]
+  | Ne [Addend] [Addend]
+  | Le Addend Addend
+  | Lt Addend Addend
+  | Ge Addend Addend
+  | Gt Addend Addend
+  | Not Formula
+  | And Formula Formula
+  | Or Formula Formula
+  | Imp Formula Formula
+  | Iff Formula Formula
+  | Q Quantifier Symbol Formula
+  deriving (Show)
+
+pSymbol :: Parser Symbol
+pSymbol = Parsec.many1 (Parsec.oneOf $ ['a' .. 'z'] ++ ['\''])
+
+pNatural :: Parser Integer
+pNatural = read <$> Parsec.many1 Parsec.digit
+
+pAddend :: Parser Addend
+pAddend = Var <$> pSymbol <|> Con <$> pNatural
+
+pTerm :: Parser [Addend]
+pTerm = do
+  c <- Parsec.option 1 pNatural
+  a <- pSymbol
+  return $ replicate (fromIntegral c) (Var a)
+
+singleton :: a -> [a]
+singleton a = [a]
+
+pSums :: String -> ([Addend] -> [Addend] -> a) -> Parser a
+pSums s op = do
+  as <- f
+  Parsec.string s
+  bs <- f
+  return $ op (concat as) (concat bs)
+  where
+    f = Parsec.sepBy1 (Parsec.try pTerm <|> Parsec.try (singleton . Con <$> pNatural)) (Parsec.char '+')
+
+pBinOp :: String -> (Addend -> Addend -> a) -> Parser a
+pBinOp s op = do
+  a <- pAddend
+  Parsec.string s
+  b <- pAddend
+  return $ op a b
+
+pMultiMatOp :: String -> (Formula -> Formula -> Formula) -> Parser Formula
+pMultiMatOp s op = do
+  term <- pFormulaInner
+  Parsec.space *> Parsec.string s *> Parsec.space
+  terms <- Parsec.sepBy1 pFormulaInner (Parsec.space *> Parsec.string s *> Parsec.space)
+  return $ foldl1 op (term : terms)
+
+pBinMatOp :: String -> (Formula -> Formula -> Formula) -> Parser Formula
+pBinMatOp s op = do
+  x <- pFormulaInner
+  Parsec.space
+  Parsec.string s
+  Parsec.space
+  y <- pFormulaInner
+  return $ op x y
+
+pNot :: Parser Formula
+pNot = Not <$> (Parsec.char '~' *> pFormulaInner)
+
+pQuantifier :: Parser Formula
+pQuantifier = do
+  q <- Parsec.oneOf ['A', 'E']
+  c <- pSymbol
+  Parsec.char '.'
+  f <- pFormulaInner
+  return $ Q (if q == 'A' then ForAll else Exists) c f
+
+pFormulaInner :: Parser Formula
+pFormulaInner =
+  Parsec.try (pSums "=" Eq)
+    <|> Parsec.try (pSums "!=" Ne)
+    <|> Parsec.try (pBinOp "<=" Le)
+    <|> Parsec.try (pBinOp "<" Lt)
+    <|> Parsec.try (pBinOp ">=" Ge)
+    <|> Parsec.try (pBinOp ">" Gt)
+    <|> Parsec.try pNot
+    <|> Parsec.between
+      (Parsec.char '(')
+      (Parsec.char ')')
+      ( Parsec.try (pMultiMatOp "&" And)
+          <|> Parsec.try (pMultiMatOp "|" Or)
+          <|> Parsec.try (pBinMatOp "<->" Iff)
+          <|> Parsec.try (pBinMatOp "->" Imp)
+      )
+    <|> Parsec.try pQuantifier
+
+pFormula :: Parser Formula
+pFormula = do
+  p <- pFormulaInner
+  Parsec.eof
+  return p
+
+data Matrix
+  = MEq [Addend] [Addend]
+  | MLe Addend Addend
+  | MLt Addend Addend
+  | MNot Matrix
+  | MAnd Matrix Matrix
+  | MOr Matrix Matrix
+  deriving (Eq, Show)
+
+data MFormula = MFormula [(Quantifier, Symbol)] Matrix deriving (Eq, Show)
+
+-- assumes simplified, pnf
+split :: Formula -> MFormula
+split (Q q v x) =
+  let (MFormula p m) = split x
+   in MFormula ((q, v) : p) m
+split (Eq as bs) = MFormula [] (MEq as bs)
+split (Le a b) = MFormula [] (MLe a b)
+split (Lt a b) = MFormula [] (MLt a b)
+split (Not x) =
+  let MFormula [] x' = split x
+   in MFormula [] (MNot x')
+split (And x y) =
+  let MFormula [] x' = split x
+      MFormula [] y' = split y
+   in MFormula [] (MAnd x' y')
+split (Or x y) =
+  let MFormula [] x' = split x
+      MFormula [] y' = split y
+   in MFormula [] (MOr x' y')
+
+(&) = And
+
+renameAddend :: (Symbol -> Symbol) -> Addend -> Addend
+renameAddend f (Var x) = Var (f x)
+renameAddend f x = x
+
+-- TODO restrict type?
+simplify :: Formula -> Formula
+simplify x@(Eq as bs) = x
+simplify (Ne as bs) = Not (Eq as bs)
+simplify x@(Le a b) = x
+simplify x@(Lt a b) = x
+simplify (Ge a b) = Le b a
+simplify (Gt a b) = Lt b a
+simplify (Not x) = Not (simplify x)
+simplify (And x y) = And (simplify x) (simplify y)
+simplify (Or x y) = Or (simplify x) (simplify y)
+simplify (Imp x y) = simplify (Or (Not x) y)
+simplify (Iff x y) = simplify (And (Imp x y) (Imp y x))
+simplify (Q q v f) = Q q v (simplify f)
+
+prenex :: Formula -> Formula
+prenex (Not x) = pull $ Not (prenex x)
+prenex (And x y) = pull (And (prenex x) (prenex y))
+prenex (Or x y) = pull (Or (prenex x) (prenex y))
+prenex (Q q v x) = Q q v (prenex x)
+prenex f = f
+
+pull :: Formula -> Formula
+pull (Not (Q ForAll x f)) = Q Exists x (pull (Not f))
+pull (Not (Q Exists x f)) = Q ForAll x (pull (Not f))
+pull (Not f) = Not f
+pull (And (Q q v x) y) = let (v', x') = fixup v x y in Q q v' (pull (And x' y))
+pull (And y (Q q v x)) = let (v', x') = fixup v x y in Q q v' (pull (And y x'))
+pull (And x y) = And x y
+pull (Or (Q q v x) y) = let (v', x') = fixup v x y in Q q v' (pull (Or x' y))
+pull (Or y (Q q v x)) = let (v', x') = fixup v x y in Q q v' (pull (Or y x'))
+pull (Or x y) = Or x y
+pull x = x
+
+newname :: Symbol -> [Symbol] -> Symbol
+newname x seen = if x `elem` seen then newname (x <> "'") seen else x
+
+rename :: (Symbol -> Symbol) -> Formula -> Formula
+rename f (Eq as bs) = Eq (renameAddend f <$> as) (renameAddend f <$> bs)
+rename f (Le a b) = Le (renameAddend f a) (renameAddend f b)
+rename f (Lt a b) = Lt (renameAddend f a) (renameAddend f b)
+rename f (Not x) = Not (rename f x)
+rename f (And x y) = And (rename f x) (rename f y)
+rename f (Or x y) = Or (rename f x) (rename f y)
+rename f (Q q v x) = Q q (f v) (rename f x)
+
+-- v is bound in x, other formula is y
+-- if v is either bound or free in y, then rename v in x (avoiding collisions in x or y)
+-- otherwise, leave as is
+fixup :: Symbol -> Formula -> Formula -> (Symbol, Formula)
+fixup v x y =
+  let xvars = vars x
+      yvars = vars y
+      v' =
+        if v `elem` yvars
+          then newname v (xvars ++ yvars)
+          else v
+      x' = rename (\z -> if z == v then v' else z) x
+   in (v', x')
+
+vars :: Formula -> [Symbol]
+vars (Eq as bs) = filtervars as ++ filtervars bs
+vars (Le a b) = filtervars [a, b]
+vars (Lt a b) = filtervars [a, b]
+vars (Not x) = vars x
+vars (And x y) = vars x ++ vars y
+vars (Or x y) = vars x ++ vars y
+vars (Q _ x f) = x : vars f
+
+boundvars :: Formula -> [Symbol]
+boundvars (Not x) = boundvars x
+boundvars (And x y) = boundvars x ++ boundvars y
+boundvars (Or x y) = boundvars x ++ boundvars y
+boundvars (Q _ v f) = v : boundvars f
+boundvars x = []
+
+filtervars :: [Addend] -> [Symbol]
+filtervars as =
+  concatMap
+    ( \case
+        (Var x) -> [x]
+        (Con x) -> []
+    )
+    as
+
+data QN = Qua (Quantifier, Symbol) | Neg deriving (Eq, Show)
+
+data QNMFormula = QNMFormula [QN] Matrix deriving (Eq, Show)
+
+eliminateUniversals :: [(Quantifier, Symbol)] -> [QN]
+eliminateUniversals [] = []
+eliminateUniversals ((q, v) : quas) =
+  let ret = eliminateUniversals quas
+      qua = Qua (Exists, v)
+   in if q == ForAll
+        then [Neg, qua, Neg] ++ ret
+        else qua : ret
+
+simplifyNegsQua :: [QN] -> [QN]
+simplifyNegsQua [] = []
+simplifyNegsQua (Neg : Neg : quas) = quas
+simplifyNegsQua (qua : quas) = qua : simplifyNegsQua quas
+
+simplifyNegs :: MFormula -> QNMFormula
+simplifyNegs (MFormula quas m) =
+  let quas' = (simplifyNegsQua . eliminateUniversals) quas
+   in QNMFormula quas' m
+
+anyUnboundVars :: Formula -> Bool
+anyUnboundVars f = not $ S.null (S.fromList (vars f) S.\\ S.fromList (boundvars f))
+
+parseMFormula :: String -> Either String QNMFormula
+parseMFormula s = do
+  formula <- E.mapLeft (flip (<>) "." . show) (prenex . simplify <$> pparse pFormula s)
+  if anyUnboundVars formula
+    then Left "All variables must be bound."
+    else Right $ simplifyNegs $ split formula
diff --git a/stack.yaml b/stack.yaml
new file mode 100644
index 0000000..a9cf2f8
--- /dev/null
+++ b/stack.yaml
@@ -0,0 +1,68 @@
+# This file was automatically generated by 'stack init'
+#
+# Some commonly used options have been documented as comments in this file.
+# For advanced use and comprehensive documentation of the format, please see:
+# https://docs.haskellstack.org/en/stable/yaml_configuration/
+
+# Resolver to choose a 'specific' stackage snapshot or a compiler version.
+# A snapshot resolver dictates the compiler version and the set of packages
+# to be used for project dependencies. For example:
+#
+# resolver: lts-3.5
+# resolver: nightly-2015-09-21
+# resolver: ghc-7.10.2
+#
+# The location of a snapshot can be provided as a file or url. Stack assumes
+# a snapshot provided as a file might change, whereas a url resource does not.
+#
+# resolver: ./custom-snapshot.yaml
+# resolver: https://example.com/snapshots/2018-01-01.yaml
+resolver:
+  url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/17/10.yaml
+
+# User packages to be built.
+# Various formats can be used as shown in the example below.
+#
+# packages:
+# - some-directory
+# - https://example.com/foo/bar/baz-0.0.2.tar.gz
+#   subdirs:
+#   - auto-update
+#   - wai
+packages:
+- .
+# Dependency packages to be pulled from upstream that are not in the resolver.
+# These entries can reference officially published versions as well as
+# forks / in-progress versions pinned to a git hash. For example:
+#
+# extra-deps:
+# - acme-missiles-0.3
+# - git: https://github.com/commercialhaskell/stack.git
+#   commit: e7b331f14bcffb8367cd58fbfc8b40ec7642100a
+#
+extra-deps:
+  - servant-lucid-0.9.0.2@sha256:693278d574dba7313e931200118424762c02682bbc654e8866be4e6d1c73d816,1803
+
+# Override default flag values for local packages and extra-deps
+# flags: {}
+
+# Extra package databases containing global packages
+# extra-package-dbs: []
+
+# Control whether we use the GHC we find on the path
+# system-ghc: true
+#
+# Require a specific version of stack, using version ranges
+# require-stack-version: -any # Default
+# require-stack-version: ">=2.5"
+#
+# Override the architecture used by stack, especially useful on Windows
+# arch: i386
+# arch: x86_64
+#
+# Extra directories used by stack for building
+# extra-include-dirs: [/path/to/dir]
+# extra-lib-dirs: [/path/to/dir]
+#
+# Allow a newer minor version of GHC than the snapshot specifies
+# compiler-check: newer-minor
diff --git a/stack.yaml.lock b/stack.yaml.lock
new file mode 100644
index 0000000..ca9134e
--- /dev/null
+++ b/stack.yaml.lock
@@ -0,0 +1,20 @@
+# This file was autogenerated by Stack.
+# You should not edit this file by hand.
+# For more information, please see the documentation at:
+#   https://docs.haskellstack.org/en/stable/lock_files
+
+snapshots:
+- original:
+    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/17/10.yaml
+  completed:
+    sha256: 321b3b9f0c7f76994b39e0dabafdc76478274b4ff74cc5e43d410897a335ad3b
+    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/17/10.yaml
+    size: 567241
+packages:
+- original:
+    hackage: servant-lucid-0.9.0.2@sha256:693278d574dba7313e931200118424762c02682bbc654e8866be4e6d1c73d816,1803
+  completed:
+    pantry-tree:
+      sha256: c5635bc53887b81087c3430341790d45cd4063340a0baa62bedd2e77ed4aa84d
+      size: 392
+    hackage: servant-lucid-0.9.0.2@sha256:693278d574dba7313e931200118424762c02682bbc654e8866be4e6d1c73d816,1803
diff --git a/static/EBGaramond-Italic-VariableFont_wght.ttf b/static/EBGaramond-Italic-VariableFont_wght.ttf
new file mode 100644
index 0000000..fa31b71
--- /dev/null
+++ b/static/EBGaramond-Italic-VariableFont_wght.ttf
diff --git a/static/EBGaramond-VariableFont_wght.ttf b/static/EBGaramond-VariableFont_wght.ttf
new file mode 100644
index 0000000..123d5dd
--- /dev/null
+++ b/static/EBGaramond-VariableFont_wght.ttf
diff --git a/static/FiraMono-Regular.ttf b/static/FiraMono-Regular.ttf
new file mode 100644
index 0000000..3910f17
--- /dev/null
+++ b/static/FiraMono-Regular.ttf
diff --git a/static/OFL.txt b/static/OFL.txt
new file mode 100644
index 0000000..1ba1596
--- /dev/null
+++ b/static/OFL.txt
@@ -0,0 +1,93 @@
+Copyright (c) 2012-2013, The Mozilla Corporation and Telefonica S.A.

+

+This Font Software is licensed under the SIL Open Font License, Version 1.1.

+This license is copied below, and is also available with a FAQ at:

+http://scripts.sil.org/OFL

+

+

+-----------------------------------------------------------

+SIL OPEN FONT LICENSE Version 1.1 - 26 February 2007

+-----------------------------------------------------------

+

+PREAMBLE

+The goals of the Open Font License (OFL) are to stimulate worldwide

+development of collaborative font projects, to support the font creation

+efforts of academic and linguistic communities, and to provide a free and

+open framework in which fonts may be shared and improved in partnership

+with others.

+

+The OFL allows the licensed fonts to be used, studied, modified and

+redistributed freely as long as they are not sold by themselves. The

+fonts, including any derivative works, can be bundled, embedded, 

+redistributed and/or sold with any software provided that any reserved

+names are not used by derivative works. The fonts and derivatives,

+however, cannot be released under any other type of license. The

+requirement for fonts to remain under this license does not apply

+to any document created using the fonts or their derivatives.

+

+DEFINITIONS

+"Font Software" refers to the set of files released by the Copyright

+Holder(s) under this license and clearly marked as such. This may

+include source files, build scripts and documentation.

+

+"Reserved Font Name" refers to any names specified as such after the

+copyright statement(s).

+

+"Original Version" refers to the collection of Font Software components as

+distributed by the Copyright Holder(s).

+

+"Modified Version" refers to any derivative made by adding to, deleting,

+or substituting -- in part or in whole -- any of the components of the

+Original Version, by changing formats or by porting the Font Software to a

+new environment.

+

+"Author" refers to any designer, engineer, programmer, technical

+writer or other person who contributed to the Font Software.

+

+PERMISSION & CONDITIONS

+Permission is hereby granted, free of charge, to any person obtaining

+a copy of the Font Software, to use, study, copy, merge, embed, modify,

+redistribute, and sell modified and unmodified copies of the Font

+Software, subject to the following conditions:

+

+1) Neither the Font Software nor any of its individual components,

+in Original or Modified Versions, may be sold by itself.

+

+2) Original or Modified Versions of the Font Software may be bundled,

+redistributed and/or sold with any software, provided that each copy

+contains the above copyright notice and this license. These can be

+included either as stand-alone text files, human-readable headers or

+in the appropriate machine-readable metadata fields within text or

+binary files as long as those fields can be easily viewed by the user.

+

+3) No Modified Version of the Font Software may use the Reserved Font

+Name(s) unless explicit written permission is granted by the corresponding

+Copyright Holder. This restriction only applies to the primary font name as

+presented to the users.

+

+4) The name(s) of the Copyright Holder(s) or the Author(s) of the Font

+Software shall not be used to promote, endorse or advertise any

+Modified Version, except to acknowledge the contribution(s) of the

+Copyright Holder(s) and the Author(s) or with their explicit written

+permission.

+

+5) The Font Software, modified or unmodified, in part or in whole,

+must be distributed entirely under this license, and must not be

+distributed under any other license. The requirement for fonts to

+remain under this license does not apply to any document created

+using the Font Software.

+

+TERMINATION

+This license becomes null and void if any of the above conditions are

+not met.

+

+DISCLAIMER

+THE FONT SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,

+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO ANY WARRANTIES OF

+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT

+OF COPYRIGHT, PATENT, TRADEMARK, OR OTHER RIGHT. IN NO EVENT SHALL THE

+COPYRIGHT HOLDER BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,

+INCLUDING ANY GENERAL, SPECIAL, INDIRECT, INCIDENTAL, OR CONSEQUENTIAL

+DAMAGES, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING

+FROM, OUT OF THE USE OR INABILITY TO USE THE FONT SOFTWARE OR FROM

+OTHER DEALINGS IN THE FONT SOFTWARE.

diff --git a/static/favicon.ico b/static/favicon.ico
new file mode 100644
index 0000000..729ab91
--- /dev/null
+++ b/static/favicon.ico
diff --git a/static/style.css b/static/style.css
new file mode 100644
index 0000000..531350c
--- /dev/null
+++ b/static/style.css
@@ -0,0 +1,107 @@
+@font-face {
+	font-family: EBGaramond;
+	src: url(/static/EBGaramond-VariableFont_wght.ttf) format('woff2-variations');
+	font-style: normal;
+}
+
+@font-face {
+	font-family: EBGaramond;
+	src: url(/static/EBGaramond-Italic-VariableFont_wght.ttf) format('woff2-variations');
+	font-style: italic;
+}
+
+@font-face {
+	font-family: FiraMono;
+	src: url(/static/FiraMono-Regular.ttf);
+	font-style: normal;
+}
+
+body {
+	background: #fdf3f3;
+	color: DarkSlateGrey;
+	font-family: EBGaramond, serif;
+    font-size: large;
+}
+
+a {
+	color: #1eaedb;
+}
+
+a:hover {
+	color: #0e99c4;
+}
+
+.container {
+    margin: 1em;
+}
+
+.row {
+	margin-bottom: 1em;
+}
+
+.title {
+	letter-spacing: -0.5px;
+}
+
+label {
+    margin-right: 4px;
+}
+
+form {
+	border: 1px DarkSlateGrey solid;
+    padding: 10px;
+    padding-left: 25px;
+}
+
+.narrow {
+    max-width: 40em;
+}
+
+.sep {
+    margin-left: 6px;
+    margin-right: 6px;
+}
+
+.nonbreaking {
+	white-space: nowrap;
+}
+
+.focus {
+	font-weight: bold;
+}
+
+input[type="text"] {
+    margin-left: .25em;
+	width: 75%;
+	max-width: 50em;
+    font-family: FiraMono, monospace;
+}
+
+ul {
+    list-style-type: lower-greek;
+}
+
+.theorem {
+    font-size: medium;
+    font-family: FiraMono, monospace;
+}
+
+button {
+    margin-right: 10px;
+}
+
+.valid {
+    background-color: #aed975;
+}
+
+.invalid {
+    background-color: #ff7c7b;
+}
+
+.error {
+    background-color: #c4c4c4;
+}
+
+.validity {
+    font-weight: bold;
+}
diff --git a/sumcheck.cabal b/sumcheck.cabal
new file mode 100644
index 0000000..6c6495b
--- /dev/null
+++ b/sumcheck.cabal
@@ -0,0 +1,77 @@
+cabal-version: 1.12
+
+-- This file has been generated from package.yaml by hpack version 0.34.4.
+--
+-- see: https://github.com/sol/hpack
+
+name:           sumcheck
+version:        0.1.0.0
+description:    Please see the README on GitHub at <https://github.com/githubuser/sumcheck#readme>
+author:         cyfraeviolae
+maintainer:     cyfraeviolae
+copyright:      2021 cyfraeviolae.org
+license:        AGPL
+license-file:   LICENSE
+build-type:     Simple
+extra-source-files:
+    README.md
+
+library
+  exposed-modules:
+      Lib
+      Parser
+  other-modules:
+      Paths_sumcheck
+  hs-source-dirs:
+      src
+  build-depends:
+      base >=4.7 && <5
+    , containers
+    , either
+    , parsec
+  default-language: Haskell2010
+
+executable sumcheck-exe
+  main-is: Main.hs
+  other-modules:
+      Web
+      Paths_sumcheck
+  hs-source-dirs:
+      app
+  ghc-options: -threaded -rtsopts -with-rtsopts=-N
+  build-depends:
+      base >=4.7 && <5
+    , bytestring
+    , containers
+    , either
+    , http-api-data
+    , lucid
+    , parsec
+    , safe-exceptions
+    , servant-lucid
+    , servant-server
+    , sumcheck
+    , text
+    , utf8-string
+    , wai
+    , warp
+  default-language: Haskell2010
+
+test-suite sumcheck-test
+  type: exitcode-stdio-1.0
+  main-is: Spec.hs
+  other-modules:
+      Paths_sumcheck
+  hs-source-dirs:
+      test
+  ghc-options: -threaded -rtsopts -with-rtsopts=-N
+  build-depends:
+      base >=4.7 && <5
+    , containers
+    , either
+    , parsec
+    , sumcheck
+    , tasty
+    , tasty-hunit
+    , tasty-quickcheck
+  default-language: Haskell2010
diff --git a/sumcheck.service b/sumcheck.service
new file mode 100644
index 0000000..c8536e0
--- /dev/null
+++ b/sumcheck.service
@@ -0,0 +1,12 @@
+[Unit]
+Description=sumcheck
+After=network.target
+
+[Service]
+Type=simple
+Restart=on-failure
+ExecStart=/srv/sumcheck/sumcheck-exe
+WorkingDirectory=/srv/sumcheck/
+
+[Install]
+WantedBy=multi-user.target
diff --git a/test/Spec.hs b/test/Spec.hs
new file mode 100644
index 0000000..5466493
--- /dev/null
+++ b/test/Spec.hs
@@ -0,0 +1,20 @@
+import Data.List
+import qualified Data.Map as M
+import Debug.Trace
+import Lib
+import Parser
+import Test.Tasty
+import Test.Tasty.HUnit
+import Test.Tasty.QuickCheck as QC
+
+main = defaultMain tests
+
+tests :: TestTree
+tests = testGroup "Tests" [unitTests]
+
+unitTests =
+  testGroup
+    "Unit tests"
+    [
+      testCase "" $ ev (cc "Ex.x+1=2") @?= True,
+    ]