feat: add date and time functionality

src/Std.lean

@@ -6,3 +6,4 @@ Authors: Sebastian Ullrich
 prelude
 import Std.Data
 import Std.Sat
+import Std.Time

src/Std/Time.lean

@@ -0,0 +1,174 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+import Std.Time.Time
+import Std.Time.Date
+import Std.Time.Zoned
+import Std.Time.Format
+import Std.Time.DateTime
+import Std.Time.Notation
+
+namespace Time
+
+/-!
+# Time
+
+The Lean4 API for date, time, and duration functionalities, following the ISO standards.
+
+# Overview
+
+This module of the standard library defines various concepts related to time, such as dates, times,
+time zones and durations. These types are designed to be strongly-typed and to avoid problems with
+conversion. It offers both unbounded and bounded variants to suit different use cases, like
+adding days to a date or representing ordinal values.
+
+# Date and Time Components
+
+Date and time components are classified into different types based how you SHOULD use them. These
+components are categorized as:
+
+## Offset
+
+Offsets represent unbounded shifts in specific date or time units. They are typically used in operations
+like `date.addDays` where a `Day.Offset` is the parameter. Some offsets, such as `Month.Offset`, do not
+correspond directly to a specific duration in seconds, as their value depends on the context (if
+the year is leap or the size of the month). Offsets with a clear correspondent to seconds can be
+converted because they use a internal type called `UnitVal`.
+
+- Types with a correspondence to seconds:
+  - `Day.Offset`
+  - `Hour.Offset`
+  - `WeekOfYear.Offset`
+  - `Millisecond.Offset`
+  - `Nanosecond.Offset`
+  - `Second.Offset`
+
+- Types without a correspondence to seconds:
+  - `Month.Offset`
+  - `Year.Offset`
+
+## Ordinal
+
+Ordinal types represent specific bounded values in reference to another unit, e.g, `Day.Ordinal`
+represents a day in a month, ranging from 1 to 31. Some ordinal types like `Hour.Ordinal` and `Second.Ordinal`,
+allow for values beyond the normal range (e.g, 24 hours and 61 seconds) to accomodate special cases
+with leap seconds like `24:00:00` that is valid in ISO 8601.
+
+- Ordinal types:
+  - `Day.Ordinal`: Ranges from 1 to 31.
+  - `Day.Ordinal.OfYear`: Ranges from 1 to (365 or 366).
+  - `Month.Ordinal`: Ranges from 1 to 12.
+  - `WeekOfYear.Ordinal`: Ranges from 1 to 53.
+  - `Hour.Ordinal`: Ranges from 0 to 24.
+  - `Millisecond.Ordinal`: Ranges from 0 to 999.
+  - `Minute.Ordinal`: Ranges from 0 to 59.
+  - `Nanosecond.Ordinal`: Ranges from 0 to 999,999,999.
+  - `Second.Ordinal`: Ranges from 0 to 60.
+  - `Weekday`: That is a inductive type with all the seven days.
+
+## Span
+
+Span types are used as subcomponents of other types. They represent a range of values in the limits
+of the parent type, e.g, `Nanosecond.Span` ranges from -999,999,999 to 999,999,999, as 1,000,000,000
+nanoseconds corresponds to one second.
+
+- Span types:
+  - `Nanosecond.Span`: Ranges from -999,999,999 to 999,999,999.
+
+# Date and Time Types
+
+Dates and times are composed of these components. Dates are "absolute" value in contrast with Offsets
+that are just shifts in dates and times. Types like `Date` are made using of components such as `Year.Offset`,
+`Month.Ordinal`, and `Day.Ordinal`, with a proof of the date's validity. Some types, like `Date.Scalar`,
+are wrappers around offsets (e.g., `Day.Offset`) and represent absolute dates relative to the UNIX Epoch.
+
+## Date
+These types provide precision down to the day level, useful for representing and manipulating dates.
+
+- **`LocalDate`:** Represents a calendar date in the format `YYYY-MM-DD`.
+- **`LocalDate.Scalar`:** : Represents an absolute date with day-level precision in a compact format `DD`.
+  It encapsulates days since the UNIX Epoch.
+- **`WeekDate`:** Uses the `YYYY-Www` format with week level precision.
+
+## Time
+These types offer precision down to the nanosecond level, useful for representing and manipulating time of day.
+
+- **`LocalTime`**: Represents a time of day in the format `HH:mm:ss.SSSSSSSSS`.
+
+## Date and time
+Combines date and time into a single representation, useful for precise timestamps and scheduling.
+
+- **`LocalDateTime`**: Represents both date and time in the format `YYYY-MM-DDTHH:mm:ss.SSSSSSSSS`.
+- **`Timestamp`**: Represents a point in time with second-level precision.
+
+## Zoned date and times.
+Combines date, time and time zones.
+
+- **`DateTime`**: Represents both date and time but with a time zone in the type constructor.
+- **`ZonedDateTime`**: An existencial version of the `DateTime`.
+
+## Duration
+Represents spans of time and the difference between two points in time.
+
+- **`Instant`**: Represents a non-negative instant in time with nanosecond precision, represents a
+  specific point on the time axis.
+- **`Duration`**: Represents the time span or difference between two `Instant` values with nanosecond precision.
+
+# Formats
+
+Format strings are used to convert between `String` representations and date/time types, e.g, `YYYY-MM-DD'T'hh:mm:ss.sssZ`.
+The supported formats include:
+
+- **Year:**
+  - `YYYY`: Four-digit year (e.g., 2024)
+  - `YY`: Two-digit year (e.g., 24 for 2024)
+- **Month:**
+  - `MMMM`: Full month name (e.g., January, February)
+  - `MMM`: Abbreviated month name (e.g., Jan, Feb)
+  - `MM`: Two-digit month (e.g., 01 for January)
+  - `M`: One or two-digit month (e.g., 1 for January, 10 for October)
+- **Day:**
+  - `DD`: Two-digit day of the month (e.g., 01, 02)
+  - `D`: One or two-digit day of the month (e.g., 1, 2)
+  - `d`: One or two-digit day of the month with space padding (e.g., " 1", "12")
+- **Day of Week:**
+  - `EEEE`: Full name of the day of the week (e.g., Monday, Tuesday)
+  - `EEE`: Abbreviated day of the week (e.g., Mon, Tue)
+- **Hour:**
+  - `hh`: Two-digit hour in 24-hour format (e.g., 13, 14)
+  - `h`: One or two-digit hour in 24-hour format (e.g., 1, 2)
+  - `HH`: Two-digit hour in 12-hour format (e.g., 01, 02)
+  - `H`: One or two-digit hour in 12-hour format (e.g., 1, 2)
+- **AM/PM Indicator:**
+  - `AA`: Uppercase AM/PM (e.g., AM, PM)
+  - `aa`: Lowercase am/pm (e.g., am, pm)
+- **Minute:**
+  - `mm`: Two-digit minute (e.g., 01, 02)
+  - `m`: One or two-digit minute (e.g., 1, 2)
+- **Second:**
+  - `sss`: Three-digit milliseconds (e.g., 001, 202)
+  - `ss`: Two-digit second (e.g., 01, 02)
+  - `s`: One or two-digit second (e.g., 1, 2)
+- **Timezone:**
+  - `ZZZZZ`: Full timezone offset with hours and minutes (e.g., +03:00)
+  - `ZZZZ`: Timezone offset without the colon (e.g., +0300)
+  - `ZZZ`: Like `ZZZZ`, but with "UTC" for UTC
+  - `Z`: Like `ZZZZZ`, but with "Z" for UTC
+  - `z`: Timezone name (e.g., Brasilia Standard Time)
+
+# Macros
+
+In order to help the user build dates easily, there are a lot of macros available for creating dates.
+
+- **`date% DD-MM-YYYY`**: Defines a date in the `DD-MM-YYYY` format.
+- **`date% HH:mm:ss`**: Defines a time in the `HH:mm:ss` format.
+- **`date% HH:mm:ss.sssssss`**: Defines a time in the `HH:mm:ss.sssssss` format, including fractional seconds.
+- **`date% YYYY-MM-DD:HH:mm:ss`**: Defines a datetime in the `YYYY-MM-DD:HH:mm:ss` format.
+- **`date% YYYY-MM-DDTHH:mm:ssZ`**: Defines a datetime with a timezone in the `YYYY-MM-DDTHH:mm:ssZ` format.
+- **`offset% +HH:mm`**: Defines a timezone offset in the format `+HH:mm`.
+- **`timezone% NAME/ID offset% +HH:mm`**: Defines a timezone with a name and an offset.
+- **`date-spec% "format"`**: Defines a date specification format at compile time using the provided format string.
+
+-/

src/Std/Time/Date.lean

@@ -0,0 +1,9 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+prelude
+import Std.Time.Date.Basic
+import Std.Time.Date.WeekDate
+import Std.Time.Date.LocalDate

src/Std/Time/Date/Basic.lean

@@ -0,0 +1,7 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+prelude
+import Std.Time.Date.Unit.Basic

src/Std/Time/Date/LocalDate.lean

@@ -0,0 +1,143 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+prelude
+import Std.Time.Internal
+import Std.Time.Date.Basic
+import Std.Time.Date.Scalar
+
+namespace Std
+namespace Time
+
+/--
+Date in YMD format.
+-/
+structure LocalDate where
+  year : Year.Offset
+  month : Month.Ordinal
+  day : Day.Ordinal
+  valid : year.Valid month day
+  deriving Repr
+
+namespace LocalDate
+
+/--
+Force the date to be valid.
+-/
+def clip (year : Year.Offset) (month : Month.Ordinal) (day : Day.Ordinal) : LocalDate :=
+  let ⟨day, valid⟩ := month.clipDay year.isLeap day
+  LocalDate.mk year month day valid
+
+instance : Inhabited LocalDate where
+  default := clip 0 1 1
+
+/--
+Creates a new `LocalDate` using YMD.
+-/
+def ofYearMonthDay (year : Year.Offset) (month : Month.Ordinal) (day : Day.Ordinal) : Option LocalDate :=
+  if valid : year.Valid month day
+    then some (LocalDate.mk year month day valid)
+    else none
+
+/--
+Creates a new `LocalDate` using YO.
+-/
+def ofYearOrdinal (year : Year.Offset) (ordinal : Day.Ordinal.OfYear year.isLeap) : LocalDate :=
+  let ⟨⟨month, day⟩, valid⟩ := ordinal.toMonthAndDay
+  LocalDate.mk year month day valid
+
+/--
+Creates a new `LocalDate` using the `Day.Offset` which `0` corresponds the UNIX Epoch.
+-/
+def ofDaysSinceUNIXEpoch (day : Day.Offset) : LocalDate :=
+  let z := day.toInt + 719468
+  let era := (if z ≥ 0 then z else z - 146096) / 146097
+  let doe := z - era * 146097
+  let yoe := (doe - doe / 1460 + doe / 36524 - doe / 146096) / 365
+  let y := yoe + era * 400
+  let doy := doe - (365 * yoe + yoe / 4 - yoe / 100)
+  let mp : Int := (5 * doy + 2) / 153
+  let d := doy - (153 * mp + 2) / 5
+  let m := mp + (if mp < 10 then 3 else -9)
+  let y := y + (if m <= 2 then 1 else 0)
+
+  .clip y (.clip m (by decide)) (.clip (d + 1) (by decide))
+
+/--
+Returns the `Weekday` of a `LocalDate`.
+-/
+def weekday (date : LocalDate) : Weekday :=
+  let q := date.day.toInt
+  let m := date.month.toInt
+  let y := date.year.toInt
+
+  let y := if m < 2 then y - 1 else y
+  let m := if m < 2 then m + 12 else m
+
+  let k := y % 100
+  let j := y / 100
+  let part := q + (13 * (m + 1)) / 5 + k + (k / 4)
+  let h :=  if y ≥ 1582 then part + (j/4) - 2*j else part + 5 - j
+  let d := (h + 5) % 7
+
+  .ofFin ⟨d.toNat % 7, Nat.mod_lt d.toNat (by decide)⟩
+
+/--
+Returns the `Weekday` of a `LocalDate` using Zeller's Congruence for the Julian calendar.
+-/
+def weekdayJulian (date : LocalDate) : Weekday :=
+  let month := date.month.toInt
+  let year := date.year.toInt
+
+  let q := date.day.toInt
+  let m := if month < 3 then month + 12 else month
+  let y := if month < 3 then year - 1 else year
+
+  let k := y % 100
+  let j := y / 100
+
+  let h := (q + (13 * (m + 1)) / 5 + k + (k / 4) + 5 - j) % 7
+  let d := (h + 5 - 1) % 7
+
+  .ofFin ⟨d.toNat % 7, Nat.mod_lt d.toNat (by decide)⟩
+
+/--
+Convert `LocalDate` to `Day.Offset` since the UNIX Epoch.
+-/
+def toDaysSinceUNIXEpoch (date : LocalDate) : Day.Offset :=
+  let y : Int := if date.month.toInt > 2 then date.year else date.year.toInt - 1
+  let era : Int := (if y ≥ 0 then y else y - 399) / 400
+  let yoe : Int := y - era * 400
+  let m : Int := date.month.toInt
+  let d : Int := date.day.toInt
+  let doy := (153 * (m + (if m > 2 then -3 else 9)) + 2) / 5 + d - 1
+  let doe := yoe * 365 + yoe / 4 - yoe / 100 + doy
+
+  .ofInt (era * 146097 + doe - 719468)
+
+/--
+Convert a `Scalar` to a `LocalDate` since the UNIX Epoch.
+-/
+def ofScalar (day : Scalar) : LocalDate :=
+  ofDaysSinceUNIXEpoch day.day
+
+/--
+Convert a `LocalDate` to a `Scalar` since the UNIX Epoch.
+-/
+def toScalar (date : LocalDate) : Scalar :=
+  ⟨toDaysSinceUNIXEpoch date⟩
+
+/--
+Calculate the Year.Offset from a LocalDate
+-/
+def yearsSince (date : LocalDate) (year : Year.Offset) : Year.Offset :=
+  date.year - year
+
+instance : HAdd LocalDate Day.Offset LocalDate where
+  hAdd date day :=  ofDaysSinceUNIXEpoch (toDaysSinceUNIXEpoch date + day)
+
+end LocalDate
+end Time
+end Std