Merge pull request #99 from objectionary/rule-context-matching

Global object matching

eo-phi-normalizer/app/Main.hs

@@ -1,5 +1,6 @@
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE OverloadedLists #-}
 {-# LANGUAGE OverloadedRecordDot #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE RecordWildCards #-}
@@ -52,8 +53,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]) (Formation bindings)
+                | otherwise = pure <$> applyRules (Context (convertRule <$> ruleSet.rules) [Formation bindings]) (Formation bindings)
               uniqueResults = nub results
               totalResults = length uniqueResults
           logStrLn "Input:"

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

@@ -5,6 +5,7 @@
 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)
@@ -37,6 +38,7 @@ unsafeParseWith parser input =
 
 data Context = Context
   { allRules :: [Rule]
+  , outerFormations :: NonEmpty Object
   }
 
 -- | A rule tries to apply a transformation to the root object, if possible.
@@ -49,41 +51,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

@@ -12,10 +12,12 @@ 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.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 @@ 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 +81,25 @@ parseRuleSetFromFile = Yaml.decodeFileThrow
 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 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

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

@@ -1,5 +1,6 @@
 {-# LANGUAGE BlockArguments #-}
 {-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE OverloadedLists #-}
 {-# LANGUAGE OverloadedRecordDot #-}
 {-# LANGUAGE QuasiQuotes #-}
 {-# LANGUAGE RecordWildCards #-}
@@ -34,7 +35,7 @@ spec = do
           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{..} ->
@@ -50,3 +51,6 @@ spec = do
 
 trim :: String -> String
 trim = dropWhileEnd isSpace
+
+progToObj :: Program -> Object
+progToObj (Program bindings) = Formation bindings

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

@@ -1,4 +1,5 @@
 {-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE OverloadedLists #-}
 {-# LANGUAGE OverloadedRecordDot #-}
 
 module Language.EO.YamlSpec where
@@ -17,4 +18,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]) ruleTest.input `shouldBe` [ruleTest.output | ruleTest.matches]

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

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