I am using constructs like the following for try-catch:
Ltac2 coq_app (func : constr) (arg1 : constr) : constr := Control.plus ( fun (_ : unit) => constr:($func $arg1) ) ( fun (exn : Init.exn) => throw_invalid_argument_scc "coq_app failed to apply: " func arg1 ).
This basically works - when the Coq application fails to type check I get the error message from the throw.
The only issue is that when something fails later - after returning from the function coq_app I still get the error from the coq_app, which is confusing and doesn't follow the usual semantics of a try-catch construct. How would I write this so that the catch block is not entered after the return of the function?
Control.case I believe
I must admit I don't understand the intention behind the signature of
Ltac2 @ external plus : (unit -> 'a) -> (exn -> 'a) -> 'a := "ltac2" "plus". Ltac2 @ external case : (unit -> 'a) -> ('a * (exn -> 'a)) result := "ltac2" "case".
Control.case calls the function given as argument. If it runs fine the
result is the
Val ('a) branch, if it throws it is the
Err (exn) branch. So in the good case I get a
('a * (exn -> 'a)). What am I supposed to do with the
(exn -> 'a) then?
I somehow would either expect the same signature as for plus or
Ltac2 @ external case : (unit -> 'a) -> 'a result := "ltac2" "case".
so that I either get a
'a or an exception.
if there are multiple successes the extra successes are in the exn -> 'a
Indeed. If you drop the continuation it's essentially as if you were wrapping the whole thunk into a
case function is essentially an isomorphism.
You can have a look at the OCaml implementation of
tclORELSE to get an idea of how this works btw.
I see. In the case of the
coq_app function I posted above it would make sense to wrap the thunk into a
once, since the application either type checks or it doesn't. So in this very specific application, I would just ignore the
(exn -> 'a) part?
Last updated: Dec 07 2023 at 09:01 UTC