diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -8,6 +8,20 @@
 
 ## Unreleased
 
+## 0.2.0 — 2024-02-16
+
+- Complete implementation of Yegor's rules (see [#109](https://github.com/objectionary/normalizer/pull/109), [#112](https://github.com/objectionary/normalizer/pull/112))
+  - Support global counter in user-defined rules (see [#105](https://github.com/objectionary/normalizer/pull/105))
+  - Context matching (global object and this object, see [#99](https://github.com/objectionary/normalizer/pull/99))
+- Fix grammar for $\varphi$-calculus (see [#97](https://github.com/objectionary/normalizer/pull/97) and [#127](https://github.com/objectionary/normalizer/pull/127))
+- Improve documentation:
+  - Set up wesbite for documentation (see [#104](https://github.com/objectionary/normalizer/pull/104), [#124](https://github.com/objectionary/normalizer/pull/124), and [#128](https://github.com/objectionary/normalizer/pull/128))
+  - Update CLI documentation (see [#113](https://github.com/objectionary/normalizer/pull/113))
+- Improve command line interface:
+  - Support `--output`/`-o` command line option (see [#92](https://github.com/objectionary/normalizer/pull/92))
+  - Remove logs from default output (see [#106](https://github.com/objectionary/normalizer/pull/106))
+- Allow collection of metrics for $\varphi$-terms (see [#121](https://github.com/objectionary/normalizer/pull/121))
+
 ## 0.1.0 - 2024-02-02
 
 First version of the normalizer.
diff --git a/app/Main.hs b/app/Main.hs
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -1,6 +1,6 @@
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE DeriveGeneric #-}
-{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE OverloadedLists #-}
 {-# LANGUAGE OverloadedRecordDot #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE RecordWildCards #-}
@@ -8,19 +8,21 @@
 
 module Main where
 
-import Control.Monad (when)
+import Control.Monad (unless, when)
 import Data.Foldable (forM_)
 
 import Data.List (nub)
 import Language.EO.Phi (Object (Formation), Program (Program), defaultMain, parseProgram, printTree)
 import Language.EO.Phi.Rules.Common (Context (..), applyRules, applyRulesChain)
-import Language.EO.Phi.Rules.Yaml
+import Language.EO.Phi.Rules.Yaml (RuleSet (rules, title), convertRule, parseRuleSetFromFile)
 import Options.Generic
+import System.IO (IOMode (WriteMode), hClose, hPutStr, hPutStrLn, openFile, stdout)
 
 data CLINamedParams = CLINamedParams
   { chain :: Bool
   , rulesYaml :: Maybe String
   , outPath :: Maybe String
+  , single :: Bool
   }
   deriving (Generic, Show, ParseRecord, Read, ParseField)
 
@@ -30,6 +32,7 @@
       <$> parseFields (Just "Print out steps of reduction") (Just "chain") (Just 'c') Nothing
       <*> parseFields (Just "Path to the Yaml file with custom rules") (Just "rules-yaml") Nothing Nothing
       <*> parseFields (Just "Output file path (defaults to stdout)") (Just "output") (Just 'o') Nothing
+      <*> parseFields (Just "Print a single normlized expression") (Just "single") (Just 's') Nothing
 
 data CLIOptions = CLIOptions CLINamedParams (Maybe FilePath)
   deriving (Generic, Show, ParseRecord)
@@ -41,30 +44,37 @@
   let (CLINamedParams{..}) = params
   case rulesYaml of
     Just path -> do
+      handle <- maybe (pure stdout) (`openFile` WriteMode) outPath
+      let logStr = hPutStr handle
+      let logStrLn = hPutStrLn handle
       ruleSet <- parseRuleSetFromFile path
-      putStrLn ruleSet.title
+      unless single $ logStrLn ruleSet.title
       src <- maybe getContents readFile inPath
       let progOrError = parseProgram src
       case progOrError of
         Left err -> error ("An error occurred parsing the input program: " <> err)
         Right input@(Program bindings) -> do
           let results
-                | chain = applyRulesChain (Context (convertRule <$> ruleSet.rules)) (Formation bindings)
-                | otherwise = pure <$> applyRules (Context (convertRule <$> ruleSet.rules)) (Formation bindings)
+                | chain = applyRulesChain (Context (convertRule <$> ruleSet.rules) [Formation bindings]) (Formation bindings)
+                | otherwise = pure <$> applyRules (Context (convertRule <$> ruleSet.rules) [Formation bindings]) (Formation bindings)
               uniqueResults = nub results
               totalResults = length uniqueResults
-          -- TODO #48:15m use outPath to output to file if provided
-          putStrLn "Input:"
-          putStrLn (printTree input)
-          putStrLn "===================================================="
-          forM_ (zip [1 ..] uniqueResults) $ \(i, steps) -> do
-            putStrLn $
-              "Result " <> show i <> " out of " <> show totalResults <> ":"
-            let n = length steps
-            forM_ (zip [1 ..] steps) $ \(k, step) -> do
-              Control.Monad.when chain $ do
-                putStr ("[ " <> show k <> " / " <> show n <> " ]")
-              putStrLn (printTree step)
-            putStrLn "----------------------------------------------------"
+          when (totalResults == 0) $ error "Could not normalize the program"
+          if single
+            then logStrLn (printTree (head uniqueResults))
+            else do
+              logStrLn "Input:"
+              logStrLn (printTree input)
+              logStrLn "===================================================="
+              forM_ (zip [1 ..] uniqueResults) $ \(i, steps) -> do
+                logStrLn $
+                  "Result " <> show i <> " out of " <> show totalResults <> ":"
+                let n = length steps
+                forM_ (zip [1 ..] steps) $ \(k, step) -> do
+                  when chain $
+                    logStr ("[ " <> show k <> " / " <> show n <> " ]")
+                  logStrLn (printTree step)
+                logStrLn "----------------------------------------------------"
+      hClose handle
     -- TODO #48:15m still need to consider `chain` (should rewrite/change defaultMain to mainWithOptions)
     Nothing -> defaultMain
diff --git a/eo-phi-normalizer.cabal b/eo-phi-normalizer.cabal
--- a/eo-phi-normalizer.cabal
+++ b/eo-phi-normalizer.cabal
@@ -5,7 +5,7 @@
 -- see: https://github.com/sol/hpack
 
 name:           eo-phi-normalizer
-version:        0.1.0
+version:        0.2.0
 synopsis:       Command line normalizer of 𝜑-calculus expressions.
 description:    Please see the README on GitHub at <https://github.com/objectionary/eo-phi-normalizer#readme>
 homepage:       https://github.com/objectionary/eo-phi-normalizer#readme
@@ -34,6 +34,7 @@
 library
   exposed-modules:
       Language.EO.Phi
+      Language.EO.Phi.Metrics.Collect
       Language.EO.Phi.Normalize
       Language.EO.Phi.Rules.Common
       Language.EO.Phi.Rules.PhiPaper
@@ -61,6 +62,8 @@
     , base >=4.7 && <5
     , directory
     , filepath
+    , generic-lens
+    , lens
     , mtl
     , string-interpolate
     , yaml
@@ -87,6 +90,8 @@
     , directory
     , eo-phi-normalizer
     , filepath
+    , generic-lens
+    , lens
     , mtl
     , optparse-generic
     , string-interpolate
@@ -101,6 +106,7 @@
       Language.EO.YamlSpec
       Test.EO.Phi
       Test.EO.Yaml
+      Test.Metrics.Phi
       Paths_eo_phi_normalizer
   hs-source-dirs:
       test
@@ -119,8 +125,10 @@
     , directory
     , eo-phi-normalizer
     , filepath
+    , generic-lens
     , hspec
     , hspec-discover
+    , lens
     , mtl
     , string-interpolate
     , yaml
diff --git a/grammar/EO/Phi/Syntax.cf b/grammar/EO/Phi/Syntax.cf
--- a/grammar/EO/Phi/Syntax.cf
+++ b/grammar/EO/Phi/Syntax.cf
@@ -6,19 +6,21 @@
 
 token Bytes ({"--"} | ["0123456789ABCDEF"] ["0123456789ABCDEF"] {"-"} | ["0123456789ABCDEF"] ["0123456789ABCDEF"] ({"-"} ["0123456789ABCDEF"] ["0123456789ABCDEF"])+) ;
 token Function upper (char - [" \r\n\t,.|':;!-?][}{)(⟧⟦"])* ;
-token LabelId  lower (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] "}" ;
+Program. Program ::= "{" "⟦" [Binding] "⟧" "}" ;
 
 Formation.      Object ::= "⟦" [Binding] "⟧" ;
 Application.    Object ::= Object "(" [Binding] ")" ;
 ObjectDispatch. Object ::= Object "." Attribute ;
-GlobalDispatch. Object ::= "Φ" "." Attribute ;
-ThisDispatch.   Object ::= "ξ" "." Attribute ;
+GlobalObject.   Object ::= "Φ";
+ThisObject.     Object ::= "ξ";
 Termination.    Object ::= "⊥" ;
 MetaObject.     Object ::= MetaId ;
+MetaFunction.   Object ::= MetaFunctionName "(" Object ")" ;
 
 AlphaBinding.   Binding ::= Attribute "↦" Object ;
 EmptyBinding.   Binding ::= Attribute "↦" "∅" ;
diff --git a/src/Language/EO/Phi/Metrics/Collect.hs b/src/Language/EO/Phi/Metrics/Collect.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/EO/Phi/Metrics/Collect.hs
@@ -0,0 +1,83 @@
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE OverloadedLabels #-}
+
+module Language.EO.Phi.Metrics.Collect where
+
+import Control.Lens ((+=))
+import Control.Monad (forM_)
+import Control.Monad.State (State, execState)
+import Data.Aeson (FromJSON)
+import Data.Generics.Labels ()
+import GHC.Generics (Generic)
+import Language.EO.Phi.Rules.Common ()
+import Language.EO.Phi.Syntax.Abs
+
+data Metrics = Metrics
+  { dataless :: Int
+  , applications :: Int
+  , formations :: Int
+  , dispatches :: Int
+  }
+  deriving (Generic, Show, FromJSON, Eq)
+
+defaultMetrics :: Metrics
+defaultMetrics =
+  Metrics
+    { dataless = 0
+    , applications = 0
+    , formations = 0
+    , dispatches = 0
+    }
+
+collectMetrics :: (Inspectable a) => a -> Metrics
+collectMetrics a = execState (inspect a) defaultMetrics
+
+class Inspectable a where
+  inspect :: a -> State Metrics ()
+
+instance Inspectable Program where
+  inspect (Program binding) = forM_ binding inspect
+
+instance Inspectable Binding where
+  inspect = \case
+    AlphaBinding attr obj -> do
+      inspect attr
+      inspect obj
+    EmptyBinding attr -> do
+      #dataless += 1
+      inspect attr
+    DeltaBinding _ -> pure ()
+    LambdaBinding _ -> #dataless += 1
+    MetaBindings _ -> pure ()
+
+instance Inspectable Attribute where
+  inspect = \case
+    Phi -> pure ()
+    Rho -> pure ()
+    Sigma -> pure ()
+    VTX -> pure ()
+    Label _ -> pure ()
+    Alpha _ -> pure ()
+    MetaAttr _ -> pure ()
+
+instance Inspectable Object where
+  inspect = \case
+    Formation bindings -> do
+      #formations += 1
+      forM_ bindings inspect
+    Application obj bindings -> do
+      #applications += 1
+      inspect obj
+      forM_ bindings inspect
+    ObjectDispatch obj attr -> do
+      #dispatches += 1
+      inspect obj
+      inspect attr
+    GlobalObject -> pure ()
+    ThisObject -> pure ()
+    Termination -> pure ()
+    MetaObject _ -> pure ()
+    MetaFunction _ _ -> pure ()
diff --git a/src/Language/EO/Phi/Normalize.hs b/src/Language/EO/Phi/Normalize.hs
--- a/src/Language/EO/Phi/Normalize.hs
+++ b/src/Language/EO/Phi/Normalize.hs
@@ -9,10 +9,9 @@
 
 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 @@
     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 @@
       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
@@ -80,7 +63,7 @@
   case object of
     -- Rule 1
     obj@(Formation _) -> rule1 obj
-    ThisDispatch a -> pure $ fromMaybe object (lookupBinding a this)
+    ObjectDispatch ThisObject a -> pure $ fromMaybe object (lookupBinding a this)
     _ -> pure object
 
 -- | Split compound object into its head and applications/dispatch actions.
@@ -89,10 +72,11 @@
   Formation bindings -> PeeledObject (HeadFormation bindings) []
   Application object bindings -> peelObject object `followedBy` ActionApplication bindings
   ObjectDispatch object attr -> peelObject object `followedBy` ActionDispatch attr
-  GlobalDispatch attr -> PeeledObject HeadGlobal [ActionDispatch attr]
-  ThisDispatch attr -> PeeledObject HeadThis [ActionDispatch attr]
+  GlobalObject -> PeeledObject HeadGlobal []
+  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])
 
@@ -102,12 +86,12 @@
     HeadFormation bindings -> go (Formation bindings) actions
     HeadGlobal ->
       case actions of
-        ActionDispatch a : as -> go (GlobalDispatch a) as
-        _ -> error "impossible: global object without dispatch!"
+        ActionApplication{} : _ -> error "impossible: application for a global object!"
+        _ -> go GlobalObject actions
     HeadThis ->
       case actions of
-        ActionDispatch a : as -> go (ThisDispatch a) as
-        _ -> error "impossible: this object without dispatch!"
+        ActionApplication{} : _ -> error "impossible: application for a global object!"
+        _ -> go ThisObject actions
     HeadTermination -> go Termination actions
  where
   go = foldl applyAction
diff --git a/src/Language/EO/Phi/Rules/Common.hs b/src/Language/EO/Phi/Rules/Common.hs
--- a/src/Language/EO/Phi/Rules/Common.hs
+++ b/src/Language/EO/Phi/Rules/Common.hs
@@ -5,13 +5,16 @@
 module Language.EO.Phi.Rules.Common where
 
 import Control.Applicative (Alternative ((<|>)), asum)
+import Data.List.NonEmpty (NonEmpty (..), (<|))
 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
+-- >>> :set -XOverloadedLists
 -- >>> import Language.EO.Phi.Syntax
 
 instance IsString Program where fromString = unsafeParseWith pProgram
@@ -37,6 +40,7 @@
 
 data Context = Context
   { allRules :: [Rule]
+  , outerFormations :: NonEmpty Object
   }
 
 -- | A rule tries to apply a transformation to the root object, if possible.
@@ -49,49 +53,55 @@
   , obj' <- rule ctx obj
   ]
 
-withSubObject :: (Object -> [Object]) -> Object -> [Object]
-withSubObject f root =
-  f root
+extendContextWith :: Object -> Context -> Context
+extendContextWith obj ctx =
+  ctx
+    { outerFormations = obj <| outerFormations ctx
+    }
+
+withSubObject :: (Context -> Object -> [Object]) -> Context -> Object -> [Object]
+withSubObject f ctx root =
+  f ctx root
     <|> case root of
       Formation bindings ->
-        Formation <$> withSubObjectBindings f bindings
+        Formation <$> withSubObjectBindings f (extendContextWith root ctx) bindings
       Application obj bindings ->
         asum
-          [ Application <$> withSubObject f obj <*> pure bindings
-          , Application obj <$> withSubObjectBindings f bindings
+          [ Application <$> withSubObject f ctx obj <*> pure bindings
+          , Application obj <$> withSubObjectBindings f ctx bindings
           ]
-      ObjectDispatch obj a -> ObjectDispatch <$> withSubObject f obj <*> pure a
-      GlobalDispatch{} -> []
-      ThisDispatch{} -> []
+      ObjectDispatch obj a -> ObjectDispatch <$> withSubObject f ctx obj <*> pure a
+      GlobalObject{} -> []
+      ThisObject{} -> []
       Termination -> []
       MetaObject _ -> []
+      MetaFunction _ _ -> []
 
-withSubObjectBindings :: (Object -> [Object]) -> [Binding] -> [[Binding]]
-withSubObjectBindings _ [] = []
-withSubObjectBindings f (b : bs) =
+withSubObjectBindings :: (Context -> Object -> [Object]) -> Context -> [Binding] -> [[Binding]]
+withSubObjectBindings _ _ [] = []
+withSubObjectBindings f ctx (b : bs) =
   asum
-    [ [b' : bs | b' <- withSubObjectBinding f b]
-    , [b : bs' | bs' <- withSubObjectBindings f bs]
+    [ [b' : bs | b' <- withSubObjectBinding f ctx b]
+    , [b : bs' | bs' <- withSubObjectBindings f ctx bs]
     ]
 
-withSubObjectBinding :: (Object -> [Object]) -> Binding -> [Binding]
-withSubObjectBinding f = \case
-  AlphaBinding a obj -> AlphaBinding a <$> withSubObject f obj
+withSubObjectBinding :: (Context -> Object -> [Object]) -> Context -> Binding -> [Binding]
+withSubObjectBinding f ctx = \case
+  AlphaBinding a obj -> AlphaBinding a <$> withSubObject f ctx obj
   EmptyBinding{} -> []
   DeltaBinding{} -> []
   LambdaBinding{} -> []
   MetaBindings _ -> []
 
 applyOneRule :: Context -> Object -> [Object]
-applyOneRule = withSubObject . applyOneRuleAtRoot
+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")
--- ⟦ ⟧ (ρ ↦ ⟦ ⟧) (ρ ↦ ⟦ ⟧)
+-- >>> 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]
@@ -119,3 +129,36 @@
   | a == a' = Just object
   | otherwise = lookupBinding a bindings
 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
+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
diff --git a/src/Language/EO/Phi/Rules/Yaml.hs b/src/Language/EO/Phi/Rules/Yaml.hs
--- a/src/Language/EO/Phi/Rules/Yaml.hs
+++ b/src/Language/EO/Phi/Rules/Yaml.hs
@@ -12,10 +12,12 @@
 import Data.Aeson (FromJSON (..), Options (sumEncoding), SumEncoding (UntaggedValue), genericParseJSON)
 import Data.Aeson.Types (defaultOptions)
 import Data.Coerce (coerce)
+import Data.List.NonEmpty qualified as NonEmpty
 import Data.Maybe (fromMaybe)
 import Data.String (IsString (..))
 import Data.Yaml qualified as Yaml
 import GHC.Generics (Generic)
+import Language.EO.Phi.Rules.Common (Context (outerFormations))
 import Language.EO.Phi.Rules.Common qualified as Common
 import Language.EO.Phi.Syntax.Abs
 
@@ -34,9 +36,16 @@
   }
   deriving (Generic, FromJSON, Show)
 
+data RuleContext = RuleContext
+  { global_object :: Maybe Object
+  , current_object :: Maybe Object
+  }
+  deriving (Generic, FromJSON, Show)
+
 data Rule = Rule
   { name :: String
   , description :: String
+  , context :: Maybe RuleContext
   , pattern :: Object
   , result :: Object
   , when :: [Condition]
@@ -72,20 +81,34 @@
 convertRule :: Rule -> Common.Rule
 convertRule Rule{..} ctx obj =
   [ obj'
-  | subst <- matchObject pattern obj
+  | contextSubsts <- matchContext ctx context
+  , let pattern' = applySubst contextSubsts pattern
+  , 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')
   ]
 
+matchContext :: Common.Context -> Maybe RuleContext -> [Subst]
+matchContext Common.Context{} Nothing = [emptySubst]
+matchContext Common.Context{..} (Just (RuleContext p1 p2)) = do
+  subst1 <- maybe [emptySubst] (`matchObject` globalObject) p1
+  subst2 <- maybe [emptySubst] ((`matchObject` thisObject) . applySubst subst1) p2
+  return (subst1 <> subst2)
+ where
+  globalObject = NonEmpty.last outerFormations
+  thisObject = NonEmpty.head outerFormations
+
 objectHasMetavars :: Object -> Bool
 objectHasMetavars (Formation bindings) = any bindingHasMetavars bindings
 objectHasMetavars (Application object bindings) = objectHasMetavars object || any bindingHasMetavars bindings
 objectHasMetavars (ObjectDispatch object attr) = objectHasMetavars object || attrHasMetavars attr
-objectHasMetavars (GlobalDispatch attr) = attrHasMetavars attr
-objectHasMetavars (ThisDispatch attr) = attrHasMetavars attr
+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
@@ -172,10 +195,8 @@
     Application (applySubst subst obj) (applySubstBindings subst bindings)
   ObjectDispatch obj a ->
     ObjectDispatch (applySubst subst obj) (applySubstAttr subst a)
-  GlobalDispatch a ->
-    GlobalDispatch (applySubstAttr subst a)
-  ThisDispatch a ->
-    ThisDispatch (applySubstAttr subst a)
+  GlobalObject -> GlobalObject
+  ThisObject -> ThisObject
   obj@(MetaObject x) -> fromMaybe obj $ lookup x objectMetas
   obj -> obj
 
@@ -220,7 +241,19 @@
       , bindingsMetas = []
       , attributeMetas = []
       }
+matchObject Termination Termination = [emptySubst]
 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]
diff --git a/src/Language/EO/Phi/Syntax/Abs.hs b/src/Language/EO/Phi/Syntax/Abs.hs
--- a/src/Language/EO/Phi/Syntax/Abs.hs
+++ b/src/Language/EO/Phi/Syntax/Abs.hs
@@ -22,10 +22,11 @@
     = Formation [Binding]
     | Application Object [Binding]
     | ObjectDispatch Object Attribute
-    | GlobalDispatch Attribute
-    | ThisDispatch Attribute
+    | GlobalObject
+    | ThisObject
     | Termination
     | MetaObject MetaId
+    | MetaFunction MetaFunctionName Object
   deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic)
 
 data Binding
@@ -73,5 +74,8 @@
   deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic, Data.String.IsString)
 
 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/src/Language/EO/Phi/Syntax/Lex.x b/src/Language/EO/Phi/Syntax/Lex.x
--- a/src/Language/EO/Phi/Syntax/Lex.x
+++ b/src/Language/EO/Phi/Syntax/Lex.x
@@ -28,7 +28,7 @@
 
 -- Symbols and non-identifier-like reserved words
 
-@rsyms = \Φ | \ξ | \Δ | \λ | \φ | \ρ | \σ | \ν | \{ | \} | \⟦ | \⟧ | \( | \) | \. | \⊥ | \↦ | \∅ | \⤍ | \,
+@rsyms = \Φ | \ξ | \Δ | \λ | \φ | \ρ | \σ | \ν | \{ | \⟦ | \⟧ | \} | \( | \) | \. | \⊥ | \↦ | \∅ | \⤍ | \,
 
 :-
 
@@ -48,7 +48,7 @@
     { tok (eitherResIdent T_Function) }
 
 -- token LabelId
-$s [$u # [\t \n \r \  \! \' \( \) \, \- \. \: \; \? \[ \] \{ \| \} \⟦ \⟧]] *
+$s [$u # [\t \n \r \  \! \' \( \) \, \. \: \; \? \[ \] \{ \| \} \⟦ \⟧]] *
     { tok (eitherResIdent T_LabelId) }
 
 -- token AlphaIndex
@@ -59,6 +59,10 @@
 \! [$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 @@
   | 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 @@
   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/src/Language/EO/Phi/Syntax/Par.y b/src/Language/EO/Phi/Syntax/Par.y
--- a/src/Language/EO/Phi/Syntax/Par.y
+++ b/src/Language/EO/Phi/Syntax/Par.y
@@ -41,31 +41,32 @@
 %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,19 +85,23 @@
 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 }
+  : '{' '⟦' ListBinding '⟧' '}' { Language.EO.Phi.Syntax.Abs.Program $3 }
 
 Object :: { Language.EO.Phi.Syntax.Abs.Object }
 Object
   : '⟦' ListBinding '⟧' { Language.EO.Phi.Syntax.Abs.Formation $2 }
   | Object '(' ListBinding ')' { Language.EO.Phi.Syntax.Abs.Application $1 $3 }
   | Object '.' Attribute { Language.EO.Phi.Syntax.Abs.ObjectDispatch $1 $3 }
-  | 'Φ' '.' Attribute { Language.EO.Phi.Syntax.Abs.GlobalDispatch $3 }
-  | 'ξ' '.' Attribute { Language.EO.Phi.Syntax.Abs.ThisDispatch $3 }
+  | 'Φ' { Language.EO.Phi.Syntax.Abs.GlobalObject }
+  | 'ξ' { 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/src/Language/EO/Phi/Syntax/Print.hs b/src/Language/EO/Phi/Syntax/Print.hs
--- a/src/Language/EO/Phi/Syntax/Print.hs
+++ b/src/Language/EO/Phi/Syntax/Print.hs
@@ -147,19 +147,22 @@
   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 "}")])
+    Language.EO.Phi.Syntax.Abs.Program bindings -> prPrec i 0 (concatD [doc (showString "{"), doc (showString "\10214"), prt 0 bindings, doc (showString "\10215"), doc (showString "}")])
 
 instance Print Language.EO.Phi.Syntax.Abs.Object where
   prt i = \case
     Language.EO.Phi.Syntax.Abs.Formation bindings -> prPrec i 0 (concatD [doc (showString "\10214"), prt 0 bindings, doc (showString "\10215")])
     Language.EO.Phi.Syntax.Abs.Application object bindings -> prPrec i 0 (concatD [prt 0 object, doc (showString "("), prt 0 bindings, doc (showString ")")])
     Language.EO.Phi.Syntax.Abs.ObjectDispatch object attribute -> prPrec i 0 (concatD [prt 0 object, doc (showString "."), prt 0 attribute])
-    Language.EO.Phi.Syntax.Abs.GlobalDispatch attribute -> prPrec i 0 (concatD [doc (showString "\934"), doc (showString "."), prt 0 attribute])
-    Language.EO.Phi.Syntax.Abs.ThisDispatch attribute -> prPrec i 0 (concatD [doc (showString "\958"), doc (showString "."), prt 0 attribute])
+    Language.EO.Phi.Syntax.Abs.GlobalObject -> prPrec i 0 (concatD [doc (showString "\934")])
+    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
diff --git a/test/Language/EO/PhiSpec.hs b/test/Language/EO/PhiSpec.hs
--- a/test/Language/EO/PhiSpec.hs
+++ b/test/Language/EO/PhiSpec.hs
@@ -1,19 +1,27 @@
 {-# LANGUAGE BlockArguments #-}
 {-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE OverloadedLists #-}
 {-# LANGUAGE OverloadedRecordDot #-}
 {-# LANGUAGE QuasiQuotes #-}
 {-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE ViewPatterns #-}
 
 module Language.EO.PhiSpec where
 
 import Control.Monad (forM_)
+import Data.Char (isSpace)
+import Data.List (dropWhileEnd)
+import Data.String (IsString (..))
 import Data.String.Interpolate (i)
+import Data.Yaml (decodeFileThrow)
 import Language.EO.Phi
+import Language.EO.Phi.Metrics.Collect (collectMetrics)
 import Language.EO.Phi.Rules.Common (Context (..), Rule)
 import Language.EO.Phi.Rules.PhiPaper (rule1, rule6)
 import Test.EO.Phi
 import Test.Hspec
+import Test.Metrics.Phi (MetricsTest (..), MetricsTestSet (..))
 
 applyRule :: (Object -> [Object]) -> Program -> [Program]
 applyRule rule = \case
@@ -24,7 +32,7 @@
 
 spec :: Spec
 spec = do
-  describe "Pre-defined rules unit tests" $
+  describe "Pre-defined rules" $
     forM_ ([(1, rule1), (6, rule6)] :: [(Int, Rule)]) $
       \(idx, rule) -> do
         PhiTestGroup{..} <- runIO (fileTests [i|test/eo/phi/rule-#{idx}.yaml|])
@@ -32,4 +40,27 @@
           forM_ tests $
             \PhiTest{..} ->
               it name $
-                applyRule (rule (Context [])) input `shouldBe` [normalized]
+                applyRule (rule (Context [] [progToObj input])) input `shouldBe` [normalized]
+  describe "Programs translated from EO" $ do
+    phiTests <- runIO (allPhiTests "test/eo/phi/from-eo/")
+    forM_ phiTests $ \PhiTestGroup{..} ->
+      describe title $
+        forM_ tests $
+          \PhiTest{..} -> do
+            describe "normalize" $
+              it name $
+                normalize input `shouldBe` normalized
+            describe "pretty-print" $
+              it name $
+                printTree input `shouldBe` trim prettified
+  describe "Metrics" $ do
+    metricsTests <- runIO $ decodeFileThrow @_ @MetricsTestSet "test/eo/phi/metrics.yaml"
+    forM_ metricsTests.tests $ \test -> do
+      it test.title $
+        collectMetrics (fromString @Program test.phi) `shouldBe` test.metrics
+
+trim :: String -> String
+trim = dropWhileEnd isSpace
+
+progToObj :: Program -> Object
+progToObj (Program bindings) = Formation bindings
diff --git a/test/Language/EO/YamlSpec.hs b/test/Language/EO/YamlSpec.hs
--- a/test/Language/EO/YamlSpec.hs
+++ b/test/Language/EO/YamlSpec.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE OverloadedLists #-}
 {-# LANGUAGE OverloadedRecordDot #-}
 
 module Language.EO.YamlSpec where
@@ -17,4 +18,4 @@
       describe rule.name do
         forM_ rule.tests $ \ruleTest -> do
           it ruleTest.name $
-            convertRule rule (Context []) ruleTest.input `shouldBe` [ruleTest.output | ruleTest.matches]
+            convertRule rule (Context [] [ruleTest.input]) ruleTest.input `shouldBe` [ruleTest.output | ruleTest.matches]
diff --git a/test/Test/Metrics/Phi.hs b/test/Test/Metrics/Phi.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Metrics/Phi.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DuplicateRecordFields #-}
+
+module Test.Metrics.Phi where
+
+import Data.Yaml (FromJSON)
+import GHC.Generics (Generic)
+import Language.EO.Phi.Metrics.Collect (Metrics)
+
+data MetricsTestSet = MetricsTestSet
+  { title :: String
+  , tests :: [MetricsTest]
+  }
+  deriving (Generic, FromJSON)
+
+data MetricsTest = MetricsTest
+  { title :: String
+  , phi :: String
+  , metrics :: Metrics
+  }
+  deriving (Generic, FromJSON)