Record updates (#2263)

- Closes #1642.

This pr introduces syntax for convenient record updates.
Example:
```
type Triple (A B C : Type) :=
  | mkTriple {
      fst : A;
      snd : B;
      thd : C;
    };

main : Triple Nat Nat Nat;
main :=
  let
    p : Triple Nat Nat Nat := mkTriple 2 2 2;
    p' :
      Triple Nat Nat Nat :=
        p @triple{
          fst := fst + 1;
          snd := snd * 3
        };
    f : Triple Nat Nat Nat -> Triple Nat Nat Nat := (@triple{fst := fst * 10});
  in f p';
```
We write `@InductiveType{..}` to update the contents of a record. The
`@` is used for parsing. The `InductiveType` symbol indicates the type
of the record update. Inside the braces we have a list of `fieldName :=
newValue` items separated by semicolon. The `fieldName` is bound in
`newValue` with the old value of the field. Thus, we can write something
like `p @triple{fst := fst + 1;}`.

Record updates `X@{..}` are parsed as postfix operators with higher
priority than application, so `f x y @x{q := 1}` is equivalent to `f x
(y @x{q := 1})`.

It is possible the use a record update with no argument by wrapping the
update in parentheses. See `f` in the above example.

runtime/src/juvix/info.h

@@ -10,6 +10,7 @@ typedef struct {
     assoc_t assoc;
 } fixity_t;
 
+#define PREC_MINUS_OMEGA1 (-2)
 #define PREC_MINUS_OMEGA (-1)
 #define PREC_OMEGA 100000
 

src/Juvix/Compiler/Backend/C/Translation/FromReg.hs

@@ -66,6 +66,7 @@ fromReg lims tab =
 
         getPrec :: Precedence -> Expression
         getPrec = \case
+          PrecMinusOmega1 -> macroVar "PREC_MINUS_OMEGA1"
           PrecMinusOmega -> macroVar "PREC_MINUS_OMEGA"
           PrecOmega -> macroVar "PREC_OMEGA"
           PrecNat n -> integer n

src/Juvix/Compiler/Concrete/Data/Name.hs

@@ -97,3 +97,8 @@ moduleNameToTopModulePath = \case
   NameQualified (QualifiedName (SymbolPath p) s) -> TopModulePath (toList p) s
 
 instance Hashable TopModulePath
+
+splitName :: Name -> ([Symbol], Symbol)
+splitName = \case
+  NameQualified (QualifiedName (SymbolPath p) s) -> (toList p, s)
+  NameUnqualified s -> ([], s)

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

@@ -17,5 +17,11 @@ newtype NameSignature = NameSignature
   }
   deriving stock (Show)
 
+newtype RecordNameSignature = RecordNameSignature
+  { _recordNames :: HashMap Symbol (Symbol, Int)
+  }
+  deriving stock (Show)
+
 makeLenses ''NameSignature
+makeLenses ''RecordNameSignature
 makeLenses ''NameBlock

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

@@ -1,12 +1,14 @@
 module Juvix.Compiler.Concrete.Data.NameSignature.Builder
   ( mkNameSignature,
+    mkRecordNameSignature,
     HasNameSignature,
     module Juvix.Compiler.Concrete.Data.NameSignature.Base,
     -- to supress unused warning
     getBuilder,
   )
 where
 
+import Data.HashMap.Strict qualified as HashMap
 import Juvix.Compiler.Concrete.Data.NameSignature.Base
 import Juvix.Compiler.Concrete.Data.NameSignature.Error
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error
@@ -182,3 +184,11 @@ addSymbol' impl sym = do
 
 endBuild' :: Sem (Re r) a
 endBuild' = get @BuilderState >>= throw
+
+mkRecordNameSignature :: RhsRecord 'Parsed -> RecordNameSignature
+mkRecordNameSignature rhs =
+  RecordNameSignature
+    ( HashMap.fromList
+        [ (s, (s, idx)) | (Indexed idx field) <- indexFrom 0 (toList (rhs ^. rhsRecordFields)), let s = field ^. fieldName
+        ]
+    )

src/Juvix/Compiler/Concrete/Data/Scope/Base.hs

@@ -47,12 +47,19 @@ data ScopeParameters = ScopeParameters
     _scopeParsedModules :: HashMap TopModulePath (Module 'Parsed 'ModuleTop)
   }
 
+data RecordInfo = RecordInfo
+  { _recordInfoConstructor :: S.Symbol,
+    _recordInfoSignature :: RecordNameSignature
+  }
+
 data ScoperState = ScoperState
   { _scoperModulesCache :: ModulesCache,
     -- | Local and top modules
     _scoperModules :: HashMap S.ModuleNameId (ModuleRef' 'S.NotConcrete),
     _scoperScope :: HashMap TopModulePath Scope,
-    _scoperSignatures :: HashMap S.NameId NameSignature
+    _scoperSignatures :: HashMap S.NameId NameSignature,
+    -- | Indexed by the inductive type. This is meant to be used for record updates
+    _scoperRecordSignatures :: HashMap S.NameId RecordInfo
   }
 
 data SymbolFixity = SymbolFixity
@@ -84,3 +91,4 @@ makeLenses ''SymbolFixity
 makeLenses ''ScoperState
 makeLenses ''ScopeParameters
 makeLenses ''ModulesCache
+makeLenses ''RecordInfo

src/Juvix/Compiler/Concrete/Extra.hs

@@ -7,11 +7,14 @@ module Juvix.Compiler.Concrete.Extra
     groupStatements,
     flattenStatement,
     migrateFunctionSyntax,
+    recordNameSignatureByIndex,
   )
 where
 
 import Data.HashMap.Strict qualified as HashMap
+import Data.IntMap.Strict qualified as IntMap
 import Data.List.NonEmpty qualified as NonEmpty
+import Juvix.Compiler.Concrete.Data.NameSignature.Base
 import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
 import Juvix.Compiler.Concrete.Keywords
 import Juvix.Compiler.Concrete.Language
@@ -191,3 +194,6 @@ migrateFunctionSyntax m = over moduleBody (mapMaybe goStatement) m
             }
     getClauses :: S.Symbol -> [FunctionClause 'Scoped]
     getClauses name = [c | StatementFunctionClause c <- ss', name == c ^. clauseOwnerFunction]
+
+recordNameSignatureByIndex :: RecordNameSignature -> IntMap Symbol
+recordNameSignatureByIndex = IntMap.fromList . (^.. recordNames . each . to swap)

src/Juvix/Compiler/Concrete/Language.hs

@@ -22,7 +22,7 @@ import Juvix.Compiler.Concrete.Data.Literal
 import Juvix.Compiler.Concrete.Data.ModuleIsTop
 import Juvix.Compiler.Concrete.Data.Name
 import Juvix.Compiler.Concrete.Data.NameRef
-import Juvix.Compiler.Concrete.Data.NameSignature.Base (NameSignature)
+import Juvix.Compiler.Concrete.Data.NameSignature.Base
 import Juvix.Compiler.Concrete.Data.NameSpace
 import Juvix.Compiler.Concrete.Data.PublicAnn
 import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
@@ -46,6 +46,16 @@ type family NameSpaceEntryType s = res | res -> s where
   NameSpaceEntryType 'NameSpaceSymbols = SymbolEntry
   NameSpaceEntryType 'NameSpaceModules = ModuleSymbolEntry
 
+type RecordUpdateExtraType :: Stage -> GHC.Type
+type family RecordUpdateExtraType s = res | res -> s where
+  RecordUpdateExtraType 'Parsed = ()
+  RecordUpdateExtraType 'Scoped = RecordUpdateExtra
+
+type FieldUpdateArgIxType :: Stage -> GHC.Type
+type family FieldUpdateArgIxType s = res | res -> s where
+  FieldUpdateArgIxType 'Parsed = ()
+  FieldUpdateArgIxType 'Scoped = Int
+
 type SymbolType :: Stage -> GHC.Type
 type family SymbolType s = res | res -> s where
   SymbolType 'Parsed = Symbol
@@ -400,6 +410,25 @@ deriving stock instance Ord (ConstructorDef 'Parsed)
 
 deriving stock instance Ord (ConstructorDef 'Scoped)
 
+data RecordUpdateField (s :: Stage) = RecordUpdateField
+  { _fieldUpdateName :: Symbol,
+    _fieldUpdateArgIx :: FieldUpdateArgIxType s,
+    _fieldUpdateAssignKw :: Irrelevant (KeywordRef),
+    _fieldUpdateValue :: ExpressionType s
+  }
+
+deriving stock instance Show (RecordUpdateField 'Parsed)
+
+deriving stock instance Show (RecordUpdateField 'Scoped)
+
+deriving stock instance Eq (RecordUpdateField 'Parsed)
+
+deriving stock instance Eq (RecordUpdateField 'Scoped)
+
+deriving stock instance Ord (RecordUpdateField 'Parsed)
+
+deriving stock instance Ord (RecordUpdateField 'Scoped)
+
 data RecordField (s :: Stage) = RecordField
   { _fieldName :: SymbolType s,
     _fieldColon :: Irrelevant (KeywordRef),
@@ -919,6 +948,8 @@ data Expression
   | ExpressionLiteral LiteralLoc
   | ExpressionFunction (Function 'Scoped)
   | ExpressionHole (HoleType 'Scoped)
+  | ExpressionRecordUpdate RecordUpdateApp
+  | ExpressionParensRecordUpdate ParensRecordUpdate
   | ExpressionBraces (WithLoc Expression)
   | ExpressionIterator (Iterator 'Scoped)
   | ExpressionNamedApplication (NamedApplication 'Scoped)
@@ -1233,6 +1264,45 @@ deriving stock instance Ord (ArgumentBlock 'Parsed)
 
 deriving stock instance Ord (ArgumentBlock 'Scoped)
 
+data RecordUpdateExtra = RecordUpdateExtra
+  { _recordUpdateExtraConstructor :: S.Symbol,
+    -- | Implicitly bound fields sorted by index
+    _recordUpdateExtraVars :: [S.Symbol],
+    _recordUpdateExtraSignature :: RecordNameSignature
+  }
+  deriving stock (Show)
+
+newtype ParensRecordUpdate = ParensRecordUpdate
+  { _parensRecordUpdate :: RecordUpdate 'Scoped
+  }
+  deriving stock (Show, Eq, Ord)
+
+data RecordUpdate (s :: Stage) = RecordUpdate
+  { _recordUpdateAtKw :: Irrelevant KeywordRef,
+    _recordUpdateDelims :: Irrelevant (KeywordRef, KeywordRef),
+    _recordUpdateTypeName :: IdentifierType s,
+    _recordUpdateExtra :: Irrelevant (RecordUpdateExtraType s),
+    _recordUpdateFields :: NonEmpty (RecordUpdateField s)
+  }
+
+deriving stock instance Show (RecordUpdate 'Parsed)
+
+deriving stock instance Show (RecordUpdate 'Scoped)
+
+deriving stock instance Eq (RecordUpdate 'Parsed)
+
+deriving stock instance Eq (RecordUpdate 'Scoped)
+
+deriving stock instance Ord (RecordUpdate 'Parsed)
+
+deriving stock instance Ord (RecordUpdate 'Scoped)
+
+data RecordUpdateApp = RecordUpdateApp
+  { _recordAppUpdate :: RecordUpdate 'Scoped,
+    _recordAppExpression :: Expression
+  }
+  deriving stock (Show, Eq, Ord)
+
 data NamedApplication (s :: Stage) = NamedApplication
   { _namedAppName :: IdentifierType s,
     _namedAppArgs :: NonEmpty (ArgumentBlock s),
@@ -1260,6 +1330,7 @@ data ExpressionAtom (s :: Stage)
   | AtomHole (HoleType s)
   | AtomBraces (WithLoc (ExpressionType s))
   | AtomLet (Let s)
+  | AtomRecordUpdate (RecordUpdate s)
   | AtomUniverse Universe
   | AtomFunction (Function s)
   | AtomFunArrow KeywordRef
@@ -1420,6 +1491,11 @@ newtype ModuleIndex = ModuleIndex
   }
 
 makeLenses ''PatternArg
+makeLenses ''ParensRecordUpdate
+makeLenses ''RecordUpdateExtra
+makeLenses ''RecordUpdate
+makeLenses ''RecordUpdateApp
+makeLenses ''RecordUpdateField
 makeLenses ''NonDefinitionsSection
 makeLenses ''DefinitionsSection
 makeLenses ''ProjectionDef
@@ -1520,6 +1596,8 @@ instance HasAtomicity Expression where
     ExpressionCase c -> atomicity c
     ExpressionIterator i -> atomicity i
     ExpressionNamedApplication i -> atomicity i
+    ExpressionRecordUpdate {} -> Aggregate updateFixity
+    ExpressionParensRecordUpdate {} -> Atom
 
 expressionAtomicity :: forall s. SingI s => ExpressionType s -> Atomicity
 expressionAtomicity e = case sing :: SStage s of
@@ -1632,6 +1710,18 @@ instance HasLoc (List s) where
 instance SingI s => HasLoc (NamedApplication s) where
   getLoc NamedApplication {..} = getLocIdentifierType _namedAppName <> getLoc (last _namedAppArgs)
 
+instance SingI s => HasLoc (RecordUpdateField s) where
+  getLoc f = getLocSymbolType (f ^. fieldUpdateName) <> getLocExpressionType (f ^. fieldUpdateValue)
+
+instance SingI s => HasLoc (RecordUpdate s) where
+  getLoc r = getLoc (r ^. recordUpdateAtKw) <> getLocSpan (r ^. recordUpdateFields)
+
+instance HasLoc RecordUpdateApp where
+  getLoc r = getLoc (r ^. recordAppExpression) <> getLoc (r ^. recordAppUpdate)
+
+instance HasLoc ParensRecordUpdate where
+  getLoc = getLoc . (^. parensRecordUpdate)
+
 instance HasLoc Expression where
   getLoc = \case
     ExpressionIdentifier i -> getLoc i
@@ -1650,6 +1740,8 @@ instance HasLoc Expression where
     ExpressionBraces i -> getLoc i
     ExpressionIterator i -> getLoc i
     ExpressionNamedApplication i -> getLoc i
+    ExpressionRecordUpdate i -> getLoc i
+    ExpressionParensRecordUpdate i -> getLoc i
 
 getLocIdentifierType :: forall s. SingI s => IdentifierType s -> Interval
 getLocIdentifierType e = case sing :: SStage s of
@@ -1955,13 +2047,25 @@ instance IsApe (Function 'Scoped) ApeLeaf where
           _infixOp = ApeLeafFunctionKw kw
         }
 
+instance IsApe RecordUpdateApp ApeLeaf where
+  toApe :: RecordUpdateApp -> Ape ApeLeaf
+  toApe a =
+    ApePostfix
+      Postfix
+        { _postfixFixity = updateFixity,
+          _postfixOp = ApeLeafAtom (sing :&: AtomRecordUpdate (a ^. recordAppUpdate)),
+          _postfixLeft = toApe (a ^. recordAppExpression)
+        }
+
 instance IsApe Expression ApeLeaf where
   toApe e = case e of
     ExpressionApplication a -> toApe a
     ExpressionInfixApplication a -> toApe a
     ExpressionPostfixApplication a -> toApe a
     ExpressionFunction a -> toApe a
     ExpressionNamedApplication a -> toApe a
+    ExpressionRecordUpdate a -> toApe a
+    ExpressionParensRecordUpdate {} -> leaf
     ExpressionParensIdentifier {} -> leaf
     ExpressionIdentifier {} -> leaf
     ExpressionList {} -> leaf
@@ -2045,3 +2149,8 @@ exportNameSpace :: forall ns. SingI ns => Lens' ExportInfo (HashMap Symbol (Name
 exportNameSpace = case sing :: SNameSpace ns of
   SNameSpaceSymbols -> exportSymbols
   SNameSpaceModules -> exportModuleSymbols
+
+_ConstructorRhsRecord :: Traversal' (ConstructorRhs s) (RhsRecord s)
+_ConstructorRhsRecord f rhs = case rhs of
+  ConstructorRhsRecord r -> ConstructorRhsRecord <$> f r
+  _ -> pure rhs

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

@@ -262,6 +262,29 @@ instance SingI s => PrettyPrint (NamedApplication s) where
   -- ppCode :: Members '[ExactPrint, Reader Options] r => NamedApplication s -> Sem r ()
   ppCode = apeHelper
 
+instance SingI s => PrettyPrint (RecordUpdateField s) where
+  ppCode RecordUpdateField {..} =
+    ppSymbolType _fieldUpdateName <+> ppCode _fieldUpdateAssignKw <+> ppExpressionType _fieldUpdateValue
+
+instance SingI s => PrettyPrint (RecordUpdate s) where
+  ppCode RecordUpdate {..} = do
+    let Irrelevant (l, r) = _recordUpdateDelims
+        fields'
+          | null (_recordUpdateFields ^. _tail1) = ppCode (_recordUpdateFields ^. _head1)
+          | otherwise =
+              line
+                <> indent
+                  ( sequenceWith
+                      (semicolon >> line)
+                      (ppCode <$> _recordUpdateFields)
+                  )
+                <> line
+    ppCode _recordUpdateAtKw
+      <> ppIdentifierType _recordUpdateTypeName
+      <> ppCode l
+      <> fields'
+      <> ppCode r
+
 instance SingI s => PrettyPrint (ExpressionAtom s) where
   ppCode = \case
     AtomIdentifier n -> ppIdentifierType n
@@ -270,6 +293,7 @@ instance SingI s => PrettyPrint (ExpressionAtom s) where
     AtomCase c -> ppCode c
     AtomList l -> ppCode l
     AtomUniverse uni -> ppCode uni
+    AtomRecordUpdate u -> ppCode u
     AtomFunction fun -> ppCode fun
     AtomLiteral lit -> ppCode lit
     AtomFunArrow a -> ppCode a
@@ -543,6 +567,7 @@ instance SingI s => PrettyPrint (Lambda s) where
 
 instance PrettyPrint Precedence where
   ppCode = \case
+    PrecMinusOmega1 -> noLoc (pretty ("-ω₁" :: Text))
     PrecMinusOmega -> noLoc (pretty ("-ω" :: Text))
     PrecNat n -> noLoc (pretty n)
     PrecOmega -> noLoc (pretty ("ω" :: Text))
@@ -576,6 +601,12 @@ instance PrettyPrint IteratorSyntaxDef where
       <+> iterSymbol'
       <+?> fmap ppCode _iterAttribs
 
+instance PrettyPrint RecordUpdateApp where
+  ppCode = apeHelper
+
+instance PrettyPrint ParensRecordUpdate where
+  ppCode = parens . ppCode . (^. parensRecordUpdate)
+
 instance PrettyPrint Expression where
   ppCode = \case
     ExpressionIdentifier n -> ppCode n
@@ -594,6 +625,8 @@ instance PrettyPrint Expression where
     ExpressionCase c -> ppCode c
     ExpressionIterator i -> ppCode i
     ExpressionNamedApplication i -> ppCode i
+    ExpressionRecordUpdate i -> ppCode i
+    ExpressionParensRecordUpdate i -> ppCode i
 
 instance PrettyPrint (WithSource Pragmas) where
   ppCode pragma = do