miscelleaneous

Random Lean experiments

  1. 1
  2. 2
  3. 3
  4. 4
  5. 5
  6. 6
  7. 7
  8. 8
  9. 9
  10. 10
  11. 11
  12. 12
  13. 13
  14. 14
  15. 15
  16. 16
  17. 17
  18. 18
  19. 19
  20. 20
  21. 21
  22. 22
  23. 23
  24. 24
  25. 25
  26. 26
  27. 27
  28. 28
  29. 29
  30. 30
  31. 31
  32. 32
  33. 33
  34. 34
  35. 35
  36. 36
  37. 37
  38. 38
  39. 39
  40. 40
  41. 41
  42. 42
  43. 43
  44. 44
  45. 45
  46. 46
  47. 47
  48. 48
  49. 49
  50. 50
  51. 51
  52. 52
  53. 53
  54. 54
  55. 55
  56. 56
  57. 57
  58. 58
  59. 59
  60. 60
  61. 61
  62. 62
  63. 63
  64. 64
  65. 65
  66. 66
  67. 67
import Std.Time
open Std.Time

def parse_csv filename (parse_row : List String  Option α) := do
  return ( IO.FS.lines filename) |>.map (fun (l : String) 
    l.replace "\\," "\n"
      |>.split ","
      |>.toList
      |>.map fun (s : String.Slice)  s.replace "\n" ",")
    |>.filterMap parse_row

instance : LT (DateTime TimeZone.UTC) := ltOfOrd
instance : LE PlainDate := leOfOrd

def main (args : List String) := do
  let lines  parse_csv args[1]! fun l  match l with
    | [a, b, c] =>
      match ZonedDateTime.fromISO8601String b with
      | .ok b => some (b.toDateTime.convertTimeZone TimeZone.UTC, ZonedDateTime.fromISO8601String c
        |>.toOption.getD zoned("3000-01-01T00:00:00-00:00")
        |>.toDateTime.convertTimeZone TimeZone.UTC)
      | _ => none
    | _ => none
  -- Must be LT not LE!
  let sorted_starts := lines.qsort (·.1 < ·.1)
  let sorted_ends := lines.qsort (·.2 < ·.2)
  IO.println <| sorted_ends.map Prod.snd
  let start_date := date("2025-03-01")
  let mut date := start_date
  let cur_date  Std.Time.PlainDate.now
  let mut i := 0
  let mut j := 0
  let mut total := 0
  let mut log_size := 0
  let mut daily := #[]
  while date  cur_date do
    while if h : i < sorted_starts.size then sorted_starts[i].1.toPlainDate  date else false do
      log_size := log_size + 1
      total := total + 1
      i := i + 1
    let mut cnt := 0
    while if h : j < sorted_ends.size then sorted_ends[j].2.toPlainDate  date else false do
      log_size := log_size - 1
      j := j + 1
      cnt := cnt + 1
    daily := daily.push cnt
    IO.println s!"{date}{List.replicate (log_size / 3) " " |> "".intercalate}|{List.replicate (total / 3 - log_size / 3) " " |> "".intercalate}|"
    date := date.addDays 1
  let m := daily.toList.max?.getD 0
  let colors := [" ", "", "", "", ""]
  i := 0
  date := start_date
  for h : cnt in daily do
    if i % 7 = 0 then
      if i > 0 then IO.println ""
      IO.print s!"{date} "
      date := date.addDays 7
    IO.print <| colors[if cnt = 0 then 0 else 4 * (cnt - 1) / m + 1]'(by
      by_cases h : cnt = 0
      · grind
      · simp [h]
        have : cnt  m := List.le_max?_getD_of_mem (by grind)
        suffices 4 * (cnt - 1) / m < 4 by grind
        apply Nat.div_lt_iff_lt_mul (by grind) |>.mpr
        grind)
    i := i + 1
  IO.println ""