Stream: Ltac2

Topic: Issues with try-catch via Control.plus

Michael Soegtrop (Feb 02 2022 at 13:33):

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?

Gaëtan Gilbert (Feb 02 2022 at 13:41):

Control.case I believe

Michael Soegtrop (Feb 02 2022 at 15:50):

I must admit I don't understand the intention behind the signature of Control.case:

Ltac2 @ external plus : (unit -> 'a) -> (exn -> 'a) -> 'a := "ltac2" "plus".
Ltac2 @ external case : (unit -> 'a) -> ('a * (exn -> 'a)) result := "ltac2" "case".

I guess 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.

Gaëtan Gilbert (Feb 02 2022 at 15:52):

if there are multiple successes the extra successes are in the exn -> 'a

Pierre-Marie Pédrot (Feb 02 2022 at 15:54):

Indeed. If you drop the continuation it's essentially as if you were wrapping the whole thunk into a once

Pierre-Marie Pédrot (Feb 02 2022 at 15:55):

The case function is essentially an isomorphism.

Pierre-Marie Pédrot (Feb 02 2022 at 15:57):

You can have a look at the OCaml implementation of tclORELSE to get an idea of how this works btw.

Michael Soegtrop (Feb 02 2022 at 16:00):

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: Oct 13 2024 at 01:02 UTC