Повышение уровня неудач тактики coq

При реализации сложной тактики в Ltac есть некоторые команды Ltac или вызов тактики, которые, как я ожидаю, потерпят неудачу и где это ожидается (например, чтобы завершить repeat или вызвать обратное отслеживание). Эти сбои обычно возникают на уровне сбоя 0.

Сбои, возникающие на более высоком уровне, «ускользают» от окружающего блока try или repeat и полезны для сигнализации о неожиданных сбоях.

Чего мне не хватает, так это способа запустить тактику tac и обработать ее неудачу, даже на уровне 0, на более высоком уровне, сохраняя при этом сообщение об ошибке. Это позволило бы мне убедиться, что repeat не завершится из-за ошибки программирования Ltac на моей стороне.

Могу ли я реализовать в Ltac такую ​​тактику более высокого уровня повышения уровня неудач?


coq coq-tactic ltac
person Joachim Breitner    schedule 14.07.2017    source источник

Ответы (2)


arrow_upward
3
arrow_downward

Вы можете написать тактику для достижения этого в Ocaml. Я разместил это на GitHub здесь.

Например, следующее должно вызвать ошибку вместо молчаливого успеха:

repeat (match goal with 
          | [ |- _ ] => 
            raise_error_level (assert (3 = 3) by idtac)
        end).
person Leonidas Lampropoulos    schedule 24.07.2017

arrow_upward
1
arrow_downward

Не знаю, можно ли получить именно то, что вы хотите, но иногда использую такую ​​идиому:

tactic_expression_that_may_fail_with_level_0
|| fail 1000 "There was some problem here"

Если первая тактика не удалась на уровне 0, || попытается запустить вторую, которая потерпит неудачу на очень высоком уровне и сообщит вам об этом.

Было бы полезно, если бы вы могли предоставить конкретный вариант использования, чтобы увидеть, подходит ли какой-либо другой метод лучше.

person Arthur Azevedo De Amorim    schedule 14.07.2017
comment
Ваша работа делает именно то, что я хочу (и я использовал это до сих пор), за исключением того, что я теряю фактическую информацию о сбое уровня 0, что для некоторых тактик на самом деле может быть весьма полезно. - person Joachim Breitner; 14.07.2017