RecordUpdateSyntax.agda

module RecordUpdateSyntax where

open import Common.Prelude
open import Common.Equality

data Param : Nat → Set where
  param : ∀ n → Param (suc n)

record R : Set where
  field
    {i} : Nat
    p : Param i
    s : Nat

old : R
old = record { p = param 0; s = 1 }

-- Simple update, it should be able to infer the type and the implicit.
new : _
new = record old { p = param 1 }

new′ : R
new′ = record { i = 2; p = param 1; s = 1 }

-- Here's a needlessly complex update.
upd-p-s : _ → _ → _ → R
upd-p-s zero s r = record r { p = param zero; s = s }
upd-p-s (suc n) s r = record (upd-p-s n 0 r) { p = param n; s = s }

eq₁ : new ≡ new′
eq₁ = refl

eq₂ : upd-p-s zero 1 (record new { s = 0 }) ≡ old
eq₂ = refl

-- Check that instance arguments are handled properly
postulate
  T : Nat → Set
  t0 : T 0
  t1 : T 1

record Instance : Set where
  field
    n : Nat
    {{t}} : T n

r0 : Instance
r0 = record { n = 0 }

r1 : Instance
r1 = record r0 { n = 1 }

check : Instance.t r1 ≡ t1
check = refl