diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,13 @@
+# Changelog for `eo-phi-normalizer`
+
+All notable changes to this project will be documented in this file.
+
+The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
+and this project adheres to the
+[Haskell Package Versioning Policy](https://pvp.haskell.org/).
+
+## Unreleased
+
+## 0.1.0 - 2024-02-02
+
+First version of the normalizer.
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright EO/Polystat Development Team (c) 2023
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of EO/Polystat Development Team nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,8 @@
+# eo-phi-normalizer
+
+[![`rzk` on Hackage](https://img.shields.io/hackage/v/eo-phi-normalizer)](http://hackage.haskell.org/package/eo-phi-normalizer)
+[![Haddock](<https://shields.io/badge/Haddock%20(master)-Code%20documentation-informational>)](https://www.objectionary.com/normalizer/haddock/)
+
+Command line normalizer of 𝜑-calculus expressions (as produced by the [EO compiler](https://github.com/objectionary/eo)).
+
+See <https://github.com/objectionary/normalizer#readme>.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,32 @@
+{-# LANGUAGE CPP #-}
+-- Source: https://github.com/haskell/cabal/issues/6726#issuecomment-918663262
+
+-- | Custom Setup that runs bnfc to generate the language sub-libraries
+-- for the parsers included in Ogma.
+module Main (main) where
+
+import           Distribution.Simple         (defaultMainWithHooks,
+                                              hookedPrograms, postConf,
+                                              preBuild, simpleUserHooks)
+import           Distribution.Simple.Program (Program (..), findProgramVersion,
+                                              simpleProgram)
+import           System.Process              (system)
+
+-- | Run BNFC on the grammar before the actual build step.
+--
+-- All options for bnfc are hard-coded here.
+main :: IO ()
+main = defaultMainWithHooks $ simpleUserHooks
+  { hookedPrograms = [ bnfcProgram ]
+  , postConf       = \args flags packageDesc localBuildInfo -> do
+#ifndef mingw32_HOST_OS
+      _ <- system "bnfc --haskell -d -p Language.EO.Phi --generic -o src/ grammar/EO/Phi/Syntax.cf"
+#endif
+      postConf simpleUserHooks args flags packageDesc localBuildInfo
+  }
+
+-- | NOTE: This should be in Cabal.Distribution.Simple.Program.Builtin.
+bnfcProgram :: Program
+bnfcProgram = (simpleProgram "bnfc")
+  { programFindVersion = findProgramVersion "--version" id
+  }
diff --git a/app/Main.hs b/app/Main.hs
new file mode 100644
--- /dev/null
+++ b/app/Main.hs
@@ -0,0 +1,70 @@
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE OverloadedRecordDot #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RecordWildCards #-}
+{-# OPTIONS_GHC -Wno-type-defaults #-}
+
+module Main where
+
+import Control.Monad (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 Options.Generic
+
+data CLINamedParams = CLINamedParams
+  { chain :: Bool
+  , rulesYaml :: Maybe String
+  , outPath :: Maybe String
+  }
+  deriving (Generic, Show, ParseRecord, Read, ParseField)
+
+instance ParseFields CLINamedParams where
+  parseFields _ _ _ _ =
+    CLINamedParams
+      <$> 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
+
+data CLIOptions = CLIOptions CLINamedParams (Maybe FilePath)
+  deriving (Generic, Show, ParseRecord)
+
+main :: IO ()
+main = do
+  opts <- getRecord "Normalizer"
+  let (CLIOptions params inPath) = opts
+  let (CLINamedParams{..}) = params
+  case rulesYaml of
+    Just path -> do
+      ruleSet <- parseRuleSetFromFile path
+      putStrLn 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)
+              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 "----------------------------------------------------"
+    -- 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
new file mode 100644
--- /dev/null
+++ b/eo-phi-normalizer.cabal
@@ -0,0 +1,127 @@
+cabal-version: 1.24
+
+-- This file has been generated from package.yaml by hpack version 0.36.0.
+--
+-- see: https://github.com/sol/hpack
+
+name:           eo-phi-normalizer
+version:        0.1.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
+bug-reports:    https://github.com/objectionary/eo-phi-normalizer/issues
+author:         EO/Polystat Development Team
+maintainer:     nickolay.kudasov@gmail.com
+copyright:      2023 EO/Polystat Development Team
+license:        BSD3
+license-file:   LICENSE
+build-type:     Custom
+extra-source-files:
+    README.md
+    CHANGELOG.md
+    grammar/EO/Phi/Syntax.cf
+
+source-repository head
+  type: git
+  location: https://github.com/objectionary/eo-phi-normalizer
+
+custom-setup
+  setup-depends:
+      Cabal >=2.4.0.1 && <4.0
+    , base >=4.11.0.0 && <5.0
+    , process >=1.6.3.0
+
+library
+  exposed-modules:
+      Language.EO.Phi
+      Language.EO.Phi.Normalize
+      Language.EO.Phi.Rules.Common
+      Language.EO.Phi.Rules.PhiPaper
+      Language.EO.Phi.Rules.Yaml
+      Language.EO.Phi.Syntax
+      Language.EO.Phi.Syntax.Abs
+      Language.EO.Phi.Syntax.Lex
+      Language.EO.Phi.Syntax.Par
+      Language.EO.Phi.Syntax.Print
+  other-modules:
+      Paths_eo_phi_normalizer
+  hs-source-dirs:
+      src
+  default-extensions:
+      ImportQualifiedPost
+  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
+  build-tools:
+      alex >=3.2.4
+    , happy >=1.19.9
+  build-tool-depends:
+      BNFC:bnfc >=2.9.4.1
+  build-depends:
+      aeson
+    , array >=0.5.5.0
+    , base >=4.7 && <5
+    , directory
+    , filepath
+    , mtl
+    , string-interpolate
+    , yaml
+  default-language: Haskell2010
+
+executable normalize-phi
+  main-is: Main.hs
+  other-modules:
+      Paths_eo_phi_normalizer
+  hs-source-dirs:
+      app
+  default-extensions:
+      ImportQualifiedPost
+  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
+  build-tools:
+      alex >=3.2.4
+    , happy >=1.19.9
+  build-tool-depends:
+      BNFC:bnfc >=2.9.4.1
+  build-depends:
+      aeson
+    , array >=0.5.5.0
+    , base >=4.7 && <5
+    , directory
+    , eo-phi-normalizer
+    , filepath
+    , mtl
+    , optparse-generic
+    , string-interpolate
+    , yaml
+  default-language: Haskell2010
+
+test-suite eo-phi-normalizer-test
+  type: exitcode-stdio-1.0
+  main-is: Spec.hs
+  other-modules:
+      Language.EO.PhiSpec
+      Language.EO.YamlSpec
+      Test.EO.Phi
+      Test.EO.Yaml
+      Paths_eo_phi_normalizer
+  hs-source-dirs:
+      test
+  default-extensions:
+      ImportQualifiedPost
+  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
+  build-tools:
+      alex >=3.2.4
+    , happy >=1.19.9
+  build-tool-depends:
+      BNFC:bnfc >=2.9.4.1
+  build-depends:
+      aeson
+    , array >=0.5.5.0
+    , base >=4.7 && <5
+    , directory
+    , eo-phi-normalizer
+    , filepath
+    , hspec
+    , hspec-discover
+    , mtl
+    , string-interpolate
+    , yaml
+  default-language: Haskell2010
diff --git a/grammar/EO/Phi/Syntax.cf b/grammar/EO/Phi/Syntax.cf
new file mode 100644
--- /dev/null
+++ b/grammar/EO/Phi/Syntax.cf
@@ -0,0 +1,52 @@
+-- ==========================================================
+-- BNFC grammar for φ-programs (translated from EO)
+-- ==========================================================
+--
+-- This is a non-ambiguous grammar for φ-programs.
+
+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)* ) ;
+token MetaId {"!"} (char - [" \r\n\t,.|':;!-?][}{)(⟧⟦"])* ;
+
+Program. Program ::= "{" [Binding] "}" ;
+
+Formation.      Object ::= "⟦" [Binding] "⟧" ;
+Application.    Object ::= Object "(" [Binding] ")" ;
+ObjectDispatch. Object ::= Object "." Attribute ;
+GlobalDispatch. Object ::= "Φ" "." Attribute ;
+ThisDispatch.   Object ::= "ξ" "." Attribute ;
+Termination.    Object ::= "⊥" ;
+MetaObject.     Object ::= MetaId ;
+
+AlphaBinding.   Binding ::= Attribute "↦" Object ;
+EmptyBinding.   Binding ::= Attribute "↦" "∅" ;
+DeltaBinding.   Binding ::= "Δ" "⤍" Bytes ;
+LambdaBinding.  Binding ::= "λ" "⤍" Function ;
+MetaBindings.   Binding ::= MetaId ;
+separator Binding "," ;
+
+Phi.    Attribute ::= "φ" ;   -- decoratee object
+Rho.    Attribute ::= "ρ" ;   -- parent object
+Sigma.  Attribute ::= "σ" ;   -- home object
+VTX.    Attribute ::= "ν" ;   -- the vertex identifier (an object that represents the unique identifier of the containing object)
+Label.  Attribute ::= LabelId ;
+Alpha.  Attribute ::= AlphaIndex ;
+MetaAttr. Attribute ::= MetaId ;
+
+-- Additional symbols used as attributes in the rules
+ObjectAttr. RuleAttribute ::= Attribute ;
+DeltaAttr.  RuleAttribute ::= "Δ" ;
+LambdaAttr. RuleAttribute ::= "λ" ;
+
+PeeledObject. PeeledObject ::= ObjectHead [ObjectAction] ;
+
+HeadFormation.    ObjectHead ::= "⟦" [Binding] "⟧" ;
+HeadGlobal.       ObjectHead ::= "Φ" ;
+HeadThis.         ObjectHead ::= "ξ" ;
+HeadTermination.  ObjectHead ::= "⊥" ;
+
+ActionApplication.  ObjectAction ::= "(" [Binding] ")" ;
+ActionDispatch.     ObjectAction ::= "." Attribute ;
+separator ObjectAction "" ;
diff --git a/src/Language/EO/Phi.hs b/src/Language/EO/Phi.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/EO/Phi.hs
@@ -0,0 +1,43 @@
+module Language.EO.Phi (
+  defaultMain,
+  normalize,
+  parseProgram,
+  unsafeParseProgram,
+  module Language.EO.Phi.Syntax,
+) where
+
+import System.Exit (exitFailure)
+
+import Language.EO.Phi.Syntax.Abs qualified as Phi
+import Language.EO.Phi.Syntax.Par qualified 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
+parseProgram input = Phi.pProgram tokens
+ where
+  tokens = Phi.myLexer input
+
+-- | Parse a 'Program' from a 'String'.
+-- May throw an 'error` if input has a syntactical or lexical errors.
+unsafeParseProgram :: String -> Phi.Program
+unsafeParseProgram input =
+  case parseProgram input of
+    Left parseError -> error parseError
+    Right program -> program
+
+-- | Default entry point.
+-- Parses a 𝜑-program from standard input, normalizes,
+-- then pretty-prints the result to standard output.
+defaultMain :: IO ()
+defaultMain = do
+  input <- getContents -- read entire standard input
+  let tokens = Phi.myLexer input
+  case Phi.pProgram tokens of
+    Left parseError -> do
+      putStrLn parseError
+      exitFailure
+    Right program -> do
+      putStrLn (printTree (normalize program))
diff --git a/src/Language/EO/Phi/Normalize.hs b/src/Language/EO/Phi/Normalize.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/EO/Phi/Normalize.hs
@@ -0,0 +1,116 @@
+{-# LANGUAGE LambdaCase #-}
+
+module Language.EO.Phi.Normalize (
+  normalizeObject,
+  normalize,
+  peelObject,
+  unpeelObject,
+) where
+
+import Control.Monad.State
+import Data.Maybe (fromMaybe)
+import Numeric (showHex)
+
+import Control.Monad (forM)
+import Language.EO.Phi.Rules.Common (lookupBinding)
+import Language.EO.Phi.Syntax.Abs
+
+data Context = Context
+  { globalObject :: [Binding]
+  , thisObject :: [Binding]
+  , totalNuCount :: Int
+  }
+
+isNu :: Binding -> Bool
+isNu (AlphaBinding VTX _) = True
+isNu (EmptyBinding VTX) = True
+isNu _ = False
+
+-- | Normalize an input 𝜑-program.
+normalize :: Program -> Program
+normalize (Program bindings) = evalState (Program . objectBindings <$> normalizeObject (Formation bindings)) context
+ where
+  context =
+    Context
+      { globalObject = bindings
+      , thisObject = bindings
+      , totalNuCount = nuCount bindings
+      }
+  nuCount binds = count isNu binds + sum (map (sum . map (nuCount . objectBindings) . values) binds)
+  count = (length .) . filter
+  values (AlphaBinding _ obj) = [obj]
+  values _ = []
+  objectBindings (Formation bs) = bs
+  objectBindings _ = []
+
+rule1 :: Object -> State Context Object
+rule1 (Formation bindings) = do
+  normalizedBindings <- forM bindings $ \case
+    AlphaBinding a object
+      | a /= VTX ->
+          do
+            object' <- rule1 object
+            pure (AlphaBinding a object')
+    b -> pure b
+  finalBindings <-
+    if not $ any isNu normalizedBindings
+      then do
+        nus <- gets totalNuCount
+        modify (\c -> c{totalNuCount = totalNuCount c + 1})
+        let pad s = (if even (length s) then "" else "0") ++ s
+        let insertDashes s
+              | length s <= 2 = s ++ "-"
+              | otherwise =
+                  let go = \case
+                        [] -> []
+                        [x] -> [x]
+                        [x, y] -> [x, y, '-']
+                        (x : y : xs) -> x : y : '-' : go xs
+                   in go s
+        let dataObject = Formation [DeltaBinding $ Bytes $ insertDashes $ pad $ showHex nus ""]
+        pure (AlphaBinding VTX dataObject : normalizedBindings)
+      else do
+        pure normalizedBindings
+  pure (Formation finalBindings)
+rule1 object = pure object
+
+normalizeObject :: Object -> State Context Object
+normalizeObject object = do
+  this <- gets thisObject
+  case object of
+    -- Rule 1
+    obj@(Formation _) -> rule1 obj
+    ThisDispatch a -> pure $ fromMaybe object (lookupBinding a this)
+    _ -> pure object
+
+-- | Split compound object into its head and applications/dispatch actions.
+peelObject :: Object -> PeeledObject
+peelObject = \case
+  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]
+  Termination -> PeeledObject HeadTermination []
+  MetaObject _ -> PeeledObject HeadTermination []
+ where
+  followedBy (PeeledObject object actions) action = PeeledObject object (actions ++ [action])
+
+unpeelObject :: PeeledObject -> Object
+unpeelObject (PeeledObject head_ actions) =
+  case head_ of
+    HeadFormation bindings -> go (Formation bindings) actions
+    HeadGlobal ->
+      case actions of
+        ActionDispatch a : as -> go (GlobalDispatch a) as
+        _ -> error "impossible: global object without dispatch!"
+    HeadThis ->
+      case actions of
+        ActionDispatch a : as -> go (ThisDispatch a) as
+        _ -> error "impossible: this object without dispatch!"
+    HeadTermination -> go Termination actions
+ where
+  go = foldl applyAction
+  applyAction object = \case
+    ActionDispatch attr -> ObjectDispatch object attr
+    ActionApplication bindings -> Application object bindings
diff --git a/src/Language/EO/Phi/Rules/Common.hs b/src/Language/EO/Phi/Rules/Common.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/EO/Phi/Rules/Common.hs
@@ -0,0 +1,121 @@
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE RecordWildCards #-}
+{-# OPTIONS_GHC -Wno-orphans #-}
+
+module Language.EO.Phi.Rules.Common where
+
+import Control.Applicative (Alternative ((<|>)), asum)
+import Data.String (IsString (..))
+import Language.EO.Phi.Syntax.Abs
+import Language.EO.Phi.Syntax.Lex (Token)
+import Language.EO.Phi.Syntax.Par
+
+-- $setup
+-- >>> :set -XOverloadedStrings
+-- >>> import Language.EO.Phi.Syntax
+
+instance IsString Program where fromString = unsafeParseWith pProgram
+instance IsString Object where fromString = unsafeParseWith pObject
+instance IsString Binding where fromString = unsafeParseWith pBinding
+instance IsString Attribute where fromString = unsafeParseWith pAttribute
+instance IsString RuleAttribute where fromString = unsafeParseWith pRuleAttribute
+instance IsString PeeledObject where fromString = unsafeParseWith pPeeledObject
+instance IsString ObjectHead where fromString = unsafeParseWith pObjectHead
+
+parseWith :: ([Token] -> Either String a) -> String -> Either String a
+parseWith parser input = parser tokens
+ where
+  tokens = myLexer input
+
+-- | Parse a 'Object' from a 'String'.
+-- May throw an 'error` if input has a syntactical or lexical errors.
+unsafeParseWith :: ([Token] -> Either String a) -> String -> a
+unsafeParseWith parser input =
+  case parseWith parser input of
+    Left parseError -> error parseError
+    Right object -> object
+
+data Context = Context
+  { allRules :: [Rule]
+  }
+
+-- | A rule tries to apply a transformation to the root object, if possible.
+type Rule = Context -> Object -> [Object]
+
+applyOneRuleAtRoot :: Context -> Object -> [Object]
+applyOneRuleAtRoot ctx@Context{..} obj =
+  [ obj'
+  | rule <- allRules
+  , 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 -> []
+      MetaObject _ -> []
+
+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{} -> []
+  MetaBindings _ -> []
+
+applyOneRule :: Context -> Object -> [Object]
+applyOneRule = withSubObject . applyOneRuleAtRoot
+
+isNF :: Context -> Object -> Bool
+isNF ctx = null . applyOneRule ctx
+
+-- | Apply rules until we get a normal form.
+--
+-- >>> mapM_ (putStrLn . Language.EO.Phi.printTree) (applyRules (Context [rule6]) "⟦ a ↦ ⟦ b ↦ ⟦ ⟧ ⟧.b ⟧.a")
+-- ⟦ ⟧ (ρ ↦ ⟦ ⟧) (ρ ↦ ⟦ ⟧)
+applyRules :: Context -> Object -> [Object]
+applyRules ctx obj
+  | isNF ctx obj = [obj]
+  | otherwise =
+      [ obj''
+      | obj' <- applyOneRule ctx obj
+      , obj'' <- applyRules ctx obj'
+      ]
+
+applyRulesChain :: Context -> Object -> [[Object]]
+applyRulesChain ctx obj
+  | isNF ctx obj = [[obj]]
+  | otherwise =
+      [ obj : chain
+      | obj' <- applyOneRule ctx obj
+      , chain <- applyRulesChain ctx obj'
+      ]
+
+-- * Helpers
+
+-- | Lookup a binding by the attribute name.
+lookupBinding :: Attribute -> [Binding] -> Maybe Object
+lookupBinding _ [] = Nothing
+lookupBinding a (AlphaBinding a' object : bindings)
+  | a == a' = Just object
+  | otherwise = lookupBinding a bindings
+lookupBinding _ _ = Nothing
diff --git a/src/Language/EO/Phi/Rules/PhiPaper.hs b/src/Language/EO/Phi/Rules/PhiPaper.hs
new file mode 100644
--- /dev/null
+++ b/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 [Formation bindings']
+  _ -> []
+
+-- | 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 _ _ = []
diff --git a/src/Language/EO/Phi/Rules/Yaml.hs b/src/Language/EO/Phi/Rules/Yaml.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/EO/Phi/Rules/Yaml.hs
@@ -0,0 +1,275 @@
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DuplicateRecordFields #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE RecordWildCards #-}
+{-# OPTIONS_GHC -Wno-orphans #-}
+{-# OPTIONS_GHC -Wno-partial-fields #-}
+
+module Language.EO.Phi.Rules.Yaml where
+
+import Data.Aeson (FromJSON (..), Options (sumEncoding), SumEncoding (UntaggedValue), genericParseJSON)
+import Data.Aeson.Types (defaultOptions)
+import Data.Coerce (coerce)
+import Data.Maybe (fromMaybe)
+import Data.String (IsString (..))
+import Data.Yaml qualified as Yaml
+import GHC.Generics (Generic)
+import Language.EO.Phi.Rules.Common qualified as Common
+import Language.EO.Phi.Syntax.Abs
+
+instance FromJSON Object where parseJSON = fmap fromString . parseJSON
+instance FromJSON Binding where parseJSON = fmap fromString . parseJSON
+instance FromJSON MetaId where parseJSON = fmap MetaId . parseJSON
+instance FromJSON Attribute where parseJSON = fmap fromString . parseJSON
+instance FromJSON RuleAttribute where parseJSON = fmap fromString . parseJSON
+
+instance FromJSON LabelId
+instance FromJSON AlphaIndex
+
+data RuleSet = RuleSet
+  { title :: String
+  , rules :: [Rule]
+  }
+  deriving (Generic, FromJSON, Show)
+
+data Rule = Rule
+  { name :: String
+  , description :: String
+  , pattern :: Object
+  , result :: Object
+  , when :: [Condition]
+  , tests :: [RuleTest]
+  }
+  deriving (Generic, FromJSON, Show)
+
+data RuleTest = RuleTest
+  { name :: String
+  , input :: Object
+  , output :: Object
+  , matches :: Bool
+  }
+  deriving (Generic, FromJSON, Show)
+
+data AttrsInBindings = AttrsInBindings
+  { attrs :: [RuleAttribute]
+  , bindings :: [Binding]
+  }
+  deriving (Generic, Show, FromJSON)
+data Condition
+  = IsNF {nf :: [MetaId]}
+  | PresentAttrs {present_attrs :: AttrsInBindings}
+  | AbsentAttrs {absent_attrs :: AttrsInBindings}
+  | AttrNotEqual {not_equal :: (Attribute, Attribute)}
+  deriving (Generic, Show)
+instance FromJSON Condition where
+  parseJSON = genericParseJSON defaultOptions{sumEncoding = UntaggedValue}
+
+parseRuleSetFromFile :: FilePath -> IO RuleSet
+parseRuleSetFromFile = Yaml.decodeFileThrow
+
+convertRule :: Rule -> Common.Rule
+convertRule Rule{..} ctx obj =
+  [ obj'
+  | subst <- matchObject pattern obj
+  , all (\cond -> checkCond ctx cond subst) when
+  , obj' <- [applySubst subst result]
+  , not (objectHasMetavars obj')
+  ]
+
+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 Termination = False
+objectHasMetavars (MetaObject _) = True
+
+bindingHasMetavars :: Binding -> Bool
+bindingHasMetavars (AlphaBinding attr obj) = attrHasMetavars attr || objectHasMetavars obj
+bindingHasMetavars (EmptyBinding attr) = attrHasMetavars attr
+bindingHasMetavars (DeltaBinding _) = False
+bindingHasMetavars (LambdaBinding _) = False
+bindingHasMetavars (MetaBindings _) = True
+
+attrHasMetavars :: Attribute -> Bool
+attrHasMetavars Phi = False
+attrHasMetavars Rho = False
+attrHasMetavars Sigma = False
+attrHasMetavars VTX = False
+attrHasMetavars (Label _) = False
+attrHasMetavars (Alpha _) = False
+attrHasMetavars (MetaAttr _) = True
+
+-- | Given a condition, and a substition from object matching
+--   tells whether the condition matches the object
+checkCond :: Common.Context -> Condition -> Subst -> Bool
+checkCond ctx (IsNF metaIds) subst = all (Common.isNF ctx . applySubst subst . MetaObject) metaIds
+checkCond _ctx (PresentAttrs (AttrsInBindings attrs bindings)) subst = any (`hasAttr` substitutedBindings) substitutedAttrs
+ where
+  substitutedBindings = concatMap (applySubstBinding subst) bindings
+  ruleToNormalAttr :: RuleAttribute -> Attribute
+  ruleToNormalAttr (ObjectAttr a) = a
+  -- Hack to be able to use applySubstAttr with RuleAttribute.
+  -- Should not actually substitute anything anyway since they are not metavariables
+  ruleToNormalAttr DeltaAttr = Label (LabelId "Δ")
+  ruleToNormalAttr LambdaAttr = Label (LabelId "λ")
+  normalToRuleAttr :: Attribute -> RuleAttribute
+  normalToRuleAttr (Label (LabelId "Δ")) = DeltaAttr
+  normalToRuleAttr (Label (LabelId "λ")) = LambdaAttr
+  normalToRuleAttr a = ObjectAttr a
+  substitutedAttrs = map (normalToRuleAttr . applySubstAttr subst . ruleToNormalAttr) attrs
+checkCond ctx (AbsentAttrs s) subst = not $ checkCond ctx (PresentAttrs s) subst
+checkCond _ctx (AttrNotEqual (a1, a2)) subst = applySubstAttr subst a1 /= applySubstAttr subst a2
+
+hasAttr :: RuleAttribute -> [Binding] -> Bool
+hasAttr attr = any (isAttr attr)
+ where
+  isAttr (ObjectAttr a) (AlphaBinding a' _) = a == a'
+  isAttr (ObjectAttr a) (EmptyBinding a') = a == a'
+  isAttr DeltaAttr (DeltaBinding _) = True
+  isAttr LambdaAttr (LambdaBinding _) = True
+  isAttr _ _ = False
+
+-- input: ⟦ a ↦ ⟦ c ↦ ⟦ ⟧ ⟧, b ↦ ⟦ ⟧ ⟧.a
+
+-- pattern:   ⟦ !a ↦ !n, !B ⟧.!a
+-- result:    !n(ρ ↦ ⟦ !B ⟧)
+
+-- match pattern input (get substitution):
+--  !a = a
+--  !n = ⟦ c ↦ ⟦ ⟧ ⟧
+--  !B = b ↦ ⟦ ⟧
+
+-- actual result (after applying substitution):
+--  ⟦ c ↦ ⟦ ⟧ ⟧(ρ ↦ ⟦ b ↦ ⟦ ⟧ ⟧)
+
+data Subst = Subst
+  { objectMetas :: [(MetaId, Object)]
+  , bindingsMetas :: [(MetaId, [Binding])]
+  , attributeMetas :: [(MetaId, Attribute)]
+  }
+  deriving (Show)
+
+instance Semigroup Subst where
+  (<>) = mergeSubst
+
+instance Monoid Subst where
+  mempty = emptySubst
+
+emptySubst :: Subst
+emptySubst = Subst [] [] []
+
+-- >>> putStrLn $ Language.EO.Phi.printTree (applySubst (Subst [("!n", "⟦ c ↦ ⟦ ⟧ ⟧")] [("!B", ["b ↦ ⟦ ⟧"])] [("!a", "a")]) "!n(ρ ↦ ⟦ !B ⟧)" :: Object)
+-- ⟦ c ↦ ⟦ ⟧ ⟧ (ρ ↦ ⟦ b ↦ ⟦ ⟧ ⟧)
+applySubst :: Subst -> Object -> Object
+applySubst subst@Subst{..} = \case
+  Formation bindings ->
+    Formation (applySubstBindings subst bindings)
+  Application obj bindings ->
+    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)
+  obj@(MetaObject x) -> fromMaybe obj $ lookup x objectMetas
+  obj -> obj
+
+applySubstAttr :: Subst -> Attribute -> Attribute
+applySubstAttr Subst{..} = \case
+  attr@(MetaAttr x) -> fromMaybe attr $ lookup x attributeMetas
+  attr -> attr
+
+applySubstBindings :: Subst -> [Binding] -> [Binding]
+applySubstBindings subst = concatMap (applySubstBinding subst)
+
+applySubstBinding :: Subst -> Binding -> [Binding]
+applySubstBinding subst@Subst{..} = \case
+  AlphaBinding a obj ->
+    [AlphaBinding (applySubstAttr subst a) (applySubst subst obj)]
+  EmptyBinding a ->
+    [EmptyBinding (applySubstAttr subst a)]
+  DeltaBinding bytes -> [DeltaBinding (coerce bytes)]
+  LambdaBinding bytes -> [LambdaBinding (coerce bytes)]
+  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')
+
+-- 1. need to implement applySubst' :: Subst -> Object -> Object
+-- 2. complete the code
+matchObject :: Object -> Object -> [Subst]
+matchObject (Formation ps) (Formation bs) = matchBindings ps bs
+matchObject (Application obj bindings) (Application obj' bindings') = do
+  subst1 <- matchObject obj obj'
+  subst2 <- matchBindings (applySubstBindings subst1 bindings) bindings'
+  pure (subst1 <> subst2)
+matchObject (ObjectDispatch pat a) (ObjectDispatch obj a') = do
+  subst1 <- matchObject pat obj
+  subst2 <- matchAttr (applySubstAttr subst1 a) a'
+  pure (subst1 <> subst2)
+matchObject (MetaObject m) obj =
+  pure
+    Subst
+      { objectMetas = [(m, obj)]
+      , bindingsMetas = []
+      , attributeMetas = []
+      }
+matchObject _ _ = [] -- ? emptySubst ?
+
+matchBindings :: [Binding] -> [Binding] -> [Subst]
+matchBindings [] [] = [emptySubst]
+matchBindings [MetaBindings b] bindings =
+  pure
+    Subst
+      { objectMetas = []
+      , bindingsMetas = [(b, bindings)]
+      , attributeMetas = []
+      }
+matchBindings (p : ps) bs = do
+  (bs', subst1) <- matchFindBinding p bs
+  subst2 <- matchBindings ps bs'
+  pure (subst1 <> subst2)
+matchBindings [] _ = []
+
+-- >>> select [1,2,3,4]
+-- [(1,[2,3,4]),(2,[1,3,4]),(3,[1,2,4]),(4,[1,2,3])]
+select :: [a] -> [(a, [a])]
+select [] = []
+select [x] = [(x, [])]
+select (x : xs) =
+  (x, xs)
+    : [ (y, x : ys)
+      | (y, ys) <- select xs
+      ]
+
+matchFindBinding :: Binding -> [Binding] -> [([Binding], Subst)]
+matchFindBinding p bindings =
+  [ (leftover, subst)
+  | (binding, leftover) <- select bindings
+  , subst <- matchBinding p binding
+  ]
+
+matchBinding :: Binding -> Binding -> [Subst]
+matchBinding MetaBindings{} _ = []
+matchBinding (AlphaBinding a obj) (AlphaBinding a' obj') = do
+  subst1 <- matchAttr a a'
+  subst2 <- matchObject obj obj'
+  pure (subst1 <> subst2)
+matchBinding _ _ = []
+
+matchAttr :: Attribute -> Attribute -> [Subst]
+matchAttr l r | l == r = [emptySubst]
+matchAttr (MetaAttr metaId) attr =
+  [ Subst
+      { objectMetas = []
+      , bindingsMetas = []
+      , attributeMetas = [(metaId, attr)]
+      }
+  ]
+matchAttr _ _ = []
diff --git a/src/Language/EO/Phi/Syntax.hs b/src/Language/EO/Phi/Syntax.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/EO/Phi/Syntax.hs
@@ -0,0 +1,86 @@
+{-# LANGUAGE LambdaCase #-}
+{-# OPTIONS_GHC -Wno-orphans #-}
+
+module Language.EO.Phi.Syntax (
+  module Language.EO.Phi.Syntax.Abs,
+  printTree,
+) where
+
+import Data.Char (isSpace)
+import Language.EO.Phi.Rules.Common ()
+import Language.EO.Phi.Syntax.Abs
+import Language.EO.Phi.Syntax.Print qualified as Phi
+
+-- * 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/src/Language/EO/Phi/Syntax/Abs.hs b/src/Language/EO/Phi/Syntax/Abs.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/EO/Phi/Syntax/Abs.hs
@@ -0,0 +1,77 @@
+-- File generated by the BNF Converter (bnfc 2.9.5).
+
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+
+-- | The abstract syntax of language Syntax.
+
+module Language.EO.Phi.Syntax.Abs where
+
+import Prelude (String)
+import qualified Prelude as C (Eq, Ord, Show, Read)
+import qualified Data.String
+
+import qualified Data.Data    as C (Data, Typeable)
+import qualified GHC.Generics as C (Generic)
+
+data Program = Program [Binding]
+  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic)
+
+data Object
+    = Formation [Binding]
+    | Application Object [Binding]
+    | ObjectDispatch Object Attribute
+    | GlobalDispatch Attribute
+    | ThisDispatch Attribute
+    | Termination
+    | MetaObject MetaId
+  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic)
+
+data Binding
+    = AlphaBinding Attribute Object
+    | EmptyBinding Attribute
+    | DeltaBinding Bytes
+    | LambdaBinding Function
+    | MetaBindings MetaId
+  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic)
+
+data Attribute
+    = Phi
+    | Rho
+    | Sigma
+    | VTX
+    | Label LabelId
+    | Alpha AlphaIndex
+    | MetaAttr MetaId
+  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic)
+
+data RuleAttribute = ObjectAttr Attribute | DeltaAttr | LambdaAttr
+  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic)
+
+data PeeledObject = PeeledObject ObjectHead [ObjectAction]
+  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic)
+
+data ObjectHead
+    = HeadFormation [Binding] | HeadGlobal | HeadThis | HeadTermination
+  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic)
+
+data ObjectAction
+    = ActionApplication [Binding] | ActionDispatch Attribute
+  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic)
+
+newtype Bytes = Bytes String
+  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic, Data.String.IsString)
+
+newtype Function = Function String
+  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic, Data.String.IsString)
+
+newtype LabelId = LabelId String
+  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic, Data.String.IsString)
+
+newtype AlphaIndex = AlphaIndex String
+  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)
+
diff --git a/src/Language/EO/Phi/Syntax/Lex.x b/src/Language/EO/Phi/Syntax/Lex.x
new file mode 100644
--- /dev/null
+++ b/src/Language/EO/Phi/Syntax/Lex.x
@@ -0,0 +1,271 @@
+-- -*- haskell -*- File generated by the BNF Converter (bnfc 2.9.5).
+
+-- Lexer definition for use with Alex 3
+{
+{-# OPTIONS -fno-warn-incomplete-patterns #-}
+{-# OPTIONS_GHC -w #-}
+
+{-# LANGUAGE PatternSynonyms #-}
+
+module Language.EO.Phi.Syntax.Lex where
+
+import Prelude
+
+import qualified Data.Bits
+import Data.Char     (ord)
+import Data.Function (on)
+import Data.Word     (Word8)
+}
+
+-- Predefined character classes
+
+$c = [A-Z\192-\221] # [\215]  -- capital isolatin1 letter (215 = \times) FIXME
+$s = [a-z\222-\255] # [\247]  -- small   isolatin1 letter (247 = \div  ) FIXME
+$l = [$c $s]         -- letter
+$d = [0-9]           -- digit
+$i = [$l $d _ ']     -- identifier character
+$u = [. \n]          -- universal: any character
+
+-- Symbols and non-identifier-like reserved words
+
+@rsyms = \Φ | \ξ | \Δ | \λ | \φ | \ρ | \σ | \ν | \{ | \} | \⟦ | \⟧ | \( | \) | \. | \⊥ | \↦ | \∅ | \⤍ | \,
+
+:-
+
+-- Whitespace (skipped)
+$white+ ;
+
+-- Symbols
+@rsyms
+    { 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]) +
+    { tok (eitherResIdent T_Bytes) }
+
+-- token Function
+$c [$u # [\t \n \r \  \! \' \( \) \, \- \. \: \; \? \[ \] \{ \| \} \⟦ \⟧]] *
+    { tok (eitherResIdent T_Function) }
+
+-- token LabelId
+$s [$u # [\t \n \r \  \! \' \( \) \, \- \. \: \; \? \[ \] \{ \| \} \⟦ \⟧]] *
+    { tok (eitherResIdent T_LabelId) }
+
+-- token AlphaIndex
+α 0 | α [$d # 0]$d *
+    { tok (eitherResIdent T_AlphaIndex) }
+
+-- token MetaId
+\! [$u # [\t \n \r \  \! \' \( \) \, \- \. \: \; \? \[ \] \{ \| \} \⟦ \⟧]] *
+    { tok (eitherResIdent T_MetaId) }
+
+-- Keywords and Ident
+$l $i*
+    { tok (eitherResIdent TV) }
+
+{
+-- | Create a token with position.
+tok :: (String -> Tok) -> (Posn -> String -> Token)
+tok f p = PT p . f
+
+-- | Token without position.
+data Tok
+  = TK {-# UNPACK #-} !TokSymbol  -- ^ Reserved word or symbol.
+  | TL !String                    -- ^ String literal.
+  | TI !String                    -- ^ Integer literal.
+  | TV !String                    -- ^ Identifier.
+  | TD !String                    -- ^ Float literal.
+  | TC !String                    -- ^ Character literal.
+  | T_Bytes !String
+  | T_Function !String
+  | T_LabelId !String
+  | T_AlphaIndex !String
+  | T_MetaId !String
+  deriving (Eq, Show, Ord)
+
+-- | Smart constructor for 'Tok' for the sake of backwards compatibility.
+pattern TS :: String -> Int -> Tok
+pattern TS t i = TK (TokSymbol t i)
+
+-- | Keyword or symbol tokens have a unique ID.
+data TokSymbol = TokSymbol
+  { tsText :: String
+      -- ^ Keyword or symbol text.
+  , tsID   :: !Int
+      -- ^ Unique ID.
+  } deriving (Show)
+
+-- | Keyword/symbol equality is determined by the unique ID.
+instance Eq  TokSymbol where (==)    = (==)    `on` tsID
+
+-- | Keyword/symbol ordering is determined by the unique ID.
+instance Ord TokSymbol where compare = compare `on` tsID
+
+-- | Token with position.
+data Token
+  = PT  Posn Tok
+  | Err Posn
+  deriving (Eq, Show, Ord)
+
+-- | Pretty print a position.
+printPosn :: Posn -> String
+printPosn (Pn _ l c) = "line " ++ show l ++ ", column " ++ show c
+
+-- | Pretty print the position of the first token in the list.
+tokenPos :: [Token] -> String
+tokenPos (t:_) = printPosn (tokenPosn t)
+tokenPos []    = "end of file"
+
+-- | Get the position of a token.
+tokenPosn :: Token -> Posn
+tokenPosn (PT p _) = p
+tokenPosn (Err p)  = p
+
+-- | Get line and column of a token.
+tokenLineCol :: Token -> (Int, Int)
+tokenLineCol = posLineCol . tokenPosn
+
+-- | Get line and column of a position.
+posLineCol :: Posn -> (Int, Int)
+posLineCol (Pn _ l c) = (l,c)
+
+-- | Convert a token into "position token" form.
+mkPosToken :: Token -> ((Int, Int), String)
+mkPosToken t = (tokenLineCol t, tokenText t)
+
+-- | Convert a token to its text.
+tokenText :: Token -> String
+tokenText t = case t of
+  PT _ (TS s _) -> s
+  PT _ (TL s)   -> show s
+  PT _ (TI s)   -> s
+  PT _ (TV s)   -> s
+  PT _ (TD s)   -> s
+  PT _ (TC s)   -> s
+  Err _         -> "#error"
+  PT _ (T_Bytes s) -> s
+  PT _ (T_Function s) -> s
+  PT _ (T_LabelId s) -> s
+  PT _ (T_AlphaIndex s) -> s
+  PT _ (T_MetaId s) -> s
+
+-- | Convert a token to a string.
+prToken :: Token -> String
+prToken t = tokenText t
+
+-- | Finite map from text to token organized as binary search tree.
+data BTree
+  = N -- ^ Nil (leaf).
+  | B String Tok BTree BTree
+      -- ^ Binary node.
+  deriving (Show)
+
+-- | Convert potential keyword into token or use fallback conversion.
+eitherResIdent :: (String -> Tok) -> String -> Tok
+eitherResIdent tv s = treeFind resWords
+  where
+  treeFind N = tv s
+  treeFind (B a t left right) =
+    case compare s a of
+      LT -> treeFind left
+      GT -> treeFind right
+      EQ -> t
+
+-- | The keywords and symbols of the language organized as binary search tree.
+resWords :: BTree
+resWords =
+  b "\958" 11
+    (b "}" 6
+       (b "," 3 (b ")" 2 (b "(" 1 N N) N) (b "{" 5 (b "." 4 N N) N))
+       (b "\955" 9 (b "\934" 8 (b "\916" 7 N N) N) (b "\957" 10 N N)))
+    (b "\8709" 16
+       (b "\966" 14 (b "\963" 13 (b "\961" 12 N N) N) (b "\8614" 15 N N))
+       (b "\10215" 19
+          (b "\10214" 18 (b "\8869" 17 N N) N) (b "\10509" 20 N N)))
+  where
+  b s n = B bs (TS bs n)
+    where
+    bs = s
+
+-- | Unquote string literal.
+unescapeInitTail :: String -> String
+unescapeInitTail = id . unesc . tail . id
+  where
+  unesc s = case s of
+    '\\':c:cs | elem c ['\"', '\\', '\''] -> c : unesc cs
+    '\\':'n':cs  -> '\n' : unesc cs
+    '\\':'t':cs  -> '\t' : unesc cs
+    '\\':'r':cs  -> '\r' : unesc cs
+    '\\':'f':cs  -> '\f' : unesc cs
+    '"':[]       -> []
+    c:cs         -> c : unesc cs
+    _            -> []
+
+-------------------------------------------------------------------
+-- Alex wrapper code.
+-- A modified "posn" wrapper.
+-------------------------------------------------------------------
+
+data Posn = Pn !Int !Int !Int
+  deriving (Eq, Show, Ord)
+
+alexStartPos :: Posn
+alexStartPos = Pn 0 1 1
+
+alexMove :: Posn -> Char -> Posn
+alexMove (Pn a l c) '\t' = Pn (a+1)  l     (((c+7) `div` 8)*8+1)
+alexMove (Pn a l c) '\n' = Pn (a+1) (l+1)   1
+alexMove (Pn a l c) _    = Pn (a+1)  l     (c+1)
+
+type Byte = Word8
+
+type AlexInput = (Posn,     -- current position,
+                  Char,     -- previous char
+                  [Byte],   -- pending bytes on the current char
+                  String)   -- current input string
+
+tokens :: String -> [Token]
+tokens str = go (alexStartPos, '\n', [], str)
+    where
+      go :: AlexInput -> [Token]
+      go inp@(pos, _, _, str) =
+               case alexScan inp 0 of
+                AlexEOF                   -> []
+                AlexError (pos, _, _, _)  -> [Err pos]
+                AlexSkip  inp' len        -> go inp'
+                AlexToken inp' len act    -> act pos (take len str) : (go inp')
+
+alexGetByte :: AlexInput -> Maybe (Byte,AlexInput)
+alexGetByte (p, c, (b:bs), s) = Just (b, (p, c, bs, s))
+alexGetByte (p, _, [], s) =
+  case s of
+    []  -> Nothing
+    (c:s) ->
+             let p'     = alexMove p c
+                 (b:bs) = utf8Encode c
+              in p' `seq` Just (b, (p', c, bs, s))
+
+alexInputPrevChar :: AlexInput -> Char
+alexInputPrevChar (p, c, bs, s) = c
+
+-- | Encode a Haskell String to a list of Word8 values, in UTF8 format.
+utf8Encode :: Char -> [Word8]
+utf8Encode = map fromIntegral . go . ord
+  where
+  go oc
+   | oc <= 0x7f       = [oc]
+
+   | oc <= 0x7ff      = [ 0xc0 + (oc `Data.Bits.shiftR` 6)
+                        , 0x80 + oc Data.Bits..&. 0x3f
+                        ]
+
+   | oc <= 0xffff     = [ 0xe0 + (oc `Data.Bits.shiftR` 12)
+                        , 0x80 + ((oc `Data.Bits.shiftR` 6) Data.Bits..&. 0x3f)
+                        , 0x80 + oc Data.Bits..&. 0x3f
+                        ]
+   | otherwise        = [ 0xf0 + (oc `Data.Bits.shiftR` 18)
+                        , 0x80 + ((oc `Data.Bits.shiftR` 12) Data.Bits..&. 0x3f)
+                        , 0x80 + ((oc `Data.Bits.shiftR` 6) Data.Bits..&. 0x3f)
+                        , 0x80 + oc Data.Bits..&. 0x3f
+                        ]
+}
diff --git a/src/Language/EO/Phi/Syntax/Par.y b/src/Language/EO/Phi/Syntax/Par.y
new file mode 100644
--- /dev/null
+++ b/src/Language/EO/Phi/Syntax/Par.y
@@ -0,0 +1,167 @@
+-- -*- haskell -*- File generated by the BNF Converter (bnfc 2.9.5).
+
+-- Parser definition for use with Happy
+{
+{-# OPTIONS_GHC -fno-warn-incomplete-patterns -fno-warn-overlapping-patterns #-}
+{-# LANGUAGE PatternSynonyms #-}
+
+module Language.EO.Phi.Syntax.Par
+  ( happyError
+  , myLexer
+  , pProgram
+  , pObject
+  , pBinding
+  , pListBinding
+  , pAttribute
+  , pRuleAttribute
+  , pPeeledObject
+  , pObjectHead
+  , pObjectAction
+  , pListObjectAction
+  ) where
+
+import Prelude
+
+import qualified Language.EO.Phi.Syntax.Abs
+import Language.EO.Phi.Syntax.Lex
+
+}
+
+%name pProgram Program
+%name pObject Object
+%name pBinding Binding
+%name pListBinding ListBinding
+%name pAttribute Attribute
+%name pRuleAttribute RuleAttribute
+%name pPeeledObject PeeledObject
+%name pObjectHead ObjectHead
+%name pObjectAction ObjectAction
+%name pListObjectAction ListObjectAction
+-- no lexer declaration
+%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 $$)     }
+
+%%
+
+Bytes :: { Language.EO.Phi.Syntax.Abs.Bytes }
+Bytes  : L_Bytes { Language.EO.Phi.Syntax.Abs.Bytes $1 }
+
+Function :: { Language.EO.Phi.Syntax.Abs.Function }
+Function  : L_Function { Language.EO.Phi.Syntax.Abs.Function $1 }
+
+LabelId :: { Language.EO.Phi.Syntax.Abs.LabelId }
+LabelId  : L_LabelId { Language.EO.Phi.Syntax.Abs.LabelId $1 }
+
+AlphaIndex :: { Language.EO.Phi.Syntax.Abs.AlphaIndex }
+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 }
+
+Program :: { Language.EO.Phi.Syntax.Abs.Program }
+Program
+  : '{' ListBinding '}' { Language.EO.Phi.Syntax.Abs.Program $2 }
+
+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.Termination }
+  | MetaId { Language.EO.Phi.Syntax.Abs.MetaObject $1 }
+
+Binding :: { Language.EO.Phi.Syntax.Abs.Binding }
+Binding
+  : Attribute '↦' Object { Language.EO.Phi.Syntax.Abs.AlphaBinding $1 $3 }
+  | Attribute '↦' '∅' { Language.EO.Phi.Syntax.Abs.EmptyBinding $1 }
+  | 'Δ' '⤍' Bytes { Language.EO.Phi.Syntax.Abs.DeltaBinding $3 }
+  | 'λ' '⤍' Function { Language.EO.Phi.Syntax.Abs.LambdaBinding $3 }
+  | MetaId { Language.EO.Phi.Syntax.Abs.MetaBindings $1 }
+
+ListBinding :: { [Language.EO.Phi.Syntax.Abs.Binding] }
+ListBinding
+  : {- empty -} { [] }
+  | Binding { (:[]) $1 }
+  | Binding ',' ListBinding { (:) $1 $3 }
+
+Attribute :: { Language.EO.Phi.Syntax.Abs.Attribute }
+Attribute
+  : 'φ' { Language.EO.Phi.Syntax.Abs.Phi }
+  | 'ρ' { Language.EO.Phi.Syntax.Abs.Rho }
+  | 'σ' { Language.EO.Phi.Syntax.Abs.Sigma }
+  | 'ν' { Language.EO.Phi.Syntax.Abs.VTX }
+  | LabelId { Language.EO.Phi.Syntax.Abs.Label $1 }
+  | AlphaIndex { Language.EO.Phi.Syntax.Abs.Alpha $1 }
+  | MetaId { Language.EO.Phi.Syntax.Abs.MetaAttr $1 }
+
+RuleAttribute :: { Language.EO.Phi.Syntax.Abs.RuleAttribute }
+RuleAttribute
+  : Attribute { Language.EO.Phi.Syntax.Abs.ObjectAttr $1 }
+  | 'Δ' { Language.EO.Phi.Syntax.Abs.DeltaAttr }
+  | 'λ' { Language.EO.Phi.Syntax.Abs.LambdaAttr }
+
+PeeledObject :: { Language.EO.Phi.Syntax.Abs.PeeledObject }
+PeeledObject
+  : ObjectHead ListObjectAction { Language.EO.Phi.Syntax.Abs.PeeledObject $1 $2 }
+
+ObjectHead :: { Language.EO.Phi.Syntax.Abs.ObjectHead }
+ObjectHead
+  : '⟦' 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 }
+  | '.' Attribute { Language.EO.Phi.Syntax.Abs.ActionDispatch $2 }
+
+ListObjectAction :: { [Language.EO.Phi.Syntax.Abs.ObjectAction] }
+ListObjectAction
+  : {- empty -} { [] } | ObjectAction ListObjectAction { (:) $1 $2 }
+
+{
+
+type Err = Either String
+
+happyError :: [Token] -> Err a
+happyError ts = Left $
+  "syntax error at " ++ tokenPos ts ++
+  case ts of
+    []      -> []
+    [Err _] -> " due to lexer error"
+    t:_     -> " before `" ++ (prToken t) ++ "'"
+
+myLexer :: String -> [Token]
+myLexer = tokens
+
+}
+
diff --git a/src/Language/EO/Phi/Syntax/Print.hs b/src/Language/EO/Phi/Syntax/Print.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/EO/Phi/Syntax/Print.hs
@@ -0,0 +1,211 @@
+-- File generated by the BNF Converter (bnfc 2.9.5).
+
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE LambdaCase #-}
+#if __GLASGOW_HASKELL__ <= 708
+{-# LANGUAGE OverlappingInstances #-}
+#endif
+
+-- | Pretty-printer for Language.
+
+module Language.EO.Phi.Syntax.Print where
+
+import Prelude
+  ( ($), (.)
+  , Bool(..), (==), (<)
+  , Int, Integer, Double, (+), (-), (*)
+  , String, (++)
+  , ShowS, showChar, showString
+  , all, elem, foldr, id, map, null, replicate, shows, span
+  )
+import Data.Char ( Char, isSpace )
+import qualified Language.EO.Phi.Syntax.Abs
+
+-- | The top-level printing method.
+
+printTree :: Print a => a -> String
+printTree = render . prt 0
+
+type Doc = [ShowS] -> [ShowS]
+
+doc :: ShowS -> Doc
+doc = (:)
+
+render :: 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 = 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
+
+  -- Make sure we are on a fresh line.
+  onNewLine :: Int -> Bool -> ShowS
+  onNewLine i p = (if p then id else showChar '\n') . indent i
+
+  -- 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 = ")],;"
+
+parenth :: Doc -> Doc
+parenth ss = doc (showChar '(') . ss . doc (showChar ')')
+
+concatS :: [ShowS] -> ShowS
+concatS = foldr (.) id
+
+concatD :: [Doc] -> Doc
+concatD = foldr (.) id
+
+replicateS :: Int -> ShowS -> ShowS
+replicateS n f = concatS (replicate n f)
+
+-- | The printer class does the job.
+
+class Print a where
+  prt :: Int -> a -> Doc
+
+instance {-# OVERLAPPABLE #-} Print a => Print [a] where
+  prt i = concatD . map (prt i)
+
+instance Print Char where
+  prt _ c = doc (showChar '\'' . mkEsc '\'' c . showChar '\'')
+
+instance Print String where
+  prt _ = printString
+
+printString :: String -> Doc
+printString s = doc (showChar '"' . concatS (map (mkEsc '"') s) . showChar '"')
+
+mkEsc :: Char -> Char -> ShowS
+mkEsc q = \case
+  s | s == q -> showChar '\\' . showChar s
+  '\\' -> showString "\\\\"
+  '\n' -> showString "\\n"
+  '\t' -> showString "\\t"
+  s -> showChar s
+
+prPrec :: Int -> Int -> Doc -> Doc
+prPrec i j = if j < i then parenth else id
+
+instance Print Integer where
+  prt _ x = doc (shows x)
+
+instance Print Double where
+  prt _ x = doc (shows x)
+
+instance Print Language.EO.Phi.Syntax.Abs.Bytes where
+  prt _ (Language.EO.Phi.Syntax.Abs.Bytes i) = doc $ showString i
+instance Print Language.EO.Phi.Syntax.Abs.Function where
+  prt _ (Language.EO.Phi.Syntax.Abs.Function i) = doc $ showString i
+instance Print Language.EO.Phi.Syntax.Abs.LabelId where
+  prt _ (Language.EO.Phi.Syntax.Abs.LabelId i) = doc $ showString i
+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.Program where
+  prt i = \case
+    Language.EO.Phi.Syntax.Abs.Program bindings -> prPrec i 0 (concatD [doc (showString "{"), prt 0 bindings, 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.Termination -> prPrec i 0 (concatD [doc (showString "\8869")])
+    Language.EO.Phi.Syntax.Abs.MetaObject metaid -> prPrec i 0 (concatD [prt 0 metaid])
+
+instance Print Language.EO.Phi.Syntax.Abs.Binding where
+  prt i = \case
+    Language.EO.Phi.Syntax.Abs.AlphaBinding attribute object -> prPrec i 0 (concatD [prt 0 attribute, doc (showString "\8614"), prt 0 object])
+    Language.EO.Phi.Syntax.Abs.EmptyBinding attribute -> prPrec i 0 (concatD [prt 0 attribute, doc (showString "\8614"), doc (showString "\8709")])
+    Language.EO.Phi.Syntax.Abs.DeltaBinding bytes -> prPrec i 0 (concatD [doc (showString "\916"), doc (showString "\10509"), prt 0 bytes])
+    Language.EO.Phi.Syntax.Abs.LambdaBinding function -> prPrec i 0 (concatD [doc (showString "\955"), doc (showString "\10509"), prt 0 function])
+    Language.EO.Phi.Syntax.Abs.MetaBindings metaid -> prPrec i 0 (concatD [prt 0 metaid])
+
+instance Print [Language.EO.Phi.Syntax.Abs.Binding] where
+  prt _ [] = concatD []
+  prt _ [x] = concatD [prt 0 x]
+  prt _ (x:xs) = concatD [prt 0 x, doc (showString ","), prt 0 xs]
+
+instance Print Language.EO.Phi.Syntax.Abs.Attribute where
+  prt i = \case
+    Language.EO.Phi.Syntax.Abs.Phi -> prPrec i 0 (concatD [doc (showString "\966")])
+    Language.EO.Phi.Syntax.Abs.Rho -> prPrec i 0 (concatD [doc (showString "\961")])
+    Language.EO.Phi.Syntax.Abs.Sigma -> prPrec i 0 (concatD [doc (showString "\963")])
+    Language.EO.Phi.Syntax.Abs.VTX -> prPrec i 0 (concatD [doc (showString "\957")])
+    Language.EO.Phi.Syntax.Abs.Label labelid -> prPrec i 0 (concatD [prt 0 labelid])
+    Language.EO.Phi.Syntax.Abs.Alpha alphaindex -> prPrec i 0 (concatD [prt 0 alphaindex])
+    Language.EO.Phi.Syntax.Abs.MetaAttr metaid -> prPrec i 0 (concatD [prt 0 metaid])
+
+instance Print Language.EO.Phi.Syntax.Abs.RuleAttribute where
+  prt i = \case
+    Language.EO.Phi.Syntax.Abs.ObjectAttr attribute -> prPrec i 0 (concatD [prt 0 attribute])
+    Language.EO.Phi.Syntax.Abs.DeltaAttr -> prPrec i 0 (concatD [doc (showString "\916")])
+    Language.EO.Phi.Syntax.Abs.LambdaAttr -> prPrec i 0 (concatD [doc (showString "\955")])
+
+instance Print Language.EO.Phi.Syntax.Abs.PeeledObject where
+  prt i = \case
+    Language.EO.Phi.Syntax.Abs.PeeledObject objecthead objectactions -> prPrec i 0 (concatD [prt 0 objecthead, prt 0 objectactions])
+
+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 "\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.ActionDispatch attribute -> prPrec i 0 (concatD [doc (showString "."), prt 0 attribute])
+
+instance Print [Language.EO.Phi.Syntax.Abs.ObjectAction] where
+  prt _ [] = concatD []
+  prt _ (x:xs) = concatD [prt 0 x, prt 0 xs]
diff --git a/test/Language/EO/PhiSpec.hs b/test/Language/EO/PhiSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Language/EO/PhiSpec.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE OverloadedRecordDot #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE ViewPatterns #-}
+
+module Language.EO.PhiSpec where
+
+import Control.Monad (forM_)
+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
+
+applyRule :: (Object -> [Object]) -> Program -> [Program]
+applyRule rule = \case
+  Program [AlphaBinding name obj] -> do
+    r <- rule obj
+    pure $ Program [AlphaBinding name r]
+  _ -> []
+
+spec :: Spec
+spec = do
+  describe "Pre-defined rules unit tests" $
+    forM_ ([(1, rule1), (6, rule6)] :: [(Int, Rule)]) $
+      \(idx, rule) -> do
+        PhiTestGroup{..} <- runIO (fileTests [i|test/eo/phi/rule-#{idx}.yaml|])
+        describe title $
+          forM_ tests $
+            \PhiTest{..} ->
+              it name $
+                applyRule (rule (Context [])) input `shouldBe` [normalized]
diff --git a/test/Language/EO/YamlSpec.hs b/test/Language/EO/YamlSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Language/EO/YamlSpec.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE OverloadedRecordDot #-}
+
+module Language.EO.YamlSpec where
+
+import Control.Monad (forM_)
+import Language.EO.Phi.Rules.Common (Context (..))
+import Language.EO.Phi.Rules.Yaml (Rule (..), RuleSet (..), RuleTest (..), convertRule)
+import Test.EO.Yaml
+import Test.Hspec
+
+spec :: Spec
+spec = describe "User-defined rules unit tests" do
+  ruleset <- runIO $ fileTests "test/eo/phi/rules/yegor.yaml"
+  describe ruleset.title do
+    forM_ ruleset.rules $ \rule -> do
+      describe rule.name do
+        forM_ rule.tests $ \ruleTest -> do
+          it ruleTest.name $
+            convertRule rule (Context []) ruleTest.input `shouldBe` [ruleTest.output | ruleTest.matches]
diff --git a/test/Spec.hs b/test/Spec.hs
new file mode 100644
--- /dev/null
+++ b/test/Spec.hs
@@ -0,0 +1,1 @@
+{-# OPTIONS_GHC -F -pgmF hspec-discover #-}
diff --git a/test/Test/EO/Phi.hs b/test/Test/EO/Phi.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/EO/Phi.hs
@@ -0,0 +1,46 @@
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# OPTIONS_GHC -Wno-orphans #-}
+
+module Test.EO.Phi where
+
+import Control.Monad (forM)
+import Data.Aeson (FromJSON (..))
+import Data.Yaml qualified as Yaml
+import GHC.Generics (Generic)
+import System.Directory (listDirectory)
+import System.FilePath ((</>))
+
+import Data.List (sort)
+import Language.EO.Phi (unsafeParseProgram)
+import Language.EO.Phi qualified as Phi
+
+data PhiTestGroup = PhiTestGroup
+  { title :: String
+  , tests :: [PhiTest]
+  }
+  deriving (Generic, FromJSON)
+
+data PhiTest = PhiTest
+  { name :: String
+  , input :: Phi.Program
+  , normalized :: Phi.Program
+  , prettified :: String
+  }
+  deriving (Generic, FromJSON)
+
+fileTests :: FilePath -> IO PhiTestGroup
+fileTests = Yaml.decodeFileThrow
+
+allPhiTests :: FilePath -> IO [PhiTestGroup]
+allPhiTests dir = do
+  paths <- listDirectory dir
+  forM (sort paths) $ \path ->
+    fileTests (dir </> path)
+
+-- * Orphan instances
+
+-- | Parsing a $\varphi$-program from a JSON string.
+instance FromJSON Phi.Program where
+  parseJSON = fmap unsafeParseProgram . parseJSON
diff --git a/test/Test/EO/Yaml.hs b/test/Test/EO/Yaml.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/EO/Yaml.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE DuplicateRecordFields #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# OPTIONS_GHC -Wno-orphans #-}
+
+module Test.EO.Yaml where
+
+import Control.Monad (forM)
+import Data.List (sort)
+import Language.EO.Phi.Rules.Yaml (RuleSet, parseRuleSetFromFile)
+import System.Directory (listDirectory)
+import System.FilePath ((</>))
+
+fileTests :: FilePath -> IO RuleSet
+fileTests = parseRuleSetFromFile
+
+directoryTests :: FilePath -> IO [RuleSet]
+directoryTests dir = do
+  paths <- listDirectory dir
+  forM (sort paths) $ \path ->
+    fileTests (dir </> path)