Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Tuesday
// Compile with `gcc -shared time.c -o time.so `
// We only need this because there's a compiler bug that prevents using System.time in a type provider:
// https://github.com/idris-lang/Idris-dev/issues/4671
#include <time.h>
int epoch_seconds() {
return time(NULL);
}
import Data.Fin
%language TypeProviders
%dynamic "./time.so"
%default total
epoch_seconds : IO Int
epoch_seconds = foreign FFI_C "epoch_seconds" (IO Int)
getTime : IO (Provider Int)
getTime = Provide <$> epoch_seconds
%provide (Time : Int) with getTime
data Day = Mon | Tue | Wed | Thu | Fri | Sat | Sun
epochSecondsToEpochDays : Int -> Int
epochSecondsToEpochDays sec = assert_total $ sec `div` 86400
epochDayToWeekDay : (day : Int) -> Day
epochDayToWeekDay day = case assert_total (day `mod` 7) of
0 => Thu -- Start on Thu because Jan 1 1970 was...
1 => Fri
2 => Sat
3 => Sun
4 => Mon
5 => Tue
_ => Wed
Weekday : Day
Weekday = epochDayToWeekDay . epochSecondsToEpochDays $ Time
isTuesday : Weekday = Tue
isTuesday = Refl
main : IO ()
main = putStrLn "Hello, World!"
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.