HOL Light 语法

C* 源文件中反引号之间的内容分三个阶段读取。 词法分析器 把字符流切分为词法单元，采取贪婪策略，尽可能匹配最长的字母数字或符号词法单元。 语法分析器 把词法单元转换为预类型或预项，其依据是一张中缀运算符、绑定子与前缀运算符的表格，理论可以在运行时扩展这张表。 随后的 类型检查 把预类型转换为 hol_typehol_type、把预项转换为 termterm，其间解析重载常量，并通过类型推断补全隐式类型。

本页给出 C* 从 HOL Light 继承的这三个阶段的规范。 这里的内容都不是 C* 特有的；C* 增补的常量、字面量与约定见 C* 的扩展。

词法分析器读入 ASCII 输入流，并把它切分为词法单元。 其做法基本是标准的：在每个位置先跳过空白，再取出同一字符类中最长的一段连续字符。

• 空白：空格、制表符（\t\t）、换行符（\n\n）、回车符（\r\r）。空白用于分隔词法单元，除此之外没有意义。
• 分隔符：逗号 ,, 与分号 ;;。二者各自成为一个词法单元，绝不与相邻字符合并。
• 括号：( ) [ ] { }( ) [ ] { }。每一个都自成一个词法单元。
• 符号字符：\ ! @ # $ % ^ & * - + | < = > / ? ~ . :\ ! @ # $ % ^ & * - + | < = > / ? ~ . :
• 字母数字字符：AA–ZZ、aa–zz、00–99、下划线 __ 与单引号 ''。
• 数字：00–99。

注意单引号 '' 属于字母数字字符，而非字符串定界符：HOL Light 没有字符字面量，'a'a 是一个普通标识符（按惯例用作类型变量）。

凡不是括号、分隔符或保留字的词法单元都是标识符，共有两类：

1. 字母数字标识符是一段最长的连续字母数字字符：xx、ListList、appendappend、x1x1、Is_ZeroIs_Zero、_foo_foo、__init__init。
2. 符号标识符是一段最长的连续符号字符：++、==>==>、!!!!、|->|->、****。

由于采用最长匹配，相邻的符号字符会融合为一个词法单元：x**yx**y 的词法分析结果是 xx、****、yy，而 x* *yx* *y 的结果是 xx、**、**、yy。 因此空白只在符号运算符之间才具有意义，别处则无关紧要。

保留字是不能用作标识符的词法单元。 默认的集合为：

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

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

这个集合并非由语言固定：理论可以保留更多的词，HOL Light 自身的库在引入新语法时就会这样做。 其余的一切——包括下面优先级表中的各个运算符——都只是附带了语法分析状态的普通标识符。

字符串字面量是词法分析器唯一特殊处理的字面量。 它们用双引号 "" 括起，并支持常见的转义：\n\n、\t\t、\"\"、\\\\，以及形如 \031\031 的十进制字符编码。 字符串字面量在项的语法分析阶段展开为 char listchar list（参见 §项的形式）。

类型先被解析为预类型，再经检查并转换为逻辑类型。 类型写在冒号之后，既可以作为项上的类型标注（t:tyt:ty），也可以作为独立的类型引述（`:ty``:ty`）。

类型的核心抽象语法，即 HOL Light 的 hol_typehol_type，恰好有两个构造子：

• Tyvar of stringTyvar of string —— 类型变量，如 'a'a 或 AA。
• Tyapp of string * hol_type listTyapp of string * hol_type list —— 应用于一组参数的类型构造子，如 boolbool（Tyapp("bool", [])Tyapp("bool", [])）、num listnum list 或 A -> BA -> B。

下面的每一种语法形式都是这两者之一的语法糖。

标识符当且仅当不是已声明的类型构造子时才被读作类型变量，因此 AA 是变量而 boolbool 是常量；这也意味着新增一个类型定义可能改变旧类型表达式的解析结果。 后缀应用只接受一个参数；元数更高的构造子则把参数写成用括号包围、以逗号分隔的元组，置于构造子名字之前。 有限类型 :1:1、:2:2、…… 是类型层面的数值，用作 cartcart 构造子的索引类型，从而给出定长向量。

由紧到松依次为：

1. 原子类型——标识符、有限类型、带括号的类型以及元组前缀；
2. 后缀类型应用 ty conty con；
3. 笛卡尔幂 ^^，左结合；
4. 积 ##，右结合；
5. 和 ++，右结合；
6. 函数 ->->，右结合。

:(int)list -> hprop

:(int)list -> hprop

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

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

类型常量 hprophprop、ctypectype、struct_namestruct_name、fieldfield，以及缩写 addraddr 与 bytebyte，由 C* 而非 HOL Light 引入；参见 C* 的扩展。

项先被解析为预项，再经过类型推断与检查，转换为逻辑项。

项的核心抽象语法，即 HOL Light 的 termterm，恰好有四个构造子：

• Var of string * hol_typeVar of string * hol_type —— 变量及其类型。
• Const of string * hol_typeConst of string * hol_type —— 常量及其类型。
• Comb of term * termComb of term * term —— 一个项对另一个项的应用（组合）。
• Abs of term * termAbs of term * term —— λ-抽象，其第一个分量是一个变量。

标识符成为 VarVar 还是 ConstConst 并非词法问题：这在类型推断与检查阶段决定，取决于该名字在当前理论中是否为已声明的常量。

中缀运算符的解析由一张表格驱动，理论在扩充过程中会不断扩展这张表。 优先级数字越大，结合力越强。 没有优先级数字的行沿用上一行的层级。

有两种形式不在表中。 函数应用的结合力强于所有中缀运算符：f x + yf x + y 即 (f x) + y(f x) + y，f x yf x y 即 (f x) y(f x) y。 类型标注 t:tyt:ty 的结合力强于所有中缀运算符，但弱于应用，因此 f x:intf x:int 标注的是应用 f xf x；若只想标注参数本身，必须加括号写成 f (x:int)f (x:int)。

由紧到松，项可以是下列形式之一。

原子项。

• 变量与常量：任何未被解析为关键字、绑定子或运算符的标识符。它成为 VarVar 还是 ConstConst，在类型推断阶段确定。
• 字面量：双引号括起的字符串字面量，会转换为 char listchar list；十进制、十六进制（0x1f0x1f）或二进制（0b10110b1011）形式的数值字面量，类型为 :num:num；以及 C* 中带 ii 后缀的整数字面量（123i123i），类型为 :int:int。
• 带括号的项：( t )( t )。
• 列表字面量：[ t1; t2; ... ][ t1; t2; ... ]，是 CONSCONS 与 NILNIL 的语法糖。注意分隔符是分号；若用逗号，构造出的则是元组。
• 集合枚举：{ t1, t2, ... }{ t1, t2, ... }，是 INSERTINSERT 与 EMPTYEMPTY 的语法糖。
• 集合概括：标准形式 { x | P }{ x | P }，以及广义形式 { f x | x | P }{ f x | x | P }，后者的中间分量显式列出被绑定的变量。
• 模式匹配：match t with p -> e | ...match t with p -> e | ...，也可以带守卫，写成 match t with p when c -> e | ...match t with p when c -> e | ...。functionfunction 形式则对被匹配的项做抽象：function p -> e | ...function p -> e | ...，同样支持 whenwhen 守卫。
• 条件式：if p then t else eif p then t else e。
• let 绑定：let x = t in bodylet x = t in body、函数形式 let f x = t in bodylet f x = t in body，以及并行绑定 let x = t and y = u in bodylet x = t and y = u in body。
• 全域：(:ty)(:ty)，某个类型的全集。

其后依次是绑定子、前缀运算符、应用与中缀运算，各自见下文；中缀的解析遵循 §运算符优先级。

绑定子的写法为

binder v1 ... vn. body

binder v1 ... vn. body

它把 v1v1 到 vnvn 逐一绑定在主体（bodybody）之中，而主体会尽可能向右延伸。 标准的绑定子如下：

例如 \x y. x + y\x y. x + y 是柯里化的加法函数，!n. n > 0!n. n > 0 对所有 nn 做全称量化。 由于主体尽可能向右延伸，!n. P n /\ Q n!n. P n /\ Q n 即 !n. (P n /\ Q n)!n. (P n /\ Q n)；若希望量词的作用域提前结束，必须加括号。 forallforall 与 existsexists 是重载的写法，同时也充当堆量词。

有三个前缀运算符，其结合力强于所有中缀运算符，但弱于应用：

• ~~ —— 逻辑否定，如 ~(x = y)~(x = y)。
• ---- —— 整数取负，如 --1i--1i。它是前缀运算符，而非中缀的 --；x - --1ix - --1i 中的空格不可省略，否则 - --- -- 会融合成一个符号词法单元。
• modmod —— 同余模前缀，与 ==== 配合使用，如 (mod n) x y(mod n) x y。

有若干运算符是重载的：语法分析器先给出一个通用常量，类型检查器再依据类型上下文把它解析为具体的常量。 作用于 :int:int 类型的项时，++ 与 -- 成为 int_addint_add 与 int_subint_sub；作用于 :num:num 时，它们成为自然数上的相应运算。 同样的机制赋予 <<、<=<=、** 等运算符以含义，也正是它让 &&&&、||||、truetrue、falsefalse、forallforall 与 existsexists 既可以表示逻辑常量，也可以表示堆命题常量。 当上下文无法确定类型时，显式的类型标注或带后缀的字面量（写 0i0i 而非 00）可以消除歧义。

变量还可以带有隐式类型：理论可以声明，除非另有说明，具有某个名字的变量就具有某个给定的类型。 C* 借助这一点，使名为 hphp 的变量无需标注即为 :hprop:hprop 类型的堆命题，也使断言的写法符合其本意。

• 反引号内的内容按最长匹配在三类字符上做词法分析——字母数字（含 __ 与 ''）、符号，以及单字符的括号与分隔符；//// 开启注释，绝不可能成为运算符。
• 全数字的词法单元、0x0x/0b0b 形式以及 123i123i 都先被词法分析为普通标识符，只有在项的语法分析阶段才成为数值字面量。
• 类型只有 TyvarTyvar 与 TyappTyapp 两种；应用是后缀形式且结合力最强，其后按结合力递减依次是 ^^（左结合），以及 ##、++、->->（均为右结合）。
• 项只有 VarVar、ConstConst、CombComb、AbsAbs 四种；应用的结合力强于所有中缀运算符，类型标注 t:tyt:ty 介于二者之间；中缀的解析遵循优先级表，其中分离逻辑运算符与各自的逻辑对应形式共享层级。
• 绑定子的形式为 binder v1 ... vn. bodybinder v1 ... vn. body，主体尽可能向右延伸；前缀运算符是 ~~、---- 与 modmod。
• 重载运算符与带隐式类型的变量由类型推断解析，而非由语法分析器解析。