From 1da9b25ff814d681afc3b741739bffbca7cc45e8 Mon Sep 17 00:00:00 2001 From: cyfraeviolae Date: Sun, 16 May 2021 18:22:49 -0400 Subject: init --- LICENSE | 16 ++ README.md | 10 + Setup.hs | 2 + app/Main.hs | 6 + app/Web.hs | 226 +++++++++++++++++++ deploy | 6 + package.yaml | 62 ++++++ src/Lib.hs | 214 ++++++++++++++++++ src/Parser.hs | 288 +++++++++++++++++++++++++ stack.yaml | 68 ++++++ stack.yaml.lock | 20 ++ static/EBGaramond-Italic-VariableFont_wght.ttf | Bin 0 -> 829752 bytes static/EBGaramond-VariableFont_wght.ttf | Bin 0 -> 897728 bytes static/FiraMono-Regular.ttf | Bin 0 -> 169464 bytes static/OFL.txt | 93 ++++++++ static/favicon.ico | Bin 0 -> 318 bytes static/style.css | 107 +++++++++ sumcheck.cabal | 77 +++++++ sumcheck.service | 12 ++ test/Spec.hs | 20 ++ 20 files changed, 1227 insertions(+) create mode 100644 LICENSE create mode 100644 README.md create mode 100644 Setup.hs create mode 100644 app/Main.hs create mode 100644 app/Web.hs create mode 100755 deploy create mode 100644 package.yaml create mode 100644 src/Lib.hs create mode 100644 src/Parser.hs create mode 100644 stack.yaml create mode 100644 stack.yaml.lock create mode 100644 static/EBGaramond-Italic-VariableFont_wght.ttf create mode 100644 static/EBGaramond-VariableFont_wght.ttf create mode 100644 static/FiraMono-Regular.ttf create mode 100644 static/OFL.txt create mode 100644 static/favicon.ico create mode 100644 static/style.css create mode 100644 sumcheck.cabal create mode 100644 sumcheck.service create mode 100644 test/Spec.hs 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 . + 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"] "(φ & ψ & ...)" + 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 + +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 Binary files /dev/null and b/static/EBGaramond-Italic-VariableFont_wght.ttf differ diff --git a/static/EBGaramond-VariableFont_wght.ttf b/static/EBGaramond-VariableFont_wght.ttf new file mode 100644 index 0000000..123d5dd Binary files /dev/null and b/static/EBGaramond-VariableFont_wght.ttf differ diff --git a/static/FiraMono-Regular.ttf b/static/FiraMono-Regular.ttf new file mode 100644 index 0000000..3910f17 Binary files /dev/null and b/static/FiraMono-Regular.ttf differ 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 Binary files /dev/null and b/static/favicon.ico differ 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 +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, + ] -- cgit v1.2.3