Allow record fields to be iterators

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

@@ -63,7 +63,13 @@ instance (SingI s) => HasNameSignature s (InductiveDef s, ConstructorDef s) wher
           addField :: RecordStatement s -> Sem r ()
           addField = \case
             RecordStatementField RecordField {..} -> addSymbol @s Explicit Nothing _fieldName _fieldType
-            RecordStatementOperator {} -> return ()
+            RecordStatementSyntax d -> goSyntax d
+
+          goSyntax :: RecordSyntaxDef s -> Sem r ()
+          goSyntax = \case
+            RecordSyntaxOperator {} -> return ()
+            RecordSyntaxIterator {} -> return ()
+
       addRhs :: ConstructorRhs s -> Sem r ()
       addRhs = \case
         ConstructorRhsGadt g -> addExpressionType (g ^. rhsGadtType)

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

@@ -378,6 +378,10 @@ data ParsedIteratorInfo = ParsedIteratorInfo
   }
   deriving stock (Show, Eq, Ord, Generic)
 
+instance Serialize ParsedIteratorInfo
+
+instance NFData ParsedIteratorInfo
+
 data SyntaxDef (s :: Stage)
   = SyntaxFixity (FixitySyntaxDef s)
   | SyntaxOperator OperatorSyntaxDef
@@ -487,7 +491,11 @@ data IteratorSyntaxDef = IteratorSyntaxDef
     _iterSyntaxKw :: KeywordRef,
     _iterIteratorKw :: KeywordRef
   }
-  deriving stock (Show, Eq, Ord)
+  deriving stock (Show, Eq, Ord, Generic)
+
+instance Serialize IteratorSyntaxDef
+
+instance NFData IteratorSyntaxDef
 
 instance HasLoc IteratorSyntaxDef where
   getLoc IteratorSyntaxDef {..} = getLoc _iterSyntaxKw <> getLoc _iterSymbol
@@ -2397,9 +2405,30 @@ deriving stock instance Ord (NamedApplicationNew 'Parsed)
 
 deriving stock instance Ord (NamedApplicationNew 'Scoped)
 
+data RecordSyntaxDef (s :: Stage)
+  = RecordSyntaxOperator OperatorSyntaxDef
+  | RecordSyntaxIterator IteratorSyntaxDef
+  deriving stock (Generic)
+
+instance Serialize (RecordSyntaxDef 'Scoped)
+
+instance NFData (RecordSyntaxDef 'Scoped)
+
+deriving stock instance Show (RecordSyntaxDef 'Parsed)
+
+deriving stock instance Show (RecordSyntaxDef 'Scoped)
+
+deriving stock instance Eq (RecordSyntaxDef 'Parsed)
+
+deriving stock instance Eq (RecordSyntaxDef 'Scoped)
+
+deriving stock instance Ord (RecordSyntaxDef 'Parsed)
+
+deriving stock instance Ord (RecordSyntaxDef 'Scoped)
+
 data RecordStatement (s :: Stage)
   = RecordStatementField (RecordField s)
-  | RecordStatementOperator OperatorSyntaxDef
+  | RecordStatementSyntax (RecordSyntaxDef s)
   deriving stock (Generic)
 
 instance Serialize (RecordStatement 'Scoped)

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

@@ -342,10 +342,15 @@ instance (SingI s) => PrettyPrint (NamedArgumentNew s) where
     NamedArgumentNewFunction f -> ppCode f
     NamedArgumentItemPun f -> ppCode f
 
+instance PrettyPrint (RecordSyntaxDef s) where
+  ppCode = \case
+    RecordSyntaxOperator d -> ppCode d
+    RecordSyntaxIterator d -> ppCode d
+
 instance (SingI s) => PrettyPrint (RecordStatement s) where
   ppCode = \case
     RecordStatementField f -> ppCode f
-    RecordStatementOperator f -> ppCode f
+    RecordStatementSyntax f -> ppCode f
 
 instance (SingI s) => PrettyPrint (RecordUpdateField s) where
   ppCode RecordUpdateField {..} =

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

@@ -1203,14 +1203,17 @@ checkInductiveDef InductiveDef {..} = do
           return rhs'
           where
             checkRecordStatements :: [RecordStatement 'Parsed] -> Sem r [RecordStatement 'Scoped]
-            checkRecordStatements = \case
-              [] -> return []
-              f : fs -> case f of
-                RecordStatementOperator d ->
-                  (RecordStatementOperator d :) <$> checkRecordStatements fs
-                RecordStatementField d -> do
-                  d' <- checkField d
-                  (RecordStatementField d' :) <$> checkRecordStatements fs
+            checkRecordStatements = mapM checkRecordStatement
+
+            checkRecordSyntaxDef :: RecordSyntaxDef 'Parsed -> Sem r (RecordSyntaxDef 'Scoped)
+            checkRecordSyntaxDef = \case
+              RecordSyntaxOperator d -> return (RecordSyntaxOperator d)
+              RecordSyntaxIterator d -> return (RecordSyntaxIterator d)
+
+            checkRecordStatement :: RecordStatement 'Parsed -> Sem r (RecordStatement 'Scoped)
+            checkRecordStatement = \case
+              RecordStatementField d -> RecordStatementField <$> checkField d
+              RecordStatementSyntax s -> RecordStatementSyntax <$> checkRecordSyntaxDef s
 
             checkField :: RecordField 'Parsed -> Sem r (RecordField 'Scoped)
             checkField RecordField {..} = do
@@ -1611,11 +1614,13 @@ checkSections sec = topBindings helper
                           where
                             goRecordStatement :: RecordStatement 'Parsed -> Sem '[State Int] (Statement 'Parsed)
                             goRecordStatement = \case
-                              RecordStatementOperator f -> StatementSyntax . SyntaxOperator <$> goOperator f
+                              RecordStatementSyntax f -> StatementSyntax <$> goSyntax f
                               RecordStatementField f -> goField f
                               where
-                                goOperator :: OperatorSyntaxDef -> Sem '[State Int] OperatorSyntaxDef
-                                goOperator = pure
+                                goSyntax :: RecordSyntaxDef 'Parsed -> Sem s (SyntaxDef 'Parsed)
+                                goSyntax = \case
+                                  RecordSyntaxOperator d -> return (SyntaxOperator d)
+                                  RecordSyntaxIterator d -> return (SyntaxIterator d)
 
                                 goField :: RecordField 'Parsed -> Sem '[State Int] (Statement 'Parsed)
                                 goField f = do

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

@@ -1549,13 +1549,14 @@ rhsRecord = P.label "<constructor record>" $ do
 
 recordStatement :: forall r. (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (RecordStatement 'Parsed)
 recordStatement =
-  RecordStatementOperator <$> operator
+  RecordStatementSyntax <$> syntax
     <|> RecordStatementField <$> recordField
   where
-    operator :: ParsecS r OperatorSyntaxDef
-    operator = do
+    syntax :: ParsecS r (RecordSyntaxDef 'Parsed)
+    syntax = do
       syn <- kw kwSyntax
-      operatorSyntaxDef syn
+      RecordSyntaxIterator <$> iteratorSyntaxDef syn
+        <|> RecordSyntaxOperator <$> operatorSyntaxDef syn
 
 pconstructorRhs :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (ConstructorRhs 'Parsed)
 pconstructorRhs =

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

@@ -653,7 +653,7 @@ goConstructorDef retTy ConstructorDef {..} = do
       where
         goRecordStatement :: Concrete.RecordStatement 'Scoped -> Sem r (Maybe Internal.FunctionParameter)
         goRecordStatement = \case
-          Concrete.RecordStatementOperator {} -> return Nothing
+          Concrete.RecordStatementSyntax {} -> return Nothing
           Concrete.RecordStatementField RecordField {..} -> do
             ty' <- goExpression _fieldType
             return $

test/Scope/Positive.hs

@@ -249,5 +249,9 @@ tests =
     posTest
       "Named argument puns"
       $(mkRelDir ".")
-      $(mkRelFile "Puns.juvix")
+      $(mkRelFile "Puns.juvix"),
+    posTest
+      "Record field iterator"
+      $(mkRelDir ".")
+      $(mkRelFile "RecordIterator.juvix")
   ]

tests/positive/RecordIterator.juvix

@@ -0,0 +1,22 @@
+module RecordIterator;
+
+trait
+type Foldable (container elem : Type) :=
+  mkFoldable {
+    syntax iterator for {init := 1; range := 1};
+    for : {B : Type} -> (B -> elem -> B) -> B -> container -> B;
+
+    syntax iterator rfor {init := 1; range := 1};
+    rfor : {B : Type} -> (B -> elem -> B) -> B → container → B
+  };
+
+open Foldable;
+
+foldl
+  {container elem}
+  {{Foldable container elem}}
+  {B : Type}
+  (g : B -> elem -> B)
+  (ini : B)
+  (ls : container)
+  : B := for (acc := ini) (x in ls) {g acc x};