如何从 GADT / 存在类型的有效负载中提取有用信息?

ELLIOTTCABLE

我正在尝试在生成的解析器中使用Menhir增量解析 API自省 API例如,我想确定与特定 LR(1) 堆栈条目相关联语义值即之前被解析器消耗的令牌。

给定一个抽象的解析检查点,封装在 Menhir 的 type 中'a env,我可以从 LR 自动机中提取一个“堆栈元素”;它看起来像这样:

type element =
  | Element: 'a lr1state * 'a * position * position -> element

type 元素描述了 LR(1) 自动机堆栈中的一个条目。在形式的堆栈元素中Element (s, v, startp, endp)s是(非初始)状态并且v是语义值。该值v与状态的传入符号 A 相关联s换句话说,值v刚好在s进入状态之前被压入堆栈因此,对于某些类型'a,状态s具有类型'a lr1state,值v具有类型'a......

为了对值做任何有用的事情v,必须'a通过检查状态来获得有关类型的信息s到目前为止,该类型'a lr1state是抽象的,因此无法检查s. 检查 API(第 9.3 节)为此提供了更多工具。

好,爽!所以我深入研究了检查 API:

类型 'a 终端是广义代数数据类型 (GADT)。'a 终结符类型的值表示终结符符号(没有语义值)。索引 'a 是与该符号关联的语义值的类型......

type _ terminal =
| T_A : unit terminal
| T_B : int terminal

类型 'a 非终结符也是 GADT。'a 非终结符类型的值表示非终结符符号(没有语义值)。索引 'a 是与该符号关联的语义值的类型......

type _ nonterminal =
| N_main : thing nonterminal

将这些拼凑在一起,我得到如下内容(其中“command”是我的语法的非终结符之一,因此N_command是 a string nonterminal):

let current_command (env : 'a env) =
   let rec f i =
      match Interpreter.get i env with
      | None -> None
      | Some Interpreter.Element (lr1state, v, _startp, _endp) ->
      match Interpreter.incoming_symbol lr1state with
      | Interpreter.N Interpreter.N_command -> Some v
      | _ -> f (i + 1)
   in
   f 0

不幸的是,这给我带来了非常令人困惑的类型错误:

File "src/incremental.ml", line 110, characters 52-53:
Error: This expression has type string but an expression was expected of type
         string
       This instance of string is ambiguous:
       it would escape the scope of its equation

这有点超出我的水平!我很确定我明白为什么我不能做我上面尝试做的事情;但我不明白我的选择是什么。事实上,Menhir 手册特别提到了这种复杂性:

此函数可用于访问v堆栈元素中的语义值Element (s, v, _, _)事实上,通过对符号的案例分析incoming_symbol s,我们可以获得关于类型的信息'a,因此可以获得对值做一些有用的事情的能力v

好的,但这就是我认为我所做的,上面:案例分析通过match继续incoming_symbol s,拉出案例 wherev是单个特定类型:string

tl; dr:我如何从这个 GADT 中提取字符串有效负载,并用它做一些有用的事情?

八时

如果你的错误听起来像

这个字符串实例是不明确的:它会超出其等式的范围

这意味着类型检查器并不确定在模式匹配分支之外的类型是否v应该是字符串,或者是等于string但仅在分支内部的另一种类型您只需要在离开分支时添加类型注释即可消除这种歧义:

 | Interpreter.(N N_command) -> Some (v:string)

本文收集自互联网,转载请注明来源。

如有侵权,请联系 [email protected] 删除。

编辑于
0

我来说两句

0 条评论
登录 后参与评论

相关文章