File structure and imports

An Abella development is a collection of plain text files. Two of them describe the object system (the specification) and the rest record definitions and proofs about it.

Source files

Suffix	Purpose
.sig	The signature: kinds, constants, and predicates.
.mod	The clauses of a specification, written in the specification logic.
.thm	A development: declarations, definitions, theorems, and proofs.
.thmod	A reasoning module: declarations, definitions, and proofs.
.thc	A compiled .thm file, produced automatically.
.thmodc	A compiled .thmod file, produced automatically.

The .sig and .mod files share a base name. A specification named eval is the pair eval.sig and eval.mod. The .thm file that reasons about it uses the same base name by convention but need not. A .thmod file likewise uses its base name as the name of its top-level module.

Signatures

A signature begins with sig followed by its name and ends with .:

eval.sig

sig eval.

kind    tm, ty                 type.

type    app                    tm -> tm -> tm.
type    abs                    (tm -> tm) -> tm.

type    arrow                  ty -> ty -> ty.

type    of                     tm -> ty -> o.
type    eval, step, nstep      tm -> tm -> o.

kind introduces atomic types and their arity. type introduces constants and gives their types. A constant whose target type is o is a predicate of the specification logic. See Specification logic for the full syntax.

A signature may build on other signatures with accum_sig:

sig eval.

accum_sig terms.

type eval tm -> tm -> o.

The named signature is read first, and its declarations become part of the current signature. A signature is flattened in dependency order, so accum_sig chains are allowed. Cycles are rejected.

Specification modules

A specification module begins with module followed by its name and contains clauses:

eval.mod

module eval.

of (abs R) (arrow T U) :- pi x\ (of x T => of (R x) U).
of (app M N) T :- of M (arrow U T), of N U.

eval (abs R) (abs R).
eval (app M N) V :- eval M (abs R), eval (R N) V.

A module may include the clauses of other modules with accumulate:

module eval.

accumulate terms.

If a module accumulates another module, its signature must accum_sig the other module's signature. This restriction ensures that every constant used by the accumulated clauses is declared in the importing signature. See Specification logic for details.

Reasoning modules

A .thmod file is a reasoning-level module. It contains one top-level Module/End block, which may contain nested modules:

List.thmod

Module List[T].
  Kind lst type.
  Type lnil lst.
  Type lcons T -> lst -> lst.
  Type contains T -> lst -> prop.
End List.

The top-level module name must match the file base name. A .thm file may also define modules inline; those modules are local to the development and are not exported by its .thc artifact. See Reasoning-level modules for the full syntax and semantics.

Developments

A .thm file is a sequence of top-level commands. The two commands that connect a development to its specification are Specification and Import.

Specification

Specification "name". reads the signature and module with the given base name. It must be the first command in a development, because the logic is parameterized by the specification:

Specification "eval".

The extension is added automatically: Abella looks for eval.sig and eval.mod. The name may include a relative path, and the path is resolved relative to the directory of the .thm file (or the current directory in interactive mode).

Specification may be used only once. If a development needs declarations from several specifications, combine them with accum_sig and accumulate instead.

Import

Import "name". loads a previously compiled development. The extension .thc is added automatically:

Import "util".

Importing makes the definitions and theorems of the compiled file available without rechecking its proofs. If the .thc file is missing or older than the corresponding .thm file, Abella recompiles it before importing.

The importing development must be compatible with the imported one:

• every kind and constant mentioned by the imported file must already exist in the importing development;
• every specification clause used by the imported file must already be present;
• the clauses of a predicate declared in the imported file cannot be extended by the importing development.

Import also accepts a with clause that renames predicates. The syntax is:

Import "name" with p = q, r = s.

Each replacement maps a predicate declared in the imported development to a predicate of the importing development. The replacements must be pairwise distinct, and they are applied simultaneously.

A .thmod file is loaded with Import Module rather than Import. See Reasoning-level modules for that form.

Recursive compilation

By default, importing a .thm file compiles it and any of its imports that are out of date. The -N (or --non-recursive) option disables this recursion:

$ abella --non-recursive foo.thm

With -N, Abella assumes that every imported .thc file is current and fails if one is missing. The same applies to .thmodc files.

Default compiled output

In batch mode, compiling file.thm writes file.thc next to it, and compiling file.thmod writes file.thmodc. The -c option is deprecated and its argument is ignored; the artifact is always written to the default location.

In interactive mode the compiled development is not written to disk.

Naming rules

The names of types, constants, predicates, variables, and theorems follow the same lexical rules:

• a name begins with a letter, or one of the symbols -, =, ^, `, ', ?, $;
• the rest may also contain digits and the symbols _, /, *, @, +, #, !, ~.

Names beginning with an uppercase letter are variables in formulas unless they are bound. Lowercase names are usually constants or predicates, but the distinction is enforced by binding structure rather than by case.

Module names must match [A-Z][A-Za-z0-9_]*. Items of a module are selected with a qualified name such as N.contains, where N is the import alias or the module name.

Nominal constants displayed by Abella have the form n1, n2, and so on. They are generated by the system, so source files normally refer to them only indirectly through nabla binders.

Directory layout

There is no required layout. The examples shipped with Abella group related files in directories:

examples/
  lambda-calculus/
    eval.sig
    eval.mod
    eval.thm
    type-uniq/
      type-uniq.sig
      type-uniq.mod
      type-uniq.thm
  logic/
    ...

A relative name is resolved against the directory of the importing file. Absolute names are used as they are. The Set load_path option records a load path, but the current implementation does not fall back to it when a relative name is not found:

Set load_path "lib".
Specification "eval".

To read a specification from another directory, write the directory as part of the name:

Specification "lib/eval".

Generated documentation

abella_doc reads .thm, .thmod, .sig, and .mod files and writes HTML pages beside them. For each file.thm or file.thmod it produces file.html, and for each specification it produces file.lp.html, together with JSON files that carry the annotations used by the generated pages. These outputs are generated artifacts and should not be edited by hand. See abella_doc.

abella_dep reads the same source files and writes a Makefile that records the dependencies between them. See abella_dep.