InitialHEADmaster

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