module Peras.Numbering where

Slots

record SlotNumber : Set where
  constructor MkSlotNumber
  field getSlotNumber : ℕ

  next : SlotNumber
  next = record {getSlotNumber = suc getSlotNumber}

  _earlierBy_  : ℕ → SlotNumber
  _earlierBy_ n = record {getSlotNumber = getSlotNumber ∸ n}

open SlotNumber public

instance
  iSlotNumberEq : Eq SlotNumber
  iSlotNumberEq ._==_ x y = getSlotNumber x == getSlotNumber y

  iSlotNumberOrd : Ord SlotNumber
  iSlotNumberOrd = ordFromCompare λ x y → compare (getSlotNumber x) (getSlotNumber y)

  iNumberSlotNumber : Number SlotNumber
  iNumberSlotNumber .Number.Constraint _ = ⊤
  iNumberSlotNumber .fromNat n = MkSlotNumber n

Rounds

record RoundNumber : Set where
  constructor MkRoundNumber
  field getRoundNumber : ℕ

  prev : RoundNumber
  prev = record { getRoundNumber = pred getRoundNumber }

open RoundNumber public

instance
  iRoundNumberEq : Eq RoundNumber
  iRoundNumberEq ._==_ x y = getRoundNumber x == getRoundNumber y

  iRoundNumberOrd : Ord RoundNumber
  iRoundNumberOrd = ordFromCompare λ x y → compare (getRoundNumber x) (getRoundNumber y)

  iNumberRoundNumber : Number RoundNumber
  iNumberRoundNumber .Number.Constraint _ = ⊤
  iNumberRoundNumber .fromNat n = MkRoundNumber n

_≟-RoundNumber_ : DecidableEquality RoundNumber
(MkRoundNumber r₁) ≟-RoundNumber (MkRoundNumber r₂) with r₁ ≟ r₂
... | yes p = yes (cong MkRoundNumber p)
... | no ¬p =  no (¬p ∘ cong getRoundNumber)

roundToSlot : ℕ → RoundNumber → SlotNumber
roundToSlot T (MkRoundNumber r) = MkSlotNumber (r * T)

slotToRound : PerasParams → SlotNumber → RoundNumber
slotToRound protocol (MkSlotNumber n) = MkRoundNumber (div n (perasU protocol))

slotInRound : PerasParams → SlotNumber → SlotNumber
slotInRound protocol slot = MkSlotNumber (mod (getSlotNumber slot) (perasU protocol))

nextSlot : SlotNumber → SlotNumber
nextSlot (MkSlotNumber n) = MkSlotNumber ( + n)

nextRound : RoundNumber → RoundNumber
nextRound (MkRoundNumber n) = MkRoundNumber ( + n)