diff --git a/.vscode/settings.json b/.vscode/settings.json index 3382fe47a..661499a77 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -1,7 +1,10 @@ { - "haskell.formattingProvider": "fourmolu", - "editor.formatOnSave": true, - "files.insertFinalNewline": true, - "files.trimFinalNewlines": true, - "files.trimTrailingWhitespace": true + "haskell.formattingProvider": "fourmolu", + "[haskell]": { + "editor.defaultFormatter": "haskell.haskell" + }, + "editor.formatOnSave": true, + "files.insertFinalNewline": true, + "files.trimFinalNewlines": true, + "files.trimTrailingWhitespace": true } diff --git a/eo-phi-normalizer/Setup.hs b/eo-phi-normalizer/Setup.hs index 4c895d998..fad5c0cbd 100644 --- a/eo-phi-normalizer/Setup.hs +++ b/eo-phi-normalizer/Setup.hs @@ -20,7 +20,7 @@ main = defaultMainWithHooks $ simpleUserHooks { hookedPrograms = [ bnfcProgram ] , postConf = \args flags packageDesc localBuildInfo -> do #ifndef mingw32_HOST_OS - _ <- system "bnfc -d -p Language.EO.Phi --generic -o src/ grammar/EO/Phi/Syntax.cf" + _ <- system "bnfc --haskell -d -p Language.EO.Phi --generic -o src/ grammar/EO/Phi/Syntax.cf" #endif postConf simpleUserHooks args flags packageDesc localBuildInfo } diff --git a/eo-phi-normalizer/app/Main.hs b/eo-phi-normalizer/app/Main.hs index 9fa108c46..1cb77b0bc 100644 --- a/eo-phi-normalizer/app/Main.hs +++ b/eo-phi-normalizer/app/Main.hs @@ -1,6 +1,71 @@ -module Main (main) where +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedRecordDot #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RecordWildCards #-} +{-# OPTIONS_GHC -Wno-type-defaults #-} -import Language.EO.Phi +module Main where + +import Control.Monad (when) +import Data.Foldable (forM_) + +import Data.List (nub) +import Language.EO.Phi (Object (Formation), Program (Program), defaultMain, parseProgram, printTree) +import Language.EO.Phi.Rules.Common (Context (..), applyRules, applyRulesChain) +import Language.EO.Phi.Rules.Yaml +import Options.Generic + +data CLINamedParams = CLINamedParams + { chain :: Bool + , rulesYaml :: Maybe String + , outPath :: Maybe String + } + deriving (Generic, Show, ParseRecord, Read, ParseField) + +instance ParseFields CLINamedParams where + parseFields _ _ _ _ = + CLINamedParams + <$> parseFields (Just "Print out steps of reduction") (Just "chain") (Just 'c') Nothing + <*> parseFields (Just "Path to the Yaml file with custom rules") (Just "rules-yaml") Nothing Nothing + <*> parseFields (Just "Output file path (defaults to stdout)") (Just "output") (Just 'o') Nothing + +data CLIOptions = CLIOptions CLINamedParams (Maybe FilePath) + deriving (Generic, Show, ParseRecord) main :: IO () -main = defaultMain +main = do + opts <- getRecord "Normalizer" + let (CLIOptions params inPath) = opts + let (CLINamedParams{..}) = params + Control.Monad.when chain (putStrLn "Sorry, --chain is not implemented yet 😅") + case rulesYaml of + Just path -> do + ruleSet <- parseRuleSetFromFile path + putStrLn ruleSet.title + src <- maybe getContents readFile inPath + let progOrError = parseProgram src + case progOrError of + Left err -> error ("An error occurred parsing the input program: " <> err) + Right input@(Program bindings) -> do + let results + | chain = applyRulesChain (Context (convertRule <$> ruleSet.rules)) (Formation bindings) + | otherwise = pure <$> applyRules (Context (convertRule <$> ruleSet.rules)) (Formation bindings) + uniqueResults = nub results + totalResults = length uniqueResults + -- TODO: use outPath to output to file if provided + putStrLn "Input:" + putStrLn (printTree input) + putStrLn "====================================================" + forM_ (zip [1 ..] uniqueResults) $ \(i, steps) -> do + putStrLn $ + "Result " <> show i <> " out of " <> show totalResults <> ":" + let n = length steps + forM_ (zip [1 ..] steps) $ \(k, step) -> do + Control.Monad.when chain $ do + putStr ("[ " <> show k <> " / " <> show n <> " ]") + putStrLn (printTree step) + putStrLn "----------------------------------------------------" + -- TODO: still need to consider `chain` + Nothing -> defaultMain diff --git a/eo-phi-normalizer/eo-phi-normalizer.cabal b/eo-phi-normalizer/eo-phi-normalizer.cabal index c0583a510..036021d70 100644 --- a/eo-phi-normalizer/eo-phi-normalizer.cabal +++ b/eo-phi-normalizer/eo-phi-normalizer.cabal @@ -36,6 +36,7 @@ library Language.EO.Phi.Normalize Language.EO.Phi.Rules.Common Language.EO.Phi.Rules.PhiPaper + Language.EO.Phi.Rules.Yaml Language.EO.Phi.Syntax Language.EO.Phi.Syntax.Abs Language.EO.Phi.Syntax.Lex @@ -45,6 +46,8 @@ library Paths_eo_phi_normalizer hs-source-dirs: src + default-extensions: + ImportQualifiedPost ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -Wno-missing-export-lists -Werror build-tools: alex >=3.2.4 @@ -68,6 +71,8 @@ executable normalize-phi Paths_eo_phi_normalizer hs-source-dirs: app + default-extensions: + ImportQualifiedPost ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -Wno-missing-export-lists -Werror -threaded -rtsopts -with-rtsopts=-N build-tools: alex >=3.2.4 @@ -82,6 +87,7 @@ executable normalize-phi , eo-phi-normalizer , filepath , mtl + , optparse-generic , string-interpolate , yaml default-language: Haskell2010 @@ -91,10 +97,14 @@ test-suite eo-phi-normalizer-test main-is: Spec.hs other-modules: Language.EO.PhiSpec + Language.EO.YamlSpec Test.EO.Phi + Test.EO.Yaml Paths_eo_phi_normalizer hs-source-dirs: test + default-extensions: + ImportQualifiedPost ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -Wno-missing-export-lists -Werror -threaded -rtsopts -with-rtsopts=-N build-tools: alex >=3.2.4 diff --git a/eo-phi-normalizer/grammar/EO/Phi/Syntax.cf b/eo-phi-normalizer/grammar/EO/Phi/Syntax.cf index 27d795e7c..25669d8ad 100644 --- a/eo-phi-normalizer/grammar/EO/Phi/Syntax.cf +++ b/eo-phi-normalizer/grammar/EO/Phi/Syntax.cf @@ -8,6 +8,7 @@ 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,.|':;!-?][}{)(⟧⟦"])* ; Program. Program ::= "{" [Binding] "}" ; @@ -17,11 +18,13 @@ ObjectDispatch. Object ::= Object "." Attribute ; GlobalDispatch. Object ::= "Φ" "." Attribute ; ThisDispatch. Object ::= "ξ" "." Attribute ; Termination. Object ::= "⊥" ; +MetaObject. Object ::= MetaId ; AlphaBinding. Binding ::= Attribute "↦" Object ; EmptyBinding. Binding ::= Attribute "↦" "∅" ; DeltaBinding. Binding ::= "Δ" "⤍" Bytes ; LambdaBinding. Binding ::= "λ" "⤍" Function ; +MetaBindings. Binding ::= MetaId ; separator Binding "," ; Phi. Attribute ::= "φ" ; -- decoratee object @@ -30,6 +33,7 @@ Sigma. Attribute ::= "σ" ; -- home object VTX. Attribute ::= "ν" ; -- the vertex identifier (an object that represents the unique identifier of the containing object) Label. Attribute ::= LabelId ; Alpha. Attribute ::= AlphaIndex ; +MetaAttr. Attribute ::= MetaId ; PeeledObject. PeeledObject ::= ObjectHead [ObjectAction] ; diff --git a/eo-phi-normalizer/grammar/EO/Phi/Syntax.old.cf b/eo-phi-normalizer/grammar/EO/Phi/Syntax.old.cf deleted file mode 100644 index 86996b16a..000000000 --- a/eo-phi-normalizer/grammar/EO/Phi/Syntax.old.cf +++ /dev/null @@ -1,49 +0,0 @@ --- ========================================================== --- BNFC grammar for φ-programs (translated from EO) --- ========================================================== --- --- This grammar is a (manual) translation of Phi.g4 grammar from objectionary/eo: --- https://github.com/objectionary/eo/blob/fa24c7cc47e1ac473fb930f3a08ccc4d88d9d1e3/eo-parser/src/main/antlr4/org/eolang/parser/Phi.g4 - -token Bytes ({"--"} | ["0123456789ABCDEF"] ["0123456789ABCDEF"] ({"-"} ["0123456789ABCDEF"] ["0123456789ABCDEF"])* {"--"}) ; -token Function upper (char - [" \r\n\t,.|':;!-?][}{)(⟧⟦"])* ; -token LabelId lower (char - [" \r\n\t,.|':;!-?][}{)(⟧⟦"])* ; -token AlphaIndex ({"α0"} | {"α"} (digit - ["0"]) (digit)* ) ; - -Program. Program ::= "{" [Binding] "}" ; - -Formation. Object ::= "{" [Binding] "}" ; -Application. Object ::= AbstractObject "{" [Binding] "}" [Bindings] ; -Dispatch. Object ::= Dispatch ; -Termination. Object ::= "⊥"; - -AbstractFormation. AbstractObject ::= "{" [Binding] "}" ; -AbstractDispatch. AbstractObject ::= Dispatch ; -AbstractTermination. AbstractObject ::= "⊥" ; - -DispatchedFormation. DispatchedObject ::= "{" [Binding] "}" ; -DispatchedTermination. DispatchedObject ::= "⊥" ; - -AlphaBinding. Binding ::= Attribute "↦" Object ; -EmptyBinding. Binding ::= Attribute "↦" "∅" ; -DeltaBinding. Binding ::= "Δ" "⤍" Bytes ; -LambdaBinding. Binding ::= "λ" "⤍" Function ; -separator Binding "," ; - -Bindings. Bindings ::= "{" [Binding] "}" ; -separator Bindings "" ; - -ObjectDispatch. Dispatch ::= DispatchedObject [Bindings] "." [Attribute] [Disp] ; -GlobalDispatch. Dispatch ::= "Φ" "." [Attribute] [Disp] ; -ThisDispatch. Dispatch ::= "ξ" "." [Attribute] [Disp] ; - -Phi. Attribute ::= "φ" ; -- decoratee object -Rho. Attribute ::= "ρ" ; -- parent object -Sigma. Attribute ::= "σ" ; -- ??? -VTX. Attribute ::= "ν" ; -- ??? -Label. Attribute ::= LabelId ; -Alpha. Attribute ::= AlphaIndex ; -separator nonempty Attribute "." ; - -Disp. Disp ::= "{" [Binding] "}" Bindings "." [Attribute] ; -separator Disp "" ; diff --git a/eo-phi-normalizer/package.yaml b/eo-phi-normalizer/package.yaml index 5bbca3dd8..e738933bb 100644 --- a/eo-phi-normalizer/package.yaml +++ b/eo-phi-normalizer/package.yaml @@ -44,6 +44,9 @@ dependencies: - mtl - string-interpolate +default-extensions: +- ImportQualifiedPost + ghc-options: - -Wall - -Wcompat @@ -65,6 +68,9 @@ library: - Language.EO.Phi.Syntax.Test - Language.EO.Phi.Syntax.ErrM - Language.EO.Phi.Syntax.Skel + - Language.EO.Phi.Rules.Syntax.Test + - Language.EO.Phi.Rules.Syntax.ErrM + - Language.EO.Phi.Rules.Syntax.Skel executables: normalize-phi: @@ -76,6 +82,8 @@ executables: - -with-rtsopts=-N dependencies: - eo-phi-normalizer + - optparse-generic + tests: eo-phi-normalizer-test: diff --git a/eo-phi-normalizer/src/Language/EO/Phi.hs b/eo-phi-normalizer/src/Language/EO/Phi.hs index 9e334fa74..f400eb57b 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi.hs +++ b/eo-phi-normalizer/src/Language/EO/Phi.hs @@ -1,3 +1,6 @@ +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE OverloadedStrings #-} + module Language.EO.Phi ( defaultMain, normalize, @@ -8,8 +11,8 @@ module Language.EO.Phi ( import System.Exit (exitFailure) -import qualified Language.EO.Phi.Syntax.Abs as Phi -import qualified Language.EO.Phi.Syntax.Par as Phi +import Language.EO.Phi.Syntax.Abs qualified as Phi +import Language.EO.Phi.Syntax.Par qualified as Phi import Language.EO.Phi.Normalize import Language.EO.Phi.Syntax diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs b/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs index d31075b71..e042e483c 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs +++ b/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs @@ -92,6 +92,7 @@ peelObject = \case GlobalDispatch attr -> PeeledObject HeadGlobal [ActionDispatch attr] ThisDispatch attr -> PeeledObject HeadThis [ActionDispatch attr] Termination -> PeeledObject HeadTermination [] + MetaObject _ -> PeeledObject HeadTermination [] where followedBy (PeeledObject object actions) action = PeeledObject object (actions ++ [action]) 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 0e3e8bc79..645c0aa1c 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs +++ b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs @@ -1,27 +1,51 @@ {-# LANGUAGE LambdaCase #-} {-# LANGUAGE RecordWildCards #-} +{-# OPTIONS_GHC -Wno-orphans #-} module Language.EO.Phi.Rules.Common where import Control.Applicative (Alternative ((<|>)), asum) +import Data.String (IsString (..)) import Language.EO.Phi.Syntax.Abs +import Language.EO.Phi.Syntax.Lex (Token) +import Language.EO.Phi.Syntax.Par -- $setup -- >>> :set -XOverloadedStrings -- >>> import Language.EO.Phi.Syntax +instance IsString Program where fromString = unsafeParseWith pProgram +instance IsString Object where fromString = unsafeParseWith pObject +instance IsString Binding where fromString = unsafeParseWith pBinding +instance IsString Attribute where fromString = unsafeParseWith pAttribute +instance IsString PeeledObject where fromString = unsafeParseWith pPeeledObject +instance IsString ObjectHead where fromString = unsafeParseWith pObjectHead + +parseWith :: ([Token] -> Either String a) -> String -> Either String a +parseWith parser input = parser tokens + where + tokens = myLexer input + +-- | Parse a 'Object' from a 'String'. +-- May throw an 'error` if input has a syntactical or lexical errors. +unsafeParseWith :: ([Token] -> Either String a) -> String -> a +unsafeParseWith parser input = + case parseWith parser input of + Left parseError -> error parseError + Right object -> object + data Context = Context { allRules :: [Rule] } -- | A rule tries to apply a transformation to the root object, if possible. -type Rule = Context -> Object -> Maybe Object +type Rule = Context -> Object -> [Object] applyOneRuleAtRoot :: Context -> Object -> [Object] applyOneRuleAtRoot ctx@Context{..} obj = [ obj' | rule <- allRules - , Just obj' <- [rule ctx obj] + , obj' <- rule ctx obj ] withSubObject :: (Object -> [Object]) -> Object -> [Object] @@ -39,6 +63,7 @@ withSubObject f root = GlobalDispatch{} -> [] ThisDispatch{} -> [] Termination -> [] + MetaObject _ -> [] withSubObjectBindings :: (Object -> [Object]) -> [Binding] -> [[Binding]] withSubObjectBindings _ [] = [] @@ -54,6 +79,7 @@ withSubObjectBinding f = \case EmptyBinding{} -> [] DeltaBinding{} -> [] LambdaBinding{} -> [] + MetaBindings _ -> [] applyOneRule :: Context -> Object -> [Object] applyOneRule = withSubObject . applyOneRuleAtRoot diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Rules/PhiPaper.hs b/eo-phi-normalizer/src/Language/EO/Phi/Rules/PhiPaper.hs index 438165b3f..f8b463aba 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Rules/PhiPaper.hs +++ b/eo-phi-normalizer/src/Language/EO/Phi/Rules/PhiPaper.hs @@ -13,8 +13,8 @@ rule1 :: Rule rule1 _ = \case Formation bindings -> let Program bindings' = normalize (Program bindings) - in Just (Formation bindings') - _ -> Nothing + in [Formation bindings'] + _ -> [] -- | Rule 6. rule6 :: Rule @@ -26,4 +26,4 @@ rule6 ctx (ObjectDispatch (Formation bindings) a) bindings' = filter (not . isDispatched) bindings isDispatched (AlphaBinding a' _) = a == a' isDispatched _ = False -rule6 _ _ = Nothing +rule6 _ _ = [] diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs new file mode 100644 index 000000000..92a0a271f --- /dev/null +++ b/eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs @@ -0,0 +1,200 @@ +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DuplicateRecordFields #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE RecordWildCards #-} +{-# OPTIONS_GHC -Wno-orphans #-} + +module Language.EO.Phi.Rules.Yaml where + +import Data.Aeson (FromJSON (..)) +import Data.Coerce (coerce) +import Data.Maybe (fromMaybe) +import Data.String (IsString (..)) +import Data.Yaml qualified as Yaml +import GHC.Generics (Generic) +import Language.EO.Phi.Rules.Common qualified as Common +import Language.EO.Phi.Syntax.Abs + +instance FromJSON Object where parseJSON = fmap fromString . parseJSON +instance FromJSON MetaId where parseJSON = fmap MetaId . parseJSON + +data RuleSet = RuleSet + { title :: String + , rules :: [Rule] + } + deriving (Generic, FromJSON, Show) + +data Rule = Rule + { name :: String + , description :: String + , pattern :: Object + , result :: Object + , when :: [Condition] + , tests :: [RuleTest] + } + deriving (Generic, FromJSON, Show) + +data RuleTest = RuleTest + { name :: String + , input :: Object + , output :: Object + , matches :: Bool + } + deriving (Generic, FromJSON, Show) + +data Condition = IsNF {nf :: [MetaId]} + deriving (Generic, FromJSON, Show) + +parseRuleSetFromFile :: FilePath -> IO RuleSet +parseRuleSetFromFile = Yaml.decodeFileThrow + +convertRule :: Rule -> Common.Rule +convertRule Rule{..} _ctx obj = + [ obj' + | subst <- matchObject pattern obj + , obj' <- [applySubst subst result] + -- TODO: check that obj' does not have any metavariables + ] + +-- input: ⟦ a ↦ ⟦ c ↦ ⟦ ⟧ ⟧, b ↦ ⟦ ⟧ ⟧.a + +-- pattern: ⟦ !a ↦ !n, !B ⟧.!a +-- result: !n(ρ ↦ ⟦ !B ⟧) + +-- match pattern input (get substitution): +-- !a = a +-- !n = ⟦ c ↦ ⟦ ⟧ ⟧ +-- !B = b ↦ ⟦ ⟧ + +-- actual result (after applying substitution): +-- ⟦ c ↦ ⟦ ⟧ ⟧(ρ ↦ ⟦ b ↦ ⟦ ⟧ ⟧) + +data Subst = Subst + { objectMetas :: [(MetaId, Object)] + , bindingsMetas :: [(MetaId, [Binding])] + , attributeMetas :: [(MetaId, Attribute)] + } + deriving (Show) + +instance Semigroup Subst where + (<>) = mergeSubst + +instance Monoid Subst where + mempty = emptySubst + +emptySubst :: Subst +emptySubst = Subst [] [] [] + +-- >>> putStrLn $ Language.EO.Phi.printTree (applySubst (Subst [("!n", "⟦ c ↦ ⟦ ⟧ ⟧")] [("!B", ["b ↦ ⟦ ⟧"])] [("!a", "a")]) "!n(ρ ↦ ⟦ !B ⟧)" :: Object) +-- ⟦ c ↦ ⟦ ⟧ ⟧ (ρ ↦ ⟦ b ↦ ⟦ ⟧ ⟧) +applySubst :: Subst -> Object -> Object +applySubst subst@Subst{..} = \case + Formation bindings -> + Formation (applySubstBindings subst bindings) + Application obj bindings -> + Application (applySubst subst obj) (applySubstBindings subst bindings) + ObjectDispatch obj a -> + ObjectDispatch (applySubst subst obj) (applySubstAttr subst a) + GlobalDispatch a -> + GlobalDispatch (applySubstAttr subst a) + ThisDispatch a -> + ThisDispatch (applySubstAttr subst a) + obj@(MetaObject x) -> fromMaybe obj $ lookup x objectMetas + obj -> obj + +applySubstAttr :: Subst -> Attribute -> Attribute +applySubstAttr Subst{..} = \case + attr@(MetaAttr x) -> fromMaybe attr $ lookup x attributeMetas + attr -> attr + +applySubstBindings :: Subst -> [Binding] -> [Binding] +applySubstBindings subst = concatMap (applySubstBinding subst) + +applySubstBinding :: Subst -> Binding -> [Binding] +applySubstBinding subst@Subst{..} = \case + AlphaBinding a obj -> + [AlphaBinding (applySubstAttr subst a) (applySubst subst obj)] + EmptyBinding a -> + [EmptyBinding (applySubstAttr subst a)] + DeltaBinding bytes -> [DeltaBinding (coerce bytes)] + LambdaBinding bytes -> [LambdaBinding (coerce bytes)] + b@(MetaBindings m) -> fromMaybe [b] (lookup m bindingsMetas) + +mergeSubst :: Subst -> Subst -> Subst +mergeSubst (Subst xs ys zs) (Subst xs' ys' zs') = + Subst (xs ++ xs') (ys ++ ys') (zs ++ zs') + +-- 1. need to implement applySubst' :: Subst -> Object -> Object +-- 2. complete the code +matchObject :: Object -> Object -> [Subst] +matchObject (Formation ps) (Formation bs) = matchBindings ps bs +matchObject (Application obj bindings) (Application obj' bindings') = do + subst1 <- matchObject obj obj' + subst2 <- matchBindings (applySubstBindings subst1 bindings) bindings' + pure (subst1 <> subst2) +matchObject (ObjectDispatch pat a) (ObjectDispatch obj a') = do + subst1 <- matchObject pat obj + subst2 <- matchAttr (applySubstAttr subst1 a) a' + pure (subst1 <> subst2) +matchObject (MetaObject m) obj = + pure + Subst + { objectMetas = [(m, obj)] + , bindingsMetas = [] + , attributeMetas = [] + } +matchObject _ _ = [] -- ? emptySubst ? + +matchBindings :: [Binding] -> [Binding] -> [Subst] +matchBindings [] [] = [emptySubst] +matchBindings [MetaBindings b] bindings = + pure + Subst + { objectMetas = [] + , bindingsMetas = [(b, bindings)] + , attributeMetas = [] + } +matchBindings (p : ps) bs = do + (bs', subst1) <- matchFindBinding p bs + subst2 <- matchBindings ps bs' + pure (subst1 <> subst2) +matchBindings [] _ = [] + +-- >>> select [1,2,3,4] +-- [(1,[2,3,4]),(2,[1,3,4]),(3,[1,2,4]),(4,[1,2,3])] +select :: [a] -> [(a, [a])] +select [] = [] +select [x] = [(x, [])] +select (x : xs) = + (x, xs) + : [ (y, x : ys) + | (y, ys) <- select xs + ] + +matchFindBinding :: Binding -> [Binding] -> [([Binding], Subst)] +matchFindBinding p bindings = + [ (leftover, subst) + | (binding, leftover) <- select bindings + , subst <- matchBinding p binding + ] + +matchBinding :: Binding -> Binding -> [Subst] +matchBinding MetaBindings{} _ = [] +matchBinding (AlphaBinding a obj) (AlphaBinding a' obj') = do + subst1 <- matchAttr a a' + subst2 <- matchObject obj obj' + pure (subst1 <> subst2) +matchBinding _ _ = [] + +matchAttr :: Attribute -> Attribute -> [Subst] +matchAttr l r | l == r = [emptySubst] +matchAttr (MetaAttr metaId) attr = + [ Subst + { objectMetas = [] + , bindingsMetas = [] + , attributeMetas = [(metaId, attr)] + } + ] +matchAttr _ _ = [] diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Syntax.hs b/eo-phi-normalizer/src/Language/EO/Phi/Syntax.hs index 3541729e4..df6734990 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax.hs +++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax.hs @@ -3,34 +3,13 @@ module Language.EO.Phi.Syntax ( module Language.EO.Phi.Syntax.Abs, - parseObject, - unsafeParseObject, printTree, ) where import Data.Char (isSpace) -import Data.String (IsString (..)) +import Language.EO.Phi.Rules.Common () import Language.EO.Phi.Syntax.Abs -import qualified Language.EO.Phi.Syntax.Abs as Phi -import qualified Language.EO.Phi.Syntax.Par as Phi -import qualified Language.EO.Phi.Syntax.Print as Phi - -instance IsString Phi.Object where - fromString = unsafeParseObject - --- | Parse a 'Object' or return a parsing error. -parseObject :: String -> Either String Phi.Object -parseObject input = Phi.pObject tokens - where - tokens = Phi.myLexer input - --- | Parse a 'Object' from a 'String'. --- May throw an 'error` if input has a syntactical or lexical errors. -unsafeParseObject :: String -> Phi.Object -unsafeParseObject input = - case parseObject input of - Left parseError -> error parseError - Right object -> object +import Language.EO.Phi.Syntax.Print qualified as Phi -- * Overriding generated pretty-printer 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 ae634d48b..ed023db0a 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Abs.hs +++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Abs.hs @@ -25,6 +25,7 @@ data Object | GlobalDispatch Attribute | ThisDispatch Attribute | Termination + | MetaObject MetaId deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic) data Binding @@ -32,10 +33,17 @@ data Binding | EmptyBinding Attribute | DeltaBinding Bytes | LambdaBinding Function + | MetaBindings MetaId deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic) data Attribute - = Phi | Rho | Sigma | VTX | Label LabelId | Alpha AlphaIndex + = Phi + | Rho + | Sigma + | VTX + | Label LabelId + | Alpha AlphaIndex + | MetaAttr MetaId deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic) data PeeledObject = PeeledObject ObjectHead [ObjectAction] @@ -61,3 +69,6 @@ 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 + deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic, Data.String.IsString) + 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 f0d529ab8..d7e8c6197 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Doc.txt +++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Doc.txt @@ -16,6 +16,7 @@ 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"])+````` @@ -30,6 +31,10 @@ 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 - [" + !'(),-.:;?[]{|}⟦⟧"])*````` + ===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. @@ -59,10 +64,12 @@ All other symbols are terminals. | | **|** | ``Φ`` ``.`` //Attribute// | | **|** | ``ξ`` ``.`` //Attribute// | | **|** | ``⊥`` + | | **|** | //MetaId// | //Binding// | -> | //Attribute// ``↦`` //Object// | | **|** | //Attribute// ``↦`` ``∅`` | | **|** | ``Δ`` ``⤍`` //Bytes// | | **|** | ``λ`` ``⤍`` //Function// + | | **|** | //MetaId// | //[Binding]// | -> | **eps** | | **|** | //Binding// | | **|** | //Binding// ``,`` //[Binding]// @@ -72,6 +79,7 @@ All other symbols are terminals. | | **|** | ``ν`` | | **|** | //LabelId// | | **|** | //AlphaIndex// + | | **|** | //MetaId// | //PeeledObject// | -> | //ObjectHead// //[ObjectAction]// | //ObjectHead// | -> | ``⟦`` //[Binding]// ``⟧`` | | **|** | ``Φ`` 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 c59d9fa5a..6b01ba126 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Lex.x +++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Lex.x @@ -55,6 +55,10 @@ $s [$u # [\t \n \r \ \! \' \( \) \, \- \. \: \; \? \[ \] \{ \| \} \⟦ \⟧]] * α 0 | α [$d # 0]$d * { tok (eitherResIdent T_AlphaIndex) } +-- token MetaId +\! [$u # [\t \n \r \ \! \' \( \) \, \- \. \: \; \? \[ \] \{ \| \} \⟦ \⟧]] * + { tok (eitherResIdent T_MetaId) } + -- Keywords and Ident $l $i* { tok (eitherResIdent TV) } @@ -76,6 +80,7 @@ data Tok | T_Function !String | T_LabelId !String | T_AlphaIndex !String + | T_MetaId !String deriving (Eq, Show, Ord) -- | Smart constructor for 'Tok' for the sake of backwards compatibility. @@ -142,6 +147,7 @@ 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 -- | Convert a token to a string. prToken :: Token -> 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 b5b530799..7a1c1b2da 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Par.y +++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Par.y @@ -63,6 +63,7 @@ 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 $$) } %% @@ -78,6 +79,9 @@ 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 } + Program :: { Language.EO.Phi.Syntax.Abs.Program } Program : '{' ListBinding '}' { Language.EO.Phi.Syntax.Abs.Program $2 } @@ -90,6 +94,7 @@ Object | 'Φ' '.' Attribute { Language.EO.Phi.Syntax.Abs.GlobalDispatch $3 } | 'ξ' '.' Attribute { Language.EO.Phi.Syntax.Abs.ThisDispatch $3 } | '⊥' { Language.EO.Phi.Syntax.Abs.Termination } + | MetaId { Language.EO.Phi.Syntax.Abs.MetaObject $1 } Binding :: { Language.EO.Phi.Syntax.Abs.Binding } Binding @@ -97,6 +102,7 @@ Binding | Attribute '↦' '∅' { Language.EO.Phi.Syntax.Abs.EmptyBinding $1 } | 'Δ' '⤍' Bytes { Language.EO.Phi.Syntax.Abs.DeltaBinding $3 } | 'λ' '⤍' Function { Language.EO.Phi.Syntax.Abs.LambdaBinding $3 } + | MetaId { Language.EO.Phi.Syntax.Abs.MetaBindings $1 } ListBinding :: { [Language.EO.Phi.Syntax.Abs.Binding] } ListBinding @@ -112,6 +118,7 @@ Attribute | 'ν' { Language.EO.Phi.Syntax.Abs.VTX } | LabelId { Language.EO.Phi.Syntax.Abs.Label $1 } | AlphaIndex { Language.EO.Phi.Syntax.Abs.Alpha $1 } + | MetaId { Language.EO.Phi.Syntax.Abs.MetaAttr $1 } PeeledObject :: { Language.EO.Phi.Syntax.Abs.PeeledObject } PeeledObject 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 f232716d3..9438f56ad 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Print.hs +++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Print.hs @@ -145,6 +145,8 @@ 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.Program where prt i = \case Language.EO.Phi.Syntax.Abs.Program bindings -> prPrec i 0 (concatD [doc (showString "{"), prt 0 bindings, doc (showString "}")]) @@ -157,6 +159,7 @@ instance Print Language.EO.Phi.Syntax.Abs.Object where Language.EO.Phi.Syntax.Abs.GlobalDispatch attribute -> prPrec i 0 (concatD [doc (showString "\934"), doc (showString "."), prt 0 attribute]) Language.EO.Phi.Syntax.Abs.ThisDispatch attribute -> prPrec i 0 (concatD [doc (showString "\958"), doc (showString "."), prt 0 attribute]) Language.EO.Phi.Syntax.Abs.Termination -> prPrec i 0 (concatD [doc (showString "\8869")]) + Language.EO.Phi.Syntax.Abs.MetaObject metaid -> prPrec i 0 (concatD [prt 0 metaid]) instance Print Language.EO.Phi.Syntax.Abs.Binding where prt i = \case @@ -164,6 +167,7 @@ instance Print Language.EO.Phi.Syntax.Abs.Binding where Language.EO.Phi.Syntax.Abs.EmptyBinding attribute -> prPrec i 0 (concatD [prt 0 attribute, doc (showString "\8614"), doc (showString "\8709")]) 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.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]) instance Print [Language.EO.Phi.Syntax.Abs.Binding] where prt _ [] = concatD [] @@ -178,6 +182,7 @@ instance Print Language.EO.Phi.Syntax.Abs.Attribute where Language.EO.Phi.Syntax.Abs.VTX -> prPrec i 0 (concatD [doc (showString "\957")]) 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]) instance Print Language.EO.Phi.Syntax.Abs.PeeledObject where prt i = \case diff --git a/eo-phi-normalizer/test/Language/EO/PhiSpec.hs b/eo-phi-normalizer/test/Language/EO/PhiSpec.hs index a2c5d5702..503540606 100644 --- a/eo-phi-normalizer/test/Language/EO/PhiSpec.hs +++ b/eo-phi-normalizer/test/Language/EO/PhiSpec.hs @@ -1,7 +1,9 @@ {-# LANGUAGE BlockArguments #-} {-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedRecordDot #-} {-# LANGUAGE QuasiQuotes #-} {-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ViewPatterns #-} module Language.EO.PhiSpec where @@ -13,21 +15,21 @@ import Language.EO.Phi.Rules.PhiPaper (rule1, rule6) import Test.EO.Phi import Test.Hspec -applyRule :: (Object -> Maybe Object) -> Program -> Maybe Program +applyRule :: (Object -> [Object]) -> Program -> [Program] applyRule rule = \case Program [AlphaBinding name obj] -> do r <- rule obj pure $ Program [AlphaBinding name r] - _ -> Nothing + _ -> [] spec :: Spec spec = do - describe "Rules unit tests" $ + describe "Pre-defined rules unit tests" $ forM_ ([(1, rule1), (6, rule6)] :: [(Int, Rule)]) $ \(idx, rule) -> do - PhiTestGroup{..} <- runIO (filePhiTests [i|test/eo/phi/rule-#{idx}.yaml|]) + PhiTestGroup{..} <- runIO (fileTests [i|test/eo/phi/rule-#{idx}.yaml|]) describe title $ forM_ tests $ \PhiTest{..} -> - it name do - applyRule (rule (Context [])) input `shouldBe` Just normalized + it name $ + applyRule (rule (Context [])) input `shouldBe` [normalized] diff --git a/eo-phi-normalizer/test/Language/EO/YamlSpec.hs b/eo-phi-normalizer/test/Language/EO/YamlSpec.hs new file mode 100644 index 000000000..6481c8f3a --- /dev/null +++ b/eo-phi-normalizer/test/Language/EO/YamlSpec.hs @@ -0,0 +1,20 @@ +{-# LANGUAGE BlockArguments #-} +{-# LANGUAGE OverloadedRecordDot #-} + +module Language.EO.YamlSpec where + +import Control.Monad (forM_) +import Language.EO.Phi.Rules.Common (Context (..)) +import Language.EO.Phi.Rules.Yaml (Rule (..), RuleSet (..), RuleTest (..), convertRule) +import Test.EO.Yaml +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 $ + convertRule rule (Context []) ruleTest.input `shouldBe` [ruleTest.output | ruleTest.matches] diff --git a/eo-phi-normalizer/test/Test/EO/Phi.hs b/eo-phi-normalizer/test/Test/EO/Phi.hs index b03ecf91c..8bbd120d8 100644 --- a/eo-phi-normalizer/test/Test/EO/Phi.hs +++ b/eo-phi-normalizer/test/Test/EO/Phi.hs @@ -7,14 +7,14 @@ module Test.EO.Phi where import Control.Monad (forM) import Data.Aeson (FromJSON (..)) -import qualified Data.Yaml as Yaml +import Data.Yaml qualified as Yaml import GHC.Generics (Generic) import System.Directory (listDirectory) import System.FilePath (()) import Data.List (sort) import Language.EO.Phi (unsafeParseProgram) -import qualified Language.EO.Phi as Phi +import Language.EO.Phi qualified as Phi data PhiTestGroup = PhiTestGroup { title :: String @@ -30,14 +30,14 @@ data PhiTest = PhiTest } deriving (Generic, FromJSON) -filePhiTests :: FilePath -> IO PhiTestGroup -filePhiTests = Yaml.decodeFileThrow +fileTests :: FilePath -> IO PhiTestGroup +fileTests = Yaml.decodeFileThrow allPhiTests :: FilePath -> IO [PhiTestGroup] allPhiTests dir = do paths <- listDirectory dir forM (sort paths) $ \path -> - filePhiTests (dir path) + fileTests (dir path) -- * Orphan instances diff --git a/eo-phi-normalizer/test/Test/EO/Yaml.hs b/eo-phi-normalizer/test/Test/EO/Yaml.hs new file mode 100644 index 000000000..8ae9b2fb5 --- /dev/null +++ b/eo-phi-normalizer/test/Test/EO/Yaml.hs @@ -0,0 +1,20 @@ +{-# LANGUAGE DuplicateRecordFields #-} +{-# LANGUAGE FlexibleInstances #-} +{-# OPTIONS_GHC -Wno-orphans #-} + +module Test.EO.Yaml where + +import Control.Monad (forM) +import Data.List (sort) +import Language.EO.Phi.Rules.Yaml (RuleSet, parseRuleSetFromFile) +import System.Directory (listDirectory) +import System.FilePath (()) + +fileTests :: FilePath -> IO RuleSet +fileTests = parseRuleSetFromFile + +directoryTests :: FilePath -> IO [RuleSet] +directoryTests dir = do + paths <- listDirectory dir + forM (sort paths) $ \path -> + fileTests (dir path) diff --git a/eo-phi-normalizer/test/eo/phi/rule-6.yaml b/eo-phi-normalizer/test/eo/phi/rule-6.yaml index 551f94dea..d48273e10 100644 --- a/eo-phi-normalizer/test/eo/phi/rule-6.yaml +++ b/eo-phi-normalizer/test/eo/phi/rule-6.yaml @@ -1,9 +1,36 @@ title: Tests for Rule 6 tests: - - name: 'Case (1)' + - name: "Case (1)" input: | { a ↦ ⟦ b ↦ ⟦ Δ ⤍ 00- ⟧, c ↦ ⟦ Δ ⤍ 03- ⟧ ⟧.b } normalized: | { a ↦ ⟦ Δ ⤍ 00- ⟧(ρ ↦ ⟦ c ↦ ⟦ Δ ⤍ 03- ⟧ ⟧) } prettified: | - { a ↦ ⟦ b ↦ ⟦ Δ ⤍ 00- ⟧, c ↦ ⟦ Δ ⤍ 03- ⟧ ⟧.b } \ No newline at end of file + { a ↦ ⟦ b ↦ ⟦ Δ ⤍ 00- ⟧, c ↦ ⟦ Δ ⤍ 03- ⟧ ⟧.b } + - name: "Case (2)" + input: | + { + a ↦ + ⟦ + b ↦ + ⟦ + c ↦ ∅, + d ↦ ⟦ φ ↦ ξ.ρ.c ⟧ + ⟧, + e ↦ ξ.b(c ↦ ⟦⟧).d + ⟧.e + } + normalized: | + { a ↦ ξ.b (c ↦ ⟦ ⟧).d (ρ ↦ ⟦ b ↦ ⟦ c ↦ ∅, d ↦ ⟦ φ ↦ ξ.ρ.c ⟧ ⟧ ⟧) } + prettified: | + { + a ↦ + ⟦ + b ↦ + ⟦ + c ↦ ∅, + d ↦ ⟦ φ ↦ ξ.ρ.c ⟧ + ⟧, + e ↦ ξ.b(c ↦ ⟦⟧).d + ⟧.e + } diff --git a/eo-phi-normalizer/test/eo/phi/rules/yegor.yaml b/eo-phi-normalizer/test/eo/phi/rules/yegor.yaml new file mode 100644 index 000000000..db1a7b72e --- /dev/null +++ b/eo-phi-normalizer/test/eo/phi/rules/yegor.yaml @@ -0,0 +1,48 @@ +title: "Rule set based on Yegor's draft" +rules: + - name: Rule 5 + description: "ξ-dispatch" + pattern: | + ⟦ !a ↦ ξ.!b, !B ⟧ + result: | + ⟦ !a ↦ ⟦ !B ⟧.!b, !B ⟧ + when: [] + tests: [] + + - name: Rule 6 + description: "Accessing an α-binding" + pattern: | + ⟦ !a ↦ !n, !B ⟧.!a + result: | + !n(ρ ↦ ⟦ !B ⟧) + when: + - nf: ["!n"] + tests: + - name: Should match + input: ⟦ hello ↦ ⟦⟧ ⟧.hello + output: ⟦⟧(ρ ↦ ⟦⟧) + matches: true + - name: Shouldn't match + input: ⟦ ⟧.hello + output: "" + matches: false + + - name: Rule 7 + description: "Application" + pattern: | + ⟦ !a ↦ ∅, !B ⟧(!a ↦ !n) + result: | + ⟦ !a ↦ !n, !B ⟧ + when: + - nf: ["!n"] + tests: [] + + # - name: Rule 8 + + - name: Rule 9 + description: "Parent application" + pattern: ⟦ ρ ↦ !t, !B ⟧(ρ ↦ !n) + result: ⟦ ρ ↦ !n, !B ⟧ + when: + - nf: ["!n"] + tests: []