Implement applyRules

eo-phi-normalizer/eo-phi-normalizer.cabal

@@ -34,6 +34,8 @@ library
   exposed-modules:
       Language.EO.Phi
       Language.EO.Phi.Normalize
+      Language.EO.Phi.Rules.Common
+      Language.EO.Phi.Syntax
       Language.EO.Phi.Syntax.Abs
       Language.EO.Phi.Syntax.Lex
       Language.EO.Phi.Syntax.Par

eo-phi-normalizer/src/Language/EO/Phi.hs

@@ -1,23 +1,18 @@
-{-# LANGUAGE LambdaCase #-}
-
 module Language.EO.Phi (
   defaultMain,
   normalize,
   parseProgram,
   unsafeParseProgram,
-  printTree,
-  module Language.EO.Phi.Syntax.Abs,
+  module Language.EO.Phi.Syntax,
 ) where
 
-import Data.Char (isSpace)
 import System.Exit (exitFailure)
 
-import Language.EO.Phi.Syntax.Abs
 import qualified Language.EO.Phi.Syntax.Abs as Phi
 import qualified Language.EO.Phi.Syntax.Par as Phi
-import qualified Language.EO.Phi.Syntax.Print as Phi
 
 import Language.EO.Phi.Normalize
+import Language.EO.Phi.Syntax
 
 -- | Parse a 'Program' or return a parsing error.
 parseProgram :: String -> Either String Phi.Program
@@ -46,77 +41,3 @@ defaultMain = do
       exitFailure
     Right program -> do
       putStrLn (printTree (normalize program))
-
--- * Overriding generated pretty-printer
-
--- | Like 'Phi.printTree', but without spaces around dots and no indentation for curly braces.
-printTree :: (Phi.Print a) => a -> String
-printTree = shrinkDots . render . Phi.prt 0
-
--- | Remove spaces around dots.
---
--- >>> putStrLn (shrinkDots "a ↦ ξ . a")
--- a ↦ ξ.a
-shrinkDots :: String -> String
-shrinkDots [] = []
-shrinkDots (' ' : '.' : ' ' : cs) = '.' : shrinkDots cs
-shrinkDots (c : cs) = c : shrinkDots cs
-
--- | Copy of 'Phi.render', except no indentation is made for curly braces.
-render :: Phi.Doc -> String
-render d = rend 0 False (map ($ "") $ d []) ""
- where
-  rend ::
-    Int ->
-    -- \^ Indentation level.
-    Bool ->
-    -- \^ Pending indentation to be output before next character?
-    [String] ->
-    ShowS
-  rend i p = \case
-    "[" : ts -> char '[' . rend i False ts
-    "(" : ts -> char '(' . rend i False ts
-    -- "{"      :ts -> onNewLine i     p . showChar   '{'  . new (i+1) ts
-    -- "}" : ";":ts -> onNewLine (i-1) p . showString "};" . new (i-1) ts
-    -- "}"      :ts -> onNewLine (i-1) p . showChar   '}'  . new (i-1) ts
-    [";"] -> char ';'
-    ";" : ts -> char ';' . new i ts
-    t : ts@(s : _)
-      | closingOrPunctuation s ->
-          pending . showString t . rend i False ts
-    t : ts -> pending . space t . rend i False ts
-    [] -> id
-   where
-    -- Output character after pending indentation.
-    char :: Char -> ShowS
-    char c = pending . showChar c
-
-    -- Output pending indentation.
-    pending :: ShowS
-    pending = if p then indent i else id
-
-  -- Indentation (spaces) for given indentation level.
-  indent :: Int -> ShowS
-  indent i = Phi.replicateS (2 * i) (showChar ' ')
-
-  -- Continue rendering in new line with new indentation.
-  new :: Int -> [String] -> ShowS
-  new j ts = showChar '\n' . rend j True ts
-
-  -- Separate given string from following text by a space (if needed).
-  space :: String -> ShowS
-  space t s =
-    case (all isSpace t, null spc, null rest) of
-      (True, _, True) -> [] -- remove trailing space
-      (False, _, True) -> t -- remove trailing space
-      (False, True, False) -> t ++ ' ' : s -- add space if none
-      _ -> t ++ s
-   where
-    (spc, rest) = span isSpace s
-
-  closingOrPunctuation :: String -> Bool
-  closingOrPunctuation [c] = c `elem` closerOrPunct
-  closingOrPunctuation _ = False
-
-  closerOrPunct :: String
-  closerOrPunct = ")],;"

eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs

@@ -13,20 +13,14 @@ import Numeric (showHex)
 
 import Control.Monad (forM)
 import Language.EO.Phi.Syntax.Abs
+import Language.EO.Phi.Rules.Common (lookupBinding)
 
 data Context = Context
   { globalObject :: [Binding]
   , thisObject :: [Binding]
   , totalNuCount :: Int
   }
 
-lookupBinding :: Attribute -> [Binding] -> Maybe Object
-lookupBinding _ [] = Nothing
-lookupBinding a (AlphaBinding a' object : bindings)
-  | a == a' = Just object
-  | otherwise = lookupBinding a bindings
-lookupBinding _ _ = Nothing
-
 isNu :: Binding -> Bool
 isNu (AlphaBinding VTX _) = True
 isNu (EmptyBinding VTX) = True

eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs

@@ -0,0 +1,103 @@
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE RecordWildCards #-}
+module Language.EO.Phi.Rules.Common where
+
+import Language.EO.Phi.Syntax.Abs
+import Control.Applicative (asum, Alternative ((<|>)))
+import Control.Monad (guard)
+import Language.EO.Phi.Syntax
+
+-- $setup
+-- >>> :set -XOverloadedStrings
+
+data Context = Context
+  { allRules :: [Rule]
+  }
+
+-- | A rule tries to apply a transformation to the root object, if possible.
+type Rule = Context -> Object -> Maybe Object
+
+applyOneRuleAtRoot :: Context -> Object -> [Object]
+applyOneRuleAtRoot ctx@Context{..} obj =
+  [ obj'
+  | rule <- allRules
+  , Just obj' <- [rule ctx obj]
+  ]
+
+withSubObject :: (Object -> [Object]) -> Object -> [Object]
+withSubObject f root = f root <|>
+  case root of
+    Formation bindings ->
+      Formation <$> withSubObjectBindings f bindings
+    Application obj bindings -> asum
+      [ Application <$> withSubObject f obj <*> pure bindings
+      , Application obj <$> withSubObjectBindings f bindings
+      ]
+    ObjectDispatch obj a -> ObjectDispatch <$> withSubObject f obj <*> pure a
+    GlobalDispatch{} -> []
+    ThisDispatch{} -> []
+    Termination -> []
+
+withSubObjectBindings :: (Object -> [Object]) -> [Binding] -> [[Binding]]
+withSubObjectBindings _ [] = []
+withSubObjectBindings f (b:bs) = asum
+  [ [ b' : bs  | b'  <- withSubObjectBinding  f b ]
+  , [ b  : bs' | bs' <- withSubObjectBindings f bs ]
+  ]
+
+withSubObjectBinding :: (Object -> [Object]) -> Binding -> [Binding]
+withSubObjectBinding f = \case
+  AlphaBinding a obj -> AlphaBinding a <$> withSubObject f obj
+  EmptyBinding{} -> []
+  DeltaBinding{} -> []
+  LambdaBinding{} -> []
+
+applyOneRule :: Context -> Object -> [Object]
+applyOneRule = withSubObject . applyOneRuleAtRoot
+
+isNF :: Context -> Object -> Bool
+isNF ctx = null . applyOneRule ctx
+
+-- | Apply rules until we get a normal form.
+--
+-- >>> mapM_ (putStrLn . Language.EO.Phi.printTree) (applyRules (Context [rule6]) "⟦ a ↦ ⟦ b ↦ ⟦ ⟧ ⟧.b ⟧.a")
+-- ⟦ ⟧ (ρ ↦ ⟦ ⟧) (ρ ↦ ⟦ ⟧)
+applyRules :: Context -> Object -> [Object]
+applyRules ctx obj
+  | isNF ctx obj = [obj]
+  | otherwise =
+      [ obj''
+      | obj' <- applyOneRule ctx obj
+      , obj'' <- applyRules ctx obj' ]
+
+applyRulesChain :: Context -> Object -> [[Object]]
+applyRulesChain ctx obj
+  | isNF ctx obj = [[obj]]
+  | otherwise =
+      [ obj : chain
+      | obj' <- applyOneRule ctx obj
+      , chain <- applyRulesChain ctx obj' ]
+
+-- * Yegor's Rules
+
+-- | Rule 6.
+rule6 :: Rule
+rule6 ctx (ObjectDispatch (Formation bindings) a)
+  | Just obj <- lookupBinding a bindings = do
+    guard (isNF ctx obj)
+    return (Application obj [AlphaBinding Rho (Formation bindings')])
+    where
+      bindings' = filter (not . isDispatched) bindings
+      isDispatched (AlphaBinding a' _) = a == a'
+      isDispatched _ = False
+rule6 _ _ = Nothing
+
+-- * Helpers
+
+-- | Lookup a binding by the attribute name.
+lookupBinding :: Attribute -> [Binding] -> Maybe Object
+lookupBinding _ [] = Nothing
+lookupBinding a (AlphaBinding a' object : bindings)
+  | a == a' = Just object
+  | otherwise = lookupBinding a bindings
+lookupBinding _ _ = Nothing

eo-phi-normalizer/src/Language/EO/Phi/Syntax.hs

@@ -0,0 +1,100 @@
+{-# OPTIONS_GHC -Wno-orphans #-}
+{-# LANGUAGE LambdaCase #-}
+module Language.EO.Phi.Syntax where
+
+import Data.Char (isSpace)
+import qualified Language.EO.Phi.Syntax.Abs as Phi
+import qualified Language.EO.Phi.Syntax.Par as Phi
+import qualified Language.EO.Phi.Syntax.Print as Phi
+import Data.String (IsString(..))
+
+instance IsString Phi.Object where
+  fromString = unsafeParseObject
+
+-- | Parse a 'Object' or return a parsing error.
+parseObject :: String -> Either String Phi.Object
+parseObject input = Phi.pObject tokens
+ where
+  tokens = Phi.myLexer input
+
+-- | Parse a 'Object' from a 'String'.
+-- May throw an 'error` if input has a syntactical or lexical errors.
+unsafeParseObject :: String -> Phi.Object
+unsafeParseObject input =
+  case parseObject input of
+    Left parseError -> error parseError
+    Right object -> object
+
+-- * Overriding generated pretty-printer
+
+-- | Like 'Phi.printTree', but without spaces around dots and no indentation for curly braces.
+printTree :: (Phi.Print a) => a -> String
+printTree = shrinkDots . render . Phi.prt 0
+
+-- | Remove spaces around dots.
+--
+-- >>> putStrLn (shrinkDots "a ↦ ξ . a")
+-- a ↦ ξ.a
+shrinkDots :: String -> String
+shrinkDots [] = []
+shrinkDots (' ' : '.' : ' ' : cs) = '.' : shrinkDots cs
+shrinkDots (c : cs) = c : shrinkDots cs
+
+-- | Copy of 'Phi.render', except no indentation is made for curly braces.
+render :: Phi.Doc -> String
+render d = rend 0 False (map ($ "") $ d []) ""
+ where
+  rend ::
+    Int ->
+    -- \^ Indentation level.
+    Bool ->
+    -- \^ Pending indentation to be output before next character?
+    [String] ->
+    ShowS
+  rend i p = \case
+    "[" : ts -> char '[' . rend i False ts
+    "(" : ts -> char '(' . rend i False ts
+    -- "{"      :ts -> onNewLine i     p . showChar   '{'  . new (i+1) ts
+    -- "}" : ";":ts -> onNewLine (i-1) p . showString "};" . new (i-1) ts
+    -- "}"      :ts -> onNewLine (i-1) p . showChar   '}'  . new (i-1) ts
+    [";"] -> char ';'
+    ";" : ts -> char ';' . new i ts
+    t : ts@(s : _)
+      | closingOrPunctuation s ->
+          pending . showString t . rend i False ts
+    t : ts -> pending . space t . rend i False ts
+    [] -> id
+   where
+    -- Output character after pending indentation.
+    char :: Char -> ShowS
+    char c = pending . showChar c
+
+    -- Output pending indentation.
+    pending :: ShowS
+    pending = if p then indent i else id
+
+  -- Indentation (spaces) for given indentation level.
+  indent :: Int -> ShowS
+  indent i = Phi.replicateS (2 * i) (showChar ' ')
+
+  -- Continue rendering in new line with new indentation.
+  new :: Int -> [String] -> ShowS
+  new j ts = showChar '\n' . rend j True ts
+
+  -- Separate given string from following text by a space (if needed).
+  space :: String -> ShowS
+  space t s =
+    case (all isSpace t, null spc, null rest) of
+      (True, _, True) -> [] -- remove trailing space
+      (False, _, True) -> t -- remove trailing space
+      (False, True, False) -> t ++ ' ' : s -- add space if none
+      _ -> t ++ s
+   where
+    (spc, rest) = span isSpace s
+
+  closingOrPunctuation :: String -> Bool
+  closingOrPunctuation [c] = c `elem` closerOrPunct
+  closingOrPunctuation _ = False
+
+  closerOrPunct :: String
+  closerOrPunct = ")],;"