[m-rev.] diff: bugfix for existential types
Mark Brown
mark at cs.mu.OZ.AU
Tue Oct 25 23:06:56 AEST 2005
Hi,
I'm going to commit this one right away, since this bug is currently holding
up my work on the propagation engine. Post-commit reviews are welcome.
Cheers,
Mark.
Estimated hours taken: 15
Branches: main
Fix a bug with functional dependencies and existentially typed data. Fix
another bug, exposed by the first fix, with field access expressions and
existentially typed data.
compiler/polymorphism.m:
Use the constraint map to determine the constraints on an
existentially typed constructions and deconstructions, rather than
trying to unify the argument types. The latter will not be able
to bind any type variables that appear in constraints but not in
the argument types.
compiler/post_typecheck.m:
When expanding field access expressions, bind newly created type
variables to the corresponding type variables created during type
checking, if such exist. This ensures that the varmaps and
constraint maps remain meaningful.
Ensure that the newly created unifications contain the goal path of
the original field access expression, since these are used as keys
into the constraint map.
compiler/typecheck.m:
When processing field access expressions, don't just add the
constraints that are required by the expression as a whole. Add
all the constraints (existential and universal) that are required by
the unifications that the field access expressions will be expanded
into. The new universal constraints don't perform any role in type
checking, since they will be eliminated immediately by context
reduction via the corresponding existential constraints, however
their presence ensures that all tables will be updated as required
by later stages.
tests/hard_coded/typeclasses/Mmakefile:
tests/hard_coded/typeclasses/fundeps_4.exp:
tests/hard_coded/typeclasses/fundeps_4.m:
A test case for the first bug. Numerous existing tests suffice for
testing the second bug.
Index: compiler/polymorphism.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/polymorphism.m,v
retrieving revision 1.281
diff -u -r1.281 polymorphism.m
--- compiler/polymorphism.m 24 Oct 2005 04:14:21 -0000 1.281
+++ compiler/polymorphism.m 24 Oct 2005 07:01:16 -0000
@@ -1273,9 +1273,8 @@
% type_info and/or type_class_info variables.
map__apply_to_list(ArgVars0, VarTypes0, ActualArgTypes),
- goal_info_get_context(GoalInfo0, Context),
process_existq_unify_functor(ConsDefn,
- IsConstruction, ActualArgTypes, TypeOfX, Context,
+ IsConstruction, ActualArgTypes, TypeOfX, GoalInfo0,
ExtraVars, ExtraGoals, !Info),
list__append(ExtraVars, ArgVars0, ArgVars),
goal_info_get_nonlocals(GoalInfo0, NonLocals0),
@@ -1382,11 +1381,11 @@
% an existentially quantified data constructor.
%
:- pred process_existq_unify_functor(ctor_defn::in, bool::in,
- list(mer_type)::in, mer_type::in, prog_context::in, list(prog_var)::out,
+ list(mer_type)::in, mer_type::in, hlds_goal_info::in, list(prog_var)::out,
list(hlds_goal)::out, poly_info::in, poly_info::out) is det.
process_existq_unify_functor(CtorDefn, IsConstruction,
- ActualArgTypes, ActualRetType, Context,
+ ActualArgTypes, ActualRetType, GoalInfo,
ExtraVars, ExtraGoals, !Info) :-
CtorDefn = ctor_defn(CtorTypeVarSet, CtorExistQVars, CtorKindMap,
CtorExistentialConstraints, CtorArgTypes, CtorRetType),
@@ -1412,20 +1411,23 @@
type_list_subsumes_det([ParentRetType | ParentArgTypes],
[ActualRetType | ActualArgTypes], ParentToActualTypeSubst),
- % Apply those type bindings to the existential type class constraints.
- apply_rec_subst_to_prog_constraint_list(ParentToActualTypeSubst,
- ParentExistentialConstraints,
- ActualExistentialConstraints),
-
% Create type_class_info variables for the type class constraints.
+ poly_info_get_constraint_map(!.Info, ConstraintMap),
+ goal_info_get_goal_path(GoalInfo, GoalPath),
+ list__length(ParentExistentialConstraints, NumExistentialConstraints),
+ goal_info_get_context(GoalInfo, Context),
(
IsConstruction = yes,
% Assume it's a construction.
+ lookup_hlds_constraint_list(ConstraintMap, unproven, GoalPath,
+ NumExistentialConstraints, ActualExistentialConstraints),
make_typeclass_info_vars(ActualExistentialConstraints, [], Context,
ExtraTypeClassVars, ExtraTypeClassGoals, !Info)
;
IsConstruction = no,
% Assume it's a deconstruction.
+ lookup_hlds_constraint_list(ConstraintMap, assumed, GoalPath,
+ NumExistentialConstraints, ActualExistentialConstraints),
make_existq_typeclass_info_vars(ActualExistentialConstraints,
ExtraTypeClassVars, ExtraTypeClassGoals, !Info)
),
@@ -1770,8 +1772,8 @@
% Make variables to hold any existentially quantified typeclass_infos
% in the call, insert them into the typeclass_info map.
list__length(ParentExistConstraints, NumExistConstraints),
- lookup_hlds_constraint_list(ConstraintMap, assumed,
- GoalPath, NumExistConstraints, ActualExistConstraints),
+ lookup_hlds_constraint_list(ConstraintMap, assumed, GoalPath,
+ NumExistConstraints, ActualExistConstraints),
make_existq_typeclass_info_vars(
ActualExistConstraints, ExtraExistClassVars,
ExtraExistClassGoals, !Info),
Index: compiler/post_typecheck.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/post_typecheck.m,v
retrieving revision 1.85
diff -u -r1.85 post_typecheck.m
--- compiler/post_typecheck.m 24 Oct 2005 04:14:21 -0000 1.85
+++ compiler/post_typecheck.m 25 Oct 2005 10:53:02 -0000
@@ -1282,7 +1282,8 @@
get_constructor_containing_field(ModuleInfo, TermType, FieldName,
ConsId, FieldNumber),
- get_cons_id_arg_types_adding_existq_tvars(ModuleInfo, ConsId,
+ goal_info_get_goal_path(OldGoalInfo, GoalPath),
+ get_cons_id_arg_types_adding_existq_tvars(ModuleInfo, GoalPath, ConsId,
TermType, ArgTypes0, ExistQVars, !PredInfo),
% If the type of the field we are extracting contains existentially
@@ -1337,7 +1338,8 @@
get_constructor_containing_field(ModuleInfo, TermType, FieldName,
ConsId0, FieldNumber),
- get_cons_id_arg_types_adding_existq_tvars(ModuleInfo, ConsId0,
+ goal_info_get_goal_path(OldGoalInfo, GoalPath),
+ get_cons_id_arg_types_adding_existq_tvars(ModuleInfo, GoalPath, ConsId0,
TermType, ArgTypes, ExistQVars, !PredInfo),
split_list_at_index(FieldNumber, ArgTypes,
@@ -1393,41 +1395,97 @@
% as an atomic goal.
Goal = scope(barrier(removable), Conj).
-:- pred get_cons_id_arg_types_adding_existq_tvars(module_info::in, cons_id::in,
- mer_type::in, list(mer_type)::out, list(tvar)::out,
- pred_info::in, pred_info::out) is det.
+:- pred get_cons_id_arg_types_adding_existq_tvars(module_info::in,
+ goal_path::in, cons_id::in, mer_type::in, list(mer_type)::out,
+ list(tvar)::out, pred_info::in, pred_info::out) is det.
-get_cons_id_arg_types_adding_existq_tvars(ModuleInfo, ConsId, TermType,
- ArgTypes, NewExistQVars, !PredInfo) :-
+get_cons_id_arg_types_adding_existq_tvars(ModuleInfo, GoalPath, ConsId,
+ TermType, ActualArgTypes, ActualExistQVars, !PredInfo) :-
% Split the list of argument types at the named field.
type_util__get_type_and_cons_defn(ModuleInfo, TermType, ConsId,
TypeDefn, ConsDefn),
- ConsDefn = hlds_cons_defn(ExistQVars, _, Args, _, _),
- assoc_list__values(Args, ArgTypes0),
+ ConsDefn = hlds_cons_defn(ConsExistQVars, ConsConstraints, ConsArgs, _, _),
+ assoc_list__values(ConsArgs, ConsArgTypes),
+
(
- ExistQVars = [],
- ArgTypes1 = ArgTypes0,
- NewExistQVars = []
+ ConsExistQVars = [],
+ ActualArgTypes0 = ConsArgTypes,
+ ActualExistQVars = []
;
- ExistQVars = [_ | _],
+ ConsExistQVars = [_ | _],
% Rename apart the existentially quantified type variables.
- list__length(ExistQVars, NumExistQVars),
+ list__length(ConsExistQVars, NumExistQVars),
pred_info_typevarset(!.PredInfo, TVarSet0),
- varset__new_vars(TVarSet0, NumExistQVars, NewExistQVars, TVarSet),
+ varset__new_vars(TVarSet0, NumExistQVars, ParentExistQVars, TVarSet),
pred_info_set_typevarset(TVarSet, !PredInfo),
- map__from_corresponding_lists(ExistQVars, NewExistQVars, TVarSubst),
- apply_variable_renaming_to_type_list(TVarSubst, ArgTypes0, ArgTypes1)
+ map__from_corresponding_lists(ConsExistQVars, ParentExistQVars,
+ ConsToParentRenaming),
+ apply_variable_renaming_to_type_list(ConsToParentRenaming,
+ ConsArgTypes, ParentArgTypes),
+ apply_variable_renaming_to_prog_constraint_list(ConsToParentRenaming,
+ ConsConstraints, ParentConstraints),
+
+ % Constrained existentially quantified tvars will have already
+ % been created during typechecking, so we need to ensure that the
+ % new ones we allocate here are bound to those created earlier,
+ % so that the varmaps remain meaningful.
+ %
+ pred_info_get_constraint_map(!.PredInfo, ConstraintMap),
+ list__length(ConsConstraints, NumConstraints),
+ lookup_hlds_constraint_list(ConstraintMap, assumed, GoalPath,
+ NumConstraints, ActualConstraints),
+ constraint_list_subsumes_det(ParentConstraints, ActualConstraints,
+ ExistTSubst),
+ apply_rec_subst_to_type_list(ExistTSubst, ParentArgTypes,
+ ActualArgTypes0),
+
+ % The kinds will be ignored when the types are converted back
+ % to tvars.
+ map__init(KindMap),
+ apply_rec_subst_to_tvar_list(KindMap, ExistTSubst, ParentExistQVars,
+ ActualExistQVarTypes),
+ ( type_list_to_var_list(ActualExistQVarTypes, ActualExistQVars0) ->
+ ActualExistQVars = ActualExistQVars0
+ ;
+ unexpected(this_file, "existq_tvar bound to non-var")
+ )
),
hlds_data__get_type_defn_tparams(TypeDefn, TypeParams),
( type_to_ctor_and_args(TermType, _, TypeArgs) ->
- map__from_corresponding_lists(TypeParams, TypeArgs, TSubst)
+ map__from_corresponding_lists(TypeParams, TypeArgs, UnivTSubst)
;
unexpected(this_file,
"get_cons_id_arg_types_adding_existq_tvars: " ++
"type_to_ctor_and_args failed")
),
- apply_subst_to_type_list(TSubst, ArgTypes1, ArgTypes).
+ apply_subst_to_type_list(UnivTSubst, ActualArgTypes0, ActualArgTypes).
+
+:- pred constraint_list_subsumes_det(list(prog_constraint)::in,
+ list(prog_constraint)::in, tsubst::out) is det.
+
+constraint_list_subsumes_det(ConstraintsA, ConstraintsB, Subst) :-
+ constraint_list_get_tvars(ConstraintsB, TVarsB),
+ map__init(Subst0),
+ (
+ unify_constraint_list(ConstraintsA, ConstraintsB, TVarsB,
+ Subst0, Subst1)
+ ->
+ Subst = Subst1
+ ;
+ unexpected(this_file, "constraint_list_subsumes_det: failed")
+ ).
+
+:- pred unify_constraint_list(list(prog_constraint)::in,
+ list(prog_constraint)::in, list(tvar)::in, tsubst::in, tsubst::out)
+ is semidet.
+
+unify_constraint_list([], [], _, !Subst).
+unify_constraint_list([A | As], [B | Bs], TVars, !Subst) :-
+ A = constraint(_, ArgsA),
+ B = constraint(_, ArgsB),
+ type_unify_list(ArgsA, ArgsB, TVars, !Subst),
+ unify_constraint_list(As, Bs, TVars, !Subst).
:- pred split_list_at_index(int::in, list(T)::in, list(T)::out, T::out,
list(T)::out) is det.
@@ -1517,6 +1575,7 @@
create_atomic_unification_with_nonlocals(Var, RHS, OldGoalInfo,
RestrictNonLocals, VarsList, UnifyContext, Goal) :-
goal_info_get_context(OldGoalInfo, Context),
+ goal_info_get_goal_path(OldGoalInfo, GoalPath),
UnifyContext = unify_context(UnifyMainContext, UnifySubContext),
create_atomic_complicated_unification(Var, RHS,
Context, UnifyMainContext, UnifySubContext, Goal0),
@@ -1525,7 +1584,13 @@
% Compute the nonlocals of the goal.
set__list_to_set(VarsList, NonLocals1),
set__intersect(RestrictNonLocals, NonLocals1, NonLocals),
- goal_info_set_nonlocals(NonLocals, GoalInfo0, GoalInfo),
+ goal_info_set_nonlocals(NonLocals, GoalInfo0, GoalInfo1),
+
+ % Use the goal path from the original goal, so that the constraint_ids
+ % will be as expected. (See the XXX comment near the definition of
+ % constraint_id in hlds_data.m for more info.)
+ goal_info_set_goal_path(GoalPath, GoalInfo1, GoalInfo),
+
Goal = GoalExpr0 - GoalInfo.
:- pred make_new_vars(list(mer_type)::in, list(prog_var)::out,
Index: compiler/typecheck.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/typecheck.m,v
retrieving revision 1.381
diff -u -r1.381 typecheck.m
--- compiler/typecheck.m 24 Oct 2005 04:14:32 -0000 1.381
+++ compiler/typecheck.m 25 Oct 2005 08:45:11 -0000
@@ -2828,7 +2828,7 @@
convert_field_access_cons_type_info(ClassTable, AccessType, FieldName,
FieldDefn, FunctorConsTypeInfo, OrigExistTVars, ConsTypeInfo) :-
- FunctorConsTypeInfo = cons_type_info(TVarSet0, ExistQVars0,
+ FunctorConsTypeInfo = cons_type_info(TVarSet0, ExistQVars,
FunctorType, ConsArgTypes, Constraints0),
FieldDefn = hlds_ctor_field_defn(_, _, _, _, FieldNumber),
list__index1_det(ConsArgTypes, FieldNumber, FieldType),
@@ -2837,20 +2837,12 @@
RetType = FieldType,
ArgTypes = [FunctorType],
TVarSet = TVarSet0,
- ExistQVars = ExistQVars0,
Constraints = Constraints0,
ConsTypeInfo = ok(cons_type_info(TVarSet, ExistQVars,
RetType, ArgTypes, Constraints))
;
AccessType = set,
- % A `'field :='/2' function has no existentially quantified type
- % variables - the values of all type variables in the field are
- % supplied by the caller, all the others are supplied by the
- % input term.
-
- ExistQVars = [],
-
% When setting a polymorphic field, the type of the field in the result
% is not necessarily the same as in the input. If a type variable
% occurs only in the field being set, create a new type variable for it
@@ -2870,12 +2862,10 @@
RetType = FunctorType,
ArgTypes = [FunctorType, FieldType],
- % Remove any existential constraints (which are in the unproven
- % field, since this is a construction). The typeclass-infos
- % supplied by the input term are local to the set function,
- % so they don't have to be considered here.
+ % None of the constraints are affected by the updated field,
+ % so the constraints are unchanged.
+ Constraints = Constraints0,
- Constraints = Constraints0 ^ unproven := [],
ConsTypeInfo = ok(cons_type_info(TVarSet, ExistQVars,
RetType, ArgTypes, Constraints))
;
@@ -2947,9 +2937,10 @@
)
).
- % Rename constraints containing variables that have been renamed.
- % These constraints are all universal constraints - the values
- % of the type variables are supplied by the caller.
+ % Add new universal constraints for constraints containing variables that
+ % have been renamed. These new constraints are the ones that will need
+ % to be supplied by the caller. The other constraints will be supplied
+ % from non-updated fields.
%
:- pred project_and_rename_constraints(class_table::in, tvarset::in,
set(tvar)::in, tvar_renaming::in,
@@ -2957,27 +2948,16 @@
project_and_rename_constraints(ClassTable, TVarSet, CallTVars, TVarRenaming,
!Constraints) :-
- !.Constraints = constraints(Unproven0, Assumed, _),
-
- % XXX We currently don't allow universal constraints on types or
- % data constructors (but we should). When we implement handling ofthose,
- % they will need to be renamed here as well. (The constraints have already
- % been flipped at this point, which is why we test the assumed constraints
- % here.)
- (
- Assumed = []
- ;
- Assumed = [_ | _],
- unexpected(this_file,
- "project_and_rename_constraints: universal constraints")
- ),
+ !.Constraints = constraints(Unproven0, Assumed, Redundant0),
% Project the constraints down onto the list of tvars in the call.
- list.filter(project_constraint(CallTVars), Unproven0, Unproven1),
- list.filter_map(rename_constraint(TVarRenaming), Unproven1, Unproven),
- update_redundant_constraints(ClassTable, TVarSet, Unproven,
- multi_map.init, Redundant),
- !:Constraints = constraints(Unproven, [], Redundant).
+ list.filter(project_constraint(CallTVars), Unproven0, NewUnproven0),
+ list.filter_map(rename_constraint(TVarRenaming), NewUnproven0,
+ NewUnproven),
+ update_redundant_constraints(ClassTable, TVarSet, NewUnproven,
+ Redundant0, Redundant),
+ list.append(NewUnproven, Unproven0, Unproven),
+ !:Constraints = constraints(Unproven, Assumed, Redundant).
:- pred project_constraint(set(tvar)::in, hlds_constraint::in) is semidet.
@@ -3268,18 +3248,29 @@
construct_type(TypeCtor, ConsTypeArgs, ConsType),
UnivProgConstraints = [],
(
- Action = do_not_flip_constraints
- ->
+ Action = do_not_flip_constraints,
ProgConstraints = constraints(UnivProgConstraints,
ExistProgConstraints),
ExistQVars = ExistQVars0
;
+ Action = flip_constraints_for_new,
% Make the existential constraints into universal ones, and discard
% the existentially quantified variables (since they are now
% universally quantified).
ProgConstraints = constraints(ExistProgConstraints,
UnivProgConstraints),
ExistQVars = []
+ ;
+ Action = flip_constraints_for_field_set,
+ % The constraints are existential for the deconstruction, and
+ % universal for the construction. Even though all of the unproven
+ % constraints here can be trivially reduced by the assumed ones,
+ % we still need to process them so that the appropriate tables
+ % get updated.
+ %
+ ProgConstraints = constraints(ExistProgConstraints,
+ ExistProgConstraints),
+ ExistQVars = ExistQVars0
),
make_body_hlds_constraints(ClassTable, ConsTypeVarSet,
GoalPath, ProgConstraints, Constraints),
Index: tests/hard_coded/typeclasses/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/hard_coded/typeclasses/Mmakefile,v
retrieving revision 1.54
diff -u -r1.54 Mmakefile
--- tests/hard_coded/typeclasses/Mmakefile 20 Apr 2005 12:57:35 -0000 1.54
+++ tests/hard_coded/typeclasses/Mmakefile 23 Oct 2005 05:29:02 -0000
@@ -23,6 +23,7 @@
fundeps_1 \
fundeps_2 \
fundeps_3 \
+ fundeps_4 \
ground_constraint \
ground_constraint_2 \
ho_map \
Index: tests/hard_coded/typeclasses/fundeps_4.exp
===================================================================
RCS file: tests/hard_coded/typeclasses/fundeps_4.exp
diff -N tests/hard_coded/typeclasses/fundeps_4.exp
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ tests/hard_coded/typeclasses/fundeps_4.exp 23 Oct 2005 05:45:56 -0000
@@ -0,0 +1 @@
+<<no info>>: V1 - <<no info>>;
Index: tests/hard_coded/typeclasses/fundeps_4.m
===================================================================
RCS file: tests/hard_coded/typeclasses/fundeps_4.m
diff -N tests/hard_coded/typeclasses/fundeps_4.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ tests/hard_coded/typeclasses/fundeps_4.m 23 Oct 2005 05:45:08 -0000
@@ -0,0 +1,61 @@
+:- module fundeps_4.
+:- interface.
+
+:- import_module assoc_list.
+:- import_module io.
+:- import_module string.
+
+:- pred main(io::di, io::uo) is det.
+
+:- type propagator_info
+ ---> some [P, V] propagator_info(P) => propagator_info(P, V).
+
+:- typeclass propagator_info(P, V) <= ((P -> V), variable_info(V)) where [
+ func propagator_name(P) = string,
+ func propagator_vars(P) = assoc_list(string, V)
+].
+
+:- typeclass variable_info(V) where [
+ func domain_desc(V) = string
+].
+
+:- func i = propagator_info.
+
+:- implementation.
+
+:- import_module list.
+:- import_module std_util.
+
+:- type no_propagator_info
+ ---> no_propagator_info.
+
+:- instance propagator_info(no_propagator_info, no_propagator_info) where [
+ (propagator_name(_) = "<<no info>>"),
+ (propagator_vars(_) = ["V1" - no_propagator_info])
+].
+
+:- instance variable_info(no_propagator_info) where [
+ (domain_desc(_) = "<<no info>>")
+].
+
+i = 'new propagator_info'(no_propagator_info).
+
+main(!IO) :-
+ write_propagator_info(i, !IO),
+ io.nl(!IO).
+
+:- pred write_propagator_info(propagator_info::in, io::di, io::uo) is det.
+
+write_propagator_info(propagator_info(P), !IO) :-
+ io.write_strings([propagator_name(P), ": "], !IO),
+ list.foldl(write_variable_info, propagator_vars(P), !IO).
+
+:- pred write_variable_info(pair(string, V), io, io) <= variable_info(V).
+:- mode write_variable_info(in, di, uo) is det.
+
+write_variable_info(N - V, !IO) :-
+ io.write_string(N, !IO),
+ io.write_string(" - ", !IO),
+ io.write_string(domain_desc(V), !IO),
+ io.write_string("; ", !IO).
+
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------
More information about the reviews
mailing list