Update prelude.er

This commit is contained in:
Shunsuke Shibayama 2022-09-12 13:52:52 +09:00
parent 0704ee34d0
commit ac5c93d89b

View file

@ -1,51 +1,57 @@
@Attach NeImpl @Attach NeImpl
Eq(R |= Self) = Trait { Eq(R |= Self) = Trait {
.`==` = Self.(R) -> Bool .`==` = (self: Self, R) -> Bool
} }
NeImpl R = Patch Eq R NeImpl R = Patch Eq R
NeImpl(R).`!=`(self, other: R): Bool = not(self == other) NeImpl(R).
`!=`(self, other: R): Bool = not(self == other)
@Attach EqImpl, LeImpl, LtImpl, GeImpl, GtImpl @Attach EqImpl, LeImpl, LtImpl, GeImpl, GtImpl
PartialOrd(R |= Self) = Trait { PartialOrd(R := Self) = Trait {
.cmp = Self.(R) -> Option Ordering .cmp = (self: Self, R) -> Option Ordering
} }
Ord = Subsume PartialOrd() Ord = Subsume PartialOrd()
EqForOrd R = Patch Ord, Impl: Eq() EqForOrd R = Patch Ord, Impl := Eq()
EqForOrd(R).`==`(self, other: R): Bool = self.cmp(other) == Ordering.Equal EqForOrd(R).
`==`(self, other: R): Bool = self.cmp(other) == Ordering.Equal
LeForOrd = Patch Ord LeForOrd = Patch Ord
LeForOrd.`<=`(self, other: Self): Bool = self.cmp(other) == Ordering.Less or self == other LeForOrd.
`<=`(self, other: Self): Bool = self.cmp(other) == Ordering.Less or self == other
LtForOrd = Patch Ord LtForOrd = Patch Ord
LtForOrd.`<`(self, other: Self): Bool = self.cmp(other) == Ordering.Less LtForOrd.
`<`(self, other: Self): Bool = self.cmp(other) == Ordering.Less
GeForOrd = Patch Ord GeForOrd = Patch Ord
GeForOrd.`>=`(self, other: Self): Bool = self.cmp(other) == Ordering.Greater or self == other GeForOrd.
`>=`(self, other: Self): Bool = self.cmp(other) == Ordering.Greater or self == other
GtForOrd = Patch Ord GtForOrd = Patch Ord
GtForOrd.`>`(self, other: Self): Bool = self.cmp(other) == Ordering.Greater GtForOrd.
`>`(self, other: Self): Bool = self.cmp(other) == Ordering.Greater
Add(R |= Self) = Trait { Add(R := Self) = Trait {
.AddO = Type .Output = Type
.`_+_` = Self.(R) -> Self.AddO .`_+_` = (self: Self, R) -> Self.Output
} }
Sub(R |= Self) = Trait { Sub(R := Self) = Trait {
.SubO = Type .Output = Type
.`_-_` = Self.(R) -> Self.SubO .`_-_` = (self: Self, R) -> Self.Output
} }
Mul(R |= Self()) = Trait { Mul(R := Self()) = Trait {
.MulO = Type .Output = Type
.`*` = Self.(R) -> Self.MulO .`*` = (self: Self, R) -> Self.Output
} }
Div(R |= Self) = Trait { Div(R := Self) = Trait {
.DivO = Type .Output = Type
.`/` = Self.(R) -> Self.DivO or Panic .`/` = (self: Self, R) -> Self.Output or Panic
} }
Num: (R |= Type) -> Type Num: (R |= Type) -> Type
Num = Add and Sub and Mul Num = Add and Sub and Mul
Seq T = Trait { Seq T = Trait {
.__len__ = Ref(Self).() -> Nat .__len__ = (self: Ref(Self)) -> Nat
.get = Ref(Self).(Nat) -> T .get = (self: Ref(Self), Nat) -> T
} }
`_+_`: |R: Type, A <: Add(R)| (A, R) -> A.AddO `_+_`: |R: Type, A <: Add(R)| (A, R) -> A.AddO
@ -53,22 +59,24 @@ Seq T = Trait {
`*`: |R, O: Type, M <: Add(R)| (M, R) -> M.MulO `*`: |R, O: Type, M <: Add(R)| (M, R) -> M.MulO
`/`: |R, O: Type, D <: Add(R)| (D, R) -> D.DivO `/`: |R, O: Type, D <: Add(R)| (D, R) -> D.DivO
AddForInt = Patch Int, Impl: Add() AddForInt = Patch Int, Impl := Add()
AddForInt.AddO = Int AddForInt.AddO = Int
AddForInt.`_+_`: (self: Self).(other: Int) -> Int AddForInt.
`_+_`: (self: Self, other: Int) -> Int = magic("Add.`_+_`")
# TODO: Mul and Div # TODO: Mul and Div
NumForInterval M, N, O, P: Int = NumForInterval M, N, O, P: Int =
Patch M..N, Impl: Add(R: O..P) and Sub(R: O..P) Patch M..N, Impl := Add(R := O..P) and Sub(R := O..P)
NumForInterval(M, N, O, P).`_+_`: (self: Self, other: O..P) -> M+O..N+P NumForInterval(M, N, O, P).
NumForInterval(M, N, O, P).`_-_`: (self: Self, other: O..P) -> M-P..N-O `_+_`: (self: Self, other: O..P) -> M+O..N+P = magic("NumForInterval.`_+_`")
`_-_`: (self: Self, other: O..P) -> M-P..N-O = magic("NumForInterval.`_-_`")
Read = Trait { Read = Trait {
.read = Ref(Self).() -> Str .read = (self: Ref(Self)) -> Str
} }
Read! = Trait { Read! = Trait {
.read! = Ref!(Self).() => Str .read! = (self: Ref!(Self)) => Str
} }
Write! = Trait { Write! = Trait {
.write! = Ref!(Self).(Str) => () .write! = (self: Ref!(Self), Str) => ()
} }