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

[Zoltan Somogyi]

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.

> @@ -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)".

> +    %   - 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.

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.

> @@ -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? And what is the justification
for the difference between date_from_string and init_date?

>  :- 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 ...

> +    % seconds and microseconds.
> +    %
> +    % A duration may be positive (moving a date forward in time) or negative
> +    % (moving a date backward in time). All non-zero components must share the
> +    % same sign; a duration with a mix of positive and negative components
> +    % cannot be constructed.
> +    %
> +    % Years and months are context-dependent units whose length in absolute
> +    % time varies with the dates they are applied to. A year is treated as
> +    % 12 months, and a month is 28-31 days depending on the calendar month
> +    % and year. In contrast, days and smaller units are fixed-length:
> +    % 1 day = 86,400 seconds (leap seconds are ignored; see below).
> +    %
> +    % When adding a year or month component causes the day to fall outside
> +    % the target month, it is clamped to the last day of that month.
> +    % This applies equally to positive and negative durations. For example:
> +    %
> +    %   - Adding  1 month  to January 31  gives February 28 (29 in a leap year)
> +    %   - Adding  1 year   to February 29, 2020 gives February 28, 2021
> +    %   - Adding -1 month  to March 31    gives February 28 (29 in a leap year)
> +    %   - Adding -1 year   to February 29, 2020 gives February 28, 2019
> +    %
> +    % Note on leap seconds: although individual dates can represent times
> +    % with leap seconds (seconds 60-61), durations ignore them. A day is
> +    % always treated as exactly 86,400 seconds, even though UTC days
> +    % containing leap seconds are 86,401 seconds long.
> +    %
> +    % Durations are stored internally using four components only: months, days,
> +    % seconds and microseconds. When a duration is constructed by
> +    % init_duration/7, the seven input components are normalised into these
> +    % four.
> +    %
> +    %   - Years are converted to months and added to the months component
> +    %   - Microseconds are divided into whole seconds (which are carried over)
> +    %     and a microseconds remainder.
> +    %   - Hours, minutes, seconds, and any carried seconds are combined into a
> +    %     total number of seconds.
> +    %   - Whole days in that seconds total are carried into the days component,
> +    %     and the remainder becomes the seconds component.
> +    %
> +    % Days are never folded into months (a month does not have a fixed number
> +    % of days), and months are never folded into years during normalisation.
> +    % As a result, the duration component access functions may return values
> +    % that differ from the init_duration/7 arguments. For example:
> +    %
> +    %   - init_duration(1, 18, 0, 0, 0, 0, 0) => years = 2, months = 6
> +    %   - init_duration(0, 0, 0, 25, 0, 0, 0) => days = 1, hours = 1
>      %
>  :- type duration.

That is a very good explanation.

> @@ -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 ....".

> +    %   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.

> +    %   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.

> +    % 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.

>  :- 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 ...

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

> +    % For example, all of the following are valid:
> +    %
> +    %  - init_duration(1, 2, 15, 0, 0, 0, 0)    (all positive or zero)
> +    %  - init_duration(0, 0, -3, -12, 0, 0, 0)  (all negative or zero)
> +    %  - init_duration(0, 0, 0, 0, 0, 0, 0)     (all zero)
> +    %
> +    % But the following contain non-zero components with mixed signs and will
> +    % throw an exception:
> +    %
> +    %  - init_duration(0, 1, -5, 0, 0, 0, 0)
> +    %  - init_duration(0, 0, 0, 2, -30, 0, 0)
>      %
>      % If you need a fixed absolute time period that is independent of calendar
>      % context, then use only the days, hours, minutes, seconds and microseconds
> @@ -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

>      % 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.

> @@ -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 ...

>  :- pred duration_leq(duration::in, duration::in) is semidet.
> 
> -    % 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.

> +    % 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

The rest is fine.

Zoltan.