|
| 1 | +import LeanPython.Interpreter.Types |
| 2 | + |
| 3 | +set_option autoImplicit false |
| 4 | + |
| 5 | +namespace LeanPython.Stdlib.Datetime |
| 6 | + |
| 7 | +open LeanPython.Runtime |
| 8 | +open LeanPython.Interpreter |
| 9 | + |
| 10 | +-- ============================================================ |
| 11 | +-- timedelta method dispatch |
| 12 | +-- ============================================================ |
| 13 | + |
| 14 | +/-- Dispatch methods on datetime.timedelta instances. -/ |
| 15 | +partial def callTimedeltaMethod (iref : HeapRef) (method : String) |
| 16 | + (args : List Value) : InterpM Value := do |
| 17 | + let id_ ← heapGetInstanceData iref |
| 18 | + let days := match id_.attrs["_days"]? with |
| 19 | + | some (.int n) => n |
| 20 | + | some (.float f) => f.toUInt64.toNat |
| 21 | + | _ => 0 |
| 22 | + let seconds := match id_.attrs["_seconds"]? with |
| 23 | + | some (.int n) => n |
| 24 | + | some (.float f) => f.toUInt64.toNat |
| 25 | + | _ => 0 |
| 26 | + let microseconds := match id_.attrs["_microseconds"]? with |
| 27 | + | some (.int n) => n |
| 28 | + | _ => 0 |
| 29 | + match method with |
| 30 | + | "total_seconds" => |
| 31 | + match args with |
| 32 | + | [] => |
| 33 | + let total : Float := Float.ofInt days * 86400.0 + |
| 34 | + Float.ofInt seconds + Float.ofInt microseconds / 1000000.0 |
| 35 | + return .float total |
| 36 | + | _ => throwTypeError "total_seconds() takes no arguments" |
| 37 | + | "__str__" | "__repr__" => |
| 38 | + let totalSec := days * 86400 + seconds |
| 39 | + let h := totalSec / 3600 |
| 40 | + let m := (totalSec % 3600) / 60 |
| 41 | + let s := totalSec % 60 |
| 42 | + if days == 0 then |
| 43 | + return .str s!"{h}:{String.ofList (padLeft2 m)}{m}:{String.ofList (padLeft2 s)}{s}" |
| 44 | + else |
| 45 | + return .str s!"datetime.timedelta(days={days}, seconds={seconds})" |
| 46 | + | _ => throwAttributeError s!"'timedelta' object has no attribute '{method}'" |
| 47 | +where |
| 48 | + padLeft2 (n : Int) : List Char := |
| 49 | + if n < 10 && n >= 0 then ['0'] else [] |
| 50 | + |
| 51 | +-- ============================================================ |
| 52 | +-- datetime method dispatch |
| 53 | +-- ============================================================ |
| 54 | + |
| 55 | +/-- Dispatch methods on datetime.datetime instances. -/ |
| 56 | +partial def callDatetimeMethod (iref : HeapRef) (method : String) |
| 57 | + (_args : List Value) : InterpM Value := do |
| 58 | + let id_ ← heapGetInstanceData iref |
| 59 | + let year := match id_.attrs["_year"]? with | some (.int n) => n | _ => 1970 |
| 60 | + let month := match id_.attrs["_month"]? with | some (.int n) => n | _ => 1 |
| 61 | + let day := match id_.attrs["_day"]? with | some (.int n) => n | _ => 1 |
| 62 | + let hour := match id_.attrs["_hour"]? with | some (.int n) => n | _ => 0 |
| 63 | + let minute := match id_.attrs["_minute"]? with | some (.int n) => n | _ => 0 |
| 64 | + let second := match id_.attrs["_second"]? with | some (.int n) => n | _ => 0 |
| 65 | + match method with |
| 66 | + | "isoformat" => |
| 67 | + let sep := "T" |
| 68 | + return .str s!"{pad4 year}-{pad2 month}-{pad2 day}{sep}{pad2 hour}:{pad2 minute}:{pad2 second}" |
| 69 | + | "__str__" => |
| 70 | + return .str s!"{pad4 year}-{pad2 month}-{pad2 day} {pad2 hour}:{pad2 minute}:{pad2 second}" |
| 71 | + | "__repr__" => |
| 72 | + return .str s!"datetime.datetime({year}, {month}, {day}, {hour}, {minute}, {second})" |
| 73 | + | "year" => return .int year |
| 74 | + | "month" => return .int month |
| 75 | + | "day" => return .int day |
| 76 | + | "hour" => return .int hour |
| 77 | + | "minute" => return .int minute |
| 78 | + | "second" => return .int second |
| 79 | + | "timestamp" => |
| 80 | + -- Simplified: return seconds since epoch (very rough) |
| 81 | + let daysSinceEpoch := (year - 1970) * 365 + (month - 1) * 30 + (day - 1) |
| 82 | + let totalSec := daysSinceEpoch * 86400 + hour * 3600 + minute * 60 + second |
| 83 | + return .float (Float.ofInt totalSec) |
| 84 | + | "replace" => return .instance iref -- simplified: just return self |
| 85 | + | _ => throwAttributeError s!"'datetime' object has no attribute '{method}'" |
| 86 | +where |
| 87 | + pad2 (n : Int) : String := |
| 88 | + if n >= 0 && n < 10 then s!"0{n}" else toString n |
| 89 | + pad4 (n : Int) : String := |
| 90 | + if n >= 0 && n < 10 then s!"000{n}" |
| 91 | + else if n >= 10 && n < 100 then s!"00{n}" |
| 92 | + else if n >= 100 && n < 1000 then s!"0{n}" |
| 93 | + else toString n |
| 94 | + |
| 95 | +-- ============================================================ |
| 96 | +-- timezone method dispatch |
| 97 | +-- ============================================================ |
| 98 | + |
| 99 | +/-- Dispatch methods on datetime.timezone instances. -/ |
| 100 | +partial def callTimezoneMethod (_iref : HeapRef) (method : String) |
| 101 | + (_args : List Value) : InterpM Value := do |
| 102 | + match method with |
| 103 | + | "__str__" | "__repr__" => return .str "UTC" |
| 104 | + | "tzname" => return .str "UTC" |
| 105 | + | "utcoffset" => return .none |
| 106 | + | _ => throwAttributeError s!"'timezone' object has no attribute '{method}'" |
| 107 | + |
| 108 | +end LeanPython.Stdlib.Datetime |
0 commit comments