Mica 7.7.2: the language written down

Mica 7.7.2 writes the language down. Its whole grammar is published in EBNF, with a syntax diagram for every rule, and is checked against every Mica source of the compiler’s test corpus, so the grammar a reader looks up is the one the compiler reads. A style guide states how a source is shaped, named, laid out and commented, rule by rule, every example a program that compiles, and mica --format lays a source out in that style. Formulas are written as a paper writes them: ≠, ≤ and ≥ compare, and π and τ stand in the math unit.

Tasks, generators and processes become dependable from end to end. A program survives the loss of its process server, a deadline reaches a typed file’s wait, a generator whose state fits a record pulls at the price of a call, and a generator waiting between two pulls is visible. A new technical report explains how a program uses all three. The editor keeps up with typing, and the project file is checked while it is typed.

The release at a glance

The grammar

The grammar is the whole syntax of Mica in EBNF, with a syntax diagram for every rule, in five chapters: the characters and tokens of a source, its units and declarations, its types, its statements and its expressions. Where the compiler decides by what surrounds a word, the rule carries a note that says so, and the spellings the compiler refuses by name have rules of their own. This is the rule for the comparisons:

comparison-operator = "=" | "#" | "≠" | "<" | "<=" | "≤" | ">" | ">=" | "≥" | "in" .

The grammar is checked against every Mica source of the compiler’s test corpus, so the grammar a reader looks up is the one the compiler reads.

The style guide

The style guide states how a Mica source is shaped, named, laid out and commented, rule by rule, and every example on it is a complete program that compiles, formatted exactly as shown. A unit runs from the comment that tells its story through its imports, constants, types and variables to its routines and its body. A name says what it holds, the strings and the numbers a body uses stand under names in the constant section, and where the sentence is mathematics, it is written as mathematics. The guide comes from the same rules the formatter applies, so the two cannot disagree.

The formatter

mica --format conversions.mica
mica --format --check sources/

mica --format lays a file, every .mica file beneath a folder, or standard input out in the house style, and prints each path it rewrote. It changes white space only: every token keeps the spelling its author wrote, so ≤ stays ≤ and 0xFF stays 0xFF, every comment keeps its words, and no line is broken or joined. With --check it writes nothing, names every file that is not formatted and exits with 1, for a build pipeline. Format Document does the same in VS Code. A file the formatter cannot lay out, such as one whose begin is never closed, is named with its line, its column and the reason, and is left as it was.

The standard library’s units and the user container’s examples are laid out by it. The style guide lists the rules the formatter applies and the four it leaves to the author.

Formulas as a paper writes them

{
    Circle - a circle's circumference and area, written the way a paper writes them.

    'π' and 'τ' come from the 'math' unit, '×' multiplies and '≤' compares, so
    each formula reads as it is printed.
}
program Circle;

imp
    WriteLn : std;
    π, τ : math;

const
    { the circle's radius, and the largest area the program accepts }
    Radius = 3.0;
    LargestArea = 30.0;

    CircleFormat = "circumference %.4lf, area %.4lf";
    FitsFormat = "the area fits within %.1lf";

var
    circumference, area : float64;

begin
    circumference := τ × Radius;
    area := π × Radius × Radius;
    WriteLn(CircleFormat, circumference, area);

    if area ≤ LargestArea then
        WriteLn(FitsFormat, LargestArea);
end.

≠, ≤ and ≥ are read exactly as #, <= and >=, as × is read as *, and the math unit exports π and τ beside Pi and Tau. A glyph is a spelling, not a new operator, and the formatter keeps the one its author wrote. The VS Code extension types the glyphs for you: \leq becomes ≤.

Text pasted from a typeset page is met by name. A minus sign of typeset text draws one diagnostic, which says what to write instead:

'−' is the minus sign of typeset text (U+2212), not an operator in Mica: Mica's minus is '-'

A decimal digit of another script inside a number, such as ٣, is named the same way, since Mica writes numbers with the digits 0 to 9.

A standby for the process server

A program that places tasks on processes starts a quiet copy of itself, the process server, before any of its tasks runs, and the server forks a worker for each placement. A standby now waits beside the server and takes its place when the server is lost, so the next placement runs, and the new server starts a standby of its own. The server answers every placement the moment it takes it, so a placement never goes to a server that has just ended and never runs twice. With no server left, each placement answers the block’s on lost section, as a lost worker does.

The whole surface of tasks and generators on processes was reviewed, and every finding is fixed: a generic task or producer meets every placement rule, a stream on a process carries elements of any width, a cancelled placement ends exactly its own worker, and a program another task starts inherits none of a placement’s pipes. The tasks on processes tutorial walks the road, and TR-3 explains the server and its standby.

Deadlines on typed files

A read or a write on a file of T over a pipe, a FIFO, a terminal or a socket parks its task, as the POSIX road’s calls do. Its carrier runs other tasks meanwhile, and a ScopeDeadline armed over it cancels the wait without taking a byte from the stream. A regular file is read and written as before. Because such a transfer can park, it stands outside a synchronized statement, as every call that may park does. The typed transfers tutorial states the rule.

Generators at the price of a call

{ The squares of 1 to 'count', one for each pull, in rising order. }
generator SquaresUpTo(count : int64) : stream of int64;
var
    k : int64;
begin
    for k := 1 to count do
        emit k * k;
end;

A generator whose emit stands inside a counted for, as this one’s does, inside a walk over a text, an array or a bitset, or inside a loop over another such generator now keeps its state in a record in its consumer’s frame instead of a stack of its own. A pull, one round of for square in SquaresUpTo(5) do, is then a call and a few word moves rather than a switch between two stacks. The compiler gives a generator this form wherever its state fits a record, and no program can tell the two forms apart; --verbose reports how many generators took each.

A generator waiting between two pulls is listed among the program’s tasks, in the debugger and in the runtime protocol’s task tree, with the state suspended and the activation that holds it. The generators tutorial follows a pull line by line, and TR-3 states which bodies keep their state in a record.

TR-3: tasks, generators and processes

TR-3, the third of Mica’s technical reports, explains the three places a piece of work runs: a task on a carrier, a generator inside its consumer, and a task in a process of its own. It takes them in turn, how each starts, waits, fails and ends, what the compiler proves about it and what the runtime guards, and states the guarantees in one table and what each placement costs. It is written for programmers and computer science students who know what a thread and a stack are but have not built a scheduler.

The editor

The language server receives only the text an edit changed, so typing in a large file costs it about as little as typing in a small one. Diagnostics appear half a second after typing stops, saved or not; correcting the text clears them, and a project’s other open units are checked with it. Every position the server exchanges counts UTF-16 code units, so on a line with a tab or a character such as 𝑥 a hover, a range or a diagnostic stands on its word, and a diagnostic at a keyword or an operator spans the word or the glyph.

A mica.project is checked while it is typed. Its JSON Schema is generated from the compiler’s own reader; the VS Code extension completes and checks the file with it, and the user container publishes it, so any editor that reads JSON Schema checks a project file the same way. The project file page says what the editor offers.

Held to its own rules

Every fix below comes with a test case that failed before it and passes now, so it stays fixed.

• The ownership checks. One heap cell stored into two slots of one container, such as two elements of an owning array, compiled and was released twice; the second store is refused now. Releasing an array cell releases every cell its elements hold, at every rank, a pointer a statement block declares is followed like any other, the value after on fail use meets every rule an assignment’s right side meets, and correct programs the checks refused compile. With --remarks, remark 13111 names every place where the checks stop following a cell, and a checked build that meets a second release inside a container’s release names the release that started it, as the traps reference shows.
• Constants. A constant computation that leaves its type, a negation or a cast past it, and a division by a constant zero are refused when compiling, on every tier. A constant widens as a variable does, a value its type cannot take is refused in a variable’s words, and a uint64 constant above int64’s range stands beside a number with no type.
• Stream capacities and counts. buffer 1 hung, and runs now, and a capacity is computed as any expression is. A capacity below one, a ring past a 64-bit address space, a reserve count below zero and a count whose bytes no allocation can have are refused by name when compiling if they are constants, and stop the program as an allocation_failure if they are not.
• Contracts. A library’s contract carries its typed array constants and its half-precision constants, a library saved with Windows line ends, a byte-order mark or a #! line publishes its generic bodies whole, and a build asked for a contract it cannot write fails with exit 1. A runtime floor that lacks a function a checked build calls is refused by name before the link.

Smaller fixes reach the scanner and the generators: a tab inside a string, a character or a regex literal stays a tab, one refused escape no longer makes the compiler misread the rest of the file, a generator keeps a variable declared in a statement block across an emit, and a routine that leaves from inside a walk over an array a function returned gives the array back.

Upgrading

Seven things a 7.7.1 build meets differently in 7.7.2:

• A constant computation that leaves its type is refused when compiling, on every tier, where debug and O2 wrapped it: Max + 1 and -Min for typed constants holding the largest and the smallest int64 (5421, 5639), and the cast Max as int32 (5233). Give the operation a type wide enough; a number with no type keeps the cast’s meaning, so 300 as int8 is 44. Every division by a constant zero is refused once, when compiling (5530).
• A stream’s buffer capacity is one or more: buffer 0 is refused (5633), where it became the default ring.
• A read or a write on a typed file stands outside a synchronized statement (5322), because it may park.
• A library that places work on processes links as an archive into the program that runs it; linking it as a shared object is refused by name.
• A swap of two elements of an owning array through a temporary that clears neither is refused at its middle store (13106), and so is a cell handed to an owning parameter after a call that borrowed its container, while the container may still hold it. Clear each element first, or take the cell out of its slot.
• A fixed arena keeps one more block for each task that receives values functions return, on one carrier as on many.
• The runtime floor’s contract is version 4, and a floor written to version 3 is refused by its version’s name.

The packages and the commands that install them are on the install page.