Tuesday

time.c

// 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);
}

Tuesday.idr

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!"