From 33b835fbe12465b3356830854ebbf479fee9f3a2 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Fri, 12 Jul 2024 10:58:58 +0300 Subject: [PATCH 01/12] Support minimal streams example --- eo-phi-normalizer/eo-phi-normalizer.cabal | 3 - .../src/Language/EO/Phi/Rules/Common.hs | 10 +++- .../src/Language/EO/Phi/Rules/Yaml.hs | 24 +++++++- .../test/Language/EO/YamlSpec.hs | 29 ++++++---- .../test/eo/phi/rules/streams.yaml | 57 +++++++++++++++++++ .../test/eo/phi/rules/yegor.yaml | 7 ++- 6 files changed, 109 insertions(+), 21 deletions(-) create mode 100644 eo-phi-normalizer/test/eo/phi/rules/streams.yaml diff --git a/eo-phi-normalizer/eo-phi-normalizer.cabal b/eo-phi-normalizer/eo-phi-normalizer.cabal index 7f35270d..400e7980 100644 --- a/eo-phi-normalizer/eo-phi-normalizer.cabal +++ b/eo-phi-normalizer/eo-phi-normalizer.cabal @@ -22,7 +22,6 @@ extra-source-files: grammar/EO/Phi/Syntax.cf report/main.js report/styles.css - data/0.36.0/0.36.0.md data/0.36.0/org/eolang/as-phi.phi data/0.36.0/org/eolang/bool.phi data/0.36.0/org/eolang/bytes.phi @@ -52,7 +51,6 @@ extra-source-files: data/0.36.0/org/eolang/try.phi data/0.36.0/org/eolang/tuple.phi data/0.36.0/org/eolang/while.phi - data/0.37.0/0.37.0.md data/0.37.0/org/eolang/as-phi.phi data/0.37.0/org/eolang/bytes.phi data/0.37.0/org/eolang/cage.phi @@ -77,7 +75,6 @@ extra-source-files: data/0.37.0/org/eolang/try.phi data/0.37.0/org/eolang/tuple.phi data/0.37.0/org/eolang/while.phi - data/0.38.0/0.38.0.md data/0.38.0/org/eolang/as-phi.phi data/0.38.0/org/eolang/bytes.phi data/0.38.0/org/eolang/cage.phi 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 ad995a53..b97b678a 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs +++ b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs @@ -64,6 +64,7 @@ data Context = Context , currentAttr :: Attribute , insideFormation :: Bool -- ^ Temporary hack for applying Ksi and Phi rules when dataizing + , insideAbstractFormation :: Bool , dataizePackage :: Bool -- ^ Temporary flag to only dataize Package attributes for the top-level formation. , minimizeTerms :: Bool @@ -85,6 +86,7 @@ defaultContext rules obj = , outerFormations = NonEmpty.singleton obj , currentAttr = Phi , insideFormation = False + , insideAbstractFormation = False , dataizePackage = True , minimizeTerms = False , insideSubObject = False @@ -117,9 +119,11 @@ withSubObject :: (Context -> Object -> [(String, Object)]) -> Context -> Object withSubObject f ctx root = f ctx root <|> case root of - Formation bindings - | not (any isEmptyBinding bindings) -> propagateName1 Formation <$> withSubObjectBindings f ((extendContextWith root subctx){insideFormation = True}) bindings - | otherwise -> [] + Formation bindings -> + propagateName1 Formation + <$> withSubObjectBindings f ((extendContextWith root subctx){insideFormation = True, insideAbstractFormation = isAbstract}) bindings + where + isAbstract = any isEmptyBinding bindings Application obj bindings -> asum [ propagateName2 Application <$> withSubObject f subctx obj <*> pure bindings 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 760062d9..9561e278 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs +++ b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs @@ -26,7 +26,7 @@ import Data.Yaml qualified as Yaml import GHC.Generics (Generic) import Language.EO.Phi -import Language.EO.Phi.Rules.Common (Context (insideFormation, outerFormations), NamedRule) +import Language.EO.Phi.Rules.Common (Context (..), NamedRule) import Language.EO.Phi.Rules.Common qualified as Common import PyF (fmt) @@ -62,6 +62,7 @@ data Rule = Rule , context :: Maybe RuleContext , pattern :: Object , result :: Object + , fresh :: Maybe [MetaId] , when :: [Condition] , tests :: [RuleTest] } @@ -86,6 +87,7 @@ data Condition | AbsentAttrs {absent_attrs :: AttrsInBindings} | AttrNotEqual {not_equal :: (Attribute, Attribute)} | ApplyInSubformations {apply_in_subformations :: Bool} + | ApplyInAbstractSubformations {apply_in_abstract_subformations :: Bool} deriving (Generic, Show) instance FromJSON Condition where parseJSON = genericParseJSON defaultOptions{sumEncoding = UntaggedValue} @@ -100,7 +102,8 @@ convertRule Rule{..} ctx obj = do result' = applySubst contextSubsts result subst <- matchObject pattern' obj guard $ all (\cond -> checkCond ctx cond (contextSubsts <> subst)) when - let result'' = applySubst (contextSubsts <> subst) result' + let substFresh = mkFreshSubst ctx result' fresh + result'' = applySubst (contextSubsts <> subst <> substFresh) result' -- TODO #152:30m what context should we pass to evaluate meta funcs? obj' = evaluateMetaFuncs obj result'' guard $ not (objectHasMetavars obj') @@ -109,6 +112,20 @@ convertRule Rule{..} ctx obj = do convertRuleNamed :: Rule -> NamedRule convertRuleNamed rule = (rule.name, convertRule rule) +mkFreshSubst :: Context -> Object -> Maybe [MetaId] -> Subst +mkFreshSubst ctx obj metas = + Subst + { objectMetas = [] + , bindingsMetas = [] + , attributeMetas = zip (fromMaybe [] metas) (filter isFresh defaultFreshAttrs) + , bytesMetas = [] + } + where + isFresh _ = True + +defaultFreshAttrs :: [Attribute] +defaultFreshAttrs = [Label (LabelId ("tmp_" <> show i)) | i <- [1 ..]] + -- >>> matchContext (Context [] ["⟦ a ↦ ⟦ ⟧, x ↦ ξ.a ⟧"] (Label (LabelId "x"))) (Just (RuleContext Nothing (Just "⟦ !a ↦ !obj, !B ⟧") (Just "!a"))) -- [Subst { -- objectMetas = [!obj -> 'ξ.a'] @@ -177,6 +194,9 @@ checkCond _ctx (AttrNotEqual (a1, a2)) subst = applySubstAttr subst a1 /= applyS checkCond ctx (ApplyInSubformations shouldApply) _subst | shouldApply = True | otherwise = not (insideFormation ctx) +checkCond ctx (ApplyInAbstractSubformations shouldApply) _subst + | shouldApply = True + | otherwise = not (insideAbstractFormation ctx) hasAttr :: RuleAttribute -> [Binding] -> Bool hasAttr attr = any (isAttr attr) diff --git a/eo-phi-normalizer/test/Language/EO/YamlSpec.hs b/eo-phi-normalizer/test/Language/EO/YamlSpec.hs index c28f86a1..30b6d80d 100644 --- a/eo-phi-normalizer/test/Language/EO/YamlSpec.hs +++ b/eo-phi-normalizer/test/Language/EO/YamlSpec.hs @@ -1,5 +1,4 @@ {-# LANGUAGE BlockArguments #-} -{-# LANGUAGE OverloadedLists #-} {-# LANGUAGE OverloadedRecordDot #-} module Language.EO.YamlSpec where @@ -12,14 +11,20 @@ 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 $ - let rule' = convertRuleNamed rule - resultOneStep = applyOneRule (defaultContext [rule'] ruleTest.input) ruleTest.input - expected = ruleTest.output - sameObjs objs1 objs2 = and ((length objs1 == length objs2) : zipWith equalObject objs2 objs1) - in map snd resultOneStep `shouldSatisfy` sameObjs expected + forM_ testPaths $ \path -> do + ruleset <- runIO $ fileTests path + describe ruleset.title do + forM_ ruleset.rules $ \rule -> do + describe rule.name do + forM_ rule.tests $ \ruleTest -> do + it ruleTest.name $ + let rule' = convertRuleNamed rule + resultOneStep = applyOneRule (defaultContext [rule'] ruleTest.input) ruleTest.input + expected = ruleTest.output + sameObjs objs1 objs2 = and ((length objs1 == length objs2) : zipWith equalObject objs2 objs1) + in map snd resultOneStep `shouldSatisfy` sameObjs expected + where + testPaths = + [ "test/eo/phi/rules/yegor.yaml" + , "test/eo/phi/rules/streams.yaml" + ] diff --git a/eo-phi-normalizer/test/eo/phi/rules/streams.yaml b/eo-phi-normalizer/test/eo/phi/rules/streams.yaml new file mode 100644 index 00000000..0eeac69c --- /dev/null +++ b/eo-phi-normalizer/test/eo/phi/rules/streams.yaml @@ -0,0 +1,57 @@ +title: "Rules for Java Streams" +rules: + - name: "[java.util.Stream] map ↦ for-each" + description: | + Replacing Java Stream's map with a for-each loop. + context: + pattern: | + ⟦ + !τ1 ↦ !b1.java_util_Stream$map(α0 ↦ !b2).!t1, + !B1 + ⟧ + result: | + ⟦ + !τ2 ↦ !b1, + !τ3 ↦ Φ.opeo.map-for-each( + α0 ↦ ξ.!τ2, + α1 ↦ !b2 + ), + !τ1 ↦ ξ.!τ3.!t1, + !B1 + ⟧ + fresh: + - '!τ2' + - '!τ3' + when: [] + tests: + - name: Simple map to for-each example works + input: | + ⟦ + list ↦ ∅, + result ↦ ξ.list.java_util_Stream$filter( + α0 ↦ ⟦ + el ↦ ∅, + φ ↦ ξ.el.equals( + α0 ↦ Φ.org.eolang.string(as-bytes ↦ Φ.org.eolang.bytes (Δ ⤍ 00-)) + ).not + ⟧ + ).java_util_Stream$map( + α0 ↦ ⟦ + el ↦ ∅, + φ ↦ Φ.java_util_Integer.parseInt( + α0 ↦ ξ.el + ) + ⟧ + ).java_util_Stream$toList + ⟧ + output: + - | + ⟦ + tmp_1 ↦ ξ.list.java_util_Stream$filter (α0 ↦ ⟦ + el ↦ ∅, φ ↦ ξ.el.equals (α0 ↦ Φ.org.eolang.string (as-bytes ↦ Φ.org.eolang.bytes (Δ ⤍ 00-))).not + ⟧), + tmp_2 ↦ Φ.opeo.map-for-each (α0 ↦ ξ.tmp_1, α1 ↦ ⟦ + el ↦ ∅, φ ↦ Φ.java_util_Integer.parseInt (α0 ↦ ξ.el) + ⟧), + result ↦ ξ.tmp_2.java_util_Stream$toList, list ↦ ∅ + ⟧ diff --git a/eo-phi-normalizer/test/eo/phi/rules/yegor.yaml b/eo-phi-normalizer/test/eo/phi/rules/yegor.yaml index 167919b3..0018fc03 100644 --- a/eo-phi-normalizer/test/eo/phi/rules/yegor.yaml +++ b/eo-phi-normalizer/test/eo/phi/rules/yegor.yaml @@ -62,6 +62,7 @@ rules: result: | !n[ ξ ↦ ⟦ !a ↦ !n, !B ⟧ ] when: + - apply_in_abstract_subformations: false - nf_inside_formation: '!n' - nf: '⟦ !B ⟧' tests: @@ -97,6 +98,7 @@ rules: result: | ⟦ !a ↦ !n0, !b ↦ !n1, !B ⟧ when: + - apply_in_abstract_subformations: false - nf: '!n0' - nf: '!n1' tests: [] @@ -111,6 +113,7 @@ rules: result: | ⟦ !a ↦ !n, !B ⟧ when: + - apply_in_abstract_subformations: false - nf: '!n' tests: [] @@ -121,6 +124,7 @@ rules: result: | ⟦ !a ↦ !n, !B ⟧ when: + - apply_in_abstract_subformations: false - nf: '!n' tests: [] @@ -130,7 +134,8 @@ rules: ⟦ Δ ⤍ ∅, !B ⟧(Δ ⤍ !bytes) result: | ⟦ Δ ⤍ !bytes, !B ⟧ - when: [] + when: + - apply_in_abstract_subformations: false tests: [] - name: R_φ From b20ae4dade7c2a41a30beb9c446820214a1e1ed5 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Fri, 12 Jul 2024 12:13:09 +0300 Subject: [PATCH 02/12] Add one-hole contexts --- eo-phi-normalizer/app/Main.hs | 1 + eo-phi-normalizer/grammar/EO/Phi/Syntax.cf | 1 + .../src/Language/EO/Phi/Normalize.hs | 1 + .../src/Language/EO/Phi/Rules/Common.hs | 2 + .../src/Language/EO/Phi/Rules/Fast.hs | 1 + .../src/Language/EO/Phi/Rules/Yaml.hs | 57 +++++++++++++++++-- .../src/Language/EO/Phi/Syntax/Abs.hs | 1 + .../src/Language/EO/Phi/Syntax/Doc.txt | 5 +- .../src/Language/EO/Phi/Syntax/Lex.x | 19 ++++--- .../src/Language/EO/Phi/Syntax/Par.y | 33 ++++++----- .../src/Language/EO/Phi/Syntax/Print.hs | 1 + .../src/Language/EO/Phi/ToLaTeX.hs | 1 + .../test/eo/phi/rules/streams.yaml | 4 +- 13 files changed, 95 insertions(+), 32 deletions(-) diff --git a/eo-phi-normalizer/app/Main.hs b/eo-phi-normalizer/app/Main.hs index b26cc9bf..c69c2187 100644 --- a/eo-phi-normalizer/app/Main.hs +++ b/eo-phi-normalizer/app/Main.hs @@ -428,6 +428,7 @@ wrapRawBytesIn = \case Termination -> wrapTermination obj@MetaSubstThis{} -> obj obj@MetaObject{} -> obj + obj@MetaOneHoleContext{} -> obj obj@MetaFunction{} -> obj -- * Main diff --git a/eo-phi-normalizer/grammar/EO/Phi/Syntax.cf b/eo-phi-normalizer/grammar/EO/Phi/Syntax.cf index 9235f12d..491fc556 100644 --- a/eo-phi-normalizer/grammar/EO/Phi/Syntax.cf +++ b/eo-phi-normalizer/grammar/EO/Phi/Syntax.cf @@ -24,6 +24,7 @@ ThisObject. Object ::= "ξ"; Termination. Object ::= "⊥" ; MetaSubstThis. Object ::= Object "[" "ξ" "↦" Object "]" ; MetaObject. Object ::= MetaId ; +MetaOneHoleContext. Object ::= MetaId "[1|" Object "|1]" ; MetaFunction. Object ::= MetaFunctionName "(" Object ")" ; AlphaBinding. Binding ::= Attribute "↦" Object ; diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs b/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs index a35b730e..31d579cf 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs +++ b/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs @@ -50,6 +50,7 @@ peelObject = \case ThisObject -> PeeledObject HeadThis [] Termination -> PeeledObject HeadTermination [] MetaObject _ -> PeeledObject HeadTermination [] + MetaOneHoleContext{} -> error "impossible" MetaFunction _ _ -> error "To be honest, I'm not sure what should be here" MetaSubstThis{} -> error "impossible" where 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 b97b678a..36291b49 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs +++ b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs @@ -135,6 +135,7 @@ withSubObject f ctx root = Termination -> [] MetaObject _ -> [] MetaFunction _ _ -> [] + MetaOneHoleContext _ _ -> [] MetaSubstThis _ _ -> [] where subctx = ctx{insideSubObject = True} @@ -203,6 +204,7 @@ objectSize = \case MetaObject{} -> 1 -- should be impossible MetaFunction{} -> 1 -- should be impossible MetaSubstThis{} -> 1 -- should be impossible + MetaOneHoleContext{} -> 1 -- should be impossible bindingSize :: Binding -> Int bindingSize = \case diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Fast.hs b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Fast.hs index 53ca558b..f05dc768 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Fast.hs +++ b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Fast.hs @@ -199,4 +199,5 @@ fastYegorInsideOut ctx = \case Termination -> Termination MetaSubstThis{} -> error "impossible MetaSubstThis!" MetaObject{} -> error "impossible MetaObject!" + MetaOneHoleContext{} -> error "impossible MetaOneHoleContext!" MetaFunction{} -> error "impossible MetaFunction!" 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 9561e278..718d5b91 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs +++ b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs @@ -10,6 +10,7 @@ {-# LANGUAGE TypeApplications #-} {-# OPTIONS_GHC -Wno-orphans #-} {-# OPTIONS_GHC -Wno-partial-fields #-} +{-# OPTIONS_GHC -Wno-type-defaults #-} module Language.EO.Phi.Rules.Yaml where @@ -113,15 +114,16 @@ convertRuleNamed :: Rule -> NamedRule convertRuleNamed rule = (rule.name, convertRule rule) mkFreshSubst :: Context -> Object -> Maybe [MetaId] -> Subst -mkFreshSubst ctx obj metas = +mkFreshSubst _ctx _obj metas = Subst { objectMetas = [] , bindingsMetas = [] , attributeMetas = zip (fromMaybe [] metas) (filter isFresh defaultFreshAttrs) , bytesMetas = [] + , contextMetas = [] } where - isFresh _ = True + isFresh _ = True -- FIXME: properly check for freshness defaultFreshAttrs :: [Attribute] defaultFreshAttrs = [Label (LabelId ("tmp_" <> show i)) | i <- [1 ..]] @@ -152,6 +154,7 @@ objectHasMetavars ThisObject = False objectHasMetavars Termination = False objectHasMetavars (MetaObject _) = True objectHasMetavars (MetaFunction _ _) = True +objectHasMetavars MetaOneHoleContext{} = True objectHasMetavars (MetaSubstThis _ _) = True -- technically not a metavar, but a substitution bindingHasMetavars :: Binding -> Bool @@ -221,11 +224,18 @@ hasAttr attr = any (isAttr attr) -- actual result (after applying substitution): -- ⟦ c ↦ ⟦ ⟧ ⟧(ρ ↦ ⟦ b ↦ ⟦ ⟧ ⟧) +data OneHoleContext = OneHoleContext + { holeMetaId :: !MetaId + , contextObject :: !Object + } + deriving (Show) + data Subst = Subst { objectMetas :: [(MetaId, Object)] , bindingsMetas :: [(MetaId, [Binding])] , attributeMetas :: [(MetaId, Attribute)] , bytesMetas :: [(MetaId, Bytes)] + , contextMetas :: [(MetaId, OneHoleContext)] } instance Show Subst where show Subst{..} = @@ -236,6 +246,7 @@ instance Show Subst where , " bindingsMetas = [" <> showMappings bindingsMetas <> "]" , " attributeMetas = [" <> showMappings attributeMetas <> "]" , " bytesMetas = [" <> showMappings bytesMetas <> "]" + , " contextMetas = [" <> show contextMetas <> "]" , "}" ] where @@ -248,7 +259,7 @@ instance Monoid Subst where mempty = emptySubst emptySubst :: Subst -emptySubst = Subst [] [] [] [] +emptySubst = Subst [] [] [] [] [] -- >>> putStrLn $ Language.EO.Phi.printTree (applySubst (Subst [("!n", "⟦ c ↦ ⟦ ⟧ ⟧")] [("!B", ["b ↦ ⟦ ⟧"])] [("!a", "a")]) "!n(ρ ↦ ⟦ !B ⟧)" :: Object) -- ⟦ c ↦ ⟦ ⟧ ⟧ (ρ ↦ ⟦ b ↦ ⟦ ⟧ ⟧) @@ -266,6 +277,12 @@ applySubst subst@Subst{..} = \case Termination -> Termination MetaSubstThis obj thisObj -> MetaSubstThis (applySubst subst thisObj) (applySubst subst obj) obj@MetaFunction{} -> obj + MetaOneHoleContext c obj -> + case lookup c contextMetas of + Nothing -> MetaOneHoleContext c (applySubst subst obj) + Just OneHoleContext{..} -> + let holeSubst = mempty{objectMetas = [(holeMetaId, applySubst subst obj)]} + in applySubst holeSubst contextObject applySubstAttr :: Subst -> Attribute -> Attribute applySubstAttr Subst{..} = \case @@ -288,8 +305,8 @@ applySubstBinding subst@Subst{..} = \case b@(MetaDeltaBinding m) -> maybe [b] (pure . DeltaBinding) (lookup m bytesMetas) mergeSubst :: Subst -> Subst -> Subst -mergeSubst (Subst xs ys zs ws) (Subst xs' ys' zs' ws') = - Subst (xs ++ xs') (ys ++ ys') (zs ++ zs') (ws ++ ws') +mergeSubst (Subst xs ys zs ws us) (Subst xs' ys' zs' ws' us') = + Subst (xs ++ xs') (ys ++ ys') (zs ++ zs') (ws ++ ws') (us ++ us') -- 1. need to implement applySubst' :: Subst -> Object -> Object -- 2. complete the code @@ -305,11 +322,40 @@ matchObject (ObjectDispatch pat a) (ObjectDispatch obj a') = do pure (subst1 <> subst2) matchObject (MetaObject m) obj = pure emptySubst{objectMetas = [(m, obj)]} +matchObject (MetaOneHoleContext x pat) obj = do + (subst@Subst{..}, matchedCtx) <- matchOneHoleContext x pat obj + return subst{contextMetas = contextMetas <> [(x, matchedCtx)]} matchObject Termination Termination = [emptySubst] matchObject ThisObject ThisObject = [emptySubst] matchObject GlobalObject GlobalObject = [emptySubst] matchObject _ _ = [] -- ? emptySubst ? +matchOneHoleContext :: MetaId -> Object -> Object -> [(Subst, OneHoleContext)] +matchOneHoleContext ctxId@(MetaId name) pat obj = matchWhole <> matchPart + where + holeId = MetaId (name ++ ":hole") -- FIXME: ensure fresh names + matchWhole = do + subst' <- matchObject pat obj + pure (subst', OneHoleContext holeId (MetaObject holeId)) + matchPart = case obj of + ObjectDispatch obj' a -> do + (subst, OneHoleContext{..}) <- matchOneHoleContext ctxId pat obj' + return (subst, OneHoleContext{contextObject = ObjectDispatch contextObject a, ..}) + -- FIXME: consider matching inside bindings of application as well + Application obj' bindings -> do + (subst, OneHoleContext{..}) <- matchOneHoleContext ctxId pat obj' + return (subst, OneHoleContext{contextObject = Application contextObject bindings, ..}) + -- cases below cannot be matched + Formation{} -> [] + GlobalObject -> [] + ThisObject -> [] + Termination -> [] + -- should cases below be errors? + MetaSubstThis{} -> [] + MetaObject{} -> [] + MetaOneHoleContext{} -> [] + MetaFunction{} -> [] + -- | Evaluate meta functions -- given top-level context as an object -- and an object @@ -410,6 +456,7 @@ substThis thisObj = go ObjectDispatch obj a -> ObjectDispatch (go obj) a GlobalObject -> GlobalObject Termination -> Termination + obj@MetaOneHoleContext{} -> error ("impossible: trying to substitute ξ in " <> printTree obj) obj@MetaSubstThis{} -> error ("impossible: trying to substitute ξ in " <> printTree obj) obj@MetaObject{} -> error ("impossible: trying to substitute ξ in " <> printTree obj) obj@MetaFunction{} -> error ("impossible: trying to substitute ξ in " <> printTree obj) diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Abs.hs b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Abs.hs index 02bcc9a2..e37133d7 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Abs.hs +++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Abs.hs @@ -27,6 +27,7 @@ data Object | Termination | MetaSubstThis Object Object | MetaObject MetaId + | MetaOneHoleContext MetaId Object | MetaFunction MetaFunctionName Object deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic) diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Doc.txt b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Doc.txt index 227b0e15..6102ffbf 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Doc.txt +++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Doc.txt @@ -51,8 +51,8 @@ The reserved words used in Syntax are the following: The symbols used in Syntax are the following: | { | ⟦ | ⟧ | } | ( | ) | . | ⊥ - | [ | ↦ | ] | ∅ - | ⤍ | , | | + | [ | ↦ | ] | [1| + | |1] | ∅ | ⤍ | , ===Comments=== Single-line comments begin with //.Multiple-line comments are enclosed with /* and */. @@ -72,6 +72,7 @@ All other symbols are terminals. | | **|** | ``⊥`` | | **|** | //Object// ``[`` ``ξ`` ``↦`` //Object// ``]`` | | **|** | //MetaId// + | | **|** | //MetaId// ``[1|`` //Object// ``|1]`` | | **|** | //MetaFunctionName// ``(`` //Object// ``)`` | //Binding// | -> | //Attribute// ``↦`` //Object// | | **|** | //Attribute// ``↦`` ``∅`` diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Lex.x b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Lex.x index 2257a1f6..bd20eba4 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Lex.x +++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Lex.x @@ -28,7 +28,7 @@ $u = [. \n] -- universal: any character -- Symbols and non-identifier-like reserved words -@rsyms = \Φ | \ξ | \Δ | \λ | \φ | \ρ | \{ | \⟦ | \⟧ | \} | \( | \) | \. | \⊥ | \[ | \↦ | \] | \∅ | \⤍ | \, +@rsyms = \Φ | \ξ | \Δ | \λ | \φ | \ρ | \{ | \⟦ | \⟧ | \} | \( | \) | \. | \⊥ | \[ | \↦ | \] | \[ "1" \| | \| "1" \] | \∅ | \⤍ | \, :- @@ -186,14 +186,17 @@ eitherResIdent tv s = treeFind resWords -- | The keywords and symbols of the language organized as binary search tree. resWords :: BTree resWords = - b "\955" 11 - (b "]" 6 + b "\934" 12 + (b "[1|" 6 (b "," 3 (b ")" 2 (b "(" 1 N N) N) (b "[" 5 (b "." 4 N N) N)) - (b "\916" 9 (b "}" 8 (b "{" 7 N N) N) (b "\934" 10 N N))) - (b "\8709" 16 - (b "\966" 14 (b "\961" 13 (b "\958" 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))) + (b "|1]" 9 + (b "{" 8 (b "]" 7 N N) N) (b "\916" 11 (b "}" 10 N N) N))) + (b "\8709" 18 + (b "\961" 15 + (b "\958" 14 (b "\955" 13 N N) N) + (b "\8614" 17 (b "\966" 16 N N) N)) + (b "\10215" 21 + (b "\10214" 20 (b "\8869" 19 N N) N) (b "\10509" 22 N N))) where b s n = B bs (TS bs n) where diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Par.y b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Par.y index a660fb01..3b69ca07 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Par.y +++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Par.y @@ -46,21 +46,23 @@ import Language.EO.Phi.Syntax.Lex ',' { 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) } + '[1|' { PT _ (TS _ 6) } + ']' { PT _ (TS _ 7) } + '{' { PT _ (TS _ 8) } + '|1]' { 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) } + '⟧' { PT _ (TS _ 21) } + '⤍' { PT _ (TS _ 22) } L_Bytes { PT _ (T_Bytes $$) } L_Function { PT _ (T_Function $$) } L_LabelId { PT _ (T_LabelId $$) } @@ -102,6 +104,7 @@ Object | '⊥' { Language.EO.Phi.Syntax.Abs.Termination } | Object '[' 'ξ' '↦' Object ']' { Language.EO.Phi.Syntax.Abs.MetaSubstThis $1 $5 } | MetaId { Language.EO.Phi.Syntax.Abs.MetaObject $1 } + | MetaId '[1|' Object '|1]' { Language.EO.Phi.Syntax.Abs.MetaOneHoleContext $1 $3 } | MetaFunctionName '(' Object ')' { Language.EO.Phi.Syntax.Abs.MetaFunction $1 $3 } Binding :: { Language.EO.Phi.Syntax.Abs.Binding } diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Print.hs b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Print.hs index d0060dcb..92900459 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Print.hs +++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Print.hs @@ -163,6 +163,7 @@ instance Print Language.EO.Phi.Syntax.Abs.Object where Language.EO.Phi.Syntax.Abs.Termination -> prPrec i 0 (concatD [doc (showString "\8869")]) Language.EO.Phi.Syntax.Abs.MetaSubstThis object1 object2 -> prPrec i 0 (concatD [prt 0 object1, doc (showString "["), doc (showString "\958"), doc (showString "\8614"), prt 0 object2, doc (showString "]")]) Language.EO.Phi.Syntax.Abs.MetaObject metaid -> prPrec i 0 (concatD [prt 0 metaid]) + Language.EO.Phi.Syntax.Abs.MetaOneHoleContext metaid object -> prPrec i 0 (concatD [prt 0 metaid, doc (showString "[1|"), prt 0 object, doc (showString "|1]")]) Language.EO.Phi.Syntax.Abs.MetaFunction metafunctionname object -> prPrec i 0 (concatD [prt 0 metafunctionname, doc (showString "("), prt 0 object, doc (showString ")")]) instance Print Language.EO.Phi.Syntax.Abs.Binding where diff --git a/eo-phi-normalizer/src/Language/EO/Phi/ToLaTeX.hs b/eo-phi-normalizer/src/Language/EO/Phi/ToLaTeX.hs index 1968926e..0e07e7f3 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/ToLaTeX.hs +++ b/eo-phi-normalizer/src/Language/EO/Phi/ToLaTeX.hs @@ -53,6 +53,7 @@ instance ToLatex Object where toLatex ThisObject = "$" toLatex Termination = "\\dead" toLatex (MetaObject _) = error "rendering MetaObject in LaTex format" + toLatex MetaOneHoleContext{} = error "rendering MetaObject in LaTex format" toLatex (MetaFunction _ _) = error "rendering MetaFunction in LaTex format" toLatex (MetaSubstThis _ _) = error "rendering MetaSubstThis in LaTex format" diff --git a/eo-phi-normalizer/test/eo/phi/rules/streams.yaml b/eo-phi-normalizer/test/eo/phi/rules/streams.yaml index 0eeac69c..a8086866 100644 --- a/eo-phi-normalizer/test/eo/phi/rules/streams.yaml +++ b/eo-phi-normalizer/test/eo/phi/rules/streams.yaml @@ -6,7 +6,7 @@ rules: context: pattern: | ⟦ - !τ1 ↦ !b1.java_util_Stream$map(α0 ↦ !b2).!t1, + !τ1 ↦ !C1 [1| !b1.java_util_Stream$map(α0 ↦ !b2) |1], !B1 ⟧ result: | @@ -16,7 +16,7 @@ rules: α0 ↦ ξ.!τ2, α1 ↦ !b2 ), - !τ1 ↦ ξ.!τ3.!t1, + !τ1 ↦ !C1 [1| ξ.!τ3 |1], !B1 ⟧ fresh: From 3afa999e8e6b6f7c38c05ac37ce5c03bf521463e Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Fri, 12 Jul 2024 12:27:02 +0300 Subject: [PATCH 03/12] Make YamlSpec stricter, but with better error messages --- eo-phi-normalizer/test/Language/EO/YamlSpec.hs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/eo-phi-normalizer/test/Language/EO/YamlSpec.hs b/eo-phi-normalizer/test/Language/EO/YamlSpec.hs index 30b6d80d..0599b40d 100644 --- a/eo-phi-normalizer/test/Language/EO/YamlSpec.hs +++ b/eo-phi-normalizer/test/Language/EO/YamlSpec.hs @@ -21,8 +21,7 @@ spec = describe "User-defined rules unit tests" do let rule' = convertRuleNamed rule resultOneStep = applyOneRule (defaultContext [rule'] ruleTest.input) ruleTest.input expected = ruleTest.output - sameObjs objs1 objs2 = and ((length objs1 == length objs2) : zipWith equalObject objs2 objs1) - in map snd resultOneStep `shouldSatisfy` sameObjs expected + in map snd resultOneStep `shouldBe` expected where testPaths = [ "test/eo/phi/rules/yegor.yaml" From ed1439564d0c8de96afe9440b84105be07c8a065 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Fri, 12 Jul 2024 12:27:30 +0300 Subject: [PATCH 04/12] Allow user-defined prefix for fresh attirbute names --- .../src/Language/EO/Phi/Rules/Yaml.hs | 19 ++++++++++++------- .../test/eo/phi/rules/streams.yaml | 12 +++++++----- 2 files changed, 19 insertions(+), 12 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 718d5b91..e0f43b26 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs +++ b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs @@ -63,12 +63,18 @@ data Rule = Rule , context :: Maybe RuleContext , pattern :: Object , result :: Object - , fresh :: Maybe [MetaId] + , fresh :: Maybe [FreshMetaId] , when :: [Condition] , tests :: [RuleTest] } deriving (Generic, FromJSON, Show) +data FreshMetaId = FreshMetaId + { name :: MetaId + , prefix :: Maybe String + } + deriving (Generic, FromJSON, Show) + data RuleTest = RuleTest { name :: String , input :: Object @@ -113,20 +119,19 @@ convertRule Rule{..} ctx obj = do convertRuleNamed :: Rule -> NamedRule convertRuleNamed rule = (rule.name, convertRule rule) -mkFreshSubst :: Context -> Object -> Maybe [MetaId] -> Subst +mkFreshSubst :: Context -> Object -> Maybe [FreshMetaId] -> Subst mkFreshSubst _ctx _obj metas = Subst { objectMetas = [] , bindingsMetas = [] - , attributeMetas = zip (fromMaybe [] metas) (filter isFresh defaultFreshAttrs) + , attributeMetas = zipWith mkFresh (fromMaybe [] metas) [1 ..] , bytesMetas = [] , contextMetas = [] } where - isFresh _ = True -- FIXME: properly check for freshness - -defaultFreshAttrs :: [Attribute] -defaultFreshAttrs = [Label (LabelId ("tmp_" <> show i)) | i <- [1 ..]] + mkFresh FreshMetaId{..} i = (name, Label (LabelId label)) + where + label = fromMaybe "tmp_" prefix <> "$fresh$" <> show i -- >>> matchContext (Context [] ["⟦ a ↦ ⟦ ⟧, x ↦ ξ.a ⟧"] (Label (LabelId "x"))) (Just (RuleContext Nothing (Just "⟦ !a ↦ !obj, !B ⟧") (Just "!a"))) -- [Subst { diff --git a/eo-phi-normalizer/test/eo/phi/rules/streams.yaml b/eo-phi-normalizer/test/eo/phi/rules/streams.yaml index a8086866..b58559fd 100644 --- a/eo-phi-normalizer/test/eo/phi/rules/streams.yaml +++ b/eo-phi-normalizer/test/eo/phi/rules/streams.yaml @@ -20,8 +20,10 @@ rules: !B1 ⟧ fresh: - - '!τ2' - - '!τ3' + - name: '!τ2' + prefix: 'foreach_body' + - name: '!τ3' + prefix: 'java_util_Stream$map_result' when: [] tests: - name: Simple map to for-each example works @@ -47,11 +49,11 @@ rules: output: - | ⟦ - tmp_1 ↦ ξ.list.java_util_Stream$filter (α0 ↦ ⟦ + foreach_body$fresh$1 ↦ ξ.list.java_util_Stream$filter (α0 ↦ ⟦ el ↦ ∅, φ ↦ ξ.el.equals (α0 ↦ Φ.org.eolang.string (as-bytes ↦ Φ.org.eolang.bytes (Δ ⤍ 00-))).not ⟧), - tmp_2 ↦ Φ.opeo.map-for-each (α0 ↦ ξ.tmp_1, α1 ↦ ⟦ + java_util_Stream$map_result$fresh$2 ↦ Φ.opeo.map-for-each (α0 ↦ ξ.foreach_body$fresh$1, α1 ↦ ⟦ el ↦ ∅, φ ↦ Φ.java_util_Integer.parseInt (α0 ↦ ξ.el) ⟧), - result ↦ ξ.tmp_2.java_util_Stream$toList, list ↦ ∅ + result ↦ ξ.java_util_Stream$map_result$fresh$2.java_util_Stream$toList, list ↦ ∅ ⟧ From ff2301c71704fc09874af17ef43816e19938ba87 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Fri, 12 Jul 2024 12:58:38 +0300 Subject: [PATCH 05/12] Fix warning --- eo-phi-normalizer/test/Language/EO/YamlSpec.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/eo-phi-normalizer/test/Language/EO/YamlSpec.hs b/eo-phi-normalizer/test/Language/EO/YamlSpec.hs index 0599b40d..2d193174 100644 --- a/eo-phi-normalizer/test/Language/EO/YamlSpec.hs +++ b/eo-phi-normalizer/test/Language/EO/YamlSpec.hs @@ -4,7 +4,7 @@ module Language.EO.YamlSpec where import Control.Monad (forM_) -import Language.EO.Phi.Rules.Common (applyOneRule, defaultContext, equalObject) +import Language.EO.Phi.Rules.Common (applyOneRule, defaultContext) import Language.EO.Phi.Rules.Yaml (Rule (..), RuleSet (..), RuleTest (..), convertRuleNamed) import Test.EO.Yaml import Test.Hspec From eb365d5aa10cc03d015bbb65609dcc3e84721035 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" Date: Fri, 12 Jul 2024 10:05:07 +0000 Subject: [PATCH 06/12] Update normalizer data files --- eo-phi-normalizer/data/0.38.0/org/eolang/int.phi | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/eo-phi-normalizer/data/0.38.0/org/eolang/int.phi b/eo-phi-normalizer/data/0.38.0/org/eolang/int.phi index 3e55b241..e03ff429 100644 --- a/eo-phi-normalizer/data/0.38.0/org/eolang/int.phi +++ b/eo-phi-normalizer/data/0.38.0/org/eolang/int.phi @@ -83,4 +83,4 @@ λ ⤍ Package ⟧ ⟧ -} +} \ No newline at end of file From 8a350c03114c2887352dc27902be82c865edcfec Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Fri, 19 Jul 2024 08:30:27 +0300 Subject: [PATCH 07/12] Use tail syntax --- eo-phi-normalizer/app/Main.hs | 2 +- eo-phi-normalizer/grammar/EO/Phi/Syntax.cf | 2 +- .../src/Language/EO/Phi/Normalize.hs | 2 +- .../src/Language/EO/Phi/Rules/Common.hs | 4 +- .../src/Language/EO/Phi/Rules/Fast.hs | 2 +- .../src/Language/EO/Phi/Rules/Yaml.hs | 12 +- .../src/Language/EO/Phi/Syntax/Abs.hs | 2 +- .../src/Language/EO/Phi/Syntax/Doc.txt | 214 +++++++++--------- .../src/Language/EO/Phi/Syntax/Lex.x | 23 +- .../src/Language/EO/Phi/Syntax/Par.y | 37 ++- .../src/Language/EO/Phi/Syntax/Print.hs | 2 +- .../src/Language/EO/Phi/ToLaTeX.hs | 2 +- .../test/eo/phi/rules/streams.yaml | 4 +- 13 files changed, 153 insertions(+), 155 deletions(-) diff --git a/eo-phi-normalizer/app/Main.hs b/eo-phi-normalizer/app/Main.hs index c69c2187..362407b8 100644 --- a/eo-phi-normalizer/app/Main.hs +++ b/eo-phi-normalizer/app/Main.hs @@ -428,7 +428,7 @@ wrapRawBytesIn = \case Termination -> wrapTermination obj@MetaSubstThis{} -> obj obj@MetaObject{} -> obj - obj@MetaOneHoleContext{} -> obj + obj@MetaTailContext{} -> obj obj@MetaFunction{} -> obj -- * Main diff --git a/eo-phi-normalizer/grammar/EO/Phi/Syntax.cf b/eo-phi-normalizer/grammar/EO/Phi/Syntax.cf index 491fc556..23ff3a72 100644 --- a/eo-phi-normalizer/grammar/EO/Phi/Syntax.cf +++ b/eo-phi-normalizer/grammar/EO/Phi/Syntax.cf @@ -24,7 +24,7 @@ ThisObject. Object ::= "ξ"; Termination. Object ::= "⊥" ; MetaSubstThis. Object ::= Object "[" "ξ" "↦" Object "]" ; MetaObject. Object ::= MetaId ; -MetaOneHoleContext. Object ::= MetaId "[1|" Object "|1]" ; +MetaTailContext. Object ::= Object "*" MetaId ; MetaFunction. Object ::= MetaFunctionName "(" Object ")" ; AlphaBinding. Binding ::= Attribute "↦" Object ; diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs b/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs index 31d579cf..7328dbb1 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs +++ b/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs @@ -50,7 +50,7 @@ peelObject = \case ThisObject -> PeeledObject HeadThis [] Termination -> PeeledObject HeadTermination [] MetaObject _ -> PeeledObject HeadTermination [] - MetaOneHoleContext{} -> error "impossible" + MetaTailContext{} -> error "impossible" MetaFunction _ _ -> error "To be honest, I'm not sure what should be here" MetaSubstThis{} -> error "impossible" where 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 36291b49..aa4da39c 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs +++ b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs @@ -135,7 +135,7 @@ withSubObject f ctx root = Termination -> [] MetaObject _ -> [] MetaFunction _ _ -> [] - MetaOneHoleContext _ _ -> [] + MetaTailContext{} -> [] MetaSubstThis _ _ -> [] where subctx = ctx{insideSubObject = True} @@ -204,7 +204,7 @@ objectSize = \case MetaObject{} -> 1 -- should be impossible MetaFunction{} -> 1 -- should be impossible MetaSubstThis{} -> 1 -- should be impossible - MetaOneHoleContext{} -> 1 -- should be impossible + MetaTailContext{} -> 1 -- should be impossible bindingSize :: Binding -> Int bindingSize = \case diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Fast.hs b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Fast.hs index f05dc768..18ff7615 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Fast.hs +++ b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Fast.hs @@ -199,5 +199,5 @@ fastYegorInsideOut ctx = \case Termination -> Termination MetaSubstThis{} -> error "impossible MetaSubstThis!" MetaObject{} -> error "impossible MetaObject!" - MetaOneHoleContext{} -> error "impossible MetaOneHoleContext!" + MetaTailContext{} -> error "impossible MetaTailContext!" MetaFunction{} -> error "impossible MetaFunction!" 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 e0f43b26..a105cd17 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs +++ b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs @@ -159,7 +159,7 @@ objectHasMetavars ThisObject = False objectHasMetavars Termination = False objectHasMetavars (MetaObject _) = True objectHasMetavars (MetaFunction _ _) = True -objectHasMetavars MetaOneHoleContext{} = True +objectHasMetavars MetaTailContext{} = True objectHasMetavars (MetaSubstThis _ _) = True -- technically not a metavar, but a substitution bindingHasMetavars :: Binding -> Bool @@ -282,9 +282,9 @@ applySubst subst@Subst{..} = \case Termination -> Termination MetaSubstThis obj thisObj -> MetaSubstThis (applySubst subst thisObj) (applySubst subst obj) obj@MetaFunction{} -> obj - MetaOneHoleContext c obj -> + MetaTailContext obj c -> case lookup c contextMetas of - Nothing -> MetaOneHoleContext c (applySubst subst obj) + Nothing -> MetaTailContext (applySubst subst obj) c Just OneHoleContext{..} -> let holeSubst = mempty{objectMetas = [(holeMetaId, applySubst subst obj)]} in applySubst holeSubst contextObject @@ -327,7 +327,7 @@ matchObject (ObjectDispatch pat a) (ObjectDispatch obj a') = do pure (subst1 <> subst2) matchObject (MetaObject m) obj = pure emptySubst{objectMetas = [(m, obj)]} -matchObject (MetaOneHoleContext x pat) obj = do +matchObject (MetaTailContext pat x) obj = do (subst@Subst{..}, matchedCtx) <- matchOneHoleContext x pat obj return subst{contextMetas = contextMetas <> [(x, matchedCtx)]} matchObject Termination Termination = [emptySubst] @@ -358,7 +358,7 @@ matchOneHoleContext ctxId@(MetaId name) pat obj = matchWhole <> matchPart -- should cases below be errors? MetaSubstThis{} -> [] MetaObject{} -> [] - MetaOneHoleContext{} -> [] + MetaTailContext{} -> [] MetaFunction{} -> [] -- | Evaluate meta functions @@ -461,7 +461,7 @@ substThis thisObj = go ObjectDispatch obj a -> ObjectDispatch (go obj) a GlobalObject -> GlobalObject Termination -> Termination - obj@MetaOneHoleContext{} -> error ("impossible: trying to substitute ξ in " <> printTree obj) + obj@MetaTailContext{} -> error ("impossible: trying to substitute ξ in " <> printTree obj) obj@MetaSubstThis{} -> error ("impossible: trying to substitute ξ in " <> printTree obj) obj@MetaObject{} -> error ("impossible: trying to substitute ξ in " <> printTree obj) obj@MetaFunction{} -> error ("impossible: trying to substitute ξ in " <> printTree obj) diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Abs.hs b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Abs.hs index e37133d7..b3387182 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Abs.hs +++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Abs.hs @@ -27,7 +27,7 @@ data Object | Termination | MetaSubstThis Object Object | MetaObject MetaId - | MetaOneHoleContext MetaId Object + | MetaTailContext Object MetaId | MetaFunction MetaFunctionName Object deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic) diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Doc.txt b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Doc.txt index 6102ffbf..bc1a3677 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Doc.txt +++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Doc.txt @@ -1,107 +1,107 @@ -The Language Syntax -BNF Converter - - -%Process by txt2tags to generate html or latex - - - -This document was automatically generated by the //BNF-Converter//. It was generated together with the lexer, the parser, and the abstract syntax module, which guarantees that the document matches with the implementation of the language (provided no hand-hacking has taken place). - -==The lexical structure of Syntax== - -===Literals=== - - - - - - - -Bytes literals are recognized by the regular expression -`````{"--"} | ["0123456789ABCDEF"] ["0123456789ABCDEF"] '-' | ["0123456789ABCDEF"] ["0123456789ABCDEF"] ('-' ["0123456789ABCDEF"] ["0123456789ABCDEF"])+````` - -Function literals are recognized by the regular expression -`````upper (char - [" - !'(),-.:;?[]{|}⟦⟧"])*````` - -LabelId literals are recognized by the regular expression -`````lower (char - [" - !'(),.:;?[]{|}⟦⟧"])*````` - -AlphaIndex literals are recognized by the regular expression -`````{"α0"} | 'α' (digit - '0') digit*````` - -MetaId literals are recognized by the regular expression -`````'!' (char - [" - !'(),-.:;?[]{|}⟦⟧"])*````` - -MetaFunctionName literals are recognized by the regular expression -`````'@' (char - [" - !'(),-.:;?[]{|}⟦⟧"])*````` - - -===Reserved words and symbols=== -The set of reserved words is the set of terminals appearing in the grammar. Those reserved words that consist of non-letter characters are called symbols, and they are treated in a different way from those that are similar to identifiers. The lexer follows rules familiar from languages like Haskell, C, and Java, including longest match and spacing conventions. - -The reserved words used in Syntax are the following: - | ``Δ`` | ``Φ`` | ``λ`` | ``ξ`` - | ``ρ`` | ``φ`` | | - -The symbols used in Syntax are the following: - | { | ⟦ | ⟧ | } - | ( | ) | . | ⊥ - | [ | ↦ | ] | [1| - | |1] | ∅ | ⤍ | , - -===Comments=== -Single-line comments begin with //.Multiple-line comments are enclosed with /* and */. - -==The syntactic structure of Syntax== -Non-terminals are enclosed between < and >. -The symbols -> (production), **|** (union) -and **eps** (empty rule) belong to the BNF notation. -All other symbols are terminals. - - | //Program// | -> | ``{`` ``⟦`` //[Binding]// ``⟧`` ``}`` - | //Object// | -> | ``⟦`` //[Binding]// ``⟧`` - | | **|** | //Object// ``(`` //[Binding]// ``)`` - | | **|** | //Object// ``.`` //Attribute// - | | **|** | ``Φ`` - | | **|** | ``ξ`` - | | **|** | ``⊥`` - | | **|** | //Object// ``[`` ``ξ`` ``↦`` //Object// ``]`` - | | **|** | //MetaId// - | | **|** | //MetaId// ``[1|`` //Object// ``|1]`` - | | **|** | //MetaFunctionName// ``(`` //Object// ``)`` - | //Binding// | -> | //Attribute// ``↦`` //Object// - | | **|** | //Attribute// ``↦`` ``∅`` - | | **|** | ``Δ`` ``⤍`` //Bytes// - | | **|** | ``Δ`` ``⤍`` ``∅`` - | | **|** | ``λ`` ``⤍`` //Function// - | | **|** | //MetaId// - | | **|** | ``Δ`` ``⤍`` //MetaId// - | //[Binding]// | -> | **eps** - | | **|** | //Binding// - | | **|** | //Binding// ``,`` //[Binding]// - | //Attribute// | -> | ``φ`` - | | **|** | ``ρ`` - | | **|** | //LabelId// - | | **|** | //AlphaIndex// - | | **|** | //MetaId// - | //RuleAttribute// | -> | //Attribute// - | | **|** | ``Δ`` - | | **|** | ``λ`` - | //PeeledObject// | -> | //ObjectHead// //[ObjectAction]// - | //ObjectHead// | -> | ``⟦`` //[Binding]// ``⟧`` - | | **|** | ``Φ`` - | | **|** | ``ξ`` - | | **|** | ``⊥`` - | //ObjectAction// | -> | ``(`` //[Binding]// ``)`` - | | **|** | ``.`` //Attribute// - | //[ObjectAction]// | -> | **eps** - | | **|** | //ObjectAction// //[ObjectAction]// - - - -%% File generated by the BNF Converter (bnfc 2.9.5). +The Language Syntax +BNF Converter + + +%Process by txt2tags to generate html or latex + + + +This document was automatically generated by the //BNF-Converter//. It was generated together with the lexer, the parser, and the abstract syntax module, which guarantees that the document matches with the implementation of the language (provided no hand-hacking has taken place). + +==The lexical structure of Syntax== + +===Literals=== + + + + + + + +Bytes literals are recognized by the regular expression +`````{"--"} | ["0123456789ABCDEF"] ["0123456789ABCDEF"] '-' | ["0123456789ABCDEF"] ["0123456789ABCDEF"] ('-' ["0123456789ABCDEF"] ["0123456789ABCDEF"])+````` + +Function literals are recognized by the regular expression +`````upper (char - [" + !'(),-.:;?[]{|}⟦⟧"])*````` + +LabelId literals are recognized by the regular expression +`````lower (char - [" + !'(),.:;?[]{|}⟦⟧"])*````` + +AlphaIndex literals are recognized by the regular expression +`````{"α0"} | 'α' (digit - '0') digit*````` + +MetaId literals are recognized by the regular expression +`````'!' (char - [" + !'(),-.:;?[]{|}⟦⟧"])*````` + +MetaFunctionName literals are recognized by the regular expression +`````'@' (char - [" + !'(),-.:;?[]{|}⟦⟧"])*````` + + +===Reserved words and symbols=== +The set of reserved words is the set of terminals appearing in the grammar. Those reserved words that consist of non-letter characters are called symbols, and they are treated in a different way from those that are similar to identifiers. The lexer follows rules familiar from languages like Haskell, C, and Java, including longest match and spacing conventions. + +The reserved words used in Syntax are the following: + | ``Δ`` | ``Φ`` | ``λ`` | ``ξ`` + | ``ρ`` | ``φ`` | | + +The symbols used in Syntax are the following: + | { | ⟦ | ⟧ | } + | ( | ) | . | ⊥ + | [ | ↦ | ] | * + | ∅ | ⤍ | , | + +===Comments=== +Single-line comments begin with //.Multiple-line comments are enclosed with /* and */. + +==The syntactic structure of Syntax== +Non-terminals are enclosed between < and >. +The symbols -> (production), **|** (union) +and **eps** (empty rule) belong to the BNF notation. +All other symbols are terminals. + + | //Program// | -> | ``{`` ``⟦`` //[Binding]// ``⟧`` ``}`` + | //Object// | -> | ``⟦`` //[Binding]// ``⟧`` + | | **|** | //Object// ``(`` //[Binding]// ``)`` + | | **|** | //Object// ``.`` //Attribute// + | | **|** | ``Φ`` + | | **|** | ``ξ`` + | | **|** | ``⊥`` + | | **|** | //Object// ``[`` ``ξ`` ``↦`` //Object// ``]`` + | | **|** | //MetaId// + | | **|** | //Object// ``*`` //MetaId// + | | **|** | //MetaFunctionName// ``(`` //Object// ``)`` + | //Binding// | -> | //Attribute// ``↦`` //Object// + | | **|** | //Attribute// ``↦`` ``∅`` + | | **|** | ``Δ`` ``⤍`` //Bytes// + | | **|** | ``Δ`` ``⤍`` ``∅`` + | | **|** | ``λ`` ``⤍`` //Function// + | | **|** | //MetaId// + | | **|** | ``Δ`` ``⤍`` //MetaId// + | //[Binding]// | -> | **eps** + | | **|** | //Binding// + | | **|** | //Binding// ``,`` //[Binding]// + | //Attribute// | -> | ``φ`` + | | **|** | ``ρ`` + | | **|** | //LabelId// + | | **|** | //AlphaIndex// + | | **|** | //MetaId// + | //RuleAttribute// | -> | //Attribute// + | | **|** | ``Δ`` + | | **|** | ``λ`` + | //PeeledObject// | -> | //ObjectHead// //[ObjectAction]// + | //ObjectHead// | -> | ``⟦`` //[Binding]// ``⟧`` + | | **|** | ``Φ`` + | | **|** | ``ξ`` + | | **|** | ``⊥`` + | //ObjectAction// | -> | ``(`` //[Binding]// ``)`` + | | **|** | ``.`` //Attribute// + | //[ObjectAction]// | -> | **eps** + | | **|** | //ObjectAction// //[ObjectAction]// + + + +%% File generated by the BNF Converter (bnfc 2.9.5). diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Lex.x b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Lex.x index bd20eba4..4119d8e5 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Lex.x +++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Lex.x @@ -28,7 +28,7 @@ $u = [. \n] -- universal: any character -- Symbols and non-identifier-like reserved words -@rsyms = \Φ | \ξ | \Δ | \λ | \φ | \ρ | \{ | \⟦ | \⟧ | \} | \( | \) | \. | \⊥ | \[ | \↦ | \] | \[ "1" \| | \| "1" \] | \∅ | \⤍ | \, +@rsyms = \Φ | \ξ | \Δ | \λ | \φ | \ρ | \{ | \⟦ | \⟧ | \} | \( | \) | \. | \⊥ | \[ | \↦ | \] | \* | \∅ | \⤍ | \, :- @@ -186,17 +186,16 @@ eitherResIdent tv s = treeFind resWords -- | The keywords and symbols of the language organized as binary search tree. resWords :: BTree resWords = - b "\934" 12 - (b "[1|" 6 - (b "," 3 (b ")" 2 (b "(" 1 N N) N) (b "[" 5 (b "." 4 N N) N)) - (b "|1]" 9 - (b "{" 8 (b "]" 7 N N) N) (b "\916" 11 (b "}" 10 N N) N))) - (b "\8709" 18 - (b "\961" 15 - (b "\958" 14 (b "\955" 13 N N) N) - (b "\8614" 17 (b "\966" 16 N N) N)) - (b "\10215" 21 - (b "\10214" 20 (b "\8869" 19 N N) N) (b "\10509" 22 N N))) + b "\934" 11 + (b "[" 6 + (b "*" 3 (b ")" 2 (b "(" 1 N N) N) (b "." 5 (b "," 4 N N) N)) + (b "}" 9 (b "{" 8 (b "]" 7 N N) N) (b "\916" 10 N N))) + (b "\8709" 17 + (b "\961" 14 + (b "\958" 13 (b "\955" 12 N N) N) + (b "\8614" 16 (b "\966" 15 N N) N)) + (b "\10215" 20 + (b "\10214" 19 (b "\8869" 18 N N) N) (b "\10509" 21 N N))) where b s n = B bs (TS bs n) where diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Par.y b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Par.y index 3b69ca07..5e45abc4 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Par.y +++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Par.y @@ -43,26 +43,25 @@ import Language.EO.Phi.Syntax.Lex %token '(' { PT _ (TS _ 1) } ')' { PT _ (TS _ 2) } - ',' { PT _ (TS _ 3) } - '.' { PT _ (TS _ 4) } - '[' { PT _ (TS _ 5) } - '[1|' { PT _ (TS _ 6) } + '*' { PT _ (TS _ 3) } + ',' { PT _ (TS _ 4) } + '.' { PT _ (TS _ 5) } + '[' { PT _ (TS _ 6) } ']' { PT _ (TS _ 7) } '{' { PT _ (TS _ 8) } - '|1]' { 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) } - '⟧' { PT _ (TS _ 21) } - '⤍' { PT _ (TS _ 22) } + '}' { 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) } + '⤍' { PT _ (TS _ 21) } L_Bytes { PT _ (T_Bytes $$) } L_Function { PT _ (T_Function $$) } L_LabelId { PT _ (T_LabelId $$) } @@ -104,7 +103,7 @@ Object | '⊥' { Language.EO.Phi.Syntax.Abs.Termination } | Object '[' 'ξ' '↦' Object ']' { Language.EO.Phi.Syntax.Abs.MetaSubstThis $1 $5 } | MetaId { Language.EO.Phi.Syntax.Abs.MetaObject $1 } - | MetaId '[1|' Object '|1]' { Language.EO.Phi.Syntax.Abs.MetaOneHoleContext $1 $3 } + | Object '*' MetaId { Language.EO.Phi.Syntax.Abs.MetaTailContext $1 $3 } | MetaFunctionName '(' Object ')' { Language.EO.Phi.Syntax.Abs.MetaFunction $1 $3 } Binding :: { Language.EO.Phi.Syntax.Abs.Binding } diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Print.hs b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Print.hs index 92900459..98c729fd 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Print.hs +++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Print.hs @@ -163,7 +163,7 @@ instance Print Language.EO.Phi.Syntax.Abs.Object where Language.EO.Phi.Syntax.Abs.Termination -> prPrec i 0 (concatD [doc (showString "\8869")]) Language.EO.Phi.Syntax.Abs.MetaSubstThis object1 object2 -> prPrec i 0 (concatD [prt 0 object1, doc (showString "["), doc (showString "\958"), doc (showString "\8614"), prt 0 object2, doc (showString "]")]) Language.EO.Phi.Syntax.Abs.MetaObject metaid -> prPrec i 0 (concatD [prt 0 metaid]) - Language.EO.Phi.Syntax.Abs.MetaOneHoleContext metaid object -> prPrec i 0 (concatD [prt 0 metaid, doc (showString "[1|"), prt 0 object, doc (showString "|1]")]) + Language.EO.Phi.Syntax.Abs.MetaTailContext object metaid -> prPrec i 0 (concatD [prt 0 object, doc (showString "*"), prt 0 metaid]) Language.EO.Phi.Syntax.Abs.MetaFunction metafunctionname object -> prPrec i 0 (concatD [prt 0 metafunctionname, doc (showString "("), prt 0 object, doc (showString ")")]) instance Print Language.EO.Phi.Syntax.Abs.Binding where diff --git a/eo-phi-normalizer/src/Language/EO/Phi/ToLaTeX.hs b/eo-phi-normalizer/src/Language/EO/Phi/ToLaTeX.hs index 0e07e7f3..7c94b06e 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/ToLaTeX.hs +++ b/eo-phi-normalizer/src/Language/EO/Phi/ToLaTeX.hs @@ -53,7 +53,7 @@ instance ToLatex Object where toLatex ThisObject = "$" toLatex Termination = "\\dead" toLatex (MetaObject _) = error "rendering MetaObject in LaTex format" - toLatex MetaOneHoleContext{} = error "rendering MetaObject in LaTex format" + toLatex MetaTailContext{} = error "rendering MetaTailContext in LaTex format" toLatex (MetaFunction _ _) = error "rendering MetaFunction in LaTex format" toLatex (MetaSubstThis _ _) = error "rendering MetaSubstThis in LaTex format" diff --git a/eo-phi-normalizer/test/eo/phi/rules/streams.yaml b/eo-phi-normalizer/test/eo/phi/rules/streams.yaml index b58559fd..b968f042 100644 --- a/eo-phi-normalizer/test/eo/phi/rules/streams.yaml +++ b/eo-phi-normalizer/test/eo/phi/rules/streams.yaml @@ -6,7 +6,7 @@ rules: context: pattern: | ⟦ - !τ1 ↦ !C1 [1| !b1.java_util_Stream$map(α0 ↦ !b2) |1], + !τ1 ↦ !b1.java_util_Stream$map(α0 ↦ !b2) * !t1, !B1 ⟧ result: | @@ -16,7 +16,7 @@ rules: α0 ↦ ξ.!τ2, α1 ↦ !b2 ), - !τ1 ↦ !C1 [1| ξ.!τ3 |1], + !τ1 ↦ ξ.!τ3 * !t1, !B1 ⟧ fresh: From 9e79118d1dc94b411924a18e12495d7b3fdb5f74 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Fri, 19 Jul 2024 11:50:43 +0300 Subject: [PATCH 08/12] Ensure fresh attributes --- eo-phi-normalizer/eo-phi-normalizer.cabal | 4 ++ eo-phi-normalizer/package.yaml | 1 + .../src/Language/EO/Phi/Rules/Yaml.hs | 58 ++++++++++++++++++- .../test/eo/phi/rules/streams.yaml | 6 +- 4 files changed, 63 insertions(+), 6 deletions(-) diff --git a/eo-phi-normalizer/eo-phi-normalizer.cabal b/eo-phi-normalizer/eo-phi-normalizer.cabal index 400e7980..f3bfad7b 100644 --- a/eo-phi-normalizer/eo-phi-normalizer.cabal +++ b/eo-phi-normalizer/eo-phi-normalizer.cabal @@ -156,6 +156,7 @@ library , blaze-markup , bytestring , cereal + , containers , directory , file-embed >=0.0.16.0 , filepath @@ -193,6 +194,7 @@ executable normalizer , blaze-markup , bytestring , cereal + , containers , directory , eo-phi-normalizer , file-embed >=0.0.16.0 @@ -257,6 +259,7 @@ test-suite doctests , blaze-markup , bytestring , cereal + , containers , directory , doctest-parallel , eo-phi-normalizer @@ -305,6 +308,7 @@ test-suite spec , blaze-markup , bytestring , cereal + , containers , directory , eo-phi-normalizer , file-embed >=0.0.16.0 diff --git a/eo-phi-normalizer/package.yaml b/eo-phi-normalizer/package.yaml index abae13a5..59aae898 100644 --- a/eo-phi-normalizer/package.yaml +++ b/eo-phi-normalizer/package.yaml @@ -58,6 +58,7 @@ dependencies: - regex-compat - cereal - bytestring + - containers default-extensions: - ImportQualifiedPost 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 a105cd17..924bbb72 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs +++ b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs @@ -25,11 +25,15 @@ import Data.Maybe (fromMaybe) import Data.String (IsString (..)) import Data.Yaml qualified as Yaml import GHC.Generics (Generic) +import Data.Set (Set) +import qualified Data.Set as Set import Language.EO.Phi import Language.EO.Phi.Rules.Common (Context (..), NamedRule) import Language.EO.Phi.Rules.Common qualified as Common import PyF (fmt) +import Language.EO.Phi (LabelId) +import Data.Monoid (Monoid(mempty)) -- $setup -- >>> :set -XOverloadedStrings @@ -120,18 +124,66 @@ convertRuleNamed :: Rule -> NamedRule convertRuleNamed rule = (rule.name, convertRule rule) mkFreshSubst :: Context -> Object -> Maybe [FreshMetaId] -> Subst -mkFreshSubst _ctx _obj metas = +mkFreshSubst ctx obj metas = Subst { objectMetas = [] , bindingsMetas = [] - , attributeMetas = zipWith mkFresh (fromMaybe [] metas) [1 ..] + , attributeMetas = mkFreshAttributes (usedLabelIds ctx <> objectLabelIds obj) (fromMaybe [] metas) , bytesMetas = [] , contextMetas = [] } where mkFresh FreshMetaId{..} i = (name, Label (LabelId label)) where - label = fromMaybe "tmp_" prefix <> "$fresh$" <> show i + label = fromMaybe "tmp_" prefix <> "$" <> show i + +mkFreshAttributes :: Set LabelId -> [FreshMetaId] -> [(MetaId, Attribute)] +mkFreshAttributes ids [] = [] +mkFreshAttributes ids (x:xs) = + case mkFreshAttribute ids x of + (ma, ids') -> ma : mkFreshAttributes ids' xs + +mkFreshAttribute :: Set LabelId -> FreshMetaId -> ((MetaId, Attribute), Set LabelId) +mkFreshAttribute ids FreshMetaId{..} = ((name, Label label), Set.insert label ids) + where + label = head + [ l + | i <- [1..] + , let l = LabelId (fromMaybe "tmp" prefix <> "$" <> show i) + , l `Set.notMember` ids + ] + +usedLabelIds :: Context -> Set LabelId +usedLabelIds Context{..} = objectLabelIds globalObject + where + globalObject = NonEmpty.last outerFormations + +objectLabelIds :: Object -> Set LabelId +objectLabelIds = \case + GlobalObject -> mempty + ThisObject -> mempty + Formation bindings -> foldMap bindingLabelIds bindings + ObjectDispatch obj a -> objectLabelIds obj <> attrLabelIds a + Application obj bindings -> objectLabelIds obj <> foldMap bindingLabelIds bindings + Termination -> mempty + MetaObject{} -> mempty + MetaFunction _ obj -> objectLabelIds obj + MetaTailContext obj _ -> objectLabelIds obj + MetaSubstThis obj obj' -> objectLabelIds obj <> objectLabelIds obj' + +bindingLabelIds :: Binding -> Set LabelId +bindingLabelIds = \case + AlphaBinding a obj -> objectLabelIds obj <> attrLabelIds a + DeltaBinding _bytes -> mempty + EmptyBinding a -> attrLabelIds a + DeltaEmptyBinding -> mempty + LambdaBinding _ -> mempty + MetaBindings _ -> mempty + MetaDeltaBinding _ -> mempty + +attrLabelIds :: Attribute -> Set LabelId +attrLabelIds (Label l) = Set.singleton l +attrLabelIds _ = mempty -- >>> matchContext (Context [] ["⟦ a ↦ ⟦ ⟧, x ↦ ξ.a ⟧"] (Label (LabelId "x"))) (Just (RuleContext Nothing (Just "⟦ !a ↦ !obj, !B ⟧") (Just "!a"))) -- [Subst { diff --git a/eo-phi-normalizer/test/eo/phi/rules/streams.yaml b/eo-phi-normalizer/test/eo/phi/rules/streams.yaml index b968f042..16f555f9 100644 --- a/eo-phi-normalizer/test/eo/phi/rules/streams.yaml +++ b/eo-phi-normalizer/test/eo/phi/rules/streams.yaml @@ -49,11 +49,11 @@ rules: output: - | ⟦ - foreach_body$fresh$1 ↦ ξ.list.java_util_Stream$filter (α0 ↦ ⟦ + foreach_body$1 ↦ ξ.list.java_util_Stream$filter (α0 ↦ ⟦ el ↦ ∅, φ ↦ ξ.el.equals (α0 ↦ Φ.org.eolang.string (as-bytes ↦ Φ.org.eolang.bytes (Δ ⤍ 00-))).not ⟧), - java_util_Stream$map_result$fresh$2 ↦ Φ.opeo.map-for-each (α0 ↦ ξ.foreach_body$fresh$1, α1 ↦ ⟦ + java_util_Stream$map_result$1 ↦ Φ.opeo.map-for-each (α0 ↦ ξ.foreach_body$1, α1 ↦ ⟦ el ↦ ∅, φ ↦ Φ.java_util_Integer.parseInt (α0 ↦ ξ.el) ⟧), - result ↦ ξ.java_util_Stream$map_result$fresh$2.java_util_Stream$toList, list ↦ ∅ + result ↦ ξ.java_util_Stream$map_result$1.java_util_Stream$toList, list ↦ ∅ ⟧ From c4071f7aa2a1c63b3482d93c082aaa1f6299c082 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Fri, 19 Jul 2024 13:08:40 +0300 Subject: [PATCH 09/12] Allow forall to explicitly mention metavariables in pattern --- .../src/Language/EO/Phi/Rules/Yaml.hs | 64 +++++++++++++++++-- .../test/eo/phi/rules/streams.yaml | 6 ++ 2 files changed, 64 insertions(+), 6 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 924bbb72..16419d31 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs +++ b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs @@ -11,10 +11,11 @@ {-# OPTIONS_GHC -Wno-orphans #-} {-# OPTIONS_GHC -Wno-partial-fields #-} {-# OPTIONS_GHC -Wno-type-defaults #-} +{-# OPTIONS_GHC -Wno-forall-identifier #-} module Language.EO.Phi.Rules.Yaml where -import Control.Monad (guard) +import Control.Monad (guard, unless) import Control.Monad.State (State, evalState) import Data.Aeson (FromJSON (..), Options (sumEncoding), SumEncoding (UntaggedValue), genericParseJSON) import Data.Aeson.Types (defaultOptions) @@ -65,6 +66,7 @@ data Rule = Rule { name :: String , description :: String , context :: Maybe RuleContext + , forall :: Maybe [MetaId] , pattern :: Object , result :: Object , fresh :: Maybe [FreshMetaId] @@ -108,6 +110,32 @@ parseRuleSetFromFile = Yaml.decodeFileThrow convertRule :: Rule -> Common.Rule convertRule Rule{..} ctx obj = do + -- first validate pattern and result in the rule + -- TODO: we should perform this check once, not every time we run the rule + let freshMetaIds = foldMap (Set.fromList . map (\FreshMetaId{..} -> name)) fresh + + patternMetaIds = objectMetaIds pattern + resultMetaIds = objectMetaIds result + + unusedFreshMetaIds = Set.difference freshMetaIds resultMetaIds + unless (null unusedFreshMetaIds) $ + error ("invalid rule: result does not use some fresh variables quantified by the fresh: " <> show (Set.toList unusedFreshMetaIds)) + + case forall of + Nothing -> return () + Just forall' -> do + let forallMetaIds = Set.fromList forall' + resultAllowedMetaIds = forallMetaIds <> freshMetaIds + unquantifiedMetaIds = Set.difference patternMetaIds forallMetaIds + unusedMetaIds = Set.difference forallMetaIds patternMetaIds + unquantifiedResultMetaIds = Set.difference resultMetaIds resultAllowedMetaIds + unless (null unquantifiedMetaIds) $ + error ("invalid rule: pattern uses meta variables not quantified by the forall: " <> show (Set.toList unquantifiedMetaIds)) + unless (null unusedMetaIds) $ + error ("invalid rule: pattern does not use some variables quantified by the forall: " <> show (Set.toList unusedMetaIds)) + unless (null unquantifiedResultMetaIds) $ + error ("invalid rule: result uses meta variables not quantified by the forall or the fresh: " <> show (Set.toList unquantifiedResultMetaIds)) + contextSubsts <- matchContext ctx context let pattern' = applySubst contextSubsts pattern result' = applySubst contextSubsts result @@ -132,13 +160,9 @@ mkFreshSubst ctx obj metas = , bytesMetas = [] , contextMetas = [] } - where - mkFresh FreshMetaId{..} i = (name, Label (LabelId label)) - where - label = fromMaybe "tmp_" prefix <> "$" <> show i mkFreshAttributes :: Set LabelId -> [FreshMetaId] -> [(MetaId, Attribute)] -mkFreshAttributes ids [] = [] +mkFreshAttributes _ids [] = [] mkFreshAttributes ids (x:xs) = case mkFreshAttribute ids x of (ma, ids') -> ma : mkFreshAttributes ids' xs @@ -202,6 +226,34 @@ matchContext Common.Context{..} (Just (RuleContext{..})) = do globalObject = NonEmpty.last outerFormations thisObject = NonEmpty.head outerFormations +objectMetaIds :: Object -> Set MetaId +objectMetaIds (Formation bindings) = foldMap bindingMetaIds bindings +objectMetaIds (Application object bindings) = objectMetaIds object <> foldMap bindingMetaIds bindings +objectMetaIds (ObjectDispatch object attr) = objectMetaIds object <> attrMetaIds attr +objectMetaIds GlobalObject = mempty +objectMetaIds ThisObject = mempty +objectMetaIds Termination = mempty +objectMetaIds (MetaObject x) = Set.singleton x +objectMetaIds (MetaFunction _ obj) = objectMetaIds obj +objectMetaIds (MetaTailContext obj x) = objectMetaIds obj <> Set.singleton x +objectMetaIds (MetaSubstThis obj obj') = foldMap objectMetaIds [obj, obj'] + +bindingMetaIds :: Binding -> Set MetaId +bindingMetaIds (AlphaBinding attr obj) = attrMetaIds attr <> objectMetaIds obj +bindingMetaIds (EmptyBinding attr) = attrMetaIds attr +bindingMetaIds (DeltaBinding _) = mempty +bindingMetaIds DeltaEmptyBinding = mempty +bindingMetaIds (LambdaBinding _) = mempty +bindingMetaIds (MetaBindings x) = Set.singleton x +bindingMetaIds (MetaDeltaBinding x) = Set.singleton x + +attrMetaIds :: Attribute -> Set MetaId +attrMetaIds Phi = mempty +attrMetaIds Rho = mempty +attrMetaIds (Label _) = mempty +attrMetaIds (Alpha _) = mempty +attrMetaIds (MetaAttr x) = Set.singleton x + objectHasMetavars :: Object -> Bool objectHasMetavars (Formation bindings) = any bindingHasMetavars bindings objectHasMetavars (Application object bindings) = objectHasMetavars object || any bindingHasMetavars bindings diff --git a/eo-phi-normalizer/test/eo/phi/rules/streams.yaml b/eo-phi-normalizer/test/eo/phi/rules/streams.yaml index 16f555f9..34c555c3 100644 --- a/eo-phi-normalizer/test/eo/phi/rules/streams.yaml +++ b/eo-phi-normalizer/test/eo/phi/rules/streams.yaml @@ -4,6 +4,12 @@ rules: description: | Replacing Java Stream's map with a for-each loop. context: + forall: + - '!τ1' + - '!b1' + - '!b2' + - '!t1' + - '!B1' pattern: | ⟦ !τ1 ↦ !b1.java_util_Stream$map(α0 ↦ !b2) * !t1, From 583944da0640c30d74a2e84d018f1291b667bebc Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Fri, 19 Jul 2024 14:01:31 +0300 Subject: [PATCH 10/12] Distinguish meta identifiers lexically --- eo-phi-normalizer/grammar/EO/Phi/Syntax.cf | 22 ++++-- .../src/Language/EO/Phi/Rules/Common.hs | 4 +- .../src/Language/EO/Phi/Rules/Yaml.hs | 67 +++++++++++-------- .../src/Language/EO/Phi/Syntax/Abs.hs | 36 ++++++++-- .../src/Language/EO/Phi/Syntax/Doc.txt | 39 +++++++++-- .../src/Language/EO/Phi/Syntax/Lex.x | 34 ++++++++-- .../src/Language/EO/Phi/Syntax/Par.y | 42 +++++++++--- .../src/Language/EO/Phi/Syntax/Print.hs | 30 +++++++-- .../test/Language/EO/Rules/PhiPaperSpec.hs | 14 +++- 9 files changed, 219 insertions(+), 69 deletions(-) diff --git a/eo-phi-normalizer/grammar/EO/Phi/Syntax.cf b/eo-phi-normalizer/grammar/EO/Phi/Syntax.cf index 23ff3a72..e69d4b79 100644 --- a/eo-phi-normalizer/grammar/EO/Phi/Syntax.cf +++ b/eo-phi-normalizer/grammar/EO/Phi/Syntax.cf @@ -11,11 +11,21 @@ token Bytes ({"--"} | ["0123456789ABCDEF"] ["0123456789ABCDEF"] {"-"} | ["012345 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,.|':;!-?][}{)(⟧⟦"])* ; +token LabelMetaId {"!τ"} (char - [" \r\n\t,.|':;!-?][}{)(⟧⟦"])* ; +token TailMetaId {"!t"} (char - [" \r\n\t,.|':;!-?][}{)(⟧⟦"])* ; +token BindingsMetaId {"!B"} (char - [" \r\n\t,.|':;!-?][}{)(⟧⟦"])* ; +token ObjectMetaId {"!b"} (char - [" \r\n\t,.|':;!-?][}{)(⟧⟦"])* ; +token BytesMetaId {"!y"} (char - [" \r\n\t,.|':;!-?][}{)(⟧⟦"])* ; token MetaFunctionName {"@"} (char - [" \r\n\t,.|':;!-?][}{)(⟧⟦"])* ; Program. Program ::= "{" "⟦" [Binding] "⟧" "}" ; +MetaIdLabel. MetaId ::= LabelMetaId ; +MetaIdTail. MetaId ::= TailMetaId ; +MetaIdBindings. MetaId ::= BindingsMetaId ; +MetaIdObject. MetaId ::= ObjectMetaId ; +MetaIdBytes. MetaId ::= BytesMetaId ; + Formation. Object ::= "⟦" [Binding] "⟧" ; Application. Object ::= Object "(" [Binding] ")" ; ObjectDispatch. Object ::= Object "." Attribute ; @@ -23,8 +33,8 @@ GlobalObject. Object ::= "Φ"; ThisObject. Object ::= "ξ"; Termination. Object ::= "⊥" ; MetaSubstThis. Object ::= Object "[" "ξ" "↦" Object "]" ; -MetaObject. Object ::= MetaId ; -MetaTailContext. Object ::= Object "*" MetaId ; +MetaObject. Object ::= ObjectMetaId ; +MetaTailContext. Object ::= Object "*" TailMetaId ; MetaFunction. Object ::= MetaFunctionName "(" Object ")" ; AlphaBinding. Binding ::= Attribute "↦" Object ; @@ -32,15 +42,15 @@ EmptyBinding. Binding ::= Attribute "↦" "∅" ; DeltaBinding. Binding ::= "Δ" "⤍" Bytes ; DeltaEmptyBinding. Binding ::= "Δ" "⤍" "∅" ; LambdaBinding. Binding ::= "λ" "⤍" Function ; -MetaBindings. Binding ::= MetaId ; -MetaDeltaBinding. Binding ::= "Δ" "⤍" MetaId ; +MetaBindings. Binding ::= BindingsMetaId ; +MetaDeltaBinding. Binding ::= "Δ" "⤍" BytesMetaId ; separator Binding "," ; Phi. Attribute ::= "φ" ; -- decoratee object Rho. Attribute ::= "ρ" ; -- parent object Label. Attribute ::= LabelId ; Alpha. Attribute ::= AlphaIndex ; -MetaAttr. Attribute ::= MetaId ; +MetaAttr. Attribute ::= LabelMetaId ; -- Additional symbols used as attributes in the rules ObjectAttr. RuleAttribute ::= Attribute ; 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 aa4da39c..e1c77261 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs +++ b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs @@ -42,6 +42,8 @@ instance IsString RuleAttribute where fromString = unsafeParseWith pRuleAttribut instance IsString PeeledObject where fromString = unsafeParseWith pPeeledObject instance IsString ObjectHead where fromString = unsafeParseWith pObjectHead +instance IsString MetaId where fromString = unsafeParseWith pMetaId + parseWith :: ([Token] -> Either String a) -> String -> Either String a parseWith parser input = parser tokens where @@ -256,7 +258,7 @@ equalBindings bindings1 bindings2 = and (zipWith equalBinding (sortOn attr bindi attr DeltaEmptyBinding = Label (LabelId "Δ") attr (MetaDeltaBinding _) = Label (LabelId "Δ") attr (LambdaBinding _) = Label (LabelId "λ") - attr (MetaBindings metaId) = MetaAttr metaId + attr (MetaBindings (BindingsMetaId metaId)) = MetaAttr (LabelMetaId metaId) equalBinding :: Binding -> Binding -> Bool equalBinding (AlphaBinding attr1 obj1) (AlphaBinding attr2 obj2) = attr1 == attr2 && equalObject obj1 obj2 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 16419d31..2484e133 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs +++ b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs @@ -29,12 +29,11 @@ import GHC.Generics (Generic) import Data.Set (Set) import qualified Data.Set as Set -import Language.EO.Phi +import Language.EO.Phi ( printTree ) import Language.EO.Phi.Rules.Common (Context (..), NamedRule) import Language.EO.Phi.Rules.Common qualified as Common import PyF (fmt) -import Language.EO.Phi (LabelId) -import Data.Monoid (Monoid(mempty)) +import Language.EO.Phi.Syntax.Abs -- $setup -- >>> :set -XOverloadedStrings @@ -42,7 +41,16 @@ import Data.Monoid (Monoid(mempty)) 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 ObjectMetaId where parseJSON = fmap ObjectMetaId . parseJSON +instance FromJSON LabelMetaId where parseJSON = fmap LabelMetaId . parseJSON +instance FromJSON TailMetaId where parseJSON = fmap TailMetaId . parseJSON +instance FromJSON BindingsMetaId where parseJSON = fmap BindingsMetaId . parseJSON +instance FromJSON BytesMetaId where parseJSON = fmap BytesMetaId . parseJSON + +instance FromJSON MetaId where + parseJSON = fmap fromString . parseJSON + instance FromJSON Attribute where parseJSON = fmap fromString . parseJSON instance FromJSON RuleAttribute where parseJSON = fmap fromString . parseJSON @@ -76,7 +84,7 @@ data Rule = Rule deriving (Generic, FromJSON, Show) data FreshMetaId = FreshMetaId - { name :: MetaId + { name :: LabelMetaId , prefix :: Maybe String } deriving (Generic, FromJSON, Show) @@ -112,14 +120,18 @@ convertRule :: Rule -> Common.Rule convertRule Rule{..} ctx obj = do -- first validate pattern and result in the rule -- TODO: we should perform this check once, not every time we run the rule - let freshMetaIds = foldMap (Set.fromList . map (\FreshMetaId{..} -> name)) fresh + let freshMetaIds = Set.mapMonotonic MetaIdLabel $ + foldMap (Set.fromList . map (\FreshMetaId{name=x} -> x)) fresh patternMetaIds = objectMetaIds pattern resultMetaIds = objectMetaIds result unusedFreshMetaIds = Set.difference freshMetaIds resultMetaIds + + ppMetaIds = intercalate ", " . map printTree . Set.toList + unless (null unusedFreshMetaIds) $ - error ("invalid rule: result does not use some fresh variables quantified by the fresh: " <> show (Set.toList unusedFreshMetaIds)) + error ("invalid rule: result does not use some fresh variables quantified by the fresh: " <> ppMetaIds unusedFreshMetaIds) case forall of Nothing -> return () @@ -130,11 +142,11 @@ convertRule Rule{..} ctx obj = do unusedMetaIds = Set.difference forallMetaIds patternMetaIds unquantifiedResultMetaIds = Set.difference resultMetaIds resultAllowedMetaIds unless (null unquantifiedMetaIds) $ - error ("invalid rule: pattern uses meta variables not quantified by the forall: " <> show (Set.toList unquantifiedMetaIds)) + error ("invalid rule: pattern uses meta variables not quantified by the forall: " <> ppMetaIds unquantifiedMetaIds) unless (null unusedMetaIds) $ - error ("invalid rule: pattern does not use some variables quantified by the forall: " <> show (Set.toList unusedMetaIds)) + error ("invalid rule: pattern does not use some variables quantified by the forall: " <> ppMetaIds unusedMetaIds) unless (null unquantifiedResultMetaIds) $ - error ("invalid rule: result uses meta variables not quantified by the forall or the fresh: " <> show (Set.toList unquantifiedResultMetaIds)) + error ("invalid rule: result uses meta variables not quantified by the forall or the fresh: " <> ppMetaIds unquantifiedResultMetaIds) contextSubsts <- matchContext ctx context let pattern' = applySubst contextSubsts pattern @@ -161,13 +173,13 @@ mkFreshSubst ctx obj metas = , contextMetas = [] } -mkFreshAttributes :: Set LabelId -> [FreshMetaId] -> [(MetaId, Attribute)] +mkFreshAttributes :: Set LabelId -> [FreshMetaId] -> [(LabelMetaId, Attribute)] mkFreshAttributes _ids [] = [] mkFreshAttributes ids (x:xs) = case mkFreshAttribute ids x of (ma, ids') -> ma : mkFreshAttributes ids' xs -mkFreshAttribute :: Set LabelId -> FreshMetaId -> ((MetaId, Attribute), Set LabelId) +mkFreshAttribute :: Set LabelId -> FreshMetaId -> ((LabelMetaId, Attribute), Set LabelId) mkFreshAttribute ids FreshMetaId{..} = ((name, Label label), Set.insert label ids) where label = head @@ -233,9 +245,9 @@ objectMetaIds (ObjectDispatch object attr) = objectMetaIds object <> attrMetaIds objectMetaIds GlobalObject = mempty objectMetaIds ThisObject = mempty objectMetaIds Termination = mempty -objectMetaIds (MetaObject x) = Set.singleton x +objectMetaIds (MetaObject x) = Set.singleton (MetaIdObject x) objectMetaIds (MetaFunction _ obj) = objectMetaIds obj -objectMetaIds (MetaTailContext obj x) = objectMetaIds obj <> Set.singleton x +objectMetaIds (MetaTailContext obj x) = objectMetaIds obj <> Set.singleton (MetaIdTail x) objectMetaIds (MetaSubstThis obj obj') = foldMap objectMetaIds [obj, obj'] bindingMetaIds :: Binding -> Set MetaId @@ -244,15 +256,15 @@ bindingMetaIds (EmptyBinding attr) = attrMetaIds attr bindingMetaIds (DeltaBinding _) = mempty bindingMetaIds DeltaEmptyBinding = mempty bindingMetaIds (LambdaBinding _) = mempty -bindingMetaIds (MetaBindings x) = Set.singleton x -bindingMetaIds (MetaDeltaBinding x) = Set.singleton x +bindingMetaIds (MetaBindings x) = Set.singleton (MetaIdBindings x) +bindingMetaIds (MetaDeltaBinding x) = Set.singleton (MetaIdBytes x) attrMetaIds :: Attribute -> Set MetaId attrMetaIds Phi = mempty attrMetaIds Rho = mempty attrMetaIds (Label _) = mempty attrMetaIds (Alpha _) = mempty -attrMetaIds (MetaAttr x) = Set.singleton x +attrMetaIds (MetaAttr x) = Set.singleton (MetaIdLabel x) objectHasMetavars :: Object -> Bool objectHasMetavars (Formation bindings) = any bindingHasMetavars bindings @@ -334,17 +346,17 @@ hasAttr attr = any (isAttr attr) -- ⟦ c ↦ ⟦ ⟧ ⟧(ρ ↦ ⟦ b ↦ ⟦ ⟧ ⟧) data OneHoleContext = OneHoleContext - { holeMetaId :: !MetaId + { holeMetaId :: !ObjectMetaId , contextObject :: !Object } deriving (Show) data Subst = Subst - { objectMetas :: [(MetaId, Object)] - , bindingsMetas :: [(MetaId, [Binding])] - , attributeMetas :: [(MetaId, Attribute)] - , bytesMetas :: [(MetaId, Bytes)] - , contextMetas :: [(MetaId, OneHoleContext)] + { objectMetas :: [(ObjectMetaId, Object)] + , bindingsMetas :: [(BindingsMetaId, [Binding])] + , attributeMetas :: [(LabelMetaId, Attribute)] + , bytesMetas :: [(BytesMetaId, Bytes)] + , contextMetas :: [(TailMetaId, OneHoleContext)] } instance Show Subst where show Subst{..} = @@ -359,7 +371,7 @@ instance Show Subst where , "}" ] where - showMappings metas = intercalate "; " $ map (\(MetaId metaId, obj) -> [fmt|{metaId} -> '{printTree obj}'|]) metas + showMappings metas = intercalate "; " $ map (\(metaId, obj) -> [fmt|{printTree metaId} -> '{printTree obj}'|]) metas instance Semigroup Subst where (<>) = mergeSubst @@ -439,10 +451,11 @@ matchObject ThisObject ThisObject = [emptySubst] matchObject GlobalObject GlobalObject = [emptySubst] matchObject _ _ = [] -- ? emptySubst ? -matchOneHoleContext :: MetaId -> Object -> Object -> [(Subst, OneHoleContext)] -matchOneHoleContext ctxId@(MetaId name) pat obj = matchWhole <> matchPart +matchOneHoleContext :: TailMetaId -> Object -> Object -> [(Subst, OneHoleContext)] +matchOneHoleContext ctxId pat obj = matchWhole <> matchPart where - holeId = MetaId (name ++ ":hole") -- FIXME: ensure fresh names + TailMetaId name = ctxId + holeId = ObjectMetaId (name ++ ":hole") -- FIXME: ensure fresh names matchWhole = do subst' <- matchObject pat obj pure (subst', OneHoleContext holeId (MetaObject holeId)) diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Abs.hs b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Abs.hs index b3387182..40736062 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Abs.hs +++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Abs.hs @@ -18,6 +18,14 @@ 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 MetaId + = MetaIdLabel LabelMetaId + | MetaIdTail TailMetaId + | MetaIdBindings BindingsMetaId + | MetaIdObject ObjectMetaId + | MetaIdBytes BytesMetaId + deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic) + data Object = Formation [Binding] | Application Object [Binding] @@ -26,8 +34,8 @@ data Object | ThisObject | Termination | MetaSubstThis Object Object - | MetaObject MetaId - | MetaTailContext Object MetaId + | MetaObject ObjectMetaId + | MetaTailContext Object TailMetaId | MetaFunction MetaFunctionName Object deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic) @@ -37,12 +45,16 @@ data Binding | DeltaBinding Bytes | DeltaEmptyBinding | LambdaBinding Function - | MetaBindings MetaId - | MetaDeltaBinding MetaId + | MetaBindings BindingsMetaId + | MetaDeltaBinding BytesMetaId deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic) data Attribute - = Phi | Rho | Label LabelId | Alpha AlphaIndex | MetaAttr MetaId + = Phi + | Rho + | Label LabelId + | Alpha AlphaIndex + | MetaAttr LabelMetaId deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic) data RuleAttribute = ObjectAttr Attribute | DeltaAttr | LambdaAttr @@ -71,7 +83,19 @@ newtype LabelId = LabelId String 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 +newtype LabelMetaId = LabelMetaId String + deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic, Data.String.IsString) + +newtype TailMetaId = TailMetaId String + deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic, Data.String.IsString) + +newtype BindingsMetaId = BindingsMetaId String + deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic, Data.String.IsString) + +newtype ObjectMetaId = ObjectMetaId String + deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic, Data.String.IsString) + +newtype BytesMetaId = BytesMetaId String deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic, Data.String.IsString) newtype MetaFunctionName = MetaFunctionName String diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Doc.txt b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Doc.txt index bc1a3677..fdbf2c08 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Doc.txt +++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Doc.txt @@ -18,6 +18,10 @@ This document was automatically generated by the //BNF-Converter//. It was gener + + + + Bytes literals are recognized by the regular expression `````{"--"} | ["0123456789ABCDEF"] ["0123456789ABCDEF"] '-' | ["0123456789ABCDEF"] ["0123456789ABCDEF"] ('-' ["0123456789ABCDEF"] ["0123456789ABCDEF"])+````` @@ -32,8 +36,24 @@ LabelId literals are recognized by the regular expression AlphaIndex literals are recognized by the regular expression `````{"α0"} | 'α' (digit - '0') digit*````` -MetaId literals are recognized by the regular expression -`````'!' (char - [" +LabelMetaId literals are recognized by the regular expression +`````{"!τ"} (char - [" + !'(),-.:;?[]{|}⟦⟧"])*````` + +TailMetaId literals are recognized by the regular expression +`````{"!t"} (char - [" + !'(),-.:;?[]{|}⟦⟧"])*````` + +BindingsMetaId literals are recognized by the regular expression +`````{"!B"} (char - [" + !'(),-.:;?[]{|}⟦⟧"])*````` + +ObjectMetaId literals are recognized by the regular expression +`````{"!b"} (char - [" + !'(),-.:;?[]{|}⟦⟧"])*````` + +BytesMetaId literals are recognized by the regular expression +`````{"!y"} (char - [" !'(),-.:;?[]{|}⟦⟧"])*````` MetaFunctionName literals are recognized by the regular expression @@ -64,6 +84,11 @@ and **eps** (empty rule) belong to the BNF notation. All other symbols are terminals. | //Program// | -> | ``{`` ``⟦`` //[Binding]// ``⟧`` ``}`` + | //MetaId// | -> | //LabelMetaId// + | | **|** | //TailMetaId// + | | **|** | //BindingsMetaId// + | | **|** | //ObjectMetaId// + | | **|** | //BytesMetaId// | //Object// | -> | ``⟦`` //[Binding]// ``⟧`` | | **|** | //Object// ``(`` //[Binding]// ``)`` | | **|** | //Object// ``.`` //Attribute// @@ -71,16 +96,16 @@ All other symbols are terminals. | | **|** | ``ξ`` | | **|** | ``⊥`` | | **|** | //Object// ``[`` ``ξ`` ``↦`` //Object// ``]`` - | | **|** | //MetaId// - | | **|** | //Object// ``*`` //MetaId// + | | **|** | //ObjectMetaId// + | | **|** | //Object// ``*`` //TailMetaId// | | **|** | //MetaFunctionName// ``(`` //Object// ``)`` | //Binding// | -> | //Attribute// ``↦`` //Object// | | **|** | //Attribute// ``↦`` ``∅`` | | **|** | ``Δ`` ``⤍`` //Bytes// | | **|** | ``Δ`` ``⤍`` ``∅`` | | **|** | ``λ`` ``⤍`` //Function// - | | **|** | //MetaId// - | | **|** | ``Δ`` ``⤍`` //MetaId// + | | **|** | //BindingsMetaId// + | | **|** | ``Δ`` ``⤍`` //BytesMetaId// | //[Binding]// | -> | **eps** | | **|** | //Binding// | | **|** | //Binding// ``,`` //[Binding]// @@ -88,7 +113,7 @@ All other symbols are terminals. | | **|** | ``ρ`` | | **|** | //LabelId// | | **|** | //AlphaIndex// - | | **|** | //MetaId// + | | **|** | //LabelMetaId// | //RuleAttribute// | -> | //Attribute// | | **|** | ``Δ`` | | **|** | ``λ`` diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Lex.x b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Lex.x index 4119d8e5..6da63877 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Lex.x +++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Lex.x @@ -61,9 +61,25 @@ $s [$u # [\t \n \r \ \! \' \( \) \, \. \: \; \? \[ \] \{ \| \} \⟦ \⟧]] * α 0 | α [$d # 0]$d * { tok (eitherResIdent T_AlphaIndex) } --- token MetaId -\! [$u # [\t \n \r \ \! \' \( \) \, \- \. \: \; \? \[ \] \{ \| \} \⟦ \⟧]] * - { tok (eitherResIdent T_MetaId) } +-- token LabelMetaId +\! τ [$u # [\t \n \r \ \! \' \( \) \, \- \. \: \; \? \[ \] \{ \| \} \⟦ \⟧]] * + { tok (eitherResIdent T_LabelMetaId) } + +-- token TailMetaId +\! t [$u # [\t \n \r \ \! \' \( \) \, \- \. \: \; \? \[ \] \{ \| \} \⟦ \⟧]] * + { tok (eitherResIdent T_TailMetaId) } + +-- token BindingsMetaId +\! B [$u # [\t \n \r \ \! \' \( \) \, \- \. \: \; \? \[ \] \{ \| \} \⟦ \⟧]] * + { tok (eitherResIdent T_BindingsMetaId) } + +-- token ObjectMetaId +\! b [$u # [\t \n \r \ \! \' \( \) \, \- \. \: \; \? \[ \] \{ \| \} \⟦ \⟧]] * + { tok (eitherResIdent T_ObjectMetaId) } + +-- token BytesMetaId +\! y [$u # [\t \n \r \ \! \' \( \) \, \- \. \: \; \? \[ \] \{ \| \} \⟦ \⟧]] * + { tok (eitherResIdent T_BytesMetaId) } -- token MetaFunctionName \@ [$u # [\t \n \r \ \! \' \( \) \, \- \. \: \; \? \[ \] \{ \| \} \⟦ \⟧]] * @@ -90,7 +106,11 @@ data Tok | T_Function !String | T_LabelId !String | T_AlphaIndex !String - | T_MetaId !String + | T_LabelMetaId !String + | T_TailMetaId !String + | T_BindingsMetaId !String + | T_ObjectMetaId !String + | T_BytesMetaId !String | T_MetaFunctionName !String deriving (Eq, Show, Ord) @@ -158,7 +178,11 @@ tokenText t = case t of PT _ (T_Function s) -> s PT _ (T_LabelId s) -> s PT _ (T_AlphaIndex s) -> s - PT _ (T_MetaId s) -> s + PT _ (T_LabelMetaId s) -> s + PT _ (T_TailMetaId s) -> s + PT _ (T_BindingsMetaId s) -> s + PT _ (T_ObjectMetaId s) -> s + PT _ (T_BytesMetaId s) -> s PT _ (T_MetaFunctionName s) -> s -- | Convert a token to a string. diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Par.y b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Par.y index 5e45abc4..f1e6760c 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Par.y +++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Par.y @@ -9,6 +9,7 @@ module Language.EO.Phi.Syntax.Par ( happyError , myLexer , pProgram + , pMetaId , pObject , pBinding , pListBinding @@ -28,6 +29,7 @@ import Language.EO.Phi.Syntax.Lex } %name pProgram Program +%name pMetaId MetaId %name pObject Object %name pBinding Binding %name pListBinding ListBinding @@ -66,7 +68,11 @@ import Language.EO.Phi.Syntax.Lex L_Function { PT _ (T_Function $$) } L_LabelId { PT _ (T_LabelId $$) } L_AlphaIndex { PT _ (T_AlphaIndex $$) } - L_MetaId { PT _ (T_MetaId $$) } + L_LabelMetaId { PT _ (T_LabelMetaId $$) } + L_TailMetaId { PT _ (T_TailMetaId $$) } + L_BindingsMetaId { PT _ (T_BindingsMetaId $$) } + L_ObjectMetaId { PT _ (T_ObjectMetaId $$) } + L_BytesMetaId { PT _ (T_BytesMetaId $$) } L_MetaFunctionName { PT _ (T_MetaFunctionName $$) } %% @@ -83,8 +89,20 @@ 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 } +LabelMetaId :: { Language.EO.Phi.Syntax.Abs.LabelMetaId } +LabelMetaId : L_LabelMetaId { Language.EO.Phi.Syntax.Abs.LabelMetaId $1 } + +TailMetaId :: { Language.EO.Phi.Syntax.Abs.TailMetaId } +TailMetaId : L_TailMetaId { Language.EO.Phi.Syntax.Abs.TailMetaId $1 } + +BindingsMetaId :: { Language.EO.Phi.Syntax.Abs.BindingsMetaId } +BindingsMetaId : L_BindingsMetaId { Language.EO.Phi.Syntax.Abs.BindingsMetaId $1 } + +ObjectMetaId :: { Language.EO.Phi.Syntax.Abs.ObjectMetaId } +ObjectMetaId : L_ObjectMetaId { Language.EO.Phi.Syntax.Abs.ObjectMetaId $1 } + +BytesMetaId :: { Language.EO.Phi.Syntax.Abs.BytesMetaId } +BytesMetaId : L_BytesMetaId { Language.EO.Phi.Syntax.Abs.BytesMetaId $1 } MetaFunctionName :: { Language.EO.Phi.Syntax.Abs.MetaFunctionName } MetaFunctionName : L_MetaFunctionName { Language.EO.Phi.Syntax.Abs.MetaFunctionName $1 } @@ -93,6 +111,14 @@ Program :: { Language.EO.Phi.Syntax.Abs.Program } Program : '{' '⟦' ListBinding '⟧' '}' { Language.EO.Phi.Syntax.Abs.Program $3 } +MetaId :: { Language.EO.Phi.Syntax.Abs.MetaId } +MetaId + : LabelMetaId { Language.EO.Phi.Syntax.Abs.MetaIdLabel $1 } + | TailMetaId { Language.EO.Phi.Syntax.Abs.MetaIdTail $1 } + | BindingsMetaId { Language.EO.Phi.Syntax.Abs.MetaIdBindings $1 } + | ObjectMetaId { Language.EO.Phi.Syntax.Abs.MetaIdObject $1 } + | BytesMetaId { Language.EO.Phi.Syntax.Abs.MetaIdBytes $1 } + Object :: { Language.EO.Phi.Syntax.Abs.Object } Object : '⟦' ListBinding '⟧' { Language.EO.Phi.Syntax.Abs.Formation $2 } @@ -102,8 +128,8 @@ Object | 'ξ' { Language.EO.Phi.Syntax.Abs.ThisObject } | '⊥' { Language.EO.Phi.Syntax.Abs.Termination } | Object '[' 'ξ' '↦' Object ']' { Language.EO.Phi.Syntax.Abs.MetaSubstThis $1 $5 } - | MetaId { Language.EO.Phi.Syntax.Abs.MetaObject $1 } - | Object '*' MetaId { Language.EO.Phi.Syntax.Abs.MetaTailContext $1 $3 } + | ObjectMetaId { Language.EO.Phi.Syntax.Abs.MetaObject $1 } + | Object '*' TailMetaId { Language.EO.Phi.Syntax.Abs.MetaTailContext $1 $3 } | MetaFunctionName '(' Object ')' { Language.EO.Phi.Syntax.Abs.MetaFunction $1 $3 } Binding :: { Language.EO.Phi.Syntax.Abs.Binding } @@ -113,8 +139,8 @@ Binding | 'Δ' '⤍' Bytes { Language.EO.Phi.Syntax.Abs.DeltaBinding $3 } | 'Δ' '⤍' '∅' { Language.EO.Phi.Syntax.Abs.DeltaEmptyBinding } | 'λ' '⤍' Function { Language.EO.Phi.Syntax.Abs.LambdaBinding $3 } - | MetaId { Language.EO.Phi.Syntax.Abs.MetaBindings $1 } - | 'Δ' '⤍' MetaId { Language.EO.Phi.Syntax.Abs.MetaDeltaBinding $3 } + | BindingsMetaId { Language.EO.Phi.Syntax.Abs.MetaBindings $1 } + | 'Δ' '⤍' BytesMetaId { Language.EO.Phi.Syntax.Abs.MetaDeltaBinding $3 } ListBinding :: { [Language.EO.Phi.Syntax.Abs.Binding] } ListBinding @@ -128,7 +154,7 @@ Attribute | 'ρ' { Language.EO.Phi.Syntax.Abs.Rho } | LabelId { Language.EO.Phi.Syntax.Abs.Label $1 } | AlphaIndex { Language.EO.Phi.Syntax.Abs.Alpha $1 } - | MetaId { Language.EO.Phi.Syntax.Abs.MetaAttr $1 } + | LabelMetaId { Language.EO.Phi.Syntax.Abs.MetaAttr $1 } RuleAttribute :: { Language.EO.Phi.Syntax.Abs.RuleAttribute } RuleAttribute diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Print.hs b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Print.hs index 98c729fd..044d40b1 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Print.hs +++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Print.hs @@ -145,14 +145,30 @@ 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.LabelMetaId where + prt _ (Language.EO.Phi.Syntax.Abs.LabelMetaId i) = doc $ showString i +instance Print Language.EO.Phi.Syntax.Abs.TailMetaId where + prt _ (Language.EO.Phi.Syntax.Abs.TailMetaId i) = doc $ showString i +instance Print Language.EO.Phi.Syntax.Abs.BindingsMetaId where + prt _ (Language.EO.Phi.Syntax.Abs.BindingsMetaId i) = doc $ showString i +instance Print Language.EO.Phi.Syntax.Abs.ObjectMetaId where + prt _ (Language.EO.Phi.Syntax.Abs.ObjectMetaId i) = doc $ showString i +instance Print Language.EO.Phi.Syntax.Abs.BytesMetaId where + prt _ (Language.EO.Phi.Syntax.Abs.BytesMetaId i) = doc $ showString i instance Print Language.EO.Phi.Syntax.Abs.MetaFunctionName where prt _ (Language.EO.Phi.Syntax.Abs.MetaFunctionName 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 "{"), doc (showString "\10214"), prt 0 bindings, doc (showString "\10215"), doc (showString "}")]) +instance Print Language.EO.Phi.Syntax.Abs.MetaId where + prt i = \case + Language.EO.Phi.Syntax.Abs.MetaIdLabel labelmetaid -> prPrec i 0 (concatD [prt 0 labelmetaid]) + Language.EO.Phi.Syntax.Abs.MetaIdTail tailmetaid -> prPrec i 0 (concatD [prt 0 tailmetaid]) + Language.EO.Phi.Syntax.Abs.MetaIdBindings bindingsmetaid -> prPrec i 0 (concatD [prt 0 bindingsmetaid]) + Language.EO.Phi.Syntax.Abs.MetaIdObject objectmetaid -> prPrec i 0 (concatD [prt 0 objectmetaid]) + Language.EO.Phi.Syntax.Abs.MetaIdBytes bytesmetaid -> prPrec i 0 (concatD [prt 0 bytesmetaid]) + 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")]) @@ -162,8 +178,8 @@ instance Print Language.EO.Phi.Syntax.Abs.Object where Language.EO.Phi.Syntax.Abs.ThisObject -> prPrec i 0 (concatD [doc (showString "\958")]) Language.EO.Phi.Syntax.Abs.Termination -> prPrec i 0 (concatD [doc (showString "\8869")]) Language.EO.Phi.Syntax.Abs.MetaSubstThis object1 object2 -> prPrec i 0 (concatD [prt 0 object1, doc (showString "["), doc (showString "\958"), doc (showString "\8614"), prt 0 object2, doc (showString "]")]) - Language.EO.Phi.Syntax.Abs.MetaObject metaid -> prPrec i 0 (concatD [prt 0 metaid]) - Language.EO.Phi.Syntax.Abs.MetaTailContext object metaid -> prPrec i 0 (concatD [prt 0 object, doc (showString "*"), prt 0 metaid]) + Language.EO.Phi.Syntax.Abs.MetaObject objectmetaid -> prPrec i 0 (concatD [prt 0 objectmetaid]) + Language.EO.Phi.Syntax.Abs.MetaTailContext object tailmetaid -> prPrec i 0 (concatD [prt 0 object, doc (showString "*"), prt 0 tailmetaid]) Language.EO.Phi.Syntax.Abs.MetaFunction metafunctionname object -> prPrec i 0 (concatD [prt 0 metafunctionname, doc (showString "("), prt 0 object, doc (showString ")")]) instance Print Language.EO.Phi.Syntax.Abs.Binding where @@ -173,8 +189,8 @@ instance Print Language.EO.Phi.Syntax.Abs.Binding where 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.DeltaEmptyBinding -> prPrec i 0 (concatD [doc (showString "\916"), doc (showString "\10509"), doc (showString "\8709")]) 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]) - Language.EO.Phi.Syntax.Abs.MetaDeltaBinding metaid -> prPrec i 0 (concatD [doc (showString "\916"), doc (showString "\10509"), prt 0 metaid]) + Language.EO.Phi.Syntax.Abs.MetaBindings bindingsmetaid -> prPrec i 0 (concatD [prt 0 bindingsmetaid]) + Language.EO.Phi.Syntax.Abs.MetaDeltaBinding bytesmetaid -> prPrec i 0 (concatD [doc (showString "\916"), doc (showString "\10509"), prt 0 bytesmetaid]) instance Print [Language.EO.Phi.Syntax.Abs.Binding] where prt _ [] = concatD [] @@ -187,7 +203,7 @@ instance Print Language.EO.Phi.Syntax.Abs.Attribute where Language.EO.Phi.Syntax.Abs.Rho -> prPrec i 0 (concatD [doc (showString "\961")]) 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]) + Language.EO.Phi.Syntax.Abs.MetaAttr labelmetaid -> prPrec i 0 (concatD [prt 0 labelmetaid]) instance Print Language.EO.Phi.Syntax.Abs.RuleAttribute where prt i = \case diff --git a/eo-phi-normalizer/test/Language/EO/Rules/PhiPaperSpec.hs b/eo-phi-normalizer/test/Language/EO/Rules/PhiPaperSpec.hs index 594b87f3..892b6766 100644 --- a/eo-phi-normalizer/test/Language/EO/Rules/PhiPaperSpec.hs +++ b/eo-phi-normalizer/test/Language/EO/Rules/PhiPaperSpec.hs @@ -51,8 +51,18 @@ instance Arbitrary Bytes where arbitrary = intToBytes <$> arbitrarySizedNatural instance Arbitrary Phi.Function where arbitrary = Phi.Function <$> arbitraryNonEmptyString -instance Arbitrary Phi.MetaId where - arbitrary = Phi.MetaId . ("!" ++) <$> arbitraryNonEmptyString + +instance Arbitrary Phi.ObjectMetaId where + arbitrary = Phi.ObjectMetaId . ("!b" ++) <$> arbitraryNonEmptyString +instance Arbitrary Phi.LabelMetaId where + arbitrary = Phi.LabelMetaId . ("!τ" ++) <$> arbitraryNonEmptyString +instance Arbitrary Phi.BindingsMetaId where + arbitrary = Phi.BindingsMetaId . ("!B" ++) <$> arbitraryNonEmptyString +instance Arbitrary Phi.TailMetaId where + arbitrary = Phi.TailMetaId . ("!t" ++) <$> arbitraryNonEmptyString +instance Arbitrary Phi.BytesMetaId where + arbitrary = Phi.BytesMetaId . ("!y" ++) <$> arbitraryNonEmptyString + instance Arbitrary Phi.MetaFunctionName where arbitrary = Phi.MetaFunctionName . ("@" ++) <$> arbitraryNonEmptyString From a2ce78ea2254637b0113efe014f65ecded6fe5f7 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Fri, 19 Jul 2024 14:01:45 +0300 Subject: [PATCH 11/12] Update identifier names in yegor.yaml --- .../test/eo/phi/rules/yegor.yaml | 60 +++++++++---------- 1 file changed, 30 insertions(+), 30 deletions(-) diff --git a/eo-phi-normalizer/test/eo/phi/rules/yegor.yaml b/eo-phi-normalizer/test/eo/phi/rules/yegor.yaml index 0018fc03..b43f8e1d 100644 --- a/eo-phi-normalizer/test/eo/phi/rules/yegor.yaml +++ b/eo-phi-normalizer/test/eo/phi/rules/yegor.yaml @@ -39,11 +39,11 @@ rules: - name: ξ-dispatch description: 'ξ-dispatch' context: - current_object: '!obj' + current_object: '!b' pattern: | ξ result: | - !obj + !b when: - apply_in_subformations: false # - present_attrs: @@ -58,12 +58,12 @@ rules: - name: R_DOT description: 'Accessing an α-binding' pattern: | - ⟦ !a ↦ !n, !B ⟧.!a + ⟦ !τ ↦ !b, !B ⟧.!τ result: | - !n[ ξ ↦ ⟦ !a ↦ !n, !B ⟧ ] + !b[ ξ ↦ ⟦ !τ ↦ !b, !B ⟧ ] when: - apply_in_abstract_subformations: false - - nf_inside_formation: '!n' + - nf_inside_formation: '!b' - nf: '⟦ !B ⟧' tests: - name: Should match @@ -76,9 +76,9 @@ rules: # - name: Rule 6a # description: 'Accessing an α-binding (for object with ρ ↦ ∅)' # pattern: | - # ⟦ !a ↦ !n, ρ ↦ ∅, !B ⟧.!a + # ⟦ !τ ↦ !b, ρ ↦ ∅, !B ⟧.!τ # result: | - # !n[ ξ ↦ ⟦ !a ↦ !n, ρ ↦ ∅, !B ⟧ ] + # !b[ ξ ↦ ⟦ !τ ↦ !b, ρ ↦ ∅, !B ⟧ ] # when: [] # tests: # - name: Should match @@ -94,13 +94,13 @@ rules: # i.e., doesn't match an empty binding after an attached one. # We should instead match the first two empty bindings. pattern: | - ⟦ !a ↦ ∅, !b ↦ ∅, !B ⟧(α0 ↦ !n0, α1 ↦ !n1) + ⟦ !τ1 ↦ ∅, !τ2 ↦ ∅, !B ⟧(α0 ↦ !b0, α1 ↦ !b1) result: | - ⟦ !a ↦ !n0, !b ↦ !n1, !B ⟧ + ⟦ !τ1 ↦ !b0, !τ2 ↦ !b1, !B ⟧ when: - apply_in_abstract_subformations: false - - nf: '!n0' - - nf: '!n1' + - nf: '!b0' + - nf: '!b1' tests: [] - name: R_COPY1 @@ -109,31 +109,31 @@ rules: # i.e., doesn't match an empty binding after an attached one. # We should instead match the first empty binding. pattern: | - ⟦ !a ↦ ∅, !B ⟧(α0 ↦ !n) + ⟦ !τ ↦ ∅, !B ⟧(α0 ↦ !b) result: | - ⟦ !a ↦ !n, !B ⟧ + ⟦ !τ ↦ !b, !B ⟧ when: - apply_in_abstract_subformations: false - - nf: '!n' + - nf: '!b' tests: [] - name: R_COPY description: 'Application of α-binding' pattern: | - ⟦ !a ↦ ∅, !B ⟧(!a ↦ !n) + ⟦ !τ ↦ ∅, !B ⟧(!τ ↦ !b) result: | - ⟦ !a ↦ !n, !B ⟧ + ⟦ !τ ↦ !b, !B ⟧ when: - apply_in_abstract_subformations: false - - nf: '!n' + - nf: '!b' tests: [] - name: R_COPY_Δ description: 'Application of Δ-binding' pattern: | - ⟦ Δ ⤍ ∅, !B ⟧(Δ ⤍ !bytes) + ⟦ Δ ⤍ ∅, !B ⟧(Δ ⤍ !y) result: | - ⟦ Δ ⤍ !bytes, !B ⟧ + ⟦ Δ ⤍ !y, !B ⟧ when: - apply_in_abstract_subformations: false tests: [] @@ -141,15 +141,15 @@ rules: - name: R_φ description: 'Accessing a decorated object' pattern: | - ⟦!B ⟧.!a + ⟦!B ⟧.!τ result: | - ⟦!B ⟧.φ.!a + ⟦!B ⟧.φ.!τ when: - present_attrs: attrs: ['φ'] bindings: ['!B'] - absent_attrs: - attrs: ['!a'] + attrs: ['!τ'] bindings: ['!B'] tests: - name: 'Attribute does not exist' @@ -161,10 +161,10 @@ rules: - name: R_MISS description: 'Invalid application' - pattern: ⟦ !t ↦ !b1, !B1 ⟧(!t ↦ !b2, !B2) + pattern: ⟦ !τ ↦ !b1, !B1 ⟧(!τ ↦ !b2, !B2) result: ⊥ when: - - not_equal: ['!t', 'ρ'] + - not_equal: ['!τ', 'ρ'] tests: - name: '' input: '⟦ t ↦ ⟦ a ↦ ∅ ⟧ ⟧(t ↦ ⟦ b ↦ ∅ ⟧)' @@ -172,7 +172,7 @@ rules: - name: R_OVER description: 'Invalid application (attribute already attached)' - pattern: ⟦ !t ↦ !b1, !B1 ⟧(!t ↦ !b2, !B2) + pattern: ⟦ !τ ↦ !b1, !B1 ⟧(!τ ↦ !b2, !B2) result: ⊥ when: [] tests: @@ -182,11 +182,11 @@ rules: - name: R_MISS description: 'Invalid application (absent attribute)' - pattern: ⟦ !B1 ⟧(!t ↦ !b2, !B2) + pattern: ⟦ !B1 ⟧(!τ ↦ !b2, !B2) result: ⊥ when: - absent_attrs: - attrs: ['!t', 'φ', 'λ'] + attrs: ['!τ', 'φ', 'λ'] bindings: ['!B1'] tests: - name: '' @@ -196,12 +196,12 @@ rules: - name: R_STOP description: 'Invalid attribute access' pattern: | - ⟦ !B ⟧.!a + ⟦ !B ⟧.!τ result: | ⊥ when: - absent_attrs: - attrs: ['!a', 'φ', 'λ'] + attrs: ['!τ', 'φ', 'λ'] bindings: ['!B'] - present_attrs: attrs: ['ρ'] @@ -215,7 +215,7 @@ rules: - name: R_DD description: 'Accessing an attribute on bottom' pattern: | - ⊥.!a + ⊥.!τ result: | ⊥ when: [] From cc287a7fd47fee47af8a5ea318ee63192f795d50 Mon Sep 17 00:00:00 2001 From: Danila Danko Date: Fri, 19 Jul 2024 14:59:30 +0300 Subject: [PATCH 12/12] refactor(normalizer): make fourmolu happy --- .../src/Language/EO/Phi/Rules/Yaml.hs | 28 ++++++++++--------- 1 file changed, 15 insertions(+), 13 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 2484e133..6a0c92cc 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs +++ b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs @@ -8,10 +8,10 @@ {-# LANGUAGE QuasiQuotes #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE TypeApplications #-} +{-# OPTIONS_GHC -Wno-forall-identifier #-} {-# OPTIONS_GHC -Wno-orphans #-} {-# OPTIONS_GHC -Wno-partial-fields #-} {-# OPTIONS_GHC -Wno-type-defaults #-} -{-# OPTIONS_GHC -Wno-forall-identifier #-} module Language.EO.Phi.Rules.Yaml where @@ -23,17 +23,17 @@ import Data.Coerce (coerce) import Data.List (intercalate) import Data.List.NonEmpty qualified as NonEmpty import Data.Maybe (fromMaybe) +import Data.Set (Set) +import Data.Set qualified as Set import Data.String (IsString (..)) import Data.Yaml qualified as Yaml import GHC.Generics (Generic) -import Data.Set (Set) -import qualified Data.Set as Set -import Language.EO.Phi ( printTree ) +import Language.EO.Phi (printTree) import Language.EO.Phi.Rules.Common (Context (..), NamedRule) import Language.EO.Phi.Rules.Common qualified as Common -import PyF (fmt) import Language.EO.Phi.Syntax.Abs +import PyF (fmt) -- $setup -- >>> :set -XOverloadedStrings @@ -120,8 +120,9 @@ convertRule :: Rule -> Common.Rule convertRule Rule{..} ctx obj = do -- first validate pattern and result in the rule -- TODO: we should perform this check once, not every time we run the rule - let freshMetaIds = Set.mapMonotonic MetaIdLabel $ - foldMap (Set.fromList . map (\FreshMetaId{name=x} -> x)) fresh + let freshMetaIds = + Set.mapMonotonic MetaIdLabel $ + foldMap (Set.fromList . map (\FreshMetaId{name = x} -> x)) fresh patternMetaIds = objectMetaIds pattern resultMetaIds = objectMetaIds result @@ -175,24 +176,25 @@ mkFreshSubst ctx obj metas = mkFreshAttributes :: Set LabelId -> [FreshMetaId] -> [(LabelMetaId, Attribute)] mkFreshAttributes _ids [] = [] -mkFreshAttributes ids (x:xs) = +mkFreshAttributes ids (x : xs) = case mkFreshAttribute ids x of (ma, ids') -> ma : mkFreshAttributes ids' xs mkFreshAttribute :: Set LabelId -> FreshMetaId -> ((LabelMetaId, Attribute), Set LabelId) mkFreshAttribute ids FreshMetaId{..} = ((name, Label label), Set.insert label ids) - where - label = head + where + label = + head [ l - | i <- [1..] + | i <- [1 ..] , let l = LabelId (fromMaybe "tmp" prefix <> "$" <> show i) , l `Set.notMember` ids ] usedLabelIds :: Context -> Set LabelId usedLabelIds Context{..} = objectLabelIds globalObject - where - globalObject = NonEmpty.last outerFormations + where + globalObject = NonEmpty.last outerFormations objectLabelIds :: Object -> Set LabelId objectLabelIds = \case