feat: add Locale and LocaleSymbols for configurable date/time formatting

src/Std/Time/Date/PlainDate.lean

@@ -310,10 +310,10 @@ Determines the week of the month for the given `PlainDate`. The week of the mont
 on the day of the month and the weekday. Each week starts on Monday because the entire library is
 based on the Gregorian Calendar.
 -/
-def alignedWeekOfMonth (date : PlainDate) : Week.Ordinal.OfMonth :=
-  let weekday := date.withDaysClip 1 |>.weekday |>.toOrdinal |>.sub 1
-  let days := date.day |>.sub 1 |>.addBounds weekday
-  days |>.ediv 7 (by decide) |>.add 1
+def alignedWeekOfMonth (date : PlainDate) (firstDay : Weekday := .monday) : Week.Ordinal.OfMonth :=
+  let day1Ord := (date.withDaysClip 1).weekday.toOrdinal.val
+  let offset := (day1Ord - firstDay.toOrdinal.val + 7) % 7
+  Bounded.LE.ofNatWrapping ((date.day.val - 1 + offset) / 7 + 1) (by decide)
 
 /--
 Sets the date to the specified `desiredWeekday`. If the `desiredWeekday` is the same as the current weekday,
@@ -335,14 +335,16 @@ def withWeekday (date : PlainDate) (desiredWeekday : Weekday) : PlainDate :=
   date.addDays (Day.Offset.ofInt offset.toInt)
 
 /--
-Calculates the week of the year starting Monday for a given year.
+Calculates the week of the year for a given date, using `firstDay` as the first day of the week.
 -/
-def weekOfYear (date : PlainDate) : Week.Ordinal :=
+def weekOfYear (date : PlainDate) (firstDay : Weekday := .monday) : Week.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 date.weekday.toOrdinal
+    |>.subBounds posInWeek
     |>.ediv 7 (by decide)
 
   if h : w.val < 1 then
@@ -355,6 +357,24 @@ def weekOfYear (date : PlainDate) : Week.Ordinal :=
     let w := w.truncateBottom h |>.truncateTop (Int.le_trans h₁ y.weeks.property.right)
     w
 
+/--
+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.
+-/
+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)
+
+  let w := Bounded.LE.exact 10
+    |>.addBounds date.dayOfYear
+    |>.subBounds posInWeek
+    |>.ediv 7 (by decide)
+
+  if w.val < 1 then y - 1
+  else if w.val > y.weeks.val then y + 1
+  else y
+
 instance : HAdd PlainDate Day.Offset PlainDate where
   hAdd := addDays
 

src/Std/Time/DateTime/PlainDateTime.lean

@@ -489,11 +489,19 @@ def inLeapYear (date : PlainDateTime) : Bool :=
   date.year.isLeap
 
 /--
-Determines the week of the year for the given `PlainDateTime`.
+Determines the week of the year for the given `PlainDateTime`, using `firstDay` as the start of the week.
 -/
 @[inline]
-def weekOfYear (date : PlainDateTime) : Week.Ordinal :=
-  date.date.weekOfYear
+def weekOfYear (date : PlainDateTime) (firstDay : Weekday := .monday) : Week.Ordinal :=
+  date.date.weekOfYear firstDay
+
+/--
+Returns the week-based year for the given `PlainDateTime`, 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.
+-/
+@[inline]
+def weekYear (date : PlainDateTime) (firstDay : Weekday := .monday) : Year.Offset :=
+  date.date.weekYear firstDay
 
 /--
 Returns the unaligned week of the month for a `PlainDateTime` (day divided by 7, plus 1).
@@ -502,13 +510,11 @@ def weekOfMonth (date : PlainDateTime) : Bounded.LE 1 5 :=
   date.date.weekOfMonth
 
 /--
-Determines the week of the month for the given `PlainDateTime`. The week of the month is calculated based
-on the day of the month and the weekday. Each week starts on Monday because the entire library is
-based on the Gregorian Calendar.
+Determines the week of the month for the given `PlainDateTime`, using `firstDay` as the start of the week.
 -/
 @[inline]
-def alignedWeekOfMonth (date : PlainDateTime) : Week.Ordinal.OfMonth :=
-  date.date.alignedWeekOfMonth
+def alignedWeekOfMonth (date : PlainDateTime) (firstDay : Weekday := .monday) : Week.Ordinal.OfMonth :=
+  date.date.alignedWeekOfMonth firstDay
 
 /--
 Transforms a tuple of a `PlainDateTime` into a `Day.Ordinal.OfYear`.

src/Std/Time/Format.lean

@@ -178,9 +178,9 @@ end TimeZone
 namespace PlainDate
 
 /--
-Formats a `PlainDate` using a specific format.
+Formats a `PlainDate` using a specific format and locale.
 -/
-def format (date : PlainDate) (format : String) : String :=
+def format (date : PlainDate) (format : String) (locale : Locale := .enUS) : String :=
   let format : Except String (GenericFormat .any) := GenericFormat.spec format
   match format with
   | .error err => s!"error: {err}"
@@ -189,10 +189,11 @@ def format (date : PlainDate) (format : String) : String :=
       | .G _ => some date.era
       | .y _ => some date.year
       | .u _ => some date.year
+      | .Y _ => some (date.weekYear locale.firstDayOfWeek)
       | .D _ => some (Sigma.mk date.year.isLeap date.dayOfYear)
       | .Qorq _ => some date.quarter
-      | .w _ => some date.weekOfYear
-      | .W _ => some date.alignedWeekOfMonth
+      | .w _ => some (date.weekOfYear locale.firstDayOfWeek)
+      | .W _ => some (date.alignedWeekOfMonth locale.firstDayOfWeek)
       | .MorL _ => some date.month
       | .d _ => some date.day
       | .E _ => some date.weekday
@@ -442,9 +443,9 @@ end ZonedDateTime
 namespace PlainDateTime
 
 /--
-Formats a `PlainDateTime` using a specific format.
+Formats a `PlainDateTime` using a specific format and locale.
 -/
-def format (date : PlainDateTime) (format : String) : String :=
+def format (date : PlainDateTime) (format : String) (locale : Locale := .enUS) : String :=
   let format : Except String (GenericFormat .any) := GenericFormat.spec format
   match format with
   | .error err => s!"error: {err}"
@@ -453,10 +454,11 @@ def format (date : PlainDateTime) (format : String) : String :=
       | .G _ => some date.era
       | .y _ => some date.year
       | .u _ => some date.year
+      | .Y _ => some (date.weekYear locale.firstDayOfWeek)
       | .D _ => some (Sigma.mk date.year.isLeap date.dayOfYear)
       | .Qorq _ => some date.quarter
-      | .w _ => some date.weekOfYear
-      | .W _ => some date.alignedWeekOfMonth
+      | .w _ => some (date.weekOfYear locale.firstDayOfWeek)
+      | .W _ => some (date.alignedWeekOfMonth locale.firstDayOfWeek)
       | .MorL _ => some date.month
       | .d _ => some date.day
       | .E _ => some date.weekday