[m-rev.] Solver support for abstract equivalence solver types

[Julien Fischer]

On Wed, 1 Dec 2004, Ralph Becket wrote:

> Index: compiler/goal_util.m
> ===================================================================
> RCS file: /home/mercury1/repository/mercury/compiler/goal_util.m,v
> retrieving revision 1.98
> diff -u -r1.98 goal_util.m
> --- compiler/goal_util.m	16 Oct 2004 15:05:51 -0000	1.98
> +++ compiler/goal_util.m	16 Nov 2004 05:14:30 -0000
> @@ -237,6 +237,9 @@
>  :- pred goal_util__generate_unsafe_cast(prog_var::in, prog_var::in,
>  	prog_context::in, hlds_goal::out) is det.
>
> +:- pred goal_util__generate_unsafe_cast(prog_var::in, prog_var::in,
> +	(inst)::in, (inst)::in, prog_context::in, hlds_goal::out) is det.
> +
I think you should add a comment to this predicate about why the version
with the two extra inst arguments is necessary.

...

> Index: compiler/polymorphism.m
> ===================================================================
> RCS file: /home/mercury1/repository/mercury/compiler/polymorphism.m,v
> retrieving revision 1.254
> diff -u -r1.254 polymorphism.m
> --- compiler/polymorphism.m	20 Jul 2004 04:41:04 -0000	1.254
> +++ compiler/polymorphism.m	30 Nov 2004 05:47:09 -0000
> @@ -197,6 +197,15 @@
>  	map(tvar, type_info_locn)::in, unification::in, unification::out,
>  	hlds_goal_info::in, hlds_goal_info::out) is det.
>
> +% Add the type_info variables for a new call goal.  This predicate assumes
> +% that polymorphism__process_module has already been run so the called pred
> +% has already been processed.
> +
> +:- pred polymorphism__process_new_call(pred_id::in, proc_id::in,
> +	list(prog_var)::in, builtin_state::in, maybe(call_unify_context)::in,
> +	sym_name::in, hlds_goal_info::in, hlds_goal::out,
> +	poly_info::in, poly_info::out) is det.
> +
>  % Given a list of types, create a list of variables to hold the type_info
>  % for those types, and create a list of goals to initialize those type_info
>  % variables to the appropriate type_info structures for the types.
> @@ -237,6 +246,12 @@
>  :- pred create_poly_info(module_info::in, pred_info::in,
>  	proc_info::in, poly_info::out) is det.
>
> +	% Extract some fields from a pred_info and proc_info and use them to
> +	% create a poly_info, for use by the polymorphism transformation for
> +	% transforming a new call goal.
> +:- pred create_poly_info_for_call(module_info::in, pred_info::in,
> +	proc_info::in, prog_varset::in, vartypes::in, poly_info::out) is det.
> +
Wouldn't create_poly_info_for_new_call be a more appropriate name for
this?

I'm a bit dubious about how well these changes to the polymorphism
module will work when there are calls to predicates whose arguments
have types that have existentially quantified data constructors that
have typeclass constraints attached to them.

As far as I'm aware the whole matter of solver types and exisential
types, typeclasses etc hasn't really been considered at the moment.
You should put a big XXX comment over these predicates saying that
they are only for use with the code that handles solver types.


>  	% Update the fields in a pred_info and proc_info with
>  	% the values in a poly_info.
>  :- pred poly_info_extract(poly_info::in, pred_info::in, pred_info::out,
> @@ -995,16 +1010,16 @@
>  	GoalExpr = generic_call(_, _, _, _),
>  	Goal = GoalExpr - GoalInfo.
>
> -polymorphism__process_goal_expr(Goal0, GoalInfo0, Goal, !Info) :-
> -	PredId = Goal0 ^ call_pred_id,
> -	ArgVars0 = Goal0 ^ call_args,
> +polymorphism__process_goal_expr(GoalExpr, GoalInfo0, Goal, !Info) :-
> +	GoalExpr = call(PredId, ProcId, ArgVars0, BuiltinState,
> +			MaybeCallUnifyContext, SymName),
>  	polymorphism__process_call(PredId, ArgVars0, GoalInfo0, GoalInfo,
>  		ExtraVars, ExtraGoals, !Info),
>  	ArgVars = ExtraVars ++ ArgVars0,
> -	CallExpr = Goal0 ^ call_args := ArgVars,
> -	Call = CallExpr - GoalInfo,
> -	list__append(ExtraGoals, [Call], GoalList),
> -	conj_list_to_goal(GoalList, GoalInfo0, Goal).
> +	CallExpr = call(PredId, ProcId, ArgVars, BuiltinState,
> +			MaybeCallUnifyContext, SymName),
> +	CallGoal = CallExpr - GoalInfo,
> +	conj_list_to_goal(ExtraGoals ++ [CallGoal], GoalInfo, Goal).
>
>  polymorphism__process_goal_expr(Goal0, GoalInfo0, Goal, !Info) :-
>  	Goal0 = foreign_proc(_, PredId, _, _, _, _),
> @@ -1864,6 +1879,107 @@
>  		goal_info_set_nonlocals(GoalInfo0, NonLocals, GoalInfo)
>  	).
>
> +%-----------------------------------------------------------------------------%
> +
> +polymorphism__process_new_call(PredId, ProcId, CallArgs0, BuiltinState,
> +		MaybeCallUnifyContext, SymName, GoalInfo0, Goal, !Info) :-
> +	poly_info_get_var_types(!.Info, CallVarTypes),
> +	poly_info_get_typevarset(!.Info, CallTypeVarSet0),
> +	poly_info_get_pred_info(!.Info, PredInfo),
> +	pred_info_arg_types(PredInfo, PredArgTypes),
> +
> +		% Work out the types of the provided call args.
> +		%
> +	CallArgTypes0 = map__apply_to_list(CallArgs0, CallVarTypes),
> +
> +		% Work out how many type_info args we need to prepend.
> +		%
> +	NCallArgs0 = length(CallArgTypes0),
> +	NPredArgs  = length(PredArgTypes),
I'd module-qualify those calls to length. It shouldn't matter but
intermodule optimization sometimes complains about type ambiguities if
you don't.

> +	NExtraArgs = NPredArgs - NCallArgs0,
> +
> +		% Construct a fresh type var for each extra type_info
> +		% we need to prepend.
> +		%
> +		% That is, for every such type_info we construct a new
> +		% type variable ExtraTypeTypeVar which we will bind to a
> +		% term private_builtin.type_info(ExtraArgTypeParam),
> +		% where ExtraArgTypeParam is also a new type variable.
> +		%
> +	varset__new_vars(CallTypeVarSet0, NExtraArgs, ExtraArgTypeVars,
> +		CallTypeVarSet1),
> +	list__map2_foldl(bind_type_var_to_type_info_wrapper,
> +		ExtraArgTypeVars, ExtraArgTypes0, ExtraArgTypeParams0,
> +		CallTypeVarSet1, _CallTypeVarSet),
> +
> +		% Prepend the list of types to the call arg types and unify
> +		% the resulting list with the pred arg types.  This should
> +		% result in the earlier fresh ExtraArgTypeParams being unified
> +		% with the types for which we need to construct type_infos.
> +		%
> +	CallArgTypes = ExtraArgTypes0 ++ CallArgTypes0,
> +	unify_corresponding_types(PredArgTypes, CallArgTypes,
> +		map__init, Substitution),
> +	ExtraArgTypeParams = term__apply_rec_substitution_to_list(
> +				ExtraArgTypeParams0, Substitution),
> +
> +		% And finally construct the type_info goals and args we
> +		% need to prepend to complete the call.
> +		%
> +	Ctxt = term__context_init,
> +	make_type_info_vars(ExtraArgTypeParams, Ctxt, ExtraArgs, ExtraGoals,
> +		!Info),
> +	CallArgs = ExtraArgs ++ CallArgs0,
> +	goal_info_get_nonlocals(GoalInfo0, NonLocals0),
> +	NonLocals1 = set__list_to_set(ExtraArgs),
> +	NonLocals = set__union(NonLocals0, NonLocals1),
> +	goal_info_set_nonlocals(GoalInfo0, NonLocals, GoalInfo),
> +	CallGoalExpr = call(PredId, ProcId, CallArgs, BuiltinState,
> +		MaybeCallUnifyContext, SymName),
> +	CallGoal = CallGoalExpr - GoalInfo,
> +	conj_list_to_goal(ExtraGoals ++ [CallGoal], GoalInfo, Goal).
> +
> +
> +	% bind_type_var_to_type_info_wrapper(X, Type, Param, VarSet0, VarSet)
> +	% constructs a new type var Param and binds X to the Type form of
> +	% `private_builtin.type_info(Param)'.
> +	%
> +:- pred bind_type_var_to_type_info_wrapper(tvar::in, (type)::out, (type)::out,
> +	tvarset::in, tvarset::out) is det.
> +
> +bind_type_var_to_type_info_wrapper(X, Type, Param, TVarSet0, TVarSet) :-
> +	varset__new_var(TVarSet0, Y, TVarSet1),
> +	Param = variable(Y),
> +	Ctxt  = term__context_init,
> +	Type  = functor(atom("."),
> +			[ functor(atom("private_builtin"), [], Ctxt),
> +			  functor(atom("type_info"), [Param], Ctxt) ],
> +			Ctxt),
> +	varset__bind_var(TVarSet1, X, Type, TVarSet).
> +
> +
> +:- pred unify_corresponding_types(list(type)::in, list(type)::in,
> +		tsubst::in, tsubst::out) is det.
> +
> +unify_corresponding_types([], [], !Subst).
> +unify_corresponding_types([], [_ | _], !Subst) :-
> +	error("polymorphism__unify_corresponding_types: " ++
> +		"differing list lengths").
> +unify_corresponding_types([_ | _], [], !Subst) :-
> +	error("polymorphism__unify_corresponding_types: " ++
> +		"differing list lengths").
> +unify_corresponding_types([A | As], [B | Bs], !Subst) :-
> +	(
> +		term__unify(A, B, !Subst)
> +	->
> +		unify_corresponding_types(As, Bs, !Subst)
> +	;
> +		error("polymorphism__unify_corresponding_types: " ++
> +			"term__unify failed")
> +	).
> +
> +%-----------------------------------------------------------------------------%
> +
>  :- pred polymorphism__update_typeclass_infos(list(class_constraint)::in,
>  	list(prog_var)::in, poly_info::in, poly_info::out) is det.
>
> @@ -3321,6 +3437,17 @@
>  	pred_info_get_constraint_proofs(PredInfo, Proofs),
>  	proc_info_varset(ProcInfo, VarSet),
>  	proc_info_vartypes(ProcInfo, VarTypes),
> +	proc_info_typeinfo_varmap(ProcInfo, TypeInfoMap),
> +	proc_info_typeclass_info_varmap(ProcInfo, TypeClassInfoMap),
> +	PolyInfo = poly_info(VarSet, VarTypes, TypeVarSet, TypeInfoMap,
> +		TypeClassInfoMap, Proofs, PredInfo, ModuleInfo).
> +
> +	% create_poly_info creates a poly_info for a call.
> +	% (See also init_poly_info.)
> +create_poly_info_for_call(ModuleInfo, PredInfo, ProcInfo, VarSet, VarTypes,
> +		PolyInfo) :-
> +	pred_info_typevarset(PredInfo, TypeVarSet),
> +	pred_info_get_constraint_proofs(PredInfo, Proofs),
>  	proc_info_typeinfo_varmap(ProcInfo, TypeInfoMap),
>  	proc_info_typeclass_info_varmap(ProcInfo, TypeClassInfoMap),
>  	PolyInfo = poly_info(VarSet, VarTypes, TypeVarSet, TypeInfoMap,
...
> Index: compiler/unify_proc.m
> ===================================================================
> RCS file: /home/mercury1/repository/mercury/compiler/unify_proc.m,v
> retrieving revision 1.140
> diff -u -r1.140 unify_proc.m
> --- compiler/unify_proc.m	5 Sep 2004 23:52:49 -0000	1.140
> +++ compiler/unify_proc.m	17 Nov 2004 06:40:33 -0000
> @@ -733,7 +733,44 @@
>  		unify_proc__quantify_clauses_body([X], Goal, Context, Clauses,
>  			!Info)
>  	;
> -		error("trying to create initialisation proc for type " ++
> +		% If this is an equivalence type then we just generate a
> +		% call to the initialisation pred of the type on the RHS
> +		% of the equivalence and cast the result back to the type
> +		% on the LHS of the equivalence.
> +		TypeBody = eqv_type(EqvType)
> +	->
> +		goal_info_init(Context, GoalInfo),
> +		unify_proc__make_fresh_named_var_from_type(EqvType,
> +			"PreCast_HeadVar", 1, X0, !Info),
> +		(
> +			type_to_ctor_and_args(EqvType, TypeCtor0, _TypeArgs)
> +		->
> +			TypeCtor = TypeCtor0
> +		;
> +			error("unify_proc__generate_initialise_clauses: " ++
> +				"type_to_ctor_and_args failed")
> +		),
> +		PredName = special_pred__special_pred_name(initialise,
> +				TypeCtor),
Fix the indentation here.

> +		hlds_module__module_info_name(ModuleInfo, ModuleName),
> +		TypeCtor = TypeSymName - _TypeArity,
> +		sym_name_get_module_name(TypeSymName, ModuleName,
> +			TypeModuleName),
> +		InitPred = qualified(TypeModuleName, PredName),
> +		PredId   = invalid_pred_id,
> +		ModeId   = invalid_proc_id,
> +		InitCall = call(PredId, ModeId, [X0], not_builtin, no,
> +				InitPred),
> +		InitGoal = InitCall - GoalInfo,
and here.

> +
> +		Any = any(shared),
> +		generate_unsafe_cast(X0, X, Any, Any, Context, CastGoal),
> +		Goal = conj([InitGoal, CastGoal]) - GoalInfo,
> +		unify_proc__quantify_clauses_body([X], Goal, Context, Clauses,
> +			!Info)
> +	;
> +		error("unify_proc__generate_initialise_clauses: " ++
> +			"trying to create initialisation proc for type " ++
>  			"that has no solver_type_details")
>  	).
>

That (along with the other bugfix) looks alright otherwise.  Can you
post the test cases for these changes before you commit.

Cheers,
Julien.

--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------