A change for varset and term

Thomas Charles CONWAY conway at cs.mu.OZ.AU
Tue Oct 20 14:53:03 AEST 1998


Hi

After just talking with Renaud, the following idea occured to me.
What do people think?

In the library we have the types `var' and `varset'. Although they're
the one type, we use them to represent a number of things including
program variables, type variables and size variables (in termination
analysis). The use of `var' and `varset' are prone to two kinds of
bug: mixing vars that represent two different kinds of thing (eg
program vars and type vars) and mixing vars from two different varsets.
The following proposal would fix the first problem and has a trivial
extension which would fix the second.

Instead of

	:- type varset.
	:- type var.

	:- pred new_varset(varset).
	:- mode new_varset(out) is det.
	...

we have

	:- type varset(T).
	:- type var(T).

	:- pred new_varset(T, varset(T)).
	:- mode new_varset(in, out) is det.
	...

now in the hlds we can use:

	:- type type_var_type	--->	type_var.
	:- type type_var	==	var(type_var_type).

	:- type prog_var_type	--->	prog_var.
	:- type prog_var	==	var(prog_var_type).

Now in varset.m, we make the concrete representation of var(T) be:
	
	:- type var(T)	--->	var(int). % Remember, we can't use an
					  % equivalence here for impl.
					  % reasons!

This has the same runtime representation as the original `var', but
is more typesafe. I think it is worth changing the compiler to do this,
though we might choose to make two new modules: poly_term and poly_varset
in the compiler rather than changing the library (or we could add these
to the library).

The extension is to make the representation of varset include the given `T',
and for `var(T)'s to include it too:

	:- type var(T)	--->	var(int, T).

(The ordering of the arguments is very deliberate here - the comparison
of the variable numbers will usually fail more quickly than the relatively
expensive polymorphic unification for the second argument). This has a
time and space cost but is certainly useful for debugging if for example
we changed prog_var:

	:- type prog_var_type	--->	prog_var(pred_proc_id).
	:- type prog_var	==	var(prog_var_type).

Now, if we try to unify two variables from different varsets the
unification can fail, or even call error (if, for example we use
user defined equality, or explicit calls to unify_var in term.m, etc).

Given that we really only need to change 1 line (the defn of var(T))
to switch between the two, the extra cost of using the extended
version may well be worthwhile during development.

I'd be happy to make the change if the consensus is that it's worthwhile.
Comments?
-- 
Thomas Conway <conway at cs.mu.oz.au>
Nail here [] for new monitor.  )O+



More information about the developers mailing list