Date.agda

--
-- Inspired by a blog post written by Arnaud Bailly
-- https://abailly.github.io/posts/dependently-typed-date.html
--

{-# OPTIONS --without-K --safe #-}

module Date where

open import Data.Nat using (ℕ; zero; suc; _≡ᵇ_; _<_; _≤_; z≤n; s≤s; _≤?_; _<?_)
open import Data.Nat.DivMod using (_%_)
open import Data.Bool using (Bool; true; false; _∧_; _∨_; not)
open import Data.Maybe using (Maybe; just; nothing)

open import Relation.Nullary using (yes; no)
open import Relation.Nullary.Decidable using (True)

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; _≢_; refl; cong)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎; step-≡)

module Day where
    data t : Set where
        Day : (n : ℕ) → {True (0 <? n)} → t   -- Capture a day which should not be zero

    make : (n : ℕ) → {True (0 <? n)} → t
    make = Day

    value : t → ℕ
    value (Day n) = n

module Year where
    t : Set
    t = ℕ

    isLeap : t → Bool
    isLeap y = (check4 ∧ not check100) ∨ check400
        where check4   = y % 4   ≡ᵇ 0
              check100 = y % 100 ≡ᵇ 0
              check400 = y % 400 ≡ᵇ 0

module Month where
    data t : Set where
        January    : t
        February   : t
        March      : t
        April      : t
        May        : t
        June       : t
        July       : t
        August     : t
        September  : t
        October    : t
        November   : t
        December   : t

    toNat : t → ℕ
    toNat January    = 1
    toNat February   = 2
    toNat March      = 3
    toNat April      = 4
    toNat May        = 5
    toNat June       = 6
    toNat July       = 7
    toNat August     = 8
    toNat September  = 9
    toNat October    = 10
    toNat November   = 11
    toNat December   = 12
    
    duration : t → Year.t → Day.t
    duration January _   = Day.make 31
    duration February year with Year.isLeap year
    ... | true           = Day.make 29
    ... | false          = Day.make 28
    duration March _     = Day.make 31
    duration April _     = Day.make 30
    duration May _       = Day.make 31
    duration June _      = Day.make 30
    duration July _      = Day.make 31
    duration August _    = Day.make 31
    duration September _ = Day.make 30
    duration October _   = Day.make 31
    duration November _  = Day.make 30
    duration December _  = Day.make 31

module Date where
    data t : Set

    DateMakeType : Set
    DateMakeType = (year : Year.t) → (month : Month.t) → (day : ℕ)
                 → {≤max : True (day ≤? Day.value (Month.duration month year))}
                 → {min≤ : True (0 <? day)}
                 --------------------------------------------------------------
                 → t

    data t where
       Date : DateMakeType

    make : DateMakeType
    make = Date

module Test where
    _ : Date.t
    _ = Date.make 2020 Month.February 29