diff options
| -rw-r--r-- | .gitignore | 1 | ||||
| -rw-r--r-- | Expr.hs | 13 | ||||
| -rw-r--r-- | Main.hs | 21 | ||||
| -rw-r--r-- | Normalise.hs | 54 | ||||
| -rw-r--r-- | Parser.hs | 67 | ||||
| -rw-r--r-- | agda-simplifier.cabal | 18 |
6 files changed, 174 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..c33954f --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +dist-newstyle/ @@ -0,0 +1,13 @@ +module Expr where + + +data Expr + = EInfix Expr String Expr + | EPrefix String Expr + | EParens Expr + | ELitInt Integer + | EVar String + deriving (Show) + +einfix :: String -> Expr -> Expr -> Expr +einfix = flip EInfix @@ -0,0 +1,21 @@ +module Main where + +import System.Exit (die) +import Text.Parsec + +-- import Expr +import Parser +import Normalise + + +main :: IO () +main = do + s <- getContents + + expr <- case parse parseExpr "<stdin>" s of + Left err -> die (show err) + Right expr -> return expr + + print expr + + print (normalise expr) diff --git a/Normalise.hs b/Normalise.hs new file mode 100644 index 0000000..3e4a696 --- /dev/null +++ b/Normalise.hs @@ -0,0 +1,54 @@ +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE LambdaCase #-} +{-# OPTIONS_GHC -Wno-deferred-out-of-scope-variables #-} +module Normalise where + +import Expr +import Data.List (foldl1', foldl') + + +data SumCollect = + SumCollect [Integer] -- ^ literals + [Expr] -- ^ positive terms + [Expr] -- ^ negative terms + +instance Semigroup SumCollect where + SumCollect a b c <> SumCollect a' b' c' = + SumCollect (a <> a') (b <> b') (c <> c') + +instance Monoid SumCollect where + mempty = SumCollect [] [] [] + +scNegate :: SumCollect -> SumCollect +scNegate (SumCollect n post negt) = SumCollect (map negate n) negt post + +collectSum :: Expr -> SumCollect +collectSum = \case + EInfix e1 "+" e2 -> collectSum e1 <> collectSum e2 + EInfix e1 "-" e2 -> collectSum e1 <> scNegate (collectSum e2) + EParens e -> collectSum e + EPrefix "+" (ELitInt n) -> SumCollect [n] [] [] + e -> SumCollect [] [e] [] + +normalise :: Expr -> Expr +normalise e + | SumCollect literals posterms negterms <- collectSum e + , length literals + length posterms + length negterms > 1 + = case (sum literals, map normalise posterms, map normalise negterms) of + (l, [], []) + | l < 0 -> EPrefix "-" (ELitInt (-l)) + | otherwise -> EPrefix "+" (ELitInt l) + (0, [], nt0 : nts) -> + foldl' (einfix "-") (EPrefix "-" nt0) nts + (0, pt, nt) -> + foldl' (einfix "-") (foldl1' (einfix "+") pt) nt + (l, pt, nt) -> + foldl' (einfix "-") (foldl' (einfix "+") (EPrefix "+" (ELitInt l)) pt) nt +normalise e = recurse normalise e + +recurse :: (Expr -> Expr) -> Expr -> Expr +recurse f (EInfix e1 n e2) = EInfix (f e1) n (f e2) +recurse f (EPrefix n e) = EPrefix n (f e) +recurse f (EParens e) = EParens (f e) +recurse _ (ELitInt x) = ELitInt x +recurse _ (EVar n) = EVar n diff --git a/Parser.hs b/Parser.hs new file mode 100644 index 0000000..fda3662 --- /dev/null +++ b/Parser.hs @@ -0,0 +1,67 @@ +module Parser where + +import Control.Monad (void) +import Data.Char (isSpace) +import Data.Functor.Identity (Identity) +import Text.Parsec +import Text.Parsec.Expr +import Debug.Trace + +import Expr + + +type Parser = Parsec String () + +pLexemeSuffix :: Parser () +pLexemeSuffix = eof <|> lookAhead (void (oneOf "()")) <|> void (many1 space) + +lexeme :: String -> Parser () +lexeme s = try $ string s >> pLexemeSuffix + +operators :: OperatorTable String () Identity Expr +operators = + [[Prefix (symPrefix "+")] + ,[Infix (symInfix "*") AssocLeft] + ,[Infix (symInfix "+") AssocLeft + ,Infix (symInfix "-") AssocLeft] + ,[Infix (symInfix ":≤") AssocNone]] + where + symInfix :: String -> Parser (Expr -> Expr -> Expr) + symInfix name = do + lexeme name + return (einfix name) + + symPrefix :: String -> Parser (Expr -> Expr) + symPrefix name = do + lexeme name + return (EPrefix name) + +pAtom :: Parser Expr +pAtom = do + e <- pAtom' + traceM ("pAtom: " ++ show e) + return e + +pAtom' :: Parser Expr +pAtom' = choice + [do _ <- char '(' + _ <- many space + e <- pExpr + lexeme ")" + return e + ,do s <- many1 digit + pLexemeSuffix + return (ELitInt (read s)) + ,do s <- many1 (satisfy (\c -> not (isSpace c) && c `notElem` "(){}")) + pLexemeSuffix + return (EVar s)] + +pExpr :: Parser Expr +pExpr = buildExpressionParser operators pAtom + +parseExpr :: Parser Expr +parseExpr = do + _ <- many space + e <- pExpr + eof + return e diff --git a/agda-simplifier.cabal b/agda-simplifier.cabal new file mode 100644 index 0000000..d5ce798 --- /dev/null +++ b/agda-simplifier.cabal @@ -0,0 +1,18 @@ +cabal-version: >=1.10 +name: agda-simplifier +synopsis: Simplifier for certain Agda expressions +version: 0.1.0.0 +license: MIT +author: Tom Smeding +maintainer: tom@tomsmeding.com +build-type: Simple + +executable agda-simplifier + main-is: Main.hs + other-modules: Expr, Parser, Normalise + build-depends: + base >= 4.16 && < 4.19, + parsec + hs-source-dirs: . + default-language: Haskell2010 + ghc-options: -Wall -threaded |