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.

2 files changed, 81 insertions, 0 deletions

diff --git a/lib/kernel/date.ml b/lib/kernel/date.ml
new file mode 100644
index 0000000..525b35b
--- /dev/null
+++ b/lib/kernel/date.ml
@@ -0,0 +1,58 @@
+type weekday = Sun | Mon | Tue | Wed | Thu | Fri | Sat
+
+(* Internal representation: rata die = days since 1970-01-01 (proleptic
+   Gregorian). Howard Hinnant's civil<->days algorithm; OCaml's `/` truncates
+   toward zero, which the negative-branch adjustments account for. *)
+type t = int
+
+let days_from_civil y m d =
+  let y = if m <= 2 then y - 1 else y in
+  let era = (if y >= 0 then y else y - 399) / 400 in
+  let yoe = y - (era * 400) in
+  let doy = ((153 * (if m > 2 then m - 3 else m + 9)) + 2) / 5 + (d - 1) in
+  let doe = (yoe * 365) + (yoe / 4) - (yoe / 100) + doy in
+  (era * 146097) + doe - 719468
+
+let civil_from_days z =
+  let z = z + 719468 in
+  let era = (if z >= 0 then z else z - 146096) / 146097 in
+  let doe = z - (era * 146097) in
+  let yoe = (doe - (doe / 1460) + (doe / 36524) - (doe / 146096)) / 365 in
+  let y = yoe + (era * 400) in
+  let doy = doe - ((365 * yoe) + (yoe / 4) - (yoe / 100)) in
+  let mp = ((5 * doy) + 2) / 153 in
+  let d = doy - (((153 * mp) + 2) / 5) + 1 in
+  let m = if mp < 10 then mp + 3 else mp - 9 in
+  ((if m <= 2 then y + 1 else y), m, d)
+
+let year t = let y, _, _ = civil_from_days t in y
+let month t = let _, m, _ = civil_from_days t in m
+let day t = let _, _, d = civil_from_days t in d
+
+let is_leap y = (y mod 4 = 0 && y mod 100 <> 0) || y mod 400 = 0
+
+let days_in_month y m =
+  match m with
+  | 1 | 3 | 5 | 7 | 8 | 10 | 12 -> 31
+  | 4 | 6 | 9 | 11 -> 30
+  | 2 -> if is_leap y then 29 else 28
+  | _ -> 0
+
+let make ~year ~month ~day =
+  if year < 1583 || year > 9999 then
+    Error (Printf.sprintf "year %d out of range 1583..9999" year)
+  else if month < 1 || month > 12 then
+    Error (Printf.sprintf "month %d out of range 1..12" month)
+  else if day < 1 || day > days_in_month year month then
+    Error (Printf.sprintf "day %d out of range for %04d-%02d" day year month)
+  else Ok (days_from_civil year month day)
+
+let to_rata t = t
+let of_rata z = z
+let add_days t n = t + n
+let compare = Int.compare
+
+let weekday t =
+  (* rata 0 = 1970-01-01 = Thursday (index 4 with Sun=0). *)
+  let w = (((t + 4) mod 7) + 7) mod 7 in
+  [| Sun; Mon; Tue; Wed; Thu; Fri; Sat |].(w)
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