remove pattern braces from scoped syntax

src/Juvix/Syntax/Concrete/Language.hs

@@ -83,7 +83,7 @@ type family ExpressionType s = res | res -> s where
 type PatternType :: Stage -> GHC.Type
 type family PatternType s = res | res -> s where
   PatternType 'Parsed = PatternAtom 'Parsed
-  PatternType 'Scoped = Pattern
+  PatternType 'Scoped = PatternArg
 
 type family ImportType (s :: Stage) :: GHC.Type where
   ImportType 'Parsed = TopModulePath
@@ -257,37 +257,42 @@ deriving stock instance (Ord (ExpressionType s), Ord (SymbolType s)) => Ord (Ind
 --------------------------------------------------------------------------------
 
 data PatternApp = PatternApp
-  { _patAppLeft :: Pattern,
-    _patAppRight :: Pattern
+  { _patAppLeft :: PatternArg,
+    _patAppRight :: PatternArg
   }
   deriving stock (Show, Eq, Ord)
 
 data PatternInfixApp = PatternInfixApp
-  { _patInfixLeft :: Pattern,
+  { _patInfixLeft :: PatternArg,
     _patInfixConstructor :: ConstructorRef,
-    _patInfixRight :: Pattern
+    _patInfixRight :: PatternArg
   }
   deriving stock (Show, Eq, Ord)
 
 instance HasFixity PatternInfixApp where
   getFixity (PatternInfixApp _ op _) = fromMaybe impossible (op ^. constructorRefName . S.nameFixity)
 
 data PatternPostfixApp = PatternPostfixApp
-  { _patPostfixParameter :: Pattern,
+  { _patPostfixParameter :: PatternArg,
     _patPostfixConstructor :: ConstructorRef
   }
   deriving stock (Show, Eq, Ord)
 
 instance HasFixity PatternPostfixApp where
   getFixity (PatternPostfixApp _ op) = fromMaybe impossible (op ^. constructorRefName . S.nameFixity)
 
+data PatternArg = PatternArg
+  { _patternArgIsImplicit :: IsImplicit,
+    _patternArgPattern :: Pattern
+  }
+  deriving stock (Show, Eq, Ord)
+
 data Pattern
   = PatternVariable (SymbolType 'Scoped)
   | PatternConstructor ConstructorRef
   | PatternApplication PatternApp
   | PatternInfixApplication PatternInfixApp
   | PatternPostfixApplication PatternPostfixApp
-  | PatternBraces Pattern
   | PatternWildcard Wildcard
   | PatternEmpty
   deriving stock (Show, Eq, Ord)
@@ -300,7 +305,6 @@ instance HasAtomicity Pattern where
     PatternInfixApplication a -> Aggregate (getFixity a)
     PatternPostfixApplication p -> Aggregate (getFixity p)
     PatternWildcard {} -> Atom
-    PatternBraces {} -> Atom
     PatternEmpty -> Atom
 
 --------------------------------------------------------------------------------
@@ -887,8 +891,7 @@ data ExpressionAtoms (s :: Stage) = ExpressionAtoms
     _expressionAtomsLoc :: Interval
   }
 
---------------------------------------------------------------------------------
-
+makeLenses ''PatternArg
 makeLenses ''Function
 makeLenses ''InductiveDef
 makeLenses ''PostfixApplication
@@ -1048,6 +1051,11 @@ instance
 
 --------------------------------------------------------------------------------
 
+instance HasAtomicity PatternArg where
+  atomicity p
+    | Implicit <- p ^. patternArgIsImplicit = Atom
+    | otherwise = atomicity (p ^. patternArgPattern)
+
 idenOverName :: (forall s. S.Name' s -> S.Name' s) -> ScopedIden -> ScopedIden
 idenOverName f = \case
   ScopedAxiom a -> ScopedAxiom (over axiomRefName f a)

src/Juvix/Syntax/Concrete/Scoped/Pretty/Base.hs

@@ -448,6 +448,9 @@ instance PrettyCode QualifiedName where
     let symbols = _qualifiedPath ^. pathParts NonEmpty.|> _qualifiedSymbol
     dotted <$> mapM ppSymbol symbols
 
+bracesIf :: Bool -> Doc Ann -> Doc Ann
+bracesIf t = if t then braces else id
+
 ppName :: forall s r. (SingI s, Members '[Reader Options] r) => IdentifierType s -> Sem r (Doc Ann)
 ppName = case sing :: SStage s of
   SParsed -> ppCode
@@ -652,6 +655,11 @@ instance PrettyCode PatternScopedIden where
     PatternScopedVar v -> ppCode v
     PatternScopedConstructor c -> ppCode c
 
+instance PrettyCode PatternArg where
+  ppCode a = do
+    p <- ppCode (a ^. patternArgPattern)
+    return (bracesIf (Implicit == a ^. patternArgIsImplicit) p)
+
 instance SingI s => PrettyCode (PatternAtom s) where
   ppCode a = case a of
     PatternAtomIden n -> case sing :: SStage s of
@@ -750,7 +758,6 @@ instance PrettyCode Pattern where
       return $ l' <+> r'
     PatternWildcard {} -> return kwWildcard
     PatternEmpty -> return $ parens mempty
-    PatternBraces p -> braces <$> ppCode p
     PatternConstructor constr -> ppCode constr
     PatternInfixApplication i -> ppPatternInfixApp i
     PatternPostfixApplication i -> ppPatternPostfixApp i

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

@@ -1198,7 +1198,7 @@ checkParseExpressionAtoms = checkExpressionAtoms >=> parseExpressionAtoms
 checkParsePatternAtom ::
   Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r =>
   PatternAtom 'Parsed ->
-  Sem r Pattern
+  Sem r PatternArg
 checkParsePatternAtom = checkPatternAtom >=> parsePatternAtom
 
 checkStatement ::
@@ -1423,7 +1423,7 @@ parseTerm =
 type ParsePat = P.Parsec () [PatternAtom 'Scoped]
 
 makePatternTable ::
-  PatternAtom 'Scoped -> [[P.Operator ParsePat Pattern]]
+  PatternAtom 'Scoped -> [[P.Operator ParsePat PatternArg]]
 makePatternTable atom = [appOp] : operators
   where
     getConstructorRef :: PatternAtom 'Scoped -> Maybe ConstructorRef
@@ -1437,24 +1437,24 @@ makePatternTable atom = [appOp] : operators
     constructorRefs = case atom of
       PatternAtomParens (PatternAtoms atoms _) -> mapMaybe getConstructorRef (toList atoms)
       _ -> []
-    mkSymbolTable :: [ConstructorRef] -> [[P.Operator ParsePat Pattern]]
+    mkSymbolTable :: [ConstructorRef] -> [[P.Operator ParsePat PatternArg]]
     mkSymbolTable = reverse . map (map snd) . groupSortOn' fst . mapMaybe unqualifiedSymbolOp
       where
-        unqualifiedSymbolOp :: ConstructorRef -> Maybe (Precedence, P.Operator ParsePat Pattern)
+        unqualifiedSymbolOp :: ConstructorRef -> Maybe (Precedence, P.Operator ParsePat PatternArg)
         unqualifiedSymbolOp (ConstructorRef' S.Name' {..})
           | Just Fixity {..} <- _nameFixity,
             _nameKind == S.KNameConstructor = Just $
               case _fixityArity of
                 Unary u -> (_fixityPrecedence, P.Postfix (unaryApp <$> parseSymbolId _nameId))
                   where
-                    unaryApp :: ConstructorRef -> Pattern -> Pattern
+                    unaryApp :: ConstructorRef -> PatternArg -> PatternArg
                     unaryApp funName = case u of
-                      AssocPostfix -> PatternPostfixApplication . (`PatternPostfixApp` funName)
+                      AssocPostfix -> explicitP . PatternPostfixApplication . (`PatternPostfixApp` funName)
                 Binary b -> (_fixityPrecedence, infixLRN (binaryInfixApp <$> parseSymbolId _nameId))
                   where
-                    binaryInfixApp :: ConstructorRef -> Pattern -> Pattern -> Pattern
-                    binaryInfixApp name argLeft = PatternInfixApplication . PatternInfixApp argLeft name
-                    infixLRN :: ParsePat (Pattern -> Pattern -> Pattern) -> P.Operator ParsePat Pattern
+                    binaryInfixApp :: ConstructorRef -> PatternArg -> PatternArg -> PatternArg
+                    binaryInfixApp name argLeft = explicitP . PatternInfixApplication . PatternInfixApp argLeft name
+                    infixLRN :: ParsePat (PatternArg -> PatternArg -> PatternArg) -> P.Operator ParsePat PatternArg
                     infixLRN = case b of
                       AssocLeft -> P.InfixL
                       AssocRight -> P.InfixR
@@ -1470,22 +1470,30 @@ makePatternTable atom = [appOp] : operators
               return ref
 
     -- Application by juxtaposition.
-    appOp :: P.Operator ParsePat Pattern
+    appOp :: P.Operator ParsePat PatternArg
     appOp = P.InfixL (return app)
       where
-        app :: Pattern -> Pattern -> Pattern
+        app :: PatternArg -> PatternArg -> PatternArg
         app l r =
-          PatternApplication
-            ( PatternApp
-                { _patAppLeft = l,
-                  _patAppRight = r
-                }
+          explicitP
+            ( PatternApplication
+                ( PatternApp
+                    { _patAppLeft = l,
+                      _patAppRight = r
+                    }
+                )
             )
 
+explicitP :: Pattern -> PatternArg
+explicitP = PatternArg Explicit
+
+implicitP :: Pattern -> PatternArg
+implicitP = PatternArg Implicit
+
 parsePatternTerm ::
   forall r.
-  Members '[Reader (ParsePat Pattern), Embed ParsePat] r =>
-  Sem r Pattern
+  Members '[Reader (ParsePat PatternArg), Embed ParsePat] r =>
+  Sem r PatternArg
 parsePatternTerm = do
   pPat <- ask
   embed @ParsePat $
@@ -1496,9 +1504,9 @@ parsePatternTerm = do
       <|> parseWildcard
       <|> parseEmpty
   where
-    parseNoInfixConstructor :: ParsePat Pattern
+    parseNoInfixConstructor :: ParsePat PatternArg
     parseNoInfixConstructor =
-      PatternConstructor
+      explicitP . PatternConstructor
         <$> P.token constructorNoFixity mempty
       where
         constructorNoFixity :: PatternAtom 'Scoped -> Maybe ConstructorRef
@@ -1509,43 +1517,46 @@ parsePatternTerm = do
               n = ref ^. constructorRefName
           _ -> Nothing
 
-    parseWildcard :: ParsePat Pattern
-    parseWildcard = PatternWildcard <$> P.token isWildcard mempty
+    parseWildcard :: ParsePat PatternArg
+    parseWildcard = explicitP . PatternWildcard <$> P.token isWildcard mempty
       where
         isWildcard :: PatternAtom 'Scoped -> Maybe Wildcard
         isWildcard s = case s of
           PatternAtomWildcard i -> Just i
           _ -> Nothing
 
-    parseEmpty :: ParsePat Pattern
-    parseEmpty = PatternEmpty <$ P.satisfy isEmpty
+    parseEmpty :: ParsePat PatternArg
+    parseEmpty = explicitP PatternEmpty <$ P.satisfy isEmpty
       where
         isEmpty :: PatternAtom 'Scoped -> Bool
         isEmpty s = case s of
           PatternAtomEmpty -> True
           _ -> False
 
-    parseVariable :: ParsePat Pattern
-    parseVariable = PatternVariable <$> P.token var mempty
+    parseVariable :: ParsePat PatternArg
+    parseVariable = explicitP . PatternVariable <$> P.token var mempty
       where
         var :: PatternAtom 'Scoped -> Maybe S.Symbol
         var s = case s of
           PatternAtomIden (PatternScopedVar sym) -> Just sym
           _ -> Nothing
 
-    parseBraces :: ParsePat Pattern -> ParsePat Pattern
+    parseBraces :: ParsePat PatternArg -> ParsePat PatternArg
     parseBraces patternParser = do
       exprs <- P.token bracesPat mempty
       case P.parse patternParser "" exprs of
-        Right r -> return (PatternBraces r)
+        Right (PatternArg i p)
+          -- TODO proper error
+          | Implicit <- i -> error "nested braces"
+          | otherwise -> return (implicitP p)
         Left {} -> mzero
       where
         bracesPat :: PatternAtom 'Scoped -> Maybe [PatternAtom 'Scoped]
         bracesPat s = case s of
           PatternAtomBraces (PatternAtoms ss _) -> Just (toList ss)
           _ -> Nothing
 
-    parseParens :: ParsePat Pattern -> ParsePat Pattern
+    parseParens :: ParsePat PatternArg -> ParsePat PatternArg
     parseParens patternParser = do
       exprs <- P.token parenPat mempty
       case P.parse patternParser "" exprs of
@@ -1560,22 +1571,22 @@ parsePatternTerm = do
 mkPatternParser ::
   forall r.
   Members '[Embed ParsePat] r =>
-  [[P.Operator ParsePat Pattern]] ->
-  Sem r Pattern
+  [[P.Operator ParsePat PatternArg]] ->
+  Sem r PatternArg
 mkPatternParser table = embed @ParsePat pPattern
   where
-    pPattern :: ParsePat Pattern
+    pPattern :: ParsePat PatternArg
     pPattern = P.makeExprParser pTerm table
-    pTerm :: ParsePat Pattern
+    pTerm :: ParsePat PatternArg
     pTerm = runM parseTermRec
       where
-        parseTermRec :: Sem '[Embed ParsePat] Pattern
+        parseTermRec :: Sem '[Embed ParsePat] PatternArg
         parseTermRec = runReader pPattern parsePatternTerm
 
 parsePatternAtom ::
   Members '[Error ScoperError, State Scope] r =>
   PatternAtom 'Scoped ->
-  Sem r Pattern
+  Sem r PatternArg
 parsePatternAtom sec = do
   case res of
     Left {} -> case sec of
@@ -1584,7 +1595,7 @@ parsePatternAtom sec = do
     Right r -> return r
   where
     tbl = makePatternTable sec
-    parser :: ParsePat Pattern
+    parser :: ParsePat PatternArg
     parser = runM (mkPatternParser tbl) <* P.eof
     res = P.parse parser filePath [sec]
 

src/Juvix/Translation/ScopedToAbstract.hs

@@ -365,7 +365,7 @@ viewApp = \case
   PatternConstructor c -> return (goConstructorRef c, [])
   PatternApplication (PatternApp l r) -> do
     r' <- goPatternArg r
-    second (`snoc` r') <$> viewApp l
+    second (`snoc` r') <$> viewAppLeft l
   PatternInfixApplication (PatternInfixApp l c r) -> do
     l' <- goPatternArg l
     r' <- goPatternArg r
@@ -375,19 +375,28 @@ viewApp = \case
     return (goConstructorRef c, [l'])
   PatternVariable {} -> err
   PatternWildcard {} -> err
-  PatternBraces {} -> err
   PatternEmpty {} -> err
   where
+    viewAppLeft :: PatternArg -> Sem r (Abstract.ConstructorRef, [Abstract.PatternArg])
+    viewAppLeft p
+      -- TODO proper error
+      | Implicit <- p ^. patternArgIsImplicit = error "An implicit pattern cannot be on the left of an application"
+      | otherwise = viewApp (p ^. patternArgPattern)
+    -- TODO proper error
     err :: a
     err = error "constructor expected on the left of a pattern application"
 
 goConstructorRef :: ConstructorRef -> Abstract.ConstructorRef
 goConstructorRef (ConstructorRef' n) = Abstract.ConstructorRef (goName n)
 
-goPatternArg :: Pattern -> Sem r Abstract.PatternArg
-goPatternArg = \case
-  PatternBraces p -> Abstract.PatternArg Implicit <$> goPattern p
-  p -> Abstract.PatternArg Explicit <$> goPattern p
+goPatternArg :: PatternArg -> Sem r Abstract.PatternArg
+goPatternArg p = do
+  pat' <- goPattern (p ^. patternArgPattern)
+  return
+    Abstract.PatternArg
+      { _patternArgIsImplicit = p ^. patternArgIsImplicit,
+        _patternArgPattern = pat'
+      }
 
 goPattern :: Pattern -> Sem r Abstract.Pattern
 goPattern p = case p of
@@ -398,7 +407,6 @@ goPattern p = case p of
   PatternPostfixApplication a -> Abstract.PatternConstructorApp <$> goPostfixPatternApplication a
   PatternWildcard i -> return (Abstract.PatternWildcard i)
   PatternEmpty -> return Abstract.PatternEmpty
-  PatternBraces {} -> impossible
 
 goAxiom :: Members '[InfoTableBuilder, Error ScoperError, Builtins] r => AxiomDef 'Scoped -> Sem r Abstract.AxiomDef
 goAxiom a = do