diff options
| -rw-r--r-- | app/Web.hs | 30 | ||||
| -rw-r--r-- | src/Parser.hs | 178 |
2 files changed, 102 insertions, 106 deletions
@@ -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 |