FO[Unit] ?

Note

This extension is work-in-progress.

Goal

This extension allows the use of synonyms for types INT and REAL, annotated with units of measurerement (e.g., kg). It also checks that equations are correct in their use of units of measure.

Lexicon

Token	Pattern	Example
UNIT	[^\W\d_]+(\d+|²|³)?	m2, m², Ω

Syntax

  TypeInterpretation ← REAL '[' Units ']';
    Units ← UNIT {UNIT} ['/' UNIT {UNIT} ];
    Units ← '1' '/' UNIT {UNIT};
  Identifier ← REALVAL '[' Units ']';

Well-formedness

1. UNIT are one of the 7 base units and the 22 derived units in the International System of Units (SI), with multiplying prefixes (e.g., M) and power suffix. Another 14 commonly-used non-SI units are also accepted.

2. Only numbers of the same type and comparable unit of measure can be added / substracted / compared. The multiplying prefixes are handled as usual.

3. The product (resp. division) of numbers of type Real[A] and Real[B] has type Real[A B] (resp. Real[A/B]).

Semantics

The interpretation of the type is the set of reals, annotated with the unit of measurement.

Example

vocabular {
    type Acceleration := Real[m/s²]
    a: () -> Acceleration
}
theory T {
    a() = 1[cm] / 1[s] / 1[s].
}

In every model of T, a has the value 0.01[m/s²].