Hi, I forgot a bit what is the rationale regarding when to use tclZERO
, tclFAIL
, or simply raise
in tactics.
For instance, convert_concl
has a raise NotConvertible
but convert_gen
has tclFailed (str "Not Convertible")
. Is it expected?
Isn't it that tclFAIL
is only for LtacX's fail
(or assimiliated, like LtacX pattern-matching)?
And that in an enter
blocks, it does not matter whether it is tclZERO
or raise
??
raise
in the closure of a Goal.enter is the same as ZERO
(NB the closure is before we go back to the monad, so eg Goal.enter (fun gl -> raise A; tclUNIT () >>= fun () -> raise B)
the raise A
is the same as tclZERO A
but the raise B
will not be properly caught)
Using raise in Goal.enter is perhaps fragile or bad style, but it is done a lot
for zero vs fail I think we generally prefer zero with a custom exception (not tclZERO (UserError Pp.(str "whatever"))
)
There is also that Fail comes with a level which is decreased at each try, right?
So, for convert_gen
(and other places in tactics.ml
), can I consider safe to replace the tclFAIL (str "Not Convertible")
with raise NotConvertible
(which gives the same error message)?
Ah, and there is the question that tclZERO
requires an info while raise
requires nothing, and Loc.raise
requires just a loc.
tclzero does not require an info, it's optional
Hugo Herbelin said:
So, for
convert_gen
(and other places intactics.ml
), can I consider safe to replace thetclFAIL (str "Not Convertible")
withraise NotConvertible
(which gives the same error message)?
I think it's fine
the default level for fail is 1 AFAIK so in try it behaves the same as any other tclZERO (ie the try succeeds doing nothing)
Ok, right. And if I have just a loc, I can also get an info from it. So, tclZERO is enough.
OK thanks, it is for #18106 and I will push something.
Last updated: Oct 13 2024 at 01:02 UTC