Getting 'any' insts to ground
Bas de Bakker
basde.bakker at pica.nl
Mon Nov 10 19:16:30 AEDT 1997
I've been experimenting a bit with the new 'any' inst, but I'm running
into the following problem:
Let's say I have
:- pred fill_list(list(int)).
:- mode fill_list(list_skel(any) -> list_skel(any)) is nondet.
I know that each successful call of fill_list will instantiate exactly
one element of the list, but which one will be hard to predict (and
vary when backtracking).
If I have a list of length N with free variables for all elements, I
can call fill_list N times in a simple recursive predicate. When I've
done this I know that the list is ground, but the compiler doesn't.
But to do something useful with the list, like print it, the compiler
must know it is ground.
In extras/trailed_update/unsafe, there's an "unsafe_promise_ground"
predicate which does what I need, but it's unsafe and can't test
whether my algorithm is correct. I'd like something along the lines
:- pred is_ground(T).
:- mode is_ground(any -> ground) is semidet.
which fails if the term isn't ground, but this is non-logical.
Is there any (logical) way to do this, either in the current Mercury
implementation or just potentially, or is it simply impossible? If
the latter, does anybody have other suggestions?
Bas de Bakker.
More information about the users