cjc_runtime/
datetime.rs

1//! DateTime support for CJC.
2//!
3//! Design decisions:
4//! - Epoch millis (i64), UTC only — deterministic, no timezone ambiguity
5//! - `datetime_now()` is NONDET (uses system clock)
6//! - All other operations are pure arithmetic on epoch millis
7//! - Leap year handling for year/month/day extraction
8
9// ---------------------------------------------------------------------------
10// Constants
11// ---------------------------------------------------------------------------
12
13const MILLIS_PER_SECOND: i64 = 1_000;
14const MILLIS_PER_MINUTE: i64 = 60 * MILLIS_PER_SECOND;
15const MILLIS_PER_HOUR: i64 = 60 * MILLIS_PER_MINUTE;
16const MILLIS_PER_DAY: i64 = 24 * MILLIS_PER_HOUR;
17
18// Days in each month (non-leap year)
19const DAYS_IN_MONTH: [i64; 12] = [31, 28, 31, 30, 31, 30, 31, 31, 30, 31, 30, 31];
20
21// ---------------------------------------------------------------------------
22// Core functions
23// ---------------------------------------------------------------------------
24
25/// Returns current UTC time as epoch milliseconds.
26/// This is NONDET — the only nondeterministic datetime operation.
27pub fn datetime_now() -> i64 {
28    std::time::SystemTime::now()
29        .duration_since(std::time::UNIX_EPOCH)
30        .unwrap_or_default()
31        .as_millis() as i64
32}
33
34/// Create a datetime from epoch milliseconds (identity, but validates type).
35pub fn datetime_from_epoch(millis: i64) -> i64 {
36    millis
37}
38
39/// Create a datetime from year, month, day, hour, minute, second components.
40/// All components are 1-based for month/day.
41pub fn datetime_from_parts(year: i64, month: i64, day: i64, hour: i64, min: i64, sec: i64) -> i64 {
42    let days = days_from_civil(year, month, day);
43    days * MILLIS_PER_DAY + hour * MILLIS_PER_HOUR + min * MILLIS_PER_MINUTE + sec * MILLIS_PER_SECOND
44}
45
46// ---------------------------------------------------------------------------
47// Extraction (pure arithmetic)
48// ---------------------------------------------------------------------------
49
50/// Extract the year from epoch millis.
51pub fn datetime_year(millis: i64) -> i64 {
52    let (y, _, _) = civil_from_days(millis.div_euclid(MILLIS_PER_DAY));
53    y
54}
55
56/// Extract the month (1-12) from epoch millis.
57pub fn datetime_month(millis: i64) -> i64 {
58    let (_, m, _) = civil_from_days(millis.div_euclid(MILLIS_PER_DAY));
59    m
60}
61
62/// Extract the day of month (1-31) from epoch millis.
63pub fn datetime_day(millis: i64) -> i64 {
64    let (_, _, d) = civil_from_days(millis.div_euclid(MILLIS_PER_DAY));
65    d
66}
67
68/// Extract the hour (0-23) from epoch millis.
69pub fn datetime_hour(millis: i64) -> i64 {
70    let day_millis = millis.rem_euclid(MILLIS_PER_DAY);
71    day_millis / MILLIS_PER_HOUR
72}
73
74/// Extract the minute (0-59) from epoch millis.
75pub fn datetime_minute(millis: i64) -> i64 {
76    let day_millis = millis.rem_euclid(MILLIS_PER_DAY);
77    (day_millis % MILLIS_PER_HOUR) / MILLIS_PER_MINUTE
78}
79
80/// Extract the second (0-59) from epoch millis.
81pub fn datetime_second(millis: i64) -> i64 {
82    let day_millis = millis.rem_euclid(MILLIS_PER_DAY);
83    (day_millis % MILLIS_PER_MINUTE) / MILLIS_PER_SECOND
84}
85
86// ---------------------------------------------------------------------------
87// Arithmetic (pure)
88// ---------------------------------------------------------------------------
89
90/// Difference between two datetimes in milliseconds.
91pub fn datetime_diff(a: i64, b: i64) -> i64 {
92    a - b
93}
94
95/// Add milliseconds to a datetime.
96pub fn datetime_add_millis(dt: i64, millis: i64) -> i64 {
97    dt + millis
98}
99
100// ---------------------------------------------------------------------------
101// Formatting (pure)
102// ---------------------------------------------------------------------------
103
104/// Format a datetime as ISO 8601 UTC string: `YYYY-MM-DDTHH:MM:SSZ`
105pub fn datetime_format(millis: i64) -> String {
106    let days = millis.div_euclid(MILLIS_PER_DAY);
107    let (year, month, day) = civil_from_days(days);
108    let day_millis = millis.rem_euclid(MILLIS_PER_DAY);
109    let hour = day_millis / MILLIS_PER_HOUR;
110    let minute = (day_millis % MILLIS_PER_HOUR) / MILLIS_PER_MINUTE;
111    let second = (day_millis % MILLIS_PER_MINUTE) / MILLIS_PER_SECOND;
112    format!(
113        "{:04}-{:02}-{:02}T{:02}:{:02}:{:02}Z",
114        year, month, day, hour, minute, second
115    )
116}
117
118// ---------------------------------------------------------------------------
119// Civil date algorithms (adapted from Howard Hinnant's algorithms)
120// ---------------------------------------------------------------------------
121
122/// Returns true if `year` is a leap year.
123fn is_leap_year(year: i64) -> bool {
124    (year % 4 == 0 && year % 100 != 0) || (year % 400 == 0)
125}
126
127/// Convert year/month/day to days since Unix epoch (1970-01-01).
128/// Month is 1-12, day is 1-31.
129fn days_from_civil(year: i64, month: i64, day: i64) -> i64 {
130    // Shift March to month 1 for easier calculation
131    let (y, m) = if month <= 2 {
132        (year - 1, month + 9)
133    } else {
134        (year, month - 3)
135    };
136    let era = y.div_euclid(400);
137    let yoe = y.rem_euclid(400); // year of era [0, 399]
138    let doy = (153 * m + 2) / 5 + day - 1; // day of year [0, 365]
139    let doe = yoe * 365 + yoe / 4 - yoe / 100 + doy; // day of era [0, 146096]
140    era * 146097 + doe - 719468 // shift to Unix epoch
141}
142
143/// Convert days since Unix epoch to (year, month, day).
144fn civil_from_days(days: i64) -> (i64, i64, i64) {
145    let z = days + 719468;
146    let era = z.div_euclid(146097);
147    let doe = z.rem_euclid(146097); // day of era [0, 146096]
148    let yoe = (doe - doe / 1460 + doe / 36524 - doe / 146096) / 365; // year of era [0, 399]
149    let y = yoe + era * 400;
150    let doy = doe - (365 * yoe + yoe / 4 - yoe / 100); // day of year [0, 365]
151    let mp = (5 * doy + 2) / 153; // month index [0, 11]
152    let d = doy - (153 * mp + 2) / 5 + 1; // day [1, 31]
153    let m = if mp < 10 { mp + 3 } else { mp - 9 };
154    let y = if m <= 2 { y + 1 } else { y };
155    (y, m, d)
156}
157
158/// Days in the given month (1-12) of the given year.
159pub fn days_in_month(year: i64, month: i64) -> i64 {
160    if month == 2 && is_leap_year(year) {
161        29
162    } else if month >= 1 && month <= 12 {
163        DAYS_IN_MONTH[(month - 1) as usize]
164    } else {
165        0
166    }
167}
168
169// ---------------------------------------------------------------------------
170// Tests
171// ---------------------------------------------------------------------------
172
173#[cfg(test)]
174mod tests {
175    use super::*;
176
177    #[test]
178    fn test_epoch_origin() {
179        // 1970-01-01 00:00:00 = 0
180        let dt = datetime_from_parts(1970, 1, 1, 0, 0, 0);
181        assert_eq!(dt, 0);
182    }
183
184    #[test]
185    fn test_known_date() {
186        // 2000-01-01 00:00:00 UTC
187        let dt = datetime_from_parts(2000, 1, 1, 0, 0, 0);
188        assert_eq!(datetime_year(dt), 2000);
189        assert_eq!(datetime_month(dt), 1);
190        assert_eq!(datetime_day(dt), 1);
191        assert_eq!(datetime_hour(dt), 0);
192    }
193
194    #[test]
195    fn test_extraction_roundtrip() {
196        let dt = datetime_from_parts(2024, 6, 15, 14, 30, 45);
197        assert_eq!(datetime_year(dt), 2024);
198        assert_eq!(datetime_month(dt), 6);
199        assert_eq!(datetime_day(dt), 15);
200        assert_eq!(datetime_hour(dt), 14);
201        assert_eq!(datetime_minute(dt), 30);
202        assert_eq!(datetime_second(dt), 45);
203    }
204
205    #[test]
206    fn test_leap_year() {
207        assert!(is_leap_year(2000));
208        assert!(is_leap_year(2024));
209        assert!(!is_leap_year(1900));
210        assert!(!is_leap_year(2023));
211    }
212
213    #[test]
214    fn test_days_in_feb_leap() {
215        assert_eq!(days_in_month(2024, 2), 29);
216        assert_eq!(days_in_month(2023, 2), 28);
217    }
218
219    #[test]
220    fn test_format_iso8601() {
221        let dt = datetime_from_parts(2024, 3, 14, 9, 26, 53);
222        let s = datetime_format(dt);
223        assert_eq!(s, "2024-03-14T09:26:53Z");
224    }
225
226    #[test]
227    fn test_diff() {
228        let a = datetime_from_parts(2024, 1, 2, 0, 0, 0);
229        let b = datetime_from_parts(2024, 1, 1, 0, 0, 0);
230        assert_eq!(datetime_diff(a, b), MILLIS_PER_DAY);
231    }
232
233    #[test]
234    fn test_add_millis() {
235        let dt = datetime_from_parts(2024, 1, 1, 0, 0, 0);
236        let dt2 = datetime_add_millis(dt, MILLIS_PER_HOUR);
237        assert_eq!(datetime_hour(dt2), 1);
238    }
239
240    #[test]
241    fn test_format_epoch() {
242        assert_eq!(datetime_format(0), "1970-01-01T00:00:00Z");
243    }
244
245    #[test]
246    fn test_determinism() {
247        // Pure operations must produce identical results
248        let a = datetime_from_parts(2024, 12, 31, 23, 59, 59);
249        let b = datetime_from_parts(2024, 12, 31, 23, 59, 59);
250        assert_eq!(a, b);
251        assert_eq!(datetime_format(a), datetime_format(b));
252    }
253}
cjc_runtime/datetime.rs

cjc_runtime/
datetime.rs
