Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 10 additions & 7 deletions docs/ambiguity/proof-obligations.md
Original file line number Diff line number Diff line change
Expand Up @@ -59,8 +59,8 @@ numbers in a proof report refer to.

| Automaton | Conflict states | with shift/reduce | with reduce/reduce |
| --------- | --------------: | ----------------: | -----------------: |
| `--GLR`, the parser that ships | 56 | 55 | 1 |
| stock | 49 | 48 | 1 |
| `--GLR`, the parser that ships | 62 | 61 | 1 |
| stock | 55 | 54 | 1 |

Menhir explains each conflict state once, so the explanations file holds one
block per state; a state with both kinds of conflict counts in both of Menhir's
Expand Down Expand Up @@ -95,7 +95,7 @@ are not independent problems:
| Lookahead | States | Reduction | Root |
| --------- | -----: | --------- | ---- |
| `(` | 15 | `loption_generics_ ->` | before a call or a lambda, including standalone constructor type arguments |
| `<` | 12 | `loption_generics_ ->` | against `<` as a declared operator |
| `<` | 18 | `loption_generics_ ->` | against `<` as a declared operator |
| `(` `<` | 3 | `loption_generics_ ->` | a named type opening a call or a generic list |
| `(` `<` `{` `.` | 3 | `loption_generics_ ->` | a named type opening a constructor body |
| `(` | 3 | `list_verb_type_suffix_ ->` | a type opening a statement, against a call |
Expand All @@ -118,13 +118,16 @@ type from a constructor call or lambda continuing after that name. The
constructor-type regression checks the permitted and rejected spellings;
operator operands and ordinary function arguments no longer admit bare types.

The `<` row is about the declaration form, not the comparison. Its twelve states
The `<` row is about the declaration form, not the comparison. Its eighteen states
all reduce toward `ret_type "<" "(" params ")" body`, the declaration of the
`<` operator, against shifting `<` as the opening bracket of a generic argument
list: after a name type, `Foo<Int> …` and `Foo <(a Int) { }` open with the same
two tokens. Three of the twelve are the same fork after an abort type,
`Int?Foo<Int>` against `Int?Foo <(a Int) { }`. Dropping `<` and `>` from the
operators a declaration may name removes all twelve and nothing else, which is what identifies the family; it is a
two tokens. Six of the eighteen are the same fork after an abort type,
`Int?Foo<Int>` against `Int?Foo <(a Int) { }`. Each fork comes three times,
once for each way a return type may name its type: bare, `&Foo` and `^Foo`,
the roaming owner a reference-typed return is written as. The `^` forms add
six states and nothing else, since `^` begins no expression. Dropping `<` and `>` from the
operators a declaration may name removes all eighteen and nothing else, which is what identifies the family; it is a
language change rather than a restructuring, so it is a measurement here and
not a proposal.

Expand Down
231 changes: 129 additions & 102 deletions docs/design/lowering.md

Large diffs are not rendered by default.

188 changes: 118 additions & 70 deletions docs/design/semantics.md

Large diffs are not rendered by default.

9 changes: 5 additions & 4 deletions docs/design/symbols.md
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,8 @@ geometry$List<%primitives$Int>
%primitives$Int
```

Arguments are separated by `, `. A guest is written `&` before its type.
Arguments are separated by `, `. A reference is written `&` before its type,
and a roaming owner `^`.

An intrinsic namespace is written with `%` where the source writes `@`:
`%primitives$Int` is `@primitives$Int`. A linker reads `@` in an exported
Expand Down Expand Up @@ -98,7 +99,7 @@ pkg$Op.apply$lambda1

## Layout tables

The table the runtime reads to find a type's hosts and blocks
The table the runtime reads to find the blocks a type's values own
([`lowering.md`](lowering.md) L9) is called by the type's name. An outcome's
table is called `outcome of T`, with ` ? A` added when the verb can abort
with `A`.
Expand All @@ -118,8 +119,8 @@ the function a spawned call to a verb expanded where it is called
(`zane.expanded.N`) or to an intrinsic (`zane.intrinsic.N`) is made into
([`lowering.md`](lowering.md) §9), each string literal's bytes
(`zane.text`), the entry that makes a program's constants and then calls
`main` (`zane.start`), and the variable a guest to a program value such as
`@program$console` is anchored at (`zane.value.@program$console`).
`main` (`zane.start`), and the variable whose address a reference to a
program value such as `@program$console` holds (`zane.value.@program$console`).

## What the compiler does today

Expand Down
83 changes: 34 additions & 49 deletions docs/spec-divergences.md
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ settles, in one pass rather than section by section. Until then:
the claim can be rechecked rather than taken on trust.

A choice the spec leaves open is recorded here when a running program can
observe it, as §10 and §13 are. The rest sit beside the design they belong
observe it, as §9 and §12 are. The rest sit beside the design they belong
to: what the type checker decides is in
[`design/semantics.md`](design/semantics.md) §9, with D12 and D14, and how
lowering and the runtime place and represent things is in
Expand Down Expand Up @@ -239,7 +239,7 @@ register(Int); // rejected: an ordinary function argument
held Slot = Int; // rejected: the value of a declaration
arr Array(Int + 1); // rejected: an operand
room Slots(Array<Int, 4>, 2); // rejected: an applied type
room Slots(&Int, 2); // rejected: a guest type
room Slots(&Int, 2); // rejected: a reference type
room Slots(Int[3], 2); // rejected: an array type
```

Expand Down Expand Up @@ -381,37 +381,7 @@ mention one. It needs a digit on each side, and none of the loose operators of
(`docs/ambiguity/proof-obligations.md`). Reconciling means either the spec
adopting the separator or the lexer dropping it.

## 9. The console's `print` takes a guest

**Spec** — [`effects.md`](https://github.com/zane-lang/spec/blob/7fa876f/spec/effects.md)
§6.6, as of `7fa876f`, which introduced it:

```zane
@primitives$Unit print(this @runtime$Console, text @primitives$String) mut
```

`@primitives$String` is a reference type ([`types.md`](https://github.com/zane-lang/spec/blob/7fa876f/spec/types.md)
§2.7), so a plain parameter of it swallows its argument: the caller moves a
view in.

**Compiler** — `text &@primitives$String`, a guest. `print` writes the view
out and keeps nothing, which is what a guest parameter is for. Zane has no
borrow of a reference type, and a guest differs from one only in taking a
place rather than any expression, so a view built for the call is stored
first:

```zane
text @primitives$String("hello world");
@program$console!print(text); // accepted
@program$console!print(@primitives$String("hello world")); // rejected: a temporary
```

A swallowing `print` would also leave `core`'s `String` no way to reach the
console, since its view is a field (`text.raw`), and a field is not a
move-source ([`lifetimes.md`](https://github.com/zane-lang/spec/blob/7fa876f/spec/lifetimes.md)
§1.2). Reconciling means the spec declaring the parameter `&@primitives$String`.

## 10. An integer division by zero stops the program
## 9. An integer division by zero stops the program

**Spec** — silent. [`operators.md`](https://github.com/zane-lang/spec/blob/7fa876f/spec/operators.md)
§4.3 says division is declared rather than derived, and nothing says what
Expand All @@ -431,7 +401,7 @@ quotient Int = Int(1) / zero(); // stops here, status 1
Reconciling means the spec stating an outcome, or making `/` abortable, now
that aborts lower (step 4 of `docs/design/lowering.md` §8).

## 11. An exit ends the run of a block
## 10. An exit ends the run of a block

**Spec** — [`control-flow.md`](https://github.com/zane-lang/spec/blob/7fa876f/spec/control-flow.md)
§2.3 and §4.2: `@controlflow$exitFromCall` ends the invocation that called
Expand All @@ -443,7 +413,7 @@ the verb containing it, and blocks are transparent to it, so a `guard` inside
written in, and a call to an exiting verb is legal only inside a block. A
verb's body must end in an explicit `return`, `Unit()` included
([`error-handling.md`](https://github.com/zane-lang/spec/blob/7fa876f/spec/error-handling.md)
§8), while a block yields nothing (§12 below), so it has nothing to give and
§8), while a block yields nothing (§11 below), so it has nothing to give and
is the one thing an exit can end.

```zane
Expand All @@ -463,7 +433,7 @@ written there. `lib/tst/analyses/exits.ml` checks the calls, and
`tests/semantics/fixtures/typing/reject/bad/exits.zn` is the rejected case.
Reconciling means the spec adopting this reading.

## 12. A block yields nothing
## 11. A block yields nothing

**Spec** — [`control-flow.md`](https://github.com/zane-lang/spec/blob/7fa876f/spec/control-flow.md)
§2.1 and §2.4: a block's type is `@concepts$Block`, or `@concepts$Block<T>`
Expand Down Expand Up @@ -491,7 +461,7 @@ done Bool = if(ready) {
condition of §3.3 has no form here. Reconciling means the spec dropping
`Block<T>`, or the compiler taking it back.

## 13. A spawned call's handler runs where the call settles
## 12. A spawned call's handler runs where the call settles

**Spec** — [`concurrency.md`](https://github.com/zane-lang/spec/blob/7fa876f/spec/concurrency.md)
§3.3: an abortable spawned call attaches `?` or `??` directly to the
Expand All @@ -503,7 +473,7 @@ or what happens when nothing reads the symbol.
its local is first read, or where the block it is spawned in ends, when
nothing has read it by then. Settling waits for the call. An abort runs the
handler there, and an exit ends the run of the block the spawn is written in
(§11), from there. A block left before it ends -- by a `return`, an exit or
(§10), from there. A block left before it ends -- by a `return`, an exit or
an `abort` -- still waits for the call as it drains, but runs no handler, and
the outcome dies with the block.

Expand All @@ -519,21 +489,22 @@ check(q == Int(7)); // settled already: the handler does not run again
`tests/codegen/fixtures/spawns` has these cases. Reconciling means the spec
saying where the handler runs.

## 14. A block does not write a host it lent a running spawn
## 13. A block does not write an owner it lent a running spawn

**Spec** — [`concurrency.md`](https://github.com/zane-lang/spec/blob/7fa876f/spec/concurrency.md)
§4.2 lets spawned work read the reference-type object graph without writing
it, which makes "every concurrent **read** of the reference-typed object
graph safe by construction". §4.3 keeps the spawning block off a location
while a spawn holds its mutable borrow. Neither says anything about the
spawning block writing a host it passed to a spawn that only reads it, and
spawning block writing an owner it passed to a spawn that only reads it, and
that block keeps running while the spawn does.

**Compiler** — a spawn written as a statement or bound by a `let` is lent
every host passed to it, directly or through a guest, until its block drains,
and the block may not write one meanwhile: by assignment, as a `!` call's
subject, or by moving it out. Where a guest's host cannot be followed, the
write is judged by type, so some programs that would not race are rejected.
every owner passed to it, directly or through a reference, until its block
drains, and the block may not write one meanwhile: by assignment, as a `!`
call's subject, or by moving it out. Where the owner a reference names cannot
be followed, the write is judged by type, so some programs that would not race
are rejected.

```zane
view &Dial = dial;
Expand All @@ -547,7 +518,7 @@ spawn dial.reading!nudge(); // accepted: written back (§4.4)
Reconciling means the spec stating a rule for this write, this one or
another.

## 15. A case is not a type
## 14. A case is not a type

**Spec** — [`adt.md`](https://github.com/zane-lang/spec/blob/7fa876f/spec/adt.md)
§3: "A member projected as a type is written `Expr.intLit`", and §5.2: "if the
Expand All @@ -569,13 +540,13 @@ projected case type would still be the whole variant (§3.2), and the
narrowing it enables is an optimization the tag jump already gives. Reconciling
means adding the type form and its narrowing, or the spec dropping it.

## 16. An index out of range stops the program
## 15. An index out of range stops the program

**Spec** — silent. [`control-flow.md`](https://github.com/zane-lang/spec/blob/7fa876f/spec/control-flow.md)
§5.2 fixes the ordinal base and leaves "the language-level behavior for
out-of-range element access" as a separate question.

**Compiler** — the program stops as it does at a division by zero (§10): what
**Compiler** — the program stops as it does at a division by zero (§9): what
it wrote so far is flushed, the runtime writes `index out of range` to stderr,
and the status is 1, for a list and an array alike.
`tests/codegen/fixtures/range` and `tests/codegen/fixtures/bounds` are the
Expand All @@ -592,8 +563,9 @@ Kept briefly so a reader who remembers them can see they were closed on
purpose, and by what. The first three closed at the `034f11a` re-pin, when the
spec moved to `;`-terminated statements and a brace that ends one. The next
closed from the other side, when the compiler adopted a spec rule it had been
standing in for, and the last when the compiler followed the spec in removing a
form.
standing in for, the next when the compiler followed the spec in removing a
form, and the last when the spec's memory model made the compiler's departure
unnecessary.

- **Statements are terminated, not separated.** The spec separated statements
by newline and called it "the one place a newline is structural"; the
Expand Down Expand Up @@ -676,3 +648,16 @@ form.
lexer, and the call is written `show(Color.red)`. The `Pipe` and
`MethodTarget` nodes went with it, since a method target was only ever a
pipe's callee.

- **The console's `print` took a reference.** The spec declares
`print(this @runtime$Console, text @primitives$String)`, and while
`@primitives$String` was a reference type a plain parameter of it consumed
its argument, which would have spent the caller's string and left `core`'s
`String` no way to pass the view it holds in a field. The compiler took
`text &@primitives$String` instead. Spec
[#209](https://github.com/zane-lang/spec/pull/209) made
`@primitives$String` a value type, whose parameter is a read-only borrow,
and [#212](https://github.com/zane-lang/spec/pull/212) made a bare
reference-type parameter a borrow too, so the spec's own signature reads the
text without taking it. The compiler now declares `print` exactly as the
spec does, and a string built in the argument is passed as it is.
Loading
Loading