Podnoszenie poziomu błędu taktyki coq

Question

Podczas implementacji złożonej taktyki w Ltacu, istnieje kilka poleceń Ltac lub taktyki, które oczekują na niepowodzenie i gdzie jest to oczekiwane (na przykład zakończenie repeat lub spowodowanie cofnięcia). Te awarie są zwykle wywoływane na poziomie błędu 0.

Błędy wykryte na wyższym poziomie "ucieczki" otaczającego bloku try lub repeat i są przydatne do sygnalizowania nieoczekiwanych awarii.

To, czego mi brakuje, to sposób na prowadzenie taktyki tac i traktowanie jej, nawet na poziomie 0, na wyższym poziomie, przy jednoczesnym zachowaniu komunikatu o niepowodzeniu. Pozwoli mi to upewnić się, że repeat nie kończy się z powodu błędu programowania Ltac na mojej stronie.

Czy mogę wdrożyć taką taktykę wyższego rzędu w Ltac?

Answer 1

Możesz napisać taktykę, aby osiągnąć to w Ocaml. Umieściłem to na GitHub here.

Na przykład następujący powinien podnieść błąd zamiast cicho powodzenia:

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

Answer 2

ja nie wiem, czy to jest możliwe, aby uzyskać dokładnie to, co chcesz, ale ja czasami użyć następującego idiom:

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

Jeżeli pierwsza taktyka nie działa z poziomu 0, a || postara się uruchomić drugi, który zawiedzie na bardzo wysokim poziomie i zgłosi to Tobie.

Pomoże Ci to, jeśli możesz podać konkretny przypadek użycia, aby sprawdzić, czy inna technika byłaby bardziej odpowiednia.