0 | module Oracle.Types.DateTime
 1 |
 2 | import Derive.Prelude
 3 |
 4 | %language ElabReflection
 5 |
 6 | public export
 7 | record OracleDate where
 8 |   constructor MkOracleDate
 9 |   year   : Int32
10 |   month  : Int32
11 |   day    : Int32
12 |   hour   : Int32
13 |   minute : Int32
14 |   second : Int32
15 |
16 | %runElab derive "OracleDate" [Eq,Ord,Show]
17 |
18 | public export
19 | record OracleTimestamp where
20 |   constructor MkOracleTimestamp
21 |   year       : Int32
22 |   month      : Int32
23 |   day        : Int32
24 |   hour       : Int32
25 |   minute     : Int32
26 |   second     : Int32
27 |   nanosecond : Int32
28 |
29 | %runElab derive "OracleTimestamp" [Eq,Ord,Show]
30 |
31 | public export
32 | OracleTimestampLTZ : Type
33 | OracleTimestampLTZ = OracleTimestamp
34 |
35 | public export
36 | record OracleTimestampTZ where
37 |   constructor MkOracleTimestampTZ
38 |   year           : Int32
39 |   month          : Int32
40 |   day            : Int32
41 |   hour           : Int32
42 |   minute         : Int32
43 |   second         : Int32
44 |   nanosecond     : Int32
45 |   tzHourOffset   : Int32
46 |   tzMinuteOffset : Int32
47 |
48 | %runElab derive "OracleTimestampTZ" [Eq,Ord,Show]
49 |
50 | public export
51 | record OracleIntervalYM where
52 |   constructor MkOracleIntervalYM
53 |   years  : Int32
54 |   months : Int32
55 |
56 | %runElab derive "OracleIntervalYM" [Eq,Ord,Show]
57 |
58 | public export
59 | record OracleIntervalDS where
60 |   constructor MkOracleIntervalDS
61 |   days        : Int32
62 |   hours       : Int32
63 |   minutes     : Int32
64 |   seconds     : Int32
65 |   nanoseconds : Int32
66 |
67 | %runElab derive "OracleIntervalDS" [Eq,Ord,Show]
68 |