[m-dev.] for review: add support for existential types [3/4]

[David Glen JEFFERY]

On 30-Jun-1998, Fergus Henderson <fjh at cs.mu.OZ.AU> wrote:
> [continued from part 2]
> 
> Index: compiler/prog_io.m
> ===================================================================
> RCS file: /home/mercury1/repository/mercury/compiler/prog_io.m,v
> retrieving revision 1.173
> diff -u -r1.173 prog_io.m
> --- prog_io.m	1998/05/30 12:25:45	1.173
> +++ prog_io.m	1998/06/29 09:26:14
>  
> +:- type decl_attribute
> +	--->	purity(purity)
> +	;	quantifier(quantifier_type, list(tvar))
> +	;	constraints(quantifier_type, term).
> +
> +:- type quantifier_type
> +	--->	exist
> +	;	univ.
> +
> +:- type decl_attrs == list(pair(decl_attribute, term)).

Could you please add a comment here saying what exactly the "term" is?

> +	% XXX we should check that `TVars' is of the
> +	%     appropriate form (i.e. a list of variables)

Does this get checked elsewhere? If so, you should add a comment saying so. If
not, you should fix the code.

> +parse_decl_attribute("all", [TVars, Decl],
> +		quantifier(univ, TVarsList), Decl) :-
> +	% XXX we should check that `TVars' is of the
> +	%     appropriate form (i.e. a list of variables)
> +	term__vars(TVars, TVarsList).

Ditto.

> +		% check that all type variables in existential quantifiers
> +		% occur somewhere in the body

I wonder if this is strictly necessary. In any case, I guess it would only
occur if the programmer had made a mistake.

> +	%
> +	% Universal quantification is the default, so we just ignore
> +	% universal quantifiers.  (It might be a good idea to check
> +	% that any universally quantified type variables do actually
> +	% occur somewhere in the type declaration, and are not also
> +	% existentially quantified, and if not, issue a warning or
> +	% error message.)

We should definately check that any universally quantified type vars aren't
also existentially quantified. Could you `XXX' that please?

> Index: compiler/switch_detection.m
> ===================================================================
> RCS file: /home/mercury1/repository/mercury/compiler/switch_detection.m,v
> retrieving revision 1.83
> diff -u -r1.83 switch_detection.m
> --- switch_detection.m	1998/06/09 02:14:48	1.83
> +++ switch_detection.m	1998/06/29 09:26:24
> @@ -227,7 +227,8 @@

This change isn't mentioned in the log message. Is it meant to be part of this
commit?

> Index: compiler/typecheck.m
> ===================================================================
> RCS file: /home/mercury1/repository/mercury/compiler/typecheck.m,v
> retrieving revision 1.242
> diff -u -r1.242 typecheck.m
> --- typecheck.m	1998/06/23 05:42:17	1.242
> +++ typecheck.m	1998/06/29 14:34:09
>
> +		; % Inferring = no
> +			pred_info_set_head_type_params(PredInfo4,
> +				HeadTypeParams2, PredInfo5),
> +
> +			%
> +			% leave the original argtypes etc., but 
> +			% apply any substititions that map existentially
> +			% quantified type variables to other type vars,
> +			% and then rename them all to match the new typevarset,
> +			% so that the type variables names match up
> +			% (e.g. with the type variables in the
> +			% constraint_proofs)
> +			%

Why does this need special handling?

That's part 3 of 4. More to come.


love and cuddles,
dgj
-- 
David Jeffery (dgj at cs.mu.oz.au) |  Marge: Did you just call everyone "chicken"?
PhD student,                    |  Homer: Noooo.  I swear on this Bible!
Department of Computer Science  |  Marge: That's not a Bible; that's a book of
University of Melbourne         |         carpet samples!
Australia                       |  Homer: Ooooh... Fuzzy.