Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

tutorial: mention @ltacfail! #509

Merged
merged 2 commits into from
Sep 30, 2023
Merged

tutorial: mention @ltacfail! #509

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
b749a01
tutorial: mention @ltacfail! (fix #501)
gares Sep 29, 2023
7eb7e0d
fix evar count
gares Sep 30, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
47 changes: 44 additions & 3 deletions examples/tutorial_coq_elpi_tactic.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -403,6 +403,47 @@ Lemma test_print (P Q : Prop) (H : P -> Q) (p : P) : Q.
print P, p, (H p). (* .in .messages *)
Abort.

(*|

========
Failure
========

The :builtin:`coq.error` aborts the execution of both
Elpi and any enclosing LTac context. This failure cannot be catched
by LTac.

On the contrary the :builtin:`coq.ltac.fail` builtin can be used to
abort the execution of Elpi code in such a way that LTac can catch it.
This API takes an integer akin to LTac's fail depth together with
the error message to be displayed to the user.

Library functions of the `assert!` family call, by default, :builtin:`coq.error`.
The flag `@ltacfail! N` can be set to alter this behavior and turn erros into
calls to `coq.ltac.fail N`.

|*)

Elpi Tactic abort.
Elpi Accumulate lp:{{
solve _ _ :- coq.error "uncatchable".
}}.

Goal True.
Fail elpi abort || idtac.
Abort.

Elpi Tactic fail.
Elpi Accumulate lp:{{
solve (goal _ _ _ _ [int N]) _ :- coq.ltac.fail N "catchable".
}}.

Goal True.
elpi fail 0 || idtac.
Fail elpi fail 1 || idtac.
Abort.


(*|

========
Expand Down Expand Up @@ -644,13 +685,13 @@ The set of constraints on `evar` represents the Coq data structure called
sigma (sometimes also called evd or evar_map) that is used to
represent the proof state in Coq. It is printed just afterwards:

.. mquote:: .s(elpi show_more).msg{EVARS:*[?]X55*x + 1 = 0*}
.. mquote:: .s(elpi show_more).msg{EVARS:*[?]X57*x + 1 = 0*}
:language: text

.. mquote:: .s(elpi show_more).msg{Coq-Elpi mapping:*RAW:*[?]X55 <-> *X1*ELAB:*[?]X55 <-> *X0*}
.. mquote:: .s(elpi show_more).msg{Coq-Elpi mapping:*RAW:*[?]X57 <-> *X1*ELAB:*[?]X57 <-> *X0*}
:language: text

Here `?X55` is a Coq evar linked with Elpi's :e:`X0` and :e:`X1`.
Here `?X57` is a Coq evar linked with Elpi's :e:`X0` and :e:`X1`.
:e:`X1` represents the goal (the trigger) while :e:`X0` represent the proof.
The meaning of the :e:`evar` Elpi predicate linking the two is that the term
assigned to the trigger :e:`X1` has to be elaborated to the final proof term
Expand Down
1 change: 0 additions & 1 deletion src/coq_elpi_arg_syntax.mlg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,6 @@ open Gramlib
open Pcoq.Constr
open Pcoq.Prim
open Pvernac.Vernac_
open Tacarg
open Pltac

module EA = Coq_elpi_arg_HOAS
Expand Down
Loading