HOL Light Syntax

Everything between backticks in a C* source file is read 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, driven by 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. Nothing here is C*-specific; the constants, literals, and conventions C* adds are the subject of C* Extensions.

The lexer consumes an ASCII input stream and breaks it into tokens. It is largely standard: 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 is a token on its own and never merges with a neighbor.
• Brackets: ( ) [ ] { }( ) [ ] { }. Each is a token on its own.
• Symbolic characters: \ ! @ # $ % ^ & * - + | < = > / ? ~ . :\ ! @ # $ % ^ & * - + | < = > / ? ~ . :
• Alphanumeric characters: AA–ZZ, aa–zz, 00–99, underscore __, and single quote ''.
• Digits: 00–99.

Note that 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 neither a bracket, a separator, nor a reserved word is an identifier, and 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 the match is maximal, adjacent symbolic characters fuse into one token: x**yx**y lexes as xx, ****, yy, while x* *yx* *y lexes as xx, **, **, yy. Whitespace is therefore significant between symbolic operators, and only there.

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

The set is not fixed by the language: a theory may reserve further words, and HOL Light’s own libraries do so as they introduce new syntax. Everything else — including the operators in the precedence table below — is an ordinary identifier that happens to have a parse status attached.

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 sugar for one of these two.

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 and then type-inferred, checked, and 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 not a lexical question: it is decided during type inference and checking, by whether the name is a declared constant in the current theory.

Parsing of infix operators is driven by a table that the theory extends as it grows. A higher precedence number binds tighter. Rows without a precedence number continue the level above them.

Two forms sit outside 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 settled 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. Note 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 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 fuse into one symbolic token.
• modmod — congruence modulus prefix, used with ==== as in (mod n) x y(mod n) x y.

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 gives <<, <=<=, ** and the rest their meaning, and it is what 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 a variable named hphp is a heap proposition of type :hprop:hprop without an annotation, and so that assertions read the way they are meant.

• 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 sits 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 maximally right; ~~, ----, and modmod are the prefixes.
• Overloaded operators and implicitly typed variables are resolved by type inference, not by the parser.