83 lines
2.8 KiB
Markdown
83 lines
2.8 KiB
Markdown
# Range Refinement
|
|
|
|
`narrower as wider` verifies that the left side is more concrete and narrower than the right side, then composes them asymmetrically.
|
|
|
|
```dcdl
|
|
Int & > 10 as Int & > 0
|
|
```
|
|
|
|
This succeeds and returns the narrower left-hand range, `Int & > 10`.
|
|
The reverse, `Int as Int & > 0`, fails because the left side is not guaranteed to satisfy the right side.
|
|
|
|
## Object
|
|
|
|
For objects, the right side defines the field domain used to check the left:
|
|
|
|
- A field found only on the left lies outside the right-hand domain and produces an error.
|
|
- A field found on both sides is checked recursively, and the narrower left-hand result is used.
|
|
- A field found only on the right remains unevaluated in the result, whether or not it has a default.
|
|
- Field order in the result follows the right-hand side.
|
|
|
|
```dcdl
|
|
partial = {
|
|
port = 8080;
|
|
} as {
|
|
host = String;
|
|
port = Int;
|
|
enabled = Bool default true;
|
|
};
|
|
```
|
|
|
|
`partial.port` becomes the concrete value `8080`.
|
|
`partial.host` and `partial.enabled` remain abstract fields from the right; `as` neither selects nor forces the default for `enabled`.
|
|
|
|
If `partial` is later materialized, the normal materialization rules apply.
|
|
In this example, unresolved `host` produces an error. If `host` is also made concrete, the default for `enabled` is selected during materialization.
|
|
|
|
## Default
|
|
|
|
A default is not evidence of range containment.
|
|
When the same field exists on both sides, the result uses the left side and does not inject the right-hand default.
|
|
|
|
```dcdl
|
|
Int & > 0 as (Int default 1)
|
|
```
|
|
|
|
The result is `Int & > 0` without a default.
|
|
A right-only object field, however, is retained as a whole and therefore retains any default its abstract value already had.
|
|
|
|
## Map and array ranges
|
|
|
|
`{...T}` allows arbitrary object keys and verifies that each value is narrower than `T`.
|
|
|
|
```dcdl
|
|
ports = {
|
|
http = 80;
|
|
https = 443;
|
|
} as {...(Int & >= 1 & <= 65535)};
|
|
```
|
|
|
|
When `[...T]` is used on the right, every array element is refined against `T` in the same way.
|
|
|
|
## Concrete right-hand ranges
|
|
|
|
Primitive and composed constraints validate values in the usual way.
|
|
If the right side is a concrete scalar or array literal, the left must have the same value or the same length and element structure.
|
|
A function cannot be used as the right-hand range.
|
|
|
|
The left side does not have to be concrete.
|
|
Abstract values can be used when their containment relation can be determined.
|
|
Primitive types, numeric bounds, identical regexes or predicates, and element ranges of arrays and maps support containment checks.
|
|
|
|
A function parameter written as `name: range` uses the same refinement rules as `as` when its argument is forced.
|
|
|
|
## Precedence
|
|
|
|
`as` has the lowest precedence, below `default`, and is left-associative.
|
|
|
|
```dcdl
|
|
narrow & overrides as Wider
|
|
```
|
|
|
|
This is interpreted as `(narrow & overrides) as Wider`.
|