HOL Light Syntax

C* reads the contents of backticks in a source file in three stages. The lexer turns the character stream into tokens, greedily matching the longest alphanumeric or symbolic token it can. The parser turns tokens into a pretype or a preterm using a table of infix operators, binders, and prefixes that the theory can extend at run time. Type checking then turns the pretype into a hol_typehol_type and the preterm into a termterm, resolving overloaded constants and filling in implicit types by inference.

This page specifies all three stages as C* inherits them from HOL Light, with examples that also use C* syntax. The constants, literals, and conventions C* adds are specified in C* Extensions.

The lexer consumes an ASCII input stream and breaks it into tokens. It follows the usual convention: at each position it skips spaces, then takes the longest run of characters from a single class.

• Spaces: space, tab (\t\t), newline (\n\n), carriage return (\r\r). Spaces separate tokens and are otherwise insignificant.
• Separators: comma ,, and semicolon ;;. Each forms a separate token and never merges with an adjacent character.
• Brackets: ( ) [ ] { }( ) [ ] { }. Each forms a separate token.
• Symbolic characters: \ ! @ # $ % ^ & * - + | < = > / ? ~ . :\ ! @ # $ % ^ & * - + | < = > / ? ~ . :
• Alphanumeric characters: AA–ZZ, aa–zz, 00–99, underscore __, and single quote ''.
• Digits: 00–99.

The single quote '' is an alphanumeric character, not a string delimiter: HOL Light has no character literals, and 'a'a is an ordinary identifier (conventionally a type variable).

A token that is not a bracket, a separator, or a reserved word is an identifier. There are two kinds:

1. An alphanumeric identifier is a maximal run of alphanumeric characters: xx, ListList, appendappend, x1x1, Is_ZeroIs_Zero, _foo_foo, __init__init.
2. A symbolic identifier is a maximal run of symbolic characters: ++, ==>==>, !!!!, |->|->, ****.

Because matching is maximal, adjacent symbolic characters form one token: x**yx**y lexes as xx, ****, yy, while x* *yx* *y lexes as xx, **, **, yy. Whitespace therefore separates alphanumeric tokens as well as symbolic tokens.

Reserved words are tokens that cannot be used as identifiers. The default set is:

(  )  [  ]  {  }
:  ;  .  |
let  in  and  if  then  else
match  with  function  ->  when

(  )  [  ]  {  }
:  ;  .  |
let  in  and  if  then  else
match  with  function  ->  when

A theory may extend this set by reserving further words, as HOL Light’s own libraries do when they introduce new syntax. Everything else — including the operators in the precedence table below — is an ordinary identifier with an associated parse status.

String literals are the only literals the lexer handles specially. They are enclosed in double quotes "" and support the usual escapes: \n\n, \t\t, \"\", \\\\, and decimal character codes such as \031\031. A string literal is expanded during term parsing into a char listchar list (see §Term Forms).

Types are parsed first as pretypes and then checked and converted into logical types. A type is written after a colon, either as a type annotation on a term (t:tyt:ty) or as a standalone type quotation (`:ty``:ty`).

The core abstract syntax for types, HOL Light’s hol_typehol_type, has exactly two constructors:

• Tyvar of stringTyvar of string — a type variable, such as 'a'a or AA.
• Tyapp of string * hol_type listTyapp of string * hol_type list — a type constructor applied to a list of arguments, such as boolbool (Tyapp("bool", [])Tyapp("bool", [])), num listnum list, or A -> BA -> B.

Every syntactic form below is syntactic sugar for one of these two constructors.

An identifier is read as a type variable exactly when it is not a declared type constructor, so AA is a variable while boolbool is a constant; adding a type definition can therefore change how an old type expression parses. Postfix application takes a single argument, and a constructor of higher arity takes its arguments as a parenthesized, comma-separated tuple written before the constructor name. Finite types :1:1, :2:2, … are type-level numerals, used as the index type of the cartcart constructor to give fixed-size vectors.

From tightest to loosest:

1. atomic types — identifiers, finite types, parenthesized types, and tuple prefixes;
2. postfix type application, ty conty con;
3. Cartesian power, ^^, left associative;
4. product, ##, right associative;
5. sum, ++, right associative;
6. function, ->->, right associative.

:(int)list -> hprop

:(int)list -> hprop

Tyapp("fun", [Tyapp("list", [Tyapp("int", [])]); Tyapp("hprop", [])])

Tyapp("fun", [Tyapp("list", [Tyapp("int", [])]); Tyapp("hprop", [])])

The type constants hprophprop, ctypectype, struct_namestruct_name, and fieldfield, and the abbreviations addraddr and bytebyte, are introduced by C* rather than by HOL Light; see C* Extensions.

Terms are parsed as preterms, then undergo type inference and checking before being converted into logical terms.

The core abstract syntax for terms, HOL Light’s termterm, has exactly four constructors:

• Var of string * hol_typeVar of string * hol_type — a variable together with its type.
• Const of string * hol_typeConst of string * hol_type — a constant together with its type.
• Comb of term * termComb of term * term — an application (combination) of one term to another.
• Abs of term * termAbs of term * term — a lambda abstraction, whose first component is a variable.

Whether an identifier becomes a VarVar or a ConstConst is determined during type inference and checking, rather than lexical analysis, by whether the name is a declared constant in the current theory.

Infix parsing uses a table that the theory can extend. A higher precedence number binds tighter. Rows without a precedence number use the preceding level.

Two forms are not listed in the table. Function application binds tighter than every infix operator: f x + yf x + y is (f x) + y(f x) + y, and f x yf x y is (f x) y(f x) y. Type annotation t:tyt:ty binds tighter than every infix but looser than application, so f x:intf x:int annotates the application f xf x, and an annotation on the argument alone must be parenthesized as f (x:int)f (x:int).

From tightest to loosest, a term is one of the following.

Atomic terms.

• Variables and constants: any identifier not parsed as a keyword, a binder, or an operator. Whether it becomes a VarVar or a ConstConst is determined during type inference.
• Literals: string literals in double quotes, converted to a char listchar list; numeric literals in decimal, hexadecimal (0x1f0x1f) or binary (0b10110b1011) form, of type :num:num; and C*‘s integer literals with the ii suffix (123i123i), of type :int:int.
• Parenthesized terms: ( t )( t ).
• List literals: [ t1; t2; ... ][ t1; t2; ... ], sugar for CONSCONS and NILNIL. The separator is a semicolon; a comma would build a tuple instead.
• Set enumerations: { t1, t2, ... }{ t1, t2, ... }, sugar for INSERTINSERT and EMPTYEMPTY.
• Set comprehensions: { x | P }{ x | P } in the standard form, and { f x | x | P }{ f x | x | P } in the generalized form, where the middle component lists the bound variables explicitly.
• Pattern matches: match t with p -> e | ...match t with p -> e | ..., with optional guards written match t with p when c -> e | ...match t with p when c -> e | .... The functionfunction form abstracts over the scrutinee: function p -> e | ...function p -> e | ..., likewise with whenwhen guards.
• Conditionals: if p then t else eif p then t else e.
• Let bindings: let x = t in bodylet x = t in body, the function form let f x = t in bodylet f x = t in body, and parallel bindings let x = t and y = u in bodylet x = t and y = u in body.
• Universe: (:ty)(:ty), the universal set of a type.

Binders, prefixes, application, and infix operations then apply in that order, each described below; infix parsing follows §Operator Precedence.

A binder is written

binder v1 ... vn. body

binder v1 ... vn. body

binding each of v1v1 … vnvn in bodybody, with the body extending as far to the right as possible. The standard binders are:

For example, \x y. x + y\x y. x + y is the curried addition function, and !n. n > 0!n. n > 0 quantifies over all nn. Because the body extends as far to the right as possible, !n. P n /\ Q n!n. P n /\ Q n is !n. (P n /\ Q n)!n. (P n /\ Q n), and a quantifier whose scope should stop earlier must be parenthesized. forallforall and existsexists are the overloaded spellings that also serve as heap quantifiers.

Three prefix operators bind tighter than every infix but looser than application:

• ~~ — logical negation, as in ~(x = y)~(x = y).
• ---- — integer negation, as in --1i--1i. It is a prefix, not the infix --; the space in x - --1ix - --1i matters, since - --- -- would otherwise form one symbolic token.
• modmod — congruence modulus, never written alone: it is the trailing (mod n)(mod n) of a congruence, as in (x == y) (mod n)(x == y) (mod n).

Several operators are overloaded: the parser emits a generic constant, and the type checker resolves it to a specific constant from the type context. ++ and -- on terms of type :int:int become int_addint_add and int_subint_sub; on :num:num they become the natural-number operations. The same mechanism determines the meaning of <<, <=<=, ** and the other operators, and lets &&&&, ||||, truetrue, falsefalse, forallforall, and existsexists denote either logical or heap-proposition constants. When the context does not determine a type, an explicit annotation or a suffixed literal (0i0i rather than 00) resolves the ambiguity.

Variables may also carry implicit types: a theory can declare that variables with a given name have a given type unless stated otherwise. C* uses this so that the variables hphp, hp1hp1, hp2hp2, hp3hp3, hp1'hp1', hp2'hp2', hp3'hp3' are heap propositions of type :hprop:hprop without an annotation, and hpAhpA, hpA'hpA' are :A->hprop:A->hprop; the library uses these names in its rules.

• Backtick contents are lexed with maximal munch over three character classes — alphanumeric (including __ and ''), symbolic, and single-character brackets and separators; //// starts a comment and can never be an operator.
• All-digit tokens, 0x0x/0b0b forms, and 123i123i are lexed as ordinary identifiers and only become numeric literals during term parsing.
• Types are TyvarTyvar or TyappTyapp; application is postfix and tightest, with ^^ (left), then ##, ++, ->-> (all right associative) in decreasing order of tightness.
• Terms are VarVar, ConstConst, CombComb, or AbsAbs; application binds tighter than every infix, type annotation t:tyt:ty has precedence between the two, and infix parsing follows the precedence table, in which the separation-logic operators share levels with their logical counterparts.
• Binders take the form binder v1 ... vn. bodybinder v1 ... vn. body with the body extending as far to the right as possible; ~~, ----, and modmod are the prefixes.
• Overloaded operators and implicitly typed variables are resolved by type inference, not by the parser.