Named arguments for record projections

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

@@ -98,6 +98,15 @@ instance (SingI s) => HasNameSignature s (InductiveDef s) where
     mapM_ addInductiveParams (a ^. inductiveParameters)
     whenJust (a ^. inductiveType) addExpressionType
 
+instance (SingI s) => HasNameSignature s (ProjectionDef s) where
+  addArgs ::
+    forall r.
+    (Members '[NameSignatureBuilder s] r) =>
+    ProjectionDef s ->
+    Sem r ()
+  addArgs p = do
+    addExpressionType (p ^. projectionType)
+
 mkNameSignature ::
   forall s d r.
   (SingI s, Members '[Error ScoperError] r, HasNameSignature s d) =>

src/Juvix/Compiler/Concrete/Gen.hs

@@ -4,6 +4,7 @@ module Juvix.Compiler.Concrete.Gen
   )
 where
 
+import Data.List.NonEmpty qualified as NonEmpty
 import Juvix.Compiler.Concrete.Keywords
 import Juvix.Compiler.Concrete.Language.Base
 import Juvix.Prelude
@@ -135,3 +136,97 @@ functionDefExpression ::
   NonEmpty (ExpressionAtom 'Parsed) ->
   Sem r (FunctionDefBody 'Parsed)
 functionDefExpression exp = SigBodyExpression <$> expressionAtoms' exp
+
+mkProjectionType :: InductiveDef 'Parsed -> ExpressionType 'Parsed -> ExpressionType 'Parsed
+mkProjectionType i indTy =
+  foldr mkFun target indParams
+  where
+    indParams = map mkFunctionParameters $ i ^. inductiveParameters
+    target = mkFun (mkRecordParameter (i ^. inductiveTypeApplied)) indTy
+
+    mkFun :: FunctionParameters 'Parsed -> ExpressionType 'Parsed -> ExpressionType 'Parsed
+    mkFun params tgt =
+      mkExpressionAtoms
+        . NonEmpty.singleton
+        . AtomFunction
+        $ Function
+          { _funParameters = params,
+            _funReturn = tgt,
+            _funKw = funkw
+          }
+      where
+        funkw =
+          KeywordRef
+            { _keywordRefKeyword = kwRightArrow,
+              _keywordRefInterval = getLoc (i ^. inductiveName),
+              _keywordRefUnicode = Ascii
+            }
+
+    mkFunctionParameters :: InductiveParameters 'Parsed -> FunctionParameters 'Parsed
+    mkFunctionParameters InductiveParameters {..} =
+      FunctionParameters
+        { _paramNames = map FunctionParameterName $ toList _inductiveParametersNames,
+          _paramImplicit = Implicit,
+          _paramDelims = Irrelevant (Just (leftBrace, rightBrace)),
+          _paramColon = Irrelevant Nothing,
+          _paramType = maybe univ (^. inductiveParametersType) _inductiveParametersRhs
+        }
+      where
+        univ :: ExpressionAtoms 'Parsed
+        univ =
+          ExpressionAtoms
+            { _expressionAtoms =
+                NonEmpty.singleton $
+                  AtomUniverse $
+                    mkUniverse (Just smallLevel) (getLoc (i ^. inductiveName)),
+              _expressionAtomsLoc = Irrelevant $ getLoc (i ^. inductiveName)
+            }
+
+        leftBrace :: KeywordRef
+        leftBrace =
+          KeywordRef
+            { _keywordRefKeyword = delimBraceL,
+              _keywordRefInterval = getLoc (i ^. inductiveName),
+              _keywordRefUnicode = Ascii
+            }
+
+        rightBrace :: KeywordRef
+        rightBrace =
+          KeywordRef
+            { _keywordRefKeyword = delimBraceR,
+              _keywordRefInterval = getLoc (i ^. inductiveName),
+              _keywordRefUnicode = Ascii
+            }
+
+    mkRecordParameter :: ExpressionType 'Parsed -> FunctionParameters 'Parsed
+    mkRecordParameter ty =
+      FunctionParameters
+        { _paramNames = [FunctionParameterName wildcard],
+          _paramImplicit = implicity,
+          _paramDelims = Irrelevant (Just (leftDoubleBrace, rightDoubleBrace)),
+          _paramColon = Irrelevant Nothing,
+          _paramType = ty
+        }
+      where
+        wildcard = WithLoc (getLoc (i ^. inductiveName)) "_self"
+
+        implicity :: IsImplicit
+        implicity
+          | isJust (i ^. inductiveTrait) = ImplicitInstance
+          | otherwise = Explicit
+
+        leftDoubleBrace :: KeywordRef
+        leftDoubleBrace =
+          KeywordRef
+            { _keywordRefKeyword = delimDoubleBraceL,
+              _keywordRefInterval = getLoc (i ^. inductiveName),
+              _keywordRefUnicode = Ascii
+            }
+
+        rightDoubleBrace :: KeywordRef
+        rightDoubleBrace =
+          KeywordRef
+            { _keywordRefKeyword = delimDoubleBraceR,
+              _keywordRefInterval = getLoc (i ^. inductiveName),
+              _keywordRefUnicode = Ascii
+            }

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

@@ -309,6 +309,7 @@ deriving stock instance Ord (Statement 'Scoped)
 data ProjectionDef s = ProjectionDef
   { _projectionConstructor :: S.Symbol,
     _projectionField :: SymbolType s,
+    _projectionType :: ExpressionType s,
     _projectionKind :: ProjectionKind,
     _projectionFieldIx :: Int,
     _projectionFieldBuiltin :: Maybe (WithLoc BuiltinFunction),
@@ -931,6 +932,7 @@ data InductiveDef (s :: Stage) = InductiveDef
     _inductiveName :: InductiveName s,
     _inductiveParameters :: [InductiveParameters s],
     _inductiveType :: Maybe (ExpressionType s),
+    _inductiveTypeApplied :: ExpressionType s,
     _inductiveConstructors :: NonEmpty (ConstructorDef s),
     _inductivePositive :: Maybe KeywordRef,
     _inductiveTrait :: Maybe KeywordRef

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

@@ -155,25 +155,6 @@ scopeCheckOpenModule = mapError (JuvixError @ScoperError) . checkOpenModule
 freshVariable :: (Members '[NameIdGen, State ScoperSyntax, State Scope, State ScoperState] r) => Symbol -> Sem r S.Symbol
 freshVariable = freshSymbol KNameLocal KNameLocal
 
-checkProjectionDef ::
-  forall r.
-  (Members '[Error ScoperError, InfoTableBuilder, Reader PackageId, Reader ScopeParameters, Reader InfoTable, Reader BindingStrategy, State Scope, State ScoperState, NameIdGen, State ScoperSyntax] r) =>
-  ProjectionDef 'Parsed ->
-  Sem r (ProjectionDef 'Scoped)
-checkProjectionDef p = do
-  _projectionField <- getReservedDefinitionSymbol (p ^. projectionField)
-  _projectionDoc <- maybe (return Nothing) (checkJudoc >=> return . Just) (p ^. projectionDoc)
-  return
-    ProjectionDef
-      { _projectionFieldIx = p ^. projectionFieldIx,
-        _projectionConstructor = p ^. projectionConstructor,
-        _projectionFieldBuiltin = p ^. projectionFieldBuiltin,
-        _projectionPragmas = p ^. projectionPragmas,
-        _projectionKind = p ^. projectionKind,
-        _projectionField,
-        _projectionDoc
-      }
-
 freshSymbol ::
   forall r.
   (Members '[State Scope, State ScoperState, NameIdGen, State ScoperSyntax] r) =>
@@ -261,6 +242,13 @@ registerConstructorSignature uid sig = do
   modify' (set (scoperScopedConstructorFields . at uid) (Just sig))
   registerConstructorSig uid sig
 
+registerProjectionSignature ::
+  (Members '[State ScoperState, Error ScoperError, InfoTableBuilder] r) =>
+  ProjectionDef 'Scoped ->
+  Sem r ()
+registerProjectionSignature p =
+  registerNameSignature (p ^. projectionField . S.nameId) p
+
 reserveSymbolOfNameSpace ::
   forall (ns :: NameSpace) r.
   ( Members
@@ -403,11 +391,7 @@ reserveProjectionSymbol ::
   ProjectionDef 'Parsed ->
   Sem r S.Symbol
 reserveProjectionSymbol d =
-  reserveSymbolOf
-    SKNameFunction
-    Nothing
-    (toBuiltinPrim <$> d ^. projectionFieldBuiltin)
-    (d ^. projectionField)
+  reserveSymbolSignatureOf SKNameFunction d (toBuiltinPrim <$> d ^. projectionFieldBuiltin) (d ^. projectionField)
 
 reserveConstructorSymbol ::
   (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable] r) =>
@@ -1180,24 +1164,26 @@ checkInductiveDef InductiveDef {..} = do
     i <- bindInductiveSymbol _inductiveName
     cs <- mapM (bindConstructorSymbol . (^. constructorName)) _inductiveConstructors
     return (i, cs)
-  (inductiveParameters', inductiveType', inductiveDoc', inductiveConstructors') <- withLocalScope $ do
+  (inductiveParameters', inductiveType', inductiveTypeApplied', inductiveDoc', inductiveConstructors') <- withLocalScope $ do
     inductiveParameters' <- mapM checkInductiveParameters _inductiveParameters
     inductiveType' <- mapM checkParseExpressionAtoms _inductiveType
+    inductiveTypeApplied' <- checkParseExpressionAtoms _inductiveTypeApplied
     inductiveDoc' <- mapM checkJudoc _inductiveDoc
     inductiveConstructors' <-
       nonEmpty'
         <$> sequence
           [ checkConstructorDef inductiveName' cname cdef
             | (cname, cdef) <- zipExact (toList constructorNames') (toList _inductiveConstructors)
           ]
-    return (inductiveParameters', inductiveType', inductiveDoc', inductiveConstructors')
+    return (inductiveParameters', inductiveType', inductiveTypeApplied', inductiveDoc', inductiveConstructors')
   let indDef =
         InductiveDef
           { _inductiveName = inductiveName',
             _inductiveDoc = inductiveDoc',
             _inductivePragmas = _inductivePragmas,
             _inductiveParameters = inductiveParameters',
             _inductiveType = inductiveType',
+            _inductiveTypeApplied = inductiveTypeApplied',
             _inductiveConstructors = inductiveConstructors',
             _inductiveBuiltin,
             _inductivePositive,
@@ -1288,6 +1274,29 @@ checkInductiveDef InductiveDef {..} = do
                 _rhsGadtColon
               }
 
+checkProjectionDef ::
+  forall r.
+  (Members '[HighlightBuilder, Error ScoperError, InfoTableBuilder, Reader PackageId, Reader ScopeParameters, Reader InfoTable, Reader BindingStrategy, State Scope, State ScoperState, NameIdGen, State ScoperSyntax] r) =>
+  ProjectionDef 'Parsed ->
+  Sem r (ProjectionDef 'Scoped)
+checkProjectionDef p = do
+  _projectionField <- getReservedDefinitionSymbol (p ^. projectionField)
+  _projectionType <- checkParseExpressionAtoms (p ^. projectionType)
+  _projectionDoc <- maybe (return Nothing) (checkJudoc >=> return . Just) (p ^. projectionDoc)
+  let p' =
+        ProjectionDef
+          { _projectionFieldIx = p ^. projectionFieldIx,
+            _projectionConstructor = p ^. projectionConstructor,
+            _projectionFieldBuiltin = p ^. projectionFieldBuiltin,
+            _projectionPragmas = p ^. projectionPragmas,
+            _projectionKind = p ^. projectionKind,
+            _projectionField,
+            _projectionType,
+            _projectionDoc
+          }
+  registerProjectionSignature p'
+  return p'
+
 topBindings :: Sem (Reader BindingStrategy ': r) a -> Sem r a
 topBindings = runReader BindingTop
 
@@ -1491,7 +1500,7 @@ checkSections sec = topBindings helper
         goDefinitions :: DefinitionsSection 'Parsed -> Sem r' (DefinitionsSection 'Scoped)
         goDefinitions DefinitionsSection {..} = goDefs [] [] (toList _definitionsSection)
           where
-            -- This functions go through a section reserving definitions and
+            -- This function goes through a section reserving definitions and
             -- collecting inductive modules. It breaks a section when the
             -- collected inductive modules are non-empty (there were some
             -- inductive definitions) and the next definition is a function
@@ -1700,6 +1709,7 @@ checkSections sec = topBindings helper
                               ProjectionDef
                                 { _projectionConstructor = headConstr,
                                   _projectionField = field ^. fieldName,
+                                  _projectionType = G.mkProjectionType i (field ^. fieldType),
                                   _projectionFieldIx = idx,
                                   _projectionKind = kind,
                                   _projectionFieldBuiltin = field ^. fieldBuiltin,

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

@@ -20,6 +20,7 @@ import Juvix.Compiler.Backend.Markdown.Error
 import Juvix.Compiler.Concrete (HighlightBuilder, ignoreHighlightBuilder)
 import Juvix.Compiler.Concrete.Extra (takeWhile1P)
 import Juvix.Compiler.Concrete.Extra qualified as P
+import Juvix.Compiler.Concrete.Gen (mkExpressionAtoms)
 import Juvix.Compiler.Concrete.Language
 import Juvix.Compiler.Concrete.Translation.FromSource.Data.Context
 import Juvix.Compiler.Concrete.Translation.FromSource.Lexer hiding
@@ -1539,6 +1540,10 @@ inductiveDef _inductiveBuiltin = do
     optional (kw kwColon >> parseExpressionAtoms)
       P.<?> "<type annotation e.g. ': Type'>"
   _inductiveAssignKw <- Irrelevant <$> kw kwAssign P.<?> "<assignment symbol ':='>"
+  let name' = NameUnqualified _inductiveName
+      params = fmap (AtomIdentifier . NameUnqualified) (concatMap (toList . (^. inductiveParametersNames)) _inductiveParameters)
+      iden = mkExpressionAtoms (AtomIdentifier name' :| [])
+      _inductiveTypeApplied = mkExpressionAtoms (AtomParens iden :| params)
   _inductiveConstructors <-
     pipeSep1 (constructorDef _inductiveName)
       P.<?> "<constructor definition>"

src/Juvix/Compiler/Internal/Extra.hs

@@ -113,36 +113,33 @@ genFieldProjection ::
   (Members '[NameIdGen] r) =>
   ProjectionKind ->
   FunctionName ->
+  Expression ->
   Maybe BuiltinFunction ->
+  [ArgInfo] ->
   Maybe Pragmas ->
   ConstructorInfo ->
   Int ->
   Sem r FunctionDef
-genFieldProjection kind _funDefName _funDefBuiltin mpragmas info fieldIx = do
+genFieldProjection kind _funDefName _funDefType _funDefBuiltin _funDefArgsInfo mpragmas info fieldIx = do
   body' <- genBody
-  let (inductiveParams, constrArgs) = constructorArgTypes info
-      saturatedTy :: FunctionParameter = unnamedParameter' constructorImplicity (constructorReturnType info)
-      inductiveArgs = map inductiveToFunctionParam inductiveParams
-      param = constrArgs !! fieldIx
-      retTy = param ^. paramType
   cloneFunctionDefSameName
     FunctionDef
       { _funDefTerminating = False,
         _funDefIsInstanceCoercion =
           if
               | kind == ProjectionCoercion -> Just IsInstanceCoercionCoercion
               | otherwise -> Nothing,
-        _funDefArgsInfo = mempty,
         _funDefPragmas =
           maybe
             (mempty {_pragmasInline = Just InlineAlways})
             (over pragmasInline (maybe (Just InlineAlways) Just))
             mpragmas,
         _funDefBody = body',
-        _funDefType = foldFunType (inductiveArgs ++ [saturatedTy]) retTy,
         _funDefDocComment = Nothing,
+        _funDefType,
         _funDefName,
-        _funDefBuiltin
+        _funDefBuiltin,
+        _funDefArgsInfo
       }
   where
     constructorImplicity :: IsImplicit

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

@@ -346,25 +346,46 @@ goAxiomInductive = \case
 
 goProjectionDef ::
   forall r.
-  (Members '[NameIdGen, Error ScoperError, State ConstructorInfos, Reader S.InfoTable] r) =>
+  (Members '[Reader DefaultArgsStack, Reader Pragmas, NameIdGen, Error ScoperError, State ConstructorInfos, Reader S.InfoTable] r) =>
   ProjectionDef 'Scoped ->
   Sem r Internal.FunctionDef
 goProjectionDef ProjectionDef {..} = do
   let c = goSymbol _projectionConstructor
   info <- gets (^?! constructorInfos . at c . _Just)
+  let field = goSymbol _projectionField
+  msig <- asks (^. S.infoNameSigs . at (field ^. Internal.nameId))
+  argInfos <- maybe (return mempty) (fmap toList . goNameSignature) msig
+  projType <- goExpression _projectionType
   fun <-
     Internal.genFieldProjection
       _projectionKind
-      (goSymbol _projectionField)
+      field
+      projType
       ( (^. withLocParam)
           <$> _projectionFieldBuiltin
       )
+      argInfos
       (fmap (^. withLocParam . withSourceValue) _projectionPragmas)
       info
       _projectionFieldIx
   whenJust (fun ^. Internal.funDefBuiltin) (checkBuiltinFunction fun)
   return fun
 
+goNameSignature :: forall r. (Members '[Reader DefaultArgsStack, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) => NameSignature 'Scoped -> Sem r [Internal.ArgInfo]
+goNameSignature = mconcatMapM (fmap toList . goBlock) . (^. nameSignatureArgs)
+  where
+    goBlock :: NameBlock 'Scoped -> Sem r (NonEmpty Internal.ArgInfo)
+    goBlock blk = mapM goItem (blk ^. nameBlockItems)
+      where
+        goItem :: NameItem 'Scoped -> Sem r Internal.ArgInfo
+        goItem i = do
+          _argInfoDefault' <- mapM goExpression (i ^? nameItemDefault . _Just . argDefaultValue)
+          return
+            Internal.ArgInfo
+              { _argInfoDefault = _argInfoDefault',
+                _argInfoName = goSymbol <$> (i ^. nameItemSymbol)
+              }
+
 goFunctionDef ::
   forall r.
   (Members '[Reader DefaultArgsStack, Reader Pragmas, Error ScoperError, NameIdGen, Reader S.InfoTable] r) =>
@@ -389,21 +410,6 @@ goFunctionDef FunctionDef {..} = do
   whenJust _signBuiltin (checkBuiltinFunction fun . (^. withLocParam))
   return fun
   where
-    goNameSignature :: NameSignature 'Scoped -> Sem r [Internal.ArgInfo]
-    goNameSignature = mconcatMapM (fmap toList . goBlock) . (^. nameSignatureArgs)
-      where
-        goBlock :: NameBlock 'Scoped -> Sem r (NonEmpty Internal.ArgInfo)
-        goBlock blk = mapM goItem (blk ^. nameBlockItems)
-          where
-            goItem :: NameItem 'Scoped -> Sem r Internal.ArgInfo
-            goItem i = do
-              _argInfoDefault' <- mapM goExpression (i ^? nameItemDefault . _Just . argDefaultValue)
-              return
-                Internal.ArgInfo
-                  { _argInfoDefault = _argInfoDefault',
-                    _argInfoName = goSymbol <$> (i ^. nameItemSymbol)
-                  }
-
     goBody :: Sem r Internal.Expression
     goBody = do
       commonPatterns <- concatMapM (fmap toList . argToPattern) _signArgs