[m-rev.] first step towards functional dependencies (1/3)

[Julien Fischer]

On Wed, 23 Mar 2005, Mark Brown wrote:

> Estimated hours taken: 240
> Branches: main
>
> Remove the assumption made by polymorphism.m that all type variables
> appearing in class constraints also appear in the type being constrained.
> This is a first step towards adding functional dependencies, since in the
> presence of functional dependencies (or "improvement" in general) this
> assumption no longer holds.
>
> The assumption made by polymorphism manifests itself in the fact that
> constraints on atomic goals are reconstructed by unifying the types of
> formal parameters with the types of actual arguments, and then applying
> the resulting substitution to the constraints.  Any type variables in
> constraints that don't appear in the formal parameters will therefore
> remain unbound.
>
> This change overcomes the assumption by building up a map from constraint
> identifiers to constraints during typechecking, and then looking up this
> map in order to reconstruct the constraint during the polymorphism
> transformation.
>
> To support this, the type 'class_constraint' has been removed and replaced
> by two distinct types, 'prog_constraint' and 'hlds_constraint'.  The former
> is part of the parse tree and holds the same information as the old
> class_constraint.  The latter is part of the HLDS, and is used during
> typechecking; in addition to the information in prog_constraints, it also
> stores a set of identifiers that represent where the constraint came from.
> These identifiers are used as the keys in the aforementioned map.
>
> At this stage the constraint identifiers are only used by typechecking to
> build the constraint map.  Other passes use either prog_constraints or
> hlds_constraints with an empty set of identifiers.
>
> compiler/hlds_data.m:
> 	Define the constraint_id type, which is used to uniquely identify
> 	class constraints.  A better scheme than this one has been suggested,
> 	but that will be left to a later change.  An XXX comment to that
> 	effect has been added.
>
> 	Define the hlds_constraint type, which is like prog_constraint but
> 	it also includes a set of constraint_ids.  Define a set of predicates
> 	to initialise and manipulate these.
>
> 	Define the constraint_map type here.  Move the definition of
> 	constraint_proof_map to here, where it more sensibly belongs.
>
> 	Update the comments in hlds_instance_defn slightly, with information
> 	that I found I needed to know when making this change.
>
> compiler/hlds_pred.m:
> 	Add a field to the pred_info to store the constraint_map.
>
> 	Move the definition of constraint_proof_map from here.
>
> compiler/hlds_out.m:
> 	Print out a representation of the constraint map if it isn't empty.
>
> compiler/type_util.m:
> 	Change the predicates that used to operate on class_constraints so
> 	that they now operate on hlds_constraints.  The old versions of these
> 	predicates have now moved to prog_util.
>
As we discussed in person, prog_type woud probably be the natural module
to put this in - that should be part of separate change though.

> 	Add some utility predicates to manipulate constraint_maps.
>
> 	Add a predicate to apply a variable renaming to constraint_proof_maps.
>
> compiler/prog_data.m:
> 	Rename class_constraint(s) to prog_constraint(s).
>
> compiler/prog_util.m:
> 	Provide a set of predicates for manipulating prog_constraints.
>
> compiler/typecheck.m:
> 	Ensure that goal_paths are filled in before the first iteration
> 	of typechecking.
>
> 	Pass the hlds_goal_info down through typecheck_goal_2 so that the
> 	goal_path can be retrieved when needed to assign identifiers to
> 	constraints.  Thread the goal_path through to wherever it is needed.
>
> 	Store hlds_constraints in the args_type_assign rather than
> 	prog_constraints, so that the required information is available
> 	when creating the new set of type_assigns.  Do likewise for the
> 	cons_type_info type.  Don't pass the module_info through
> 	make_pred_cons_info*, since it isn't used.  Do pass the goal_path,
> 	though, so that constraints in cons_type_infos can be given the
> 	correct identifier.
>
> 	Add a constraint_map field to the typecheck_info, initialised to empty.
>
> 	When retrieving the final information from a typecheck_info, return
> 	the resulting constraint_map, after applying any type bindings.
> 	Ensure that any constraints that may not have been entered into the
> 	constraint_map are put there now.  Call the new predicate in type_util
> 	to rename the constraint_proof_map, rather than doing it longhand
> 	here.
>
> 	Make the following changes to context reduction:
>
> 		- Thread the constraint_map through, so that it can be updated
> 		as constraints are eliminated.
>
> 		- Instead of simply calling sort_and_remove_dups on the
> 		set of constraints remaining after one iteration, merge the
> 		constraints in such a way that the complete set of
> 		constraint_ids is retained.
>
> 		- Disregard the constraint_ids when deleting newly introduced
> 		constraints that are equivalent to constraints that have
> 		already been seen.
>
> 		- Simplify the code of find_matching_instance_rule_2 by
> 		moving the deterministic code out of the condition of the
> 		if-then-else.
>
> 	Move find_first_map into the library.
>
> compiler/polymorphism.m:
> 	Ensure that the goal_path is set when constructing lambda goals.
>
> 	In process_call, look up the constraints in the constraint_map
> 	using the goal_path as part of the key, rather than calculating
> 	the constraints by applying the ParentToActual type substitution.
> 	Rearrange this code so that it is divided into easier to understand
> 	blocks.
>
> 	Add a field to the poly_info to store the constraint_map, and
> 	initialise it from the pred_info.
>
> compiler/goal_path.m:
> 	Fill slots in lambda_goals, since constraints inside these will
> 	otherwise not be identified properly.  The goal_paths inside here
> 	do not entirely make sense, since there is no goal_path_step for
> 	the lambda_goal itself.  However, there is enough information
> 	retained to distinguish these goal_paths from any other possible
> 	goal_path, which is all that we require to identify constraints.
>
> 	Add a warning not to fill in the goal slots between the typechecking
> 	and polymorphism passes, since doing so could potentially render the
> 	constraint_maps incorrect.
>
> compiler/make_hlds.m:
> 	Initialise the constraint_map to empty in pred_infos.
>
> 	Move the code for updating the superclass_table into a separate
> 	predicate.  Initially this change was made because, in an earlier
> 	version of the change, the superclass_table had some extra
> 	information that needed to be filled in.  That part of the change
> 	is not needed in this diff, but the new predicate simplifies the
> 	code a bit so I've left it there.
>
> compiler/check_typeclass.m:
> 	Convert the prog_constraints into hlds_constraints before passing
> 	them to typecheck.reduce_context_by_rule_application.  They are
> 	assigned no identifiers, since these constraints are not required
> 	to be put into the constraint map.
>
> 	Change the name of the function get_constraint_id to
> 	get_constraint_class_id, since it would now be ambiguous otherwise.
>
> compiler/cse_detection.m:
> 	Import parse_tree__prog_util, since that is where renamings of
> 	prog_constraints are now defined.
>
> compiler/higher_order.m:
> 	Initialise pred_infos here with an empty constraint_map.
>
> compiler/post_typecheck.m:
> 	When binding type vars to void, apply the void substitution to the
> 	constraint_map.
>
> compiler/table_gen.m:
> 	Pass the constraint_map when creating a new pred_info.
>
> compiler/unused_args.m:
> 	Create the pred_info with an empty constraint_map.  The constraint_map
> 	won't be used by this stage anyway.
>
> compiler/*.m:
> 	Update to use the new type names.  Also update to use the existing
> 	type synonyms typeclass_info_varmap and constraint_proof_map.
>
> 	Change names of predicates and functions to use prog_constraint
> 	instead of class_constraint, where applicable.
>
> library/list.m:
> 	Add find_first_map from typecheck.  Also add find_first_map{2,3},
> 	since at one stage during development I needed find_first_map3, and,
> 	although it's not used in the current diff, there is little point
> 	removing it now.
>

> @@ -843,14 +845,66 @@
>  					% proc_ids of all the methods
>  		instance_tvarset	:: tvarset,
>  					% VarNames
> -		instance_proofs		:: map(class_constraint,
> -						constraint_proof)
> +		instance_proofs		:: constraint_proof_map
...

> +:- type constraint_type
> +	--->	existential
> +	;	universal.
> +
> +	% THe identifier of a constraint is stored along with the constraint.
s/THe/The

> +	% Each value of this type may have more than one identifier because
> +	% if two constraints in a context are equivalent then we merge them
> +	% together in order to not have to prove the same constraint twice.
> +	%
> +:- type hlds_constraint
> +	--->	constraint(
> +			list(constraint_id),
> +			class_name,
> +			list(type)
> +		).
> +
> +:- type hlds_constraints
> +	--->	constraints(
> +			list(hlds_constraint),	% Universal constraints.
> +			list(hlds_constraint)	% Existential constraints.
> +		).
> +
Is it worth giving field names to these things?

> +	% During type checking we fill in a constraint_map which gives
> +	% the constraint that corresponds to each identifier.  This is used
> +	% by the polymorphism translation to retrieve details of constraints.
> +	%
> +:- type constraint_map == map(constraint_id, prog_constraint).
> +
>  	% `Proof' of why a constraint is redundant
>  :- type constraint_proof
>  			% Apply the instance decl with the given number.
> @@ -871,9 +925,135 @@
>
>  			% The constraint is redundant because of the
>  			% following class's superclass declaration
> -	;	superclass(class_constraint).
> +	;	superclass(prog_constraint).
> +
> +:- type constraint_proof_map == map(prog_constraint, constraint_proof).
> +
> +:- pred init_hlds_constraint_list(list(prog_constraint)::in,
> +	list(hlds_constraint)::out) is det.
> +
> +:- pred make_hlds_constraints(prog_constraints::in, goal_path::in,
> +	hlds_constraints::out) is det.
> +
> +:- pred make_hlds_constraint_list(list(prog_constraint)::in,
> +	constraint_type::in, goal_path::in, list(hlds_constraint)::out) is det.
> +
> +:- pred retrieve_prog_constraints(hlds_constraints::in, prog_constraints::out)
> +	is det.
> +
> +:- pred retrieve_prog_constraint_list(list(hlds_constraint)::in,
> +	list(prog_constraint)::out) is det.
> +
> +:- pred retrieve_prog_constraint(hlds_constraint::in, prog_constraint::out)
> +	is det.
> +
> +:- pred matching_constraints(hlds_constraint::in, hlds_constraint::in)
> +	is semidet.
> +
> +:- pred compare_hlds_constraints(hlds_constraint::in, hlds_constraint::in,
> +	comparison_result::out) is det.
> +
> +:- pred update_constraint_map(hlds_constraint::in, constraint_map::in,
> +	constraint_map::out) is det.
> +
> +:- pred lookup_hlds_constraint_list(constraint_map::in, constraint_type::in,
> +	goal_path::in, int::in, list(prog_constraint)::out) is det.
> +
> +:- implementation.
> +
It would be worth adding a dashed line there just to make the separation
from interface to implementation more obvious.

> Index: compiler/hlds_pred.m
> ===================================================================
> RCS file: /home/mercury1/repository/mercury/compiler/hlds_pred.m,v
> retrieving revision 1.159
> diff -u -r1.159 hlds_pred.m
> --- compiler/hlds_pred.m	22 Mar 2005 06:40:00 -0000	1.159
> +++ compiler/hlds_pred.m	22 Mar 2005 12:23:48 -0000
> @@ -575,12 +575,6 @@
>  	% module, name and arity.
>  :- type aditi_owner == string.
>
> -	% The constraint_proof_map is a map which for each type class
> -	% constraint records how/why that constraint was satisfied.
> -	% This information is used to determine how to construct the
> -	% typeclass_info for that constraint.
> -:- type constraint_proof_map == map(class_constraint, constraint_proof).
> -
>  	% Describes the class constraints on an instance method implementation.
>  	% This information is used by polymorphism.m to ensure that the
>  	% type_info and typeclass_info arguments are added in the order in
> @@ -590,9 +584,9 @@
>  		class_id,
>  		list(type),		% The types in the head of the
>  					% instance declaration.
> -		list(class_constraint),	% The universal constraints
> +		list(prog_constraint),	% The universal constraints
>  					% on the instance declaration.
> -		class_constraints	% The contraints on the method's
> +		prog_constraints	% The contraints on the method's
>  					% type declaration in the
>  					% `:- typeclass' declaration.
>  	).
...

> Index: compiler/lambda.m
> ===================================================================
> RCS file: /home/mercury1/repository/mercury/compiler/lambda.m,v
> retrieving revision 1.96
> diff -u -r1.96 lambda.m
> --- compiler/lambda.m	22 Mar 2005 06:40:02 -0000	1.96
> +++ compiler/lambda.m	22 Mar 2005 12:23:48 -0000
> @@ -118,14 +118,13 @@
>  	lambda_info(
>  		prog_varset,		% from the proc_info
>  		map(prog_var, type),	% from the proc_info
> -		class_constraints,	% from the pred_info
> +		prog_constraints,	% from the pred_info
>  		tvarset,		% from the proc_info
>  		inst_varset,		% from the proc_info
>  		map(tvar, type_info_locn),
>  					% from the proc_info
>  					% (typeinfos)
> -		map(class_constraint, prog_var),
> -					% from the proc_info
> +		typeclass_info_varmap,	% from the proc_info
>  					% (typeclass_infos)
>  		pred_markers,		% from the pred_info
>  		pred_or_func,
> @@ -597,7 +596,7 @@
>  		InstVarSet, TVarMap, TCVarMap, Markers, POF, OrigPredName,
>  		Owner, ModuleInfo, MustRecomputeNonLocals).
>
> -:- pred lambda__constraint_contains_vars(list(tvar)::in, class_constraint::in)
> +:- pred lambda__constraint_contains_vars(list(tvar)::in, prog_constraint::in)
>  	is semidet.
>
>  lambda__constraint_contains_vars(LambdaVars, ClassConstraint) :-

...

>      OldConstraints = Constraints.
>
> @@ -3524,6 +3517,26 @@
>          )
>      ).
>
> +    % insert an entry into the super class table
> +    % for each super class of this class
Make that into a proper sentence.

> +:- pred update_superclass_table(class_id::in, list(tvar)::in, tvarset::in,
> +    list(prog_constraint)::in, superclass_table::in, superclass_table::out)
> +    is det.
> +
> +update_superclass_table(ClassId, Vars, VarSet, Constraints, !Supers) :-
> +    list.foldl(update_superclass_table_2(ClassId, Vars, VarSet), Constraints,
> +        !Supers).
> +
> +:- pred update_superclass_table_2(class_id::in, list(tvar)::in, tvarset::in,
> +    prog_constraint::in, superclass_table::in, superclass_table::out) is det.
> +
> +update_superclass_table_2(ClassId, Vars, VarSet, Constraint, !Supers) :-
> +    Constraint = constraint(SuperName, SuperTypes),
> +    list__length(SuperTypes, SuperClassArity),
> +    SuperClassId = class_id(SuperName, SuperClassArity),
> +    SubClassDetails = subclass_details(SuperTypes, ClassId, Vars, VarSet),
> +    multi_map__set(!.Supers, SuperClassId, SubClassDetails, !:Supers).
You may want to use the svmulti_map version of set there.


To be continued ...

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