diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -6,6 +6,21 @@ ## [Unreleased] +## [5.0.0.0] - 2026-09-30 + +### Added + +- `RULES` pragmas are parsed. A `{-# RULES ... #-}` pragma at the top level + is a `DeclRules` declaration that holds one `RuleDecl` per rule: the name, + the phase control (`[n]`, `[~n]` or `[~]`), the type variables of a leading + `forall` that a second `forall` follows, the pattern variables with their + optional types, and the two sides as expressions. The lexer opens the + pragma with a `TkPragmaOpen "RULES"` token and closes it with + `TkPragmaClose`, and lexes the rules between them as ordinary tokens, so + the rules take part in layout the way GHC reads them: a rule that starts + in the column of the enclosing declarations begins a new rule. Before, a + `RULES` pragma was a `DeclPragma` with a `PragmaUnknown` body. + ## [4.0.0.0] - 2026-09-17 ### Fixed diff --git a/aihc-parser.cabal b/aihc-parser.cabal --- a/aihc-parser.cabal +++ b/aihc-parser.cabal @@ -1,6 +1,6 @@ cabal-version: 3.8 name: aihc-parser -version: 4.0.0.0 +version: 5.0.0.0 build-type: Simple license: Unlicense license-file: LICENSE diff --git a/docs/aihc-parser-supported-extensions.md b/docs/aihc-parser-supported-extensions.md --- a/docs/aihc-parser-supported-extensions.md +++ b/docs/aihc-parser-supported-extensions.md @@ -68,7 +68,7 @@ | PatternSynonyms | 🟢 | 34/34 | | PolyKinds | 🟢 | 14/14 | | QualifiedDo | 🟢 | 4/4 | -| QuantifiedConstraints | 🟢 | 2/2 | +| QuantifiedConstraints | 🟢 | 6/6 | | QuasiQuotes | 🟢 | 11/11 | | RankNTypes | 🟢 | 5/5 | | RecordWildCards | 🟢 | 10/10 | @@ -76,7 +76,7 @@ | RequiredTypeArguments | 🟢 | 4/4 | | RoleAnnotations | 🟢 | 7/7 | | Safe | 🟢 | 2/2 | -| ScopedTypeVariables | 🟢 | 18/18 | +| ScopedTypeVariables | 🟢 | 19/19 | | StandaloneDeriving | 🟢 | 18/18 | | StandaloneKindSignatures | 🟢 | 12/12 | | StarIsType | 🟢 | 4/4 | @@ -85,7 +85,7 @@ | TransformListComp | 🟢 | 18/18 | | TupleSections | 🟢 | 4/4 | | TypeAbstractions | 🟢 | 5/5 | -| TypeApplications | 🟢 | 14/14 | +| TypeApplications | 🟢 | 15/15 | | TypeData | 🟢 | 1/1 | | TypeFamilies | 🟢 | 61/61 | | TypeFamilyDependencies | 🟢 | 4/4 | diff --git a/src/Aihc/Parser/Internal/Decl.hs b/src/Aihc/Parser/Internal/Decl.hs --- a/src/Aihc/Parser/Internal/Decl.hs +++ b/src/Aihc/Parser/Internal/Decl.hs @@ -97,6 +97,7 @@ TkKeywordInstance -> typeFamilyInstParser _ -> typeDeclarationParser TkKeywordPattern -> patternSynonymParser + TkPragmaOpen "RULES" -> rulesDeclParser TkVarId {} -> case nextTokKind of TkReservedDoubleColon -> sigOrValueDecl @@ -144,6 +145,118 @@ -- | Parse a pragma declaration (e.g. {-# INLINE f #-}, {-# SPECIALIZE ... #-}) pragmaDeclParser :: TokParser Decl pragmaDeclParser = withSpanAnn (DeclAnn . mkAnnotation) $ DeclPragma <$> anyPragmaParser "pragma declaration" + +-- | Parse a @RULES@ pragma: +-- +-- > {-# RULES "map/map" [2] forall f g xs. map f (map g xs) = map (f . g) xs #-} +-- +-- The lexer opens the pragma with 'TkPragmaOpen' and closes it with +-- 'TkPragmaClose', and lexes the rules between them as ordinary tokens. The +-- rules are separated by semicolons, which the layout rule supplies for a +-- rule that starts in the column of the enclosing declarations. +rulesDeclParser :: TokParser Decl +rulesDeclParser = withSpanAnn (DeclAnn . mkAnnotation) $ do + expectedTok (TkPragmaOpen "RULES") + rules <- region "while parsing RULES pragma" (plainSemiSep ruleDeclParser) + expectedTok TkPragmaClose + pure (DeclRules rules) + +-- | One rule: +-- +-- > "name" [2] forall a. forall (x :: a) y. lhs = rhs +-- +-- With one @forall@, every binder is a pattern variable. With two, the +-- first binds type variables and the second the pattern variables. +ruleDeclParser :: TokParser RuleDecl +ruleDeclParser = withSpan $ do + name <- stringTextParser + activation <- MP.optional ruleActivationParser + binders <- MP.option [] ruleForallParser + (typeBinders, termBinders) <- + MP.option ([], binders) $ do + termBinders <- ruleForallParser + pure (map ruleBinderToTyVarBinder binders, termBinders) + lhs <- region "while parsing rule left-hand side" exprParser + expectedTok TkReservedEquals + rhs <- region "while parsing rule right-hand side" exprParser + pure $ \span' -> + RuleDecl + { ruleAnns = [mkAnnotation span'], + ruleName = name, + ruleActivation = activation, + ruleTypeBinders = typeBinders, + ruleBinders = termBinders, + ruleLhs = lhs, + ruleRhs = rhs + } + +-- | The phase control of a rule: @[n]@, @[~n]@ or @[~]@. +ruleActivationParser :: TokParser RuleActivation +ruleActivationParser = do + expectedTok TkSpecialLBracket + activation <- + (ruleTildeParser *> (RuleActiveBefore <$> rulePhaseParser <|> pure RuleNeverActive)) + <|> (RuleActiveAfter <$> rulePhaseParser) + expectedTok TkSpecialRBracket + pure activation + +ruleTildeParser :: TokParser () +ruleTildeParser = + tokenSatisfy "~" $ \tok -> + case lexTokenKind tok of + TkPrefixTilde -> Just () + TkVarSym "~" -> Just () + _ -> Nothing + +rulePhaseParser :: TokParser Int +rulePhaseParser = + tokenSatisfy "phase number" $ \tok -> + case lexTokenKind tok of + TkInteger n _ | n >= 0 && n <= fromIntegral (maxBound :: Int) -> Just (fromInteger n) + _ -> Nothing + +-- | @forall x (y :: t).@ +ruleForallParser :: TokParser [RuleBinder] +ruleForallParser = do + expectedTok TkKeywordForall + binders <- MP.many ruleBinderParser + expectedTok (TkVarSym ".") + pure binders + +-- | @x@ or @(x :: t)@. +ruleBinderParser :: TokParser RuleBinder +ruleBinderParser = + withSpan $ + ( do + name <- ruleBinderNameParser + pure (\span' -> RuleBinder [mkAnnotation span'] name Nothing) + ) + <|> ( do + expectedTok TkSpecialLParen + name <- ruleBinderNameParser + expectedTok TkReservedDoubleColon + ty <- typeParser + expectedTok TkSpecialRParen + pure (\span' -> RuleBinder [mkAnnotation span'] name (Just ty)) + ) + +ruleBinderNameParser :: TokParser UnqualifiedName +ruleBinderNameParser = + tokenSatisfy "rule variable" $ \tok -> + case lexTokenKind tok of + TkVarId ident -> Just (mkUnqualifiedNameAt tok NameVarId ident) + _ -> Nothing + +-- | A binder of the first of two @forall@s binds a type variable. +ruleBinderToTyVarBinder :: RuleBinder -> TyVarBinder +ruleBinderToTyVarBinder binder = + TyVarBinder + { tyVarBinderAnns = ruleBinderAnns binder, + tyVarBinderName = unqualifiedNameText (ruleBinderName binder), + tyVarBinderKind = ruleBinderType binder, + tyVarBinderSpecificity = TyVarBSpecified, + tyVarBinderVisibility = TyVarBVisible + } -- | Check whether the expression-as-declaration fallback is enabled. -- GHC allows top-level expressions under TemplateHaskell (bare splices), diff --git a/src/Aihc/Parser/Lex.hs b/src/Aihc/Parser/Lex.hs --- a/src/Aihc/Parser/Lex.hs +++ b/src/Aihc/Parser/Lex.hs @@ -52,7 +52,7 @@ lexIntBase, withOptionalMagicHashSuffix, ) -import Aihc.Parser.Lex.Pragmas (tryParsePragma) +import Aihc.Parser.Lex.Pragmas (tryParsePragma, tryParsePragmaClose) import Aihc.Parser.Lex.Quoted ( decodeStringBody, processMultilineString, @@ -231,6 +231,7 @@ -- (<|>) for Maybe short-circuits on the first Just without allocating. fromMaybe (lexErrorToken st "unexpected character") $ lexPragma st + <|> tryParsePragmaClose st <|> lexTHQuoteBracket env st <|> lexQuasiQuote st <|> lexHexFloat env st @@ -519,6 +520,8 @@ TkReservedBackslash -> True TkTypeApp -> True TkPragma _ -> True + TkPragmaOpen _ -> True + TkPragmaClose -> True _ -> False -- | Returns True for tokens after which a '.' can begin a record field access diff --git a/src/Aihc/Parser/Lex/Pragmas.hs b/src/Aihc/Parser/Lex/Pragmas.hs --- a/src/Aihc/Parser/Lex/Pragmas.hs +++ b/src/Aihc/Parser/Lex/Pragmas.hs @@ -3,6 +3,7 @@ module Aihc.Parser.Lex.Pragmas ( tryParsePragma, + tryParsePragmaClose, parsePragmaType, parseControlPragma, ) @@ -25,13 +26,48 @@ -- | Single entry point for pragma parsing. -- Scans "{-# ... #-}" once, then parses the body to determine which Pragma it is. +-- +-- A pragma whose body is Haskell syntax, such as @RULES@, does not become one +-- token. The lexer emits a 'TkPragmaOpen' token for its opening and keyword, +-- lexes the body as ordinary tokens, and emits 'TkPragmaClose' at its @#-}@ +-- (see 'tryParsePragmaClose'). The body then takes part in layout like the +-- code around it, which is how GHC reads it. tryParsePragma :: LexerState -> Maybe (LexToken, LexerState) tryParsePragma st = do (rawBody, consumedLen) <- extractPragmaBody (lexerInput st) - let fullText = "{-#" <> rawBody <> "#-}" - pragma = Pragma {pragmaType = parsePragmaType rawBody, pragmaRawText = fullText} - st' = advanceN consumedLen st - Just (mkToken st st' fullText (TkPragma pragma), st') + case openPragmaKeyword rawBody of + Just (keyword, openLen) -> + let st' = (advanceN openLen st) {lexerInPragma = True} + in Just (mkToken st st' (T.take openLen (lexerInput st)) (TkPragmaOpen keyword), st') + Nothing -> + let fullText = "{-#" <> rawBody <> "#-}" + pragma = Pragma {pragmaType = parsePragmaType rawBody, pragmaRawText = fullText} + st' = advanceN consumedLen st + in Just (mkToken st st' fullText (TkPragma pragma), st') + +-- | The keyword of a pragma whose body is lexed as ordinary tokens, and the +-- length of the opening up to and including the keyword. +openPragmaKeyword :: Text -> Maybe (Text, Int) +openPragmaKeyword rawBody = + let leading = T.takeWhile isSpace rawBody + keyword = T.takeWhile (not . isSpace) (T.drop (T.length leading) rawBody) + upper = T.toUpper keyword + in if upper `elem` openPragmaKeywords + then Just (upper, 3 + T.length leading + T.length keyword) + else Nothing + +-- | The pragmas that 'tryParsePragma' opens rather than lexes as one token. +openPragmaKeywords :: [Text] +openPragmaKeywords = ["RULES"] + +-- | The @#-}@ that closes a pragma opened by 'tryParsePragma'. +tryParsePragmaClose :: LexerState -> Maybe (LexToken, LexerState) +tryParsePragmaClose st + | lexerInPragma st, + "#-}" `T.isPrefixOf` lexerInput st = + let st' = (advanceN 3 st) {lexerInPragma = False} + in Just (mkToken st st' "#-}" TkPragmaClose, st') + | otherwise = Nothing -- | Extract the raw body text between "{-#" and "#-}". -- Returns (body_text, total_consumed_length) where total includes "{-#" and "#-}". diff --git a/src/Aihc/Parser/Lex/Types.hs b/src/Aihc/Parser/Lex/Types.hs --- a/src/Aihc/Parser/Lex/Types.hs +++ b/src/Aihc/Parser/Lex/Types.hs @@ -162,6 +162,11 @@ TkTypeApp | -- Pragmas TkPragma Pragma + | -- | The opening of a pragma whose body is lexed as ordinary tokens, + -- such as @{-# RULES@. The text is the pragma keyword in upper case. + TkPragmaOpen Text + | -- | The @#-}@ that closes a pragma opened by 'TkPragmaOpen'. + TkPragmaClose | -- TemplateHaskellQuotes bracket tokens TkTHExpQuoteOpen | TkTHExpQuoteClose @@ -232,7 +237,10 @@ lexerByteOffset :: !Int, lexerAtLineStart :: !Bool, lexerPrevTokenKind :: !(Maybe LexTokenKind), - lexerHadTrivia :: !Bool + lexerHadTrivia :: !Bool, + -- | Whether the lexer is inside a pragma opened by 'TkPragmaOpen', so + -- that the next @#-}@ closes it. + lexerInPragma :: !Bool } deriving (Eq, Show) @@ -331,7 +339,8 @@ lexerByteOffset = 0, lexerAtLineStart = True, lexerPrevTokenKind = Nothing, - lexerHadTrivia = True + lexerHadTrivia = True, + lexerInPragma = False } ) diff --git a/src/Aihc/Parser/Parens.hs b/src/Aihc/Parser/Parens.hs --- a/src/Aihc/Parser/Parens.hs +++ b/src/Aihc/Parser/Parens.hs @@ -630,6 +630,23 @@ DeclTypeFamilyInst tfi -> DeclTypeFamilyInst (addTypeFamilyInstParens tfi) DeclDataFamilyInst dfi -> DeclDataFamilyInst (addDataFamilyInstParens dfi) DeclPragma {} -> decl + DeclRules rules -> DeclRules (map addRuleDeclParens rules) + +-- | Parenthesize the sides and binder types of a rewrite rule. The +-- left-hand side is followed by @=@ on the same line, so a side whose +-- rightmost part would take the @=@ into itself is wrapped. +addRuleDeclParens :: RuleDecl -> RuleDecl +addRuleDeclParens rule = + rule + { ruleTypeBinders = map addTyVarBinderParens (ruleTypeBinders rule), + ruleBinders = map addRuleBinderParens (ruleBinders rule), + ruleLhs = wrapExpr (lhsNeedsParens (ruleLhs rule)) (addExprParens (ruleLhs rule)), + ruleRhs = addExprParens (ruleRhs rule) + } + where + lhsNeedsParens expr = isGreedyExpr expr || isOpenEnded expr || endsWithTypeSig expr + addRuleBinderParens binder = + binder {ruleBinderType = fmap addSignatureTypeParens (ruleBinderType binder)} addDeclSpliceParens :: Expr -> Expr addDeclSpliceParens = addExprParens diff --git a/src/Aihc/Parser/Pretty.hs b/src/Aihc/Parser/Pretty.hs --- a/src/Aihc/Parser/Pretty.hs +++ b/src/Aihc/Parser/Pretty.hs @@ -278,6 +278,51 @@ DeclTypeFamilyInst tfi -> [prettyTopTypeFamilyInst tfi] DeclDataFamilyInst dfi -> [prettyTopDataFamilyInst dfi] DeclPragma pragma -> [prettyPragma pragma] + DeclRules rules -> prettyRulesLines rules + +-- | A @RULES@ pragma, one rule per line. Every rule after the first starts +-- with an explicit semicolon in the first column, so the rules are separated +-- whether or not an enclosing layout context supplies semicolons, and the +-- closing @#-}@ stands in the first column so that it ends any layout +-- context a rule opened. +prettyRulesLines :: [RuleDecl] -> [Doc ann] +prettyRulesLines rules = + ["{-# RULES"] + <> zipWith prettyRuleLine [0 :: Int ..] rules + <> ["#-}"] + where + prettyRuleLine index rule + | index == 0 = nest 2 (prettyRuleDecl rule) + | otherwise = nest 2 (";" <+> prettyRuleDecl rule) + +prettyRuleDecl :: RuleDecl -> Doc ann +prettyRuleDecl rule = + hsep + ( [pretty (show (ruleName rule))] + <> maybe [] (pure . prettyRuleActivation) (ruleActivation rule) + <> foralls + <> [prettyExpr (ruleLhs rule), "=", prettyExpr (ruleRhs rule)] + ) + where + foralls = + case (ruleTypeBinders rule, ruleBinders rule) of + ([], []) -> [] + ([], binders) -> [ruleForall (map prettyRuleBinder binders)] + (typeBinders, binders) -> [ruleForall (map prettyTyVarBinder typeBinders), ruleForall (map prettyRuleBinder binders)] + ruleForall binders = hsep ("forall" : binders) <> "." + +prettyRuleActivation :: RuleActivation -> Doc ann +prettyRuleActivation activation = + case activation of + RuleActiveAfter phase -> brackets (pretty phase) + RuleActiveBefore phase -> brackets ("~" <> pretty phase) + RuleNeverActive -> brackets "~" + +prettyRuleBinder :: RuleBinder -> Doc ann +prettyRuleBinder binder = + case ruleBinderType binder of + Nothing -> prettyBinderName (ruleBinderName binder) + Just ty -> parens (prettyBinderName (ruleBinderName binder) <+> "::" <+> prettyType ty) prettyRoleAnnotation :: RoleAnnotation -> Doc ann prettyRoleAnnotation ann = diff --git a/src/Aihc/Parser/Shorthand.hs b/src/Aihc/Parser/Shorthand.hs --- a/src/Aihc/Parser/Shorthand.hs +++ b/src/Aihc/Parser/Shorthand.hs @@ -236,7 +236,39 @@ DeclTypeFamilyInst tfi -> "DeclTypeFamilyInst" <+> parens (docTypeFamilyInst tfi) DeclDataFamilyInst dfi -> "DeclDataFamilyInst" <+> parens (docDataFamilyInst dfi) DeclPragma pragma -> "DeclPragma" <+> docPragma pragma + DeclRules rules -> "DeclRules" <+> brackets (hsep (punctuate comma (map docRuleDecl rules))) +docRuleDecl :: RuleDecl -> Doc ann +docRuleDecl rule = + "RuleDecl" <+> braces (hsep (punctuate comma fields)) + where + fields = + [docText (ruleName rule)] + <> optionalField docRuleActivation (ruleActivation rule) + <> listField docTyVarBinder (ruleTypeBinders rule) + <> listField docRuleBinder (ruleBinders rule) + <> [docExpr (ruleLhs rule), docExpr (ruleRhs rule)] + +docRuleActivation :: RuleActivation -> Doc ann +docRuleActivation activation = + case activation of + RuleActiveAfter phase -> "RuleActiveAfter" <+> pretty phase + RuleActiveBefore phase -> "RuleActiveBefore" <+> pretty phase + RuleNeverActive -> "RuleNeverActive" + +docRuleBinder :: RuleBinder -> Doc ann +docRuleBinder binder = + "RuleBinder" + <+> braces + ( hsep + ( punctuate + comma + ( [docUnqualifiedNameText (ruleBinderName binder)] + <> optionalField (\ty -> "Just" <+> parens (docType ty)) (ruleBinderType binder) + ) + ) + ) + docValueDecl :: ValueDecl -> Doc ann docValueDecl vdecl = case vdecl of @@ -1112,6 +1144,8 @@ TkPrefixTilde -> "TkPrefixTilde" TkRecordDot -> "TkRecordDot" TkPragma pragma' -> "TkPragma" <+> docPragmaType (pragmaType pragma') + TkPragmaOpen keyword -> "TkPragmaOpen" <+> docText keyword + TkPragmaClose -> "TkPragmaClose" TkQuasiQuote quoter body -> "TkQuasiQuote" <+> docText quoter <+> docText body TkLineComment -> "TkLineComment" TkBlockComment -> "TkBlockComment" diff --git a/src/Aihc/Parser/Syntax.hs b/src/Aihc/Parser/Syntax.hs --- a/src/Aihc/Parser/Syntax.hs +++ b/src/Aihc/Parser/Syntax.hs @@ -87,6 +87,9 @@ Role (..), RoleAnnotation (..), Rhs (..), + RuleActivation (..), + RuleBinder (..), + RuleDecl (..), SourceSpan, pattern SourceSpan, sourceSpanSourceName, @@ -1203,6 +1206,48 @@ DeclDataFamilyInst DataFamilyInst | -- | A standalone pragma declaration such as @{-# INLINE f #-}@. DeclPragma Pragma + | -- | @{-# RULES "map/map" forall f g xs. map f (map g xs) = map (f . g) xs #-}@ + DeclRules [RuleDecl] + deriving (Data, Eq, Show, Generic, NFData) + +-- | One rewrite rule of a @RULES@ pragma. +-- Example: @"map/map" [2] forall f g xs. map f (map g xs) = map (f . g) xs@. +data RuleDecl = RuleDecl + { ruleAnns :: [Annotation], + -- | The name in double quotes. It only identifies the rule in reports. + ruleName :: Text, + -- | The phase control after the name, such as @[2]@ or @[~2]@. + ruleActivation :: Maybe RuleActivation, + -- | The type variables of a leading @forall a b.@ that a second + -- @forall@ follows. A rule with one @forall@ binds only term variables. + ruleTypeBinders :: [TyVarBinder], + -- | The pattern variables bound by @forall@. + ruleBinders :: [RuleBinder], + -- | The left-hand side, matched against the program. + ruleLhs :: Expr, + -- | The right-hand side, put in place of a match. + ruleRhs :: Expr + } + deriving (Data, Eq, Show, Generic, NFData) + +-- | The phases in which a rule is active. +-- Examples: @[2]@, @[~2]@, and @[~]@. +data RuleActivation + = -- | @[n]@: active in phase @n@ and later phases. + RuleActiveAfter Int + | -- | @[~n]@: active before phase @n@. + RuleActiveBefore Int + | -- | @[~]@: never active. + RuleNeverActive + deriving (Data, Eq, Show, Generic, NFData) + +-- | One pattern variable of a rule, bound by @forall@. +-- Examples: @xs@ and @(g :: forall b. (a -> b -> b) -> b -> b)@. +data RuleBinder = RuleBinder + { ruleBinderAnns :: [Annotation], + ruleBinderName :: UnqualifiedName, + ruleBinderType :: Maybe Type + } deriving (Data, Eq, Show, Generic, NFData) -- | Peel nested 'DeclAnn' wrappers. diff --git a/test/Spec.hs b/test/Spec.hs --- a/test/Spec.hs +++ b/test/Spec.hs @@ -648,6 +648,7 @@ "type instance F Int = Bool", "data instance DF Int = DFInt", "{-# INLINE f #-}", + "{-# RULES \"f/g\" forall x. f (g x) = x #-}", "pattern Q :: Int -> T Int", "pattern Q x = MkT x", "$(pure [])" diff --git a/test/Test/Fixtures/golden/pragma/rules-layout.yaml b/test/Test/Fixtures/golden/pragma/rules-layout.yaml new file mode 100644 --- /dev/null +++ b/test/Test/Fixtures/golden/pragma/rules-layout.yaml @@ -0,0 +1,12 @@ +extensions: [] +input: | + module Demo where + {-# RULES + "map/map" [2] forall f g xs. map f (map g xs) = map (f . g) xs + "map/id" [~1] forall xs. map id xs = xs + "fold/build" forall k z (g :: forall b. (a -> b -> b) -> b -> b) . foldr k z (build g) = g k z + #-} + x = 1 +ast: |- + Module {ModuleHead {"Demo"}, [DeclRules [RuleDecl {"map/map", RuleActiveAfter 2, [RuleBinder {"f"}, RuleBinder {"g"}, RuleBinder {"xs"}], EApp (EApp (EVar "map") (EVar "f")) (EParen (EApp (EApp (EVar "map") (EVar "g")) (EVar "xs"))), EApp (EApp (EVar "map") (EParen (EInfix (EVar "f") "." (EVar "g")))) (EVar "xs")}, RuleDecl {"map/id", RuleActiveBefore 1, [RuleBinder {"xs"}], EApp (EApp (EVar "map") (EVar "id")) (EVar "xs"), EVar "xs"}, RuleDecl {"fold/build", [RuleBinder {"k"}, RuleBinder {"z"}, RuleBinder {"g", Just (TForall [TyVarBinder {"b"}] (TFun (TParen (TFun (TVar "a") (TFun (TVar "b") (TVar "b")))) (TFun (TVar "b") (TVar "b"))))}], EApp (EApp (EApp (EVar "foldr") (EVar "k")) (EVar "z")) (EParen (EApp (EVar "build") (EVar "g"))), EApp (EApp (EVar "g") (EVar "k")) (EVar "z")}], DeclValue (PatternBind (PVar "x") (EInt 1 TInteger))]} +status: pass diff --git a/test/Test/Fixtures/golden/pragma/rules-type-binders.yaml b/test/Test/Fixtures/golden/pragma/rules-type-binders.yaml new file mode 100644 --- /dev/null +++ b/test/Test/Fixtures/golden/pragma/rules-type-binders.yaml @@ -0,0 +1,7 @@ +extensions: [TypeApplications] +input: | + {-# RULES "id" forall a. forall (x :: a). id @a x = x; "never" [~] forall. f = g #-} + {-# RULES #-} +ast: |- + Module {[DeclRules [RuleDecl {"id", [TyVarBinder {"a"}], [RuleBinder {"x", Just (TVar "a")}], EApp (ETypeApp (EVar "id") (TVar "a")) (EVar "x"), EVar "x"}, RuleDecl {"never", RuleNeverActive, EVar "f", EVar "g"}], DeclRules []]} +status: pass diff --git a/test/Test/Fixtures/oracle/pragma/RulesPragmaForms.hs b/test/Test/Fixtures/oracle/pragma/RulesPragmaForms.hs new file mode 100644 --- /dev/null +++ b/test/Test/Fixtures/oracle/pragma/RulesPragmaForms.hs @@ -0,0 +1,20 @@ +{- ORACLE_TEST pass -} +{-# LANGUAGE ScopedTypeVariables, TypeApplications #-} +module RulesPragmaForms where + +{-# RULES +"map/map" [2] forall f g xs. map f (map g xs) = map (f . g) xs +"map/id" [~1] forall xs. map id xs = xs +"fold/build" forall k z (g :: forall b. (a -> b -> b) -> b -> b) . foldr k z (build g) = g k z +"id/type" forall a. forall (x :: a). id @a x = x +"never" [~] forall (x :: Int). negate (negate x) = x + #-} + +{-# RULES "one" forall x. one x = x ; "two" forall y. two y = y #-} + +build :: (forall b. (a -> b -> b) -> b -> b) -> [a] +build g = g (:) [] + +one, two :: Int -> Int +one = id +two = id diff --git a/test/Test/Properties/Arb/Decl.hs b/test/Test/Properties/Arb/Decl.hs --- a/test/Test/Properties/Arb/Decl.hs +++ b/test/Test/Properties/Arb/Decl.hs @@ -24,6 +24,7 @@ genConName, genConSym, genConUnqualifiedName, + genStringValue, genVarId, genVarIdNoHash, genVarName, @@ -69,6 +70,7 @@ genDeclTypeFamilyInst, genDeclDataFamilyInst, genDeclPragma, + genDeclRules, genDeclPatSyn, genDeclPatSynSig, genDeclStandaloneKindSig @@ -1109,6 +1111,59 @@ mkPragma :: PragmaType -> Pragma mkPragma pt = Pragma {pragmaType = pt, pragmaRawText = ""} +genDeclRules :: Gen Decl +genDeclRules = DeclRules <$> smallList0 genRuleDecl + +genRuleDecl :: Gen RuleDecl +genRuleDecl = do + name <- genStringValue + activation <- optional genRuleActivation + typeBinders <- smallList0 genSimpleTyVarBinder + binders <- smallList0 genRuleBinder + lhs <- genRuleLhs + rhs <- genExpr + pure + RuleDecl + { ruleAnns = [], + ruleName = name, + ruleActivation = activation, + ruleTypeBinders = typeBinders, + ruleBinders = binders, + ruleLhs = lhs, + ruleRhs = rhs + } + +genRuleActivation :: Gen RuleActivation +genRuleActivation = + oneof + [ RuleActiveAfter <$> chooseInt (0, 3), + RuleActiveBefore <$> chooseInt (0, 3), + pure RuleNeverActive + ] + +genRuleBinder :: Gen RuleBinder +genRuleBinder = RuleBinder [] . mkUnqualifiedName NameVarId <$> genVarId <*> optional genType + +-- | A left-hand side is a variable applied to arguments, as GHC requires. +genRuleLhs :: Gen Expr +genRuleLhs = do + headName <- genVarName + args <- smallList0 genExpr + pure (foldl EApp (EVar headName) args) + +shrinkRuleDecl :: RuleDecl -> [RuleDecl] +shrinkRuleDecl rule = + [rule {ruleActivation = Nothing} | isJust (ruleActivation rule)] + <> [rule {ruleTypeBinders = binders'} | binders' <- shrinkTyVarBinders (ruleTypeBinders rule)] + <> [rule {ruleBinders = binders'} | binders' <- shrinkList shrinkRuleBinder (ruleBinders rule)] + <> [rule {ruleLhs = lhs'} | lhs' <- shrinkExpr (ruleLhs rule)] + <> [rule {ruleRhs = rhs'} | rhs' <- shrinkExpr (ruleRhs rule)] + +shrinkRuleBinder :: RuleBinder -> [RuleBinder] +shrinkRuleBinder binder = + [binder {ruleBinderType = Nothing} | isJust (ruleBinderType binder)] + <> [binder {ruleBinderType = Just ty'} | Just ty <- [ruleBinderType binder], ty' <- shrinkType ty] + genDeclPatSyn :: Gen Decl genDeclPatSyn = do synName <- genConUnqualifiedName @@ -1235,6 +1290,8 @@ DeclDataFamilyInst dfi -> [DeclDataFamilyInst dfi' | dfi' <- shrinkDataFamilyInst dfi] DeclPragma _ -> [] + DeclRules rules -> + [DeclRules rules' | rules' <- shrinkList shrinkRuleDecl rules] -- --------------------------------------------------------------------------- -- Value declarations (function binds and pattern binds) diff --git a/test/Test/Properties/NoExceptions.hs b/test/Test/Properties/NoExceptions.hs --- a/test/Test/Properties/NoExceptions.hs +++ b/test/Test/Properties/NoExceptions.hs @@ -194,6 +194,8 @@ TkPragma . (\pt -> Syntax.Pragma {Syntax.pragmaType = pt, Syntax.pragmaRawText = ""}) <$> (Syntax.PragmaSource <$> genTokenText <*> genTokenText), TkPragma . (\pt -> Syntax.Pragma {Syntax.pragmaType = pt, Syntax.pragmaRawText = ""}) . Syntax.PragmaSCC <$> genTokenText, TkPragma . (\pt -> Syntax.Pragma {Syntax.pragmaType = pt, Syntax.pragmaRawText = ""}) . Syntax.PragmaUnknown <$> genTokenText, + TkPragmaOpen <$> genTokenText, + pure TkPragmaClose, TkVarId <$> genIdentifierText, TkConId <$> genConstructorText, TkQVarId <$> genModuleText <*> genIdentifierText,