Page 148 - 《软件学报》2021年第6期

1722 Journal of Software 软件学报 Vol.32, No.6, June 2021

类型.这 3 个类型检查函数在 Isabelle/HOL 中的类型如表 1 上半部分所示,3 个函数的具体定义相互递归.
表 1 下半部分给出了变量类型环境、函数类型环境和表达式类型检查结果在 Isabelle/HOL 中的形式化类
型.变量类型环境(vte::type_env)将变量标识符映射为变量类型 vtype,包括布尔型、不同位数的无符号整型、有
符号整型等.函数类型环境(fte::ftype_env)将函数标识符映射为函数类型 ftype.其中,函数类型包含函数输入参数
和输出参数类型的列表.
Table 1 Type checking functions and structures
表 1 类型检查函数和函数中包含的结构
type_es :: “type_env⇒id0 set⇒ftype_env⇒expr list⇒(bool×type_env)”
type_b :: “type_env⇒id0 set⇒ftype_env⇒block⇒bool”
type_e :: “type_env⇒id0 set⇒ftype_env⇒expr⇒expr_type_res”
type_env = “vtype list_map” (变量类型环境)
ftype_env = “ftype list_map” (函数类型环境)
expr_type_res = ETypable etype type_env|EUntypable (表达式类型的结果)
vtype = VType type_name (变量类型)
ftype = FType “type_name list” “type_name list” (函数类型)
etype = DataType “type_name list”|StmtType (表达式类型)

表达式结果的类型 expr_type_res 首先包含表达式是否为良类型的信息:若表达式为良类型,则进一步给出
其类型(t::etype)和更新的变量类型环境(vte′::type_env).表达式类型 etype 可以为数据类型(DataType “type_name
list”)或语句类型(StmtType).更新的变量类型环境中包括原有变量到其类型的映射以及在所检查表达式中新声
明变量到其类型的映射.
最后,Yul 语言是分程序语言,允许函数定义的嵌套(在该方面类似 Pascal 语言).对于某个函数定义,其外层
所声明变量在函数体内既不能重新声明,亦不能使用.这与普通代码块嵌套中变量作用域规则不同.因此,为各
个类型检查函数提供外层所声明变量的集合,以帮助进行内层函数定义的类型检查.

4.2 类型检查规则
Isabelle/HOL 中的函数定义可包括多个子句,每个子句对应于所提供参数值的一种情形.类型检查函数
type_e 定义中的一种情形可视为一条类型规则.以下对函数调用表达式的类型规则(如下所示)进行说明.
1. type_e vte xs fte (EFunCall f es)=(
2. case (lm_get(fte@builtin_fte) f) of
3. Some (FType ptl rtl)⇒(
4. if |ptl|=|es| then (
5. let es_no_elist=(foldl(λacc e.(acc∧(not_elist e))) True es) in
6. let es_pts=zip es ptl in
7. let es_res=(foldl(λacc(e,t).
8. (if acc then type_e vte xs fte e=ETypable(DataType[t]) vte else False)) True es_pts)
9. in (if es_no_elist∧es_res then
10. (if |rtl|=0 then ETypable StmtType vte else ETypable(DataType rtl) vte)
11. else EUntypable))
12. else ...)
13. |None⇒EUntypable)
在给定变量类型环境 vte、外层声明变量集合 xs 以及函数环境 fte 下,对函数调用 EFunCall f es 进行类型
检查.首先判断函数类型环境 fte 或内置函数类型环境 builtin_fte 是否将被调函数的标识符 f 映射到某个函数类
型 FType ptl rtl:若该条件满足,进而检查实参列表 es 和形参列表 ptl 的长度是否一致(第 4 行,其中,|ptl|是本文中
表示列表 ptl 长度的直观记号).若此二列表长度相同,则判断实参列表 es 中每个表达式 e 是否都为良类型,且具
有形参列表中所规定的数据类型(第 6 行~第 9 行).本步的实现方法为:先生成列表 es 与 ptl 中对位元素所构成