[m-rev.] for review: improve the documentation of the calendar module

[Julien Fischer]

Hi Zoltan,

On Fri, 13 Mar 2026 at 18:50, Zoltan Somogyi <zoltan.somogyi at runbox.com> wrote:
>
>
> On Fri, 13 Mar 2026 17:46:20 +1100, Julien Fischer <jfischer at opturion.com> wrote:
> > diff --git a/library/calendar.m b/library/calendar.m
> > index 192d8f02d..9dd627ccd 100644
> > --- a/library/calendar.m
> > +++ b/library/calendar.m
> > @@ -10,15 +10,15 @@
> >  % Main authors: maclarty
> >  % Stability: high.
> >  %
> > -% Proleptic Gregorian calendar utilities.
> > +% Proleptic Gregorian calendar utilities with date-time representation to
> > +% microsecond resolution.
> >  % The Gregorian calendar is the calendar that is currently used by most of
> >  % the world. In this calendar, a year is a leap year if it is divisible by
> > -% 4, but not divisible by 100. The only exception is if the year is divisible
> > -% by 400, in which case it is a leap year. For example, 1900 is not a leap
> > -% year, while 2000 is. The proleptic Gregorian calendar is an extension of the
> > -% Gregorian calendar backward in time to before it was first introduced in
> > -% 1582.
> > +% 400, or if it is divisible by 4 but not by 100. For example, 2000 and 2024
> > +% were leap years, while 1900 and 2023 were not. The proleptic Gregorian
> > +% calendar is an extension of the Gregorian calendar backward in time to
> > +% before it was first introduced in October 1582.
>
> I don't like either version much; will propose changes after you commit.

Feel free, although as I am actively working on this module at the moment,
could you please avoid touching the actual code.

> > @@ -120,12 +122,24 @@
> >  %---------------------%
> >
> >      % init_date(Year, Month, Day, Hour, Minute, Second, MicroSecond, Date):
> > -    % Initialize a new date. Fails if the given date is invalid.
> > +    %
> > +    % Initialise a new date from the given components. Fails if any of the
> > +    % following conditions are not met:
> > +    %
> > +    %   - Day is in the range 1..N, where N is the number of days in Month
> > +    %     of Year
> > +    %   - Hour is in the range 0..23
> > +    %   - Minute is in the range 0..59
> > +    %   - Second is in the range 0..61
>
> Add "(to account for up to two leap seconds per year)".

Done.  Note that the whole two leap second thing seems to have resulted
from a misunderstanding that crept into the C90 standard; C99 only requires
one.

> > +    %   - MicroSecond is in the range 0..999999
> > +    %
> > +    % No validation is performed on Year; years with more or fewer than
> > +    % four digits are accepted.
>
> I don't think this says anything that "This predicate accepts all X values for Year"
> does not.

On reflection, it does seem a bit pointless ;-)

> In other places, you mention that operations can *generate* negative values
> for Year, so you must specify whether you *accept* them. You can do this by
> using either "positive", "non-negative", or "" as the value of X above.

Done.

> > @@ -138,41 +152,62 @@
> >
> >  %---------------------%
> >
> > -    % Convert a string of the form "YYYY-MM-DD HH:MM:SS.mmmmmm" to a date.
> > -    % The microseconds component (.mmmmmm) is optional.
> > +    % Convert a string of the form "[-]YYYY-MM-DD HH:MM:SS.mmmmmm" to a date.
> > +    % The year must have at least four digits; years with more than four digits
> > +    % are accepted. The microseconds component (.mmmmmm) is optional. If
> > +    % present, it may have between one and six digits.
> > +    %
> > +    % Fail if the string does not conform to the above format, or if any
> > +    % date or time component is outside its valid range.
>
> What is the justification for restricting to 4+ digit years?

Good question. The short answer is I don't know.
I intend to investigate further and lift the restriction if I can't
find a reason.

> And what is the justification
> for the difference between date_from_string and init_date?

Again, I don't know.

> >  :- pred date_from_string(string::in, date::out) is semidet.
> >
> > -    % Same as above, but throws an exception if the string is not a valid date.
> > +    % As above, but throw an exception if the string is not a valid date.
> >      %
> >  :- func det_date_from_string(string) = date.
> >
> > -    % Convert a date to a string of the form "YYYY-MM-DD HH:MM:SS.mmmmmm".
> > -    % If the microseconds component of the date is zero, then the
> > -    % ".mmmmmm" part is omitted.
> > +    % Convert a date to a string of the form "[-]YYYY-MM-DD HH:MM:SS.mmmmmm".
> > +    % If the microseconds component of the date is zero, then the ".mmmmmm"
> > +    % part is omitted.
>
> ... then omit the ...

Done

...

> > @@ -226,7 +278,37 @@
> >  :- type seconds == int.
> >  :- type microseconds == int.
> >
> > -    % Functions to retrieve duration components.
> > +    % Functions to retrieve the components of a duration.
> > +    %
> > +    % Years and months are derived from the single combined months total in the
> > +    % duration:
> > +    %
> > +    %   years/1  = total months // 12
>
> The / in "years/1" is doing a completely different job from the ones in
> "months // 12". I would make this "the years function returns ....".

Done.

> > +    %   months/1 = total months rem 12
> > +    %
> > +    % Hours, minutes and seconds are derived from the single combined seconds
> > +    % total in the duration:
> > +    %
> > +    %   hours/1   = total seconds // 3600
> > +    %   minutes/1 = total seconds rem 3600 // 60
> > +    %   seconds/1 = total seconds rem 60
> > +    %   microseconds/1 = total microseconds
> > +    %
> > +    % For positive durations:
> > +    %   months/1 returns a value in 0..11
> > +    %   days/1 returns a non-negative value
>
> You *must* explicitly mention the absence of an upper limit,
> if indeed there is none.

I have changed it to say that it returns a value in 0..max_int.

> > +    %   hours/1 returns a value in 0..23
> > +    %   minutes/1 returns a value in 0..59
> > +    %   seconds/1 returns a value in 0..59
> > +    %   microseconds/1 returns a value in 0..999999
>
> The last three are immediate consequences of the above block
> (the one with //s and rems), and the first would be also, if you
> specify that any hours above 24 get carried to the days part.

Hours exceeding 24 hours carry over into the days count.
However, that occurs during construction of durations, not when
accessing their components.

I have adjusted the block above to describe days.
T the block with the return value ranges may well be a consequence
of the previous block, but unless we expect readers to go back, do the
arithmetic and arrive at those consequences, I think they are better off
stated directly.

> > +    % For negative durations:
> > +    %   months/1 returns a value in -11..0
> > +    %   days/1 returns a non-positive value
> > +    %   hours/1 returns a value in -23..0
> > +    %   minutes/1 returns a value in -59..0
> > +    %   seconds/1 returns a value in -59..0
> > +    %   microseconds/1 returns a value in -999999..0
>
> Mirror images of the my comments above.

Ditto.

> >  :- func years(duration) = years.
> >  :- func months(duration) = months.
> > @@ -239,8 +321,22 @@
> >      % init_duration(Years, Months, Days, Hours, Minutes, Seconds,
> >      %   MicroSeconds) = Duration:
> >      %
> > -    % Create a new duration. All of the components should either be
> > -    % non-negative or non-positive (they can all be zero).
> > +    % Create a new duration from the given components.
> > +    % All non-zero components must have the same sign (they must be entirely
> > +    % positive or entirely negative). An exception is thrown if two or more
> > +    % non-zero components have different signs.
>
> This function throws an exception if ...

Done.

> Also, the "or more" does not help here; there is no third sign available.

Deleted.

....

> > @@ -267,30 +363,37 @@
> >
> >      % Parse a duration string.
> >      %
> > -    % The string should be of the form "PnYnMnDTnHnMnS" where each "n" is a
> > +    % The string should be of the form "[-]PnYnMnDTnHnMnS" where each "n" is a
>
> should HAVE the form

Done.


> >      % non-negative integer representing the number of years (Y), months (M),
> >      % days (D), hours (H), minutes (M) or seconds (S).
>
> I would say explicitly that the units follow the numbers, not precede them

Done.

> > @@ -301,78 +404,73 @@
> >
> >  %---------------------%
> >
> > -    % Add a duration to a date.
> > +    % add_duration(Duration, Date0, Date):
> >      %
> > -    % First the years and months are added to the date.
> > -    % If this causes the day to be out of range (e.g. April 31), then it is
> > -    % decreased until it is in range (e.g. April 30). Next the remaining
> > -    % days, hours, minutes and seconds components are added. These could
> > -    % in turn cause the month and year components of the date to change again.
> > +    % Add Duration to Date0 to yield Date, clamping the day to the end of the
> > +    % month if the month or year component of the duration causes it to fall
> > +    % out of range.
> > +    % (See the documentation of the type duration/0 for the clamping rules.)
> >      %
> >  :- pred add_duration(duration::in, date::in, date::out) is det.
> >
> > -    % This predicate implements a partial order relation on durations.
> > -    % DurationA is less than or equal to DurationB if-and-only-if for all
> > -    % of the dates listed below, adding DurationA to the date results in a date
> > -    % less than or equal to the date obtained by adding DurationB.
> > +    % duration_leq(DurationA, DurationB):
> > +    %
> > +    % Succeed if-and-only-if DurationA is less than or equal to DurationB.
> > +    % This relation is a partial order: some pairs of durations are
> > +    % incomparable, because their relative size depends on the date they
> > +    % are applied to (e.g. 1 month vs. 30 days may compare differently
> > +    % in different months).
> > +    %
> > +    % DurationA is considered less than or equal to DurationB if adding
> > +    % DurationA to each of the following dates yields a result no later
> > +    % than adding DurationB to the same date. These dates are chosen to
> > +    % exercise leap-year and variable month-length boundaries:
> >      %
> >      %    1696-09-01 00:00:00
> >      %    1697-02-01 00:00:00
> >      %    1903-03-01 00:00:00
> >      %    1903-07-01 00:00:00
> >      %
> > -    % There is only a partial order on durations, because some durations
> > -    % cannot be said to be less than, equal to or greater than another duration
> > -    % (e.g. 1 month vs. 30 days).
> > +    % The predicate fails if DurationA is greater than DurationB for any
> > +    % of the above dates, including the case where the two durations are
> > +    % incomparable (i.e. DurationA yields an earlier result for some test
> > +    % dates but a later result for others).
>
> They exercise leap-year and month-length boundaries, but do they exercise
> all possible combinations of those boundaries? The fact that there are four dates
> seems promising, since there leap/nonleap and 28/29 days for feb also has
> four combinations, but without an explicit promise, and preferably a correctness
> argument, I would not want to rely on just that fact ...

The duration leq algorithm was taken from the XML schema specification
that Ian based this module on.
The implementation of the predicate duration_leq has a pointer
to the relevant spot: <https://www.w3.org/TR/xmlschema-2/#duration>

For further details about *why* those four dates, see:
<https://www.unicode.org/L2/L2001/01043-time-intervals.html#Distinguished_DateTimes>

(I don't think the user-facing documentation needs to go into that much detail.)

...

> > -    % Get the difference between local and UTC time as a duration.
> > +    % local_time_offset(Offset, !IO):
> >      %
> > -    % local_time_offset(TZ, !IO) is equivalent to:
> > -    %   current_local_time(Local, !IO),
> > -    %   current_utc_time(UTC, !IO),
> > -    %   TZ = duration(UTC, Local)
> > -    % except that it is as if the calls to current_utc_time and
> > -    % current_local_time occurred at the same instant.
> > +    % Offset is the difference between local and UTC time, that is, the
> > +    % value of duration(UTC, Local), where Local and UTC are the local and UTC
> > +    % representations of the same point in time.
> >      %
> > -    % To convert UTC time to local time, add the result of local_time_offset/3
> > -    % to UTC (using add_duration/3). To compute UTC given the local time,
> > -    % first negate the result of local_time_offset/3 (using negate/1) and then
> > -    % add it to the local time.
> > +    % To convert UTC time to local time, add Offset to UTC using
> > +    % add_duration/3. To convert local time to UTC, negate Offset using
> > +    % negate/1 and add the result to the local time.
>
> You probably want to explicitly mention that Offset will vary with Daylight
> Savings time.

I have added:

    Offset reflects the system's current daylight savings state at the time of
    the call.

> > +    % duration(DateA, DateB) = Duration:
> > +    %
> > +    % Return the duration from DateA to DateB using a greedy algorithm that
> > +    % maximises each component in this order: years, months, days, hours,
> > +    % minutes, seconds, microseconds. The result is positive if DateB is after
> > +    % DateA and negative if DateB is before DateA. Leap seconds are ignored.
> > +    %
> > +    % The dates should be in the same timezone and daylight savings phase;
> > +    % to find the duration between dates in different timezones or daylight
> > +    % savings phases, first convert them to UTC.
>
> convert them BOTH

Done.

> The rest is fine.

Thanks for the review.

Julien.