Improve As-Pattern parsing (#1603)

* Allow naming nullary constructors without using parentheses
* Negative test cases

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)
 

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

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

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

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 =>

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

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 "<pattern>" $
-    patternAtomNamed
-      <|> PatternAtomWildcard <$> wildcard
-      <|> patternAtomDelim Nothing
+patternAtom = P.label "<pattern>" $ patternAtomNamed <|> patternAtomAnon
 
 parsePatternAtoms :: Members '[InfoTableBuilder, JudocStash, NameIdGen] r => ParsecS r (PatternAtoms 'Parsed)
 parsePatternAtoms = do

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

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"
       "."

tests/negative/AsPatternAlias.juvix

@@ -0,0 +1,6 @@
+module AsPatternAlias;
+
+f : Type -> Type;
+f a@b := b;
+
+end;

tests/negative/NestedAsPatterns.juvix

@@ -0,0 +1,6 @@
+module NestedAsPatterns;
+
+f : Type -> Type;
+f a@b@_ := a;
+
+end;

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;