[m-rev.] for review: try goals

[Peter Wang]

2009/2/18 Julien Fischer <juliensf at csse.unimelb.edu.au>:
>
> On Wed, 18 Feb 2009, Peter Wang wrote:
>
>> 2009/2/18 Julien Fischer <juliensf at csse.unimelb.edu.au>:
>>>
>>> Hi Peter,
>>>
>>> Here are some initial comments that cover the change to the reference
>>> manual.
>>>
>>> On Tue, 17 Feb 2009, Peter Wang wrote:
>>>
>>>> Branches: main
>>>>
>>>> Add support for `try' goals, syntactic sugar on top of the exception
>>>> handling
>>>> predicates in the standard library.  The syntax is documented in the
>>>> reference
>>>> manual.  Currently one of the proposed try parameters, io(!IO), is
>>>> implemented,
>>>> and the user must import the `exception' and `univ' modules explicitly.
>>>
>>> Is there some reason that add_implict_imports in
>>> compiler/module_imports.m can not be extended to import them if a
>>> module uses a try goal?
>>
>> I didn't know it existed.  I will add it for `exception'.
>
> Yes, it is used for the implicit imports required by tabling and STM.

It now automatically imports `exception'.

>>>
>>> Is the @samp{io} parameter really needed at all?  Can't the compiler
>>> just infer it by the use of I/O state in @var{Goal}?
>>
>> It can.  I originally thought it might make the implementation hard, but
>> actually it shouldn't make much difference.  I can change it later if
>> people
>> think it's a good idea.  The only objection I might have is that it break
>> the
>> parallel with the other proposed try parameters, but those are extremely
>> uncommon whereas try_io is even more common than plain try.
>
> The only other proposed try parameters I can think of are store/0 and
> the STM state - it ought to be able to infer both of those as well.
> (Certainly the latter.)

That leaves only "try [all(Solutions)]", which actually needs to be
"try [all(Output, Solutions)]" so we know what to collect.  On the other
hand it's not common enough to provide special syntax, and I don't feel
like implementing it ;-)

Ian had an idea to supply the name of the "try" predicate yourself;
something like "try [pred(foo.bar)]" I suppose.  You could use the try
syntax to enclose blocks of code which need to be run in a particular context,
e.g. a database transaction.  The details are not worked out yet but this
could be generally useful so I think the parameter list should stay, even if
it'll always be empty right now.

>
> Could you please post an updated version of just the reference manual
> changes.
>

Below.

[also]
> The reference manual should also state an purity restrictions on
> @var{Goal}, @var{ThenGoal}, ... etc.

There are no purity restrictions.  Should there be?

Previously if Goal was non-pure, once it got moved into a lambda
the call to try* would still be pure.  I've now wrapped the try* call
into a promise_semipure/promise_impure scope to match the purity of Goal.

Peter


diff --git a/doc/reference_manual.texi b/doc/reference_manual.texi
index a027612..0cb344f 100644
--- a/doc/reference_manual.texi
+++ b/doc/reference_manual.texi
@@ -96,6 +96,8 @@ into another language, under the above conditions
for modified versions.
 * Type classes::      Constrained polymorphism.
 * Existential types:: Support for data abstraction and heterogeneous
                       collections.
+* Exception handling:: Catching exceptions to recover from exceptional
+                      situations.
 * Semantics::         Declarative and operational semantics of Mercury
                       programs.
 * Foreign language interface:: Calling code written in other programming
@@ -867,6 +869,21 @@ but to be confined to the provision of extra information
 for the user of the program.
 See @ref{Trace goals} for the details.

+ at item @code{try @var{Params} @var{Goal} @dots{} catch @var{Term} ->
@var{CGoal} @dots{}}
+A try goal. Exceptions thrown during the execution of @var{Goal}
+may be caught and handled. A summary of the try goal syntax is:
+
+ at example
+    try @var{Params} @var{Goal}
+    then @var{ThenGoal}
+    else @var{ElseGoal}
+    catch @var{Term} -> @var{CatchGoal}
+    ...
+    catch_any @var{CatchAnyVar} -> @var{CatchAnyGoal}
+ at end example
+
+See @ref{Exception handling} for the full details.
+
 @item @code{@var{Call}}
 Any goal which does not match any of the above forms
 must be a predicate call.
@@ -6136,6 +6153,137 @@ good_example3_univ("foo"::in(bound("foo")),
univ(42)::out).
 good_example3_univ("bar"::in(bound("bar")), univ("blah")::out).
 @end example

+ at node Exception handling
+ at chapter Exception handling
+
+Mercury procedures may throw exceptions.  Exceptions may be caught using
+the predicates defined in the @samp{exception} library module,
+or using try goals.
+
+ at noindent
+A @samp{try} goal has the following form:
+
+ at example
+        try @var{Params} @var{Goal}
+        then @var{ThenGoal}
+        else @var{ElseGoal}
+        catch @var{Term} -> @var{CatchGoal}
+        ...
+        catch_any @var{CatchAnyVar} -> @var{CatchAnyGoal}
+ at end example
+
+ at var{Goal}, @var{ThenGoal}, @var{ElseGoal}, @var{CatchGoal},
+ at var{CatchAnyGoal} must be valid goals.
+
+ at var{Goal} must have one of the following determinisms: @samp{det},
+ at samp{semidet}, @samp{cc_multi}, or @samp{cc_nondet}.
+
+The non-local variables of @var{Goal} must not have an inst equivalent to
+ at samp{unique} or @samp{mostly_unique} or @samp{any}, unless they have the
+type @samp{io.state}.
+ at c or (later) the store/1.)
+
+ at var{Params} must be a valid list of zero or more try parameters.
+
+The ``then'' part is mandatory.
+The ``else'' part is mandatory if @var{Goal} may fail; otherwise it
+must be omitted.
+There may be zero or more ``catch'' branches.
+The ``catch_any'' part is optional.  @var{CatchAnyVar} must be a single
+variable.
+
+The try parameter @samp{io} takes a single argument, which must be the name
+of a state variable prefixed by @samp{!}; for example, @samp{io(!IO)}.
+The state variable must have the type @samp{io.state}, and be in scope
+of the try goal.  The state variable is threaded through @samp{Goal},
+so it may perform I/O but cannot fail.
+If no @samp{io} parameter exists, @samp{Goal} may not perform I/O and may
+fail.
+
+A try goal has determinism @samp{cc_multi}.
+ at c Exception: if all of the then/else/catch/catch_any parts only succeed
+ at c without binding non-local variables then the determinism is det.
+ at c In the implementation we may still infer cc_multi though.
+
+On entering a try goal, @var{Goal} is executed.  If it succeeds
+without throwing an exception, @var{ThenGoal} is executed.
+Any variables bound by @var{Goal} are visible in @var{ThenGoal} only.
+If @var{Goal} fails, then @var{ElseGoal} is executed.
+
+If @var{Goal} throws an exception, the exception value is unified
+with each the @var{Term}s in the ``catch'' branches in turn.
+On the first successful unification, the corresponding @var{CatchGoal} is
+executed (and other ``catch'' and ``catch_any'' branches ignored).
+Variables bound during the unification of the @var{Term} are in scope
+of the corresponding @var{CatchGoal}.
+
+If the exception value does not unify with any of the terms in ``catch''
+branches, and a ``catch_any'' branch is present, the exception is bound
+to @var{CatchAnyVar} and the @var{CatchAnyGoal} executed.
+ at var{CatchAnyVar} is visible in the @var{CatchAnyGoal} only, and
+is existentially typed, i.e. it has type @samp{some [T] T}.
+
+Finally, if the thrown value did not unify with any ``catch'' term,
+and there is no ``catch_any'' branch, the exception is rethrown.
+
+ at noindent
+The declarative semantics of a try goal is:
+
+ at example
+        (try [] Goal
+         then Then
+         else Else
+         catch CP1 -> CG1
+         catch CG2 -> CG2
+         ...
+         catch_any CAV -> CAG
+        )  <=>
+                (
+                        Goal, Then
+                ;
+                        not Goal, Else
+                ;
+                        some [Excp]
+                        ( Excp = CP1 -> CG1
+                        ; Excp = CP2 -> CG2
+                        ; ...
+                        ; Excp = CAV, CAG
+                        )
+                ).
+ at end example
+
+If no @samp{else} branch is present, let @samp{Else = fail}.
+If no @samp{catch_any} branch is present, let @samp{CAG = fail}.
+
+ at noindent
+An example of a try goal that performs I/O is:
+
+ at example
+:- pred p_carefully(io::di, io::uo) is det.
+
+p_carefully(!IO) :-
+        (try [io(!IO)] (
+                io.write_string("Calling p\n", !IO),
+                p(Output, !IO)
+        )
+        then
+                io.write_string("p returned: ", !IO),
+                io.write(Output, !IO),
+                io.nl(!IO)
+        catch S ->
+                io.write_string("p threw a string: ", !IO),
+                io.write_string(S, !IO),
+                io.nl(!IO)
+        catch 42 ->
+                io.write_string("p threw 42\n", !IO)
+        catch_any Other ->
+                io.write_string("p threw something: ", !IO),
+                io.write(Other, !IO),
+                % Rethrow the value.
+                throw(X)
+        ).
+ at end example
+
 @node Semantics
 @chapter Semantics
--------------------------------------------------------------------------
mercury-reviews mailing list
Post messages to:       mercury-reviews at csse.unimelb.edu.au
Administrative Queries: owner-mercury-reviews at csse.unimelb.edu.au
Subscriptions:          mercury-reviews-request at csse.unimelb.edu.au
--------------------------------------------------------------------------