Refactor childs of pattern parentheses and braces (#1398)

src/Juvix/Syntax/Concrete/Language.hs

@@ -85,6 +85,11 @@ type family PatternType s = res | res -> s where
   PatternType 'Parsed = PatternAtom 'Parsed
   PatternType 'Scoped = PatternArg
 
+type PatternParensType :: Stage -> GHC.Type
+type family PatternParensType s = res | res -> s where
+  PatternParensType 'Parsed = PatternAtoms 'Parsed
+  PatternParensType 'Scoped = PatternArg
+
 type family ImportType (s :: Stage) :: GHC.Type where
   ImportType 'Parsed = TopModulePath
   ImportType 'Scoped = Module 'Scoped 'ModuleTop
@@ -294,7 +299,7 @@ data Pattern
   | PatternInfixApplication PatternInfixApp
   | PatternPostfixApplication PatternPostfixApp
   | PatternWildcard Wildcard
-  | PatternEmpty
+  | PatternEmpty Interval
   deriving stock (Show, Eq, Ord)
 
 instance HasAtomicity Pattern where
@@ -305,7 +310,7 @@ instance HasAtomicity Pattern where
     PatternInfixApplication a -> Aggregate (getFixity a)
     PatternPostfixApplication p -> Aggregate (getFixity p)
     PatternWildcard {} -> Atom
-    PatternEmpty -> Atom
+    PatternEmpty {} -> Atom
 
 --------------------------------------------------------------------------------
 -- Pattern section
@@ -319,9 +324,9 @@ data PatternScopedIden
 data PatternAtom (s :: Stage)
   = PatternAtomIden (PatternAtomIdenType s)
   | PatternAtomWildcard Wildcard
-  | PatternAtomEmpty
-  | PatternAtomParens (PatternAtoms s)
-  | PatternAtomBraces (PatternAtoms s)
+  | PatternAtomEmpty Interval
+  | PatternAtomParens (PatternParensType s)
+  | PatternAtomBraces (PatternParensType s)
 
 data PatternAtoms (s :: Stage) = PatternAtoms
   { _patternAtoms :: NonEmpty (PatternAtom s),
@@ -924,6 +929,7 @@ deriving stock instance
   ( Show (ExpressionType s),
     Show (IdentifierType s),
     Show (PatternAtomIdenType s),
+    Show (PatternParensType s),
     Show (PatternType s)
   ) =>
   Show (PatternAtom s)
@@ -932,6 +938,7 @@ deriving stock instance
   ( Eq (ExpressionType s),
     Eq (IdentifierType s),
     Eq (PatternAtomIdenType s),
+    Eq (PatternParensType s),
     Eq (PatternType s)
   ) =>
   Eq (PatternAtom s)
@@ -940,6 +947,7 @@ deriving stock instance
   ( Ord (ExpressionType s),
     Ord (IdentifierType s),
     Ord (PatternAtomIdenType s),
+    Ord (PatternParensType s),
     Ord (PatternType s)
   ) =>
   Ord (PatternAtom s)
@@ -948,17 +956,65 @@ deriving stock instance
   ( Show (ExpressionType s),
     Show (IdentifierType s),
     Show (PatternAtomIdenType s),
+    Show (PatternParensType s),
     Show (PatternType s)
   ) =>
   Show (PatternAtoms s)
 
+instance HasLoc PatternScopedIden where
+  getLoc = \case
+    PatternScopedVar v -> getLoc v
+    PatternScopedConstructor c -> getLoc c
+
+instance SingI s => HasLoc (PatternAtom s) where
+  getLoc = \case
+    PatternAtomIden i -> getLocIden i
+    PatternAtomWildcard w -> getLoc w
+    PatternAtomEmpty i -> i
+    PatternAtomParens p -> getLocParens p
+    PatternAtomBraces p -> getLocParens p
+    where
+      getLocIden :: forall r. SingI r => PatternAtomIdenType r -> Interval
+      getLocIden p = case sing :: SStage r of
+        SParsed -> getLoc p
+        SScoped -> getLoc p
+      getLocParens :: forall r. SingI r => PatternParensType r -> Interval
+      getLocParens p =
+        case sing :: SStage r of
+          SParsed -> getLoc p
+          SScoped -> getLoc p
+
 instance HasLoc (PatternAtoms s) where
   getLoc = (^. patternAtomsLoc)
 
+instance HasLoc PatternArg where
+  getLoc = getLoc . (^. patternArgPattern)
+
+instance HasLoc PatternInfixApp where
+  getLoc (PatternInfixApp l _ r) =
+    getLoc l <> getLoc r
+
+instance HasLoc PatternPostfixApp where
+  getLoc (PatternPostfixApp l _) = getLoc l
+
+instance HasLoc PatternApp where
+  getLoc (PatternApp l r) = getLoc l <> getLoc r
+
+instance HasLoc Pattern where
+  getLoc = \case
+    PatternVariable v -> getLoc v
+    PatternConstructor c -> getLoc c
+    PatternApplication a -> getLoc a
+    PatternWildcard w -> getLoc w
+    PatternEmpty i -> i
+    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 (PatternAtoms s)
@@ -969,6 +1025,7 @@ instance
   ( Ord (ExpressionType s),
     Ord (IdentifierType s),
     Ord (PatternAtomIdenType s),
+    Ord (PatternParensType s),
     Ord (PatternType s)
   ) =>
   Ord (PatternAtoms s)

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

@@ -90,3 +90,6 @@ instance Ord (RefNameType s) => Ord (ConstructorRef' s) where
 
 instance Show (RefNameType s) => Show (ConstructorRef' s) where
   show = show . (^. constructorRefName)
+
+instance HasLoc (ConstructorRef' 'S.Concrete) where
+  getLoc (ConstructorRef' c) = getLoc c

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

@@ -660,15 +660,20 @@ instance PrettyCode PatternArg where
     p <- ppCode (a ^. patternArgPattern)
     return (bracesIf (Implicit == a ^. patternArgIsImplicit) p)
 
+ppPatternParenType :: forall s r. (SingI s, Member (Reader Options) r) => PatternParensType s -> Sem r (Doc Ann)
+ppPatternParenType p = case sing :: SStage s of
+  SParsed -> ppCode p
+  SScoped -> ppCode p
+
 instance SingI s => PrettyCode (PatternAtom s) where
   ppCode a = case a of
     PatternAtomIden n -> case sing :: SStage s of
       SParsed -> ppCode n
       SScoped -> ppCode n
     PatternAtomWildcard {} -> return kwWildcard
-    PatternAtomEmpty -> return $ parens mempty
-    PatternAtomParens p -> parens <$> ppCode p
-    PatternAtomBraces p -> braces <$> ppCode p
+    PatternAtomEmpty {} -> return $ parens mempty
+    PatternAtomParens p -> parens <$> ppPatternParenType p
+    PatternAtomBraces p -> braces <$> ppPatternParenType p
 
 instance SingI s => PrettyCode (PatternAtoms s) where
   ppCode (PatternAtoms ps _) = hsep . toList <$> mapM ppCode ps
@@ -757,7 +762,7 @@ instance PrettyCode Pattern where
       r' <- ppRightExpression appFixity r
       return $ l' <+> r'
     PatternWildcard {} -> return kwWildcard
-    PatternEmpty -> return $ parens mempty
+    PatternEmpty {} -> return $ parens mempty
     PatternConstructor constr -> ppCode constr
     PatternInfixApplication i -> ppPatternInfixApp i
     PatternPostfixApplication i -> ppPatternPostfixApp i

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

@@ -1130,10 +1130,10 @@ checkPatternAtom ::
   Sem r (PatternAtom 'Scoped)
 checkPatternAtom p = case p of
   PatternAtomWildcard i -> return (PatternAtomWildcard i)
-  PatternAtomEmpty -> return PatternAtomEmpty
-  PatternAtomParens e -> PatternAtomParens <$> checkPatternAtoms e
+  PatternAtomEmpty i -> return (PatternAtomEmpty i)
+  PatternAtomParens e -> PatternAtomParens <$> (checkPatternAtoms e >>= parsePatternAtoms)
   PatternAtomIden n -> PatternAtomIden <$> checkPatternName n
-  PatternAtomBraces n -> PatternAtomBraces <$> checkPatternAtoms n
+  PatternAtomBraces n -> PatternAtomBraces <$> (checkPatternAtoms n >>= parsePatternAtoms)
 
 checkName ::
   Members '[Error ScoperError, State Scope, Reader LocalVars, State ScoperState, InfoTableBuilder] r =>
@@ -1423,8 +1423,8 @@ parseTerm =
 type ParsePat = P.Parsec () [PatternAtom 'Scoped]
 
 makePatternTable ::
-  PatternAtom 'Scoped -> [[P.Operator ParsePat PatternArg]]
-makePatternTable atom = [appOp] : operators
+  PatternAtoms 'Scoped -> [[P.Operator ParsePat PatternArg]]
+makePatternTable (PatternAtoms latoms _) = [appOp] : operators
   where
     getConstructorRef :: PatternAtom 'Scoped -> Maybe ConstructorRef
     getConstructorRef s = case s of
@@ -1432,11 +1432,13 @@ makePatternTable atom = [appOp] : operators
         PatternScopedConstructor r -> Just r
         PatternScopedVar {} -> Nothing
       _ -> Nothing
-    operators = mkSymbolTable constructorRefs
-    constructorRefs :: [ConstructorRef]
-    constructorRefs = case atom of
-      PatternAtomParens (PatternAtoms atoms _) -> mapMaybe getConstructorRef (toList atoms)
-      _ -> []
+    operators = mkSymbolTable (mapMaybe constructorRefs (toList latoms))
+    constructorRefs :: PatternAtom 'Scoped -> Maybe ConstructorRef
+    constructorRefs = \case
+      PatternAtomIden i -> case i of
+        PatternScopedConstructor c -> Just c
+        _ -> Nothing
+      _ -> Nothing
     mkSymbolTable :: [ConstructorRef] -> [[P.Operator ParsePat PatternArg]]
     mkSymbolTable = reverse . map (map snd) . groupSortOn' fst . mapMaybe unqualifiedSymbolOp
       where
@@ -1492,15 +1494,14 @@ implicitP = PatternArg Implicit
 
 parsePatternTerm ::
   forall r.
-  Members '[Reader (ParsePat PatternArg), Embed ParsePat] r =>
+  Members '[Embed ParsePat] r =>
   Sem r PatternArg
 parsePatternTerm = do
-  pPat <- ask
   embed @ParsePat $
     parseNoInfixConstructor
       <|> parseVariable
-      <|> parseParens pPat
-      <|> parseBraces pPat
+      <|> parseParens
+      <|> parseBraces
       <|> parseWildcard
       <|> parseEmpty
   where
@@ -1526,12 +1527,12 @@ parsePatternTerm = do
           _ -> Nothing
 
     parseEmpty :: ParsePat PatternArg
-    parseEmpty = explicitP PatternEmpty <$ P.satisfy isEmpty
+    parseEmpty = explicitP . PatternEmpty <$> P.token isEmpty mempty
       where
-        isEmpty :: PatternAtom 'Scoped -> Bool
+        isEmpty :: PatternAtom 'Scoped -> Maybe Interval
         isEmpty s = case s of
-          PatternAtomEmpty -> True
-          _ -> False
+          PatternAtomEmpty i -> Just i
+          _ -> Nothing
 
     parseVariable :: ParsePat PatternArg
     parseVariable = explicitP . PatternVariable <$> P.token var mempty
@@ -1541,31 +1542,20 @@ parsePatternTerm = do
           PatternAtomIden (PatternScopedVar sym) -> Just sym
           _ -> Nothing
 
-    parseBraces :: ParsePat PatternArg -> ParsePat PatternArg
-    parseBraces patternParser = do
-      exprs <- P.token bracesPat mempty
-      case P.parse patternParser "" exprs of
-        Right (PatternArg i p)
-          -- TODO proper error
-          | Implicit <- i -> error "nested braces"
-          | otherwise -> return (implicitP p)
-        Left {} -> mzero
+    parseBraces :: ParsePat PatternArg
+    parseBraces = P.token bracesPat mempty
       where
-        bracesPat :: PatternAtom 'Scoped -> Maybe [PatternAtom 'Scoped]
+        bracesPat :: PatternAtom 'Scoped -> Maybe PatternArg
         bracesPat s = case s of
-          PatternAtomBraces (PatternAtoms ss _) -> Just (toList ss)
+          PatternAtomBraces r -> Just (set patternArgIsImplicit Implicit r)
           _ -> Nothing
 
-    parseParens :: ParsePat PatternArg -> ParsePat PatternArg
-    parseParens patternParser = do
-      exprs <- P.token parenPat mempty
-      case P.parse patternParser "" exprs of
-        Right r -> return r
-        Left {} -> mzero
+    parseParens :: ParsePat PatternArg
+    parseParens = P.token parenPat mempty
       where
-        parenPat :: PatternAtom 'Scoped -> Maybe [PatternAtom 'Scoped]
+        parenPat :: PatternAtom 'Scoped -> Maybe PatternArg
         parenPat s = case s of
-          PatternAtomParens (PatternAtoms ss _) -> Just (toList ss)
+          PatternAtomParens r -> Just r
           _ -> Nothing
 
 mkPatternParser ::
@@ -1587,17 +1577,25 @@ parsePatternAtom ::
   Members '[Error ScoperError, State Scope] r =>
   PatternAtom 'Scoped ->
   Sem r PatternArg
-parsePatternAtom sec = do
+parsePatternAtom = parsePatternAtoms . singletonAtom
+  where
+    singletonAtom :: PatternAtom 'Scoped -> PatternAtoms 'Scoped
+    singletonAtom a = PatternAtoms (NonEmpty.singleton a) (getLoc a)
+
+parsePatternAtoms ::
+  Members '[Error ScoperError, State Scope] r =>
+  PatternAtoms 'Scoped ->
+  Sem r PatternArg
+parsePatternAtoms atoms@(PatternAtoms sec' _) = do
   case res of
-    Left {} -> case sec of
-      PatternAtomParens a -> throw (ErrInfixPattern (InfixErrorP a))
-      _ -> impossible
+    Left {} -> throw (ErrInfixPattern (InfixErrorP atoms))
     Right r -> return r
   where
-    tbl = makePatternTable sec
+    sec = toList sec'
+    tbl = makePatternTable atoms
     parser :: ParsePat PatternArg
     parser = runM (mkPatternParser tbl) <* P.eof
-    res = P.parse parser filePath [sec]
+    res = P.parse parser filePath sec
 
     filePath :: FilePath
     filePath = "tmp"

src/Juvix/Translation/ScopedToAbstract.hs

@@ -406,7 +406,7 @@ goPattern p = case p of
   PatternInfixApplication a -> Abstract.PatternConstructorApp <$> goInfixPatternApplication a
   PatternPostfixApplication a -> Abstract.PatternConstructorApp <$> goPostfixPatternApplication a
   PatternWildcard i -> return (Abstract.PatternWildcard i)
-  PatternEmpty -> return Abstract.PatternEmpty
+  PatternEmpty {} -> return Abstract.PatternEmpty
 
 goAxiom :: Members '[InfoTableBuilder, Error ScoperError, Builtins] r => AxiomDef 'Scoped -> Sem r Abstract.AxiomDef
 goAxiom a = do