summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--app/Web.hs30
-rw-r--r--src/Parser.hs178
2 files changed, 102 insertions, 106 deletions
diff --git a/app/Web.hs b/app/Web.hs
index 60b3120..7bc233b 100644
--- a/app/Web.hs
+++ b/app/Web.hs
@@ -163,32 +163,29 @@ instance ToHtml HomeView where
ul_ $ do
li_ $ span_ [class_ "theorem"] "c"
li_ $ span_ [class_ "theorem"] "x"
- p_ $ span_ "The following are addends:"
- ul_ $ do
- li_ $ span_ [class_ "theorem"] "c"
- li_ $ span_ [class_ "theorem"] "x"
li_ $ span_ [class_ "theorem"] "cx"
+ p_ $ span_ "The following are relations:"
+ ul_ $ do
+ li_ $ span_ [class_ "theorem"] "="
+ li_ $ span_ [class_ "theorem"] "!="
+ li_ $ span_ [class_ "theorem"] "<="
+ li_ $ span_ [class_ "theorem"] "<"
+ li_ $ span_ [class_ "theorem"] ">="
+ li_ $ span_ [class_ "theorem"] ">"
p_ $ do
- span_ "For addends "
+ span_ "For terms "
code_ "a"
span_ " and "
code_ "b"
- span_ ", terms "
- code_ "t"
- span_ " and "
- code_ "r"
+ span_ ", relation "
+ code_ "★"
span_ ", and theorems "
code_ "φ"
span_ " and "
code_ "ψ"
span_ ", the following are theorems:"
ul_ $ do
- li_ $ span_ [class_ "theorem"] "a+...=b+..."
- li_ $ span_ [class_ "theorem"] "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"] "a+...★b+..."
li_ $ span_ [class_ "theorem"] "(φ & ψ & ...)"
li_ $ span_ [class_ "theorem"] "(φ | ψ | ...)"
li_ $ span_ [class_ "theorem"] "(φ -> ψ)"
@@ -217,6 +214,3 @@ pageTemplate crumbs body = doctypehtml_ $ 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/src/Parser.hs b/src/Parser.hs
index 77cde09..e328b6e 100644
--- a/src/Parser.hs
+++ b/src/Parser.hs
@@ -3,17 +3,17 @@
module Parser where
-import Control.Applicative
-import qualified Data.Either.Combinators as E
-import Data.Functor.Identity
-import qualified Data.Set as S
-import qualified Text.Parsec as Parsec
-
-pparse
- :: Parsec.Stream s Data.Functor.Identity.Identity t
- => Parsec.Parsec s () a
- -> s
- -> Either Parsec.ParseError a
+import Control.Applicative
+import qualified Data.Either.Combinators as E
+import Data.Functor.Identity
+import qualified Data.Set as S
+import qualified Text.Parsec as Parsec
+
+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
@@ -29,10 +29,10 @@ data Quantifier = ForAll | Exists deriving (Show, Eq, Ord)
data Formula
= Eq [Addend] [Addend]
| Ne [Addend] [Addend]
+ | GenLe [Addend] [Addend]
+ | GenLt [Addend] [Addend]
| Le Addend Addend
| Lt Addend Addend
- | Ge Addend Addend
- | Gt Addend Addend
| Not Formula
| And Formula Formula
| Or Formula Formula
@@ -62,27 +62,23 @@ singleton a = [a]
pSums :: String -> ([Addend] -> [Addend] -> a) -> Parser a
pSums s op = do
as <- f
- _ <- Parsec.string s
+ _ <- 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
+ where
+ f =
+ Parsec.sepBy1
+ (Parsec.try pTerm <|> Parsec.try (singleton . Con <$> pNatural))
+ (Parsec.char '+')
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)
+ 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
@@ -109,19 +105,19 @@ 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 (pSums "<=" GenLe)
+ <|> Parsec.try (pSums "<" GenLt)
+ <|> Parsec.try (pSums ">=" (flip GenLe))
+ <|> Parsec.try (pSums ">" (flip GenLt))
<|> Parsec.try pNot
<|> Parsec.between
- (Parsec.char '(')
- (Parsec.char ')')
- ( Parsec.try (pMultiMatOp "&" And)
+ (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
@@ -144,50 +140,53 @@ data MFormula = MFormula [(Quantifier, Symbol)] Matrix
-- assumes simplified, pnf
split :: Formula -> MFormula
-split (Q q v x ) = let (MFormula p m) = split x in MFormula ((q, v) : p) m
+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 (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')
+ in MFormula [] (MAnd x' y')
split (Or x y) =
let MFormula [] x' = split x
MFormula [] y' = split y
- in MFormula [] (MOr x' y')
+ in MFormula [] (MOr x' y')
renameAddend :: (Symbol -> Symbol) -> Addend -> Addend
renameAddend f (Var x) = Var (f x)
-renameAddend f x = 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)
+simplify (Ne as bs) = Not (Eq as bs)
+simplify x@(Le a b) = x
+simplify x@(Lt a b) = x
+-- note: "V" will not appear in user input, as Symbol is over a-z
+simplify (GenLe [a] [b]) = Le a b
+simplify (GenLe as bs) = Q Exists "V" (Eq (Var "V" : as) bs)
+simplify (GenLt [a] [b]) = Lt a b
+simplify (GenLt as bs) = Q Exists "V" (Eq (Var "V" : Con 1 : as) bs)
+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 (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 (Or x y) = pull (Or (prenex x) (prenex y))
prenex (Q q v x) = Q q v (prenex x)
-prenex f = f
+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 (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)) =
@@ -203,12 +202,12 @@ 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)
+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)
@@ -217,32 +216,33 @@ 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')
+ 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
+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 (Not x) = boundvars x
boundvars (And x y) = boundvars x ++ boundvars y
-boundvars (Or x y) = boundvars x ++ boundvars y
+boundvars (Or x y) = boundvars x ++ boundvars y
boundvars (Q _ v f) = v : boundvars f
-boundvars _ = []
+boundvars _ = []
filtervars :: [Addend] -> [Symbol]
-filtervars = concatMap
- (\case
- (Var x) -> [x]
- (Con _) -> []
- )
+filtervars =
+ concatMap
+ ( \case
+ (Var x) -> [x]
+ (Con _) -> []
+ )
data QN = Qua (Quantifier, Symbol) | Neg deriving (Eq, Show)
@@ -254,17 +254,17 @@ 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
+ in if q == ForAll then [Neg, qua, Neg] ++ ret else qua : ret
simplifyNegsQua :: [QN] -> [QN]
-simplifyNegsQua [] = []
+simplifyNegsQua [] = []
simplifyNegsQua (Neg : Neg : quas) = quas
-simplifyNegsQua (qua : quas) = qua : simplifyNegsQua quas
+simplifyNegsQua (qua : quas) = qua : simplifyNegsQua quas
simplifyNegs :: MFormula -> QNMFormula
simplifyNegs (MFormula quas m) =
let quas' = (simplifyNegsQua . eliminateUniversals) quas
- in QNMFormula quas' m
+ in QNMFormula quas' m
anyUnboundVars :: Formula -> Bool
anyUnboundVars f =
@@ -272,8 +272,10 @@ anyUnboundVars f =
parseMFormula :: String -> Either String QNMFormula
parseMFormula s = do
- formula <- E.mapLeft (flip (<>) "." . show)
- (prenex . simplify <$> pparse pFormula s)
+ 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