From 9f4c9acf50f1d1a8d0b49a21bcc2eb508a35bc2d Mon Sep 17 00:00:00 2001
From: Abdelrahman Abounegm <abounegm.abdelrahman@gmail.com>
Date: Mon, 25 Dec 2023 10:26:51 +0300
Subject: [PATCH 01/23] Fix bytes token rule in grammar

---
 eo-phi-normalizer/grammar/EO/Phi/Syntax.cf    |   7 +-
 .../src/Language/EO/Phi/Syntax/Abs.hs         |   2 +-
 .../src/Language/EO/Phi/Syntax/Doc.txt        | 172 +++++++++---------
 .../src/Language/EO/Phi/Syntax/Lex.x          |   4 +-
 .../src/Language/EO/Phi/Syntax/Par.y          |   2 +-
 .../src/Language/EO/Phi/Syntax/Print.hs       |   2 +-
 6 files changed, 96 insertions(+), 93 deletions(-)

diff --git a/eo-phi-normalizer/grammar/EO/Phi/Syntax.cf b/eo-phi-normalizer/grammar/EO/Phi/Syntax.cf
index 40099c94c..1ba2696af 100644
--- a/eo-phi-normalizer/grammar/EO/Phi/Syntax.cf
+++ b/eo-phi-normalizer/grammar/EO/Phi/Syntax.cf
@@ -4,7 +4,10 @@
 --
 -- This is a non-ambiguous grammar for φ-programs.
 
-token Bytes ({"--"} | ["0123456789ABCDEF"] ["0123456789ABCDEF"] ({"-"} ["0123456789ABCDEF"] ["0123456789ABCDEF"])* {"--"}) ;
+token Bytes ({"--"}
+            | ["0123456789ABCDEF"] ["0123456789ABCDEF"] {"-"}
+            | (["0123456789ABCDEF"] ["0123456789ABCDEF"] {"-"} ["0123456789ABCDEF"] ["0123456789ABCDEF"])+)
+            ;
 token Function upper (char - [" \r\n\t,.|':;!-?][}{)(⟧⟦"])* ;
 token LabelId  lower (char - [" \r\n\t,.|':;!-?][}{)(⟧⟦"])* ;
 token AlphaIndex ({"α0"} | {"α"} (digit - ["0"]) (digit)* ) ;
@@ -27,7 +30,7 @@ separator Binding "," ;
 Phi.    Attribute ::= "φ" ;   -- decoratee object
 Rho.    Attribute ::= "ρ" ;   -- parent object
 Sigma.  Attribute ::= "σ" ;   -- home object
-VTX.    Attribute ::= "ν" ;   -- ???
+VTX.    Attribute ::= "ν" ;   -- an object that represents the unique identifier of the containing object
 Label.  Attribute ::= LabelId ;
 Alpha.  Attribute ::= AlphaIndex ;
 
diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Abs.hs b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Abs.hs
index 4ae129573..9a58833ce 100644
--- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Abs.hs
+++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Abs.hs
@@ -1,4 +1,4 @@
--- File generated by the BNF Converter (bnfc 2.9.5).
+-- File generated by the BNF Converter (bnfc 2.9.6).
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Doc.txt b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Doc.txt
index d611fb084..6e5dd3b6c 100644
--- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Doc.txt
+++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Doc.txt
@@ -1,86 +1,86 @@
-The Language Syntax
-BNF Converter
-
-
-%Process by txt2tags to generate html or latex
-
-
-
-This document was automatically generated by the //BNF-Converter//. It was generated together with the lexer, the parser, and the abstract syntax module, which guarantees that the document matches with the implementation of the language (provided no hand-hacking has taken place).
-
-==The lexical structure of Syntax==
-
-===Literals===
-
-
-
-
-
-Bytes literals are recognized by the regular expression
-`````{"--"} | ["0123456789ABCDEF"] ["0123456789ABCDEF"] ('-' ["0123456789ABCDEF"] ["0123456789ABCDEF"])* {"--"}`````
-
-Function literals are recognized by the regular expression
-`````upper (char - ["
-
 !'(),-.:;?[]{|}⟦⟧"])*`````
-
-LabelId literals are recognized by the regular expression
-`````lower (char - ["
-
 !'(),-.:;?[]{|}⟦⟧"])*`````
-
-AlphaIndex literals are recognized by the regular expression
-`````{"α0"} | 'α' (digit - '0') digit*`````
-
-
-===Reserved words and symbols===
-The set of reserved words is the set of terminals appearing in the grammar. Those reserved words that consist of non-letter characters are called symbols, and they are treated in a different way from those that are similar to identifiers. The lexer follows rules familiar from languages like Haskell, C, and Java, including longest match and spacing conventions.
-
-The reserved words used in Syntax are the following:
-  | ``Δ`` | ``Φ`` | ``λ`` | ``ν``
-  | ``ξ`` | ``ρ`` | ``σ`` | ``φ``
-
-The symbols used in Syntax are the following:
-  | { | } | . | ⊥
-  | ↦ | ∅ | ⤍ | ,
-
-===Comments===
-There are no single-line comments in the grammar.There are no multiple-line comments in the grammar.
-
-==The syntactic structure of Syntax==
-Non-terminals are enclosed between < and >.
-The symbols -> (production),  **|**  (union)
-and **eps** (empty rule) belong to the BNF notation.
-All other symbols are terminals.
-
-  | //Program// | -> | ``{`` //[Binding]// ``}``
-  | //Object// | -> | ``{`` //[Binding]// ``}``
-  |  |  **|**  | //Object// ``{`` //[Binding]// ``}``
-  |  |  **|**  | //Object// ``.`` //Attribute//
-  |  |  **|**  | ``Φ`` ``.`` //Attribute//
-  |  |  **|**  | ``ξ`` ``.`` //Attribute//
-  |  |  **|**  | ``⊥``
-  | //Binding// | -> | //Attribute// ``↦`` //Object//
-  |  |  **|**  | //Attribute// ``↦`` ``∅``
-  |  |  **|**  | ``Δ`` ``⤍`` //Bytes//
-  |  |  **|**  | ``λ`` ``⤍`` //Function//
-  | //[Binding]// | -> | **eps**
-  |  |  **|**  | //Binding//
-  |  |  **|**  | //Binding// ``,`` //[Binding]//
-  | //Attribute// | -> | ``φ``
-  |  |  **|**  | ``ρ``
-  |  |  **|**  | ``σ``
-  |  |  **|**  | ``ν``
-  |  |  **|**  | //LabelId//
-  |  |  **|**  | //AlphaIndex//
-  | //PeeledObject// | -> | //ObjectHead// //[ObjectAction]//
-  | //ObjectHead// | -> | ``{`` //[Binding]// ``}``
-  |  |  **|**  | ``Φ``
-  |  |  **|**  | ``ξ``
-  |  |  **|**  | ``⊥``
-  | //ObjectAction// | -> | ``{`` //[Binding]// ``}``
-  |  |  **|**  | ``.`` //Attribute//
-  | //[ObjectAction]// | -> | **eps**
-  |  |  **|**  | //ObjectAction// //[ObjectAction]//
-
-
-
-%% File generated by the BNF Converter (bnfc 2.9.5).
+The Language Syntax
+BNF Converter
+
+
+%Process by txt2tags to generate html or latex
+
+
+
+This document was automatically generated by the //BNF-Converter//. It was generated together with the lexer, the parser, and the abstract syntax module, which guarantees that the document matches with the implementation of the language (provided no hand-hacking has taken place).
+
+==The lexical structure of Syntax==
+
+===Literals===
+
+
+
+
+
+Bytes literals are recognized by the regular expression
+`````{"--"} | ["0123456789ABCDEF"] ["0123456789ABCDEF"] '-' | (["0123456789ABCDEF"] ["0123456789ABCDEF"] '-' ["0123456789ABCDEF"] ["0123456789ABCDEF"])+`````
+
+Function literals are recognized by the regular expression
+`````upper (char - ["
+
 !'(),-.:;?[]{|}⟦⟧"])*`````
+
+LabelId literals are recognized by the regular expression
+`````lower (char - ["
+
 !'(),-.:;?[]{|}⟦⟧"])*`````
+
+AlphaIndex literals are recognized by the regular expression
+`````{"α0"} | 'α' (digit - '0') digit*`````
+
+
+===Reserved words and symbols===
+The set of reserved words is the set of terminals appearing in the grammar. Those reserved words that consist of non-letter characters are called symbols, and they are treated in a different way from those that are similar to identifiers. The lexer follows rules familiar from languages like Haskell, C, and Java, including longest match and spacing conventions.
+
+The reserved words used in Syntax are the following:
+  | ``Δ`` | ``Φ`` | ``λ`` | ``ν``
+  | ``ξ`` | ``ρ`` | ``σ`` | ``φ``
+
+The symbols used in Syntax are the following:
+  | { | } | . | ⊥
+  | ↦ | ∅ | ⤍ | ,
+
+===Comments===
+There are no single-line comments in the grammar.There are no multiple-line comments in the grammar.
+
+==The syntactic structure of Syntax==
+Non-terminals are enclosed between < and >.
+The symbols -> (production),  **|**  (union)
+and **eps** (empty rule) belong to the BNF notation.
+All other symbols are terminals.
+
+  | //Program// | -> | ``{`` //[Binding]// ``}``
+  | //Object// | -> | ``{`` //[Binding]// ``}``
+  |  |  **|**  | //Object// ``{`` //[Binding]// ``}``
+  |  |  **|**  | //Object// ``.`` //Attribute//
+  |  |  **|**  | ``Φ`` ``.`` //Attribute//
+  |  |  **|**  | ``ξ`` ``.`` //Attribute//
+  |  |  **|**  | ``⊥``
+  | //Binding// | -> | //Attribute// ``↦`` //Object//
+  |  |  **|**  | //Attribute// ``↦`` ``∅``
+  |  |  **|**  | ``Δ`` ``⤍`` //Bytes//
+  |  |  **|**  | ``λ`` ``⤍`` //Function//
+  | //[Binding]// | -> | **eps**
+  |  |  **|**  | //Binding//
+  |  |  **|**  | //Binding// ``,`` //[Binding]//
+  | //Attribute// | -> | ``φ``
+  |  |  **|**  | ``ρ``
+  |  |  **|**  | ``σ``
+  |  |  **|**  | ``ν``
+  |  |  **|**  | //LabelId//
+  |  |  **|**  | //AlphaIndex//
+  | //PeeledObject// | -> | //ObjectHead// //[ObjectAction]//
+  | //ObjectHead// | -> | ``{`` //[Binding]// ``}``
+  |  |  **|**  | ``Φ``
+  |  |  **|**  | ``ξ``
+  |  |  **|**  | ``⊥``
+  | //ObjectAction// | -> | ``{`` //[Binding]// ``}``
+  |  |  **|**  | ``.`` //Attribute//
+  | //[ObjectAction]// | -> | **eps**
+  |  |  **|**  | //ObjectAction// //[ObjectAction]//
+
+
+
+%% File generated by the BNF Converter (bnfc 2.9.6).
diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Lex.x b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Lex.x
index 6978d4e61..bcb8c56a3 100644
--- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Lex.x
+++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Lex.x
@@ -1,4 +1,4 @@
--- -*- haskell -*- File generated by the BNF Converter (bnfc 2.9.5).
+-- -*- haskell -*- File generated by the BNF Converter (bnfc 2.9.6).
 
 -- Lexer definition for use with Alex 3
 {
@@ -40,7 +40,7 @@ $white+ ;
     { tok (eitherResIdent TV) }
 
 -- token Bytes
-\- \- | [0 1 2 3 4 5 6 7 8 9 A B C D E F][0 1 2 3 4 5 6 7 8 9 A B C D E F](\- [0 1 2 3 4 5 6 7 8 9 A B C D E F][0 1 2 3 4 5 6 7 8 9 A B C D E F]) * (\- \-)
+\- \- | [0 1 2 3 4 5 6 7 8 9 A B C D E F][0 1 2 3 4 5 6 7 8 9 A B C D E F]\- | ([0 1 2 3 4 5 6 7 8 9 A B C D E F][0 1 2 3 4 5 6 7 8 9 A B C D E F]\- [0 1 2 3 4 5 6 7 8 9 A B C D E F][0 1 2 3 4 5 6 7 8 9 A B C D E F]) +
     { tok (eitherResIdent T_Bytes) }
 
 -- token Function
diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Par.y b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Par.y
index e07d7cc2d..9fe41c67b 100644
--- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Par.y
+++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Par.y
@@ -1,4 +1,4 @@
--- -*- haskell -*- File generated by the BNF Converter (bnfc 2.9.5).
+-- -*- haskell -*- File generated by the BNF Converter (bnfc 2.9.6).
 
 -- Parser definition for use with Happy
 {
diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Print.hs b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Print.hs
index 835a64076..cb3eb0312 100644
--- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Print.hs
+++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Print.hs
@@ -1,4 +1,4 @@
--- File generated by the BNF Converter (bnfc 2.9.5).
+-- File generated by the BNF Converter (bnfc 2.9.6).
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE LambdaCase #-}

From c3d3cb8172b35a5118d74b7d238f7a24af1a30dd Mon Sep 17 00:00:00 2001
From: Abdelrahman Abounegm <abounegm.abdelrahman@gmail.com>
Date: Mon, 25 Dec 2023 10:27:26 +0300
Subject: [PATCH 02/23] Add an explicit export list

---
 eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs b/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs
index 817a409db..8aad53bea 100644
--- a/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs
+++ b/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs
@@ -1,7 +1,12 @@
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE RecordWildCards #-}
 
-module Language.EO.Phi.Normalize where
+module Language.EO.Phi.Normalize (
+  normalizeObjectWith,
+  normalize,
+  peelObject,
+  unpeelObject,
+) where
 
 import Data.Maybe (fromMaybe)
 import Language.EO.Phi.Syntax.Abs

From e20b57ab027fc66f23e4db8bd15440233bfb1baf Mon Sep 17 00:00:00 2001
From: Abdelrahman Abounegm <abounegm.abdelrahman@gmail.com>
Date: Mon, 25 Dec 2023 10:29:39 +0300
Subject: [PATCH 03/23] Add a draft implementation for the first rule

---
 .../src/Language/EO/Phi/Normalize.hs          | 27 ++++++++++++++++++-
 1 file changed, 26 insertions(+), 1 deletion(-)

diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs b/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs
index 8aad53bea..e03966b39 100644
--- a/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs
+++ b/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs
@@ -10,6 +10,7 @@ module Language.EO.Phi.Normalize (
 
 import Data.Maybe (fromMaybe)
 import Language.EO.Phi.Syntax.Abs
+import Numeric (showHex)
 
 data Context = Context
   { globalObject :: [Binding]
@@ -38,9 +39,33 @@ normalizeBindingWith context = \case
   AlphaBinding a object -> AlphaBinding a (normalizeObjectWith context object)
   binding -> binding
 
+count :: (a -> Bool) -> [a] -> Int
+count = (length .) . filter
+
 normalizeObjectWith :: Context -> Object -> Object
-normalizeObjectWith Context{..} object =
+normalizeObjectWith ctx@Context{..} object =
   case object of
+    -- Rule 1
+    Formation bindings -> Formation bindings'
+     where
+      bindings'
+        | not $ any isNu bindings = AlphaBinding VTX (dataObject nu) : normalizedBindings
+        | otherwise = normalizedBindings
+      normalizedBindings = map (normalizeBindingWith ctx) bindings
+      nuCount binds = count isNu binds + sum (map (sum . map (nuCount . objectBindings) . values) binds)
+      dataObject n = Formation [DeltaBinding $ Bytes $ showHex n ""]
+
+      values (AlphaBinding _ obj) = [obj]
+      values _ = []
+
+      objectBindings (Formation bs) = bs
+      objectBindings _ = []
+
+      isNu (AlphaBinding VTX _) = True
+      isNu (EmptyBinding VTX) = True
+      isNu _ = False
+
+      nu = nuCount normalizedBindings
     ThisDispatch a ->
       fromMaybe object (lookupBinding a thisObject)
     _ -> object

From 329d7822619f83323455fadfa2df071b0bd370e4 Mon Sep 17 00:00:00 2001
From: Abdelrahman Abounegm <abounegm.abdelrahman@gmail.com>
Date: Fri, 29 Dec 2023 00:41:25 +0300
Subject: [PATCH 04/23] Fix the implementation of the first rules using State
 monad to keep track of total Nu count

Co-authored-by: Danila Danko <deemp@users.noreply.github.com>
---
 eo-phi-normalizer/eo-phi-normalizer.cabal     |  3 +
 eo-phi-normalizer/package.yaml                |  1 +
 .../src/Language/EO/Phi/Normalize.hs          | 82 +++++++++++--------
 3 files changed, 51 insertions(+), 35 deletions(-)

diff --git a/eo-phi-normalizer/eo-phi-normalizer.cabal b/eo-phi-normalizer/eo-phi-normalizer.cabal
index 7949d9e9c..d7ba18152 100644
--- a/eo-phi-normalizer/eo-phi-normalizer.cabal
+++ b/eo-phi-normalizer/eo-phi-normalizer.cabal
@@ -54,6 +54,7 @@ library
     , base >=4.7 && <5
     , directory
     , filepath
+    , mtl
     , yaml
   default-language: Haskell2010
 
@@ -76,6 +77,7 @@ executable normalize-phi
     , directory
     , eo-phi-normalizer
     , filepath
+    , mtl
     , yaml
   default-language: Haskell2010
 
@@ -103,5 +105,6 @@ test-suite eo-phi-normalizer-test
     , filepath
     , hspec
     , hspec-discover
+    , mtl
     , yaml
   default-language: Haskell2010
diff --git a/eo-phi-normalizer/package.yaml b/eo-phi-normalizer/package.yaml
index 420d19164..da1735273 100644
--- a/eo-phi-normalizer/package.yaml
+++ b/eo-phi-normalizer/package.yaml
@@ -41,6 +41,7 @@ dependencies:
 - directory
 - filepath
 - yaml
+- mtl
 
 ghc-options:
 - -Wall
diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs b/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs
index e03966b39..4d35b5573 100644
--- a/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs
+++ b/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs
@@ -1,20 +1,23 @@
 {-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE RecordWildCards #-}
 
 module Language.EO.Phi.Normalize (
-  normalizeObjectWith,
+  normalizeObject,
   normalize,
   peelObject,
   unpeelObject,
 ) where
 
+import Control.Monad.State
 import Data.Maybe (fromMaybe)
-import Language.EO.Phi.Syntax.Abs
 import Numeric (showHex)
 
+import Control.Monad (forM)
+import Language.EO.Phi.Syntax.Abs
+
 data Context = Context
   { globalObject :: [Binding]
   , thisObject :: [Binding]
+  , totalNuCount :: Int
   }
 
 lookupBinding :: Attribute -> [Binding] -> Maybe Object
@@ -24,51 +27,60 @@ lookupBinding a (AlphaBinding a' object : bindings)
   | 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 <$> forM bindings normalizeBinding) 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
+normalizeBinding :: Binding -> State Context Binding
+normalizeBinding = \case
+  AlphaBinding a object -> AlphaBinding a <$> normalizeObject object
+  binding -> pure binding
 
-count :: (a -> Bool) -> [a] -> Int
-count = (length .) . filter
+rule1 :: Object -> State Context Object
+rule1 (Formation bindings) = do
+  normalizedBindings <- forM bindings $ \case
+    AlphaBinding a object -> 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 dataObject = Formation [DeltaBinding $ Bytes $ showHex nus ""]
+        pure (AlphaBinding VTX dataObject : normalizedBindings)
+      else do
+        pure normalizedBindings
+  pure (Formation finalBindings)
+rule1 object = pure object
 
-normalizeObjectWith :: Context -> Object -> Object
-normalizeObjectWith ctx@Context{..} object =
+normalizeObject :: Object -> State Context Object
+normalizeObject object = do
+  this <- gets thisObject
   case object of
     -- Rule 1
-    Formation bindings -> Formation bindings'
-     where
-      bindings'
-        | not $ any isNu bindings = AlphaBinding VTX (dataObject nu) : normalizedBindings
-        | otherwise = normalizedBindings
-      normalizedBindings = map (normalizeBindingWith ctx) bindings
-      nuCount binds = count isNu binds + sum (map (sum . map (nuCount . objectBindings) . values) binds)
-      dataObject n = Formation [DeltaBinding $ Bytes $ showHex n ""]
-
-      values (AlphaBinding _ obj) = [obj]
-      values _ = []
-
-      objectBindings (Formation bs) = bs
-      objectBindings _ = []
-
-      isNu (AlphaBinding VTX _) = True
-      isNu (EmptyBinding VTX) = True
-      isNu _ = False
-
-      nu = nuCount normalizedBindings
-    ThisDispatch a ->
-      fromMaybe object (lookupBinding a thisObject)
-    _ -> object
+    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

From 70d57e483a93af218a956a7e83ef8e6226f9f4dd Mon Sep 17 00:00:00 2001
From: Abdelrahman Abounegm <abounegm.abdelrahman@gmail.com>
Date: Fri, 29 Dec 2023 00:47:36 +0300
Subject: [PATCH 05/23] Stop normalizing objects that are values of Nu

Co-authored-by: Danila Danko <br4ch1st0chr0n3@gmail.com>
---
 eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs b/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs
index 4d35b5573..550d5fa5f 100644
--- a/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs
+++ b/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs
@@ -57,9 +57,11 @@ normalizeBinding = \case
 rule1 :: Object -> State Context Object
 rule1 (Formation bindings) = do
   normalizedBindings <- forM bindings $ \case
-    AlphaBinding a object -> do
-      object' <- rule1 object
-      pure (AlphaBinding a object')
+    AlphaBinding a object
+      | a /= VTX ->
+          do
+            object' <- rule1 object
+            pure (AlphaBinding a object')
     b -> pure b
   finalBindings <-
     if not $ any isNu normalizedBindings

From 802360a7f8591486cc1138ddf76a066c6148fa50 Mon Sep 17 00:00:00 2001
From: Abdelrahman Abounegm <abounegm.abdelrahman@gmail.com>
Date: Fri, 29 Dec 2023 00:48:42 +0300
Subject: [PATCH 06/23] Treat program as a formation when normalizing

So that state would be preserved across its bindings

Co-authored-by: Danila Danko <br4ch1st0chr0n3@gmail.com>
---
 eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs b/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs
index 550d5fa5f..03b0e5df5 100644
--- a/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs
+++ b/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs
@@ -34,7 +34,7 @@ isNu _ = False
 
 -- | Normalize an input 𝜑-program.
 normalize :: Program -> Program
-normalize (Program bindings) = evalState (Program <$> forM bindings normalizeBinding) context
+normalize (Program bindings) = evalState (Program . objectBindings <$> normalizeObject (Formation bindings)) context
  where
   context =
     Context
@@ -49,11 +49,6 @@ normalize (Program bindings) = evalState (Program <$> forM bindings normalizeBin
   objectBindings (Formation bs) = bs
   objectBindings _ = []
 
-normalizeBinding :: Binding -> State Context Binding
-normalizeBinding = \case
-  AlphaBinding a object -> AlphaBinding a <$> normalizeObject object
-  binding -> pure binding
-
 rule1 :: Object -> State Context Object
 rule1 (Formation bindings) = do
   normalizedBindings <- forM bindings $ \case

From ac64050f534efcd12dceea9c8994d50256418af2 Mon Sep 17 00:00:00 2001
From: Abdelrahman Abounegm <abounegm.abdelrahman@gmail.com>
Date: Fri, 29 Dec 2023 00:57:58 +0300
Subject: [PATCH 07/23] Update tests

---
 eo-phi-normalizer/test/eo/phi/normal-1.yaml |  6 +++---
 eo-phi-normalizer/test/eo/phi/normal-2.yaml |  6 +++---
 eo-phi-normalizer/test/eo/phi/test.yaml     | 11 ++++-------
 3 files changed, 10 insertions(+), 13 deletions(-)

diff --git a/eo-phi-normalizer/test/eo/phi/normal-1.yaml b/eo-phi-normalizer/test/eo/phi/normal-1.yaml
index 758437236..053ba0630 100644
--- a/eo-phi-normalizer/test/eo/phi/normal-1.yaml
+++ b/eo-phi-normalizer/test/eo/phi/normal-1.yaml
@@ -1,7 +1,7 @@
-name: "Program in normal form (1)"
+name: 'Program in normal form (1)'
 input: |
   {}
 normalized: |
-  {}
+  { ν ↦ { Δ ⤍ 0 } }
 prettified: |
-  { }
+  { ν ↦ { Δ ⤍ 0 } }
diff --git a/eo-phi-normalizer/test/eo/phi/normal-2.yaml b/eo-phi-normalizer/test/eo/phi/normal-2.yaml
index 2420abe2f..5b885cbe2 100644
--- a/eo-phi-normalizer/test/eo/phi/normal-2.yaml
+++ b/eo-phi-normalizer/test/eo/phi/normal-2.yaml
@@ -1,7 +1,7 @@
-name: "Program in normal form (2)"
+name: 'Program in normal form (2)'
 input: |
   { φ ↦ { φ ↦ { φ ↦ { } } } }
 normalized: |
-  { φ ↦ { φ ↦ { φ ↦ { } } } }
+  { ν ↦ { Δ ⤍ 3 }, φ ↦ { ν ↦ { Δ ⤍ 2 }, φ ↦ { ν ↦ { Δ ⤍ 1 }, φ ↦ { ν ↦ { Δ ⤍ 0 } } } } }
 prettified: |
-  { φ ↦ { φ ↦ { φ ↦ { } } } }
+  { ν ↦ { Δ ⤍ 3 }, φ ↦ { ν ↦ { Δ ⤍ 2 }, φ ↦ { ν ↦ { Δ ⤍ 1 }, φ ↦ { ν ↦ { Δ ⤍ 0 } } } } }
diff --git a/eo-phi-normalizer/test/eo/phi/test.yaml b/eo-phi-normalizer/test/eo/phi/test.yaml
index 741ee8506..07ebcb315 100644
--- a/eo-phi-normalizer/test/eo/phi/test.yaml
+++ b/eo-phi-normalizer/test/eo/phi/test.yaml
@@ -1,10 +1,7 @@
-name: "Simple static attribute reference"
+name: 'Simple static attribute reference'
 input: |
-  { φ ↦ {   } , a ↦ ξ.φ }
+  { φ ↦ { } , a ↦ ξ.φ }
 normalized: |
-  {
-    φ ↦ {},
-    a ↦ {}
-  }
+  { ν ↦ { Δ ⤍ 1 }, φ ↦ { ν ↦ { Δ ⤍ 0 } }, a ↦ ξ.φ }
 prettified: |
-  { φ ↦ { }, a ↦ ξ.φ }
+  { ν ↦ { Δ ⤍ 1 }, φ ↦ { ν ↦ { Δ ⤍ 0 } }, a ↦ ξ.φ }

From 59d4e425569af06fe724a5458287b543a6f4d68e Mon Sep 17 00:00:00 2001
From: Abdelrahman Abounegm <abounegm.abdelrahman@gmail.com>
Date: Fri, 29 Dec 2023 01:30:37 +0300
Subject: [PATCH 08/23] Fix the hex representation of data bytes

Co-authored-by: Danila Danko <br4ch1st0chr0n3@gmail.com>
---
 eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs b/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs
index 03b0e5df5..9010d5aee 100644
--- a/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs
+++ b/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs
@@ -63,7 +63,17 @@ rule1 (Formation bindings) = do
       then do
         nus <- gets totalNuCount
         modify (\c -> c{totalNuCount = totalNuCount c + 1})
-        let dataObject = Formation [DeltaBinding $ Bytes $ showHex nus ""]
+        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

From b296cddce619a692a08f5571055772ee731c8cd2 Mon Sep 17 00:00:00 2001
From: Abdelrahman Abounegm <abounegm.abdelrahman@gmail.com>
Date: Fri, 29 Dec 2023 01:31:34 +0300
Subject: [PATCH 09/23] Change the test Yaml format to an array of tests

Co-authored-by: Danila Danko <br4ch1st0chr0n3@gmail.com>
---
 eo-phi-normalizer/test/Language/EO/PhiSpec.hs |  4 ++--
 eo-phi-normalizer/test/Test/EO/Phi.hs         |  2 +-
 eo-phi-normalizer/test/eo/phi/normal-1.yaml   |  7 -------
 eo-phi-normalizer/test/eo/phi/normal-2.yaml   |  7 -------
 eo-phi-normalizer/test/eo/phi/rule-1.yaml     | 15 +++++++++++++++
 eo-phi-normalizer/test/eo/phi/rule-5.yaml     |  7 +++++++
 eo-phi-normalizer/test/eo/phi/test.yaml       |  7 -------
 7 files changed, 25 insertions(+), 24 deletions(-)
 delete mode 100644 eo-phi-normalizer/test/eo/phi/normal-1.yaml
 delete mode 100644 eo-phi-normalizer/test/eo/phi/normal-2.yaml
 create mode 100644 eo-phi-normalizer/test/eo/phi/rule-1.yaml
 create mode 100644 eo-phi-normalizer/test/eo/phi/rule-5.yaml
 delete mode 100644 eo-phi-normalizer/test/eo/phi/test.yaml

diff --git a/eo-phi-normalizer/test/Language/EO/PhiSpec.hs b/eo-phi-normalizer/test/Language/EO/PhiSpec.hs
index 195d02d05..a4b22d891 100644
--- a/eo-phi-normalizer/test/Language/EO/PhiSpec.hs
+++ b/eo-phi-normalizer/test/Language/EO/PhiSpec.hs
@@ -14,10 +14,10 @@ spec :: Spec
 spec = do
   tests <- runIO (allPhiTests "test/eo/phi/")
   describe "Normalizer" $ do
-    forM_ tests $ \PhiTest{..} -> do
+    forM_ tests $ mapM_ $ \PhiTest{..} -> do
       it name $ do
         Phi.printTree (Phi.normalize input) `shouldBe` Phi.printTree normalized
   describe "Prettify" $ do
-    forM_ tests $ \PhiTest{..} -> do
+    forM_ tests $ mapM_ $ \PhiTest{..} -> do
       it name $ do
         Phi.printTree input `shouldBe` dropWhileEnd isSpace prettified
diff --git a/eo-phi-normalizer/test/Test/EO/Phi.hs b/eo-phi-normalizer/test/Test/EO/Phi.hs
index b4f9f16ff..0f98d1fb2 100644
--- a/eo-phi-normalizer/test/Test/EO/Phi.hs
+++ b/eo-phi-normalizer/test/Test/EO/Phi.hs
@@ -24,7 +24,7 @@ data PhiTest = PhiTest
   }
   deriving (Generic, FromJSON)
 
-allPhiTests :: FilePath -> IO [PhiTest]
+allPhiTests :: FilePath -> IO [[PhiTest]]
 allPhiTests dir = do
   paths <- listDirectory dir
   forM (sort paths) $ \path ->
diff --git a/eo-phi-normalizer/test/eo/phi/normal-1.yaml b/eo-phi-normalizer/test/eo/phi/normal-1.yaml
deleted file mode 100644
index 053ba0630..000000000
--- a/eo-phi-normalizer/test/eo/phi/normal-1.yaml
+++ /dev/null
@@ -1,7 +0,0 @@
-name: 'Program in normal form (1)'
-input: |
-  {}
-normalized: |
-  { ν ↦ { Δ ⤍ 0 } }
-prettified: |
-  { ν ↦ { Δ ⤍ 0 } }
diff --git a/eo-phi-normalizer/test/eo/phi/normal-2.yaml b/eo-phi-normalizer/test/eo/phi/normal-2.yaml
deleted file mode 100644
index 5b885cbe2..000000000
--- a/eo-phi-normalizer/test/eo/phi/normal-2.yaml
+++ /dev/null
@@ -1,7 +0,0 @@
-name: 'Program in normal form (2)'
-input: |
-  { φ ↦ { φ ↦ { φ ↦ { } } } }
-normalized: |
-  { ν ↦ { Δ ⤍ 3 }, φ ↦ { ν ↦ { Δ ⤍ 2 }, φ ↦ { ν ↦ { Δ ⤍ 1 }, φ ↦ { ν ↦ { Δ ⤍ 0 } } } } }
-prettified: |
-  { ν ↦ { Δ ⤍ 3 }, φ ↦ { ν ↦ { Δ ⤍ 2 }, φ ↦ { ν ↦ { Δ ⤍ 1 }, φ ↦ { ν ↦ { Δ ⤍ 0 } } } } }
diff --git a/eo-phi-normalizer/test/eo/phi/rule-1.yaml b/eo-phi-normalizer/test/eo/phi/rule-1.yaml
new file mode 100644
index 000000000..1652f59e5
--- /dev/null
+++ b/eo-phi-normalizer/test/eo/phi/rule-1.yaml
@@ -0,0 +1,15 @@
+- name: 'Program in normal form (1)'
+  input: |
+    {}
+  normalized: |
+    { ν ↦ { Δ ⤍ 00- } }
+  prettified: |
+    { }
+
+- name: 'Program in normal form (2)'
+  input: |
+    { φ ↦ { φ ↦ { φ ↦ { } } } }
+  normalized: |
+    { ν ↦ { Δ ⤍ 03- }, φ ↦ { ν ↦ { Δ ⤍ 02- }, φ ↦ { ν ↦ { Δ ⤍ 01- }, φ ↦ { ν ↦ { Δ ⤍ 00- } } } } }
+  prettified: |
+    { φ ↦ { φ ↦ { φ ↦ { } } } }
diff --git a/eo-phi-normalizer/test/eo/phi/rule-5.yaml b/eo-phi-normalizer/test/eo/phi/rule-5.yaml
new file mode 100644
index 000000000..5ae468e8b
--- /dev/null
+++ b/eo-phi-normalizer/test/eo/phi/rule-5.yaml
@@ -0,0 +1,7 @@
+- name: 'Simple static attribute reference'
+  input: |
+    { φ ↦ { } , a ↦ ξ.φ }
+  normalized: |
+    { ν ↦ { Δ ⤍ 01- }, φ ↦ { ν ↦ { Δ ⤍ 00- } }, a ↦ ξ.φ }
+  prettified: |
+    { φ ↦ { }, a ↦ ξ.φ }
diff --git a/eo-phi-normalizer/test/eo/phi/test.yaml b/eo-phi-normalizer/test/eo/phi/test.yaml
deleted file mode 100644
index 07ebcb315..000000000
--- a/eo-phi-normalizer/test/eo/phi/test.yaml
+++ /dev/null
@@ -1,7 +0,0 @@
-name: 'Simple static attribute reference'
-input: |
-  { φ ↦ { } , a ↦ ξ.φ }
-normalized: |
-  { ν ↦ { Δ ⤍ 1 }, φ ↦ { ν ↦ { Δ ⤍ 0 } }, a ↦ ξ.φ }
-prettified: |
-  { ν ↦ { Δ ⤍ 1 }, φ ↦ { ν ↦ { Δ ⤍ 0 } }, a ↦ ξ.φ }

From c4f6a161c027c617d1e1eebad7c1dc997465a247 Mon Sep 17 00:00:00 2001
From: Abdelrahman Abounegm <abounegm.abdelrahman@gmail.com>
Date: Wed, 10 Jan 2024 09:27:52 +0300
Subject: [PATCH 10/23] Update syntax in phi unit tests

---
 eo-phi-normalizer/test/eo/phi/rule-1.yaml | 8 ++++----
 eo-phi-normalizer/test/eo/phi/rule-5.yaml | 6 +++---
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/eo-phi-normalizer/test/eo/phi/rule-1.yaml b/eo-phi-normalizer/test/eo/phi/rule-1.yaml
index 1652f59e5..c37aa8a9c 100644
--- a/eo-phi-normalizer/test/eo/phi/rule-1.yaml
+++ b/eo-phi-normalizer/test/eo/phi/rule-1.yaml
@@ -2,14 +2,14 @@
   input: |
     {}
   normalized: |
-    { ν ↦ { Δ ⤍ 00- } }
+    { ν ↦ ⟦ Δ ⤍ 00- ⟧ }
   prettified: |
     { }
 
 - name: 'Program in normal form (2)'
   input: |
-    { φ ↦ { φ ↦ { φ ↦ { } } } }
+    { φ ↦ ⟦ φ ↦ ⟦ φ ↦ ⟦ ⟧ ⟧ ⟧ }
   normalized: |
-    { ν ↦ { Δ ⤍ 03- }, φ ↦ { ν ↦ { Δ ⤍ 02- }, φ ↦ { ν ↦ { Δ ⤍ 01- }, φ ↦ { ν ↦ { Δ ⤍ 00- } } } } }
+    { ν ↦ ⟦ Δ ⤍ 03- ⟧, φ ↦ ⟦ ν ↦ ⟦ Δ ⤍ 02- ⟧, φ ↦ ⟦ ν ↦ ⟦ Δ ⤍ 01- ⟧, φ ↦ ⟦ ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧ ⟧ ⟧ }
   prettified: |
-    { φ ↦ { φ ↦ { φ ↦ { } } } }
+    { φ ↦ ⟦ φ ↦ ⟦ φ ↦ ⟦ ⟧ ⟧ ⟧ }
diff --git a/eo-phi-normalizer/test/eo/phi/rule-5.yaml b/eo-phi-normalizer/test/eo/phi/rule-5.yaml
index 5ae468e8b..ab5ee703a 100644
--- a/eo-phi-normalizer/test/eo/phi/rule-5.yaml
+++ b/eo-phi-normalizer/test/eo/phi/rule-5.yaml
@@ -1,7 +1,7 @@
 - name: 'Simple static attribute reference'
   input: |
-    { φ ↦ { } , a ↦ ξ.φ }
+    { φ ↦ ⟦ ⟧ , a ↦ ξ.φ }
   normalized: |
-    { ν ↦ { Δ ⤍ 01- }, φ ↦ { ν ↦ { Δ ⤍ 00- } }, a ↦ ξ.φ }
+    { ν ↦ ⟦ Δ ⤍ 01- ⟧, φ ↦ ⟦ ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, a ↦ ξ.φ }
   prettified: |
-    { φ ↦ { }, a ↦ ξ.φ }
+    { φ ↦ ⟦ ⟧, a ↦ ξ.φ }

From 17f46eee99becf6f88614514682e208e06148387 Mon Sep 17 00:00:00 2001
From: Danila Danko <br4ch1st0chr0n3@gmail.com>
Date: Wed, 10 Jan 2024 12:46:25 +0300
Subject: [PATCH 11/23] Revert "Fix bytes token rule in grammar"

This reverts commit 9f4c9acf50f1d1a8d0b49a21bcc2eb508a35bc2d.
---
 eo-phi-normalizer/grammar/EO/Phi/Syntax.cf            | 7 ++-----
 eo-phi-normalizer/src/Language/EO/Phi/Syntax/Abs.hs   | 2 +-
 eo-phi-normalizer/src/Language/EO/Phi/Syntax/Lex.x    | 4 ++--
 eo-phi-normalizer/src/Language/EO/Phi/Syntax/Par.y    | 2 +-
 eo-phi-normalizer/src/Language/EO/Phi/Syntax/Print.hs | 2 +-
 5 files changed, 7 insertions(+), 10 deletions(-)

diff --git a/eo-phi-normalizer/grammar/EO/Phi/Syntax.cf b/eo-phi-normalizer/grammar/EO/Phi/Syntax.cf
index 12842f2d0..be9180219 100644
--- a/eo-phi-normalizer/grammar/EO/Phi/Syntax.cf
+++ b/eo-phi-normalizer/grammar/EO/Phi/Syntax.cf
@@ -4,10 +4,7 @@
 --
 -- This is a non-ambiguous grammar for φ-programs.
 
-token Bytes ({"--"}
-            | ["0123456789ABCDEF"] ["0123456789ABCDEF"] {"-"}
-            | (["0123456789ABCDEF"] ["0123456789ABCDEF"] {"-"} ["0123456789ABCDEF"] ["0123456789ABCDEF"])+)
-            ;
+token Bytes ({"--"} | ["0123456789ABCDEF"] ["0123456789ABCDEF"] ({"-"} ["0123456789ABCDEF"] ["0123456789ABCDEF"])* {"--"}) ;
 token Function upper (char - [" \r\n\t,.|':;!-?][}{)(⟧⟦"])* ;
 token LabelId  lower (char - [" \r\n\t,.|':;!-?][}{)(⟧⟦"])* ;
 token AlphaIndex ({"α0"} | {"α"} (digit - ["0"]) (digit)* ) ;
@@ -30,7 +27,7 @@ separator Binding "," ;
 Phi.    Attribute ::= "φ" ;   -- decoratee object
 Rho.    Attribute ::= "ρ" ;   -- parent object
 Sigma.  Attribute ::= "σ" ;   -- home object
-VTX.    Attribute ::= "ν" ;   -- an object that represents the unique identifier of the containing object
+VTX.    Attribute ::= "ν" ;   -- ???
 Label.  Attribute ::= LabelId ;
 Alpha.  Attribute ::= AlphaIndex ;
 
diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Abs.hs b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Abs.hs
index 9a58833ce..4ae129573 100644
--- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Abs.hs
+++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Abs.hs
@@ -1,4 +1,4 @@
--- File generated by the BNF Converter (bnfc 2.9.6).
+-- File generated by the BNF Converter (bnfc 2.9.5).
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Lex.x b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Lex.x
index 9dbbbaf5a..1cf92758d 100644
--- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Lex.x
+++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Lex.x
@@ -1,4 +1,4 @@
--- -*- haskell -*- File generated by the BNF Converter (bnfc 2.9.6).
+-- -*- haskell -*- File generated by the BNF Converter (bnfc 2.9.5).
 
 -- Lexer definition for use with Alex 3
 {
@@ -40,7 +40,7 @@ $white+ ;
     { tok (eitherResIdent TV) }
 
 -- token Bytes
-\- \- | [0 1 2 3 4 5 6 7 8 9 A B C D E F][0 1 2 3 4 5 6 7 8 9 A B C D E F]\- | ([0 1 2 3 4 5 6 7 8 9 A B C D E F][0 1 2 3 4 5 6 7 8 9 A B C D E F]\- [0 1 2 3 4 5 6 7 8 9 A B C D E F][0 1 2 3 4 5 6 7 8 9 A B C D E F]) +
+\- \- | [0 1 2 3 4 5 6 7 8 9 A B C D E F][0 1 2 3 4 5 6 7 8 9 A B C D E F](\- [0 1 2 3 4 5 6 7 8 9 A B C D E F][0 1 2 3 4 5 6 7 8 9 A B C D E F]) * (\- \-)
     { tok (eitherResIdent T_Bytes) }
 
 -- token Function
diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Par.y b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Par.y
index 1fba42102..3964497f3 100644
--- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Par.y
+++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Par.y
@@ -1,4 +1,4 @@
--- -*- haskell -*- File generated by the BNF Converter (bnfc 2.9.6).
+-- -*- haskell -*- File generated by the BNF Converter (bnfc 2.9.5).
 
 -- Parser definition for use with Happy
 {
diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Print.hs b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Print.hs
index 85cb8cbbc..30051053e 100644
--- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Print.hs
+++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Print.hs
@@ -1,4 +1,4 @@
--- File generated by the BNF Converter (bnfc 2.9.6).
+-- File generated by the BNF Converter (bnfc 2.9.5).
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE LambdaCase #-}

From fdc66c9eafe5ce518c4ecbda3bc17f48719f56e9 Mon Sep 17 00:00:00 2001
From: Danila Danko <br4ch1st0chr0n3@gmail.com>
Date: Wed, 10 Jan 2024 13:07:56 +0300
Subject: [PATCH 12/23] feat: explain \nu

---
 eo-phi-normalizer/grammar/EO/Phi/Syntax.cf | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/eo-phi-normalizer/grammar/EO/Phi/Syntax.cf b/eo-phi-normalizer/grammar/EO/Phi/Syntax.cf
index 36ce7fb2d..1fdda8502 100644
--- a/eo-phi-normalizer/grammar/EO/Phi/Syntax.cf
+++ b/eo-phi-normalizer/grammar/EO/Phi/Syntax.cf
@@ -27,7 +27,7 @@ separator Binding "," ;
 Phi.    Attribute ::= "φ" ;   -- decoratee object
 Rho.    Attribute ::= "ρ" ;   -- parent object
 Sigma.  Attribute ::= "σ" ;   -- home object
-VTX.    Attribute ::= "ν" ;   -- ???
+VTX.    Attribute ::= "ν" ;   -- an object that represents the unique identifier of the containing object
 Label.  Attribute ::= LabelId ;
 Alpha.  Attribute ::= AlphaIndex ;
 

From 13f019b4142e5c0caf706e2de8a50ac1a6abaebf Mon Sep 17 00:00:00 2001
From: Nikolai Kudasov <nickolay.kudasov@gmail.com>
Date: Thu, 11 Jan 2024 12:20:32 +0300
Subject: [PATCH 13/23] Make test groups objects, not arrays

---
 eo-phi-normalizer/test/Language/EO/PhiSpec.hs | 18 ++++++-----
 eo-phi-normalizer/test/Test/EO/Phi.hs         |  8 ++++-
 eo-phi-normalizer/test/eo/phi/rule-1.yaml     | 30 ++++++++++---------
 eo-phi-normalizer/test/eo/phi/rule-5.yaml     | 16 +++++-----
 4 files changed, 43 insertions(+), 29 deletions(-)

diff --git a/eo-phi-normalizer/test/Language/EO/PhiSpec.hs b/eo-phi-normalizer/test/Language/EO/PhiSpec.hs
index a4b22d891..ecdb925e9 100644
--- a/eo-phi-normalizer/test/Language/EO/PhiSpec.hs
+++ b/eo-phi-normalizer/test/Language/EO/PhiSpec.hs
@@ -12,12 +12,16 @@ import Test.EO.Phi
 
 spec :: Spec
 spec = do
-  tests <- runIO (allPhiTests "test/eo/phi/")
+  testGroups <- runIO (allPhiTests "test/eo/phi/")
   describe "Normalizer" $ do
-    forM_ tests $ mapM_ $ \PhiTest{..} -> do
-      it name $ do
-        Phi.printTree (Phi.normalize input) `shouldBe` Phi.printTree normalized
+    forM_ testGroups $ \PhiTestGroup{..} ->
+      describe title $
+        forM_ tests $ \PhiTest{..} -> do
+          it name $ do
+            Phi.printTree (Phi.normalize input) `shouldBe` Phi.printTree normalized
   describe "Prettify" $ do
-    forM_ tests $ mapM_ $ \PhiTest{..} -> do
-      it name $ do
-        Phi.printTree input `shouldBe` dropWhileEnd isSpace prettified
+    forM_ testGroups $ \PhiTestGroup{..} ->
+      describe title $
+        forM_ tests $ \PhiTest{..} -> do
+          it name $ do
+            Phi.printTree input `shouldBe` dropWhileEnd isSpace prettified
diff --git a/eo-phi-normalizer/test/Test/EO/Phi.hs b/eo-phi-normalizer/test/Test/EO/Phi.hs
index 0f98d1fb2..1f26321bd 100644
--- a/eo-phi-normalizer/test/Test/EO/Phi.hs
+++ b/eo-phi-normalizer/test/Test/EO/Phi.hs
@@ -16,6 +16,12 @@ import Data.List (sort)
 import Language.EO.Phi (unsafeParseProgram)
 import qualified Language.EO.Phi as Phi
 
+data PhiTestGroup = PhiTestGroup
+  { title :: String
+  , tests :: [PhiTest]
+  }
+  deriving (Generic, FromJSON)
+
 data PhiTest = PhiTest
   { name :: String
   , input :: Phi.Program
@@ -24,7 +30,7 @@ data PhiTest = PhiTest
   }
   deriving (Generic, FromJSON)
 
-allPhiTests :: FilePath -> IO [[PhiTest]]
+allPhiTests :: FilePath -> IO [PhiTestGroup]
 allPhiTests dir = do
   paths <- listDirectory dir
   forM (sort paths) $ \path ->
diff --git a/eo-phi-normalizer/test/eo/phi/rule-1.yaml b/eo-phi-normalizer/test/eo/phi/rule-1.yaml
index c37aa8a9c..84d8bc3fd 100644
--- a/eo-phi-normalizer/test/eo/phi/rule-1.yaml
+++ b/eo-phi-normalizer/test/eo/phi/rule-1.yaml
@@ -1,15 +1,17 @@
-- name: 'Program in normal form (1)'
-  input: |
-    {}
-  normalized: |
-    { ν ↦ ⟦ Δ ⤍ 00- ⟧ }
-  prettified: |
-    { }
+title: Tests for Rule 1
+tests:
+  - name: 'Program in normal form (1)'
+    input: |
+      {}
+    normalized: |
+      { ν ↦ ⟦ Δ ⤍ 00- ⟧ }
+    prettified: |
+      { }
 
-- name: 'Program in normal form (2)'
-  input: |
-    { φ ↦ ⟦ φ ↦ ⟦ φ ↦ ⟦ ⟧ ⟧ ⟧ }
-  normalized: |
-    { ν ↦ ⟦ Δ ⤍ 03- ⟧, φ ↦ ⟦ ν ↦ ⟦ Δ ⤍ 02- ⟧, φ ↦ ⟦ ν ↦ ⟦ Δ ⤍ 01- ⟧, φ ↦ ⟦ ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧ ⟧ ⟧ }
-  prettified: |
-    { φ ↦ ⟦ φ ↦ ⟦ φ ↦ ⟦ ⟧ ⟧ ⟧ }
+  - name: 'Program in normal form (2)'
+    input: |
+      { φ ↦ ⟦ φ ↦ ⟦ φ ↦ ⟦ ⟧ ⟧ ⟧ }
+    normalized: |
+      { ν ↦ ⟦ Δ ⤍ 03- ⟧, φ ↦ ⟦ ν ↦ ⟦ Δ ⤍ 02- ⟧, φ ↦ ⟦ ν ↦ ⟦ Δ ⤍ 01- ⟧, φ ↦ ⟦ ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧ ⟧ ⟧ }
+    prettified: |
+      { φ ↦ ⟦ φ ↦ ⟦ φ ↦ ⟦ ⟧ ⟧ ⟧ }
diff --git a/eo-phi-normalizer/test/eo/phi/rule-5.yaml b/eo-phi-normalizer/test/eo/phi/rule-5.yaml
index ab5ee703a..fbb3be13c 100644
--- a/eo-phi-normalizer/test/eo/phi/rule-5.yaml
+++ b/eo-phi-normalizer/test/eo/phi/rule-5.yaml
@@ -1,7 +1,9 @@
-- name: 'Simple static attribute reference'
-  input: |
-    { φ ↦ ⟦ ⟧ , a ↦ ξ.φ }
-  normalized: |
-    { ν ↦ ⟦ Δ ⤍ 01- ⟧, φ ↦ ⟦ ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, a ↦ ξ.φ }
-  prettified: |
-    { φ ↦ ⟦ ⟧, a ↦ ξ.φ }
+title: Tests for Rule 5
+tests:
+  - name: 'Simple static attribute reference'
+    input: |
+      { φ ↦ ⟦ ⟧ , a ↦ ξ.φ }
+    normalized: |
+      { ν ↦ ⟦ Δ ⤍ 01- ⟧, φ ↦ ⟦ ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, a ↦ ξ.φ }
+    prettified: |
+      { φ ↦ ⟦ ⟧, a ↦ ξ.φ }

From ece7fbd89c7c2549d9b46f9c770a078a0ea4db49 Mon Sep 17 00:00:00 2001
From: Nikolai Kudasov <nickolay.kudasov@gmail.com>
Date: Thu, 11 Jan 2024 12:24:27 +0300
Subject: [PATCH 14/23] Update Syntax.cf

---
 eo-phi-normalizer/grammar/EO/Phi/Syntax.cf | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/eo-phi-normalizer/grammar/EO/Phi/Syntax.cf b/eo-phi-normalizer/grammar/EO/Phi/Syntax.cf
index 1fdda8502..27d795e7c 100644
--- a/eo-phi-normalizer/grammar/EO/Phi/Syntax.cf
+++ b/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 ::= "ν" ;   -- an object that represents the unique identifier of the containing object
+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 "" ;

From cb9d91b17a32fdce0d9fd467f010c36ec6d93641 Mon Sep 17 00:00:00 2001
From: Nikolai Kudasov <nickolay.kudasov@gmail.com>
Date: Thu, 11 Jan 2024 14:09:13 +0300
Subject: [PATCH 15/23] Implement applyRules

---
 eo-phi-normalizer/eo-phi-normalizer.cabal     |   2 +
 eo-phi-normalizer/src/Language/EO/Phi.hs      |  83 +-------------
 .../src/Language/EO/Phi/Normalize.hs          |   8 +-
 .../src/Language/EO/Phi/Rules/Common.hs       | 103 ++++++++++++++++++
 .../src/Language/EO/Phi/Syntax.hs             | 100 +++++++++++++++++
 .../src/Language/EO/Phi/Syntax/Doc.txt        |   4 +-
 .../src/Language/EO/Phi/Syntax/Par.y          |   4 +-
 .../src/Language/EO/Phi/Syntax/Print.hs       |   4 +-
 8 files changed, 214 insertions(+), 94 deletions(-)
 create mode 100644 eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs
 create mode 100644 eo-phi-normalizer/src/Language/EO/Phi/Syntax.hs

diff --git a/eo-phi-normalizer/eo-phi-normalizer.cabal b/eo-phi-normalizer/eo-phi-normalizer.cabal
index d7ba18152..dae1d7b14 100644
--- a/eo-phi-normalizer/eo-phi-normalizer.cabal
+++ b/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
diff --git a/eo-phi-normalizer/src/Language/EO/Phi.hs b/eo-phi-normalizer/src/Language/EO/Phi.hs
index b824c217e..9e334fa74 100644
--- a/eo-phi-normalizer/src/Language/EO/Phi.hs
+++ b/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 = ")],;"
diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs b/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs
index 9010d5aee..0f45a0e9f 100644
--- a/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs
+++ b/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs
@@ -13,6 +13,7 @@ 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]
@@ -20,13 +21,6 @@ data Context = Context
   , 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
diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs
new file mode 100644
index 000000000..5f76d51ce
--- /dev/null
+++ b/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
diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Syntax.hs b/eo-phi-normalizer/src/Language/EO/Phi/Syntax.hs
new file mode 100644
index 000000000..1e149913e
--- /dev/null
+++ b/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 = ")],;"
diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Doc.txt b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Doc.txt
index 5bdd30af9..f0d529ab8 100644
--- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Doc.txt
+++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Doc.txt
@@ -73,11 +73,11 @@ All other symbols are terminals.
   |  |  **|**  | //LabelId//
   |  |  **|**  | //AlphaIndex//
   | //PeeledObject// | -> | //ObjectHead// //[ObjectAction]//
-  | //ObjectHead// | -> | ``{`` //[Binding]// ``}``
+  | //ObjectHead// | -> | ``⟦`` //[Binding]// ``⟧``
   |  |  **|**  | ``Φ``
   |  |  **|**  | ``ξ``
   |  |  **|**  | ``⊥``
-  | //ObjectAction// | -> | ``{`` //[Binding]// ``}``
+  | //ObjectAction// | -> | ``(`` //[Binding]// ``)``
   |  |  **|**  | ``.`` //Attribute//
   | //[ObjectAction]// | -> | **eps**
   |  |  **|**  | //ObjectAction// //[ObjectAction]//
diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Par.y b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Par.y
index 3964497f3..b5b530799 100644
--- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Par.y
+++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Par.y
@@ -119,14 +119,14 @@ PeeledObject
 
 ObjectHead :: { Language.EO.Phi.Syntax.Abs.ObjectHead }
 ObjectHead
-  : '{' ListBinding '}' { Language.EO.Phi.Syntax.Abs.HeadFormation $2 }
+  : '⟦' ListBinding '⟧' { Language.EO.Phi.Syntax.Abs.HeadFormation $2 }
   | 'Φ' { Language.EO.Phi.Syntax.Abs.HeadGlobal }
   | 'ξ' { Language.EO.Phi.Syntax.Abs.HeadThis }
   | '⊥' { Language.EO.Phi.Syntax.Abs.HeadTermination }
 
 ObjectAction :: { Language.EO.Phi.Syntax.Abs.ObjectAction }
 ObjectAction
-  : '{' ListBinding '}' { Language.EO.Phi.Syntax.Abs.ActionApplication $2 }
+  : '(' ListBinding ')' { Language.EO.Phi.Syntax.Abs.ActionApplication $2 }
   | '.' Attribute { Language.EO.Phi.Syntax.Abs.ActionDispatch $2 }
 
 ListObjectAction :: { [Language.EO.Phi.Syntax.Abs.ObjectAction] }
diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Print.hs b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Print.hs
index 62bc11297..f232716d3 100644
--- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Print.hs
+++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Print.hs
@@ -185,14 +185,14 @@ instance Print Language.EO.Phi.Syntax.Abs.PeeledObject where
 
 instance Print Language.EO.Phi.Syntax.Abs.ObjectHead where
   prt i = \case
-    Language.EO.Phi.Syntax.Abs.HeadFormation bindings -> prPrec i 0 (concatD [doc (showString "{"), prt 0 bindings, doc (showString "}")])
+    Language.EO.Phi.Syntax.Abs.HeadFormation bindings -> prPrec i 0 (concatD [doc (showString "\10214"), prt 0 bindings, doc (showString "\10215")])
     Language.EO.Phi.Syntax.Abs.HeadGlobal -> prPrec i 0 (concatD [doc (showString "\934")])
     Language.EO.Phi.Syntax.Abs.HeadThis -> prPrec i 0 (concatD [doc (showString "\958")])
     Language.EO.Phi.Syntax.Abs.HeadTermination -> prPrec i 0 (concatD [doc (showString "\8869")])
 
 instance Print Language.EO.Phi.Syntax.Abs.ObjectAction where
   prt i = \case
-    Language.EO.Phi.Syntax.Abs.ActionApplication bindings -> prPrec i 0 (concatD [doc (showString "{"), prt 0 bindings, doc (showString "}")])
+    Language.EO.Phi.Syntax.Abs.ActionApplication bindings -> prPrec i 0 (concatD [doc (showString "("), prt 0 bindings, doc (showString ")")])
     Language.EO.Phi.Syntax.Abs.ActionDispatch attribute -> prPrec i 0 (concatD [doc (showString "."), prt 0 attribute])
 
 instance Print [Language.EO.Phi.Syntax.Abs.ObjectAction] where

From c5d45f59a9c0609fe61053279fb9bd7623c2466f Mon Sep 17 00:00:00 2001
From: Nikolai Kudasov <nickolay.kudasov@gmail.com>
Date: Thu, 11 Jan 2024 23:28:01 +0300
Subject: [PATCH 16/23] Fix imports/exports for the build

---
 eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs | 2 +-
 eo-phi-normalizer/src/Language/EO/Phi/Syntax.hs       | 8 +++++++-
 2 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs
index 5f76d51ce..d4c0a88fc 100644
--- a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs
+++ b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs
@@ -5,10 +5,10 @@ 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
+-- >>> import Language.EO.Phi.Syntax
 
 data Context = Context
   { allRules :: [Rule]
diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Syntax.hs b/eo-phi-normalizer/src/Language/EO/Phi/Syntax.hs
index 1e149913e..5bbec4962 100644
--- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax.hs
+++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax.hs
@@ -1,8 +1,14 @@
 {-# OPTIONS_GHC -Wno-orphans #-}
 {-# LANGUAGE LambdaCase #-}
-module Language.EO.Phi.Syntax where
+module Language.EO.Phi.Syntax (
+  module Language.EO.Phi.Syntax.Abs,
+  parseObject,
+  unsafeParseObject,
+  printTree,
+) where
 
 import Data.Char (isSpace)
+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

From c5bf9c5fe3a9d3c84ea425b922a2785b574c1dc7 Mon Sep 17 00:00:00 2001
From: Danila Danko <br4ch1st0chr0n3@gmail.com>
Date: Fri, 12 Jan 2024 16:58:42 +0300
Subject: [PATCH 17/23] add: string-interpolate package

---
 eo-phi-normalizer/eo-phi-normalizer.cabal | 3 +++
 eo-phi-normalizer/package.yaml            | 1 +
 2 files changed, 4 insertions(+)

diff --git a/eo-phi-normalizer/eo-phi-normalizer.cabal b/eo-phi-normalizer/eo-phi-normalizer.cabal
index dae1d7b14..ca67985ef 100644
--- a/eo-phi-normalizer/eo-phi-normalizer.cabal
+++ b/eo-phi-normalizer/eo-phi-normalizer.cabal
@@ -57,6 +57,7 @@ library
     , directory
     , filepath
     , mtl
+    , string-interpolate
     , yaml
   default-language: Haskell2010
 
@@ -80,6 +81,7 @@ executable normalize-phi
     , eo-phi-normalizer
     , filepath
     , mtl
+    , string-interpolate
     , yaml
   default-language: Haskell2010
 
@@ -108,5 +110,6 @@ test-suite eo-phi-normalizer-test
     , hspec
     , hspec-discover
     , mtl
+    , string-interpolate
     , yaml
   default-language: Haskell2010
diff --git a/eo-phi-normalizer/package.yaml b/eo-phi-normalizer/package.yaml
index da1735273..5828f16e0 100644
--- a/eo-phi-normalizer/package.yaml
+++ b/eo-phi-normalizer/package.yaml
@@ -42,6 +42,7 @@ dependencies:
 - filepath
 - yaml
 - mtl
+- string-interpolate
 
 ghc-options:
 - -Wall

From 2cac3f2ed6a20fe8c50f7f16ad164922d7d9968f Mon Sep 17 00:00:00 2001
From: Danila Danko <br4ch1st0chr0n3@gmail.com>
Date: Fri, 12 Jan 2024 16:50:23 +0300
Subject: [PATCH 18/23] refactor: move rules from phi-paper

---
 .../src/Language/EO/Phi/Rules/Common.hs       | 14 ---------
 .../src/Language/EO/Phi/Rules/PhiPaper.hs     | 29 +++++++++++++++++++
 2 files changed, 29 insertions(+), 14 deletions(-)
 create mode 100644 eo-phi-normalizer/src/Language/EO/Phi/Rules/PhiPaper.hs

diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs
index d4c0a88fc..f47cab9c8 100644
--- a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs
+++ b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs
@@ -78,20 +78,6 @@ applyRulesChain ctx obj
       | 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.
diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Rules/PhiPaper.hs b/eo-phi-normalizer/src/Language/EO/Phi/Rules/PhiPaper.hs
new file mode 100644
index 000000000..84df95f82
--- /dev/null
+++ b/eo-phi-normalizer/src/Language/EO/Phi/Rules/PhiPaper.hs
@@ -0,0 +1,29 @@
+{-# LANGUAGE LambdaCase #-}
+
+module Language.EO.Phi.Rules.PhiPaper where
+
+import Control.Monad (guard)
+import Language.EO.Phi
+import Language.EO.Phi.Rules.Common
+
+-- * Yegor's Rules
+
+-- | Rule 1.
+rule1 :: Rule
+rule1 _ = \case
+    Formation bindings ->
+        let Program bindings' = normalize (Program bindings)
+         in Just (Formation bindings')
+    _ -> Nothing
+
+-- | 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
\ No newline at end of file

From 06cd141c7788187b6a311b35e9ce8c7af4a9523f Mon Sep 17 00:00:00 2001
From: Danila Danko <br4ch1st0chr0n3@gmail.com>
Date: Fri, 12 Jan 2024 16:56:23 +0300
Subject: [PATCH 19/23] upd: tests

---
 eo-phi-normalizer/test/eo/phi/rule-1.yaml | 22 +++++++++++++++-------
 eo-phi-normalizer/test/eo/phi/rule-5.yaml |  9 ---------
 eo-phi-normalizer/test/eo/phi/rule-6.yaml |  9 +++++++++
 3 files changed, 24 insertions(+), 16 deletions(-)
 delete mode 100644 eo-phi-normalizer/test/eo/phi/rule-5.yaml
 create mode 100644 eo-phi-normalizer/test/eo/phi/rule-6.yaml

diff --git a/eo-phi-normalizer/test/eo/phi/rule-1.yaml b/eo-phi-normalizer/test/eo/phi/rule-1.yaml
index 84d8bc3fd..9c001884b 100644
--- a/eo-phi-normalizer/test/eo/phi/rule-1.yaml
+++ b/eo-phi-normalizer/test/eo/phi/rule-1.yaml
@@ -1,17 +1,25 @@
 title: Tests for Rule 1
 tests:
-  - name: 'Program in normal form (1)'
+  - name: 'Program without vertices (1)'
     input: |
-      {}
+      {a ↦ ⟦ ⟧ }
     normalized: |
-      { ν ↦ ⟦ Δ ⤍ 00- ⟧ }
+      { a ↦ ⟦ ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧ }
     prettified: |
       { }
 
-  - name: 'Program in normal form (2)'
+  - name: 'Program without vertices (2)'
     input: |
-      { φ ↦ ⟦ φ ↦ ⟦ φ ↦ ⟦ ⟧ ⟧ ⟧ }
+      { a ↦ ⟦ φ ↦ ⟦ φ ↦ ⟦ φ ↦ ⟦ ⟧ ⟧ ⟧ ⟧ }
     normalized: |
-      { ν ↦ ⟦ Δ ⤍ 03- ⟧, φ ↦ ⟦ ν ↦ ⟦ Δ ⤍ 02- ⟧, φ ↦ ⟦ ν ↦ ⟦ Δ ⤍ 01- ⟧, φ ↦ ⟦ ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧ ⟧ ⟧ }
+      { a ↦ ⟦ ν ↦ ⟦ Δ ⤍ 03- ⟧, φ ↦ ⟦ ν ↦ ⟦ Δ ⤍ 02- ⟧, φ ↦ ⟦ ν ↦ ⟦ Δ ⤍ 01- ⟧, φ ↦ ⟦ ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧ ⟧ ⟧ ⟧ }
     prettified: |
-      { φ ↦ ⟦ φ ↦ ⟦ φ ↦ ⟦ ⟧ ⟧ ⟧ }
+      { a ↦ ⟦ φ ↦ ⟦ φ ↦ ⟦ φ ↦ ⟦ ⟧ ⟧ ⟧ ⟧ }
+
+  - name: 'Program without vertices (3)'
+    input: |
+      { a ↦ ⟦ φ ↦ ⟦ ⟧ , a ↦ ξ.φ ⟧ }
+    normalized: |
+      { a ↦ ⟦ ν ↦ ⟦ Δ ⤍ 01- ⟧, φ ↦ ⟦ ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, a ↦ ξ.φ ⟧ }
+    prettified: |
+      { a ↦ ⟦ φ ↦ ⟦ ⟧, a ↦ ξ.φ ⟧ }
diff --git a/eo-phi-normalizer/test/eo/phi/rule-5.yaml b/eo-phi-normalizer/test/eo/phi/rule-5.yaml
deleted file mode 100644
index fbb3be13c..000000000
--- a/eo-phi-normalizer/test/eo/phi/rule-5.yaml
+++ /dev/null
@@ -1,9 +0,0 @@
-title: Tests for Rule 5
-tests:
-  - name: 'Simple static attribute reference'
-    input: |
-      { φ ↦ ⟦ ⟧ , a ↦ ξ.φ }
-    normalized: |
-      { ν ↦ ⟦ Δ ⤍ 01- ⟧, φ ↦ ⟦ ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, a ↦ ξ.φ }
-    prettified: |
-      { φ ↦ ⟦ ⟧, a ↦ ξ.φ }
diff --git a/eo-phi-normalizer/test/eo/phi/rule-6.yaml b/eo-phi-normalizer/test/eo/phi/rule-6.yaml
new file mode 100644
index 000000000..551f94dea
--- /dev/null
+++ b/eo-phi-normalizer/test/eo/phi/rule-6.yaml
@@ -0,0 +1,9 @@
+title: Tests for Rule 6
+tests:
+  - name: 'Case (1)'
+    input: |
+      { a ↦ ⟦ b ↦ ⟦ Δ ⤍ 00- ⟧, c ↦ ⟦ Δ ⤍ 03- ⟧ ⟧.b }
+    normalized: |
+      { a ↦ ⟦ Δ ⤍ 00- ⟧(ρ ↦ ⟦ c ↦ ⟦ Δ ⤍ 03- ⟧ ⟧) }
+    prettified: |
+      { a ↦ ⟦ b ↦ ⟦ Δ ⤍ 00- ⟧, c ↦ ⟦ Δ ⤍ 03- ⟧ ⟧.b }
\ No newline at end of file

From 655019eec97a66d4f959eb84f0987049661f46a6 Mon Sep 17 00:00:00 2001
From: Danila Danko <br4ch1st0chr0n3@gmail.com>
Date: Fri, 12 Jan 2024 17:00:05 +0300
Subject: [PATCH 20/23] upd: cabal file

---
 eo-phi-normalizer/eo-phi-normalizer.cabal | 1 +
 1 file changed, 1 insertion(+)

diff --git a/eo-phi-normalizer/eo-phi-normalizer.cabal b/eo-phi-normalizer/eo-phi-normalizer.cabal
index ca67985ef..83383349a 100644
--- a/eo-phi-normalizer/eo-phi-normalizer.cabal
+++ b/eo-phi-normalizer/eo-phi-normalizer.cabal
@@ -35,6 +35,7 @@ library
       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

From fcd7bb9c9a05a32d7111f3b5b68a194ef998a1c2 Mon Sep 17 00:00:00 2001
From: Danila Danko <br4ch1st0chr0n3@gmail.com>
Date: Fri, 12 Jan 2024 17:06:10 +0300
Subject: [PATCH 21/23] refactor: code to run rules unit tests

---
 eo-phi-normalizer/test/Language/EO/PhiSpec.hs | 40 +++++++++++--------
 eo-phi-normalizer/test/Test/EO/Phi.hs         |  5 ++-
 2 files changed, 27 insertions(+), 18 deletions(-)

diff --git a/eo-phi-normalizer/test/Language/EO/PhiSpec.hs b/eo-phi-normalizer/test/Language/EO/PhiSpec.hs
index ecdb925e9..df0d3409f 100644
--- a/eo-phi-normalizer/test/Language/EO/PhiSpec.hs
+++ b/eo-phi-normalizer/test/Language/EO/PhiSpec.hs
@@ -1,27 +1,33 @@
+{-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE QuasiQuotes #-}
 {-# LANGUAGE RecordWildCards #-}
 
 module Language.EO.PhiSpec where
 
 import Control.Monad (forM_)
-import Data.Char (isSpace)
-import Data.List (dropWhileEnd)
+import Data.String.Interpolate (i)
+import Language.EO.Phi
+import Language.EO.Phi.Rules.Common (Context (..), Rule)
+import Language.EO.Phi.Rules.PhiPaper (rule1, rule6)
+import Test.EO.Phi
 import Test.Hspec
 
-import qualified Language.EO.Phi as Phi
-import Test.EO.Phi
+applyRule :: (Object -> Maybe Object) -> Program -> Maybe Program
+applyRule rule = \case
+  Program [AlphaBinding name obj] -> do
+    r <- rule obj
+    pure $ Program [AlphaBinding name r]
+  _ -> Nothing
 
 spec :: Spec
 spec = do
-  testGroups <- runIO (allPhiTests "test/eo/phi/")
-  describe "Normalizer" $ do
-    forM_ testGroups $ \PhiTestGroup{..} ->
-      describe title $
-        forM_ tests $ \PhiTest{..} -> do
-          it name $ do
-            Phi.printTree (Phi.normalize input) `shouldBe` Phi.printTree normalized
-  describe "Prettify" $ do
-    forM_ testGroups $ \PhiTestGroup{..} ->
-      describe title $
-        forM_ tests $ \PhiTest{..} -> do
-          it name $ do
-            Phi.printTree input `shouldBe` dropWhileEnd isSpace prettified
+  describe "Rules unit tests"
+    $ forM_ ([(1, rule1), (6, rule6)] :: [(Int, Rule)])
+    $ \(idx, rule) -> do
+      PhiTestGroup{..} <- runIO (filePhiTests [i|test/eo/phi/rule-#{idx}.yaml|])
+      describe title
+        $ forM_ tests
+        $ \PhiTest{..} ->
+          it name do
+            applyRule (rule (Context [])) input `shouldBe` Just normalized
diff --git a/eo-phi-normalizer/test/Test/EO/Phi.hs b/eo-phi-normalizer/test/Test/EO/Phi.hs
index 1f26321bd..b03ecf91c 100644
--- a/eo-phi-normalizer/test/Test/EO/Phi.hs
+++ b/eo-phi-normalizer/test/Test/EO/Phi.hs
@@ -30,11 +30,14 @@ data PhiTest = PhiTest
   }
   deriving (Generic, FromJSON)
 
+filePhiTests :: FilePath -> IO PhiTestGroup
+filePhiTests = Yaml.decodeFileThrow
+
 allPhiTests :: FilePath -> IO [PhiTestGroup]
 allPhiTests dir = do
   paths <- listDirectory dir
   forM (sort paths) $ \path ->
-    Yaml.decodeFileThrow (dir </> path)
+    filePhiTests (dir </> path)
 
 -- * Orphan instances
 

From 8b0ab4ed12826de11f971260ed24df1c71c3b45b Mon Sep 17 00:00:00 2001
From: Danila Danko <br4ch1st0chr0n3@gmail.com>
Date: Fri, 12 Jan 2024 17:20:10 +0300
Subject: [PATCH 22/23] fix: rm redundant input

---
 eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs | 1 -
 1 file changed, 1 deletion(-)

diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs
index f47cab9c8..8fc732797 100644
--- a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs
+++ b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs
@@ -4,7 +4,6 @@ module Language.EO.Phi.Rules.Common where
 
 import Language.EO.Phi.Syntax.Abs
 import Control.Applicative (asum, Alternative ((<|>)))
-import Control.Monad (guard)
 
 -- $setup
 -- >>> :set -XOverloadedStrings

From 2494f118709697930e01e408d68b50aabb4777ec Mon Sep 17 00:00:00 2001
From: Danila Danko <br4ch1st0chr0n3@gmail.com>
Date: Fri, 12 Jan 2024 17:22:43 +0300
Subject: [PATCH 23/23] fix: add -Werror flag to match CI

---
 eo-phi-normalizer/eo-phi-normalizer.cabal | 6 +++---
 eo-phi-normalizer/package.yaml            | 1 +
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/eo-phi-normalizer/eo-phi-normalizer.cabal b/eo-phi-normalizer/eo-phi-normalizer.cabal
index 83383349a..c0583a510 100644
--- a/eo-phi-normalizer/eo-phi-normalizer.cabal
+++ b/eo-phi-normalizer/eo-phi-normalizer.cabal
@@ -45,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
@@ -68,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
@@ -95,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
diff --git a/eo-phi-normalizer/package.yaml b/eo-phi-normalizer/package.yaml
index 5828f16e0..5bbca3dd8 100644
--- a/eo-phi-normalizer/package.yaml
+++ b/eo-phi-normalizer/package.yaml
@@ -55,6 +55,7 @@ ghc-options:
 - -Wpartial-fields
 - -Wredundant-constraints
 - -Wno-missing-export-lists
+- -Werror
 
 library:
   source-dirs: src