From 5cea26ac7f66095e55917d3397c663807c9424fc Mon Sep 17 00:00:00 2001 From: Murray Date: Thu, 3 Nov 2022 09:02:22 +0000 Subject: [PATCH] Improve As-Pattern parsing (#1603) * Allow naming nullary constructors without using parentheses * Negative test cases --- src/Juvix/Compiler/Abstract/Language.hs | 12 +++ src/Juvix/Compiler/Abstract/Pretty/Base.hs | 2 +- src/Juvix/Compiler/Concrete/Language.hs | 89 ++++++++++--------- src/Juvix/Compiler/Concrete/Pretty/Base.hs | 22 ++--- .../FromParsed/Analysis/Scoping.hs | 74 +++++++-------- .../Analysis/Scoping/Error/Types.hs | 24 ++--- .../Concrete/Translation/FromSource.hs | 20 ++--- src/Juvix/Compiler/Internal/Pretty/Base.hs | 2 +- test/Scope/Negative.hs | 14 +++ tests/negative/AsPatternAlias.juvix | 6 ++ tests/negative/NestedAsPatterns.juvix | 6 ++ tests/positive/Internal/AsPattern.juvix | 2 +- 12 files changed, 158 insertions(+), 115 deletions(-) create mode 100644 tests/negative/AsPatternAlias.juvix create mode 100644 tests/negative/NestedAsPatterns.juvix diff --git a/src/Juvix/Compiler/Abstract/Language.hs b/src/Juvix/Compiler/Abstract/Language.hs index 1d6aef00f..1bc55144e 100644 --- a/src/Juvix/Compiler/Abstract/Language.hs +++ b/src/Juvix/Compiler/Abstract/Language.hs @@ -224,6 +224,18 @@ makeLenses ''InductiveRef makeLenses ''AxiomRef makeLenses ''AxiomDef +instance HasAtomicity ConstructorApp where + atomicity (ConstructorApp _ ps) + | null ps = Atom + | otherwise = Aggregate appFixity + +instance HasAtomicity Pattern where + atomicity = \case + PatternVariable {} -> Atom + PatternConstructorApp a -> atomicity a + PatternWildcard {} -> Atom + PatternEmpty -> Atom + instance HasLoc InductiveConstructorDef where getLoc = getLoc . (^. constructorName) diff --git a/src/Juvix/Compiler/Abstract/Pretty/Base.hs b/src/Juvix/Compiler/Abstract/Pretty/Base.hs index ef27a7657..2173efc8e 100644 --- a/src/Juvix/Compiler/Abstract/Pretty/Base.hs +++ b/src/Juvix/Compiler/Abstract/Pretty/Base.hs @@ -101,7 +101,7 @@ instance PrettyCode PatternArg where ppCode (PatternArg i n p) = do n' <- traverse ppCode n p' <- ppCode p - return $ (n' <&> (<> kwAt)) ?<> delimIf i (isJust n) p' + return $ (n' <&> (<> kwAt)) ?<> delimIf i (isJust n && not (isAtomic p)) p' instance PrettyCode LambdaClause where ppCode LambdaClause {..} = do diff --git a/src/Juvix/Compiler/Concrete/Language.hs b/src/Juvix/Compiler/Concrete/Language.hs index 4428f10c9..8bfffe0b6 100644 --- a/src/Juvix/Compiler/Concrete/Language.hs +++ b/src/Juvix/Compiler/Concrete/Language.hs @@ -82,6 +82,11 @@ type family PatternParensType s = res | res -> s where PatternParensType 'Parsed = PatternAtoms 'Parsed PatternParensType 'Scoped = PatternArg +type PatternAtType :: Stage -> GHC.Type +type family PatternAtType s = res | res -> s where + PatternAtType 'Parsed = PatternBinding + PatternAtType 'Scoped = PatternArg + type family ImportType (s :: Stage) :: GHC.Type where ImportType 'Parsed = TopModulePath ImportType 'Scoped = Module 'Scoped 'ModuleTop @@ -319,12 +324,18 @@ data PatternScopedIden | PatternScopedConstructor ConstructorRef deriving stock (Show, Ord, Eq) +data PatternBinding = PatternBinding + { _patternBindingName :: Symbol, + _patternBindingPattern :: PatternAtom 'Parsed + } + data PatternAtom (s :: Stage) = PatternAtomIden (PatternAtomIdenType s) | PatternAtomWildcard Wildcard | PatternAtomEmpty Interval - | PatternAtomParens (Maybe (SymbolType s)) (PatternParensType s) - | PatternAtomBraces (Maybe (SymbolType s)) (PatternParensType s) + | PatternAtomParens (PatternParensType s) + | PatternAtomBraces (PatternParensType s) + | PatternAtomAt (PatternAtType s) data PatternAtoms (s :: Stage) = PatternAtoms { _patternAtoms :: NonEmpty (PatternAtom s), @@ -971,19 +982,38 @@ makeLenses ''PatternApp makeLenses ''PatternInfixApp makeLenses ''PatternPostfixApp makeLenses ''Compile +makeLenses ''PatternBinding makeLenses ''PatternAtoms makeLenses ''ExpressionAtoms instance HasAtomicity (PatternAtom 'Parsed) where atomicity = const Atom +deriving stock instance + ( Show Symbol, + Show (PatternAtom 'Parsed) + ) => + Show PatternBinding + +deriving stock instance + ( Eq Symbol, + Eq (PatternAtom 'Parsed) + ) => + Eq PatternBinding + +deriving stock instance + ( Ord Symbol, + Ord (PatternAtom 'Parsed) + ) => + Ord PatternBinding + deriving stock instance ( Show (ExpressionType s), Show (IdentifierType s), Show (PatternAtomIdenType s), Show (PatternParensType s), - Show (PatternType s), - Show (SymbolType s) + Show (PatternAtType s), + Show (PatternType s) ) => Show (PatternAtom s) @@ -992,8 +1022,8 @@ deriving stock instance Eq (IdentifierType s), Eq (PatternAtomIdenType s), Eq (PatternParensType s), - Eq (PatternType s), - Eq (SymbolType s) + Eq (PatternAtType s), + Eq (PatternType s) ) => Eq (PatternAtom s) @@ -1002,36 +1032,33 @@ deriving stock instance Ord (IdentifierType s), Ord (PatternAtomIdenType s), Ord (PatternParensType s), - Ord (PatternType s), - Ord (SymbolType s) + Ord (PatternAtType s), + Ord (PatternType s) ) => Ord (PatternAtom s) deriving stock instance - ( Show (ExpressionType s), - Show (IdentifierType s), - Show (PatternAtomIdenType s), - Show (PatternParensType s), - Show (PatternType s), - Show (SymbolType s) - ) => - Show (PatternAtoms s) + Show (PatternAtom s) => Show (PatternAtoms s) instance HasLoc PatternScopedIden where getLoc = \case PatternScopedVar v -> getLoc v PatternScopedConstructor c -> getLoc c +instance HasLoc PatternBinding where + getLoc (PatternBinding n p) = getLoc n <> getLoc p + instance SingI s => HasLoc (PatternAtom s) where getLoc = \case PatternAtomIden i -> getLocIden i PatternAtomWildcard w -> getLoc w PatternAtomEmpty i -> i - PatternAtomParens n p -> fmap getLocSym n ?<> getLocParens p - PatternAtomBraces n p -> fmap getLocSym n ?<> getLocParens p + PatternAtomParens p -> getLocParens p + PatternAtomBraces p -> getLocParens p + PatternAtomAt p -> getLocAt p where - getLocSym :: forall r. SingI r => SymbolType r -> Interval - getLocSym p = case sing :: SStage r of + getLocAt :: forall r. SingI r => PatternAtType r -> Interval + getLocAt p = case sing :: SStage r of SParsed -> getLoc p SScoped -> getLoc p getLocIden :: forall r. SingI r => PatternAtomIdenType r -> Interval @@ -1069,28 +1096,10 @@ instance HasLoc Pattern where PatternInfixApplication i -> getLoc i PatternPostfixApplication i -> getLoc i -instance - ( Eq (ExpressionType s), - Eq (IdentifierType s), - Eq (PatternAtomIdenType s), - Eq (PatternParensType s), - Eq (PatternType s), - Eq (SymbolType s) - ) => - Eq (PatternAtoms s) - where +instance Eq (PatternAtom s) => Eq (PatternAtoms s) where (==) = (==) `on` (^. patternAtoms) -instance - ( Ord (ExpressionType s), - Ord (IdentifierType s), - Ord (PatternAtomIdenType s), - Ord (PatternParensType s), - Ord (PatternType s), - Ord (SymbolType s) - ) => - Ord (PatternAtoms s) - where +instance Ord (PatternAtom s) => Ord (PatternAtoms s) where compare = compare `on` (^. patternAtoms) deriving stock instance diff --git a/src/Juvix/Compiler/Concrete/Pretty/Base.hs b/src/Juvix/Compiler/Concrete/Pretty/Base.hs index d03632011..4626d5f06 100644 --- a/src/Juvix/Compiler/Concrete/Pretty/Base.hs +++ b/src/Juvix/Compiler/Concrete/Pretty/Base.hs @@ -551,7 +551,7 @@ instance PrettyCode PatternArg where ppCode (PatternArg i n p) = do n' <- traverse ppCode n p' <- ppCode p - return $ (n' <&> (<> kwAt)) ?<> delimIf i (isJust n) p' + return $ (n' <&> (<> kwAt)) ?<> delimIf i (isJust n && not (isAtomic p)) p' instance PrettyCode PatternApp where ppCode (PatternApp l r) = do @@ -564,6 +564,12 @@ ppPatternParenType p = case sing :: SStage s of SParsed -> ppCode p SScoped -> ppCode p +instance PrettyCode PatternBinding where + ppCode (PatternBinding n p) = do + n' <- ppSymbol n + p' <- ppCode p + return $ n' <> kwAt <> p' + instance SingI s => PrettyCode (PatternAtom s) where ppCode a = case a of PatternAtomIden n -> case sing :: SStage s of @@ -571,15 +577,11 @@ instance SingI s => PrettyCode (PatternAtom s) where SScoped -> ppCode n PatternAtomWildcard {} -> return kwWildcard PatternAtomEmpty {} -> return $ parens mempty - PatternAtomParens n p -> ppEnclosed parens n p - PatternAtomBraces n p -> ppEnclosed braces n p - where - ppEnclosed :: Member (Reader Options) r => (Doc Ann -> Doc Ann) -> Maybe (SymbolType s) -> PatternParensType s -> Sem r (Doc Ann) - ppEnclosed wrap Nothing p = wrap <$> ppPatternParenType p - ppEnclosed wrap (Just n) p = do - n' <- ppSymbol n - p' <- ppPatternParenType p - return $ n' <> kwAt <> wrap p' + PatternAtomParens p -> parens <$> ppPatternParenType p + PatternAtomBraces p -> braces <$> ppPatternParenType p + PatternAtomAt p -> case sing :: SStage s of + SParsed -> ppCode p + SScoped -> ppCode p instance SingI s => PrettyCode (PatternAtoms s) where ppCode (PatternAtoms ps _) = hsep <$> mapM ppCode ps diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index edeeceada..b13d4f3ca 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -1086,6 +1086,17 @@ checkPatternName n = do EntryConstructor r -> Just r _ -> Nothing +checkPatternBinding :: + Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r => + PatternBinding -> + Sem r PatternArg +checkPatternBinding (PatternBinding n p) = do + n' <- groupBindLocalVariable n + p' <- checkParsePatternAtom p + if isJust (p' ^. patternArgName) + then throw (ErrDoubleBinderPattern (DoubleBinderPattern n' p')) + else return $ set patternArgName (Just n') p' + withBindCurrentGroup :: Members '[State Scope, Reader LocalVars] r => Sem r a -> @@ -1146,12 +1157,13 @@ checkPatternAtom :: Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r => PatternAtom 'Parsed -> Sem r (PatternAtom 'Scoped) -checkPatternAtom p = case p of +checkPatternAtom = \case PatternAtomIden n -> PatternAtomIden <$> checkPatternName n PatternAtomWildcard i -> return (PatternAtomWildcard i) PatternAtomEmpty i -> return (PatternAtomEmpty i) - PatternAtomParens n e -> PatternAtomParens <$> traverse groupBindLocalVariable n <*> (checkPatternAtoms e >>= parsePatternAtoms) - PatternAtomBraces n a -> PatternAtomBraces <$> traverse groupBindLocalVariable n <*> (checkPatternAtoms a >>= parsePatternAtoms) + PatternAtomParens e -> PatternAtomParens <$> (checkPatternAtoms e >>= parsePatternAtoms) + PatternAtomBraces a -> PatternAtomBraces <$> (checkPatternAtoms a >>= parsePatternAtoms) + PatternAtomAt p -> PatternAtomAt <$> checkPatternBinding p checkName :: Members '[Error ScoperError, State Scope, Reader LocalVars, State ScoperState, InfoTableBuilder] r => @@ -1544,6 +1556,7 @@ parsePatternTerm = do <|> parseBraces <|> parseWildcard <|> parseEmpty + <|> parseAt where parseNoInfixConstructor :: ParsePat PatternArg parseNoInfixConstructor = @@ -1574,6 +1587,20 @@ parsePatternTerm = do PatternAtomEmpty i -> Just i _ -> Nothing + parseAt :: ParsePat PatternArg + parseAt = do + res <- P.token isAt mempty + case res of + Left e -> P.lift (throw e) + Right a -> return a + where + isAt :: PatternAtom 'Scoped -> Maybe (Either ScoperError PatternArg) + isAt = \case + PatternAtomAt p -> Just $ case p ^. patternArgPattern of + PatternVariable _ -> Left (ErrAliasBinderPattern (AliasBinderPattern p)) + _ -> Right p + _ -> Nothing + parseVariable :: ParsePat PatternArg parseVariable = explicitP . PatternVariable <$> P.token var mempty where @@ -1590,44 +1617,21 @@ parsePatternTerm = do Right a -> return a where bracesPat :: PatternAtom 'Scoped -> Maybe (Either ScoperError PatternArg) - bracesPat s = case s of - PatternAtomBraces n r -> Just $ case r ^. patternArgIsImplicit of - Implicit -> Left (ErrDoubleBracesPattern (DoubleBracesPattern r)) - Explicit -> case (n, r ^. patternArgName) of - (Just n', Just _) -> Left (ErrDoubleBinderPattern (DoubleBinderPattern Implicit n' r)) - (Just n', Nothing) -> - if isConstr (r ^. patternArgPattern) - then Right (PatternArg Implicit (Just n') (r ^. patternArgPattern)) - else Left (ErrAliasBinderPattern (AliasBinderPattern Implicit n' r)) - _ -> Right (set patternArgIsImplicit Implicit r) + bracesPat = \case + PatternAtomBraces r + | Implicit <- r ^. patternArgIsImplicit -> + Just (Left (ErrDoubleBracesPattern (DoubleBracesPattern r))) + | otherwise -> Just (Right (set patternArgIsImplicit Implicit r)) _ -> Nothing parseParens :: ParsePat PatternArg - parseParens = do - res <- P.token parenPat mempty - case res of - Left e -> P.lift (throw e) - Right a -> return a + parseParens = P.token parenPat mempty where - parenPat :: PatternAtom 'Scoped -> Maybe (Either ScoperError PatternArg) - parenPat s = case s of - PatternAtomParens Nothing r -> Just (Right r) - PatternAtomParens n@(Just n') r -> Just $ case r ^. patternArgName of - Just _ -> Left (ErrDoubleBinderPattern (DoubleBinderPattern Explicit n' r)) - Nothing -> - if isConstr (r ^. patternArgPattern) - then Right (set patternArgName n r) - else Left (ErrAliasBinderPattern (AliasBinderPattern Explicit n' r)) + parenPat :: PatternAtom 'Scoped -> Maybe PatternArg + parenPat = \case + PatternAtomParens r -> Just r _ -> Nothing - isConstr :: Pattern -> Bool - isConstr = \case - PatternConstructor {} -> True - PatternApplication {} -> True - PatternInfixApplication {} -> True - PatternPostfixApplication {} -> True - _ -> False - mkPatternParser :: forall r. Members '[Embed ParsePat] r => diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs index b9b3b098d..b58deaf13 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs @@ -660,8 +660,7 @@ instance ToGenericError DoubleBracesPattern where <+> code (braces (ppCode opts' pat)) data DoubleBinderPattern = DoubleBinderPattern - { _doubleBinderPatternIsImplicit :: IsImplicit, - _doubleBinderPatternName :: S.Symbol, + { _doubleBinderPatternName :: S.Symbol, _doubleBinderPatternArg :: PatternArg } deriving stock (Show) @@ -681,17 +680,14 @@ instance ToGenericError DoubleBinderPattern where where opts' = fromGenericOptions opts name = e ^. doubleBinderPatternName - implicit = e ^. doubleBinderPatternIsImplicit pat = e ^. doubleBinderPatternArg i = getLoc pat msg = - "As-patterns cannot be nested:" - <+> code (ppCode opts' name <> kwAt <> implicitDelim implicit (ppCode opts' pat)) + "As-Patterns cannot be nested:" + <+> code (ppCode opts' name <> kwAt <> parens (ppCode opts' pat)) -data AliasBinderPattern = AliasBinderPattern - { _aliasBinderPatternIsImplicit :: IsImplicit, - _aliasBinderPatternName :: S.Symbol, - _aliasBinderPatternArg :: PatternArg +newtype AliasBinderPattern = AliasBinderPattern + { _aliasBinderPatternArg :: PatternArg } deriving stock (Show) @@ -709,17 +705,11 @@ instance ToGenericError AliasBinderPattern where } where opts' = fromGenericOptions opts - name = e ^. aliasBinderPatternName - implicit = e ^. aliasBinderPatternIsImplicit pat = e ^. aliasBinderPatternArg i = getLoc pat - wrap = case implicit of - Implicit -> "braces" - Explicit -> "parentheses" msg = - "As-patterns require a constructor inside the" - <+> wrap <> ":" - <+> code (ppCode opts' name <> kwAt <> implicitDelim implicit (ppCode opts' pat)) + "As-Patterns cannot be used to alias pattern variables:" + <+> code (ppCode opts' pat) newtype ImplicitPatternLeftApplication = ImplicitPatternLeftApplication { _implicitPatternLeftApplication :: PatternApp diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs index 4b257a95f..907d17e35 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs @@ -512,24 +512,24 @@ wildcard = Wildcard . snd <$> interval (kw kwWildcard) -- Pattern section -------------------------------------------------------------------------------- -patternAtomDelim :: Members '[InfoTableBuilder, JudocStash, NameIdGen] r => Maybe (SymbolType 'Parsed) -> ParsecS r (PatternAtom 'Parsed) -patternAtomDelim n = - PatternAtomParens n <$> parens parsePatternAtoms - <|> PatternAtomBraces n <$> braces parsePatternAtoms +patternAtomAnon :: Members '[InfoTableBuilder, JudocStash, NameIdGen] r => ParsecS r (PatternAtom 'Parsed) +patternAtomAnon = + PatternAtomWildcard <$> wildcard + <|> PatternAtomParens <$> parens parsePatternAtoms + <|> PatternAtomBraces <$> braces parsePatternAtoms + +patternAtomAt :: Members '[InfoTableBuilder, JudocStash, NameIdGen] r => SymbolType 'Parsed -> ParsecS r (PatternAtom 'Parsed) +patternAtomAt s = kw kwAt >> PatternAtomAt . PatternBinding s <$> patternAtom patternAtomNamed :: Members '[InfoTableBuilder, JudocStash, NameIdGen] r => ParsecS r (PatternAtom 'Parsed) patternAtomNamed = do n <- name case n of NameQualified _ -> return (PatternAtomIden n) - NameUnqualified s -> (kw kwAt >> patternAtomDelim (Just s)) <|> return (PatternAtomIden n) + NameUnqualified s -> patternAtomAt s <|> return (PatternAtomIden n) patternAtom :: Members '[InfoTableBuilder, JudocStash, NameIdGen] r => ParsecS r (PatternAtom 'Parsed) -patternAtom = - P.label "" $ - patternAtomNamed - <|> PatternAtomWildcard <$> wildcard - <|> patternAtomDelim Nothing +patternAtom = P.label "" $ patternAtomNamed <|> patternAtomAnon parsePatternAtoms :: Members '[InfoTableBuilder, JudocStash, NameIdGen] r => ParsecS r (PatternAtoms 'Parsed) parsePatternAtoms = do diff --git a/src/Juvix/Compiler/Internal/Pretty/Base.hs b/src/Juvix/Compiler/Internal/Pretty/Base.hs index d5d3c1cfb..2d3bc98cf 100644 --- a/src/Juvix/Compiler/Internal/Pretty/Base.hs +++ b/src/Juvix/Compiler/Internal/Pretty/Base.hs @@ -135,7 +135,7 @@ instance PrettyCode PatternArg where ppCode (PatternArg i n p) = do n' <- traverse ppCode n p' <- ppCode p - return $ (n' <&> (<> kwAt)) ?<> delimIf i (isJust n) p' + return $ (n' <&> (<> kwAt)) ?<> delimIf i (isJust n && not (isAtomic p)) p' instance PrettyCode ConstructorApp where ppCode c = do diff --git a/test/Scope/Negative.hs b/test/Scope/Negative.hs index d9aaa9936..e646f28da 100644 --- a/test/Scope/Negative.hs +++ b/test/Scope/Negative.hs @@ -212,6 +212,20 @@ scoperErrorTests = $ \case ErrDoubleBracesPattern {} -> Nothing _ -> wrongError, + NegTest + "As-Pattern aliasing variable" + "." + "AsPatternAlias.juvix" + $ \case + ErrAliasBinderPattern {} -> Nothing + _ -> wrongError, + NegTest + "Nested As-Patterns" + "." + "NestedAsPatterns.juvix" + $ \case + ErrDoubleBinderPattern {} -> Nothing + _ -> wrongError, NegTest "Pattern matching an implicit argument on the left of an application" "." diff --git a/tests/negative/AsPatternAlias.juvix b/tests/negative/AsPatternAlias.juvix new file mode 100644 index 000000000..da9da2d07 --- /dev/null +++ b/tests/negative/AsPatternAlias.juvix @@ -0,0 +1,6 @@ +module AsPatternAlias; + +f : Type -> Type; +f a@b := b; + +end; diff --git a/tests/negative/NestedAsPatterns.juvix b/tests/negative/NestedAsPatterns.juvix new file mode 100644 index 000000000..e0bc2fbe2 --- /dev/null +++ b/tests/negative/NestedAsPatterns.juvix @@ -0,0 +1,6 @@ +module NestedAsPatterns; + +f : Type -> Type; +f a@b@_ := a; + +end; diff --git a/tests/positive/Internal/AsPattern.juvix b/tests/positive/Internal/AsPattern.juvix index 3b0d4d01b..9d6e69d9a 100644 --- a/tests/positive/Internal/AsPattern.juvix +++ b/tests/positive/Internal/AsPattern.juvix @@ -32,7 +32,7 @@ lambda : Nat → Nat → Nat; lambda x := λ { a@(suc _) := a + x + zero }; a : {A : Type} → (A × Nat) → Nat; -a p@(x, s@(zero)) := snd p + 1; +a p@(x, s@zero) := snd p + 1; b : {A : Type} → (A × Nat) → ({B : Type} → B → B) → A; b p@(_, zero) f := (f ∘ fst) p;