From cdb7ffe804ca19aee935af090f76c9eb83cbce14 Mon Sep 17 00:00:00 2001 From: Lukasz Kasprzak Date: Fri, 31 Jul 2026 14:04:22 +0200 Subject: kernel(date): proleptic Gregorian date, validated make + arithmetic Hinnant civil<->days rep (1970-epoch rata die); make validates month/day and the 1583..9999 domain; of_rata/add_days are total arithmetic. Weekday, compare. Tested: known weekdays, leap boundaries, rejects; qcheck round-trip / add-inverse / weekday-cycle properties over random in-range dates. --- lib/kernel/date.mli | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 lib/kernel/date.mli (limited to 'lib/kernel/date.mli') diff --git a/lib/kernel/date.mli b/lib/kernel/date.mli new file mode 100644 index 0000000..b684d61 --- /dev/null +++ b/lib/kernel/date.mli @@ -0,0 +1,23 @@ +(** Proleptic Gregorian calendar dates over the supported domain 1583..9999. + [t] is opaque; the internal representation is a day-count (rata die) so + arithmetic and comparison are total and cheap. *) + +type t +type weekday = Sun | Mon | Tue | Wed | Thu | Fri | Sat + +(** [make ~year ~month ~day] validates the date; rejects a month/day out of + range and any year outside 1583..9999. *) +val make : year:int -> month:int -> day:int -> (t, string) result + +val year : t -> int +val month : t -> int +val day : t -> int +val weekday : t -> weekday + +(** [to_rata]/[of_rata] expose the underlying day-count (days since 1970-01-01); + [of_rata] and [add_days] are unbounded total arithmetic (they may denote a + year outside 1583..9999 — only [make] enforces the domain). *) +val to_rata : t -> int +val of_rata : int -> t +val add_days : t -> int -> t +val compare : t -> t -> int -- cgit v1.3