Skip to content

Commit

Permalink
Define Enso epoch start as 15th October 1582.
Browse files Browse the repository at this point in the history
  • Loading branch information
Akirathan committed Oct 19, 2022
1 parent a53fbc7 commit c356d39
Show file tree
Hide file tree
Showing 6 changed files with 167 additions and 61 deletions.
63 changes: 41 additions & 22 deletions distribution/lib/Standard/Base/0.0.0-dev/src/Data/Time/Date.enso
Original file line number Diff line number Diff line change
Expand Up @@ -184,6 +184,8 @@ type Date

## Returns the number of week of year this date falls into.

Throws `Time_Error` for a Date that is before epoch start.

Arguments:
- locale: the locale used to define the notion of weeks of year.
If no locale is provided, then the ISO 8601 week of year is used.
Expand All @@ -196,18 +198,23 @@ type Date
other hand, the first day of the week is Monday, and week 1 is the week
containing the first Thursday of the year. Therefore it is important to
properly specify the `locale` argument.
week_of_year : (Locale.Locale | Nothing) -> Integer
week_of_year : (Locale.Locale | Nothing) -> Integer ! Time_Error
week_of_year self locale=Nothing =
if locale.is_nothing then Time_Utils.get_field_as_localdate self IsoFields.WEEK_OF_WEEK_BASED_YEAR else
Time_Utils.week_of_year_localdate self locale.java_locale
self_in_epoch = Date_Time.ensure_in_epoch self
if locale.is_nothing then Time_Utils.get_field_as_localdate self_in_epoch IsoFields.WEEK_OF_WEEK_BASED_YEAR else
Time_Utils.week_of_year_localdate self_in_epoch locale.java_locale

## Returns if the date is in a leap year.
is_leap_year : Boolean
is_leap_year self = Time_Utils.is_leap_year self

Throws `Time_Error` for a Date that is before epoch start.
is_leap_year : Boolean ! Time_Error
is_leap_year self = Time_Utils.is_leap_year (Date_Time.ensure_in_epoch self)

## Returns the number of days in the year represented by this date.
length_of_year : Integer
length_of_year self = if self.is_leap_year then 366 else 365

Throws `Time_Error` for a Date that is before epoch start.
length_of_year : Integer ! Time_Error
length_of_year self = if (Date_Time.ensure_in_epoch self).is_leap_year then 366 else 365

## Returns the century of the date.
century : Integer
Expand All @@ -219,17 +226,21 @@ type Date
quarter self = Time_Utils.get_field_as_localdate self IsoFields.QUARTER_OF_YEAR

## Returns the number of days in the month represented by this date.
length_of_month : Integer
length_of_month self = Time_Utils.length_of_month self

Throws `Time_Error` for a Date that is before epoch start.
length_of_month : Integer ! Time_Error
length_of_month self = Time_Utils.length_of_month (Date_Time.ensure_in_epoch self)

## Returns the day of the year.
day_of_year : Integer
day_of_year self = Time_Utils.get_field_as_localdate self ChronoField.DAY_OF_YEAR

## Returns the day of the week.
day_of_week : Day_Of_Week

Throws `Time_Error` for a Date that is before epoch start.
day_of_week : Day_Of_Week ! Time_Error
day_of_week self =
Day_Of_Week.from (Time_Utils.get_field_as_localdate self ChronoField.DAY_OF_WEEK) Day_Of_Week.Monday
Day_Of_Week.from (Time_Utils.get_field_as_localdate (Date_Time.ensure_in_epoch self) ChronoField.DAY_OF_WEEK) Day_Of_Week.Monday

## Returns the first date within the `Date_Period` containing self.
start_of : Date_Period -> Date
Expand All @@ -242,6 +253,9 @@ type Date
## Counts workdays between self (inclusive) and the provided end date
(exclusive).

Throws `Time_Error` if called on a Date that is before an epoch
start. See `Date_Time.epoch_start`.

Arguments:
- end: the end date of the interval to count workdays in.
- holidays: dates of holidays to skip when counting workdays.
Expand All @@ -268,16 +282,17 @@ type Date
from Standard.Base import Date

example_workdays = Date.new 2020 1 1 . work_days_until (Date.new 2020 1 5)
work_days_until : Date -> Vector Date -> Boolean -> Integer
work_days_until : Date -> Vector Date -> Boolean -> Integer ! Time_Error
work_days_until self end holidays=[] include_end_date=False =
if include_end_date then self.work_days_until (end + 1.day) holidays include_end_date=False else
weekdays = week_days_between self end
self_in_epoch = Date_Time.ensure_in_epoch self
if include_end_date then self_in_epoch.work_days_until (end + 1.day) holidays include_end_date=False else
weekdays = week_days_between self_in_epoch end
## We count holidays that occurred within the period, but not on the
weekends (as weekend days have already been excluded from the count).
We also need to ensure we exclude each holiday only once, even if the
user provided it multiple times.
overlapping_holidays = holidays.filter holiday->
fits_in_range self end holiday && (is_weekend holiday).not
fits_in_range self_in_epoch end holiday && (is_weekend holiday).not
weekdays - overlapping_holidays.distinct.length

## ALIAS Date to Time
Expand Down Expand Up @@ -316,6 +331,9 @@ type Date
For the purpose of this method, the business days are defined to be
Monday through Friday.

Throws `Time_Error` if called on a Date that is before an epoch
start. See `Date_Time.epoch_start`.

This method always returns a day which is a business day - if the shift
amount is zero, the closest following business day is returned. For the
purpose of calculating the shift, the holidays are treated as if we were
Expand All @@ -342,14 +360,15 @@ type Date
Shift the date by 5 business days.

example_shift = Date.new 2020 2 3 . add_work_days 5
add_work_days : Integer -> Vector Date -> Date
add_work_days : Integer -> Vector Date -> Date ! Time_Error
add_work_days self days=1 holidays=[] = case days >= 0 of
self_in_epoch = Date_Time.ensure_in_epoch self
True ->
full_weeks = days.div 5
remaining_days = days % 5

# If the current day is a Saturday, the ordinal will be 6.
ordinal = self.day_of_week.to_integer first_day=Day_Of_Week.Monday start_at_zero=False
ordinal = self_in_epoch.day_of_week.to_integer first_day=Day_Of_Week.Monday start_at_zero=False

## If the current day is a Sunday, we just need to shift by one day
to 'escape' the weekend, regardless of the overall remaining
Expand All @@ -360,14 +379,14 @@ type Date
if ordinal + remaining_days > 5 then 2 else 0

days_to_shift = full_weeks*7 + remaining_days + additional_shift
end = self + days_to_shift.days
end = self_in_epoch + days_to_shift.days

## We have shifted the date so that weekends are taken into account,
but other holidays may have happened during that shift period.
Thus we may have shifted by less workdays than really desired. We
compute the difference and if there are still remaining workdays
to shift by, we re-run the whole shift procedure.
workdays = self.work_days_until end holidays include_end_date=False
workdays = self_in_epoch.work_days_until end holidays include_end_date=False
diff = days - workdays
if diff > 0 then @Tail_Call end.add_work_days diff holidays else
## Otherwise we have accounted for all workdays we were asked
Expand All @@ -390,7 +409,7 @@ type Date
remaining_days = (days + 1) % 5 - 1

# If the current day is a Sunday, the ordinal will be 1.
ordinal = self.day_of_week.to_integer first_day=Day_Of_Week.Sunday start_at_zero=False
ordinal = self_in_epoch.day_of_week.to_integer first_day=Day_Of_Week.Sunday start_at_zero=False

## If we overlapped the weekend, we need to increase the shift by
one day (our current shift already shifts us by one day, but we
Expand All @@ -403,8 +422,8 @@ type Date
`days_to_shift` will be negative so `end` will come _before_
`self`.
days_to_shift = full_weeks*7 + remaining_days + additional_shift
end = self + days_to_shift.days
workdays = end.work_days_until self holidays include_end_date=False
end = self_in_epoch + days_to_shift.days
workdays = end.work_days_until self_in_epoch holidays include_end_date=False

## `days` is negative but `workdays` is positive, `diff` will be
zero if we accounted for all days or negative if there are
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,27 @@ polyglot java import java.lang.ArithmeticException

polyglot java import org.enso.base.Time_Utils

## Obtains the start of the epoch for Enso.

? Start of the epoch
For Enso, start of the epoch is equal to the start of the Gregorian calendar,
which is on 15th October 1582. It is possible to create a Date_Time that is
before the start of the epoch, however, it is invalid to invoke any (Gregorian)
calendar related functionalities on such a Date_Time, e.g., `length_of_month` or
`day_of_week`. All the other operations, including `+` and `-` should succeed.

epoch_start : Date_Time
epoch_start = @Builtin_Method "Date_Time.epoch_start"

## PRIVATE
ensure_in_epoch : (Date_Time | Date) -> (Date_Time | Date) ! Time_Error
ensure_in_epoch date =
datetime = case date of
x : Date_Time -> x
x : Date.Date -> x.to_date_time
if epoch_start <= datetime then date else Error.throw Time_Error.epoch_start


## ALIAS Current Time

Obtains the current date-time from the system clock in the system timezone.
Expand All @@ -29,6 +50,7 @@ now = @Builtin_Method "Date_Time.now"
second, nanosecond and timezone.

Arguments:
- year: The year to represent, any Integer is valid.
- month: the month-of-year to represent, from 1 (January) to 12 (December)
- day: the day-of-month to represent, from 1 to 31 and must be valid for the
year and month
Expand Down Expand Up @@ -247,27 +269,33 @@ type Date_Time
zone : Time_Zone
zone self = @Builtin_Method "Date_Time.zone"

## Return the number of seconds from the Unix epoch.
## Return the number of seconds from the Enso epoch. See Date_Time.epoch_start

If this Date_Time is before an epoch start, throws `Time_Error`.

> Example
Get the current number of seconds from the Unix epoch.
Get the current number of seconds from the Enso epoch.

from Standard.Base import Date_Time

example_epoch = Date_Time.now.to_epoch_seconds
to_epoch_seconds : Integer
to_epoch_seconds self = @Builtin_Method "Date_Time.to_epoch_seconds"
to_epoch_seconds : Integer ! Time_Error
to_epoch_seconds self =
(Duration.between epoch_start (ensure_in_epoch self)).total_seconds.floor

## Return the number of milliseconds from the Unix epoch.
## Return the number of milliseconds from the Enso epoch. See Date_Time.epoch_start

If this Date_Time is before an epoch start, throws `Time_Error`.

> Example
Get the current number of milliseconds from the unix epoch.
Get the current number of milliseconds from the Enso epoch.

from Standard.Base import Date_Time

example_epoch = Date_Time.now.to_epoch_milliseconds
to_epoch_milliseconds : Integer
to_epoch_milliseconds self = @Builtin_Method "Date_Time.to_epoch_milliseconds"
to_epoch_milliseconds : Integer ! Time_Error
to_epoch_milliseconds self =
(Duration.between epoch_start (ensure_in_epoch self)).total_milliseconds.floor

## Convert this point in time to time of day, discarding the time zone
information.
Expand All @@ -283,6 +311,8 @@ type Date_Time

## Returns the number of week of year this date falls into.

Throws `Time_Error` for a Date_Time that is before epoch start.

Arguments:
- locale: the locale used to define the notion of weeks of year.
If no locale is provided, then the ISO 8601 week of year is used.
Expand All @@ -295,18 +325,23 @@ type Date_Time
other hand, the first day of the week is Monday, and week 1 is the week
containing the first Thursday of the year. Therefore it is important to
properly specify the `locale` argument.
week_of_year : (Locale.Locale | Nothing) -> Integer
week_of_year : (Locale.Locale | Nothing) -> Integer ! Time_Error
week_of_year self locale=Nothing =
if locale.is_nothing then Time_Utils.get_field_as_zoneddatetime self IsoFields.WEEK_OF_WEEK_BASED_YEAR else
Time_Utils.week_of_year_zoneddatetime self locale.java_locale
self_in_epoch = (ensure_in_epoch self)
if locale.is_nothing then Time_Utils.get_field_as_zoneddatetime self_in_epoch IsoFields.WEEK_OF_WEEK_BASED_YEAR else
Time_Utils.week_of_year_zoneddatetime self_in_epoch locale.java_locale

## Returns if the date is in a leap year.
is_leap_year : Boolean
is_leap_year self = self.date.is_leap_year

Throws `Time_Error` for a Date_Time that is before epoch start.
is_leap_year : Boolean ! Time_Error
is_leap_year self = (ensure_in_epoch self).date.is_leap_year

## Returns the number of days in the year represented by this date.
length_of_year : Integer
length_of_year self = self.date.length_of_year

Throws `Time_Error` for a Date_Time that is before epoch start.
length_of_year : Integer ! Time_Error
length_of_year self = (ensure_in_epoch self).date.length_of_year

## Returns the century of the date.
century : Integer
Expand All @@ -317,17 +352,19 @@ type Date_Time
quarter self = Time_Utils.get_field_as_zoneddatetime self IsoFields.QUARTER_OF_YEAR

## Returns the number of days in the month represented by this date.
length_of_month : Integer
length_of_month self = self.date.length_of_month

Throws `Time_Error` for a Date_Time that is before epoch start.
length_of_month : Integer ! Time_Error
length_of_month self = (ensure_in_epoch self).date.length_of_month

## Returns the day of the year.
day_of_year : Integer
day_of_year self = Time_Utils.get_field_as_zoneddatetime self ChronoField.DAY_OF_YEAR

## Returns the day of the week.
day_of_week : Day_Of_Week
day_of_week : Day_Of_Week ! Time_Error
day_of_week self =
Day_Of_Week.from (Time_Utils.get_field_as_zoneddatetime self ChronoField.DAY_OF_WEEK) Day_Of_Week.Monday
Day_Of_Week.from (Time_Utils.get_field_as_zoneddatetime (ensure_in_epoch self) ChronoField.DAY_OF_WEEK) Day_Of_Week.Monday

## Returns the first date within the `Time_Period` or `Date_Period`
containing self.
Expand Down Expand Up @@ -398,6 +435,9 @@ type Date_Time
For the purpose of this method, the business days are defined to be
Monday through Friday.

Throws `Time_Error` if called on a Date_Time that is before an epoch
start. See `Date_Time.epoch_start`.

This method always returns a day which is a business day - if the shift
amount is zero, the closest following business day is returned. For the
purpose of calculating the shift, the holidays are treated as if we were
Expand Down Expand Up @@ -426,9 +466,9 @@ type Date_Time
Shift the date by 5 business days.

example_shift = Date_Time.new 2020 2 3 11 45 . add_work_days 5
add_work_days : Integer -> Vector Date -> Date_Time
add_work_days : Integer -> Vector Date -> Date_Time ! Time_Error
add_work_days self days=1 holidays=[] =
self.date.add_work_days days holidays . to_date_time self.time_of_day self.zone
(ensure_in_epoch self).date.add_work_days days holidays . to_date_time self.time_of_day self.zone

## Subtract the specified amount of time from this instant to get a new
instant.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -761,6 +761,11 @@ type Time_Error
- error_message: The message for the error.
Time_Error_Data error_message

## PRIVATE
epoch_start : Time_Error
epoch_start = Time_Error_Data "Epoch start underflow"


## TODO Dubious constructor export
from project.Error.Common.Unsupported_File_Type import all
from project.Error.Common.Unsupported_File_Type export all
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,11 @@ public EnsoDateTime(ZonedDateTime dateTime) {
this.dateTime = dateTime;
}

@Builtin.Method(name = "epoch_start", description = "Return the Enso start of the Epoch")
public static EnsoDateTime epochStart() {
return epochStart;
}

@Builtin.Method(description = "Return current DateTime")
@CompilerDirectives.TruffleBoundary
public static EnsoDateTime now() {
Expand Down Expand Up @@ -162,18 +167,6 @@ public EnsoDateTime minus(Object durationObject, InteropLibrary interop)
return new EnsoDateTime(dateTime.minus(interop.asDuration(durationObject)));
}

@Builtin.Method(description = "Return the number of seconds from the Unix epoch.")
@CompilerDirectives.TruffleBoundary
public long toEpochSeconds() {
return dateTime.toEpochSecond();
}

@Builtin.Method(description = "Return the number of milliseconds from the Unix epoch.")
@CompilerDirectives.TruffleBoundary
public long toEpochMilliseconds() {
return dateTime.toInstant().toEpochMilli();
}

@Builtin.Method(
name = "to_localtime_builtin",
description = "Return the localtime of this date time value.")
Expand Down Expand Up @@ -264,6 +257,11 @@ public final Object toDisplayString(boolean allowSideEffects) {
return DateTimeFormatter.ISO_ZONED_DATE_TIME.format(dateTime);
}

// 15. October 1582
/** 15. October 1582 in UTC timezone. Note that Java considers an epoch start 1.1.1970 UTC. */
private static final EnsoDateTime epochStart =
EnsoDateTime.create(1582, 10, 15, 0, 0, 0, 0, EnsoTimeZone.parse("UTC"));

private static final DateTimeFormatter TIME_FORMAT =
new DateTimeFormatterBuilder()
.parseCaseInsensitive()
Expand Down
Loading

0 comments on commit c356d39

Please sign in to comment.