summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--.gitignore1
-rw-r--r--Expr.hs13
-rw-r--r--Main.hs21
-rw-r--r--Normalise.hs54
-rw-r--r--Parser.hs67
-rw-r--r--agda-simplifier.cabal18
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/
diff --git a/Expr.hs b/Expr.hs
new file mode 100644
index 0000000..80ce440
--- /dev/null
+++ b/Expr.hs
@@ -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
diff --git a/Main.hs b/Main.hs
new file mode 100644
index 0000000..7099e07
--- /dev/null
+++ b/Main.hs
@@ -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