Add initial support for pre-defined rules

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

@@ -34,6 +34,9 @@ library
   exposed-modules:
       Language.EO.Phi
       Language.EO.Phi.Normalize
+      Language.EO.Phi.Rules.Common
+      Language.EO.Phi.Rules.PhiPaper
+      Language.EO.Phi.Syntax
       Language.EO.Phi.Syntax.Abs
       Language.EO.Phi.Syntax.Lex
       Language.EO.Phi.Syntax.Par
@@ -42,7 +45,7 @@ library
       Paths_eo_phi_normalizer
   hs-source-dirs:
       src
-  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -Wno-missing-export-lists
+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -Wno-missing-export-lists -Werror
   build-tools:
       alex >=3.2.4
     , happy >=1.19.9
@@ -54,6 +57,8 @@ library
     , base >=4.7 && <5
     , directory
     , filepath
+    , mtl
+    , string-interpolate
     , yaml
   default-language: Haskell2010
 
@@ -63,7 +68,7 @@ executable normalize-phi
       Paths_eo_phi_normalizer
   hs-source-dirs:
       app
-  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -Wno-missing-export-lists -threaded -rtsopts -with-rtsopts=-N
+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -Wno-missing-export-lists -Werror -threaded -rtsopts -with-rtsopts=-N
   build-tools:
       alex >=3.2.4
     , happy >=1.19.9
@@ -76,6 +81,8 @@ executable normalize-phi
     , directory
     , eo-phi-normalizer
     , filepath
+    , mtl
+    , string-interpolate
     , yaml
   default-language: Haskell2010
 
@@ -88,7 +95,7 @@ test-suite eo-phi-normalizer-test
       Paths_eo_phi_normalizer
   hs-source-dirs:
       test
-  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -Wno-missing-export-lists -threaded -rtsopts -with-rtsopts=-N
+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -Wno-missing-export-lists -Werror -threaded -rtsopts -with-rtsopts=-N
   build-tools:
       alex >=3.2.4
     , happy >=1.19.9
@@ -103,5 +110,7 @@ test-suite eo-phi-normalizer-test
     , filepath
     , hspec
     , hspec-discover
+    , mtl
+    , string-interpolate
     , yaml
   default-language: Haskell2010

eo-phi-normalizer/grammar/EO/Phi/Syntax.cf

@@ -27,17 +27,17 @@ separator Binding "," ;
 Phi.    Attribute ::= "φ" ;   -- decoratee object
 Rho.    Attribute ::= "ρ" ;   -- parent object
 Sigma.  Attribute ::= "σ" ;   -- home object
-VTX.    Attribute ::= "ν" ;   -- ???
+VTX.    Attribute ::= "ν" ;   -- the vertex identifier (an object that represents the unique identifier of the containing object)
 Label.  Attribute ::= LabelId ;
 Alpha.  Attribute ::= AlphaIndex ;
 
 PeeledObject. PeeledObject ::= ObjectHead [ObjectAction] ;
 
-HeadFormation.    ObjectHead ::= "{" [Binding] "}" ;
+HeadFormation.    ObjectHead ::= "⟦" [Binding] "⟧" ;
 HeadGlobal.       ObjectHead ::= "Φ" ;
 HeadThis.         ObjectHead ::= "ξ" ;
 HeadTermination.  ObjectHead ::= "⊥" ;
 
-ActionApplication.  ObjectAction ::= "{" [Binding] "}" ;
+ActionApplication.  ObjectAction ::= "(" [Binding] ")" ;
 ActionDispatch.     ObjectAction ::= "." Attribute ;
 separator ObjectAction "" ;

eo-phi-normalizer/package.yaml

@@ -41,6 +41,8 @@ dependencies:
 - directory
 - filepath
 - yaml
+- mtl
+- string-interpolate
 
 ghc-options:
 - -Wall
@@ -53,6 +55,7 @@ ghc-options:
 - -Wpartial-fields
 - -Wredundant-constraints
 - -Wno-missing-export-lists
+- -Werror
 
 library:
   source-dirs: src

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

@@ -1,44 +1,87 @@
 {-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE RecordWildCards #-}
 
-module Language.EO.Phi.Normalize where
+module Language.EO.Phi.Normalize (
+  normalizeObject,
+  normalize,
+  peelObject,
+  unpeelObject,
+) where
 
+import Control.Monad.State
 import Data.Maybe (fromMaybe)
+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
+isNu _ = False
 
 -- | Normalize an input 𝜑-program.
 normalize :: Program -> Program
-normalize (Program bindings) = Program (map (normalizeBindingWith context) bindings)
+normalize (Program bindings) = evalState (Program . objectBindings <$> normalizeObject (Formation bindings)) context
  where
   context =
     Context
       { globalObject = bindings
       , thisObject = bindings
+      , totalNuCount = nuCount bindings
       }
+  nuCount binds = count isNu binds + sum (map (sum . map (nuCount . objectBindings) . values) binds)
+  count = (length .) . filter
+  values (AlphaBinding _ obj) = [obj]
+  values _ = []
+  objectBindings (Formation bs) = bs
+  objectBindings _ = []
 
-normalizeBindingWith :: Context -> Binding -> Binding
-normalizeBindingWith context = \case
-  AlphaBinding a object -> AlphaBinding a (normalizeObjectWith context object)
-  binding -> binding
+rule1 :: Object -> State Context Object
+rule1 (Formation bindings) = do
+  normalizedBindings <- forM bindings $ \case
+    AlphaBinding a object
+      | a /= VTX ->
+          do
+            object' <- rule1 object
+            pure (AlphaBinding a object')
+    b -> pure b
+  finalBindings <-
+    if not $ any isNu normalizedBindings
+      then do
+        nus <- gets totalNuCount
+        modify (\c -> c{totalNuCount = totalNuCount c + 1})
+        let pad s = (if even (length s) then "" else "0") ++ s
+        let insertDashes s
+              | length s <= 2 = s ++ "-"
+              | otherwise =
+                  let go = \case
+                        [] -> []
+                        [x] -> [x]
+                        [x, y] -> [x, y, '-']
+                        (x : y : xs) -> x : y : '-' : go xs
+                   in go s
+        let dataObject = Formation [DeltaBinding $ Bytes $ insertDashes $ pad $ showHex nus ""]
+        pure (AlphaBinding VTX dataObject : normalizedBindings)
+      else do
+        pure normalizedBindings
+  pure (Formation finalBindings)
+rule1 object = pure object
 
-normalizeObjectWith :: Context -> Object -> Object
-normalizeObjectWith Context{..} object =
+normalizeObject :: Object -> State Context Object
+normalizeObject object = do
+  this <- gets thisObject
   case object of
-    ThisDispatch a ->
-      fromMaybe object (lookupBinding a thisObject)
-    _ -> object
+    -- Rule 1
+    obj@(Formation _) -> rule1 obj
+    ThisDispatch a -> pure $ fromMaybe object (lookupBinding a this)
+    _ -> pure object
 
 -- | Split compound object into its head and applications/dispatch actions.
 peelObject :: Object -> PeeledObject

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

@@ -0,0 +1,88 @@
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE RecordWildCards #-}
+module Language.EO.Phi.Rules.Common where
+
+import Language.EO.Phi.Syntax.Abs
+import Control.Applicative (asum, Alternative ((<|>)))
+
+-- $setup
+-- >>> :set -XOverloadedStrings
+-- >>> import Language.EO.Phi.Syntax
+
+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' ]
+
+-- * 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