This chapter builds a small notes application on the sqlite library. You copy the library’s files into a fresh project, write one program against them, and end with a binary that keeps its notes in a real database file.

Everything here runs in the starter container; the library lives in libraries/sqlite, and libsqlite3-dev is already installed.

The files you copy

The library is source you own, not a package you depend on:

  • sqlite.mica is the library unit: its whole surface, commented, yours to read and change.
  • sqlite3.external is the contract for sqlite’s C interface: the functions the unit calls, with their exact C shapes.
  • sqlite3-internal.external is the part of that interface only the library calls: the connection’s error text and the mutex it is copied under. Your program never consumes it.
mkdir notes && cd notes
cp ../mica-container/libraries/sqlite/{sqlite.mica,sqlite3.external,sqlite3-internal.external,mica.project} .

The mica.project is for your editor and for the library’s build: the language server reads it to resolve the contracts, so everything analyzes clean while you work, and it states the library’s version, 2.0.0, which the library’s build writes into the contract it emits. Point its sources at your own program as you go.

Opening and migrating

program notes;

imp
    WriteLn : std;
    Halt : process;
    Database, Statement : sqlite;
    Open, Close, Exec, Prepare, Finalize, Run, Rows, Parameter, Column : sqlite;
    BindText, BindInt64, Text, Int64 : sqlite;
    Begin, Commit, RollbackUnlessCommitted, LastInsertRowId, Message, Describe : sqlite;
    SqliteExec, SqliteCode, SqliteConstraint : sqlite3;

var
    database : Database;
    code : SqliteCode;

{ Stop reports a failure the program cannot go on after, and ends it. }
procedure Stop(what : string, failure : SqliteCode);
begin
    WriteLn("%ls failed: %ls", what, Describe(failure));
    Halt(1);
end;

begin
    database := Open("notes.db") on fail code do Stop("open", code);
    defer Close(address database);

    Exec(database, "create table if not exists notes (title text primary key, stars integer not null)")
    on fail code do Stop("migration", code);
    Exec(database, "delete from notes") on fail code do Stop("clearing", code);
end.

Two things carry the whole chapter. First, failure travels the failure channel. Open and Exec fail with sqlite’s own result code, and you meet trouble with the language’s forms: on fail code do at the statement here, on fail leave where an enclosing routine should pass it on. There are no return codes to check, and a call whose failure nothing meets does not compile.

Second, a Database is a value holding sqlite’s handle. Close gives the handle back and empties the record, so the defer right after the open releases it however the program ends, and a second Close would do nothing.

Writing notes through one statement

Never build SQL out of user text; bind it. A statement is compiled once and run for each note:

procedure AddNotes(notes : Database) fails SqliteCode;
var
    insert : Statement;
    title : int32;
    stars : int32;
begin
    insert := Prepare(notes, "insert into notes (title, stars) values (:title, :stars)") on fail leave;
    defer Finalize(address insert);
    title := Parameter(insert, ":title") on fail leave;
    stars := Parameter(insert, ":stars") on fail leave;

    BindText(insert, title, "buy milk") on fail leave;
    BindInt64(insert, stars, 1) on fail leave;
    Run(insert) on fail leave;

    BindText(insert, title, "write the report") on fail leave;
    BindInt64(insert, stars, 3) on fail leave;
    Run(insert) on fail leave;

    BindText(insert, title, "call the plumber") on fail leave;
    BindInt64(insert, stars, 2) on fail leave;
    Run(insert) on fail leave;

    WriteLn("the last note is row %lld", LastInsertRowId(notes));
end;

Parameter turns each named parameter into its position once, and every bind takes the position. Run steps the insert to its end and resets it, ready for the next note, with its bindings kept until new ones replace them. The text crosses into sqlite as UTF-8, whatever encoding your program targets, and sqlite copies it before the bind returns.

Inside a fails procedure the honest form is on fail leave: the failure goes on through this procedure’s own channel, and its caller decides.

A constraint is a failure like any other

The table’s primary key keeps titles unique, so a second “buy milk” breaks it. The failure carries sqlite’s code, and Message answers sqlite’s own words for it:

Exec(database, "insert into notes (title, stars) values ('buy milk', 2)") on fail code do
    if code = SqliteConstraint then
        WriteLn("not added twice: %ls", Message(database));
not added twice: UNIQUE constraint failed: notes.title

Reading notes

This is the daily idiom the library exists for:

procedure ListStarred(notes : Database, minimum : int64) fails SqliteCode;
var
    query : Statement;
    row : Statement;
    title : int32;
    stars : int32;
begin
    query := Prepare(notes, "select title, stars from notes where stars >= ?1 order by stars desc") on fail leave;
    defer Finalize(address query);
    BindInt64(query, 1, minimum) on fail leave;
    title := Column(query, "title") on fail leave;
    stars := Column(query, "stars") on fail leave;

    for row in Rows(query) do
    begin
        WriteLn("  %ls (%lld)", Text(row, title), Int64(row, stars));
    end
    on fail leave;
end;

The order on the page is the order it runs: prepare, bind, find the columns, pull the rows, read them. Each row is the statement itself, positioned on that row, and Text and Int64 read its columns. Every text a reader answers is a copy of your program’s own, because sqlite’s buffer changes at the next row.

Rows is a generator. When the loop ends, at the last row, by a leave, or by a failure of a step such as a database another connection has locked, the statement is reset, so it can run again. A failure reaches the loop’s on fail, and it can never pass for a clean end of rows.

Changing notes in a transaction

Begin(database) on fail code do Stop("begin", code);
defer RollbackUnlessCommitted(database);
Exec(database, "update notes set stars = stars + 1") on fail code do Stop("update", code);
Commit(database) on fail code do Stop("commit", code);

RollbackUnlessCommitted is the one call to defer right after Begin. If anything between the two fails, the transaction is rolled back when the block ends; after Commit it does nothing.

The callback road

sqlite also speaks its own shape: sqlite3_exec fires a function pointer once per row. Mica has no function pointers, because a routine is called with its argument list and never read by name. Its answer at the boundary is the third declared subprogram kind, the callback:

type
    Tally = record
        rows : int64;
    end;

var
    tally : Tally;

callback CountRow(context : pointer Tally, columns : int32, values : pointer int64, names : pointer int64) : int32;
begin
    context.rows := context.rows + 1;
    CountRow := 0;
end;

SqliteExec(database.handle, "select title from notes", CountRow, address tally, nil) on fail code do Stop("count", code);

A callback is never called from Mica and is never a value: sqlite fires it, while the exec call itself runs. Its whole environment is the context record whose address you pass, so everything the callback can touch is on that one line. Use the pull road every day; the callback road is there when a C interface’s own shape is the honest one. Callbacks at the boundary is the kind’s own chapter.

The whole program

Put together in the order they run, the pieces make one file, notes.mica, beside the library’s files:

program notes;

imp
    WriteLn : std;
    Halt : process;
    Database, Statement : sqlite;
    Open, Close, Exec, Prepare, Finalize, Run, Rows, Parameter, Column : sqlite;
    BindText, BindInt64, Text, Int64 : sqlite;
    Begin, Commit, RollbackUnlessCommitted, LastInsertRowId, Message, Describe : sqlite;
    SqliteExec, SqliteCode, SqliteConstraint : sqlite3;

type
    Tally = record
        rows : int64;
    end;

var
    database : Database;
    code : SqliteCode;
    tally : Tally;

{ Stop reports a failure the program cannot go on after, and ends it. }
procedure Stop(what : string, failure : SqliteCode);
begin
    WriteLn("%ls failed: %ls", what, Describe(failure));
    Halt(1);
end;

procedure AddNotes(notes : Database) fails SqliteCode;
var
    insert : Statement;
    title : int32;
    stars : int32;
begin
    insert := Prepare(notes, "insert into notes (title, stars) values (:title, :stars)") on fail leave;
    defer Finalize(address insert);
    title := Parameter(insert, ":title") on fail leave;
    stars := Parameter(insert, ":stars") on fail leave;

    BindText(insert, title, "buy milk") on fail leave;
    BindInt64(insert, stars, 1) on fail leave;
    Run(insert) on fail leave;

    BindText(insert, title, "write the report") on fail leave;
    BindInt64(insert, stars, 3) on fail leave;
    Run(insert) on fail leave;

    BindText(insert, title, "call the plumber") on fail leave;
    BindInt64(insert, stars, 2) on fail leave;
    Run(insert) on fail leave;

    WriteLn("the last note is row %lld", LastInsertRowId(notes));
end;

procedure ListStarred(notes : Database, minimum : int64) fails SqliteCode;
var
    query : Statement;
    row : Statement;
    title : int32;
    stars : int32;
begin
    query := Prepare(notes, "select title, stars from notes where stars >= ?1 order by stars desc") on fail leave;
    defer Finalize(address query);
    BindInt64(query, 1, minimum) on fail leave;
    title := Column(query, "title") on fail leave;
    stars := Column(query, "stars") on fail leave;

    for row in Rows(query) do
    begin
        WriteLn("  %ls (%lld)", Text(row, title), Int64(row, stars));
    end
    on fail leave;
end;

callback CountRow(context : pointer Tally, columns : int32, values : pointer int64, names : pointer int64) : int32;
begin
    context.rows := context.rows + 1;
    CountRow := 0;
end;

begin
    database := Open("notes.db") on fail code do Stop("open", code);
    defer Close(address database);

    Exec(database, "create table if not exists notes (title text primary key, stars integer not null)")
    on fail code do Stop("migration", code);
    Exec(database, "delete from notes") on fail code do Stop("clearing", code);

    AddNotes(database) on fail code do Stop("adding", code);

    Exec(database, "insert into notes (title, stars) values ('buy milk', 2)") on fail code do
        if code = SqliteConstraint then
            WriteLn("not added twice: %ls", Message(database));

    WriteLn("notes with at least two stars:");
    ListStarred(database, 2) on fail code do Stop("listing", code);

    Begin(database) on fail code do Stop("begin", code);
    defer RollbackUnlessCommitted(database);
    Exec(database, "update notes set stars = stars + 1") on fail code do Stop("update", code);
    Commit(database) on fail code do Stop("commit", code);

    SqliteExec(database.handle, "select title from notes", CountRow, address tally, nil) on fail code do Stop("count", code);
    WriteLn("%lld notes counted by the callback", tally.rows);
end.

Building

mica --compile --link --output-modifier archive --emit-contract --external static \
    --project . --source sqlite.mica --build build/sqlite

mica --compile --link \
    --external-contract build/sqlite/mica.external,sqlite3.external --external static \
    --source notes.mica --build build

The library compiles once into an archive, through the project file, which supplies sqlite’s contract and the library’s version, and emits its own contract. That contract carries the archive, sqlite’s link flag and the version to your program, so your link line composes itself from the two contracts you name, and your build names the library:

Using library 'sqlite' 2.0.0
Using library 'sqlite3'

There is no C to compile: every shape of sqlite’s interface the library uses, from the handle sqlite3_open_v2 answers through a sqlite3 ** to the constant that tells sqlite to copy a bound text, is stated in sqlite3.external.

Run it:

./build/notes
the last note is row 3
not added twice: UNIQUE constraint failed: notes.title
notes with at least two stars:
  write the report (3)
  call the plumber (2)
3 notes counted by the callback

Where to go next

The library’s page lists every routine, and the library’s own make check runs each of them against sqlite. The contracts reference states every field a contract uses, and callbacks at the boundary goes deeper into the callback road.