From c0050aa3581bd8edaddab6f6548027d3ea2a540e Mon Sep 17 00:00:00 2001
From: Abdelrahman Abounegm <abounegm.abdelrahman@gmail.com>
Date: Wed, 7 Feb 2024 16:36:52 +0300
Subject: [PATCH 01/10] Add descriptions to some rules

---
 eo-phi-normalizer/test/eo/phi/rules/yegor.yaml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/eo-phi-normalizer/test/eo/phi/rules/yegor.yaml b/eo-phi-normalizer/test/eo/phi/rules/yegor.yaml
index c41b0c06a..b2c10a448 100644
--- a/eo-phi-normalizer/test/eo/phi/rules/yegor.yaml
+++ b/eo-phi-normalizer/test/eo/phi/rules/yegor.yaml
@@ -1,7 +1,7 @@
 title: "Rule set based on Yegor's draft"
 rules:
   - name: Rule 3
-    description: ""
+    description: 'Initialization of parent attribute'
     pattern: |
       ⟦ !B ⟧
     result: |
@@ -78,7 +78,7 @@ rules:
     tests: []
 
   - name: Rule 8
-    description: ""
+    description: 'Accessing a decorated object'
     pattern: |
       ⟦ φ ↦ !n, !B ⟧.!a
     result: |
@@ -107,7 +107,7 @@ rules:
     tests: []
 
   - name: Rule 10
-    description: ""
+    description: 'Invalid application'
     pattern: ⟦ !t ↦ !b1, !B1 ⟧(!t ↦ !b2, !B2)
     result: ⊥
     when:
@@ -119,7 +119,7 @@ rules:
         matches: true
 
   - name: Rule 11
-    description: ""
+    description: 'Invalid attribute access'
     pattern: |
       ⟦ !B ⟧.!a
     result: |

From 95dec7b1a6313af949a22862ed62349693a8b4a2 Mon Sep 17 00:00:00 2001
From: Abdelrahman Abounegm <abounegm.abdelrahman@gmail.com>
Date: Wed, 7 Feb 2024 16:55:54 +0300
Subject: [PATCH 02/10] Fix missing argument in doctest

---
 eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs | 4 ++--
 1 file changed, 2 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 f8ee92f1c..b73ddada3 100644
--- a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs
+++ b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs
@@ -13,6 +13,7 @@ import Language.EO.Phi.Syntax.Par
 
 -- $setup
 -- >>> :set -XOverloadedStrings
+-- >>> :set -XOverloadedLists
 -- >>> import Language.EO.Phi.Syntax
 
 instance IsString Program where fromString = unsafeParseWith pProgram
@@ -98,8 +99,7 @@ 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")
--- ⟦ ⟧ (ρ ↦ ⟦ ⟧) (ρ ↦ ⟦ ⟧)
+-- >>> mapM_ (putStrLn . Language.EO.Phi.printTree) (applyRules (Context [rule6] ["⟦ a ↦ ⟦ b ↦ ⟦ ⟧ ⟧.b ⟧"]) "⟦ a ↦ ⟦ b ↦ ⟦ ⟧ ⟧.b ⟧.a")
 applyRules :: Context -> Object -> [Object]
 applyRules ctx obj
   | isNF ctx obj = [obj]

From 56738b7b27480ad4a32f15267bd83b5544ee534b Mon Sep 17 00:00:00 2001
From: Abdelrahman Abounegm <abounegm.abdelrahman@gmail.com>
Date: Thu, 8 Feb 2024 23:51:01 +0300
Subject: [PATCH 03/10] Add syntax support for meta functions

---
 eo-phi-normalizer/grammar/EO/Phi/Syntax.cf    |   2 +
 .../src/Language/EO/Phi/Normalize.hs          |   1 +
 .../src/Language/EO/Phi/Rules/Common.hs       |   1 +
 .../src/Language/EO/Phi/Rules/Yaml.hs         |   1 +
 .../src/Language/EO/Phi/Syntax/Abs.hs         |   4 +
 .../src/Language/EO/Phi/Syntax/Doc.txt        | 202 +++++++++---------
 .../src/Language/EO/Phi/Syntax/Lex.x          |   6 +
 .../src/Language/EO/Phi/Syntax/Par.y          |  55 ++---
 .../src/Language/EO/Phi/Syntax/Print.hs       |   3 +
 9 files changed, 152 insertions(+), 123 deletions(-)

diff --git a/eo-phi-normalizer/grammar/EO/Phi/Syntax.cf b/eo-phi-normalizer/grammar/EO/Phi/Syntax.cf
index 5253ffad3..29d0d171f 100644
--- a/eo-phi-normalizer/grammar/EO/Phi/Syntax.cf
+++ b/eo-phi-normalizer/grammar/EO/Phi/Syntax.cf
@@ -9,6 +9,7 @@ token Function upper (char - [" \r\n\t,.|':;!-?][}{)(⟧⟦"])* ;
 token LabelId  lower (char - [" \r\n\t,.|':;!?][}{)(⟧⟦"])* ;
 token AlphaIndex ({"α0"} | {"α"} (digit - ["0"]) (digit)* ) ;
 token MetaId {"!"} (char - [" \r\n\t,.|':;!-?][}{)(⟧⟦"])* ;
+token MetaFunctionName {"@"} (char - [" \r\n\t,.|':;!-?][}{)(⟧⟦"])* ;
 
 Program. Program ::= "{" [Binding] "}" ;
 
@@ -19,6 +20,7 @@ GlobalObject.   Object ::= "Φ";
 ThisObject.     Object ::= "ξ";
 Termination.    Object ::= "⊥" ;
 MetaObject.     Object ::= MetaId ;
+MetaFunction.   Object ::= MetaFunctionName "(" Object ")" ;
 
 AlphaBinding.   Binding ::= Attribute "↦" Object ;
 EmptyBinding.   Binding ::= Attribute "↦" "∅" ;
diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs b/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs
index 82173e869..afe6d6f6d 100644
--- a/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs
+++ b/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs
@@ -93,6 +93,7 @@ peelObject = \case
   ThisObject -> PeeledObject HeadThis []
   Termination -> PeeledObject HeadTermination []
   MetaObject _ -> PeeledObject HeadTermination []
+  MetaFunction _ _ -> error "To be honest, I'm not sure what should be here"
  where
   followedBy (PeeledObject object actions) action = PeeledObject object (actions ++ [action])
 
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 b73ddada3..0aa0e9ef0 100644
--- a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs
+++ b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs
@@ -74,6 +74,7 @@ withSubObject f ctx root =
       ThisObject{} -> []
       Termination -> []
       MetaObject _ -> []
+      MetaFunction _ _ -> []
 
 withSubObjectBindings :: (Context -> Object -> [Object]) -> Context -> [Binding] -> [[Binding]]
 withSubObjectBindings _ _ [] = []
diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs
index 7437f8d60..6ba862cce 100644
--- a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs
+++ b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs
@@ -108,6 +108,7 @@ objectHasMetavars GlobalObject = False
 objectHasMetavars ThisObject = False
 objectHasMetavars Termination = False
 objectHasMetavars (MetaObject _) = True
+objectHasMetavars (MetaFunction _ _) = True
 
 bindingHasMetavars :: Binding -> Bool
 bindingHasMetavars (AlphaBinding attr obj) = attrHasMetavars attr || objectHasMetavars obj
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 e5d238899..3756fa6d0 100644
--- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Abs.hs
+++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Abs.hs
@@ -26,6 +26,7 @@ data Object
     | ThisObject
     | Termination
     | MetaObject MetaId
+    | MetaFunction MetaFunctionName Object
   deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic)
 
 data Binding
@@ -75,3 +76,6 @@ newtype AlphaIndex = AlphaIndex String
 newtype MetaId = MetaId String
   deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic, Data.String.IsString)
 
+newtype MetaFunctionName = MetaFunctionName String
+  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic, Data.String.IsString)
+
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 cbf58b07a..a80517a82 100644
--- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Doc.txt
+++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Doc.txt
@@ -1,98 +1,104 @@
-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*`````
-
-MetaId literals are recognized by the regular expression
-`````'!' (char - ["
-
 !'(),-.:;?[]{|}⟦⟧"])*`````
-
-
-===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//
-  |  |  **|**  | ``Φ``
-  |  |  **|**  | ``ξ``
-  |  |  **|**  | ``⊥``
-  |  |  **|**  | //MetaId//
-  | //Binding// | -> | //Attribute// ``↦`` //Object//
-  |  |  **|**  | //Attribute// ``↦`` ``∅``
-  |  |  **|**  | ``Δ`` ``⤍`` //Bytes//
-  |  |  **|**  | ``λ`` ``⤍`` //Function//
-  |  |  **|**  | //MetaId//
-  | //[Binding]// | -> | **eps**
-  |  |  **|**  | //Binding//
-  |  |  **|**  | //Binding// ``,`` //[Binding]//
-  | //Attribute// | -> | ``φ``
-  |  |  **|**  | ``ρ``
-  |  |  **|**  | ``σ``
-  |  |  **|**  | ``ν``
-  |  |  **|**  | //LabelId//
-  |  |  **|**  | //AlphaIndex//
-  |  |  **|**  | //MetaId//
-  | //RuleAttribute// | -> | //Attribute//
-  |  |  **|**  | ``Δ``
-  |  |  **|**  | ``λ``
-  | //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*`````
+
+MetaId literals are recognized by the regular expression
+`````'!' (char - ["
+
 !'(),-.:;?[]{|}⟦⟧"])*`````
+
+MetaFunctionName literals are recognized by the regular expression
+`````'@' (char - ["
+
 !'(),-.:;?[]{|}⟦⟧"])*`````
+
+
+===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//
+  |  |  **|**  | ``Φ``
+  |  |  **|**  | ``ξ``
+  |  |  **|**  | ``⊥``
+  |  |  **|**  | //MetaId//
+  |  |  **|**  | //MetaFunctionName// ``(`` //Object// ``)``
+  | //Binding// | -> | //Attribute// ``↦`` //Object//
+  |  |  **|**  | //Attribute// ``↦`` ``∅``
+  |  |  **|**  | ``Δ`` ``⤍`` //Bytes//
+  |  |  **|**  | ``λ`` ``⤍`` //Function//
+  |  |  **|**  | //MetaId//
+  | //[Binding]// | -> | **eps**
+  |  |  **|**  | //Binding//
+  |  |  **|**  | //Binding// ``,`` //[Binding]//
+  | //Attribute// | -> | ``φ``
+  |  |  **|**  | ``ρ``
+  |  |  **|**  | ``σ``
+  |  |  **|**  | ``ν``
+  |  |  **|**  | //LabelId//
+  |  |  **|**  | //AlphaIndex//
+  |  |  **|**  | //MetaId//
+  | //RuleAttribute// | -> | //Attribute//
+  |  |  **|**  | ``Δ``
+  |  |  **|**  | ``λ``
+  | //PeeledObject// | -> | //ObjectHead// //[ObjectAction]//
+  | //ObjectHead// | -> | ``⟦`` //[Binding]// ``⟧``
+  |  |  **|**  | ``Φ``
+  |  |  **|**  | ``ξ``
+  |  |  **|**  | ``⊥``
+  | //ObjectAction// | -> | ``(`` //[Binding]// ``)``
+  |  |  **|**  | ``.`` //Attribute//
+  | //[ObjectAction]// | -> | **eps**
+  |  |  **|**  | //ObjectAction// //[ObjectAction]//
+
+
+
+%% File generated by the BNF Converter (bnfc 2.9.5).
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 bc087772b..44a8ecd8e 100644
--- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Lex.x
+++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Lex.x
@@ -59,6 +59,10 @@ $s [$u # [\t \n \r \  \! \' \( \) \, \. \: \; \? \[ \] \{ \| \} \⟦ \⟧]] *
 \! [$u # [\t \n \r \  \! \' \( \) \, \- \. \: \; \? \[ \] \{ \| \} \⟦ \⟧]] *
     { tok (eitherResIdent T_MetaId) }
 
+-- token MetaFunctionName
+\@ [$u # [\t \n \r \  \! \' \( \) \, \- \. \: \; \? \[ \] \{ \| \} \⟦ \⟧]] *
+    { tok (eitherResIdent T_MetaFunctionName) }
+
 -- Keywords and Ident
 $l $i*
     { tok (eitherResIdent TV) }
@@ -81,6 +85,7 @@ data Tok
   | T_LabelId !String
   | T_AlphaIndex !String
   | T_MetaId !String
+  | T_MetaFunctionName !String
   deriving (Eq, Show, Ord)
 
 -- | Smart constructor for 'Tok' for the sake of backwards compatibility.
@@ -148,6 +153,7 @@ tokenText t = case t of
   PT _ (T_LabelId s) -> s
   PT _ (T_AlphaIndex s) -> s
   PT _ (T_MetaId s) -> s
+  PT _ (T_MetaFunctionName s) -> s
 
 -- | Convert a token to a string.
 prToken :: Token -> String
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 73f3876bc..4deb4ab03 100644
--- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Par.y
+++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Par.y
@@ -41,31 +41,32 @@ import Language.EO.Phi.Syntax.Lex
 %monad { Err } { (>>=) } { return }
 %tokentype {Token}
 %token
-  '('          { PT _ (TS _ 1)          }
-  ')'          { PT _ (TS _ 2)          }
-  ','          { PT _ (TS _ 3)          }
-  '.'          { PT _ (TS _ 4)          }
-  '{'          { PT _ (TS _ 5)          }
-  '}'          { PT _ (TS _ 6)          }
-  'Δ'          { PT _ (TS _ 7)          }
-  'Φ'          { PT _ (TS _ 8)          }
-  'λ'          { PT _ (TS _ 9)          }
-  'ν'          { PT _ (TS _ 10)         }
-  'ξ'          { PT _ (TS _ 11)         }
-  'ρ'          { PT _ (TS _ 12)         }
-  'σ'          { PT _ (TS _ 13)         }
-  'φ'          { PT _ (TS _ 14)         }
-  '↦'          { PT _ (TS _ 15)         }
-  '∅'          { PT _ (TS _ 16)         }
-  '⊥'          { PT _ (TS _ 17)         }
-  '⟦'          { PT _ (TS _ 18)         }
-  '⟧'          { PT _ (TS _ 19)         }
-  '⤍'          { PT _ (TS _ 20)         }
-  L_Bytes      { PT _ (T_Bytes $$)      }
-  L_Function   { PT _ (T_Function $$)   }
-  L_LabelId    { PT _ (T_LabelId $$)    }
-  L_AlphaIndex { PT _ (T_AlphaIndex $$) }
-  L_MetaId     { PT _ (T_MetaId $$)     }
+  '('                { PT _ (TS _ 1)                }
+  ')'                { PT _ (TS _ 2)                }
+  ','                { PT _ (TS _ 3)                }
+  '.'                { PT _ (TS _ 4)                }
+  '{'                { PT _ (TS _ 5)                }
+  '}'                { PT _ (TS _ 6)                }
+  'Δ'                { PT _ (TS _ 7)                }
+  'Φ'                { PT _ (TS _ 8)                }
+  'λ'                { PT _ (TS _ 9)                }
+  'ν'                { PT _ (TS _ 10)               }
+  'ξ'                { PT _ (TS _ 11)               }
+  'ρ'                { PT _ (TS _ 12)               }
+  'σ'                { PT _ (TS _ 13)               }
+  'φ'                { PT _ (TS _ 14)               }
+  '↦'                { PT _ (TS _ 15)               }
+  '∅'                { PT _ (TS _ 16)               }
+  '⊥'                { PT _ (TS _ 17)               }
+  '⟦'                { PT _ (TS _ 18)               }
+  '⟧'                { PT _ (TS _ 19)               }
+  '⤍'                { PT _ (TS _ 20)               }
+  L_Bytes            { PT _ (T_Bytes $$)            }
+  L_Function         { PT _ (T_Function $$)         }
+  L_LabelId          { PT _ (T_LabelId $$)          }
+  L_AlphaIndex       { PT _ (T_AlphaIndex $$)       }
+  L_MetaId           { PT _ (T_MetaId $$)           }
+  L_MetaFunctionName { PT _ (T_MetaFunctionName $$) }
 
 %%
 
@@ -84,6 +85,9 @@ AlphaIndex  : L_AlphaIndex { Language.EO.Phi.Syntax.Abs.AlphaIndex $1 }
 MetaId :: { Language.EO.Phi.Syntax.Abs.MetaId }
 MetaId  : L_MetaId { Language.EO.Phi.Syntax.Abs.MetaId $1 }
 
+MetaFunctionName :: { Language.EO.Phi.Syntax.Abs.MetaFunctionName }
+MetaFunctionName  : L_MetaFunctionName { Language.EO.Phi.Syntax.Abs.MetaFunctionName $1 }
+
 Program :: { Language.EO.Phi.Syntax.Abs.Program }
 Program
   : '{' ListBinding '}' { Language.EO.Phi.Syntax.Abs.Program $2 }
@@ -97,6 +101,7 @@ Object
   | 'ξ' { Language.EO.Phi.Syntax.Abs.ThisObject }
   | '⊥' { Language.EO.Phi.Syntax.Abs.Termination }
   | MetaId { Language.EO.Phi.Syntax.Abs.MetaObject $1 }
+  | MetaFunctionName '(' Object ')' { Language.EO.Phi.Syntax.Abs.MetaFunction $1 $3 }
 
 Binding :: { Language.EO.Phi.Syntax.Abs.Binding }
 Binding
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 0a781b042..cef0892d5 100644
--- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Print.hs
+++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Print.hs
@@ -147,6 +147,8 @@ instance Print Language.EO.Phi.Syntax.Abs.AlphaIndex where
   prt _ (Language.EO.Phi.Syntax.Abs.AlphaIndex i) = doc $ showString i
 instance Print Language.EO.Phi.Syntax.Abs.MetaId where
   prt _ (Language.EO.Phi.Syntax.Abs.MetaId i) = doc $ showString i
+instance Print Language.EO.Phi.Syntax.Abs.MetaFunctionName where
+  prt _ (Language.EO.Phi.Syntax.Abs.MetaFunctionName i) = doc $ showString i
 instance Print Language.EO.Phi.Syntax.Abs.Program where
   prt i = \case
     Language.EO.Phi.Syntax.Abs.Program bindings -> prPrec i 0 (concatD [doc (showString "{"), prt 0 bindings, doc (showString "}")])
@@ -160,6 +162,7 @@ instance Print Language.EO.Phi.Syntax.Abs.Object where
     Language.EO.Phi.Syntax.Abs.ThisObject -> prPrec i 0 (concatD [doc (showString "\958")])
     Language.EO.Phi.Syntax.Abs.Termination -> prPrec i 0 (concatD [doc (showString "\8869")])
     Language.EO.Phi.Syntax.Abs.MetaObject metaid -> prPrec i 0 (concatD [prt 0 metaid])
+    Language.EO.Phi.Syntax.Abs.MetaFunction metafunctionname object -> prPrec i 0 (concatD [prt 0 metafunctionname, doc (showString "("), prt 0 object, doc (showString ")")])
 
 instance Print Language.EO.Phi.Syntax.Abs.Binding where
   prt i = \case

From a3acf39773fa338d4434fb1e19684f10eaab2b57 Mon Sep 17 00:00:00 2001
From: Abdelrahman Abounegm <abounegm.abdelrahman@gmail.com>
Date: Thu, 8 Feb 2024 23:52:04 +0300
Subject: [PATCH 04/10] Move nu counting functions to Common

in preparation for reusing them in the Yaml rules
---
 .../src/Language/EO/Phi/Normalize.hs          | 23 ++-----------
 .../src/Language/EO/Phi/Rules/Common.hs       | 32 +++++++++++++++++++
 2 files changed, 35 insertions(+), 20 deletions(-)

diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs b/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs
index afe6d6f6d..a5250bbf2 100644
--- a/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs
+++ b/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs
@@ -9,10 +9,9 @@ module Language.EO.Phi.Normalize (
 
 import Control.Monad.State
 import Data.Maybe (fromMaybe)
-import Numeric (showHex)
 
 import Control.Monad (forM)
-import Language.EO.Phi.Rules.Common (lookupBinding)
+import Language.EO.Phi.Rules.Common (intToBytesObject, lookupBinding, nuCount, objectBindings)
 import Language.EO.Phi.Syntax.Abs
 
 data Context = Context
@@ -34,14 +33,8 @@ normalize (Program bindings) = evalState (Program . objectBindings <$> normalize
     Context
       { globalObject = bindings
       , thisObject = bindings
-      , totalNuCount = nuCount bindings
+      , totalNuCount = nuCount (Formation 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 _ = []
 
 rule1 :: Object -> State Context Object
 rule1 (Formation bindings) = do
@@ -57,17 +50,7 @@ rule1 (Formation bindings) = do
       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 ""]
+        let dataObject = intToBytesObject nus
         pure (AlphaBinding VTX dataObject : normalizedBindings)
       else do
         pure normalizedBindings
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 0aa0e9ef0..437e983c3 100644
--- a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs
+++ b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs
@@ -10,6 +10,7 @@ import Data.String (IsString (..))
 import Language.EO.Phi.Syntax.Abs
 import Language.EO.Phi.Syntax.Lex (Token)
 import Language.EO.Phi.Syntax.Par
+import Numeric (showHex)
 
 -- $setup
 -- >>> :set -XOverloadedStrings
@@ -128,3 +129,34 @@ lookupBinding a (AlphaBinding a' object : bindings)
   | a == a' = Just object
   | otherwise = lookupBinding a bindings
 lookupBinding _ _ = Nothing
+
+objectBindings :: Object -> [Binding]
+objectBindings (Formation bs) = bs
+objectBindings _ = []
+
+nuCount :: Object -> Int
+nuCount obj = count isNu (objectBindings obj) + sum (map (sum . map nuCount . values) (objectBindings obj))
+ where
+  isNu (AlphaBinding VTX _) = True
+  isNu (EmptyBinding VTX) = True
+  isNu _ = False
+  count = (length .) . filter
+  values (AlphaBinding _ obj') = [obj']
+  values _ = []
+
+intToBytesObject :: Int -> Object
+intToBytesObject n = Formation [DeltaBinding $ Bytes $ insertDashes $ pad $ showHex n ""]
+ where
+  pad s = (if even (length s) then "" else "0") ++ s
+  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
+
+nuCountAsDataObj :: Object -> Object
+nuCountAsDataObj = intToBytesObject . nuCount

From c0e5ecc6c30819bdde69233824428f59545f849b Mon Sep 17 00:00:00 2001
From: Abdelrahman Abounegm <abounegm.abdelrahman@gmail.com>
Date: Thu, 8 Feb 2024 23:53:09 +0300
Subject: [PATCH 05/10] Implement substitution for meta function

---
 eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs
index 6ba862cce..bf73d2f33 100644
--- a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs
+++ b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs
@@ -173,6 +173,7 @@ data Subst = Subst
   { objectMetas :: [(MetaId, Object)]
   , bindingsMetas :: [(MetaId, [Binding])]
   , attributeMetas :: [(MetaId, Attribute)]
+  , functionMetas :: [(MetaFunctionName, Object)]
   }
   deriving (Show)
 
@@ -183,7 +184,7 @@ instance Monoid Subst where
   mempty = emptySubst
 
 emptySubst :: Subst
-emptySubst = Subst [] [] []
+emptySubst = Subst [] [] [] []
 
 -- >>> putStrLn $ Language.EO.Phi.printTree (applySubst (Subst [("!n", "⟦ c ↦ ⟦ ⟧ ⟧")] [("!B", ["b ↦ ⟦ ⟧"])] [("!a", "a")]) "!n(ρ ↦ ⟦ !B ⟧)" :: Object)
 -- ⟦ c ↦ ⟦ ⟧ ⟧ (ρ ↦ ⟦ b ↦ ⟦ ⟧ ⟧)
@@ -198,6 +199,7 @@ applySubst subst@Subst{..} = \case
   GlobalObject -> GlobalObject
   ThisObject -> ThisObject
   obj@(MetaObject x) -> fromMaybe obj $ lookup x objectMetas
+  obj@(MetaFunction name _) -> fromMaybe obj $ lookup name functionMetas
   obj -> obj
 
 applySubstAttr :: Subst -> Attribute -> Attribute
@@ -219,8 +221,8 @@ applySubstBinding subst@Subst{..} = \case
   b@(MetaBindings m) -> fromMaybe [b] (lookup m bindingsMetas)
 
 mergeSubst :: Subst -> Subst -> Subst
-mergeSubst (Subst xs ys zs) (Subst xs' ys' zs') =
-  Subst (xs ++ xs') (ys ++ ys') (zs ++ zs')
+mergeSubst (Subst xs ys zs fs) (Subst xs' ys' zs' fs') =
+  Subst (xs ++ xs') (ys ++ ys') (zs ++ zs') (fs ++ fs')
 
 -- 1. need to implement applySubst' :: Subst -> Object -> Object
 -- 2. complete the code
@@ -240,7 +242,9 @@ matchObject (MetaObject m) obj =
       { objectMetas = [(m, obj)]
       , bindingsMetas = []
       , attributeMetas = []
+      , functionMetas = []
       }
+matchObject (MetaFunction name@(MetaFunctionName "@T") obj) _ = [Subst [] [] [] [(name, Common.nuCountAsDataObj obj)]]
 matchObject _ _ = [] -- ? emptySubst ?
 
 matchBindings :: [Binding] -> [Binding] -> [Subst]
@@ -251,6 +255,7 @@ matchBindings [MetaBindings b] bindings =
       { objectMetas = []
       , bindingsMetas = [(b, bindings)]
       , attributeMetas = []
+      , functionMetas = []
       }
 matchBindings (p : ps) bs = do
   (bs', subst1) <- matchFindBinding p bs
@@ -291,6 +296,7 @@ matchAttr (MetaAttr metaId) attr =
       { objectMetas = []
       , bindingsMetas = []
       , attributeMetas = [(metaId, attr)]
+      , functionMetas = []
       }
   ]
 matchAttr _ _ = []

From 10cda89a47050b607337497462e66fb60afd4ef9 Mon Sep 17 00:00:00 2001
From: Abdelrahman Abounegm <abounegm.abdelrahman@gmail.com>
Date: Thu, 8 Feb 2024 23:53:28 +0300
Subject: [PATCH 06/10] Add rule 1 as a user-defined rule

---
 eo-phi-normalizer/test/eo/phi/rules/yegor.yaml | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/eo-phi-normalizer/test/eo/phi/rules/yegor.yaml b/eo-phi-normalizer/test/eo/phi/rules/yegor.yaml
index b2c10a448..2c3e595a3 100644
--- a/eo-phi-normalizer/test/eo/phi/rules/yegor.yaml
+++ b/eo-phi-normalizer/test/eo/phi/rules/yegor.yaml
@@ -1,5 +1,22 @@
 title: "Rule set based on Yegor's draft"
 rules:
+  - name: Rule 1
+    description: 'Initialization of vertex attribute'
+    pattern: |
+      ⟦ !a ↦ ⟦ !B ⟧, !B_rest ⟧
+    result: |
+      ⟦ !a ↦ ⟦ !B, ν ↦ @T(Φ) ⟧, !B_rest ⟧
+    when:
+      - absent_attrs:
+          attrs: ['ν']
+          bindings: ['!B']
+      - not_equal: ['!a', 'ν']
+    tests:
+      - name: Adds vertex attribute
+        input: '⟦ a ↦ ⟦ ⟧ ⟧'
+        output: '⟦ a ↦ ⟦ ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧ ⟧'
+        matches: true
+
   - name: Rule 3
     description: 'Initialization of parent attribute'
     pattern: |

From 5028df76db7cd7bf83be652c7df2ffe655eb5b8a Mon Sep 17 00:00:00 2001
From: Abdelrahman Abounegm <abounegm.abdelrahman@gmail.com>
Date: Fri, 9 Feb 2024 15:02:11 +0300
Subject: [PATCH 07/10] Add a function for evaluating meta functions

It couldn't be done in `matchObject` because we don't match on results,
only on patterns.
---
 .../src/Language/EO/Phi/Rules/Yaml.hs             | 15 ++++++++++++---
 1 file changed, 12 insertions(+), 3 deletions(-)

diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs
index bf73d2f33..24de9767d 100644
--- a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs
+++ b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs
@@ -86,7 +86,7 @@ convertRule Rule{..} ctx obj =
   , let result' = applySubst contextSubsts result
   , subst <- matchObject pattern' obj
   , all (\cond -> checkCond ctx cond subst) when
-  , obj' <- [applySubst subst result']
+  , obj' <- [applySubst subst (evaluateMetaFuncs result')]
   , not (objectHasMetavars obj')
   ]
 
@@ -199,7 +199,6 @@ applySubst subst@Subst{..} = \case
   GlobalObject -> GlobalObject
   ThisObject -> ThisObject
   obj@(MetaObject x) -> fromMaybe obj $ lookup x objectMetas
-  obj@(MetaFunction name _) -> fromMaybe obj $ lookup name functionMetas
   obj -> obj
 
 applySubstAttr :: Subst -> Attribute -> Attribute
@@ -244,9 +243,19 @@ matchObject (MetaObject m) obj =
       , attributeMetas = []
       , functionMetas = []
       }
-matchObject (MetaFunction name@(MetaFunctionName "@T") obj) _ = [Subst [] [] [] [(name, Common.nuCountAsDataObj obj)]]
 matchObject _ _ = [] -- ? emptySubst ?
 
+evaluateMetaFuncs :: Object -> Object
+evaluateMetaFuncs (MetaFunction (MetaFunctionName "@T") obj) = Common.nuCountAsDataObj obj
+evaluateMetaFuncs (Formation bindings) = Formation (map evaluateMetaFuncsBinding bindings)
+evaluateMetaFuncs (Application obj bindings) = Application (evaluateMetaFuncs obj) (map evaluateMetaFuncsBinding bindings)
+evaluateMetaFuncs (ObjectDispatch obj a) = ObjectDispatch (evaluateMetaFuncs obj) a
+evaluateMetaFuncs obj = obj
+
+evaluateMetaFuncsBinding :: Binding -> Binding
+evaluateMetaFuncsBinding (AlphaBinding attr obj) = AlphaBinding attr (evaluateMetaFuncs obj)
+evaluateMetaFuncsBinding binding = binding
+
 matchBindings :: [Binding] -> [Binding] -> [Subst]
 matchBindings [] [] = [emptySubst]
 matchBindings [MetaBindings b] bindings =

From bb970e57ecbc9fbd5078b3bb378ab5e58547b2af Mon Sep 17 00:00:00 2001
From: Abdelrahman Abounegm <abounegm.abdelrahman@gmail.com>
Date: Fri, 9 Feb 2024 15:03:29 +0300
Subject: [PATCH 08/10] =?UTF-8?q?Fix=20the=20first=20rule=20by=20defining?=
 =?UTF-8?q?=20=CE=A6=20in=20rule=20context?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 eo-phi-normalizer/test/eo/phi/rules/yegor.yaml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/eo-phi-normalizer/test/eo/phi/rules/yegor.yaml b/eo-phi-normalizer/test/eo/phi/rules/yegor.yaml
index 2c3e595a3..02485a76c 100644
--- a/eo-phi-normalizer/test/eo/phi/rules/yegor.yaml
+++ b/eo-phi-normalizer/test/eo/phi/rules/yegor.yaml
@@ -2,10 +2,12 @@ title: "Rule set based on Yegor's draft"
 rules:
   - name: Rule 1
     description: 'Initialization of vertex attribute'
+    context:
+      global_object: '!Phi'
     pattern: |
       ⟦ !a ↦ ⟦ !B ⟧, !B_rest ⟧
     result: |
-      ⟦ !a ↦ ⟦ !B, ν ↦ @T(Φ) ⟧, !B_rest ⟧
+      ⟦ !a ↦ ⟦ !B, ν ↦ @T(!Phi) ⟧, !B_rest ⟧
     when:
       - absent_attrs:
           attrs: ['ν']

From 9fe8c05d683cc58179c41cba98be6c072cbab55b Mon Sep 17 00:00:00 2001
From: Abdelrahman Abounegm <abounegm.abdelrahman@gmail.com>
Date: Fri, 9 Feb 2024 15:06:46 +0300
Subject: [PATCH 09/10] Remove the redundant field of Subst

I previously thought it's needed, but turns out not
---
 eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs | 10 +++-------
 1 file changed, 3 insertions(+), 7 deletions(-)

diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs
index 24de9767d..196c5a7cf 100644
--- a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs
+++ b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs
@@ -173,7 +173,6 @@ data Subst = Subst
   { objectMetas :: [(MetaId, Object)]
   , bindingsMetas :: [(MetaId, [Binding])]
   , attributeMetas :: [(MetaId, Attribute)]
-  , functionMetas :: [(MetaFunctionName, Object)]
   }
   deriving (Show)
 
@@ -184,7 +183,7 @@ instance Monoid Subst where
   mempty = emptySubst
 
 emptySubst :: Subst
-emptySubst = Subst [] [] [] []
+emptySubst = Subst [] [] []
 
 -- >>> putStrLn $ Language.EO.Phi.printTree (applySubst (Subst [("!n", "⟦ c ↦ ⟦ ⟧ ⟧")] [("!B", ["b ↦ ⟦ ⟧"])] [("!a", "a")]) "!n(ρ ↦ ⟦ !B ⟧)" :: Object)
 -- ⟦ c ↦ ⟦ ⟧ ⟧ (ρ ↦ ⟦ b ↦ ⟦ ⟧ ⟧)
@@ -220,8 +219,8 @@ applySubstBinding subst@Subst{..} = \case
   b@(MetaBindings m) -> fromMaybe [b] (lookup m bindingsMetas)
 
 mergeSubst :: Subst -> Subst -> Subst
-mergeSubst (Subst xs ys zs fs) (Subst xs' ys' zs' fs') =
-  Subst (xs ++ xs') (ys ++ ys') (zs ++ zs') (fs ++ fs')
+mergeSubst (Subst xs ys zs) (Subst xs' ys' zs') =
+  Subst (xs ++ xs') (ys ++ ys') (zs ++ zs')
 
 -- 1. need to implement applySubst' :: Subst -> Object -> Object
 -- 2. complete the code
@@ -241,7 +240,6 @@ matchObject (MetaObject m) obj =
       { objectMetas = [(m, obj)]
       , bindingsMetas = []
       , attributeMetas = []
-      , functionMetas = []
       }
 matchObject _ _ = [] -- ? emptySubst ?
 
@@ -264,7 +262,6 @@ matchBindings [MetaBindings b] bindings =
       { objectMetas = []
       , bindingsMetas = [(b, bindings)]
       , attributeMetas = []
-      , functionMetas = []
       }
 matchBindings (p : ps) bs = do
   (bs', subst1) <- matchFindBinding p bs
@@ -305,7 +302,6 @@ matchAttr (MetaAttr metaId) attr =
       { objectMetas = []
       , bindingsMetas = []
       , attributeMetas = [(metaId, attr)]
-      , functionMetas = []
       }
   ]
 matchAttr _ _ = []

From 24f74ef9930b7303ea03beae47d8e0d891bc32aa Mon Sep 17 00:00:00 2001
From: Abdelrahman Abounegm <abounegm.abdelrahman@gmail.com>
Date: Sun, 11 Feb 2024 18:20:24 +0300
Subject: [PATCH 10/10] Count vertex indices in applications and dispatch

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

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 437e983c3..9d0c22bc7 100644
--- a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs
+++ b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs
@@ -132,6 +132,8 @@ lookupBinding _ _ = Nothing
 
 objectBindings :: Object -> [Binding]
 objectBindings (Formation bs) = bs
+objectBindings (Application obj bs) = objectBindings obj ++ bs
+objectBindings (ObjectDispatch obj _attr) = objectBindings obj
 objectBindings _ = []
 
 nuCount :: Object -> Int