From 68284cd884fe5a69a90343c1e9276414ced2ce0a Mon Sep 17 00:00:00 2001 From: Abdelrahman Abounegm Date: Wed, 7 Feb 2024 01:01:51 +0300 Subject: [PATCH 1/6] Add outerFormations to context --- eo-phi-normalizer/app/Main.hs | 4 +- .../src/Language/EO/Phi/Rules/Common.hs | 39 +++++++++++-------- eo-phi-normalizer/test/Language/EO/PhiSpec.hs | 2 +- .../test/Language/EO/YamlSpec.hs | 2 +- 4 files changed, 27 insertions(+), 20 deletions(-) diff --git a/eo-phi-normalizer/app/Main.hs b/eo-phi-normalizer/app/Main.hs index df4cef5ac..a6c0d5396 100644 --- a/eo-phi-normalizer/app/Main.hs +++ b/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:" diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs index a379786f9..f536f0ade 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs +++ b/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 diff --git a/eo-phi-normalizer/test/Language/EO/PhiSpec.hs b/eo-phi-normalizer/test/Language/EO/PhiSpec.hs index 2df5e9b2a..f6c41887d 100644 --- a/eo-phi-normalizer/test/Language/EO/PhiSpec.hs +++ b/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{..} -> diff --git a/eo-phi-normalizer/test/Language/EO/YamlSpec.hs b/eo-phi-normalizer/test/Language/EO/YamlSpec.hs index 6481c8f3a..e10fdcac5 100644 --- a/eo-phi-normalizer/test/Language/EO/YamlSpec.hs +++ b/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] From 94348a3875197c1616abd936a71e1a3f1e7376f9 Mon Sep 17 00:00:00 2001 From: Abdelrahman Abounegm Date: Wed, 7 Feb 2024 01:02:18 +0300 Subject: [PATCH 2/6] Implement matching Phi from rule context --- .../src/Language/EO/Phi/Rules/Yaml.hs | 26 +++++++++++++++++-- 1 file changed, 24 insertions(+), 2 deletions(-) diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs index 6a0a8e374..d6ea8c6f7 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs +++ b/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 From 346046dc98eca320336b61ce75356ec6a798f449 Mon Sep 17 00:00:00 2001 From: Abdelrahman Abounegm Date: Wed, 7 Feb 2024 01:04:21 +0300 Subject: [PATCH 3/6] Add rule 4 to user-defined rules --- eo-phi-normalizer/test/eo/phi/rules/yegor.yaml | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/eo-phi-normalizer/test/eo/phi/rules/yegor.yaml b/eo-phi-normalizer/test/eo/phi/rules/yegor.yaml index 2644a7e5f..6d01d3622 100644 --- a/eo-phi-normalizer/test/eo/phi/rules/yegor.yaml +++ b/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: | From 0b78d54191333590209c1aaf3c388bee9c5dc435 Mon Sep 17 00:00:00 2001 From: Abdelrahman Abounegm Date: Wed, 7 Feb 2024 16:11:58 +0300 Subject: [PATCH 4/6] Change outerFormation to a non-empty list Co-authored-by: Nikolai Kudasov --- eo-phi-normalizer/app/Main.hs | 5 +++-- eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs | 5 +++-- eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs | 5 +++-- eo-phi-normalizer/test/Language/EO/PhiSpec.hs | 6 +++++- eo-phi-normalizer/test/Language/EO/YamlSpec.hs | 3 ++- 5 files changed, 16 insertions(+), 8 deletions(-) diff --git a/eo-phi-normalizer/app/Main.hs b/eo-phi-normalizer/app/Main.hs index a6c0d5396..8e179ce62 100644 --- a/eo-phi-normalizer/app/Main.hs +++ b/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:" diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs index f536f0ade..f8ee92f1c 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs +++ b/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,7 +38,7 @@ unsafeParseWith parser input = data Context = Context { allRules :: [Rule] - , outerFormations :: [Object] + , outerFormations :: NonEmpty Object } -- | A rule tries to apply a transformation to the root object, if possible. @@ -53,7 +54,7 @@ applyOneRuleAtRoot ctx@Context{..} obj = extendContextWith :: Object -> Context -> Context extendContextWith obj ctx = ctx - { outerFormations = obj : outerFormations ctx + { outerFormations = obj <| outerFormations ctx } withSubObject :: (Context -> Object -> [Object]) -> Context -> Object -> [Object] diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs index d6ea8c6f7..0ce242e01 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs +++ b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs @@ -12,6 +12,7 @@ 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 @@ -97,8 +98,8 @@ matchContext Common.Context{..} obj = \case 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 + globalObject = NonEmpty.last outerFormations + thisObject = NonEmpty.head outerFormations objectHasMetavars :: Object -> Bool objectHasMetavars (Formation bindings) = any bindingHasMetavars bindings diff --git a/eo-phi-normalizer/test/Language/EO/PhiSpec.hs b/eo-phi-normalizer/test/Language/EO/PhiSpec.hs index f6c41887d..9d0185acb 100644 --- a/eo-phi-normalizer/test/Language/EO/PhiSpec.hs +++ b/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 diff --git a/eo-phi-normalizer/test/Language/EO/YamlSpec.hs b/eo-phi-normalizer/test/Language/EO/YamlSpec.hs index e10fdcac5..dfbb78024 100644 --- a/eo-phi-normalizer/test/Language/EO/YamlSpec.hs +++ b/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] From 4d68a2f2647ce771fa16d4db349e3db143ba8d53 Mon Sep 17 00:00:00 2001 From: Abdelrahman Abounegm Date: Wed, 7 Feb 2024 16:30:48 +0300 Subject: [PATCH 5/6] Clean up (and fix) the context matching function Co-authored-by: Nikolai Kudasov --- .../src/Language/EO/Phi/Rules/Yaml.hs | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs index 0ce242e01..7437f8d60 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs +++ b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs @@ -81,7 +81,7 @@ parseRuleSetFromFile = Yaml.decodeFileThrow convertRule :: Rule -> Common.Rule convertRule Rule{..} ctx obj = [ obj' - | contextSubsts <- matchContext ctx obj context + | contextSubsts <- matchContext ctx context , let pattern' = applySubst contextSubsts pattern , let result' = applySubst contextSubsts result , subst <- matchObject pattern' obj @@ -90,13 +90,12 @@ convertRule Rule{..} ctx obj = , 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 +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 From 067109de9727408dab06ff23870afd7f914b9916 Mon Sep 17 00:00:00 2001 From: Abdelrahman Abounegm Date: Wed, 7 Feb 2024 16:31:21 +0300 Subject: [PATCH 6/6] Modify rule 5 to use context Co-authored-by: Nikolai Kudasov --- eo-phi-normalizer/test/eo/phi/rules/yegor.yaml | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/eo-phi-normalizer/test/eo/phi/rules/yegor.yaml b/eo-phi-normalizer/test/eo/phi/rules/yegor.yaml index 6d01d3622..c41b0c06a 100644 --- a/eo-phi-normalizer/test/eo/phi/rules/yegor.yaml +++ b/eo-phi-normalizer/test/eo/phi/rules/yegor.yaml @@ -36,18 +36,16 @@ rules: result: | ⟦ σ ↦ Φ, !B ⟧.!a when: [] - tests: - - name: Should match - input: Φ.a - output: ⟦ σ ↦ Φ ⟧.a - matches: true + tests: [] - name: Rule 5 description: "ξ-dispatch" + context: + current_object: ⟦ !a ↦ ξ.!b, !B ⟧ pattern: | - ⟦ !a ↦ ξ.!b, !B ⟧ + ξ result: | - ⟦ !a ↦ ⟦ !B ⟧.!b, !B ⟧ + ⟦ !B ⟧ when: [] tests: []