Я попытался получить решение, которое использовало только обозначения Coq, но не могло заставить его работать. Я подозреваю, что расширяемый парсер Coq недостаточно силен, чтобы понять нужную вам нотацию. Однако существует решение бедного человека, которое включает зависимые типы. Идея состоит в том, чтобы написать парсер для этой нотации и использовать этот синтаксический анализатор для кодирования состояния парсера. Тип говорит, что синтаксический анализатор «читает» некоторый токен (фактически, берет этот токен в качестве аргумента для вызова функции) и переходит в следующее состояние: зависит от токена, который он только что прочитал.
Однако есть небольшая тонкость, которая заключается в том, что нельзя писать этот тип, используя только обычные типы функций Coq, потому что количество аргументов, которые будут выполняться, будет зависеть от всех аргументов, к которым оно применяется. Одним из решений является использование coinductive типа для кодирования такое поведение, объявляя принуждение, чтобы сделать его похожим на функции:
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 в определение. Это, вероятно, не так практично, как настоящая нотация, и определение, по общему признанию, немного сложное, но в некоторых случаях это может быть очень полезно.
Вот gist со всем .v файлом.
ОБНОВЛЕНИЕ: Я написал post с упрощенной версией этой техники, сделанной более общей.
Можете ли вы пояснить немного больше, как мы должны интерпретировать это обозначение?Я думаю, что возможно сделать то, что вы хотите, хотя и не только с обозначениями. –
'' 'следует понимать как префиксный оператор, который принимает 2 аргумента и возвращает дерево с первым и вторым аргументами в качестве левого и правого дочерних узлов. – user287393