0 | module JS.Date
 1 |
 2 | import Data.String
 3 |
 4 | %default total
 5 |
 6 | ||| External data type for working with JS `Date` values
 7 | public export
 8 | data JSDate : Type where [external]
 9 |
10 | %foreign "javascript:lambda:(w) => new Date(Number(w))"
11 | prim__date : Bits64 -> JSDate
12 |
13 | %foreign "javascript:lambda:(w) => new Date(w)"
14 | prim__stringDate : String -> JSDate
15 |
16 | %foreign "javascript:lambda:(w) => w.toLocaleDateString()"
17 | prim__toLocaleDateString : JSDate -> String
18 |
19 | %foreign "javascript:lambda:(w) => w.toLocaleTimeString()"
20 | prim__toLocaleTimeString : JSDate -> String
21 |
22 | %foreign "javascript:lambda:(d) => BigInt(d.getTime())"
23 | prim__getTime : JSDate -> Bits64
24 |
25 | %foreign "javascript:lambda:(d) => BigInt(d.getFullYear())"
26 | prim__getFullYear : JSDate -> Bits64
27 |
28 | %foreign "javascript:lambda:(d) => BigInt(d.getMonth())"
29 | prim__getMonth : JSDate -> Bits64
30 |
31 | %foreign "javascript:lambda:(d) => BigInt(d.getDate())"
32 | prim__getDate : JSDate -> Bits64
33 |
34 | export %inline
35 | Cast Bits64 JSDate where cast = prim__date
36 |
37 | export %inline
38 | Cast String JSDate where cast = prim__stringDate
39 |
40 | export %inline
41 | toLocaleDateString : JSDate -> String
42 | toLocaleDateString = prim__toLocaleDateString
43 |
44 | export %inline
45 | toLocaleTimeString : JSDate -> String
46 | toLocaleTimeString = prim__toLocaleTimeString
47 |
48 | export %inline
49 | getTime : JSDate -> Bits64
50 | getTime = prim__getTime
51 |
52 | export %inline
53 | getFullYear : JSDate -> Bits64
54 | getFullYear = prim__getFullYear
55 |
56 | export %inline
57 | getMonth : JSDate -> Bits64
58 | getMonth = prim__getMonth
59 |
60 | export %inline
61 | getDate : JSDate -> Bits64
62 | getDate = prim__getDate
63 |
64 | pad2 : Bits64 -> String
65 | pad2 v = padLeft 2 '0' (show v)
66 |
67 | ||| Prints a date in the format "yyyy-mm-dd"
68 | export
69 | dateString : Bits64 -> String
70 | dateString ts =
71 |   let d := cast {to = JSDate} ts
72 |    in "\{show $ getFullYear d}-\{pad2 $ getMonth d + 1}-\{pad2 $ getDate d}"
73 |