juvix/NoNamedArguments.juvix at 5194e7c2cd9f2274d1ac2b3c85bf706b7364f2f5 - juvix - gitea: Gitea Service

anoma/juvix

mirror of https://github.com/anoma/juvix.git synced 2024-12-01 00:04:58 +03:00

Jan Mas Rovira f7382caeac

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.

2023-08-07 12:35:36 +02:00

6 lines

68 B

Plaintext

Raw Blame History

 module NoNamedArguments;
 axiom T : Type;
 axiom B : T (x := Type);