language-servers/erg
1
0
Fork 0
mirror of https://github.com/erg-lang/erg.git synced 2025-08-03 10:23:20 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Update datetime.d.er

Browse source
This commit is contained in:
Shunsuke Shibayama 2023-03-13 16:37:51 +09:00
parent 5a386a7481
commit bee4561275
2 changed files with 44 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

9
crates/erg_compiler/context/compare.rs
View file

@ -1068,6 +1068,15 @@ impl Context {
.try_cmp(rhs, rhs2)
.map(|ord| ord.canbe_ge())
.unwrap_or(false),
// 0..59 :> 1..20 == { I >= 0 and I < 60 } :> { I >= 1 and I < 20 }
(Pred::And(l1, r1), Pred::And(l2, r2)) => {
(self.is_super_pred_of(l1, l2) && self.is_super_pred_of(r1, r2))
|| (self.is_super_pred_of(l1, r2) && self.is_super_pred_of(r1, l2))
}
(Pred::Or(l1, r1), Pred::Or(l2, r2)) => {
(self.is_super_pred_of(l1, l2) && self.is_super_pred_of(r1, r2))
|| (self.is_super_pred_of(l1, r2) && self.is_super_pred_of(r1, l2))
}
(lhs, Pred::And(l, r)) => {
self.is_super_pred_of(lhs, l) || self.is_super_pred_of(lhs, r)
}

39
crates/erg_compiler/lib/pystd/datetime.d.er
View file

@ -6,6 +6,12 @@ time = pyimport "time"
.TimeDelta = 'timedelta': ClassType
.TimeDelta.
__call__: (days := Nat, seconds := Nat, microseconds := Nat, milliseconds := Nat, minutes := Nat, hours := Nat, weeks := Nat) -> .TimeDelta
__eq__: (self: .TimeDelta, other: .TimeDelta) -> Bool
__ne__: (self: .TimeDelta, other: .TimeDelta) -> Bool
__lt__: (self: .TimeDelta, other: .TimeDelta) -> Bool
__le__: (self: .TimeDelta, other: .TimeDelta) -> Bool
__gt__: (self: .TimeDelta, other: .TimeDelta) -> Bool
__ge__: (self: .TimeDelta, other: .TimeDelta) -> Bool
min: .TimeDelta
max: .TimeDelta
resolution: .TimeDelta
@ -13,6 +19,12 @@ time = pyimport "time"
.Date = 'date': ClassType
.Date.
__call__: (year: Nat, month: Nat, day: Nat) -> .Date
__eq__: (self: .Date, other: .Date) -> Bool
__ne__: (self: .Date, other: .Date) -> Bool
__lt__: (self: .Date, other: .Date) -> Bool
__le__: (self: .Date, other: .Date) -> Bool
__gt__: (self: .Date, other: .Date) -> Bool
__ge__: (self: .Date, other: .Date) -> Bool
fromtimestamp: (timestamp: Float) -> .Date
fromordinal: (ordinal: Nat) -> .Date
fromisoformat: (date_string: Str) -> .Date
@ -35,16 +47,28 @@ time = pyimport "time"
.TZInfo = 'tzinfo': ClassType
.Time = 'time': ClassType
.Time.
__call__: (hour: Nat, minute: Nat, second := Nat, microsecond := Nat, tzinfo := .TZInfo or NoneType) -> .Time
__call__: (hour: 0..23, minute: 0..59, second := 0..59, microsecond := Nat, tzinfo := .TZInfo or NoneType) -> .Time
__eq__: (self: .Time, other: .Time) -> Bool
__ne__: (self: .Time, other: .Time) -> Bool
__lt__: (self: .Time, other: .Time) -> Bool
__le__: (self: .Time, other: .Time) -> Bool
__gt__: (self: .Time, other: .Time) -> Bool
__ge__: (self: .Time, other: .Time) -> Bool
min: .Time
max: .Time
resolution: .TimeDelta
fromisoformat: (time_string: Str) -> .Time
replace: (self: .Time, hour := Nat, minute := Nat, second := Nat, microsecond := Nat, tzinfo := .TZInfo or NoneType) -> .Time
replace: (self: .Time, hour := 0..23, minute := 0..59, second := 0..59, microsecond := Nat, tzinfo := .TZInfo or NoneType) -> .Time
isoformat: (self: .Time, timespec := Str) -> Str
.DateTime = 'datetime': ClassType
.DateTime.
__call__: (year: Nat, month: Nat, day: Nat, hour := Nat, minute := Nat, second := Nat, microsecond := Nat, tzinfo := .TZInfo or NoneType) -> .DateTime
__call__: (year: 0..9999, month: 1..12, day: 1..31, hour := 0..23, minute := 0..59, second := 0..59, microsecond := Nat, tzinfo := .TZInfo or NoneType) -> .DateTime
__eq__: (self: .DateTime, other: .DateTime) -> Bool
__ne__: (self: .DateTime, other: .DateTime) -> Bool
__lt__: (self: .DateTime, other: .DateTime) -> Bool
__le__: (self: .DateTime, other: .DateTime) -> Bool
__gt__: (self: .DateTime, other: .DateTime) -> Bool
__ge__: (self: .DateTime, other: .DateTime) -> Bool
today!: () => .DateTime
now!: (tz := .TZInfo or NoneType) => .DateTime
utcnow!: () => .DateTime
@ -60,6 +84,13 @@ time = pyimport "time"
resolution: .TimeDelta
date: (self: .DateTime) -> .Date
time: (self: .DateTime) -> .Time
replace: (self: .DateTime, year := Nat, month := Nat, day := Nat, hour := Nat, minute := Nat, second := Nat, microsecond := Nat, tzinfo := .TZInfo or NoneType) -> .DateTime
replace: (self: .DateTime, year := 0..9999, month := 1..12, day := 1..31, hour := 0..23, minute := 0..59, second := 0..59, microsecond := Nat, tzinfo := .TZInfo or NoneType) -> .DateTime
utcoffset: (self: .DateTime) -> .TimeDelta or NoneType
.TimeZone = 'timezone': ClassType
.TimeZone.
__eq__: (self: .TimeZone, other: .TimeZone) -> Bool
__ne__: (self: .TimeZone, other: .TimeZone) -> Bool
__lt__: (self: .TimeZone, other: .TimeZone) -> Bool
__le__: (self: .TimeZone, other: .TimeZone) -> Bool
__gt__: (self: .TimeZone, other: .TimeZone) -> Bool
__ge__: (self: .TimeZone, other: .TimeZone) -> Bool