[m-dev.] Re: [HAL-dev] Adding Herbrand types to Mercury
Fergus Henderson
fjh at cs.mu.OZ.AU
Wed Dec 17 12:02:28 AEDT 2003
I missed the start of this thread. The hal-developers list doesn't
appear to be publically archived. Some of the stuff I'm replying to
seems to be descriptions of Mercury as it currently stands, and some of
it appears to be (fragments of) a proposal to extend Mercury, and it's
not clear which is which. So sorry if I am replying to stuff which is
quoted out of context.
On 17-Dec-2003, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> David Overton, Wednesday, 17 December 2003:
> > On Tue, Dec 16, 2003 at 05:40:31PM +1100, Ralph Becket wrote:
> > > The reserve_tag pragma adds an extra data constructor (which I'll call
> > > '$') to the type t and is roughly the same as saying
> > >
> > > :- solver type t
> > > ---> '$'(herbrand_var(t))
> > > ; f
> > > ; g(t)
> > > where equality is unify_t.
> > >
> > > where herbrand_var/1 is a private builtin type that might look like
The reserve_tag pragma in Mercury is equivalent to adding an extra data
constructor, but the Mercury implementation does not know the type or
even the number of arguments to this constructor. The argument might be
herbrand_var/1 or it might be something else. It is not a type defined
in library/private_builtin.m, rather, it is up to the user-defined code
which implements unification for `t'.
> > > where herbrand_var/1 is a private builtin type that might look like
> > > this:
> > >
> > > :- type herbrand_var(T)
> > > ---> free
> > > ; bound(T).
> >
> > The `free' case here is really a reference to a PARMA pointer chain.
> > The `bound(T)' case does not apply because once a variable of type `t'
> > is bound it will be fully dereferenced.
>
> True - I was thinking in terms of traditional Prolog alias structures
> rather than PARMA pointer chains when I wrote the above. But either
> option is good by me.
For traditional Prolog alias structures, you'd need something like this:
:- type herbrand_var(T)
---> free
; alias(herbrand_var(T))
; bound(T).
Or, if you want to be completely traditional, you can drop the "free"
case and represent free variables as self-references, X = alias(X).
> > > The effect of the solver modifier on the transformed type definition for
> > > t is as follows:
> > > - a solver type value with inst *any* is not free and may be any of the
> > > data constructors for the type *including* '$';
> > > - a solver type value with inst *ground* is not free and may be any of
> > > the data constructors for the type *except* '$';
> > > - the inst *any* is identical to the inst *ground* for non-solver
> > > types.
> >
> > Not quite true, because a non-solver type could contain solver types.
> > E.g.
> >
> > :- type foo ---> f(bar).
> > :- solver type bar.
> >
> > inst `any' for type `foo' would be equivalent to `bound(f(any))'.
>
> Okay, so in what I wrote above s/solver type value/solver type value or
> a non-solver type value containing a solver type value/ and s/non-solver
> types/non-solver types that do not contain a solver type value/. Would
> you agree?
No. In particular, there is no requirement that a solver type value
with inst "ground" always be represented by a non-'$' data constructur.
For example, the ground value "f" might be represented as '$'(bound(f))'.
> > It is reasonably easy to check where inits need to be inserted during
> > mode analysis. In fact the Mercury mode checker already does this,
> > although it assumes the init predicate will be called <type>_init_any/1.
> > (See modes.m line 2111.)
>
> Righto. I presume the <type>_init_any/1 predicate is defined in the
> same module as <type>?
Yes.
--
Fergus Henderson <fjh at cs.mu.oz.au> | "I have always known that the pursuit
The University of Melbourne | of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh> | -- the last words of T. S. Garp.
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to: mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions: mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------
More information about the developers
mailing list