[m-rev.] For review: solver-types

[Zoltan Somogyi]

On 18-Aug-2004, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> +equiv_type__replace_in_type_defn(EqvMap, TypeCtor,
> +		solver_type(SolverTypeDetails0, MaybeUserEqComp),
> +		solver_type(SolverTypeDetails,  MaybeUserEqComp),
> +		ContainsCirc, !VarSet, !Info) :-
> +	RepresentationType0 =
> +		SolverTypeDetails0 ^ representation_type,
> +	equiv_type__replace_in_type_2(EqvMap, [TypeCtor], 
> +		RepresentationType0, RepresentationType,
> +		_, ContainsCirc, !VarSet, !Info),
> +	SolverTypeDetails =
> +		SolverTypeDetails0 ^ representation_type :=
> +			RepresentationType.

You didn't address my comment here; you should list all fields of
SolverTypeDetails0 here, instead of using field access notation.

> --- equiv_type_hlds.m	14 Jun 2004 04:16:02 -0000	1.6
> +++ equiv_type_hlds.m	17 Aug 2004 03:50:10 -0000
> @@ -129,11 +129,19 @@
>  			TVarSet0, TVarSet, EquivTypeInfo0, EquivTypeInfo),
>  		Body = eqv_type(Type)
>  	;
> -		Body0 = foreign_type(_, _),
> +		Body0 = foreign_type(_),
>  		EquivTypeInfo = EquivTypeInfo0,
>  		Body = Body0,
>  		TVarSet = TVarSet0
>  	;
> +		Body0 = solver_type(SolverTypeDetails0, UserEq),
> +		RepnType0 = SolverTypeDetails0 ^ representation_type,
> +		equiv_type__replace_in_type(EqvMap, RepnType0, RepnType, _,
> +			TVarSet0, TVarSet, EquivTypeInfo0, EquivTypeInfo),
> +		SolverTypeDetails =
> +			SolverTypeDetails0 ^ representation_type := RepnType,
> +		Body = solver_type(SolverTypeDetails, UserEq)
> +	;
>  		Body0 = abstract_type(_),
>  		EquivTypeInfo = EquivTypeInfo0,
>  		Body = Body0,

Same here.

>  maybe_make_shared_inst_list([_|_], [], _, _, _) :-
>  	error("maybe_make_shared_inst_list: length mismatch").
>  
> +
>  make_shared_inst_list([], ModuleInfo, [], ModuleInfo).
>  make_shared_inst_list([Inst0 | Insts0], ModuleInfo0,
>  		[Inst | Insts], ModuleInfo) :-
> @@ -1408,6 +1415,7 @@
>  		inst_merge_2(InstA, InstB, MaybeType, ModuleInfo1, Inst0,
>  			ModuleInfo2),
>  
> +

I systematically replace sequences of two or more blank lines with one blank
line in the files I touch to make limited height windows more effective.

> +	% A solver type t defined with
> +	%
> +	% :- solver type st
> +	% 	where representation is rt,		% type
> +	% 	      initialisation is ip,		% pred
> +	% 	      ground         is gi,		% inst
> +	% 	      any            is ai, ...		% inst
> +	%
> +	% causes the following to be introduced:
> +	%
> +	% :- impure func 'representation of st'(st)      = rt.
> +	% :-        mode 'representation of st'(in)      = out(gi) is det.
> +	% :-        mode 'representation of st'(in(any)) = out(ai) is det.

Are the circumstances in which having these two procedures be from the same
function is advantageous? Having them be from two different functions would,
I think, make HLDS dumps more easily readable, and would make the design
more symmetrical. If there are reasons for doing things the current way,
then document them.

> +	ToRepnSymName     = solver_to_repn_symname(TypeSymName, Arity),
> +	ToRepnArgTypes    = [type_only(SolverType), type_only(RepnType)],
> +	ToRepnTypeSigItem =
> +		pred_or_func(TVarSet, InstVarSet, ExistQTVars,
> +			function,
> +			ToRepnSymName,
> +			ToRepnArgTypes,
> +			no,	/* no `with_type` ... */
> +			no,	/* no `with_inst` ... */
> +			no,	/* no determinism */
> +			true,	/* no `where ...' */
> +			(impure), 
> +			constraints([], []) /* no type class constraints */
> +		),
> +	add_item_decl_pass_1(ToRepnTypeSigItem, Context,
> +		!Status, !Module, _, !IO),

You should add a sanity check on the third last argument, here and in the
later calls to add_item_decl_pass_1.

> +
> +	% Obtain the solver type conversion function sym_names from
> +	% the solver type sym_name.
> +	%
> +:- func solver_to_repn_symname(sym_name, arity) = sym_name.
> +
> +solver_to_repn_symname(unqualified(Name), Arity) =
> +	unqualified(
> +		"representation of " ++ Name ++ "/" ++ int_to_string(Arity)
> +	).
> +solver_to_repn_symname(qualified(ModuleNames, Name), Arity) =
> +	qualified(ModuleNames,
> +		"representation of " ++ Name ++ "/" ++ int_to_string(Arity)
> +	).

Eventually, you will need to add these patterns to both the C and Mercury
versions of the demanglers (util/mdemangle.c, profiler/demangle.m and
deep_profiler/read_profile.m), but for now it is sufficient to add a XXX
to both files.

> +:- func repn_to_any_solver_symname(sym_name, arity) = sym_name.
> +
> +repn_to_any_solver_symname(SymName, Arity) =
> +	repn_to_solver_symname("any", SymName, Arity).
> +
> +
> +:- func repn_to_ground_solver_symname(sym_name, arity) = sym_name.
> +
> +repn_to_ground_solver_symname(SymName, Arity) =
> +	repn_to_solver_symname("ground", SymName, Arity).
> +
> +
> +:- func repn_to_solver_symname(string, sym_name, arity) = sym_name.
> +
> +repn_to_solver_symname(AnyOrGround, unqualified(Name), Arity) =
> +	unqualified(
> +		string.format("representation to %s %s/%d",
> +			[s(AnyOrGround), s(Name), i(Arity)])
> +	).
> +repn_to_solver_symname(AnyOrGround, qualified(ModuleNames, Name), Arity) =
> +	qualified(ModuleNames,
> +		string.format("representation to %s %s/%d",
> +			[s(AnyOrGround), s(Name), i(Arity)])
> +	).

And likewise these patterns.

> @@ -2295,26 +2670,13 @@
>  	% default to having an is_solver_type field of `non_solver_type'.
>  	% If another declaration for the type has a `solver' annotation then
>  	% we must update the foreign_type body to reflect this.
> +	%
> +	% rafe: XXX think it should be an error for foreign types to
> +	% be solver types.
> +	%

Are you sure? In some cases, a pointer to a solver data structure may be
a more natural representation than an index into a solver table.

> @@ -3687,6 +4067,19 @@
>  					TVarSet, Type, TypeCtor, TypeBody,
>  					Context, Status0, !Module)
>  			;
> +				true
> +			)
> +		;
> +			SpecialPredId = initialise,
> +			(
> +				type_is_solver_type(!.Module, Type)
> +			->
> +				add_special_pred_for_real(SpecialPredId,
> +					TVarSet, Type, TypeCtor, TypeBody,
> +					Context, Status0, !Module)
> +			;
> +				% rafe: XXX Should this be an error?
> +				%
>  				true

An initialise predicate for a nonsolver type should of course be an error,
unless in your design solver types may be visible in other modules as
non-solver types.

> ===================================================================
> RCS file: /home/mercury1/repository/mercury/compiler/maybe_mlds_to_gcc.pp,v
> retrieving revision 1.8
> diff -u -r1.8 maybe_mlds_to_gcc.pp
> --- maybe_mlds_to_gcc.pp	14 Jun 2004 04:16:16 -0000	1.8
> +++ maybe_mlds_to_gcc.pp	14 Jul 2004 07:30:38 -0000
> @@ -58,6 +58,7 @@
>  
>  #else
>  
> +:- import_module hlds__passes_aux.
>  :- import_module parse_tree__prog_out.
>  :- import_module string.

This looks unnecessary.

> -			io__write_string(", ")
> +mercury_output_where_attributes(TVarSet,
> +		MaybeSolverTypeDetails, MaybeUserEqComp) -->
> +	(
> +		{ MaybeSolverTypeDetails = no },
> +		{ MaybeUserEqComp        = no }
> +	->
> +		[]
> +	;
> +		{ if
> +			MaybeUserEqComp = yes(unify_compare(MaybeUnifyPred0,
> +							    MaybeComparePred0))
> +		  then
> +			MaybeUnifyPred   = MaybeUnifyPred0,
> +			MaybeComparePred = MaybeComparePred0
> +		  else
> +			MaybeUnifyPred   = no,
> +			MaybeComparePred = no
> +		},

I don't like code that uses both -> and if. However, this if-then-else,
and other yes/no decisions, should be switches. I would also consider
using state variable notation instead of DCGs.

> --- modes.m	14 Jun 2004 04:16:23 -0000	1.279
> +++ modes.m	7 Jul 2004 06:48:46 -0000
> @@ -242,10 +242,10 @@
>  	mode_info::in, mode_info::out) is det.
>  
>  	% check that the final insts of the head vars of a lambda
> -	% goal matches their expected insts
> +	% goal matches their expected insts.
>  	%
>  :- pred modecheck_final_insts(list(prog_var)::in, list(inst)::in,
> -	mode_info::in, mode_info::out) is det.
> +	hlds_goal::in, hlds_goal::out, mode_info::in, mode_info::out) is det.

Since you are changing the signature of this predicate, you must update its
documentation to mention the new arguments.

> +:- pred prepend_initialisation_call(module_info::in,
> +		prog_var::in, (type)::in, (inst)::in,
> +		hlds_goal::in, hlds_goal::out) is det.
> +
> +prepend_initialisation_call(ModuleInfo, Var, VarType, InitialInst,
> +		Goal0, Goal) :-
> +	Goal0   = _GoalExpr0 - GoalInfo0,
> +	hlds_goal__goal_info_get_context(GoalInfo0, Context),
> +	construct_initialisation_call(ModuleInfo, Var, VarType, InitialInst,
> +		Context, no /* CallUnifyContext */, InitVarGoal),
> +	goal_to_conj_list(Goal0, ConjList0),
> +	conj_list_to_goal([InitVarGoal | ConjList0], GoalInfo0, Goal).

I think it would be simpler if instead of returning a modified goal,
you returned a list of goals, both here and its callers all the way to the code
that modechecks a call. This would remove the need to construct Goal here
with a mostly bogus goal_info, since most calls are part of conjunctions.

>  
>  % Modecheck a goal by abstractly interpreteting it, as explained

s/interpreteting/interpreting/

> +qualify_type_defn(solver_type(SolverTypeDetails0, MaybeUserEqComp),
> +		solver_type(SolverTypeDetails, MaybeUserEqComp),
> +		Info0, Info) -->
> +	{ RepnType0   = SolverTypeDetails0 ^ representation_type },
> +	{ GroundInst0 = SolverTypeDetails0 ^ ground_inst },
> +	{ AnyInst0    = SolverTypeDetails0 ^ any_inst },
> +	qualify_type(RepnType0, RepnType,     Info0, Info1),
> +	qualify_inst(GroundInst0, GroundInst, Info1, Info2),
> +	qualify_inst(AnyInst0, AnyInst,       Info2, Info ),
> +	{ SolverTypeDetails =
> +		(((SolverTypeDetails0
> +			^ representation_type := RepnType   )
> +			^ ground_inst         := GroundInst )
> +			^ any_inst            := AnyInst    ) }.

Again, you should list match SolverTypeDetails0 against a function symbol
instead of using field access notation, to guard against the future addition
of more fields.

>  		TypeDefn = abstract_type(IsSolverType)
>  	;
> +		TypeDefn = solver_type(_, _),
> +		% rafe: XXX we need to also export the details of the
> +		% forwarding type for the representation and the forwarding
> +		% pred for initialization.
> +		IsSolverType = solver_type
> +	;
>  		TypeDefn = eqv_type(_),
> +		% rafe: XXX what *should* IsSolverType be here?  We need
> +		% to know properly.
> +		IsSolverType = non_solver_type,
>  		% For the `.int2' files, we need the full definitions of
>  		% equivalence types. They are needed to ensure that
>  		% non-abstract equivalence types always get fully expanded

I guess you'll fix these XXXs soon, so they are ok for now.

>  	(
> -		TypeDefn0 = du_type(Constructors, IsSolverType,
> -			yes(_UnifyCompare)),
> -		TypeDefn  = du_type(Constructors, IsSolverType,
> -			yes(abstract_noncanonical_type))
> -	;
> -		TypeDefn0 = foreign_type(ForeignType, yes(_), Assertions),
> -		TypeDefn = foreign_type(ForeignType,
> -			yes(abstract_noncanonical_type), Assertions)
> +		TypeDefn0 = du_type(Constructors, yes(_UserEqComp)),
> +		TypeDefn  = du_type(Constructors, yes(
> +				abstract_noncanonical_type(non_solver_type)))
> +	;
> +		TypeDefn0 = foreign_type(ForeignType, yes(_UserEqComp),
> +				Assertions),
> +		TypeDefn  = foreign_type(ForeignType,
> +				yes(abstract_noncanonical_type(
> +					non_solver_type)),
> +				Assertions)

I prefer to have only a single extra indent when continuing lines, and this
is the perfect example why.

> +	get_condition(B, Body, Condition),
>  	get_is_solver_type(Attributes0, IsSolverType, Attributes),
> -	process_du_type(ModuleName, H, Body, IsSolverType, EqCompare, R0),
> -	check_no_attributes(R0, Attributes, R).
> +	(
> +		IsSolverType = solver_type,
> +		Result = error("a solver type cannot have data constructors",
> +				H)
> +	;
> +		IsSolverType = non_solver_type,
> +		du_type_rhs_ctors_and_where_terms(Body, CtorsTerm,
> +			MaybeWhereTerm),
> +		CtorsResult = convert_constructors(ModuleName, CtorsTerm),
> +		(
> +			CtorsResult = error(String, Term),
> +			Result      = error(String, Term)
> +		;
> +			CtorsResult = ok(Ctors),
> +			WhereResult = parse_type_decl_where_term(
> +					non_solver_type, ModuleName,
> +					MaybeWhereTerm),
> +			(
> +				WhereResult = error(String, Term),
> +				Result      = error(String, Term)
> +			;
> +				WhereResult = ok(_NoSolverTypeDetails,
> +						 MaybeUserEqComp),

That underscore in _NoSolverTypeDetails means you don't detect e.g.
"where representation" clauses on non-solver types; please fix that
oversight, or document why it isn't an oversight.

> +:- func parse_type_decl_where_term(is_solver_type, module_name, maybe(term)) =
> +		maybe2(maybe(solver_type_details), maybe(unify_compare)).

That looks like one too many maybes to me. Why do you need the outer maybe2?
If there is a good reason for it then document it, otherwise return just
a pair of maybes.

> +parse_where_is(Name, Parser, Term) = Result :-
> +	(
> +		Term = term__functor(term__atom("is"), [LHS, RHS], _Context1)
>  	->
> -		Body = Body1,
>  		(
> -			EqCompTerm = term__functor(
> +			LHS = term__functor(term__atom(Name), [], _Context2)
> +		->
> +			Result0 = Parser(RHS),
> +			(
> +				Result0 = ok(X),
> +				Result  = ok(yes(X))

Can you find a better variable name than X?

> +	(
> +		Term = term__functor(
>  				term__atom("type_is_abstract_noncanonical"),
> -				[], _Context2)
> +				[],
> +				_Context)
> +	->

Improve indentation.

> +parse_where_initialisation_is(ModuleName, Term) = Result :-
> +	Result0 = parse_where_is("initialisation",
> +			parse_where_pred_is(ModuleName), Term),
> +	(
> +		Result0 = ok(no)
> +	->
> +		Result  = parse_where_is("initialization",
> +				parse_where_pred_is(ModuleName), Term)
> +	;
> +		Result  = Result0
> +	).
> +
> +
> +:- func parse_where_pred_is(module_name, term) = maybe1(sym_name).
> +
> +parse_where_pred_is(ModuleName, Term) = Result :-
> +	parse_implicitly_qualified_symbol_name(ModuleName, Term, Result).
> +
> +
> +:- func parse_where_inst_is(module_name, term) = maybe1(inst).
> +
> +parse_where_inst_is(_ModuleName, Term) =
> +	( if
> +		prog_io_util__convert_inst(no_allow_constrained_inst_var,
> +			Term, Inst),
> +		not inst_util__inst_contains_unconstrained_var(Inst)
> +	  then ok(Inst)
> +	  else error("expected a ground, unconstrained inst", Term)
> +	).

Again, mixing -> and if.

As I told you earlier, this diff updates a fundamentally misdesigned parser.

> +solver_inst_cast_sym_name(TypeSymName, TypeArity) =
> +	unqualified_sym_name_with_prefix_suffix("inst cast ", TypeSymName,
> +		"/" ++ int_to_string(TypeArity)).
> +
> +
> +:- func solver_inst_sym_name(sym_name, arity) = sym_name.
> +
> +solver_inst_sym_name(TypeSymName, TypeArity) =
> +	unqualified_sym_name_with_prefix_suffix("", TypeSymName,
> +		"/" ++ int_to_string(TypeArity) ++ " inst").

What are these for?

> -	(
> -		convert_constructors(ModuleName, Body, Constrs)
> -	->
> -		% check that all type variables in the body
> -		% are either explicitly existentially quantified
> -		% or occur in the head.
> -		(
> -			list__member(Ctor, Constrs),
> -			Ctor = ctor(ExistQVars, _Constraints, _CtorName,
> -					CtorArgs),
> -			assoc_list__values(CtorArgs, CtorArgTypes),
> -			term__contains_var_list(CtorArgTypes, Var),
> -			\+ list__member(Var, ExistQVars),
> -			\+ term__contains_var_list(Args, Var)
> -		->
> -			Result = error(
> -			"free type parameter in RHS of type definition",
> -					Body)

It would be a lot easier to check this part of the diff if you used diff's -b
option.

> +convert_constructor_arg_list( ModuleName, [Term | Terms]) = Result :-

Why the space before ModuleName?

> -special_pred_name(unify, _TypeCtor) = "__Unify__".
> -special_pred_name(index, _TypeCtor) = "__Index__".
> -special_pred_name(compare, _TypeCtor) = "__Compare__".
> +special_pred_name(unify,      SymName - Arity) =
> +	string__format("__Unify__%s/%d",
> +		[s(sym_name_to_string(SymName)), i(Arity)]).
> +special_pred_name(index,      SymName - Arity) =
> +	string__format("__Index__%s/%d",
> +		[s(sym_name_to_string(SymName)), i(Arity)]).
> +special_pred_name(compare,    SymName - Arity) =
> +	string__format("__Compare__%s/%d",
> +		[s(sym_name_to_string(SymName)), i(Arity)]).
> +special_pred_name(initialise, SymName - Arity) =
> +	string__format("__Initialise__%s/%d",
> +		[s(sym_name_to_string(SymName)), i(Arity)]).

This change requires immediate updates to name_mangle.m (whose handling
of these names is now redundant) and to all three demanglers.

>  special_pred_is_generated_lazily(ModuleInfo, TypeCtor, Body, Status) :-
> +	% rafe: XXX Is there a cleaner way of doing this?  I don't
> +	% want special preds for solver types to be generated lazily
> +	% because I have to insert calls to their initialisation preds
> +	% during mode analysis and I therefore require the appropriate
> +	% names to appear in the symbol table.
> +	%

The answer to your quesion is "no", so delete that part of the comment
(or turn it into an enhancement request), but leave the rest.

> +		% rafe: XXX I think the [yes] here is correct.
> +		%
> +special_pred_id_to_termination(initialise, HeadVars, ArgSize, Termination) :-
> +	term_util__make_bool_list(HeadVars, [yes], OutList),
> +	ArgSize = finite(0, OutList),
> +	Termination = cannot_loop.

If the initialization predicate is user supplied, then whether it can loop
depends on the user supplied predicate. It looks like the code for unify and
compare is also wrong; it is wrong because it predates user-defined unify
and compare predicates. For now, leave a XXX.

> +				% We treat solver_types as being
> +				% equivalent to their representation
> +				% types for RTTI purposes.
> +				%
> +				% rafe: XXX Won't this cause trouble
> +				% with construct etc?

No more problems than are caused by construct on abstract types in general.

> +	% Obtain the type definition and type definition body respectively,
> +	% if known, for the principal type constructor of the given type.
> +	%
> +	% Fail if the given type is a type variable.
> +:- pred type_util__type_to_type_defn(module_info::in, (type)::in,
> +		hlds_type_defn::out) is semidet.
> +
> +:- pred type_util__type_to_type_defn_body(module_info::in, (type)::in,
> +		hlds_type_body::out) is semidet.
> +
>  	% Succeed iff there was either a `where equality is <predname>' or a
>  	% `where comparison is <predname>' declaration for the principal type
>  	% constructor of the specified type, and return the ids of the declared
> @@ -83,12 +93,23 @@
>  :- pred type_body_has_user_defined_equality_pred(module_info::in,
>  	hlds_type_body::in, unify_compare::out) is semidet.
>  
> -	% Succeed if the inst `any' can be considered `bound' for this type.
> +	% Succeed iff the principal type constructor for the given type
> +	% is a solver type.
> +	%
> +	% If the type is a type variable and thus has no principal type
> +	% constructor, fail.
> +:- pred type_util__type_is_solver_type(module_info::in, (type)::in) is semidet.
> +
> +:- pred type_util__type_has_solver_type_details(module_info::in, (type)::in,
> +		solver_type_details::out) is semidet.
> +
> +:- pred type_util__type_body_has_solver_type_details(module_info::in,
> +		hlds_type_body::in, solver_type_details::out) is semidet.
> +
>  :- pred type_util__is_solver_type(module_info::in, (type)::in) is semidet.

All these new predicates in type_util, except the one working on a
hlds_type_body, beg the question of what they should do if the type
supplied is a type variable, and *has* no principal type constructor.

I think you should leave it to the caller to extra the principal type
constructor with type_to_ctor_and_args, and redefine these predicates
to work on the type constructor.

In fact, the same should be done to a bunch of old predicates in this module
too, but that can wait.

You can commit after addressing these points, and testing the changes I asked
you to make to name manglers/demanglers for unify/compare predicate names.

Zoltan.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------