When it comes to raising and catching exceptions, MetaPRL expects its modules to observe certain rules. This section describes the rules you'll need to follow to make sure your code does not change the system behavior in any unwanted way.
Raising. In MetaPRL, Invalid_argument exceptions is a canonical way to notify user about potential bugs in the system. And more generally, when something happens that prohibits your code from returning a sensible answer and you believe that user has to be notified, raise Invalid_argument. To be more precise, you should raise an Invalid_argument in following cases:
However if it makes sense to call your functions with some class of inputs even if the function will not necessarily be successful on these inputs (for example, it may make sense to call the unify function even if you are not sure whether the terms are unifiable), then it may be reasonable to not consider such calls to be a bug and raise RefineError exception instead of Invalid_argument.
Catching. We need to make sure that whenever an Invalid_argument is raised, it will go all the way up to the user. Because of that, you are not supposed to catch Invalid_argument exceptions. In particular, it means that you are not supposed to use "catch all" try ... with _ -> ... expression.
The same is true for other "serious" exceptions from the Pervasives module. In particular, your code should not catch any of Match_failure, Assert_failure, Out_of_memory, Stack_overflow and Division_by_zero exceptions without a good reason.
Examples: dest_var_term would raise RefineError if its input term is not a variable. unify would raise RefineError if input terms are not unifiable. A primitive tactic would raise RefineError if a rule is not applicable to the current goal.
The orelseT and similar tacticals only "know" about RefineError exceptions. (t1 orelseT t2) would run t2 if and only if t1 raises RefineError exception.
Raising. When a certain proof search or proof refinement procedure can not be applied to the given input, raise RefineError. On the other hand, if you believe that the procedure shouldn't have even been attempted on such an input, raise Invalid_argument to notify the user of a problem. Note that if you are doing a lot of raising and catching of RefineErrors, you may want to consider raising generic_refiner_exn to avoid unnecessary allocation overhead.
Catching. Whenever you are calling something that may raise RefineError, feel free to catch it. Of course, if you procedure has no way of recovering from that error, it would make sense to just let this exception to propagate back up. But there is one restriction - if you catch some RefineErrors, you have to catch them all, not matter what the parameters are. And your code's behavior should not in any way depend on the parameters of the RefineError exception it caught. In short, you have to always use try ... with RefineError _ -> ... for catching RefineError exceptions. This limitation makes it possible to increase efficiency by replacing some common RefineError exceptions with with generic_refiner_exn.
Another exception is the low-level code that implements some basic operations or basic data structures and is located below the Refiner in the module hierarchy (for example - all the code in the mllib/ directory). For such code, it's normal to raise one of the standard exceptions, such as Failure or Not_found.
P.S. If your interface function may raise some exception, it may be a good idea to document that in the .mli file and tell in which situations what exceptions would be raised. Of course, you do not have to document obvious things like "this function will raise Invalid_argument if there is a bug or when called with invalid argument" or "This tactic will raise RefineError if proof search fails".