Allow wildcard arguments in new function definition syntax (#2295)

* Closes #2288

src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs

@@ -134,7 +134,9 @@ addConstructorParams :: Members '[NameSignatureBuilder] r => InductiveParameters
 addConstructorParams = addInductiveParams' Implicit
 
 addSigArg :: Members '[NameSignatureBuilder] r => SigArg 'Parsed -> Sem r ()
-addSigArg a = forM_ (a ^. sigArgNames) (addSymbol (a ^. sigArgImplicit))
+addSigArg a = forM_ (a ^. sigArgNames) $ \case
+  ArgumentSymbol s -> addSymbol (a ^. sigArgImplicit) s
+  ArgumentWildcard {} -> return ()
 
 type Re r = State BuilderState ': Error BuilderState ': Error NameSignatureError ': r
 

src/Juvix/Compiler/Concrete/Language.hs

@@ -146,6 +146,22 @@ type ParsedIteratorAttribs = WithLoc (WithSource IteratorAttribs)
 
 type ParsedFixityInfo = WithLoc (WithSource FixityInfo)
 
+data Argument (s :: Stage)
+  = ArgumentSymbol (SymbolType s)
+  | ArgumentWildcard Wildcard
+
+deriving stock instance Show (Argument 'Parsed)
+
+deriving stock instance Show (Argument 'Scoped)
+
+deriving stock instance Eq (Argument 'Parsed)
+
+deriving stock instance Eq (Argument 'Scoped)
+
+deriving stock instance Ord (Argument 'Parsed)
+
+deriving stock instance Ord (Argument 'Scoped)
+
 -- | We group consecutive definitions and reserve symbols in advance, so that we
 -- don't need extra syntax for mutually recursive definitions. Also, it allows
 -- us to be more flexible with the ordering of the definitions.
@@ -317,7 +333,7 @@ data SigArg (s :: Stage) = SigArg
   { _sigArgDelims :: Irrelevant (KeywordRef, KeywordRef),
     _sigArgImplicit :: IsImplicit,
     _sigArgColon :: Irrelevant KeywordRef,
-    _sigArgNames :: NonEmpty (SymbolType s),
+    _sigArgNames :: NonEmpty (Argument s),
     _sigArgType :: ExpressionType s
   }
 

src/Juvix/Compiler/Concrete/Print/Base.hs

@@ -753,11 +753,17 @@ instance SingI s => PrettyPrint (NewFunctionClause s) where
         e' = ppExpressionType _clausenBody
     ppCode _clausenPipeKw <+> pats' <+> ppCode _clausenAssignKw <> oneLineOrNext e'
 
+instance SingI s => PrettyPrint (Argument s) where
+  ppCode :: Members '[ExactPrint, Reader Options] r => Argument s -> Sem r ()
+  ppCode = \case
+    ArgumentSymbol s -> ppSymbolType s
+    ArgumentWildcard w -> ppCode w
+
 instance SingI s => PrettyPrint (SigArg s) where
   ppCode :: Members '[ExactPrint, Reader Options] r => SigArg s -> Sem r ()
   ppCode SigArg {..} = do
     let Irrelevant (l, r) = _sigArgDelims
-        names' = hsep (ppSymbolType <$> _sigArgNames)
+        names' = hsep (fmap ppCode _sigArgNames)
         colon' = ppCode _sigArgColon
         ty' = ppExpressionType _sigArgType
     ppCode l <> names' <+> colon' <+> ty' <> ppCode r

src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs

@@ -741,7 +741,9 @@ checkFunctionDef FunctionDef {..} = do
   where
     checkArg :: SigArg 'Parsed -> Sem r (SigArg 'Scoped)
     checkArg SigArg {..} = do
-      names' <- mapM bindVariableSymbol _sigArgNames
+      names' <- forM _sigArgNames $ \case
+        ArgumentSymbol s -> ArgumentSymbol <$> bindVariableSymbol s
+        ArgumentWildcard w -> return $ ArgumentWildcard w
       ty' <- checkParseExpressionAtoms _sigArgType
       return
         SigArg

src/Juvix/Compiler/Concrete/Translation/FromSource.hs

@@ -957,7 +957,7 @@ newTypeSignature _signBuiltin = P.label "<function definition>" $ do
     parseArg = do
       (openDelim, _sigArgNames, _sigArgImplicit, _sigArgColon) <- P.try $ do
         (opn, impl) <- implicitOpen
-        n <- some1 symbol
+        n <- some1 ((ArgumentSymbol <$> symbol) <|> (ArgumentWildcard <$> wildcard))
         c <- Irrelevant <$> kw kwColon
         return (opn, n, impl, c)
       _sigArgType <- parseExpressionAtoms

src/Juvix/Compiler/Internal/Translation/FromConcrete.hs

@@ -510,20 +510,27 @@ goTopNewFunctionDef FunctionDef {..} = do
         argToParam SigArg {..} = do
           _paramType <- goExpression _sigArgType
           let _paramImplicit = _sigArgImplicit
-              mk :: S.Symbol -> Sem r Internal.FunctionParameter
-              mk s =
-                let _paramName = Just (goSymbol s)
-                 in return Internal.FunctionParameter {..}
+              mk :: Concrete.Argument 'Scoped -> Sem r Internal.FunctionParameter
+              mk = \case
+                Concrete.ArgumentSymbol s ->
+                  let _paramName = Just (goSymbol s)
+                   in return Internal.FunctionParameter {..}
+                Concrete.ArgumentWildcard {} ->
+                  return Internal.FunctionParameter {_paramName = Nothing, ..}
           mapM mk _sigArgNames
 
     argToPattern :: SigArg 'Scoped -> Sem r (NonEmpty Internal.PatternArg)
     argToPattern SigArg {..} = do
       let _patternArgIsImplicit = _sigArgImplicit
           _patternArgName :: Maybe Internal.Name = Nothing
-          mk :: S.Symbol -> Sem r Internal.PatternArg
-          mk s = do
-            let _patternArgPattern = Internal.PatternVariable (goSymbol s)
-            return Internal.PatternArg {..}
+          mk :: Concrete.Argument 'Scoped -> Sem r Internal.PatternArg
+          mk = \case
+            Concrete.ArgumentSymbol s ->
+              let _patternArgPattern = Internal.PatternVariable (goSymbol s)
+               in return Internal.PatternArg {..}
+            Concrete.ArgumentWildcard w -> do
+              _patternArgPattern <- Internal.PatternVariable <$> varFromWildcard w
+              return Internal.PatternArg {..}
       mapM mk _sigArgNames
 
 goTopFunctionDef ::

test/Typecheck/Positive.hs

@@ -264,7 +264,11 @@ tests =
     posTest
       "Record patterns"
       $(mkRelDir ".")
-      $(mkRelFile "RecordPattern.juvix")
+      $(mkRelFile "RecordPattern.juvix"),
+    posTest
+      "Wildcard arguments"
+      $(mkRelDir ".")
+      $(mkRelFile "WildcardArguments.juvix")
   ]
     <> [ compilationTest t | t <- Compilation.tests
        ]

tests/positive/WildcardArguments.juvix

@@ -0,0 +1,3 @@
+module WildcardArguments;
+
+fn {A : Type} (a _ _ : A) : A := a;