refactor: format specifiers to align with Java/CLDR pattern language

src/Std/Time/Date/PlainDate.lean

@@ -334,46 +334,67 @@ def withWeekday (date : PlainDate) (desiredWeekday : Weekday) : PlainDate :=
 
   date.addDays (Day.Offset.ofInt offset.toInt)
 
+private def localizedDayOfWeek (weekday firstDay : Weekday) : Bounded.LE 0 6 :=
+  weekday.toOrdinal
+  |>.subBounds firstDay.toOrdinal
+  |>.emod 7 (by decide)
+
 /--
-Calculates the week of the year for a given date, using `firstDay` as the first day of the week.
+Returns the first day of the week-based year for the given `year`, where weeks start on `firstDay`
+and the first week must contain at least `minimalDays` days of the new year.
 -/
-def weekOfYear (date : PlainDate) (firstDay : Weekday := .monday) : Week.OfYear.Ordinal :=
-  let y := date.year
-  let posInWeek : Bounded.LE 1 7 :=
-    .ofNatWrapping ((date.weekday.toOrdinal.val - firstDay.toOrdinal.val + 7) % 7 + 1) (by decide)
-
-  let w := Bounded.LE.exact 10
-    |>.addBounds date.dayOfYear
-    |>.subBounds posInWeek
-    |>.ediv 7 (by decide)
+def startOfWeekBasedYear (year : Year.Offset) (firstDay : Weekday) (minimalDays : Bounded.LE 0 6) : PlainDate :=
+  let jan1 := PlainDate.ofYearMonthDayClip year 1 1
+  let localDay := localizedDayOfWeek jan1.weekday firstDay
+  let daysInNewYearWeek : Bounded.LE 1 7 := Bounded.LE.exact 7 |>.subBounds localDay
+  let weekStart := jan1 |>.subDays (Day.Offset.ofNat localDay.toNat)
 
-  if h : w.val < 1 then
-    (y-1).weeks |>.expandBottom (by decide)
-  else if h₁ : w.val > y.weeks.val then
-    .ofNat' 1 (by decide)
+  if daysInNewYearWeek.val >= minimalDays.val then
+    weekStart
   else
-    let h := Int.not_lt.mp h
-    let h₁ := Int.not_lt.mp h₁
-    let w := w.truncateBottom h |>.truncateTop (Int.le_trans h₁ y.weeks.property.right)
-    w
+    weekStart.addDays 7
 
 /--
-Returns the week-based year for the given `PlainDate`, using `firstDay` as the start of the week.
-The week-based year may differ from the calendar year for dates near the start or end of the year.
+Returns the week number within the week-based year for the given `PlainDate`, using `firstDay` as
+the start of the week and `minDays` as the minimum number of days required in the first week of the
+year (default 4 for ISO 8601). Dates before the first week of the calendar year are counted as part
+of the last week of the previous year.
 -/
-def weekYear (date : PlainDate) (firstDay : Weekday := .monday) : Year.Offset :=
-  let y := date.year
-  let posInWeek : Bounded.LE 1 7 :=
-    .ofNatWrapping ((date.weekday.toOrdinal.val - firstDay.toOrdinal.val + 7) % 7 + 1) (by decide)
+def weekOfYear (date : PlainDate) (firstDay : Weekday := .monday) (minDaysBounded : Bounded.LE 0 6 := .mk 4 (by decide)) : Week.OfYear.Ordinal :=
+  let year := date.year
+  let thisYearStart := startOfWeekBasedYear year firstDay minDaysBounded
 
-  let w := Bounded.LE.exact 10
-    |>.addBounds date.dayOfYear
-    |>.subBounds posInWeek
-    |>.ediv 7 (by decide)
+  if date.toEpochDay < thisYearStart.toEpochDay then
+    let prevYearStart := startOfWeekBasedYear (year - 1) firstDay minDaysBounded
+    let interval := date.toEpochDay - prevYearStart.toEpochDay
+    let interval := Bounded.LE.ofNatWrapping interval.val (by decide) (lo := 0) (hi := 370)
+    let w := interval.ediv 7 (by decide)
+    w.add 1
+  else
+    let nextYearStart := startOfWeekBasedYear (year + 1) firstDay minDaysBounded
+    if date.toEpochDay >= nextYearStart.toEpochDay then
+      1
+    else
+      let interval := date.toEpochDay - thisYearStart.toEpochDay
+      let interval := Bounded.LE.ofNatWrapping interval.val (by decide) (lo := 0) (hi := 370)
+      let w := interval.ediv 7 (by decide)
+      w.add 1
 
-  if w.val < 1 then y - 1
-  else if w.val > y.weeks.val then y + 1
-  else y
+/--
+Returns the week-based year for the given `PlainDate`, using `firstDay` as the start of the week
+and `minDays` as the minimum number of days in the first week of the year (default 4 for ISO 8601).
+-/
+def weekYear (date : PlainDate) (firstDay : Weekday := .monday) (minDays : Bounded.LE 0 6 := Bounded.LE.mk 4 (by decide)) : Year.Offset :=
+  let year := date.year
+  let thisYearStart := startOfWeekBasedYear year firstDay minDays
+  if date.toEpochDay < thisYearStart.toEpochDay then
+    year - 1
+  else
+    let nextYearStart := startOfWeekBasedYear (year + 1) firstDay minDays
+    if date.toEpochDay >= nextYearStart.toEpochDay then
+      year + 1
+    else
+      year
 
 instance : HAdd PlainDate Day.Offset PlainDate where
   hAdd := addDays

src/Std/Time/Date/Unit/Year.lean

@@ -107,8 +107,8 @@ Calculates the number of days in the specified `year`.
 -/
 def days (year : Offset) : Bounded.LE 365 366 :=
   if year.isLeap
-    then .ofNatWrapping 366 (by decide)
-    else .ofNatWrapping 355 (by decide)
+    then .mk 366 (by decide)
+    else .mk 365 (by decide)
 
 /--
 Calculates the number of weeks in the specified `year`.

src/Std/Time/DateTime.lean

@@ -14,6 +14,8 @@ public section
 namespace Std
 namespace Time
 
+open Internal
+
 /--
 Represents a date and time with timezone information.
 -/
@@ -185,19 +187,21 @@ def dayOfYear (date : DateTime) : Day.Ordinal.OfYear date.date.get.date.year.isL
   ValidDate.dayOfYear ⟨(date.date.get.date.month, date.date.get.date.day), date.date.get.date.valid⟩
 
 /--
-Determines the week of the year for the given `DateTime`, using `firstDay` as the start of the week.
+Determines the week of the year for the given `DateTime`, using `firstDay` as the start of the week
+and `minDays` as the minimum number of days a week must have in the new year to count as week 1.
 -/
 @[inline]
-def weekOfYear (date : DateTime) (firstDay : Weekday := .monday) : Week.OfYear.Ordinal :=
-  date.date.get.weekOfYear firstDay
+def weekOfYear (dt : DateTime) (firstDay : Weekday := .monday) (minDays : Bounded.LE 0 6 := Bounded.LE.mk 4 (by decide)) : Week.OfYear.Ordinal :=
+  PlainDate.weekOfYear dt.date.get.date firstDay minDays
 
 /--
-Returns the week-based year for the given `DateTime`, using `firstDay` as the start of the week.
+Returns the week-based year for the given `DateTime`, using `firstDay` as the start of the week
+and `minDays` as the minimum number of days a week must have in the new year to count as week 1.
 The week-based year may differ from the calendar year for dates near the start or end of the year.
 -/
 @[inline]
-def weekYear (date : DateTime) (firstDay : Weekday := .monday) : Year.Offset :=
-  date.date.get.weekYear firstDay
+def weekYear (date : DateTime) (firstDay : Weekday := .monday) (minDays : Bounded.LE 0 6 := Bounded.LE.mk 4 (by decide)) : Year.Offset :=
+  date.date.get.weekYear firstDay minDays
 
 /--
 Returns the aligned week of the month for a `DateTime`. Weeks are fixed 7-day slots

src/Std/Time/DateTime/PlainDateTime.lean

@@ -489,19 +489,21 @@ def inLeapYear (date : PlainDateTime) : Bool :=
   date.year.isLeap
 
 /--
-Determines the week of the year for the given `PlainDateTime`, using `firstDay` as the start of the week.
+Determines the week of the year for the given `PlainDateTime`, using `firstDay` as the start of the week
+and `minDays` as the minimum number of days a week must have in the new year to count as week 1.
 -/
 @[inline]
-def weekOfYear (date : PlainDateTime) (firstDay : Weekday := .monday) : Week.OfYear.Ordinal :=
-  date.date.weekOfYear firstDay
+def weekOfYear (date : PlainDateTime) (firstDay : Weekday := .monday) (minDays : Bounded.LE 0 6 := Bounded.LE.mk 4 (by decide)) : Week.OfYear.Ordinal :=
+  PlainDate.weekOfYear date.date firstDay minDays
 
 /--
-Returns the week-based year for the given `PlainDateTime`, using `firstDay` as the start of the week.
+Returns the week-based year for the given `PlainDateTime`, using `firstDay` as the start of the week
+and `minDays` as the minimum number of days a week must have in the new year to count as week 1.
 The week-based year may differ from the calendar year for dates near the start or end of the year.
 -/
 @[inline]
-def weekYear (date : PlainDateTime) (firstDay : Weekday := .monday) : Year.Offset :=
-  date.date.weekYear firstDay
+def weekYear (date : PlainDateTime) (firstDay : Weekday := .monday) (minDays : Bounded.LE 0 6 := Bounded.LE.mk 4 (by decide)) : Year.Offset :=
+  date.date.weekYear firstDay minDays
 
 /--
 Returns the aligned week of the month for a `PlainDateTime`. Weeks are fixed 7-day slots

src/Std/Time/Format.lean

@@ -189,15 +189,14 @@ def format (date : PlainDate) (format : String) (locale : DateFormat := .enUS) :
       | .G _ => some date.era
       | .y _ => some date.year
       | .u _ => some date.year
-      | .Y _ => some (date.weekYear locale.firstDayOfWeek)
+      | .Y _ => some (date.weekYear locale.firstDayOfWeek locale.minimalDaysInFirstWeek)
       | .D _ => some (Sigma.mk date.year.isLeap date.dayOfYear)
-      | .Qorq _ => some date.quarter
-      | .w _ => some (date.weekOfYear locale.firstDayOfWeek)
+      | .Q _ | .q _ => some date.quarter
+      | .w _ => some (date.weekOfYear locale.firstDayOfWeek locale.minimalDaysInFirstWeek)
       | .W _ => some (date.weekOfMonth locale.firstDayOfWeek)
-      | .MorL _ => some date.month
+      | .M _ | .L _ => some date.month
       | .d _ => some date.day
-      | .E _ => some date.weekday
-      | .eorc _ => some date.weekday
+      | .E _ | .e _ | .c _ => some date.weekday
       | .F _ => some date.alignedWeekOfMonth
       | _ => none
     match res with
@@ -272,6 +271,8 @@ def format (time : PlainTime) (format : String) : String :=
       | .n _ => some time.nanosecond
       | .s _ => some time.second
       | .a _ => some (HourMarker.ofOrdinal time.hour)
+      | .b _ => some (classifyDayPeriod time.hour time.minute time.second)
+      | .B _ => some (classifyExtendedDayPeriod time.hour time.minute time.second)
       | .h _ => some time.hour.toRelative
       | .K _ => some (time.hour.emod 12 (by decide))
       | .S _ => some time.nanosecond
@@ -454,22 +455,23 @@ def format (date : PlainDateTime) (format : String) (locale : DateFormat := .enU
       | .G _ => some date.era
       | .y _ => some date.year
       | .u _ => some date.year
-      | .Y _ => some (date.weekYear locale.firstDayOfWeek)
+      | .Y _ => some (date.weekYear locale.firstDayOfWeek locale.minimalDaysInFirstWeek)
       | .D _ => some (Sigma.mk date.year.isLeap date.dayOfYear)
-      | .Qorq _ => some date.quarter
-      | .w _ => some (date.weekOfYear locale.firstDayOfWeek)
+      | .Q _ | .q _ => some date.quarter
+      | .w _ => some (date.weekOfYear locale.firstDayOfWeek locale.minimalDaysInFirstWeek)
       | .W _ => some (date.weekOfMonth locale.firstDayOfWeek)
-      | .MorL _ => some date.month
+      | .M _ | .L _ => some date.month
       | .d _ => some date.day
-      | .E _ => some date.weekday
-      | .eorc _ => some date.weekday
+      | .E _ | .e _ | .c _ => some date.weekday
       | .F _ => some date.alignedWeekOfMonth
       | .H _ => some date.hour
       | .k _ => some date.hour.shiftTo1BasedHour
       | .m _ => some date.minute
       | .n _ => some date.nanosecond
       | .s _ => some date.time.second
       | .a _ => some (HourMarker.ofOrdinal date.hour)
+      | .b _ => some (classifyDayPeriod date.hour date.minute date.time.second)
+      | .B _ => some (classifyExtendedDayPeriod date.hour date.minute date.time.second)
       | .h _ => some date.hour.toRelative
       | .K _ => some (date.hour.emod 12 (by decide))
       | .S _ => some date.nanosecond