0 | module IotaTime.Pattern.CalendarDateTime
 1 |
 2 | import IotaTime.Calendar
 3 | import IotaTime.Calendar.Gregorian
 4 | import IotaTime.CalendarDateTime
 5 | import IotaTime.LocalTime
 6 | import IotaTime.Pattern
 7 | import IotaTime.Pattern.Calendar
 8 | import IotaTime.Pattern.CalendarDate
 9 | import IotaTime.Pattern.LocalTime
10 |
11 | %default total
12 |
13 | ||| Combine independently typed calendar-date and local-time patterns.
14 | public export
15 | calendarDateTimePattern :
16 |   {calendar : Type} -> {auto patterned : CalendarPattern calendar} ->
17 |   Pattern dateState (CalendarDate calendar) ->
18 |   Pattern timeState LocalTime ->
19 |   Pattern (dateState, timeState) (CalendarDateTime calendar)
20 | calendarDateTimePattern = pairPattern datePart localTimeOfDay
21 |   (\date, time => on time date)
22 |
23 | ||| Sortable ISO local date-time: `yyyy-MM-ddTHH:mm:ss`.
24 | public export
25 | ps : {calendar : Type} -> {auto patterned : CalendarPattern calendar} ->
26 |   Pattern (DateFields, TimeFields) (CalendarDateTime calendar)
27 | ps = calendarDateTimePattern (pR <% char 'T') pT
28 |
29 | ||| Sortable ISO local date-time with nine fractional digits.
30 | public export
31 | po : {calendar : Type} -> {auto patterned : CalendarPattern calendar} ->
32 |   Pattern (DateFields, TimeFields) (CalendarDateTime calendar)
33 | po = calendarDateTimePattern (pR <% char 'T') pr
34 |
35 | ||| Full date with a short 12-hour local time.
36 | public export
37 | pf : {calendar : Type} -> {auto patterned : CalendarPattern calendar} ->
38 |   Pattern (DateFields, TimeFields) (CalendarDateTime calendar)
39 | pf = calendarDateTimePattern (pD <% char ' ') pt
40 |
41 | ||| Full date with a long 24-hour local time.
42 | public export
43 | pF : {calendar : Type} -> {auto patterned : CalendarPattern calendar} ->
44 |   Pattern (DateFields, TimeFields) (CalendarDateTime calendar)
45 | pF = calendarDateTimePattern (pD <% char ' ') pT
46 |
47 | ||| Short date with a short 12-hour local time.
48 | public export
49 | pg : {calendar : Type} -> {auto patterned : CalendarPattern calendar} ->
50 |   Pattern (DateFields, TimeFields) (CalendarDateTime calendar)
51 | pg = calendarDateTimePattern (pd <% char ' ') pt
52 |
53 | ||| Short date with a long 24-hour local time.
54 | public export
55 | pG : {calendar : Type} -> {auto patterned : CalendarPattern calendar} ->
56 |   Pattern (DateFields, TimeFields) (CalendarDateTime calendar)
57 | pG = calendarDateTimePattern (pd <% char ' ') pT