[m-dev.] diff: some stuff for existential data types

Fergus Henderson fjh at cs.mu.OZ.AU
Wed Jun 30 04:19:35 AEST 1999


I'll commit this on the existential types branch.
As usual, any review comments would be most welcome.

--------------------

Estimated hours taken: 12

A few more steps towards proper code generation for existentially-typed
data types.  We should now generate correct code for deconstruction
of existentially-typed data types, I hope.

(Currently type analysis assumes that all unifications with existentially
typed functors are deconstructions rather than constructions, so
attempts to write construction unifications for existentially typed
data type will result in type errors.

RTTI generation for existentially typed data types is probably not
correct, so attempts to use io__print and the like on such types will
probably result in seg faults.)

----------

library/private_builtin.m:
	Add new predicates `typed_unify' and `typed_compare', for use
	by unify_proc.m when unifying and comparing existentially typed
	data types.  These predicates can unify or compare two arguments
	whose types differ; they do this by first comparing the type,
	and then (only if the types are equal) comparing the value.

compiler/unify_proc.m:
	When unifying or comparing existentially typed arguments,
	use `typed_unify' or `typed_compare' rather than ordinary
	unification or comparison.
	Previously the code that we generated for unification and
	comparison predicates of existentially-typed data types
	was not type-correct.

compiler/typecheck.m:
	Ensure that we typecheck special predicates for existentially
	typed data types.  For ordinary data types, the special preds
	are generated with the variable types filled in, but for
	existentially typed data types, this is a bit tricky, so we
	leave it up to type inference to figure out the types.

compiler/unify_proc.m:
	When generating procedure calls, ensure that we generate them
	as fully module-qualified.  This is necessary to avoid potential
	ambiguity errors when typechecking them.

compiler/polymorphism.m:
	When checking for calls to special preds such as compare/3
	that are generated by unify_proc.m, expect a module-qualified
	call rather than an unqualified one.

----------

compiler/polymorphism.m:
	When unifying with an existentially typed data constructor,
	insert the appropriate type_info and type_class_info variables.

compiler/type_util.m:
	Add new predicate type_util__get_existq_cons_defn, similar to the
	existing routine type_util__get_cons_id_arg_types, for use by
	polymorphism.m.

----------

compiler/modecheck_unify.m:
	Ensure that we preserve the original arity of cons_ids.
	This avoids a map__lookup failed when the code generator tries
	to look up the cons_tag for the cons_id in a unification with
	an existentially typed data type.

----------

tests/hard_coded/typeclasses/Mmakefile:
tests/hard_coded/typeclasses/existential_data_types.m:
tests/hard_coded/typeclasses/existential_data_types.exp:
	A test case.

Workspace: /home/mercury0/fjh/mercury-other
Index: compiler/modecheck_unify.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/modecheck_unify.m,v
retrieving revision 1.37.2.5
diff -u -r1.37.2.5 modecheck_unify.m
--- modecheck_unify.m	1999/06/24 17:27:51	1.37.2.5
+++ modecheck_unify.m	1999/06/28 22:01:11
@@ -407,14 +407,13 @@
 	% fully module qualify all cons_ids
 	% (except for builtins such as ints and characters).
 	%
-	list__length(ArgVars0, Arity),
 	(
-		ConsId0 = cons(Name, _),
+		ConsId0 = cons(Name, OrigArity),
 		type_to_type_id(TypeOfX, TypeId, _),
 		TypeId = qualified(TypeModule, _) - _
 	->
 		unqualify_name(Name, UnqualName),
-		ConsId = cons(qualified(TypeModule, UnqualName), Arity)
+		ConsId = cons(qualified(TypeModule, UnqualName), OrigArity)
 	;
 		ConsId = ConsId0
 	),
@@ -478,6 +477,7 @@
 		),
 		(
 			inst_expand(ModuleInfo1, InstOfX, InstOfX1),
+			list__length(ArgVars0, Arity),
 			get_arg_insts(InstOfX1, ConsId, Arity, InstOfXArgs),
 			get_mode_of_args(Inst, InstOfXArgs, ModeOfXArgs0)
 		->
Index: compiler/polymorphism.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/polymorphism.m,v
retrieving revision 1.163.2.7
diff -u -r1.163.2.7 polymorphism.m
--- polymorphism.m	1999/06/29 17:37:22	1.163.2.7
+++ polymorphism.m	1999/06/29 17:37:30
@@ -998,8 +998,11 @@
 	% for which the type is known at compile-time.
 	% Replace such calls with calls to the particular version
 	% for that type.
+	% (Note: higher_order.m also performs the same optimization.
+	% Is there really much advantage in doing it here too?)
 	(
-		{ Name0 = unqualified(PredName0) },
+		{ Name0 = qualified(ModuleName, PredName0) },
+		{ mercury_public_builtin_module(ModuleName) },
 		{ list__length(ArgVars0, Arity) },
 		{ special_pred_name_arity(SpecialPredId, PredName0,
 						MangledPredName, Arity) },
@@ -1349,6 +1352,29 @@
 				PolyInfo1, PolyInfo)
 	;
 		%
+		% is this a construction or deconstruction of an
+		% existentially typed data type?
+		%
+		ConsId0 = cons(_, _),
+		type_util__get_existq_cons_defn(ModuleInfo0, TypeOfX, ConsId0,
+			ConsDefn)
+	->
+		%
+		% add extra arguments to the unification for the
+		% type_info and/or type_class_info variables
+		%
+		map__apply_to_list(ArgVars0, VarTypes0, ActualArgTypes),
+		goal_info_get_context(GoalInfo0, Context),
+		polymorphism__process_existq_unify_functor(ConsDefn,
+			ActualArgTypes, TypeOfX, Context,
+			ExtraVars, ExtraGoals, PolyInfo0, PolyInfo),
+		list__append(ExtraVars, ArgVars0, ArgVars),
+		Unify = unify(X0, functor(ConsId0, ArgVars), Mode0,
+				Unification0, UnifyContext) - GoalInfo0,
+		list__append(ExtraGoals, [Unify], GoalList),
+		conj_list_to_goal(GoalList, GoalInfo0, Goal)
+	;
+		%
 		% ordinary construction/deconstruction unifications
 		% we leave alone
 		%
@@ -1452,6 +1478,111 @@
 	map__det_insert(VarTypes0, Var, Type, VarTypes1),
 	make_fresh_vars(Types, VarSet1, VarTypes1, Vars, VarSet, VarTypes).
 
+%-----------------------------------------------------------------------------%
+
+%
+% compute the extra arguments that we need to add to a unification with
+% an existentially quantified data constructor.
+%
+:- pred polymorphism__process_existq_unify_functor(
+		ctor_defn, list(type), (type), prog_context,
+		list(prog_var), list(hlds_goal), poly_info, poly_info).
+:- mode polymorphism__process_existq_unify_functor(in, in, in, in,
+		out, out, in, out) is det.
+
+polymorphism__process_existq_unify_functor(
+		CtorDefn, ActualArgTypes, ActualRetType, Context,
+		ExtraVars, ExtraGoals, PolyInfo0, PolyInfo) :-
+
+	CtorDefn = ctor_defn(CtorTypeVarSet, ExistQVars0,
+		ExistentialConstraints0, CtorArgTypes0, CtorRetType0),
+
+	%
+	% rename apart the type variables in the constructor definition
+	%
+	poly_info_get_typevarset(PolyInfo0, TypeVarSet0),
+	varset__merge_subst(TypeVarSet0, CtorTypeVarSet, TypeVarSet, Subst),
+	term__var_list_to_term_list(ExistQVars0, ExistQVarTerms0),
+	term__apply_substitution_to_list(ExistQVarTerms0, Subst,
+			ExistQVarsTerms1),
+	apply_subst_to_constraint_list(Subst, ExistentialConstraints0,
+			ExistentialConstraints1),
+	term__apply_substitution_to_list(CtorArgTypes0, Subst, CtorArgTypes1),
+	term__apply_substitution(CtorRetType0, Subst, CtorRetType1),
+	poly_info_set_typevarset(TypeVarSet, PolyInfo0, PolyInfo1),
+
+	%
+	% Compute the type bindings resulting from the functor's actual
+	% argument and return types.
+	% These are the ones that might bind the ExistQVars.
+	%
+	( type_list_subsumes([CtorRetType1 | CtorArgTypes1],
+			[ActualRetType | ActualArgTypes], TypeSubst1) ->
+		TypeSubst = TypeSubst1
+	;
+		error(
+	"polymorphism__process_existq_unify_functor: type unification failed")
+	),
+
+	%
+	% Apply those type bindings to the existential type class constraints
+	%
+	apply_rec_subst_to_constraint_list(TypeSubst, ExistentialConstraints1,
+		ExistentialConstraints),
+
+	%
+	% create type_class_info variables for the
+	% type class constraints
+	%
+	
+	% assume it's a deconstruction
+	polymorphism__make_typeclass_info_head_vars(	
+			ExistentialConstraints, 
+			ExtraTypeClassVars,
+			PolyInfo1, PolyInfo2),
+	ExtraTypeClassGoals = [],
+/*******
+	% assume it's a construction
+	polymorphism__make_typeclass_info_vars(	
+			ExistentialConstraints, [], Context,
+			ExtraTypeClassVars, ExtraTypeClassGoals,
+			PolyInfo1, PolyInfo2),
+*******/
+
+	polymorphism__update_typeclass_infos(
+			ExistentialConstraints, ExtraTypeClassVars,
+			PolyInfo2, PolyInfo3),
+
+	%
+	% Compute the set of _unconstrained_ existentially quantified type
+	% variables, and then apply the type bindings to those type variables
+	% to figure out what types they are bound to.
+	%
+	constraint_list_get_tvars(ExistentialConstraints1,
+			ExistConstrainedTVars),
+	term__var_list_to_term_list(ExistConstrainedTVars,
+			ExistConstrainedTVarTerms),
+	list__delete_elems(ExistQVarsTerms1, ExistConstrainedTVarTerms,
+			UnconstrainedExistQVarTerms),
+	term__apply_rec_substitution_to_list(UnconstrainedExistQVarTerms,
+			TypeSubst, ExistentialTypes),
+
+	%
+	% create type_info variables for the _unconstrained_
+	% existentially quantified type variables
+	%
+	polymorphism__make_type_info_vars(ExistentialTypes, [],
+			Context, ExtraTypeInfoVars, ExtraTypeInfoGoals,
+			PolyInfo3, PolyInfo),
+
+	%
+	% the type_class_info variables go before the type_info variables
+	%
+	list__append(ExtraTypeClassGoals, ExtraTypeInfoGoals, ExtraGoals),
+	list__append(ExtraTypeClassVars, ExtraTypeInfoVars, ExtraVars).
+
+%-----------------------------------------------------------------------------%
+
 :- pred polymorphism__process_c_code(pred_info, int, list(type), list(type),
 	list(maybe(pair(string, mode))), list(maybe(pair(string, mode)))).
 :- mode polymorphism__process_c_code(in, in, in, out, in, out) is det.
@@ -1747,12 +1878,11 @@
 		polymorphism__make_type_info_vars(PredTypes, PredExistQVars,
 			Context, ExtraTypeInfoVars, ExtraTypeInfoGoals,
 			Info4, Info),
-		list__append(ExtraTypeClassVars, ArgVars0, ArgVars1),
-		list__append(ExtraTypeInfoVars, ArgVars1, ArgVars),
 		list__append(ExtraTypeClassGoals, ExtraTypeInfoGoals,
 			ExtraGoals),
 		list__append(ExtraTypeClassVars, ExtraTypeInfoVars,
 			ExtraVars),
+		list__append(ExtraVars, ArgVars0, ArgVars),
 
 		%
 		% update the non-locals
Index: compiler/type_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/type_util.m,v
retrieving revision 1.66.2.1
diff -u -r1.66.2.1 type_util.m
--- type_util.m	1999/06/24 17:28:00	1.66.2.1
+++ type_util.m	1999/06/28 21:45:11
@@ -128,6 +128,24 @@
 :- pred type_util__get_cons_id_arg_types(module_info::in, (type)::in,
 		cons_id::in, list(type)::out) is det.
 
+	% Given a type and a cons_id, look up the definition of that
+	% constructor; if it is existentially typed, return its definition,
+	% otherwise fail.
+:- pred type_util__get_existq_cons_defn(module_info::in,
+		(type)::in, cons_id::in, ctor_defn::out) is semidet.
+
+	% This type is used to return information about a constructor
+	% definition, extracted from the hlds_type_defn and hlds_cons_defn
+	% data types.
+:- type ctor_defn
+	--->	ctor_defn(
+			tvarset,
+			existq_tvars,
+			list(class_constraint),	% existential constraints
+			list(type),	% functor argument types
+			(type)		% functor result type
+		).
+
 	% Given a list of constructors for a type,
 	% check whether that type is a no_tag type
 	% (i.e. one with only one constructor, and
@@ -452,18 +470,42 @@
 				ConsDefn = hlds_cons_defn(_, _, _, TypeId, _)
 			)),
 		list__filter(CorrectCons, ConsDefns,
-			[hlds_cons_defn(_, _, ArgTypes0, _, _)]),
+			[hlds_cons_defn(_ExistQVars0, _Constraints0, ArgTypes0,
+				_, _)]),
 		ArgTypes0 \= []
 	->
 		module_info_types(ModuleInfo, Types),
 		map__lookup(Types, TypeId, TypeDefn),
 		hlds_data__get_type_defn_tparams(TypeDefn, TypeDefnParams),
 		term__term_list_to_var_list(TypeDefnParams, TypeDefnVars),
-		term__substitute_corresponding_list(TypeDefnVars, TypeArgs,
-			ArgTypes0, ArgTypes)
+		% XXX handle ExistQVars
+		map__from_corresponding_lists(TypeDefnVars, TypeArgs, TSubst),
+		term__apply_substitution_to_list(ArgTypes0, TSubst, ArgTypes)
 	;
 		ArgTypes = []
 	).
+
+	% Given a type and a cons_id, look up the definition of that
+	% constructor; if it is existentially typed, return its definition,
+	% otherwise fail.
+type_util__get_existq_cons_defn(ModuleInfo, VarType, ConsId, CtorDefn) :-
+	type_to_type_id(VarType, TypeId, _TypeArgs),
+	module_info_ctors(ModuleInfo, Ctors),
+	% will fail for builtin cons_ids.
+	map__search(Ctors, ConsId, ConsDefns),
+	MatchingCons = lambda([ConsDefn::in] is semidet, (
+			ConsDefn = hlds_cons_defn(_, _, _, TypeId, _)
+		)),
+	list__filter(MatchingCons, ConsDefns,
+		[hlds_cons_defn(ExistQVars, Constraints, ArgTypes, _, _)]),
+	ExistQVars \= [],
+	module_info_types(ModuleInfo, Types),
+	map__lookup(Types, TypeId, TypeDefn),
+	hlds_data__get_type_defn_tvarset(TypeDefn, TypeVarSet),
+	hlds_data__get_type_defn_tparams(TypeDefn, TypeDefnParams),
+	construct_type(TypeId, TypeDefnParams, RetType),
+	CtorDefn = ctor_defn(TypeVarSet, ExistQVars, Constraints,
+		ArgTypes, RetType).
 
 %-----------------------------------------------------------------------------%
 
Index: compiler/typecheck.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/typecheck.m,v
retrieving revision 1.258.2.1
diff -u -r1.258.2.1 typecheck.m
--- typecheck.m	1999/06/10 16:10:52	1.258.2.1
+++ typecheck.m	1999/06/28 15:57:45
@@ -311,9 +311,10 @@
 	    % Compiler-generated predicates are created already type-correct,
 	    % there's no need to typecheck them.  Same for builtins.
 	    % But, compiler-generated unify predicates are not guaranteed
-	    % to be type-correct if they call a user-defined equality pred.
+	    % to be type-correct if they call a user-defined equality pred
+	    % or if it is a special pred for an existentially typed data type.
 	    ( code_util__compiler_generated(PredInfo0),
-	      \+ pred_is_user_defined_equality_pred(PredInfo0, ModuleInfo)
+	      \+ special_pred_needs_typecheck(PredInfo0, ModuleInfo)
 	    ; code_util__predinfo_is_builtin(PredInfo0)
 	    )
 	->
@@ -682,20 +683,31 @@
 	list__append(ArgTypesA, TypesA0, TypesA),
 	list__append(ArgTypesB, TypesB0, TypesB).
 
-:- pred pred_is_user_defined_equality_pred(pred_info::in, module_info::in)
+%
+% A compiler-generated predicate only needs type checking if
+%	(a) it is a user-defined equality pred
+% or	(b) it is the unification or comparison predicate for an
+%           existially quantified type.
+%
+% In case (b), we need to typecheck it to fill in the head_type_params
+% field in the pred_info.
+%
+
+:- pred special_pred_needs_typecheck(pred_info::in, module_info::in)
 	is semidet.
 
-pred_is_user_defined_equality_pred(PredInfo, ModuleInfo) :-
+special_pred_needs_typecheck(PredInfo, ModuleInfo) :-
 	%
-	% check if the predicate is a compiler-generated unification predicate
+	% check if the predicate is a compiler-generated special
+	% predicate
 	%
 	pred_info_name(PredInfo, PredName),
 	pred_info_arity(PredInfo, PredArity),
-	special_pred_name_arity(unify, _, PredName, PredArity),
+	special_pred_name_arity(_, _, PredName, PredArity),
 	%
-	% find out which type it is a unification predicate for,
+	% find out which type it is a special predicate for,
 	% and check whether that type is a type for which there is
-	% a user-defined equality predicate.
+	% a user-defined equality predicate, or which is existentially typed.
 	%
 	pred_info_arg_types(PredInfo, ArgTypes),
 	special_pred_get_type(PredName, ArgTypes, Type),
@@ -703,7 +715,12 @@
 	module_info_types(ModuleInfo, TypeTable),
 	map__lookup(TypeTable, TypeId, TypeDefn),
 	hlds_data__get_type_defn_body(TypeDefn, Body),
-	Body = du_type(_, _, _, yes(_)).
+	Body = du_type(Ctors, _, _, MaybeEqualityPred),
+	(	MaybeEqualityPred = yes(_)
+	;	list__member(Ctor, Ctors),
+		Ctor = ctor(ExistQTVars, _, _, _),
+		ExistQTVars \= []
+	).
 
 %-----------------------------------------------------------------------------%
 
Index: compiler/unify_proc.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/unify_proc.m,v
retrieving revision 1.75.2.1
diff -u -r1.75.2.1 unify_proc.m
--- unify_proc.m	1999/06/10 16:10:56	1.75.2.1
+++ unify_proc.m	1999/06/29 18:15:20
@@ -107,7 +107,7 @@
 %-----------------------------------------------------------------------------%
 
 :- implementation.
-:- import_module tree, map, queue, int, string, require.
+:- import_module tree, map, queue, int, string, require, assoc_list.
 
 :- import_module code_util, code_info, type_util.
 :- import_module mercury_to_mercury, hlds_out.
@@ -640,18 +640,19 @@
 unify_proc__generate_du_unify_clauses([], _H1, _H2, _Context, []) --> [].
 unify_proc__generate_du_unify_clauses([Ctor | Ctors], H1, H2, Context,
 		[Clause | Clauses]) -->
-	{ Ctor = ctor(_ExistQVars, _Constraints, FunctorName, ArgTypes) },
+	{ Ctor = ctor(ExistQTVars, _Constraints, FunctorName, ArgTypes) },
 	{ list__length(ArgTypes, FunctorArity) },
 	{ FunctorConsId = cons(FunctorName, FunctorArity) },
-	unify_proc__make_fresh_vars(ArgTypes, Vars1),
-	unify_proc__make_fresh_vars(ArgTypes, Vars2),
+	unify_proc__make_fresh_vars(ArgTypes, ExistQTVars, Vars1),
+	unify_proc__make_fresh_vars(ArgTypes, ExistQTVars, Vars2),
 	{ create_atomic_unification(
 		H1, functor(FunctorConsId, Vars1), Context, explicit, [], 
 		UnifyH1_Goal) },
 	{ create_atomic_unification(
 		H2, functor(FunctorConsId, Vars2), Context, explicit, [], 
 		UnifyH2_Goal) },
-	{ unify_proc__unify_var_lists(Vars1, Vars2, UnifyArgs_Goal) },
+	unify_proc__unify_var_lists(ArgTypes, ExistQTVars, Vars1, Vars2,
+		UnifyArgs_Goal),
 	{ GoalList = [UnifyH1_Goal, UnifyH2_Goal | UnifyArgs_Goal] },
 	{ goal_info_init(GoalInfo0) },
 	{ goal_info_set_context(GoalInfo0, Context,
@@ -697,10 +698,10 @@
 unify_proc__generate_du_index_clauses([], _X, _Index, _Context, _N, []) --> [].
 unify_proc__generate_du_index_clauses([Ctor | Ctors], X, Index, Context, N,
 		[Clause | Clauses]) -->
-	{ Ctor = ctor(_ExistQVars, _Constraints, FunctorName, ArgTypes) },
+	{ Ctor = ctor(ExistQTVars, _Constraints, FunctorName, ArgTypes) },
 	{ list__length(ArgTypes, FunctorArity) },
 	{ FunctorConsId = cons(FunctorName, FunctorArity) },
-	unify_proc__make_fresh_vars(ArgTypes, ArgVars),
+	unify_proc__make_fresh_vars(ArgTypes, ExistQTVars, ArgVars),
 	{ create_atomic_unification(
 		X, functor(FunctorConsId, ArgVars), Context, explicit, [], 
 		UnifyX_Goal) },
@@ -888,18 +889,19 @@
 	is det.
 
 unify_proc__generate_compare_case(Ctor, R, X, Y, Context, Case) -->
-	{ Ctor = ctor(_ExistQVars, _Constraints, FunctorName, ArgTypes) },
+	{ Ctor = ctor(ExistQTVars, _Constraints, FunctorName, ArgTypes) },
 	{ list__length(ArgTypes, FunctorArity) },
 	{ FunctorConsId = cons(FunctorName, FunctorArity) },
-	unify_proc__make_fresh_vars(ArgTypes, Vars1),
-	unify_proc__make_fresh_vars(ArgTypes, Vars2),
+	unify_proc__make_fresh_vars(ArgTypes, ExistQTVars, Vars1),
+	unify_proc__make_fresh_vars(ArgTypes, ExistQTVars, Vars2),
 	{ create_atomic_unification(
 		X, functor(FunctorConsId, Vars1), Context, explicit, [], 
 		UnifyX_Goal) },
 	{ create_atomic_unification(
 		Y, functor(FunctorConsId, Vars2), Context, explicit, [], 
 		UnifyY_Goal) },
-	unify_proc__compare_args(Vars1, Vars2, R, Context, CompareArgs_Goal),
+	unify_proc__compare_args(ArgTypes, ExistQTVars, Vars1, Vars2,
+		R, Context, CompareArgs_Goal),
 	{ GoalList = [UnifyX_Goal, UnifyY_Goal, CompareArgs_Goal] },
 	{ goal_info_init(GoalInfo0) },
 	{ goal_info_set_context(GoalInfo0, Context,
@@ -932,20 +934,53 @@
 
 */
 
-:- pred unify_proc__compare_args(list(prog_var), list(prog_var), prog_var,
-		prog_context, hlds_goal, unify_proc_info, unify_proc_info).
-:- mode unify_proc__compare_args(in, in, in, in, out, in, out) is det.
+:- pred unify_proc__compare_args(list(constructor_arg), existq_tvars,
+		list(prog_var), list(prog_var), prog_var, prog_context,
+		hlds_goal, unify_proc_info, unify_proc_info).
+:- mode unify_proc__compare_args(in, in, in, in, in, in, out, in, out) is det.
+
+unify_proc__compare_args(ArgTypes, ExistQTVars, Xs, Ys, R, Context, Goal) -->
+	(
+		unify_proc__compare_args_2(ArgTypes, ExistQTVars, Xs, Ys, R,
+			Context, Goal0)
+	->
+		{ Goal = Goal0 }
+	;
+		{ error("unify_proc__compare_args: length mismatch") }
+	).
+
+:- pred unify_proc__compare_args_2(list(constructor_arg), existq_tvars,
+		list(prog_var), list(prog_var), prog_var, prog_context,
+		hlds_goal, unify_proc_info, unify_proc_info).
+:- mode unify_proc__compare_args_2(in, in, in, in, in, in, out, in, out)
+		is semidet.
 
-unify_proc__compare_args([], [], R, Context, Return_Equal) -->
+unify_proc__compare_args_2([], _, [], [], R, Context, Return_Equal) -->
 	{ create_atomic_unification(
 		R, functor(cons(unqualified("="), 0), []),
 		Context, explicit, [], 
 		Return_Equal) }.
-unify_proc__compare_args([X|Xs], [Y|Ys], R, Context, Goal) -->
+unify_proc__compare_args_2([_Name - Type|ArgTypes], ExistQTVars, [X|Xs], [Y|Ys],
+		R, Context, Goal) -->
 	{ goal_info_init(GoalInfo0) },
 	{ goal_info_set_context(GoalInfo0, Context, GoalInfo) },
+	%
+	% When comparing existentially typed arguments, the arguments may
+	% have different types; in that case, rather than just comparing them,
+	% which would be a type error, we call `typed_compare', which is a
+	% builtin that first compares their types and then compares
+	% their values.
+	%
+	{
+		list__member(ExistQTVar, ExistQTVars),
+		term__contains_var(Type, ExistQTVar)
+	->
+		ComparePred = "typed_compare"
+	;
+		ComparePred = "compare"
+	},
 	( { Xs = [], Ys = [] } ->
-		unify_proc__build_call("compare", [R, X, Y], Context, Goal)
+		unify_proc__build_call(ComparePred, [R, X, Y], Context, Goal)
 	;
 		{ mercury_public_builtin_module(MercuryBuiltin) },
 		{ construct_type(
@@ -953,7 +988,7 @@
 			[], ResType) },
 		unify_proc__info_new_var(ResType, R1),
 
-		unify_proc__build_call("compare", [R1, X, Y], Context,
+		unify_proc__build_call(ComparePred, [R1, X, Y], Context,
 			Do_Comparison),
 
 		{ create_atomic_unification(
@@ -969,12 +1004,9 @@
 		{ map__init(Empty) },
 		{ Goal = if_then_else([], Condition, Return_R1, ElseCase, Empty)
 					- GoalInfo},
-		unify_proc__compare_args(Xs, Ys, R, Context, ElseCase)
+		unify_proc__compare_args_2(ArgTypes, ExistQTVars, Xs, Ys, R,
+			Context, ElseCase)
 	).
-unify_proc__compare_args([], [_|_], _, _, _) -->
-	{ error("unify_proc__compare_args: length mismatch") }.
-unify_proc__compare_args([_|_], [], _, _, _) -->
-	{ error("unify_proc__compare_args: length mismatch") }.
 
 %-----------------------------------------------------------------------------%
 
@@ -1013,7 +1045,7 @@
 	},
 	{ hlds_pred__initial_proc_id(ModeId) },
 	{ Call = call(IndexPredId, ModeId, ArgVars, not_builtin,
-			no, unqualified(Name)) },
+			no, qualified(MercuryBuiltin, Name)) },
 	{ goal_info_init(GoalInfo0) },
 	{ goal_info_set_context(GoalInfo0, Context, GoalInfo) },
 	{ Goal = Call - GoalInfo }.
@@ -1021,37 +1053,80 @@
 %-----------------------------------------------------------------------------%
 
 :- pred unify_proc__make_fresh_vars_from_types(list(type), list(prog_var),
-					unify_proc_info, unify_proc_info).
+			unify_proc_info, unify_proc_info).
 :- mode unify_proc__make_fresh_vars_from_types(in, out, in, out) is det.
 
 unify_proc__make_fresh_vars_from_types([], []) --> [].
 unify_proc__make_fresh_vars_from_types([Type | Types], [Var | Vars]) -->
 	unify_proc__info_new_var(Type, Var),
 	unify_proc__make_fresh_vars_from_types(Types, Vars).
+
+:- pred unify_proc__make_fresh_vars(list(constructor_arg), existq_tvars,
+			list(prog_var), unify_proc_info, unify_proc_info).
+:- mode unify_proc__make_fresh_vars(in, in, out, in, out) is det.
+
+unify_proc__make_fresh_vars(CtorArgs, ExistQTVars, Vars) -->
+	( { ExistQTVars = [] } ->
+		{ assoc_list__values(CtorArgs, ArgTypes) },
+		unify_proc__make_fresh_vars_from_types(ArgTypes, Vars)
+	;
+		%
+		% If there are existential types involved, then it's too
+		% hard to get the types right here (it would require
+		% allocating new type variables) -- instead, typecheck.m
+		% will typecheck the clause to figure out the correct types.
+		% So we just allocate the variables and leave it up to
+		% typecheck.m to infer their types.
+		%
+		unify_proc__info_get_varset(VarSet0),
+		{ list__length(CtorArgs, NumVars) },
+		{ varset__new_vars(VarSet0, NumVars, Vars, VarSet) },
+		unify_proc__info_set_varset(VarSet)
+	).
+		
+:- pred unify_proc__unify_var_lists(list(constructor_arg), existq_tvars,
+		list(prog_var), list(prog_var), list(hlds_goal),
+		unify_proc_info, unify_proc_info).
+:- mode unify_proc__unify_var_lists(in, in, in, in, out, in, out) is det.
 
-:- pred unify_proc__make_fresh_vars(list(constructor_arg), list(prog_var),
-					unify_proc_info, unify_proc_info).
-:- mode unify_proc__make_fresh_vars(in, out, in, out) is det.
+unify_proc__unify_var_lists(ArgTypes, ExistQVars, Vars1, Vars2, Goal) -->
+	(
+		unify_proc__unify_var_lists_2(ArgTypes, ExistQVars,
+			Vars1, Vars2, Goal0)
+	->
+		{ Goal = Goal0 }
+	;
+		{ error("unify_proc__unify_var_lists: length mismatch") }
+	).
 
-unify_proc__make_fresh_vars([], []) --> [].
-unify_proc__make_fresh_vars([_Name - Type | Args], [Var | Vars]) -->
-	unify_proc__info_new_var(Type, Var),
-	unify_proc__make_fresh_vars(Args, Vars).
+:- pred unify_proc__unify_var_lists_2(list(constructor_arg), existq_tvars,
+		list(prog_var), list(prog_var), list(hlds_goal),
+		unify_proc_info, unify_proc_info).
+:- mode unify_proc__unify_var_lists_2(in, in, in, in, out, in, out) is semidet.
 
-:- pred unify_proc__unify_var_lists(list(prog_var), list(prog_var),
-		list(hlds_goal)).
-:- mode unify_proc__unify_var_lists(in, in, out) is det.
-
-unify_proc__unify_var_lists([], [_|_], _) :-
-	error("unify_proc__unify_var_lists: length mismatch").
-unify_proc__unify_var_lists([_|_], [], _) :-
-	error("unify_proc__unify_var_lists: length mismatch").
-unify_proc__unify_var_lists([], [], []).
-unify_proc__unify_var_lists([Var1 | Vars1], [Var2 | Vars2], [Goal | Goals]) :-
-	term__context_init(Context),
-	create_atomic_unification(Var1, var(Var2), Context, explicit, [],
-		Goal),
-	unify_proc__unify_var_lists(Vars1, Vars2, Goals).
+unify_proc__unify_var_lists_2([], _, [], [], []) --> [].
+unify_proc__unify_var_lists_2([_Name - Type | ArgTypes], ExistQTVars,
+		[Var1 | Vars1], [Var2 | Vars2], [Goal | Goals]) -->
+	{ term__context_init(Context) },
+	%
+	% When unifying existentially typed arguments, the arguments may
+	% have different types; in that case, rather than just unifying them,
+	% which would be a type error, we call `typed_unify', which is a
+	% builtin that first checks that their types are equal and then
+	% unifies the values.
+	%
+	(
+		{ list__member(ExistQTVar, ExistQTVars) },
+		{ term__contains_var(Type, ExistQTVar) }
+	->
+		unify_proc__build_call("typed_unify", [Var1, Var2], Context,
+			Goal)
+	;
+		{ create_atomic_unification(Var1, var(Var2), Context, explicit,
+			[], Goal) }
+	),
+	unify_proc__unify_var_lists_2(ArgTypes, ExistQTVars, Vars1, Vars2,
+		Goals).
 
 %-----------------------------------------------------------------------------%
 %-----------------------------------------------------------------------------%
Index: library/private_builtin.m
===================================================================
RCS file: /home/mercury1/repository/mercury/library/private_builtin.m,v
retrieving revision 1.25
diff -u -r1.25 private_builtin.m
--- private_builtin.m	1999/06/01 09:45:45	1.25
+++ private_builtin.m	1999/06/28 21:32:37
@@ -37,7 +37,8 @@
 	% should not be used by user programs directly.
 
 	% Changes here may also require changes in compiler/polymorphism.m,
-	% compiler/higher_order.m and runtime/mercury_type_info.{c,h}.
+	% compiler/unify_proc.m, compiler/higher_order.m and
+	% runtime/mercury_type_info.{c,h}.
 
 :- pred builtin_unify_int(int::in, int::in) is semidet.
 :- pred builtin_index_int(int::in, int::out) is det.
@@ -85,6 +86,18 @@
 :- mode builtin_int_gt(in, in) is semidet.
 :- external(builtin_int_gt/2).
 
+	% A "typed" version of unify/2 -- i.e. one that can handle arguments
+	% of different types.  It first unifies their types, and then if
+	% the types are equal it unifies the values.
+:- pred typed_unify(T1, T2).
+:- mode typed_unify(in, in) is semidet.
+
+	% A "typed" version of compare/3 -- i.e. one that can handle arguments
+	% of different types.  It first compares the types, and then if the
+	% types are equal it compares the values.
+:- pred typed_compare(comparison_result, T1, T2).
+:- mode typed_compare(uo, in, in) is det.
+
 %-----------------------------------------------------------------------------%
 
 :- implementation.
@@ -181,6 +194,12 @@
 	% This is used by the code that the compiler generates for compare/3.
 compare_error :-
 	error("internal error in compare/3").
+
+	% XXX These could be implemented more efficiently using
+	%     `pragma c_code' -- the implementation below does some
+	%     unnecessary memory allocatation.
+typed_unify(X, Y) :- univ(X) = univ(Y).
+typed_compare(R, X, Y) :- compare(R, univ(X), univ(Y)).
 
 %-----------------------------------------------------------------------------%
 %-----------------------------------------------------------------------------%
Index: tests/hard_coded/typeclasses/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/hard_coded/typeclasses/Mmakefile,v
retrieving revision 1.16
diff -u -r1.16 Mmakefile
--- Mmakefile	1999/03/17 20:41:47	1.16
+++ Mmakefile	1999/06/28 22:44:20
@@ -10,6 +10,7 @@
 	constrained_lambda \
 	extract_typeinfo \
 	existential_type_classes \
+	existential_data_types \
 	extra_typeinfo \
 	func_default_mode_bug \
 	ho_map \
Index: tests/hard_coded/typeclasses/existential_data_types.exp
===================================================================
RCS file: existential_data_types.exp
diff -N existential_data_types.exp
--- /dev/null	Wed Jun 30 04:06:06 1999
+++ existential_data_types.exp	Tue Jun 29 08:42:07 1999
@@ -0,0 +1,6 @@
+84
+4
+86
+86
+90
+9
Index: tests/hard_coded/typeclasses/existential_data_types.m
===================================================================
RCS file: existential_data_types.m
diff -N existential_data_types.m
--- /dev/null	Wed Jun 30 04:06:06 1999
+++ existential_data_types.m	Tue Jun 29 08:34:59 1999
@@ -0,0 +1,81 @@
+% This test case tests the combination of existential types and
+% type classes, i.e. existential type class constraints.
+
+:- module existential_data_types.
+:- interface.
+:- import_module io.
+
+:- pred main(io__state::di, state::uo) is det.
+
+:- implementation.
+:- import_module std_util, int, string.
+
+:- typeclass fooable(T) where [
+	pred foo(T::in, int::out) is det
+].
+:- typeclass barable(T) where [
+	pred bar(T::in, int::out) is det
+].
+
+:- instance fooable(int) where [
+	pred(foo/2) is int_foo
+].
+
+:- instance fooable(string) where [
+	pred(foo/2) is string_foo
+].
+
+	% my_univ_value(Univ):
+	%	returns the value of the object stored in Univ.
+
+:- type my_univ ---> some [T] make_my_univ(T) => fooable(T).
+
+:- some [T] func my_univ_value(my_univ) = T => fooable(T).
+
+:- func my_univ(T) = my_univ <= fooable(T).
+
+:- some [T] func call_my_univ_value(my_univ) = T => fooable(T).
+
+:- some [T] func my_exist_t = T => fooable(T).
+
+:- some [T] func call_my_exist_t = T => fooable(T).
+
+:- pred int_foo(int::in, int::out) is det.
+int_foo(X, 2*X).
+
+:- pred string_foo(string::in, int::out) is det.
+string_foo(S, N) :- string__length(S, N).
+
+main -->
+	do_foo(42),
+	do_foo("blah"),
+	do_foo(my_exist_t),
+	do_foo(call_my_exist_t),
+	do_foo(my_univ_value(my_univ(45))),
+	do_foo(call_my_univ_value(my_univ("something"))).
+
+:- pred do_foo(T::in, io__state::di, state::uo) is det <= fooable(T).
+do_foo(X) -->
+	{ foo(X, N) },
+	write(N), nl.
+
+call_my_exist_t = my_exist_t.
+
+call_my_univ_value(Univ) = my_univ_value(Univ).
+
+my_exist_t = 43.
+
+my_univ_value(make_my_univ(X)) = X.
+
+/*
+** Construction of existentially typed data types are not yet implemented,
+** so we have to use the C interface.
+*/
+% my_univ(X) = make_my_univ(X).
+:- pragma c_code(my_univ(Value::in) = (Univ::out), will_not_call_mercury, "
+        incr_hp(Univ, 2);
+        field(mktag(0), Univ, 0) = (Word)
+                TypeClassInfo_for_existential_data_types__fooable_T;
+        field(mktag(0), Univ, 1) = (Word) Value;
+
+").

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- 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