Support --chain option, sketch more rules in yegor.yaml

eo-phi-normalizer/app/Main.hs

@@ -4,6 +4,7 @@
 {-# LANGUAGE OverloadedRecordDot #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE RecordWildCards #-}
+{-# OPTIONS_GHC -Wno-type-defaults #-}
 
 module Main where
 
@@ -12,7 +13,7 @@ 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)
+import Language.EO.Phi.Rules.Common (Context (..), applyRules, applyRulesChain)
 import Language.EO.Phi.Rules.Yaml
 import Options.Generic
 
@@ -47,15 +48,24 @@ main = do
       let progOrError = parseProgram src
       case progOrError of
         Left err -> error ("An error occurred parsing the input program: " <> err)
-        Right (Program bindings) -> do
-          let objects = applyRules (Context (convertRule <$> ruleSet.rules)) (Formation bindings)
-              progs =
-                ( \case
-                    Formation x -> Right $ Program x
-                    obj -> Left ("Normalization yielded an invalid program: " <> printTree obj)
-                )
-                  <$> objects
+        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: use outPath to output to file if provided
-          forM_ (nub progs) (putStrLn . either id printTree)
+          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: still need to consider `chain`
     Nothing -> defaultMain

eo-phi-normalizer/test/eo/phi/rule-6.yaml

@@ -1,9 +1,22 @@
 title: Tests for Rule 6
 tests:
-  - name: 'Case (1)'
+  - name: "Case (1)"
     input: |
       { a ↦ ⟦ b ↦ ⟦ Δ ⤍ 00- ⟧, c ↦ ⟦ Δ ⤍ 03- ⟧ ⟧.b }
     normalized: |
       { a ↦ ⟦ Δ ⤍ 00- ⟧(ρ ↦ ⟦ c ↦ ⟦ Δ ⤍ 03- ⟧ ⟧) }
     prettified: |
-      { a ↦ ⟦ b ↦ ⟦ Δ ⤍ 00- ⟧, c ↦ ⟦ Δ ⤍ 03- ⟧ ⟧.b }
+      { a ↦ ⟦ b ↦ ⟦ Δ ⤍ 00- ⟧, c ↦ ⟦ Δ ⤍ 03- ⟧ ⟧.b }
+  - name: "Case (2)"
+    input: |
+      {
+        a ↦
+          ⟦
+            b ↦
+              ⟦
+                c ↦ ∅,
+                d ↦ ⟦ φ ↦ ξ.ρ.c ⟧
+              ⟧,
+            e ↦ ξ.b(c ↦ ⟦⟧).d
+          ⟧.e
+      }

eo-phi-normalizer/test/eo/phi/rules/yegor.yaml

@@ -1,19 +1,48 @@
 title: "Rule set based on Yegor's draft"
 rules:
+  - name: Rule 5
+    description: "ξ-dispatch"
+    pattern: |
+      ⟦ !a ↦ ξ.!b, !B ⟧
+    result: |
+      ⟦ !a ↦ ⟦ !B ⟧.!b, !B ⟧
+    when: []
+    tests: []
+
   - name: Rule 6
     description: "Accessing an α-binding"
     pattern: |
       ⟦ !a ↦ !n, !B ⟧.!a
     result: |
       !n(ρ ↦ ⟦ !B ⟧)
     when:
-      - nf: [ "!n" ]
+      - nf: ["!n"]
     tests:
       - name: Should match
         input: ⟦ hello ↦ ⟦⟧ ⟧.hello
         output: ⟦⟧(ρ ↦ ⟦⟧)
         matches: true
       - name: Shouldn't match
         input: ⟦ ⟧.hello
-        output: ''
+        output: ""
         matches: false
+
+  - name: Rule 7
+    description: "Application"
+    pattern: |
+      ⟦ !a ↦ ∅, !B ⟧(!a ↦ !n)
+    result: |
+      ⟦ !a ↦ !n, !B ⟧
+    when:
+      - nf: ["!n"]
+    tests: []
+
+  # - name: Rule 8
+
+  - name: Rule 9
+    description: "Parent application"
+    pattern: ⟦ ρ ↦ !t, !B ⟧(ρ ↦ !n)
+    result: ⟦ ρ ↦ !n, !B ⟧
+    when:
+      - nf: ["!n"]
+    tests: []