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.

1 files changed, 23 insertions, 0 deletions

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