[m-rev.] for review: try goals

[Peter Wang]

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'.

`univ' however is an implementation detail, used I guess for historical reasons.
I'll add private forwarding predicates in `exception' for `univ_value' and
`univ_to_type' so `univ' doesn't need to be imported.

> In the long run it might be nice to redefine the exception_result/1 type
> as:
>
>        :- type exception_result(T)
>                --->    succeeded(T)
>                ;       failed
>                ;       some [E] exception(E).
>
> and do away with the univ there entirely.

Yes.

> > diff --git a/doc/reference_manual.texi b/doc/reference_manual.texi
> > index a027612..93ad1e6 100644
> > --- a/doc/reference_manual.texi
> > +++ b/doc/reference_manual.texi
> > @@ -105,6 +105,7 @@ into another language, under the above conditions
> > for modified versions.
> > * Impurity::          Users can write impure Mercury code.
> > * Trace goals::       Trace goals allow programmers to add debugging and
> >                      logging code to their programs.
> > +* Try goals::         Exception handling.
>
> I think that the new chapter should occur much earlier in the reference
> manual - I suggest placing it just after the ``Existential types''
> chapter.  The name of the chapter should be ``Exception handling'' rather
> than ``Try goals''.

Ok.

> > + at var{CatchAnyGoal} must be valid goals.
>
> @var{Goal} must have one of the following determinisms: det, semidet,
> cc_multi, or cc_nondet.
>
> The non-locals of @var{Goal} must (presumably) not have an inst
> equivalent to (mostly-)unique or any?  (Unless they have the type I/O state
> or (later) the store/1.)
>
> > + at var{Params} must be a valid list of zero or more try parameters.
> > +
> > +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.
>
> 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 above description covers the operational semantics of try goals,
> I think there needs to be a description of their declarative semantics
> as well.  (Like what we have in the library reference manual for
> try and friends.)

This is what Ian and I came up with:

@noindent
The declarative semantics of a try goal without I/O is:

@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
                        )
                ).
@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}.


Peter
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------