Allow syntax operator in the rhs of a record declaration (#2442)

- Closes #2431.

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

@@ -56,10 +56,12 @@ instance (SingI s) => HasNameSignature s (InductiveDef s, ConstructorDef s) wher
     addRhs (c ^. constructorRhs)
     where
       addRecord :: RhsRecord s -> Sem r ()
-      addRecord RhsRecord {..} = mapM_ addField _rhsRecordFields
+      addRecord RhsRecord {..} = mapM_ addField _rhsRecordStatements
         where
-          addField :: RecordField s -> Sem r ()
-          addField RecordField {..} = addSymbol @s Explicit Nothing (symbolParsed _fieldName)
+          addField :: RecordStatement s -> Sem r ()
+          addField = \case
+            RecordStatementField RecordField {..} -> addSymbol @s Explicit Nothing (symbolParsed _fieldName)
+            RecordStatementOperator {} -> return ()
       addRhs :: ConstructorRhs s -> Sem r ()
       addRhs = \case
         ConstructorRhsGadt g -> addExpressionType (g ^. rhsGadtType)
@@ -212,6 +214,8 @@ mkRecordNameSignature :: RhsRecord 'Parsed -> RecordNameSignature
 mkRecordNameSignature rhs =
   RecordNameSignature
     ( HashMap.fromList
-        [ (s, NameItem s idx Nothing) | (Indexed idx field) <- indexFrom 0 (toList (rhs ^. rhsRecordFields)), let s = field ^. fieldName
+        [ (s, (NameItem s idx Nothing))
+          | (Indexed idx field) <- indexFrom 0 (toList (rhs ^.. rhsRecordStatements . each . _RecordStatementField)),
+            let s = field ^. fieldName
         ]
     )

src/Juvix/Compiler/Concrete/Language.hs

@@ -626,7 +626,7 @@ deriving stock instance Ord (RhsAdt 'Scoped)
 
 data RhsRecord (s :: Stage) = RhsRecord
   { _rhsRecordDelim :: Irrelevant (KeywordRef, KeywordRef),
-    _rhsRecordFields :: [RecordField s]
+    _rhsRecordStatements :: [RecordStatement s]
   }
 
 deriving stock instance Show (RhsRecord 'Parsed)
@@ -1635,6 +1635,22 @@ deriving stock instance Ord (NamedApplication 'Parsed)
 
 deriving stock instance Ord (NamedApplication 'Scoped)
 
+data RecordStatement (s :: Stage)
+  = RecordStatementField (RecordField s)
+  | RecordStatementOperator OperatorSyntaxDef
+
+deriving stock instance Show (RecordStatement 'Parsed)
+
+deriving stock instance Show (RecordStatement 'Scoped)
+
+deriving stock instance Eq (RecordStatement 'Parsed)
+
+deriving stock instance Eq (RecordStatement 'Scoped)
+
+deriving stock instance Ord (RecordStatement 'Parsed)
+
+deriving stock instance Ord (RecordStatement 'Scoped)
+
 data RecordCreation (s :: Stage) = RecordCreation
   { _recordCreationConstructor :: IdentifierType s,
     _recordCreationAtKw :: Irrelevant KeywordRef,
@@ -2653,6 +2669,11 @@ _SyntaxAlias f x = case x of
   SyntaxAlias r -> SyntaxAlias <$> f r
   _ -> pure x
 
+_RecordStatementField :: Traversal' (RecordStatement s) (RecordField s)
+_RecordStatementField f x = case x of
+  RecordStatementField p -> RecordStatementField <$> f p
+  _ -> pure x
+
 scopedIdenName :: Lens' ScopedIden S.Name
 scopedIdenName f n = case n ^. scopedIdenAlias of
   Nothing -> scopedIdenFinal f n

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

@@ -290,6 +290,11 @@ instance (SingI s) => PrettyPrint (NamedApplication s) where
   -- ppCode :: Members '[ExactPrint, Reader Options] r => NamedApplication s -> Sem r ()
   ppCode = apeHelper
 
+instance (SingI s) => PrettyPrint (RecordStatement s) where
+  ppCode = \case
+    RecordStatementField f -> ppCode f
+    RecordStatementOperator f -> ppCode f
+
 instance (SingI s) => PrettyPrint (RecordCreation s) where
   ppCode RecordCreation {..} = do
     let fields'
@@ -1134,14 +1139,14 @@ instance (SingI s) => PrettyPrint (RhsRecord s) where
   ppCode RhsRecord {..} = do
     let Irrelevant (l, r) = _rhsRecordDelim
         fields'
-          | [] <- _rhsRecordFields = mempty
-          | [f] <- _rhsRecordFields = ppCode f
+          | [] <- _rhsRecordStatements = mempty
+          | [f] <- _rhsRecordStatements = ppCode f
           | otherwise =
               hardline
                 <> indent
                   ( sequenceWith
                       (semicolon >> line)
-                      (ppCode <$> _rhsRecordFields)
+                      (ppCode <$> _rhsRecordStatements)
                   )
                 <> hardline
     ppCode l <> fields' <> ppCode r

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

@@ -944,27 +944,36 @@ checkInductiveDef InductiveDef {..} = do
 
     checkRecord :: RhsRecord 'Parsed -> Sem r (RhsRecord 'Scoped)
     checkRecord RhsRecord {..} = do
-      fields' <- checkFields _rhsRecordFields
+      fields' <- checkRecordStatements _rhsRecordStatements
       return
         RhsRecord
-          { _rhsRecordFields = fields',
+          { _rhsRecordStatements = fields',
             _rhsRecordDelim
           }
       where
-        checkFields :: [RecordField 'Parsed] -> Sem r [RecordField 'Scoped]
-        checkFields = \case
+        checkRecordStatements :: [RecordStatement 'Parsed] -> Sem r [RecordStatement 'Scoped]
+        checkRecordStatements = \case
           [] -> return []
-          RecordField {..} : fs -> do
-            type' <- checkParseExpressionAtoms _fieldType
-            withLocalScope $ do
-              name' <- bindVariableSymbol _fieldName
-              let f =
-                    RecordField
-                      { _fieldType = type',
-                        _fieldName = name',
-                        ..
-                      }
-              (f :) <$> checkFields fs
+          f : fs -> case f of
+            RecordStatementOperator d ->
+              (RecordStatementOperator d :) <$> checkRecordStatements fs
+            RecordStatementField d -> do
+              d' <- checkField d
+              (RecordStatementField d' :) <$> checkRecordStatements fs
+
+        checkField :: RecordField 'Parsed -> Sem r (RecordField 'Scoped)
+        checkField RecordField {..} = do
+          type' <- checkParseExpressionAtoms _fieldType
+          -- Since we don't allow dependent types in constructor types, each
+          -- field is checked with a local scope
+          withLocalScope $ do
+            name' <- bindVariableSymbol _fieldName
+            return
+              RecordField
+                { _fieldType = type',
+                  _fieldName = name',
+                  ..
+                }
 
     checkAdt :: RhsAdt 'Parsed -> Sem r (RhsAdt 'Scoped)
     checkAdt RhsAdt {..} = do
@@ -1300,9 +1309,27 @@ checkSections sec = do
                       where
                         genFieldProjections :: Sem (Fail ': s') [Statement 'Parsed]
                         genFieldProjections = do
-                          fs <- indexFrom 0 . toList <$> getFields
-                          return (map (StatementProjectionDef . mkProjection) fs)
+                          fs <- toList <$> getFields
+                          return . run . evalState 0 $ mapM goRecordStatement fs
                           where
+                            goRecordStatement :: RecordStatement 'Parsed -> Sem '[State Int] (Statement 'Parsed)
+                            goRecordStatement = \case
+                              RecordStatementOperator f -> StatementSyntax . SyntaxOperator <$> goOperator f
+                              RecordStatementField f -> goField f
+                              where
+                                goOperator :: OperatorSyntaxDef -> Sem '[State Int] OperatorSyntaxDef
+                                goOperator = pure
+
+                                goField :: RecordField 'Parsed -> Sem '[State Int] (Statement 'Parsed)
+                                goField f = do
+                                  idx <- get
+                                  let s = mkProjection (Indexed idx f)
+                                  incFieldIx
+                                  return (StatementProjectionDef s)
+                                  where
+                                    incFieldIx :: Sem '[State Int] ()
+                                    incFieldIx = modify' @Int succ
+
                             mkProjection ::
                               Indexed (RecordField 'Parsed) ->
                               ProjectionDef 'Parsed
@@ -1313,10 +1340,10 @@ checkSections sec = do
                                   _projectionFieldIx = idx
                                 }
 
-                            getFields :: Sem (Fail ': s') [RecordField 'Parsed]
+                            getFields :: Sem (Fail ': s') [RecordStatement 'Parsed]
                             getFields = case i ^. inductiveConstructors of
                               c :| [] -> case c ^. constructorRhs of
-                                ConstructorRhsRecord r -> return (r ^. rhsRecordFields)
+                                ConstructorRhsRecord r -> return (r ^. rhsRecordStatements)
                                 _ -> fail
                               _ -> fail
 
@@ -2165,7 +2192,7 @@ checkDefineField ::
   RecordDefineField 'Parsed ->
   Sem r (RecordDefineField 'Scoped)
 checkDefineField sig RecordDefineField {..} = do
-  def <- localBindings $ ignoreSyntax $ checkFunctionDef _fieldDefineFunDef
+  def <- localBindings . ignoreSyntax $ checkFunctionDef _fieldDefineFunDef
   iden <- checkScopedIden _fieldDefineIden
   let fname = def ^. signName . nameConcrete
   unless (HashMap.member fname (sig ^. recordNames)) $

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

@@ -1271,11 +1271,21 @@ rhsAdt = P.label "<constructor arguments>" $ do
 rhsRecord :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (RhsRecord 'Parsed)
 rhsRecord = P.label "<constructor record>" $ do
   l <- kw delimBraceL
-  _rhsRecordFields <- P.sepEndBy recordField semicolon
+  _rhsRecordStatements <- P.sepEndBy recordStatement semicolon
   r <- kw delimBraceR
   let _rhsRecordDelim = Irrelevant (l, r)
   return RhsRecord {..}
 
+recordStatement :: forall r. (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (RecordStatement 'Parsed)
+recordStatement =
+  RecordStatementOperator <$> operator
+    <|> RecordStatementField <$> recordField
+  where
+    operator :: ParsecS r OperatorSyntaxDef
+    operator = do
+      syn <- kw kwSyntax
+      operatorSyntaxDef syn
+
 pconstructorRhs :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (ConstructorRhs 'Parsed)
 pconstructorRhs =
   ConstructorRhsGadt <$> rhsGadt

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

@@ -650,8 +650,8 @@ goConstructorDef retTy ConstructorDef {..} = do
         _inductiveConstructorPragmas = pragmas'
       }
   where
-    goAdt :: Concrete.RhsAdt 'Scoped -> Sem r Internal.Expression
-    goAdt RhsAdt {..} = do
+    goAdtType :: Concrete.RhsAdt 'Scoped -> Sem r Internal.Expression
+    goAdtType RhsAdt {..} = do
       args <- mapM goArg _rhsAdtArguments
       return (Internal.foldFunType args retTy)
       where
@@ -665,29 +665,32 @@ goConstructorDef retTy ConstructorDef {..} = do
                 _paramType = ty'
               }
 
-    goRecord :: Concrete.RhsRecord 'Scoped -> Sem r Internal.Expression
-    goRecord RhsRecord {..} = do
-      params <- mapM goField _rhsRecordFields
-      return (Internal.foldFunType (toList params) retTy)
+    goRecordType :: Concrete.RhsRecord 'Scoped -> Sem r Internal.Expression
+    goRecordType RhsRecord {..} = do
+      params <- mapMaybeM goRecordStatement _rhsRecordStatements
+      return (Internal.foldFunType params retTy)
       where
-        goField :: Concrete.RecordField 'Scoped -> Sem r Internal.FunctionParameter
-        goField RecordField {..} = do
-          ty' <- goExpression _fieldType
-          return
-            Internal.FunctionParameter
-              { _paramName = Just (goSymbol _fieldName),
-                _paramImplicit = Explicit,
-                _paramType = ty'
-              }
+        goRecordStatement :: Concrete.RecordStatement 'Scoped -> Sem r (Maybe Internal.FunctionParameter)
+        goRecordStatement = \case
+          Concrete.RecordStatementOperator {} -> return Nothing
+          Concrete.RecordStatementField RecordField {..} -> do
+            ty' <- goExpression _fieldType
+            return $
+              Just
+                Internal.FunctionParameter
+                  { _paramName = Just (goSymbol _fieldName),
+                    _paramImplicit = Explicit,
+                    _paramType = ty'
+                  }
 
-    goGadt :: Concrete.RhsGadt 'Scoped -> Sem r Internal.Expression
-    goGadt = goExpression . (^. Concrete.rhsGadtType)
+    goGadtType :: Concrete.RhsGadt 'Scoped -> Sem r Internal.Expression
+    goGadtType = goExpression . (^. Concrete.rhsGadtType)
 
     goRhs :: Concrete.ConstructorRhs 'Scoped -> Sem r Internal.Expression
     goRhs = \case
-      ConstructorRhsGadt r -> goGadt r
-      ConstructorRhsRecord r -> goRecord r
-      ConstructorRhsAdt r -> goAdt r
+      ConstructorRhsGadt r -> goGadtType r
+      ConstructorRhsRecord r -> goRecordType r
+      ConstructorRhsAdt r -> goAdtType r
 
 goLiteral :: LiteralLoc -> Internal.LiteralLoc
 goLiteral = fmap go

tests/positive/Format.juvix

@@ -322,4 +322,23 @@ module Traits;
 
 end;
 
+module OperatorRecord;
+  trait
+  type Natural A :=
+    myNatural {
+      syntax operator + additive;
+      + : A -> A -> A;
+
+      syntax operator * multiplicative;
+      * : A -> A -> A
+    };
+
+  open Natural;
+
+  calc {A : Type} {{Natural A}} (n m : A) : A :=
+    let
+      open Natural;
+    in n + m * m;
+end;
+
 -- Comment at the end of a module