我试图获得一个仅使用 Coq 表示法的解决方案，但无法使其工作。我怀疑 Coq 的可扩展解析器不够强大，无法理解您想要的符号。然而，有一个穷人的解决方案涉及依赖类型。这个想法是为该符号编写一个解析器，并使用该解析器的类型来编码解析器状态。该类型表示解析器“读取”了某个标记（实际上，将该标记作为函数调用的参数），然后进入下一个状态，取决于它刚刚读取的标记。 p>
不过，有一点微妙之处，那就是不能仅使用常规 Coq 函数类型来编写该类型，因为该函数将采用的参数数量取决于它所应用的所有参数。一种解决方案是使用协归纳类型来编码这种行为，声明一个强制使其看起来像一个函数：
Inductive tree (X : Type) : Type :=
| t_a : X -> tree X
| t_m : tree X -> tree X -> tree X.
Arguments t_a {X} _.
Arguments t_m {X} _ _.
CoInductive tree_builder X : nat -> Type :=
| TbDone : tree X -> tree_builder X 0
| TbRead : forall n, (forall o : option X, tree_builder X match o with
| Some x => n
| None => S (S n)
end) ->
tree_builder X (S n).
Arguments TbDone {X} _.
Arguments TbRead {X} _ _.
(* Destructors for tree_builder *)
Definition case0 {X} (x : tree_builder X 0) : tree X :=
match x with
| TbDone t => t
end.
Definition caseS {X n} (x : tree_builder X (S n)) :
forall o : option X, tree_builder X match o with
| Some x => n
| None => S (S n)
end :=
match x with
| TbRead _ f => f
end.
Definition tb X n := tree_builder X (S n).
(* force is what does the magic here: it takes a tb and coerces it to a
function that may produce another tb, depending on what it is applied to. *)
Definition force X n (x : tb X n) : forall o : option X,
match o with
| Some x =>
match n with
| 0 => tree X
| S n' => tb X n'
end
| None =>
tb X (S n)
end :=
fun o =>
match o return tree_builder X match o with
| Some x => n
| None => S (S n)
end ->
match o with
| Some x => match n with
| 0 => tree X
| S n' => tb X n'
end
| None => tb X (S n)
end
with
| Some x => match n return tree_builder X n -> match n with
| 0 => tree X
| S n' => tb X n'
end
with
| 0 => fun t => case0 t
| S _ => fun t => t
end
| None => fun t => t
end (caseS x o).
Coercion force : tb >-> Funclass.
那么，我们的解析器只是tb X 0 类型的术语。正如通常所做的那样，由于参数数量可变，因此必须以连续传递样式编写。
Fixpoint parser_cont_type X (n : nat) : Type :=
match n with
| 0 => tree X
| S n' => tree X -> parser_cont_type X n'
end.
CoFixpoint parser X n : parser_cont_type X n -> tree_builder X n :=
match n with
| 0 => fun k => TbDone k
| S n' => fun k : tree X -> parser_cont_type X n' =>
TbRead n' (fun o => match o return tree_builder X match o with
| Some _ => n'
| None => S (S n')
end
with
| Some x => parser X n' (k (t_a x))
| None => parser X (S (S n')) (fun (t1 t2 : tree X) => k (t_m t1 t2))
end)
end.
Definition parser' X : tb X 0 :=
parser X 1 (fun t => t).
接下来，我们可以定义一些额外的符号以使其更易于使用：
Notation "[ x ]" := (Some x) (at level 0).
Notation "''" := None (at level 0).
Notation "!" := (parser' _) (at level 20).
这是编写示例树的方法，例如：
Definition my_tree : tree nat := Eval hnf in ! '' [1] '' '' [2] [3] [4].
注意初始的! 开始调用解析器，以及标记叶子所需的[]。我也无法让 Coq 的解析器自己接受 ' 作为令牌。但是，除了这些小细节之外，它与您所拥有的非常接近。
一个问题是，由于解析器是使用 Coq 函数定义的，因此需要进行一些简化才能得到一个与您最初的术语完全相同的术语。这就是我在定义上添加Eval 调用的原因。这可能不如真正的符号实用，而且定义确实有点棘手，但在某些情况下它可能非常有用。
这是带有整个 .v 文件的 gist。
更新：我已经写了一个post，其中包含了这种技术的简化版本，使其更通用。