menhir-将AST节点与源文件中的令牌位置相关联

我不知道这是否是最佳实践,但我喜欢Frama-C系统抽象语法树中采用的方法;看见 https://github.com/Frama-C/Frama-C-snapshot/blob/master/src/kernel_services/ast_data/cil_types.mli

这种方法使用相互嵌套的记录和代数类型的“层”。这些记录包含元信息,如源位置,以及可以匹配的代数“节点”。

type ...

and exp = { 
  eid: int; (** unique identifier *)
  enode: exp_node; (** the expression itself *)
  eloc: location; (** location of the expression. *)
}

and exp_node =
  | Const      of constant              (** Constant *)
  | Lval       of lval                  (** Lvalue *)
  | UnOp       of unop * exp * typ
  | BinOp      of binop * exp * exp * typ
...

给定一个变量 e 类型 exp e.eloc e.enode

因此,语法上的“顶级”匹配非常简单:

let rec is_const_expr e =
  match e.enode with
  | Const _ -> true
  | Lval _ -> false
  | UnOp (_op, e', _typ) -> is_const_expr e'
  | BinOp (_op, l, r, _typ) -> is_const_expr l && is_const_expr r

要在表达式中进行更深入的匹配,必须在每个级别上遍历一个记录。这会增加一些语法混乱,但不会太多,因为您只能在您感兴趣的一个记录字段上进行模式匹配:

let optimize_double_negation e =
  match e.enode with
  | UnOp (Neg, { enode = UnOp (Neg, e', _) }, _) -> e'
  | _ -> e

let optimize_double_negation e =
  match e.enode with
  | UnOp (Neg, UnOp (Neg, e', _), _) -> e'
  | _ -> e

您需要以某种方式将位置信息附加到节点。通常的解决方案是将AST节点编码为记录,例如。,

type node = 
  | Typedef of typdef
  | Typeexp of typeexp
  | Literal of string
  | Constant of int
  | ...

type annotated_node = { node : node; loc : loc}

由于您使用的是记录,因此您仍然可以在没有太多语法开销的情况下进行模式匹配,例如。,

 match node with
 | {node=Typedef t} -> pp_typedef t
 | ...

根据您的表示,您可以选择单独包装类型的每个分支、包装整个类型,或者递归地包装,如@Isabelle Newbie在Frama-C示例中所示。

一种类似但更通用的方法是扩展节点,而不是使用位置,而只是使用唯一标识符,并使用最终映射向节点添加任意数据。这种方法的好处是,在实际外部化节点属性时,可以使用任意数据扩展节点。缺点是,实际上无法保证属性的总体性,因为有限映射不是总体。因此,很难保持不变,例如,所有节点都有一个位置。

node 事实上,只要每个节点都是堆对象,即节点定义不包含常量构造函数(如果包含常量构造函数,可以通过添加虚假单位值来解决,例如。, | End 可以表示为 | End of unit

当然,我所说的地址并不是指一个物体的物理或虚拟地址。OCaml使用移动GC,因此OCaml对象的实际地址可能在程序执行期间发生变化。此外,地址通常不是唯一的,因为一旦对象被释放,其地址就可以被完全不同的实体抓取。

c1 和 c2 :

let c1 = Literal "hello"
let c2 = Constant 42

module Locations = Ephemeron.K1.Make(struct
   type t = node
   let hash = Hashtbl.hash (* or your own hash if you have one *)
   let equal = (=) (* or a specilized equal operator *)
end)

这个 Locations locations

let locations = Locations.create 1337


(* somewhere in the semantics actions, where c1 and c2 are created *)

Locations.add c1 "hello.ml:12:32"
Locations.add c2 "hello.ml:13:56"

# Locations.find locs c1;;
- : string = "hello.ml:12:32"

正如您所看到的,虽然解决方案在某种意义上很好,它不涉及节点数据类型,因此您的其余代码可以很容易地在其上进行模式匹配,但它仍然有点脏,因为它需要全局可变状态,这很难维护。此外,由于我们使用对象地址作为键,因此每个新创建的对象,即使在逻辑上是从原始对象派生的,也将具有不同的标识。例如,假设您有一个函数,用于规范化所有文字:

let normalize = function
  | Literal str -> Literal (normalize_literal str)
  | node -> node 

它将创建一个新的 Literal 节点从原始节点中删除,因此所有位置信息都将丢失。这意味着,每次从一个节点派生另一个节点时,都需要更新位置信息。

location 表将变空。

说到你在评论中提到的“一元法”。虽然单子很神奇,但它们仍然不能神奇地解决所有问题。它们不是灵丹妙药:)为了将某个东西附加到节点,我们仍然需要使用额外的属性对其进行扩展,这些属性可以是直接的位置信息,也可以是我们可以间接附加属性的标识。不过,单子对于后者很有用,因为我们可以使用状态单子来封装id生成器,而不是对最后分配的标识符进行全局引用。为了完整性起见,您可以使用UUID来获取标识符,而不是使用状态单子或全局引用来生成唯一标识符,这些标识符不仅在程序运行中是唯一的,而且是普遍唯一的,因为世界上没有其他对象具有相同的标识符,无论您运行程序的频率有多高(在理智的世界中)。虽然生成UUID看起来不使用任何状态,但在后台它仍然使用命令随机数生成器,因此这有点欺骗,但仍然可以被视为纯函数,因为它不包含可观察的效果。