Global object matching

eo-phi-normalizer/app/Main.hs

@@ -52,8 +52,8 @@ main = do
         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)
+                | otherwise = pure <$> applyRules (Context (convertRule <$> ruleSet.rules) []) (Formation bindings)
               uniqueResults = nub results
               totalResults = length uniqueResults
           logStrLn "Input:"

eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs

@@ -37,6 +37,7 @@ unsafeParseWith parser input =
 
 data Context = Context
   { allRules :: [Rule]
+  , outerFormations :: [Object]
   }
 
 -- | A rule tries to apply a transformation to the root object, if possible.
@@ -49,41 +50,47 @@ applyOneRuleAtRoot ctx@Context{..} obj =
   , 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
+      ObjectDispatch obj a -> ObjectDispatch <$> withSubObject f ctx obj <*> pure a
       GlobalObject{} -> []
       ThisObject{} -> []
       Termination -> []
       MetaObject _ -> []
 
-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

eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs

@@ -16,6 +16,7 @@ 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 +35,16 @@ data RuleSet = RuleSet
   }
   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,12 +80,26 @@ parseRuleSetFromFile = Yaml.decodeFileThrow
 convertRule :: Rule -> Common.Rule
 convertRule Rule{..} ctx obj =
   [ obj'
-  | subst <- matchObject pattern obj
+  | contextSubsts <- matchContext ctx obj 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 result']
   , not (objectHasMetavars obj')
   ]
 
+matchContext :: Common.Context -> Object -> Maybe RuleContext -> [Subst]
+matchContext Common.Context{..} obj = \case
+  Nothing -> [emptySubst]
+  Just (RuleContext Nothing Nothing) -> [emptySubst]
+  Just (RuleContext (Just pattern) Nothing) -> matchObject pattern globalObject
+  Just (RuleContext Nothing (Just pattern)) -> matchObject pattern thisObject
+  Just (RuleContext (Just globalPattern) (Just thisPattern)) -> matchObject globalPattern globalObject ++ matchObject thisPattern thisObject
+ where
+  globalObject = last outerFormations
+  thisObject = head outerFormations
+
 objectHasMetavars :: Object -> Bool
 objectHasMetavars (Formation bindings) = any bindingHasMetavars bindings
 objectHasMetavars (Application object bindings) = objectHasMetavars object || any bindingHasMetavars bindings

eo-phi-normalizer/test/Language/EO/PhiSpec.hs

@@ -34,7 +34,7 @@ spec = do
           forM_ tests $
             \PhiTest{..} ->
               it name $
-                applyRule (rule (Context [])) input `shouldBe` [normalized]
+                applyRule (rule (Context [] [])) input `shouldBe` [normalized]
   describe "Programs translated from EO" $ do
     phiTests <- runIO (allPhiTests "test/eo/phi/from-eo/")
     forM_ phiTests $ \PhiTestGroup{..} ->

eo-phi-normalizer/test/Language/EO/YamlSpec.hs

@@ -17,4 +17,4 @@ spec = describe "User-defined rules unit tests" do
       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 `shouldBe` [ruleTest.output | ruleTest.matches]

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

@@ -27,6 +27,21 @@ rules:
         output: '⟦ a ↦ ⟦ b ↦ ⟦ ⟧ ⟧ ⟧'
         matches: false
 
+  - name: Rule 4
+    description: 'Φ-dispatch'
+    context:
+      global_object: ⟦ !B ⟧
+    pattern: |
+      Φ.!a
+    result: |
+      ⟦ σ ↦ Φ, !B ⟧.!a
+    when: []
+    tests:
+      - name: Should match
+        input: Φ.a
+        output: ⟦ σ ↦ Φ ⟧.a
+        matches: true
+
   - name: Rule 5
     description: "ξ-dispatch"
     pattern: |