idris-time

A port of GHC time library to Idris.

Currently, this library supports basis functionality in terms of UTC. All the calculations have been ported from (https://hackage.haskell.org/package/time). There is a lot of functionality that is available in Haskell time library that still needs to be added to this port. Contributions are welcome!

Currently, this library has only been tested with Idris 1.3.3 (on Linux)

Examples

Calendar

*Main> :doc Gregorian
Record Gregorian

Constructor:
    MkGregorian : (year : Integer) -> (month : Int) -> (day : Int) -> Gregorian


        The function is: public export
Projections:
    year : (rec : Gregorian) -> Integer


        The function is: public export
    month : (rec : Gregorian) -> Int


        The function is: public export
    day : (rec : Gregorian) -> Int


        The function is: public export
        
*Main> :doc today
Data.DateTime.today : IO Gregorian
    Return the Gregorian date based on the call to machine's getSystemTime
    
    The function is: possibly not total due to: Data.Time.Clock.Internal.SystemTime.getSystemTime & public export
    
*Main> :exec today
2020-07-24

Time

*Main> :doc TimeOfDay 
Record TimeOfDay

Constructor:
    MkTimeOfDay : (todHour : Integer) -> (todMin : Integer) -> (todSec : Pico) -> TimeOfDay
        
        
        The function is: public export
Projections:
    todHour : (rec : TimeOfDay) -> Integer
        
        
        The function is: public export
    todMin : (rec : TimeOfDay) -> Integer
        
        
        The function is: public export
    todSec : (rec : TimeOfDay) -> Pico
        
        
        The function is: public export
        
*Main> :doc getCurrentUTCTimeOfDay 
Data.DateTime.getCurrentUTCTimeOfDay : IO TimeOfDay
    Return the current TimeOfDay based on machine's getSystemTime
    
    The function is: possibly not total due to: Data.DateTime.getUTCTime & public export
    
*Main> :exec getCurrentUTCTimeOfDay 
12:01:46

Nice to Haves/Required Improvements

• LocalTime support
• Timezone support
• More mathematical operations on Gregorian dates
• Use dependent-types to Bound Month arguments based on Month number, which is currently bound with Fin 12.
• Formatting functions
• Use specidris
• Add to elba
• A lot of functions are not total. Need more %total-ity checks.
• Support Time resolution in nanoseconds.