Record updates

[janmasrovira]

• Closes Add syntax support for record updates #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.

[lukaszcz]

I think the renaming would be a good idea. Do we use these precedences for anything other than application, update and arrow?

[janmasrovira]

Do we use these precedences for anything other than application, update and arrow?

I think that is an exhaustive list, so no.

• Maybe you can apply this change in User-friendly operator declaration syntax #2270.

[lukaszcz]

Yes, makes sense, I can do the renaming there. Though not to disrupt the code too much I'm not getting rid of the old Fixity/Precedence framework, but translating the precedence graph to a linear precedence ordering at scoping.

[lukaszcz]

It seems on the right-hand side only the field being modified is available as an identifier denoting the old field. This is confusing, and leads to internal errors in some cases.

Type-checking

module records;

import Stdlib.Prelude open;

type Pair (A B : Type) := mkPair {pfst : A; psnd : B};

main : Pair Nat Nat;
main :=
     let p : Pair Nat Nat := mkPair 2 2
     in
     p @Pair{
       pfst := pfst + psnd
     }

results in:

/Users/heliax/Documents/progs/juvix/records.juvix:12:23-27: error:
Symbol not in scope: psnd
Perhaps you meant: snd
                   and

Type-checking:

module records;

import Stdlib.Prelude open;

type Pair (A B : Type) := mkPair {pfst : A; psnd : B};

main : Pair Nat Nat;
main :=
     let p : Pair Nat Nat := mkPair 2 2
     in
     p @Pair{
       pfst := pfst + 3;
       psnd := pfst;
     }

results in:

juvix: internal error: could not find var pfst@658
CallStack (from HasCallStack):
  error, called at src/Juvix/Prelude/Base.hs:375:9 in juvix-0.4.2-83yOy15uIzk3Wi2drQRaG6:Juvix.Prelude.Base
  error, called at src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs:299:11 in juvix-0.4.2-83yOy15uIzk3Wi2drQRaG6:Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Checker

Type-checking:

module records;

import Stdlib.Prelude open;

type Pair (A B : Type) := mkPair {fst : A; snd : B};

main : Pair Nat Nat;
main :=
     let p : Pair Nat Nat := mkPair 2 2
     in
     p @Pair{
       fst := fst + snd;
     }

results in:

/Users/heliax/Documents/progs/juvix/records.juvix:12:21-24: error:
The expression snd {_} {_} has type:
  × _ _ → _
but is expected to have type:
  Nat

[janmasrovira]

This should be fixed now