Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Timezone support #970

Merged
merged 7 commits into from
May 11, 2021
Merged

Timezone support #970

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
ef686a7
Moved time library from time to chrono
May 8, 2021
d41c3c6
rust lint
May 9, 2021
ca80b57
rust lint
May 9, 2021
967cd50
Add copyright; timezone support
May 9, 2021
4010af2
Review comments
May 10, 2021
6a0edbf
Review comments
May 10, 2021
7e2b314
lint
May 10, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
148 changes: 99 additions & 49 deletions lib/time.dl
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,13 +1,16 @@
/// Library supporting dates, times, and date-times
/// This parallels closely the Rust time crate
/// https://time-rs.github.io/time/time/struct.Time.html
/// Based on the chrono crate
/// https://github.com/chronotope/chrono

///////////////////////////////////////////////////////////////////////////////////////////
/// The clock time within a given date. Nanosecond precision.
/// All minutes are assumed to have exactly 60 seconds; no attempt is
/// made to handle leap seconds (either positive or negative).
/// When comparing two Times, they are assumed to be in the same
/// calendar date.
/// ATTENTION: This module only contains deterministic function.
/// Since DDlog programs are supposed to be deterministic, there are no
/// functions such as today(), now()

extern type Time

Expand Down Expand Up @@ -44,47 +47,90 @@ extern function microsecond(t: Time): bit<32>
/// Get the nanoseconds within the second. The returned value will always be in the range 0..1000000000.
extern function nanosecond(t: Time): bit<32>

// Here is a list of the format specifiers:
// Spec Replaced by Example
// %a Abbreviated weekday name Thu
// %A Full weekday name Thursday
// %b Abbreviated month name Aug
// %B Full month name August
// %c Date and time representation, equivalent to %a %b %-d %-H:%M:%S %-Y Thu Aug 23 14:55:02 2001
// %C Year divided by 100 and truncated to integer (00-99) 20
// %d Day of the month, zero-padded (01-31) 23
// %D Short MM/DD/YY date, equivalent to %-m/%d/%y 8/23/01
// %F Short YYYY-MM-DD date, equivalent to %-Y-%m-%d 2001-08-23
// %g Week-based year, last two digits (00-99) 01
// %G Week-based year 2001
// %H Hour in 24h format (00-23) 14
// %I Hour in 12h format (01-12) 02
// %j Day of the year (001-366) 235
// %m Month as a decimal number (01-12) 08
// %M Minute (00-59) 55
// %N Subsecond nanoseconds. Always 9 digits 012345678
// %p am or pm designation pm
// %P AM or PM designation PM
// %r 12-hour clock time, equivalent to %-I:%M:%S %p 2:55:02 pm
// %R 24-hour HH:MM time, equivalent to %-H:%M 14:55
// %S Second (00-59) 02
// %T 24-hour clock time with seconds, equivalent to %-H:%M:%S 14:55:02
// %u ISO 8601 weekday as number with Monday as 1 (1-7) 4
// %U Week number with the first Sunday as the start of week one (00-53) 33
// %V ISO 8601 week number (01-53) 34
// %w Weekday as a decimal number with Sunday as 0 (0-6) 4
// %W Week number with the first Monday as the start of week one (00-53) 34
// %y Year, last two digits (00-99) 01
// %Y Full year, including + if >= 10,000 2001
// %z ISO 8601 offset from UTC in timezone (+HHMM) +0100
// %% Literal % %

// All specifiers that are strictly numerical have modifiers for formatting.
// Adding a modifier to a non-supporting specifier is a no-op.
// Modifier Behavior Example
// - (dash) No padding %-d => 5
// _ (underscore) Pad with spaces %_d => 5
// 0 Pad with zeros %0d => 05
// Here is a list of the format specifiers, which can be used for both parsing and formatting.
// This is based on the strftime format specification.
// https://docs.rs/chrono/0.4.19/chrono/format/strftime/index.html
/*
Spec. Example Description
DATE SPECIFIERS:
%Y 2001 The full proleptic Gregorian year, zero-padded to 4 digits.
%C 20 The proleptic Gregorian year divided by 100, zero-padded to 2 digits.
%y 01 The proleptic Gregorian year modulo 100, zero-padded to 2 digits.

%m 07 Month number (01--12), zero-padded to 2 digits.
%b Jul Abbreviated month name. Always 3 letters.
%B July Full month name. Also accepts corresponding abbreviation in parsing.
%h Jul Same as %b.

%d 08 Day number (01--31), zero-padded to 2 digits.
%e 8 Same as %d but space-padded. Same as %_d.

%a Sun Abbreviated weekday name. Always 3 letters.
%A Sunday Full weekday name. Also accepts corresponding abbreviation in parsing.
%w 0 Sunday = 0, Monday = 1, ..., Saturday = 6.
%u 7 Monday = 1, Tuesday = 2, ..., Sunday = 7. (ISO 8601)

%U 28 Week number starting with Sunday (00--53), zero-padded to 2 digits.
%W 27 Same as %U, but week 1 starts with the first Monday in that year instead.

%G 2001 Same as %Y but uses the year number in ISO 8601 week date.
%g 01 Same as %y but uses the year number in ISO 8601 week date.
%V 27 Same as %U but uses the week number in ISO 8601 week date (01--53).

%j 189 Day of the year (001--366), zero-padded to 3 digits.

%D 07/08/01 Month-day-year format. Same as %m/%d/%y.
%x 07/08/01 Locale's date representation (e.g., 12/31/99).
%F 2001-07-08 Year-month-day format (ISO 8601). Same as %Y-%m-%d.
%v 8-Jul-2001 Day-month-year format. Same as %e-%b-%Y.

TIME SPECIFIERS:
%H 00 Hour number (00--23), zero-padded to 2 digits.
%k 0 Same as %H but space-padded. Same as %_H.
%I 12 Hour number in 12-hour clocks (01--12), zero-padded to 2 digits.
%l 12 Same as %I but space-padded. Same as %_I.

%P am am or pm in 12-hour clocks.
%p AM AM or PM in 12-hour clocks.

%M 34 Minute number (00--59), zero-padded to 2 digits.
%S 60 Second number (00--60), zero-padded to 2 digits.
%f 026490000 The fractional seconds (in nanoseconds) since last whole second.
%.f .026490 Similar to .%f but left-aligned. These all consume the leading dot.
%.3f .026 Similar to .%f but left-aligned but fixed to a length of 3.
%.6f .026490 Similar to .%f but left-aligned but fixed to a length of 6.
%.9f .026490000 Similar to .%f but left-aligned but fixed to a length of 9.
%3f 026 Similar to %.3f but without the leading dot.
%6f 026490 Similar to %.6f but without the leading dot.
%9f 026490000 Similar to %.9f but without the leading dot.

%R 00:34 Hour-minute format. Same as %H:%M.
%T 00:34:60 Hour-minute-second format. Same as %H:%M:%S.
%X 00:34:60 Locale's time representation (e.g., 23:13:48).
%r 12:34:60 AM Hour-minute-second format in 12-hour clocks. Same as %I:%M:%S %p.

TIME ZONE SPECIFIERS:
%Z ACST Local time zone name. Skips all non-whitespace characters during parsing.
%z +0930 Offset from the local time to UTC (with UTC being +0000).
%:z +09:30 Same as %z but with a colon.
%#z +09 Parsing only: Same as %z but allows minutes to be missing or present.

DATE & TIME SPECIFIERS:
%c Sun Jul 8 00:34:60 2001 Locale's date and time (e.g., Thu Mar 3 23:05:25 2005).
%+ 2001-07-08T00:34:60.026490+09:30 ISO 8601 / RFC 3339 date & time format.
%s 994518299 UNIX timestamp, the number of seconds since 1970-01-01 00:00 UTC.

SPECIAL SPECIFIERS:
%t Literal tab (\t).
%n Literal newline (\n).
%% Literal percent sign.

It is possible to override the default padding behavior of numeric specifiers %?. This is not allowed for other specifiers and will result in the BAD_FORMAT error.
Modifier Description
%-? Suppresses any padding including spaces and zeroes. (e.g. %j = 012, %-j = 12)
%_? Uses spaces as a padding. (e.g. %j = 012, %_j = 12)
%0? Uses zeroes as a padding. (e.g. %e = 9, %0e = 09)
*/

/// Convert the time to a string using a default format.
extern function time2string(t: Time): string
Expand Down Expand Up @@ -136,12 +182,6 @@ extern function ordinal(date: Date): bit<16>
/// Get the ISO week number. The returned value will always be in the range 1..=53.
extern function week(date: Date): bit<8>

/// Get the week number where week 1 begins on the first Sunday. The returned value will always be in the range 0..=53.
extern function sunday_based_week(date: Date): bit<8>

/// Get the week number where week 1 begins on the first Monday. The returned value will always be in the range 0..=53.
extern function monday_based_week(date: Date): bit<8>

/// Get the weekday.
extern function weekday(date: Date): Weekday

Expand Down Expand Up @@ -183,6 +223,7 @@ typedef Weekday = Monday
| Saturday
| Sunday

// This is really a local date + time, without timezone information
typedef DateTime = DateTime { date: Date, time: Time }

/// Parse a string into a DateTime using the specified format
Expand All @@ -205,3 +246,12 @@ extern function datetime_format(d: DateTime, format: string): string

/// Create a DateTime from a given unix timestamp
extern function datetime_from_unix_timestamp(timestamp: signed<64>): DateTime

///////////////////////////////////////////////////
// Timezone handling, based on chrono

/// An object representing a datetime with a timezone
extern type TzDateTime

/// Convert a DateTime to a TzDateTime in the UTC timezone
extern function utc_timezone(dt: DateTime): TzDateTime
Loading