mirror of
https://github.com/erg-lang/erg.git
synced 2025-09-29 20:34:44 +00:00
Merge branch 'main' into pr/212
This commit is contained in:
Shunsuke Shibayama
commit
a4d5b09df9
14 changed files with 242 additions and 114 deletions
|
|
@ -753,6 +753,9 @@ impl PyCodeGenerator {
|
|||
}
|
||||
|
||||
fn cancel_if_pop_top(&mut self) {
|
||||
if self.cur_block_codeobj().code.len() < 2 {
|
||||
return;
|
||||
}
|
||||
let lasop_t_idx = self.cur_block_codeobj().code.len() - 2;
|
||||
if self.cur_block_codeobj().code.get(lasop_t_idx) == Some(&(POP_TOP as u8)) {
|
||||
self.mut_cur_block_codeobj().code.pop();
|
||||
|
|
@ -1495,7 +1498,7 @@ impl PyCodeGenerator {
|
|||
} else {
|
||||
// no else block
|
||||
let idx_end = if self.py_version.minor >= Some(11) {
|
||||
self.lasti() - idx_pop_jump_if_false
|
||||
self.lasti() - idx_pop_jump_if_false - 1
|
||||
} else {
|
||||
self.lasti()
|
||||
};
|
||||
|
|
@ -2376,14 +2379,15 @@ impl PyCodeGenerator {
|
|||
log!(info "entered {}", fn_name!());
|
||||
let line = sig.ln_begin().unwrap();
|
||||
let class_name = sig.ident().inspect();
|
||||
let ident = Identifier::public_with_line(DOT, Str::ever("__init__"), line);
|
||||
let mut ident = Identifier::public_with_line(DOT, Str::ever("__init__"), line);
|
||||
ident.vi.t = __new__.clone();
|
||||
let param_name = fresh_varname();
|
||||
let param = VarName::from_str_and_line(Str::from(param_name.clone()), line);
|
||||
let param = NonDefaultParamSignature::new(ParamPattern::VarName(param), None);
|
||||
let self_param = VarName::from_str_and_line(Str::ever("self"), line);
|
||||
let self_param = NonDefaultParamSignature::new(ParamPattern::VarName(self_param), None);
|
||||
let params = Params::new(vec![self_param, param], None, vec![], None);
|
||||
let subr_sig = SubrSignature::new(ident, params, __new__.clone());
|
||||
let subr_sig = SubrSignature::new(ident, params);
|
||||
let mut attrs = vec![];
|
||||
match __new__.non_default_params().unwrap()[0].typ() {
|
||||
// namedtupleは仕様上::xなどの名前を使えない
|
||||
|
|
@ -2431,11 +2435,12 @@ impl PyCodeGenerator {
|
|||
log!(info "entered {}", fn_name!());
|
||||
let class_ident = sig.ident();
|
||||
let line = sig.ln_begin().unwrap();
|
||||
let ident = Identifier::public_with_line(DOT, Str::ever("new"), line);
|
||||
let mut ident = Identifier::public_with_line(DOT, Str::ever("new"), line);
|
||||
ident.vi.t = __new__;
|
||||
let param_name = fresh_varname();
|
||||
let param = VarName::from_str_and_line(Str::from(param_name.clone()), line);
|
||||
let param = NonDefaultParamSignature::new(ParamPattern::VarName(param), None);
|
||||
let sig = SubrSignature::new(ident, Params::new(vec![param], None, vec![], None), __new__);
|
||||
let sig = SubrSignature::new(ident, Params::new(vec![param], None, vec![], None));
|
||||
let arg = PosArg::new(Expr::Accessor(Accessor::private_with_line(
|
||||
Str::from(param_name),
|
||||
line,
|
||||
|
|
|
|||
|
|
@ -3,7 +3,7 @@ use std::option::Option; // conflicting to Type::Option
|
|||
|
||||
use erg_common::error::MultiErrorDisplay;
|
||||
|
||||
use crate::ty::constructors::{and, or};
|
||||
use crate::ty::constructors::{and, or, poly};
|
||||
use crate::ty::free::fresh_varname;
|
||||
use crate::ty::free::{Constraint, FreeKind};
|
||||
use crate::ty::typaram::{OpKind, TyParam, TyParamOrdering};
|
||||
|
|
@ -848,6 +848,35 @@ impl Context {
|
|||
let t = self.into_refinement(t.clone());
|
||||
Type::Refinement(self.union_refinement(&t, r))
|
||||
}
|
||||
// Array({1, 2}, 2), Array({3, 4}, 2) ==> Array({1, 2, 3, 4}, 2)
|
||||
(
|
||||
Type::Poly {
|
||||
name: ln,
|
||||
params: lps,
|
||||
},
|
||||
Type::Poly {
|
||||
name: rn,
|
||||
params: rps,
|
||||
},
|
||||
) if ln == rn => {
|
||||
debug_assert_eq!(lps.len(), rps.len());
|
||||
let mut unified_params = vec![];
|
||||
for (lp, rp) in lps.iter().zip(rps.iter()) {
|
||||
match (lp, rp) {
|
||||
(TyParam::Type(l), TyParam::Type(r)) => {
|
||||
unified_params.push(TyParam::t(self.union(l, r)))
|
||||
}
|
||||
(_, _) => {
|
||||
if self.eq_tp(lp, rp) {
|
||||
unified_params.push(lp.clone());
|
||||
} else {
|
||||
return or(lhs.clone(), rhs.clone());
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
poly(ln, unified_params)
|
||||
}
|
||||
(l, r) => or(l.clone(), r.clone()),
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -686,8 +686,11 @@ impl Context {
|
|||
self.deref_tyvar(mem::take(var.ref_mut_t()), Covariant, var.loc())?;
|
||||
}
|
||||
hir::Signature::Subr(subr) => {
|
||||
subr.t =
|
||||
self.deref_tyvar(mem::take(&mut subr.t), Covariant, subr.loc())?;
|
||||
*subr.ref_mut_t() = self.deref_tyvar(
|
||||
mem::take(subr.ref_mut_t()),
|
||||
Covariant,
|
||||
subr.loc(),
|
||||
)?;
|
||||
}
|
||||
}
|
||||
for chunk in attr.body.block.iter_mut() {
|
||||
|
|
@ -738,8 +741,11 @@ impl Context {
|
|||
self.deref_tyvar(mem::take(var.ref_mut_t()), Covariant, var.loc())?;
|
||||
}
|
||||
hir::Signature::Subr(subr) => {
|
||||
subr.t =
|
||||
self.deref_tyvar(mem::take(&mut subr.t), Covariant, subr.loc())?;
|
||||
*subr.ref_mut_t() = self.deref_tyvar(
|
||||
mem::take(subr.ref_mut_t()),
|
||||
Covariant,
|
||||
subr.loc(),
|
||||
)?;
|
||||
}
|
||||
}
|
||||
for chunk in def.body.block.iter_mut() {
|
||||
|
|
|
|||
|
|
@ -437,6 +437,11 @@ impl Identifier {
|
|||
self.name.inspect()
|
||||
}
|
||||
|
||||
/// show dot + name (no qual_name & type)
|
||||
pub fn show(&self) -> String {
|
||||
format!("{}{}", fmt_option!(self.dot), self.name)
|
||||
}
|
||||
|
||||
pub fn is_procedural(&self) -> bool {
|
||||
self.name.is_procedural()
|
||||
}
|
||||
|
|
@ -1366,22 +1371,45 @@ impl Params {
|
|||
pub struct SubrSignature {
|
||||
pub ident: Identifier,
|
||||
pub params: Params,
|
||||
pub t: Type,
|
||||
}
|
||||
|
||||
impl NestedDisplay for SubrSignature {
|
||||
fn fmt_nest(&self, f: &mut fmt::Formatter<'_>, _level: usize) -> fmt::Result {
|
||||
write!(f, "{}{} (: {})", self.ident, self.params, self.t,)
|
||||
write!(
|
||||
f,
|
||||
"{}{} (: {})",
|
||||
self.ident.show(),
|
||||
self.params,
|
||||
self.ident.t()
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
impl_display_from_nested!(SubrSignature);
|
||||
impl_locational!(SubrSignature, ident, params);
|
||||
impl_t!(SubrSignature);
|
||||
|
||||
impl HasType for SubrSignature {
|
||||
#[inline]
|
||||
fn ref_t(&self) -> &Type {
|
||||
self.ident.ref_t()
|
||||
}
|
||||
#[inline]
|
||||
fn ref_mut_t(&mut self) -> &mut Type {
|
||||
self.ident.ref_mut_t()
|
||||
}
|
||||
#[inline]
|
||||
fn signature_t(&self) -> Option<&Type> {
|
||||
self.ident.signature_t()
|
||||
}
|
||||
#[inline]
|
||||
fn signature_mut_t(&mut self) -> Option<&mut Type> {
|
||||
self.ident.signature_mut_t()
|
||||
}
|
||||
}
|
||||
|
||||
impl SubrSignature {
|
||||
pub const fn new(ident: Identifier, params: Params, t: Type) -> Self {
|
||||
Self { ident, params, t }
|
||||
pub const fn new(ident: Identifier, params: Params) -> Self {
|
||||
Self { ident, params }
|
||||
}
|
||||
|
||||
pub fn is_procedural(&self) -> bool {
|
||||
|
|
|
|||
|
|
@ -988,8 +988,9 @@ impl ASTLowerer {
|
|||
id,
|
||||
found_body_t,
|
||||
)?;
|
||||
let ident = hir::Identifier::bare(sig.ident.dot, sig.ident.name);
|
||||
let sig = hir::SubrSignature::new(ident, params, t);
|
||||
let mut ident = hir::Identifier::bare(sig.ident.dot, sig.ident.name);
|
||||
ident.vi.t = t;
|
||||
let sig = hir::SubrSignature::new(ident, params);
|
||||
let body = hir::DefBody::new(body.op, block, body.id);
|
||||
Ok(hir::Def::new(hir::Signature::Subr(sig), body))
|
||||
}
|
||||
|
|
@ -1019,7 +1020,7 @@ impl ASTLowerer {
|
|||
);
|
||||
let block = self.lower_block(body.block)?;
|
||||
let ident = hir::Identifier::bare(sig.ident.dot, sig.ident.name);
|
||||
let sig = hir::SubrSignature::new(ident, params, Type::Failure);
|
||||
let sig = hir::SubrSignature::new(ident, params);
|
||||
let body = hir::DefBody::new(body.op, block, body.id);
|
||||
Ok(hir::Def::new(hir::Signature::Subr(sig), body))
|
||||
}
|
||||
|
|
|
|||
|
|
@ -273,7 +273,14 @@ impl Parser {
|
|||
chunks.push(expr);
|
||||
}
|
||||
}
|
||||
None => switch_unreachable!(),
|
||||
None => {
|
||||
if !self.errs.is_empty() {
|
||||
self.level -= 1;
|
||||
return Err(());
|
||||
} else {
|
||||
switch_unreachable!()
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
self.level -= 1;
|
||||
|
|
|
|||
|
|
@ -29,14 +29,27 @@ That is, expressions such as `X**2 - 5X + 6 == 0` cannot be used as refinement-t
|
|||
If you know how to solve quadratic equations, you would expect the above refinement form to be equivalent to `{2, 3}`.
|
||||
However, the Erg compiler has very little knowledge of algebra, so it cannot solve the predicate on the right.
|
||||
|
||||
## Subtyping rules for refinement types
|
||||
|
||||
All refinement types are subtypes of the type specified in the `Type` part.
|
||||
|
||||
```erg
|
||||
{I: Int | I <= 0} <: Int
|
||||
```
|
||||
|
||||
Otherwise, the current Erg has a subtyping type rule for integer comparisons.
|
||||
|
||||
```erg
|
||||
{I: Int | I <= 5} <: {I: Int | I <= 0}
|
||||
```
|
||||
|
||||
## Smart Cast
|
||||
|
||||
It's nice that you defined `Odd`, but as it is, it doesn't look like it can be used much outside of literals. To promote an odd number in a normal `Int` object to `Odd`, i.e., to downcast an `Int` to `Odd`, you need to pass the constructor of `Odd`.
|
||||
For refinement types, the normal constructor `.new` may panic, and there is an auxiliary constructor called `.try_new` that returns a `Result` type.
|
||||
|
||||
```python
|
||||
i = Odd.new (0..10).sample!()
|
||||
i: Odd # or Panic
|
||||
i = Odd.new (0..10).sample!() # i: Odd (or Panic)
|
||||
```
|
||||
|
||||
It can also be used as a type specification in `match`.
|
||||
|
|
|
|||
|
|
@ -2,6 +2,8 @@
|
|||
|
||||
[](https://gezf7g7pd5.execute-api.ap-northeast-1.amazonaws.com/default/source_up_to_date?owner=erg-lang&repos=erg&ref=main&path=doc/EN/API/funcs.md&commit_hash=06f8edc9e2c0cee34f6396fd7c64ec834ffb5352)
|
||||
|
||||
> __Note__: `match`は関数ではなく特殊形式です。
|
||||
|
||||
## 基本関数
|
||||
|
||||
### if|T; U|(cond: Bool, then: T, else: U) -> T or U
|
||||
|
|
|
|||
|
|
@ -53,46 +53,21 @@ if True, do:
|
|||
|
||||
無名プロシージャ、プロシージャ型を生成する。
|
||||
|
||||
## `:`(subject, T)
|
||||
|
||||
subjectがTに合致しているか判定する。合致していない場合はコンパイルエラーを送出する。
|
||||
|
||||
```python
|
||||
a: Int
|
||||
f x: Int, y: Int = x / y
|
||||
```
|
||||
|
||||
また、`:`適用スタイルにも使われる。
|
||||
|
||||
```python
|
||||
f x:
|
||||
y
|
||||
z
|
||||
```
|
||||
|
||||
`:`も`=`と同じく演算の結果が未定義である。
|
||||
|
||||
```python
|
||||
_ = x: Int # SyntaxError:
|
||||
print!(x: Int) # SyntaxError:
|
||||
```
|
||||
|
||||
## `.`(obj, attr)
|
||||
|
||||
objの属性を読み込む。
|
||||
`x.[y, z]`とすると、xのyとzという属性を配列にして返す。
|
||||
|
||||
## `|>`(obj, c: Callable)
|
||||
|
||||
`c(obj)`を実行する。`x + y |>.foo()`は`(x + y).foo()`と同じ。
|
||||
|
||||
### (x: Option T)`?` -> T | T
|
||||
### (x: Option T)`?` -> T
|
||||
|
||||
後置演算子。`x.unwrap()`を呼び出し、エラーの場合はその場で`return`する。
|
||||
|
||||
## match(obj, ...lambdas: Lambda)
|
||||
## match(obj, ...arms: Lambda)
|
||||
|
||||
objについて、パターンにマッチしたlambdaを実行する。
|
||||
objについて、パターンにマッチしたarmを実行する。armは無名関数でなくてはならない。
|
||||
|
||||
```python
|
||||
match [1, 2, 3]:
|
||||
|
|
@ -102,15 +77,25 @@ match [1, 2, 3]:
|
|||
# (1, 2, 3)
|
||||
```
|
||||
|
||||
## del(x: ...T) -> NoneType | T
|
||||
型指定によって処理を分岐できるが、型推論の結果は分岐に影響しない。
|
||||
|
||||
```python
|
||||
zero: {0} -> {0}
|
||||
one: {1} -> {1}
|
||||
_ = match x:
|
||||
i -> zero i
|
||||
j -> one j # Warning: cannot reach this arm
|
||||
```
|
||||
|
||||
## Del(x: ...T) -> NoneType
|
||||
|
||||
変数`x`を削除する。ただし組み込みのオブジェクトは削除できない。
|
||||
|
||||
```python
|
||||
a = 1
|
||||
del a # OK
|
||||
Del a # OK
|
||||
|
||||
del True # SyntaxError: cannot delete a built-in object
|
||||
Del True # SyntaxError: cannot delete a built-in object
|
||||
```
|
||||
|
||||
## do(body: Body) -> Func
|
||||
|
|
@ -149,7 +134,7 @@ assert True.then(choice) == 1
|
|||
|
||||
### `{}`(layout, ...names, ...preds)
|
||||
|
||||
篩型、ランク2型を生成する。
|
||||
篩型を生成する。
|
||||
|
||||
### `...`
|
||||
|
||||
|
|
@ -169,10 +154,10 @@ assert {x; ...yz} == {x = 1; y = 2; z = 3}
|
|||
|
||||
ユーザーが直接使用できない演算子です。
|
||||
|
||||
### ref(x: T) -> Ref T | T
|
||||
### ref(x: T) -> Ref T
|
||||
|
||||
オブジェクトの不変参照を返す。
|
||||
|
||||
### ref!(x: T!) -> Ref! T! | T!
|
||||
### ref!(x: T!) -> Ref! T!
|
||||
|
||||
可変オブジェクトの可変参照を返す。
|
||||
|
|
|
|||
|
|
@ -8,13 +8,13 @@
|
|||
|
||||
基本的に、すべてのパターンは「平坦化」される。具体的には、
|
||||
|
||||
```
|
||||
```erg
|
||||
[i, [j, k]] -> ...
|
||||
```
|
||||
|
||||
は、
|
||||
|
||||
```
|
||||
```erg
|
||||
%1 ->
|
||||
i = %1[0]
|
||||
%2 = %1[1]
|
||||
|
|
@ -46,7 +46,7 @@ Typeが篩型(e.g. `{I: Int | I >= 0}`)の場合は、中の述語式を評価
|
|||
|
||||
`F(X)`型の検査を考える。定義が`F(A <-> E) = ...`(`E`中に現れる`Self`はオブジェクト自身に置換される)であるとき、`fits(X, E)`で検査される。
|
||||
|
||||
```
|
||||
```erg
|
||||
fits X, E =
|
||||
if Typeof(X) == Type:
|
||||
then := do subtypeof X, E
|
||||
|
|
@ -55,7 +55,7 @@ fits X, E =
|
|||
|
||||
`Array`の定義は
|
||||
|
||||
```
|
||||
```erg
|
||||
Array T <-> Union Self.iter().map(Typeof), N <-> Self.__len__() = ...
|
||||
```
|
||||
|
||||
|
|
@ -79,55 +79,69 @@ match x:
|
|||
match x:
|
||||
_: {1} -> log "one"
|
||||
_: {"a"} -> log "a"
|
||||
_: Obj -> log "other"
|
||||
_ -> log "other"
|
||||
```
|
||||
|
||||
Ergの型付けは基本的にextrinsic(外在的)であり、型を消去したコードも動的には実行できる(型なしで項が意味を持ちうる)。これは、ErgがPythonとの相互運用性を企図して設計されているためである。
|
||||
しかしパターンマッチにおいては、Ergの型はintrinsic(内在的)であるといえる。型によって処理が変わるため、型を消去したコードは最早実行できない。
|
||||
Ergの型は基本的にextrinsic(外在的)であり、型を消去したコードも動的には実行できる(型なしで項が意味を持ちうる)。これは、ErgがPythonとの相互運用性を企図して設計されているためである。
|
||||
しかしパターンマッチにおいては、Ergの型はintrinsic(内在的)であるといえる。型指定自体がパターンの一つであり、型によって処理が変わるため、型消去をしたコードは最早実行できない。
|
||||
|
||||
## 配列・タプルパターン
|
||||
## タプルパターン
|
||||
|
||||
```erg
|
||||
(True, 1) -> ...
|
||||
```
|
||||
|
||||
↓
|
||||
|
||||
```erg
|
||||
%1: ({True}, {1}) ->
|
||||
_ = %1[0]
|
||||
_ = %1[1]
|
||||
...
|
||||
```
|
||||
|
||||
## 配列パターン
|
||||
|
||||
配列は型情報が平坦化されてしまうので、一工夫が必要である。具体的には、篩型を使う。
|
||||
|
||||
```erg
|
||||
[[True, False], [True, True]] -> ...
|
||||
```
|
||||
|
||||
↓
|
||||
|
||||
```
|
||||
%1 ->
|
||||
%2 = %1[0]
|
||||
_: {True} = %2[0]
|
||||
_: {False} = %2[1]
|
||||
%3 = %1[1]
|
||||
_: {True} = %3[0]
|
||||
_: {True} = %3[1]
|
||||
```erg
|
||||
%1: {I: ? | } ->
|
||||
...
|
||||
```
|
||||
|
||||
全ての変数の型を推論すると
|
||||
|
||||
```
|
||||
%1: [[{True}, {False}], [{True}, {True}]] ->
|
||||
%2 [{True}, {False}] = %1[0]
|
||||
_: {True} = %2[0]
|
||||
_: {False} = %2[1]
|
||||
%3: [{True}, {True}] = %1[1]
|
||||
_: {True} = %3[0]
|
||||
_: {True} = %3[1]
|
||||
...
|
||||
```
|
||||
|
||||
コンパイルする場合は、`%1[0] == True and %1[1] == False and ...`というように、配列の要素を直接比較することになる。
|
||||
|
||||
```
|
||||
[True, False, i] -> ...
|
||||
↓
|
||||
%1: [{True}, {False}, Obj] ->
|
||||
_: {True} = %1[0]
|
||||
_: {False} = %1[1]
|
||||
i = %1[2]
|
||||
|
||||
```erg
|
||||
%1: {I: [[_; ?]; ?] | } ->
|
||||
%2 = %1[0]
|
||||
...
|
||||
```
|
||||
|
||||
バイトコードでの検査は`%1`の各要素に対してこれまでに見た検査を行い、`and`を取る。
|
||||
`_: {True}`なら`_ == True`、`i`は検査なしで束縛するから、`%1[0] == True and %1[1] == False`というようになる。
|
||||
↓
|
||||
|
||||
```erg
|
||||
%1: {I: [[_; 2]; ?] | I[0][0] == True and I[0][1] == False} ->
|
||||
%2 = %1[0]
|
||||
_ = %2[0]
|
||||
_ = %2[1]
|
||||
...
|
||||
```
|
||||
|
||||
↓
|
||||
|
||||
```erg
|
||||
%1: {I: [[_; 2]; 2] | I[0][0] == True and I[0][1] == False and I[1][0] == True and I[1][1] == True} ->
|
||||
%2 = %1[0]
|
||||
_ = %2[0]
|
||||
_ = %2[1]
|
||||
%3 = %1[1]
|
||||
_ = %3[0]
|
||||
_ = %3[1]
|
||||
...
|
||||
```
|
||||
|
|
|
|||
|
|
@ -9,23 +9,19 @@
|
|||
```python
|
||||
# 基本的な代入
|
||||
i = 1
|
||||
# 型つき
|
||||
i: Int = 1
|
||||
# 無名型つき
|
||||
i: {1, 2, 3} = 2
|
||||
|
||||
# function
|
||||
fn x = x + 1
|
||||
# equals
|
||||
fn x: Add(Int) = x + 1
|
||||
# (無名)関数
|
||||
fn = x -> x + 1
|
||||
fn: Int -> Int = x -> x + 1
|
||||
```
|
||||
|
||||
# 上位型
|
||||
a: [Int; 4] = [0, 1, 2, 3]
|
||||
# もしくは
|
||||
a: Array Int, 4 = [0, 1, 2, 3]
|
||||
## 型宣言パターン
|
||||
|
||||
```
|
||||
i: Int = 1
|
||||
j: {1, 2, 3} = 2
|
||||
(k: Int, s: Str) = 1, "a"
|
||||
```
|
||||
|
||||
### リテラルパターン
|
||||
|
|
|
|||
|
|
@ -4,8 +4,8 @@
|
|||
|
||||
Refinement type(篩型、ふるいがた)は、述語式によって制約付けられた型です。列挙型や区間型は篩型の一種です。
|
||||
|
||||
篩型の標準形は`{Elem: Type | (Pred)*}`です。これは、`Pred`を満たす`Elem`を要素とする型である、という意味です。
|
||||
篩型に使えるのは[Value型](./08_value.md)のみです。
|
||||
篩型の標準形は`{Elem: Type | (Pred)*}`です。これは、述語式`Pred`を満たす`Elem`を要素とする型である、という意味です。
|
||||
`Type`に使えるのは[Value型](./08_value.md)のみです。
|
||||
|
||||
```python
|
||||
Nat = 0.._
|
||||
|
|
@ -31,14 +31,27 @@ Array3OrMore == {A: Array _, N | N >= 3}
|
|||
あなたが二次方程式の解法を知っているならば、上の篩型は`{2, 3}`と同等になるだろうと予想できるはずです。
|
||||
しかしErgコンパイラは代数学の知識をほとんど持ち合わせていないので、右の述語式を解決できないのです。
|
||||
|
||||
## 篩型の部分型付け規則
|
||||
|
||||
全ての篩型は、`Type`部で指定された型の部分型です。
|
||||
|
||||
```erg
|
||||
{I: Int | I <= 0} <: Int
|
||||
```
|
||||
|
||||
その他、現在のErgは整数の比較に関する部分型規則を持っています。
|
||||
|
||||
```erg
|
||||
{I: Int | I <= 5} <: {I: Int | I <= 0}
|
||||
```
|
||||
|
||||
## スマートキャスト
|
||||
|
||||
`Odd`を定義したのはいいですが、このままではリテラル以外ではあまり使えないようにみえます。通常の`Int`オブジェクトの中の奇数を`Odd`に昇格させる、つまり`Int`を`Odd`にダウンキャストするためには、`Odd`のコンストラクタを通す必要があります。
|
||||
篩型の場合、通常のコンストラクタ`.new`はパニックする可能性があり、`.try_new`という`Result`型を返す補助的なコンストラクタもあります。
|
||||
|
||||
```python
|
||||
i = Odd.new (0..10).sample!()
|
||||
i: Odd # or Panic
|
||||
i = Odd.new (0..10).sample!() # i: Odd (or Panic)
|
||||
```
|
||||
|
||||
また、`match`中で型指定として使用することもできます。
|
||||
|
|
@ -73,8 +86,9 @@ match i:
|
|||
```python
|
||||
# メソッド.mは長さ3以上の配列に定義される
|
||||
Array(T, N | N >= 3)
|
||||
.m(&self) = ...
|
||||
.m(ref self) = ...
|
||||
```
|
||||
|
||||
<p align='center'>
|
||||
<a href='./11_enum.md'>Previous</a> | <a href='./13_algebraic.md'>Next</a>
|
||||
</p>
|
||||
|
|
@ -74,6 +74,36 @@ MyArray(T, N) = Inherit [T; N]
|
|||
# .arrayと連動してself: Self(T, N)の型が変わる
|
||||
MyStruct!(T, N: Nat!) = Class {.array: [T; !N]}
|
||||
```
|
||||
|
||||
## 実体指定
|
||||
|
||||
動的配列`arr: [T; !N]`について、処理を進めていくうちに`N`の情報が失われてしまったとします。
|
||||
この情報は`assert arr.__len__() == X`とすることで回復させることができます。
|
||||
|
||||
```erg
|
||||
arr: [Int; !_]
|
||||
assert arr.__len__() == 3
|
||||
arr: [Int; !3]
|
||||
```
|
||||
|
||||
これは型パラメータの __実体指定__ によって可能となっています。配列型`Array(T, N)`は以下のように定義されています。
|
||||
|
||||
```erg
|
||||
Array T <-> Union Self.map(x -> Typeof x), N <-> Self.__len__() = ...
|
||||
```
|
||||
|
||||
`<->`は依存型のパラメータのみで使える特別な記号で、そのパラメータに対する実体を指示します。実体であるところの右辺式は、コンパイル時に計算可能でなくても構いません。コンパイル時情報である`N`と実行時情報である`Self.__len__()`が実体指定を通してリンクされる訳です。
|
||||
実体指定に沿った方法でassertionが行われると、型パラメータの情報が復活します。すなわち、`assert arr.__len__() == N`とすると`N`の情報が復活します。ただしこの場合の`N`はコンパイル時計算可能でなくてはなりません。
|
||||
実体指定は`assert`以外に`match`でも活用されます。
|
||||
|
||||
```erg
|
||||
arr: [Obj; _]
|
||||
match! arr:
|
||||
pair: [Obj; 2] => ...
|
||||
ints: [Int; _] => ...
|
||||
_ => ...
|
||||
```
|
||||
|
||||
<p align='center'>
|
||||
<a href='./13_algebraic.md'>Previous</a> | <a href='./15_quantified.md'>Next</a>
|
||||
</p>
|
||||
|
|
|
|||
|
|
@ -155,9 +155,7 @@ impl Runnable for DummyVM {
|
|||
.to_string(),
|
||||
);
|
||||
if let Some(Expr::Def(def)) = last {
|
||||
res.push_str(&format!(" ({}: ", def.sig.ident()));
|
||||
res.push_str(&def.sig.t().to_string());
|
||||
res.push(')');
|
||||
res.push_str(&format!(" ({})", def.sig.ident()));
|
||||
}
|
||||
}
|
||||
Ok(res)
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue