diff options
| -rw-r--r-- | lib/kernel/date.ml | 58 | ||||
| -rw-r--r-- | lib/kernel/date.mli | 23 | ||||
| -rw-r--r-- | test/test_colitur.ml | 7 | ||||
| -rw-r--r-- | test/test_date.ml | 62 |
4 files changed, 145 insertions, 5 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 diff --git a/test/test_colitur.ml b/test/test_colitur.ml index 7fc5239..734257c 100644 --- a/test/test_colitur.ml +++ b/test/test_colitur.ml @@ -1,5 +1,2 @@ -(* Aggregating test runner. Per-module suites (Test_date, Test_computus) are added - in Tasks 1-2; for now the scaffold proves the harness builds and runs. *) -let () = - Alcotest.run "colitur" - [ ("scaffold", [ Alcotest.test_case "harness builds" `Quick (fun () -> ()) ]) ] +(* Aggregating test runner. Per-module suites live in test_<module>.ml. *) +let () = Alcotest.run "colitur" [ Test_date.suite ] diff --git a/test/test_date.ml b/test/test_date.ml new file mode 100644 index 0000000..2458659 --- /dev/null +++ b/test/test_date.ml @@ -0,0 +1,62 @@ +module D = Colitur_kernel.Date + +let mk y m d = + match D.make ~year:y ~month:m ~day:d with + | Ok t -> t + | Error e -> Alcotest.failf "make %04d-%02d-%02d: %s" y m d e + +let wd_str = function + | D.Sun -> "Sun" | D.Mon -> "Mon" | D.Tue -> "Tue" | D.Wed -> "Wed" + | D.Thu -> "Thu" | D.Fri -> "Fri" | D.Sat -> "Sat" + +let ymd d = (D.year d, D.month d, D.day d) + +let test_weekday () = + Alcotest.(check string) "1970-01-01 is Thursday" "Thu" (wd_str (D.weekday (mk 1970 1 1))); + Alcotest.(check string) "2026-07-31 is Friday" "Fri" (wd_str (D.weekday (mk 2026 7 31))) + +let test_roundtrip () = + let d = mk 2026 7 31 in + Alcotest.(check int) "of_rata(to_rata d) = d" 0 (D.compare (D.of_rata (D.to_rata d)) d) + +let test_add_days () = + Alcotest.(check (triple int int int)) "2024-02-28 +1 = 2024-02-29" + (2024, 2, 29) (ymd (D.add_days (mk 2024 2 28) 1)); + Alcotest.(check (triple int int int)) "2023-02-28 +1 = 2023-03-01" + (2023, 3, 1) (ymd (D.add_days (mk 2023 2 28) 1)) + +let test_make_reject () = + Alcotest.(check bool) "reject 2026-02-30" true (Result.is_error (D.make ~year:2026 ~month:2 ~day:30)); + Alcotest.(check bool) "reject year 1000" true (Result.is_error (D.make ~year:1000 ~month:1 ~day:1)) + +(* ---- properties (year-independent, the confidence-to-9999 core) ---- *) + +let arb_date = + let open QCheck in + map + (fun (y, off) -> + let jan1 = match D.make ~year:y ~month:1 ~day:1 with Ok t -> t | Error e -> failwith e in + D.of_rata (D.to_rata jan1 + off)) + (pair (int_range 1583 9999) (int_range 0 364)) + +let prop_roundtrip = + QCheck.Test.make ~name:"of_rata . to_rata = id" arb_date + (fun d -> D.compare (D.of_rata (D.to_rata d)) d = 0) + +let prop_add_inverse = + QCheck.Test.make ~name:"add_days n then -n = id" + QCheck.(pair arb_date (int_range (-4000) 4000)) + (fun (d, n) -> D.compare (D.add_days (D.add_days d n) (-n)) d = 0) + +let prop_weekday_cycle = + QCheck.Test.make ~name:"weekday(add_days d 7) = weekday d" arb_date + (fun d -> D.weekday (D.add_days d 7) = D.weekday d) + +let suite = + ( "Date", + [ Alcotest.test_case "weekday" `Quick test_weekday; + Alcotest.test_case "roundtrip" `Quick test_roundtrip; + Alcotest.test_case "add_days boundaries" `Quick test_add_days; + Alcotest.test_case "make rejects invalid" `Quick test_make_reject ] + @ List.map QCheck_alcotest.to_alcotest + [ prop_roundtrip; prop_add_inverse; prop_weekday_cycle ] ) |
