juvix/tests/Rust/Compilation/positive/test060.juvix

-- record updates and record patterns
module test060;

import Stdlib.Prelude open hiding {fst};

type Triple (A B C : Type) :=
  mkTriple {
    fst : A;
    snd : B;
    thd : C
  };

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

sum : Triple Nat Nat Nat → Nat
  | mkTriple@{fst; snd; thd} := fst + snd + thd;

mf : Pair' (Pair' Bool (List Nat)) (List Nat) → Bool
  | mkPair@{fst := mkPair@{fst; snd := nil};
           snd := zero :: _} := fst
  | x := case x of {_ := false};

main : Nat :=
  let
    p : Triple Nat Nat Nat := mkTriple 2 2 2;
    p' : Triple Nat Nat Nat :=
      p@Triple{
        fst := fst + 1;
        snd := snd * 3 + thd + fst
      };
    f : Triple Nat Nat Nat -> Triple Nat Nat Nat :=
      (@Triple{fst := fst * 10});
  in sum <| ite
    (mf
      mkPair@{
        fst := mkPair true nil;
        snd := 0 :: nil
      })
    (f p')
    mkTriple@{
      fst := 0;
      thd := 0;
      snd := 0
    };