implement error for double braces

src/Juvix/Syntax/Concrete/Scoped/Error.hs

@@ -33,6 +33,7 @@ data ScoperError
   | ErrMultipleCompileRuleSameBackend MultipleCompileRuleSameBackend
   | ErrWrongKindExpressionCompileBlock WrongKindExpressionCompileBlock
   | ErrDuplicateInductiveParameterName DuplicateInductiveParameterName
+  | ErrDoubleBracesPattern DoubleBracesPattern
   deriving stock (Show)
 
 instance ToGenericError ScoperError where
@@ -60,3 +61,4 @@ instance ToGenericError ScoperError where
     ErrMultipleCompileRuleSameBackend e -> genericError e
     ErrWrongKindExpressionCompileBlock e -> genericError e
     ErrDuplicateInductiveParameterName e -> genericError e
+    ErrDoubleBracesPattern e -> genericError e

src/Juvix/Syntax/Concrete/Scoped/Error/Types.hs

@@ -546,3 +546,26 @@ instance ToGenericError DuplicateInductiveParameterName where
             <> "."
             <> line
             <> "Inductive parameter names can not be repeated."
+
+newtype DoubleBracesPattern = DoubleBracesPattern
+  { _doubleBracesPatternArg :: PatternArg
+  }
+  deriving stock (Show)
+
+makeLenses ''DoubleBracesPattern
+
+instance ToGenericError DoubleBracesPattern where
+  genericError e =
+    GenericError
+      { _genericErrorLoc = i,
+        _genericErrorMessage = prettyError msg,
+        _genericErrorIntervals = [i]
+      }
+    where
+      pat :: PatternArg
+      pat = e ^. doubleBracesPatternArg
+      i = getLoc (e ^. doubleBracesPatternArg)
+      msg =
+        "Double braces are not valid:"
+        -- TODO add bold to braces
+          <+> braces (ppCode pat)

src/Juvix/Syntax/Concrete/Scoped/Scoper.hs

@@ -1420,7 +1420,7 @@ parseTerm =
 -- Infix Patterns
 -------------------------------------------------------------------------------
 
-type ParsePat = P.Parsec () [PatternAtom 'Scoped]
+type ParsePat = P.ParsecT () [PatternAtom 'Scoped] (Sem '[Error ScoperError])
 
 makePatternTable ::
   PatternAtoms 'Scoped -> [[P.Operator ParsePat PatternArg]]
@@ -1543,11 +1543,18 @@ parsePatternTerm = do
           _ -> Nothing
 
     parseBraces :: ParsePat PatternArg
-    parseBraces = P.token bracesPat mempty
+    parseBraces = do
+      res <- P.token bracesPat mempty
+      case res of
+        Left er -> P.lift (throw er)
+        Right a -> return a
       where
-        bracesPat :: PatternAtom 'Scoped -> Maybe PatternArg
+        bracesPat :: PatternAtom 'Scoped -> Maybe (Either ScoperError PatternArg)
         bracesPat s = case s of
-          PatternAtomBraces r -> Just (set patternArgIsImplicit Implicit r)
+          PatternAtomBraces r
+            | Implicit <- r ^. patternArgIsImplicit ->
+              Just (Left (ErrDoubleBracesPattern (DoubleBracesPattern r)))
+            | otherwise -> Just (Right (set patternArgIsImplicit Implicit r))
           _ -> Nothing
 
     parseParens :: ParsePat PatternArg
@@ -1587,15 +1594,16 @@ parsePatternAtoms ::
   PatternAtoms 'Scoped ->
   Sem r PatternArg
 parsePatternAtoms atoms@(PatternAtoms sec' _) = do
-  case res of
-    Left {} -> throw (ErrInfixPattern (InfixErrorP atoms))
-    Right r -> return r
+  case run (runError res) of
+    Left e -> throw e -- Scoper effect error
+    Right Left {} -> throw (ErrInfixPattern (InfixErrorP atoms)) -- Megaparsec error
+    Right (Right r) -> return r
   where
     sec = toList sec'
     tbl = makePatternTable atoms
     parser :: ParsePat PatternArg
     parser = runM (mkPatternParser tbl) <* P.eof
-    res = P.parse parser filePath sec
+    res = P.runParserT parser filePath sec
 
     filePath :: FilePath
     filePath = "tmp"

test/Scope/Negative.hs

@@ -205,6 +205,13 @@ scoperErrorTests =
       $ \case
         ErrQualSymNotInScope {} -> Nothing
         _ -> wrongError,
+    NegTest
+      "Double braces in pattern"
+      "."
+      "NestedPatternBraces.juvix"
+      $ \case
+        ErrDoubleBracesPattern {} -> Nothing
+        _ -> wrongError,
     NegTest
       "Compile block for a unsupported kind of expression"
       "CompileBlocks"

tests/negative/NestedPatternBraces.juvix

@@ -0,0 +1,6 @@
+module NestedPatternBraces;
+
+a : {A : Type} → Type;
+a {{A}} ≔ a;
+
+end;