CBS-beta

Beta-release of the CBS framework

View My GitHub Profile

CBS-beta Browsing Guide

All references to names of funcons (etc.) in CBS specifications are hyperlinks leading to their declarations.

These hyperlinks avoid the need to drill down through the hierarchy of folders and files. Specifications in CBS are independent of the file system: all names declared in Funcons-beta are globally visible, and names declared in a particular language specification are local to that language, regardless of file structure.

The global Funcons-Index page lists the names of all current funcons, grouped according to their types. The local funcons-index page for a particular language lists only the names of the funcons actually used in its specification. The funcon reuse page shows which of the included languages reference each funcon.

Hovering on a reference to a funcon displays the declared arity of symbol: values stands for a single argument, and values* for any number of arguments.

The large button at the top right of each CBS page is a fixed drop-down menu.

For pages in Funcons-beta, it has the following links:

For pages in Languages-beta/L, it has also the following links:

Folding

When a CBS web page is opened, all the rules, comments, and subsections are unfolded, as indicated by downward-pointing disclosure symbols (e.g.: ▼).

Individual rules, comments, and subsections can be folded/unfolded by clicking on a character in the line containing the disclosure symbol. Note that printing the page omits the disclosure symbols, but does not show lines hidden by the current folding.

The top right corner of each CBS web page has buttons for unfolding (▼) or folding (►) all rules, comments, or subsections on the current page. (These buttons require Javascript, and are not shown when Javascript is off.)


Languages

See the CBS of IMP for illustration of the following points.

Syntax

Syntax introduces one or more grammar productions for the abstract (context-free) syntax of the language, together with meta-variables ranging over the associated sorts of ASTs.

Lexis introduces one or more grammar productions for the lexical (regular or context-free) syntax of the language, together with meta-variables ranging over the specified strings of characters.

Parsers generated from grammars for abstract syntax are usually ambiguous. Associativity, relative priority, and lexical disambiguation are currently specified separately, using notation from SDF, embedded in multi-line comments /*...*/.

Semantics

Semantics introduces a declaration of a translation function from ASTs (with strings as leaves) to funcon terms.

Rule introduces an equation defining the translation function on trees matching a specified pattern.

All funcons (etc.) defined in Funcons-beta can be used in all language definitions. Funcons defined in a language definition file must have fresh names, and cannot be reused in other language definitions (except by copy-paste).


Funcons

Funcon names start with lowercase letters, and may include letters, digits, and dashes -.

Variables in funcon terms start with uppercase letters, and may be suffixed by digits and/or primes. Variables that stand for sequences of indefinite length are suffixed by *, +, or ?. Variables whose values are not required may be replaced by underscores _.

A funcon term formed from a funcon f and argument sequence s is written in prefix form: f s. When f has no arguments, it is written without parentheses: f; when it has 2 or more arguments t1, …, tn, they are written in ordinary parentheses: f(t1,...,tn). Parentheses are optional when there is a single argument term, so both f t and f(t) are allowed.

Funcons are not higher-order, so implicit grouping of f g t as (f g)(t) would here be completely useless, as it would never give a well-formed term. Grouping in funcon terms treats funcon names as prefix operations, such as the ‘-’ in ‘-sin(x)’. (Readers accustomed to higher-order programming in Haskell may find it helpful to imagine f g t written as f$g t.)

Some funcons can take argument sequences of varying lengths; funcons may also compute sequences of values. An example of a funcon that does both is left-to-right, which is used to ensure that arguments are evaluated in the specified order (the default is to allow interleaving). Composition with left-to-right provides sequential variants of all multi-argument funcons, e.g.:

The following special forms of funcon terms are allowed:

The funcon definitions in Funcons-beta are language-independent.

CBS specifications do not refer to the hierarchy of folders and files used for Funcons-beta.

Files in Funcons-beta are generally divided into unnumbered subsections. The number of # characters in a subsection heading indicates its level, with the top level sections Computations and Values having a single #.

Type definitions

In CBS, types are values. They can be given as arguments to funcons, and computed by funcons.

Type introduces a declaration of a fresh funcon name for a type, and lists any arguments. The type of values it computes is types.

Datatype introduces a definition of an algebraic datatype, written t ::= f1(...) | ... | fn(...), which also declares the constructor funcons fi(...):t for its values.

Meta-variables introduces type constraints on variables used in rules. These constraints are usually of the form v <: t where v is a variable, requiring v to be a subtype of t.

Funcon definitions

Funcon introduces a declaration of a fresh funcon name, together with its signature.

Alias introduces an equation n1 = n2 that declares a fresh name n1 and defines it to be equivalent to another name n2. n1 is usually an abbreviation for a longer n2; its declaration as an alias prevents it from being defined elsewhere to have a different interpretation.

Built-in introduces a declaration of a fresh funcon name and its signature, but does not provide a definition for it. Built-ins can be regarded as parameters of a collection of funcon definitions. They are generally reserved for types of values such as integers, sets, and maps, which are not amenable to specification using operational rules.

Auxiliary introduces a name that is not intended for direct use in language definitions.

Rule introduces a formula or inference rule defining the operational behaviour of a funcon.

Assert introduces a formula that expresses the intention that it should hold (either as a consequence of specified definitions, or as a requirement for built-ins).

Entities

Entity introduces a declaration of a fresh auxiliary entity name.