[m-rev.] diff: fix superclass reduction
Mark Brown
mark at csse.unimelb.edu.au
Sun Oct 22 19:13:32 AEST 2006
Estimated hours taken: 15
Branches: main, release
Implement superclass reduction in the style of CHRs rather than as a top
down search. This is shorter, simpler, and more consistent with the rest
of the typeclass implementation. It also removes a few XXXs and fixes a
bug reported by Julien.
compiler/hlds_data.m:
Add an ancestors field to the hlds_constraint type. This caches
all the ancestors of assumed constraints, along with proofs (in the
form of a sequence of subclass constraints) of how each ancestor is
derived.
Update this field whenever new assumed constraints are created, by
traversing the class hierarchy bottom up.
Delete the old subclass_details type, which was part of the
superclass table.
compiler/typeclasses.m:
Use the cached ancestors to apply the class rules, rather than
performing a top down search.
compiler/type_util.m:
Apply substitutions to the ancestors.
compiler/typecheck.m:
compiler/typecheck_info.m:
Update to account for the additional field.
compiler/*.m:
Remove the superclass table from the module_info and from the
interface to context reduction; it is no longer needed.
compiler/hlds_out.m:
Don't output the superclass table.
tests/valid/Mmakefile:
tests/valid/superclass_bug.m:
Regression test for the bug that is now fixed.
Index: compiler/add_class.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/add_class.m,v
retrieving revision 1.22
diff -u -r1.22 add_class.m
--- compiler/add_class.m 13 Oct 2006 04:52:16 -0000 1.22
+++ compiler/add_class.m 21 Oct 2006 15:51:01 -0000
@@ -79,7 +79,6 @@
module_add_class_defn(Constraints, FunDeps, Name, Vars, Interface, VarSet,
Context, Status, !ModuleInfo, !Specs) :-
module_info_get_class_table(!.ModuleInfo, Classes0),
- module_info_get_superclass_table(!.ModuleInfo, SuperClasses0),
list.length(Vars, ClassArity),
ClassId = class_id(Name, ClassArity),
Status = item_status(ImportStatus0, _),
@@ -183,10 +182,6 @@
(
IsNewDefn = yes,
- update_superclass_table(ClassId, Vars, VarSet, Constraints,
- SuperClasses0, SuperClasses),
-
- module_info_set_superclass_table(SuperClasses, !ModuleInfo),
% When we find the class declaration, make an
% entry for the instances.
@@ -393,27 +388,6 @@
)
).
- % Insert an entry into the super class table for each super class of
- % this class.
- %
-:- 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).
-
% Go through the list of class methods, looking for
% - functions without mode declarations: add a default mode
% - predicates without mode declarations: report an error
Index: compiler/check_typeclass.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/check_typeclass.m,v
retrieving revision 1.103
diff -u -r1.103 check_typeclass.m
--- compiler/check_typeclass.m 13 Oct 2006 04:52:16 -0000 1.103
+++ compiler/check_typeclass.m 21 Oct 2006 14:42:49 -0000
@@ -821,7 +821,6 @@
module_info_get_class_table(ModuleInfo, ClassTable),
module_info_get_instance_table(ModuleInfo, InstanceTable),
- module_info_get_superclass_table(ModuleInfo, SuperClassTable),
% Build a suitable constraint context for checking the instance.
% To do this, we assume any constraints on the instance declaration
@@ -840,11 +839,9 @@
% Try to reduce the superclass constraints, using the declared instance
% constraints and the usual context reduction rules.
map.init(ConstraintMap0),
- typeclasses.reduce_context_by_rule_application(ClassTable,
- InstanceTable, SuperClassTable, ClassVars, TypeSubst, _,
- InstanceVarSet1, InstanceVarSet2,
- Proofs0, Proofs1, ConstraintMap0, _,
- Constraints0, Constraints),
+ typeclasses.reduce_context_by_rule_application(ClassTable, InstanceTable,
+ ClassVars, TypeSubst, _, InstanceVarSet1, InstanceVarSet2,
+ Proofs0, Proofs1, ConstraintMap0, _, Constraints0, Constraints),
UnprovenConstraints = Constraints ^ unproven,
(
Index: compiler/hlds_data.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/hlds_data.m,v
retrieving revision 1.109
diff -u -r1.109 hlds_data.m
--- compiler/hlds_data.m 20 Aug 2006 08:21:09 -0000 1.109
+++ compiler/hlds_data.m 21 Oct 2006 18:09:29 -0000
@@ -36,6 +36,7 @@
:- import_module parse_tree.prog_type_subst.
:- import_module int.
+:- import_module svmap.
:- import_module svmulti_map.
:- import_module term.
:- import_module varset.
@@ -933,7 +934,7 @@
% constraints from the goal being checked, or
% universal constraints on the head).
- redundant :: redundant_constraints
+ redundant :: redundant_constraints,
% Constraints that are known to be redundant.
% This includes constraints that have already been
% proved as well as constraints that are ancestors
@@ -941,6 +942,9 @@
% constraints. Not all such constraints are
% included, only those which may be used for
% the purposes of improvement.
+
+ ancestors :: ancestor_constraints
+ % Ancestors of assumed constraints.
).
% Redundant constraints are partitioned by class, which helps us
@@ -948,6 +952,16 @@
%
:- type redundant_constraints == multi_map(class_id, hlds_constraint).
+ % Constraints which are ancestors of assumed constraints, along with the
+ % list of constraints (following the class hierarchy) which leads to
+ % the assumed constraint. The assumed constraint is the last item in the
+ % list.
+ %
+ % Note that if there are two possible lists for the same constraint, we
+ % always keep the shorter one.
+ %
+:- type ancestor_constraints == map(prog_constraint, list(prog_constraint)).
+
% 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.
@@ -1045,7 +1059,7 @@
:- implementation.
empty_hlds_constraints(Constraints) :-
- Constraints = constraints([], [], multi_map.init).
+ Constraints = constraints([], [], multi_map.init, map.init).
init_hlds_constraint_list(ProgConstraints, Constraints) :-
list.map(init_hlds_constraint, ProgConstraints, Constraints).
@@ -1080,7 +1094,9 @@
Unproven, multi_map.init, Redundant0),
list.foldl(update_redundant_constraints_2(ClassTable, TVarSet),
Assumed, Redundant0, Redundant),
- Constraints = constraints(Unproven, Assumed, Redundant).
+ list.foldl(update_ancestor_constraints(ClassTable, TVarSet),
+ Assumed, map.init, Ancestors),
+ Constraints = constraints(Unproven, Assumed, Redundant, Ancestors).
make_hlds_constraint_list(ProgConstraints, ConstraintType, GoalPath,
Constraints) :-
@@ -1101,15 +1117,31 @@
N + 1, HLDSConstraints).
merge_hlds_constraints(ConstraintsA, ConstraintsB, Constraints) :-
- ConstraintsA = constraints(UnprovenA, AssumedA, RedundantA),
- ConstraintsB = constraints(UnprovenB, AssumedB, RedundantB),
+ ConstraintsA = constraints(UnprovenA, AssumedA, RedundantA, AncestorsA),
+ ConstraintsB = constraints(UnprovenB, AssumedB, RedundantB, AncestorsB),
list.append(UnprovenA, UnprovenB, Unproven),
list.append(AssumedA, AssumedB, Assumed),
multi_map.merge(RedundantA, RedundantB, Redundant),
- Constraints = constraints(Unproven, Assumed, Redundant).
+ map.union(shortest_list, AncestorsA, AncestorsB, Ancestors),
+ Constraints = constraints(Unproven, Assumed, Redundant, Ancestors).
+
+:- pred shortest_list(list(T)::in, list(T)::in, list(T)::out) is det.
+
+shortest_list(As, Bs, Cs) :-
+ ( is_shorter(As, Bs) ->
+ Cs = As
+ ;
+ Cs = Bs
+ ).
+
+:- pred is_shorter(list(T)::in, list(T)::in) is semidet.
+
+is_shorter([], _).
+is_shorter([_ | As], [_ | Bs]) :-
+ is_shorter(As, Bs).
retrieve_prog_constraints(Constraints, ProgConstraints) :-
- Constraints = constraints(Unproven, Assumed, _),
+ Constraints = constraints(Unproven, Assumed, _, _),
retrieve_prog_constraint_list(Unproven, UnivProgConstraints),
retrieve_prog_constraint_list(Assumed, ExistProgConstraints),
ProgConstraints = constraints(UnivProgConstraints, ExistProgConstraints).
@@ -1224,26 +1256,65 @@
%-----------------------------------------------------------------------------%
-:- interface.
-
-:- type subclass_details
- ---> subclass_details(
- subclass_types :: list(mer_type),
- % Arguments of the superclass constraint.
-
- subclass_id :: class_id,
- % Name of the subclass.
+ % Search the superclasses of the given constraint for a potential proof,
+ % and add it to the map if no better proof exists already.
+ %
+:- pred update_ancestor_constraints(class_table::in, tvarset::in,
+ hlds_constraint::in, ancestor_constraints::in, ancestor_constraints::out)
+ is det.
- subclass_tvars :: list(tvar),
- % Variables of the subclass.
+update_ancestor_constraints(ClassTable, TVarSet, HLDSConstraint, !Ancestors) :-
+ retrieve_prog_constraint(HLDSConstraint, Constraint),
+ update_ancestor_constraints_2(ClassTable, TVarSet, [], Constraint,
+ !Ancestors).
+
+:- pred update_ancestor_constraints_2(class_table::in, tvarset::in,
+ list(prog_constraint)::in, prog_constraint::in,
+ ancestor_constraints::in, ancestor_constraints::out) is det.
+
+update_ancestor_constraints_2(ClassTable, TVarSet, Descendants0, Constraint,
+ !Ancestors) :-
+ Constraint = constraint(Class, Args),
+ list.length(Args, Arity),
+ ClassId = class_id(Class, Arity),
+ map.lookup(ClassTable, ClassId, ClassDefn),
- subclass_tvarset :: tvarset
- % The names of these vars.
- ).
+ % We can ignore the resulting tvarset, since any new variables
+ % will become bound when the arguments are bound. (This follows
+ % from the fact that constraints on class declarations can only use
+ % variables that appear in the head of the declaration.)
+
+ tvarset_merge_renaming(TVarSet, ClassDefn ^ class_tvarset, _, Renaming),
+ apply_variable_renaming_to_prog_constraint_list(Renaming,
+ ClassDefn ^ class_supers, RenamedSupers),
+ apply_variable_renaming_to_tvar_list(Renaming, ClassDefn ^ class_vars,
+ RenamedParams),
+ map.from_corresponding_lists(RenamedParams, Args, Subst),
+ apply_subst_to_prog_constraint_list(Subst, RenamedSupers, Supers),
+
+ Descendants = [Constraint | Descendants0],
+ list.foldl(update_ancestor_constraints_3(ClassTable, TVarSet, Descendants),
+ Supers, !Ancestors).
+
+:- pred update_ancestor_constraints_3(class_table::in, tvarset::in,
+ list(prog_constraint)::in, prog_constraint::in,
+ ancestor_constraints::in, ancestor_constraints::out) is det.
- % I'm sure there's a very clever way of doing this with graphs
- % or relations...
-:- type superclass_table == multi_map(class_id, subclass_details).
+update_ancestor_constraints_3(ClassTable, TVarSet, Descendants, Constraint,
+ !Ancestors) :-
+ (
+ map.search(!.Ancestors, Constraint, OldDescendants),
+ is_shorter(OldDescendants, Descendants)
+ ->
+ % We don't want to update the ancestors because we already have a
+ % better path. The same will apply for all superclasses, so we
+ % don't traverse any further.
+ true
+ ;
+ svmap.set(Constraint, Descendants, !Ancestors),
+ update_ancestor_constraints_2(ClassTable, TVarSet, Descendants,
+ Constraint, !Ancestors)
+ ).
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
Index: compiler/hlds_module.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/hlds_module.m,v
retrieving revision 1.142
diff -u -r1.142 hlds_module.m
--- compiler/hlds_module.m 25 Sep 2006 18:31:22 -0000 1.142
+++ compiler/hlds_module.m 21 Oct 2006 14:47:32 -0000
@@ -275,12 +275,6 @@
:- pred module_info_set_instance_table(instance_table::in,
module_info::in, module_info::out) is det.
-:- pred module_info_get_superclass_table(module_info::in,
- superclass_table::out) is det.
-
-:- pred module_info_set_superclass_table(superclass_table::in,
- module_info::in, module_info::out) is det.
-
:- pred module_info_get_assertion_table(module_info::in, assertion_table::out)
is det.
@@ -660,7 +654,6 @@
cons_table :: cons_table,
class_table :: class_table,
instance_table :: instance_table,
- superclass_table :: superclass_table,
assertion_table :: assertion_table,
exclusive_table :: exclusive_table,
ctor_field_table :: ctor_field_table,
@@ -794,7 +787,6 @@
map.init(ClassTable),
map.init(InstanceTable),
- map.init(SuperClassTable),
% The builtin modules are automatically imported.
get_implicit_dependencies(Items, Globals, ImportDeps, UseDeps),
@@ -814,8 +806,8 @@
map.init, used_modules_init, set.init),
ModuleInfo = module_info(ModuleSubInfo, PredicateTable, Requests,
UnifyPredMap, QualifierInfo, Types, Insts, Modes, Ctors,
- ClassTable, SuperClassTable, InstanceTable, AssertionTable,
- ExclusiveTable, FieldNameTable, RecompInfo).
+ ClassTable, InstanceTable, AssertionTable, ExclusiveTable,
+ FieldNameTable, RecompInfo).
%-----------------------------------------------------------------------------%
%
@@ -832,7 +824,6 @@
module_info_get_cons_table(MI, MI ^ cons_table).
module_info_get_class_table(MI, MI ^ class_table).
module_info_get_instance_table(MI, MI ^ instance_table).
-module_info_get_superclass_table(MI, MI ^ superclass_table).
module_info_get_assertion_table(MI, MI ^ assertion_table).
module_info_get_exclusive_table(MI, MI ^ exclusive_table).
module_info_get_ctor_field_table(MI, MI ^ ctor_field_table).
@@ -853,7 +844,6 @@
module_info_set_cons_table(C, MI, MI ^ cons_table := C).
module_info_set_class_table(C, MI, MI ^ class_table := C).
module_info_set_instance_table(I, MI, MI ^ instance_table := I).
-module_info_set_superclass_table(S, MI, MI ^ superclass_table := S).
module_info_set_assertion_table(A, MI, MI ^ assertion_table := A).
module_info_set_exclusive_table(PXT, MI, MI ^ exclusive_table := PXT).
module_info_set_ctor_field_table(CF, MI, MI ^ ctor_field_table := CF).
Index: compiler/hlds_out.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/hlds_out.m,v
retrieving revision 1.408
diff -u -r1.408 hlds_out.m
--- compiler/hlds_out.m 15 Oct 2006 23:26:40 -0000 1.408
+++ compiler/hlds_out.m 21 Oct 2006 14:48:03 -0000
@@ -691,7 +691,6 @@
module_info_get_inst_table(Module, InstTable),
module_info_get_mode_table(Module, ModeTable),
module_info_get_class_table(Module, ClassTable),
- module_info_get_superclass_table(Module, SuperClassTable),
module_info_get_instance_table(Module, InstanceTable),
write_header(Indent, Module, !IO),
globals.io_lookup_string_option(dump_hlds_options, Verbose, !IO),
@@ -705,8 +704,6 @@
io.write_string("\n", !IO),
write_classes(Indent, ClassTable, !IO),
io.write_string("\n", !IO),
- write_superclasses(Indent, SuperClassTable, !IO),
- io.write_string("\n", !IO),
write_instances(Indent, InstanceTable, !IO),
io.write_string("\n", !IO)
;
@@ -3426,55 +3423,6 @@
%-----------------------------------------------------------------------------%
-:- pred write_superclasses(int::in, superclass_table::in, io::di, io::uo)
- is det.
-
-write_superclasses(Indent, SuperClassTable, !IO) :-
- write_indent(Indent, !IO),
- io.write_string("%-------- Super Classes --------\n", !IO),
- multi_map.to_assoc_list(SuperClassTable, SuperClassTableList),
- io.write_list(SuperClassTableList, "\n\n", write_superclass(Indent), !IO),
- io.nl(!IO).
-
-:- pred write_superclass(int::in, pair(class_id, list(subclass_details))::in,
- io::di, io::uo) is det.
-
-write_superclass(Indent, ClassId - SubClassDetailsList, !IO) :-
- write_indent(Indent, !IO),
- io.write_string("% ", !IO),
- write_class_id(ClassId, !IO),
- io.write_string(":\n", !IO),
-
- io.write_list(SubClassDetailsList, "\n",
- write_subclass_details(Indent, ClassId), !IO).
-
-:- pred write_subclass_details(int::in, class_id::in, subclass_details::in,
- io::di, io::uo) is det.
-
-write_subclass_details(Indent, SuperClassId, SubClassDetails, !IO) :-
- SubClassDetails = subclass_details(SuperClassVars, SubClassId,
- SubClassVars, VarSet),
-
- % Curry the varset for term_io.write_variable/4.
- PrintVar = (pred(VarName::in, IO0::di, IO::uo) is det :-
- term_io.write_variable(VarName, VarSet, IO0, IO)
- ),
- write_indent(Indent, !IO),
- io.write_string("% ", !IO),
- SubClassId = class_id(SubSymName, _SubArity),
- prog_out.write_sym_name(SubSymName, !IO),
- io.write_char('(', !IO),
- io.write_list(SubClassVars, ", ", PrintVar, !IO),
- io.write_string(") <= ", !IO),
-
- SuperClassId = class_id(SuperSymName, _SuperArity),
- prog_out.write_sym_name(SuperSymName, !IO),
- io.write_char('(', !IO),
- io.write_list(SuperClassVars, ", ", mercury_output_type(VarSet, no), !IO),
- io.write_char(')', !IO).
-
-%-----------------------------------------------------------------------------%
-
:- pred write_instances(int::in, instance_table::in, io::di, io::uo) is det.
write_instances(Indent, InstanceTable, !IO) :-
Index: compiler/type_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/type_util.m,v
retrieving revision 1.172
diff -u -r1.172 type_util.m
--- compiler/type_util.m 1 Oct 2006 04:57:32 -0000 1.172
+++ compiler/type_util.m 21 Oct 2006 18:11:05 -0000
@@ -923,34 +923,55 @@
%-----------------------------------------------------------------------------%
apply_variable_renaming_to_constraints(Renaming, !Constraints) :-
- !.Constraints = constraints(Unproven0, Assumed0, Redundant0),
+ !.Constraints = constraints(Unproven0, Assumed0, Redundant0, Ancestors0),
apply_variable_renaming_to_constraint_list(Renaming, Unproven0, Unproven),
apply_variable_renaming_to_constraint_list(Renaming, Assumed0, Assumed),
Pred = (pred(_::in, C0::in, C::out) is det :-
apply_variable_renaming_to_constraint_list(Renaming, C0, C)
),
map.map_values(Pred, Redundant0, Redundant),
- !:Constraints = constraints(Unproven, Assumed, Redundant).
+ map.keys(Ancestors0, AncestorsKeys0),
+ map.values(Ancestors0, AncestorsValues0),
+ apply_variable_renaming_to_prog_constraint_list(Renaming, AncestorsKeys0,
+ AncestorsKeys),
+ list.map(apply_variable_renaming_to_prog_constraint_list(Renaming),
+ AncestorsValues0, AncestorsValues),
+ map.from_corresponding_lists(AncestorsKeys, AncestorsValues, Ancestors),
+ !:Constraints = constraints(Unproven, Assumed, Redundant, Ancestors).
apply_subst_to_constraints(Subst, !Constraints) :-
- !.Constraints = constraints(Unproven0, Assumed0, Redundant0),
+ !.Constraints = constraints(Unproven0, Assumed0, Redundant0, Ancestors0),
apply_subst_to_constraint_list(Subst, Unproven0, Unproven),
apply_subst_to_constraint_list(Subst, Assumed0, Assumed),
Pred = (pred(_::in, C0::in, C::out) is det :-
apply_subst_to_constraint_list(Subst, C0, C)
),
map.map_values(Pred, Redundant0, Redundant),
- !:Constraints = constraints(Unproven, Assumed, Redundant).
+ map.keys(Ancestors0, AncestorsKeys0),
+ map.values(Ancestors0, AncestorsValues0),
+ apply_subst_to_prog_constraint_list(Subst, AncestorsKeys0,
+ AncestorsKeys),
+ list.map(apply_subst_to_prog_constraint_list(Subst),
+ AncestorsValues0, AncestorsValues),
+ map.from_corresponding_lists(AncestorsKeys, AncestorsValues, Ancestors),
+ !:Constraints = constraints(Unproven, Assumed, Redundant, Ancestors).
apply_rec_subst_to_constraints(Subst, !Constraints) :-
- !.Constraints = constraints(Unproven0, Assumed0, Redundant0),
+ !.Constraints = constraints(Unproven0, Assumed0, Redundant0, Ancestors0),
apply_rec_subst_to_constraint_list(Subst, Unproven0, Unproven),
apply_rec_subst_to_constraint_list(Subst, Assumed0, Assumed),
Pred = (pred(_::in, C0::in, C::out) is det :-
apply_rec_subst_to_constraint_list(Subst, C0, C)
),
map.map_values(Pred, Redundant0, Redundant),
- !:Constraints = constraints(Unproven, Assumed, Redundant).
+ map.keys(Ancestors0, AncestorsKeys0),
+ map.values(Ancestors0, AncestorsValues0),
+ apply_rec_subst_to_prog_constraint_list(Subst, AncestorsKeys0,
+ AncestorsKeys),
+ list.map(apply_rec_subst_to_prog_constraint_list(Subst),
+ AncestorsValues0, AncestorsValues),
+ map.from_corresponding_lists(AncestorsKeys, AncestorsValues, Ancestors),
+ !:Constraints = constraints(Unproven, Assumed, Redundant, Ancestors).
%-----------------------------------------------------------------------------%
Index: compiler/typecheck.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/typecheck.m,v
retrieving revision 1.407
diff -u -r1.407 typecheck.m
--- compiler/typecheck.m 13 Oct 2006 04:52:26 -0000 1.407
+++ compiler/typecheck.m 21 Oct 2006 17:44:23 -0000
@@ -2788,7 +2788,7 @@
project_and_rename_constraints(ClassTable, TVarSet, CallTVars, TVarRenaming,
!Constraints) :-
- !.Constraints = constraints(Unproven0, Assumed, Redundant0),
+ !.Constraints = constraints(Unproven0, Assumed, Redundant0, Ancestors),
% Project the constraints down onto the list of tvars in the call.
list.filter(project_constraint(CallTVars), Unproven0, NewUnproven0),
@@ -2797,7 +2797,7 @@
update_redundant_constraints(ClassTable, TVarSet, NewUnproven,
Redundant0, Redundant),
list.append(NewUnproven, Unproven0, Unproven),
- !:Constraints = constraints(Unproven, Assumed, Redundant).
+ !:Constraints = constraints(Unproven, Assumed, Redundant, Ancestors).
:- pred project_constraint(set(tvar)::in, hlds_constraint::in) is semidet.
Index: compiler/typecheck_info.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/typecheck_info.m,v
retrieving revision 1.18
diff -u -r1.18 typecheck_info.m
--- compiler/typecheck_info.m 27 Sep 2006 06:17:08 -0000 1.18
+++ compiler/typecheck_info.m 21 Oct 2006 16:02:41 -0000
@@ -424,7 +424,7 @@
% constraint map now.
HLDSTypeConstraints = constraints(HLDSUnivConstraints,
- HLDSExistConstraints, _),
+ HLDSExistConstraints, _, _),
list.foldl(update_constraint_map, HLDSUnivConstraints,
ConstraintMap1, ConstraintMap2),
list.foldl(update_constraint_map, HLDSExistConstraints,
@@ -830,7 +830,7 @@
write_type_assign_hlds_constraints(Constraints, TypeBindings, TypeVarSet,
!IO) :-
- Constraints = constraints(ConstraintsToProve, AssumedConstraints, _),
+ Constraints = constraints(ConstraintsToProve, AssumedConstraints, _, _),
write_type_assign_constraints("&", AssumedConstraints,
TypeBindings, TypeVarSet, no, !IO),
write_type_assign_constraints("<=", ConstraintsToProve,
@@ -841,7 +841,7 @@
type_assign_hlds_constraints_to_pieces(Constraints, TypeBindings, TypeVarSet)
= Pieces1 ++ Pieces2 :-
- Constraints = constraints(ConstraintsToProve, AssumedConstraints, _),
+ Constraints = constraints(ConstraintsToProve, AssumedConstraints, _, _),
PiecesList1 = type_assign_constraints_to_pieces_list("&",
AssumedConstraints, TypeBindings, TypeVarSet, no),
PiecesList2 = type_assign_constraints_to_pieces_list("<=",
Index: compiler/typeclasses.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/typeclasses.m,v
retrieving revision 1.16
diff -u -r1.16 typeclasses.m
--- compiler/typeclasses.m 27 Sep 2006 06:17:08 -0000 1.16
+++ compiler/typeclasses.m 21 Oct 2006 17:44:18 -0000
@@ -76,9 +76,8 @@
% the instance rules or superclass rules, building up proofs for
% redundant constraints.
%
-:- pred reduce_context_by_rule_application(class_table::in,
- instance_table::in, superclass_table::in, head_type_params::in,
- tsubst::in, tsubst::out, tvarset::in, tvarset::out,
+:- pred reduce_context_by_rule_application(class_table::in, instance_table::in,
+ head_type_params::in, tsubst::in, tsubst::out, tvarset::in, tvarset::out,
constraint_proof_map::in, constraint_proof_map::out,
constraint_map::in, constraint_map::out,
hlds_constraints::in, hlds_constraints::out) is det.
@@ -101,6 +100,7 @@
:- import_module multi_map.
:- import_module pair.
:- import_module set.
+:- import_module svmap.
:- import_module term.
:- import_module varset.
@@ -112,11 +112,10 @@
),
typecheck_info_get_module_info(!.Info, ModuleInfo),
module_info_get_class_table(ModuleInfo, ClassTable),
- module_info_get_superclass_table(ModuleInfo, SuperClassTable),
module_info_get_instance_table(ModuleInfo, InstanceTable),
typecheck_info_get_type_assign_set(!.Info, TypeAssignSet0),
list.filter_map(
- reduce_type_assign_context(ClassTable, SuperClassTable, InstanceTable),
+ reduce_type_assign_context(ClassTable, InstanceTable),
TypeAssignSet0, TypeAssignSet),
(
% Check that this context reduction hasn't eliminated
@@ -139,11 +138,10 @@
typecheck_info_set_type_assign_set(TypeAssignSet, !Info)
).
-:- pred reduce_type_assign_context(class_table::in, superclass_table::in,
- instance_table::in, type_assign::in, type_assign::out) is semidet.
+:- pred reduce_type_assign_context(class_table::in, instance_table::in,
+ type_assign::in, type_assign::out) is semidet.
-reduce_type_assign_context(ClassTable, SuperClassTable, InstanceTable,
- !TypeAssign) :-
+reduce_type_assign_context(ClassTable, InstanceTable, !TypeAssign) :-
type_assign_get_head_type_params(!.TypeAssign, HeadTypeParams),
type_assign_get_type_bindings(!.TypeAssign, Bindings0),
type_assign_get_typeclass_constraints(!.TypeAssign, Constraints0),
@@ -151,10 +149,10 @@
type_assign_get_constraint_proofs(!.TypeAssign, Proofs0),
type_assign_get_constraint_map(!.TypeAssign, ConstraintMap0),
- typeclasses.reduce_context_by_rule_application(ClassTable,
- InstanceTable, SuperClassTable, HeadTypeParams,
- Bindings0, Bindings, TVarSet0, TVarSet, Proofs0, Proofs,
- ConstraintMap0, ConstraintMap, Constraints0, Constraints),
+ typeclasses.reduce_context_by_rule_application(ClassTable, InstanceTable,
+ HeadTypeParams, Bindings0, Bindings, TVarSet0, TVarSet,
+ Proofs0, Proofs, ConstraintMap0, ConstraintMap,
+ Constraints0, Constraints),
check_satisfiability(Constraints ^ unproven, HeadTypeParams),
type_assign_set_type_bindings(Bindings, !TypeAssign),
@@ -163,25 +161,22 @@
type_assign_set_constraint_proofs(Proofs, !TypeAssign),
type_assign_set_constraint_map(ConstraintMap, !TypeAssign).
-reduce_context_by_rule_application(ClassTable, InstanceTable,
- SuperClassTable, HeadTypeParams, !Bindings, !TVarSet, !Proofs,
- !ConstraintMap, !Constraints) :-
- reduce_context_by_rule_application_2(ClassTable,
- InstanceTable, SuperClassTable, HeadTypeParams, !Bindings,
- !TVarSet, !Proofs, !ConstraintMap, !Constraints,
- !.Constraints ^ unproven, _).
+reduce_context_by_rule_application(ClassTable, InstanceTable, HeadTypeParams,
+ !Bindings, !TVarSet, !Proofs, !ConstraintMap, !Constraints) :-
+ reduce_context_by_rule_application_2(ClassTable, InstanceTable,
+ HeadTypeParams, !Bindings, !TVarSet, !Proofs, !ConstraintMap,
+ !Constraints, !.Constraints ^ unproven, _).
:- pred reduce_context_by_rule_application_2(class_table::in,
- instance_table::in, superclass_table::in, head_type_params::in,
+ instance_table::in, head_type_params::in,
tsubst::in, tsubst::out, tvarset::in, tvarset::out,
constraint_proof_map::in, constraint_proof_map::out,
constraint_map::in, constraint_map::out,
hlds_constraints::in, hlds_constraints::out,
list(hlds_constraint)::in, list(hlds_constraint)::out) is det.
-reduce_context_by_rule_application_2(ClassTable, InstanceTable,
- SuperClassTable, HeadTypeParams, !Bindings, !TVarSet, !Proofs,
- !ConstraintMap, !Constraints, !Seen) :-
+reduce_context_by_rule_application_2(ClassTable, InstanceTable, HeadTypeParams,
+ !Bindings, !TVarSet, !Proofs, !ConstraintMap, !Constraints, !Seen) :-
apply_rec_subst_to_constraints(!.Bindings, !Constraints),
apply_improvement_rules(ClassTable, InstanceTable, HeadTypeParams,
!.Constraints, !TVarSet, !Bindings, AppliedImprovementRule),
@@ -202,10 +197,7 @@
EliminatedAssumed),
apply_instance_rules(ClassTable, InstanceTable, !TVarSet, !Proofs,
!ConstraintMap, !Seen, !Constraints, AppliedInstanceRule),
- % XXX Kind inference: we assume that all tvars have kind `star'.
- map.init(KindMap),
- apply_class_rules(SuperClassTable, !.TVarSet, KindMap, !Proofs,
- !ConstraintMap, !Constraints, AppliedClassRule),
+ apply_class_rules(!Proofs, !ConstraintMap, !Constraints, AppliedClassRule),
(
AppliedImprovementRule = no,
EliminatedAssumed = no,
@@ -215,9 +207,9 @@
% We have reached fixpoint.
sort_and_merge_dups(!Constraints)
;
- reduce_context_by_rule_application_2(ClassTable,
- InstanceTable, SuperClassTable, HeadTypeParams, !Bindings,
- !TVarSet, !Proofs, !ConstraintMap, !Constraints, !Seen)
+ reduce_context_by_rule_application_2(ClassTable, InstanceTable,
+ HeadTypeParams, !Bindings, !TVarSet, !Proofs, !ConstraintMap,
+ !Constraints, !Seen)
).
:- pred sort_and_merge_dups(hlds_constraints::in, hlds_constraints::out)
@@ -501,10 +493,10 @@
hlds_constraints::in, hlds_constraints::out, bool::out) is det.
eliminate_assumed_constraints(!ConstraintMap, !Constraints, Changed) :-
- !.Constraints = constraints(Unproven0, Assumed, Redundant),
+ !.Constraints = constraints(Unproven0, Assumed, Redundant, Ancestors),
eliminate_assumed_constraints_2(Assumed, !ConstraintMap,
Unproven0, Unproven, Changed),
- !:Constraints = constraints(Unproven, Assumed, Redundant).
+ !:Constraints = constraints(Unproven, Assumed, Redundant, Ancestors).
:- pred eliminate_assumed_constraints_2(list(hlds_constraint)::in,
constraint_map::in, constraint_map::out,
@@ -539,11 +531,11 @@
apply_instance_rules(ClassTable, InstanceTable, !TVarSet, !Proofs,
!ConstraintMap, !Seen, !Constraints, Changed) :-
- !.Constraints = constraints(Unproven0, Assumed, Redundant0),
+ !.Constraints = constraints(Unproven0, Assumed, Redundant0, Ancestors),
apply_instance_rules_2(ClassTable, InstanceTable, !TVarSet, !Proofs,
!ConstraintMap, Redundant0, Redundant, !Seen,
Unproven0, Unproven, Changed),
- !:Constraints = constraints(Unproven, Assumed, Redundant).
+ !:Constraints = constraints(Unproven, Assumed, Redundant, Ancestors).
:- pred apply_instance_rules_2(class_table::in, instance_table::in,
tvarset::in, tvarset::out,
@@ -650,170 +642,49 @@
).
% To reduce a constraint using class declarations, we search the
- % superclass relation to find a path from the inferred constraint to
- % another (declared or inferred) constraint.
+ % ancestors in the hlds_constraints to find a path from the inferred
+ % constraint to another (declared or inferred) constraint.
%
-:- pred apply_class_rules(superclass_table::in, tvarset::in, tvar_kind_map::in,
- constraint_proof_map::in, constraint_proof_map::out,
+:- pred apply_class_rules(constraint_proof_map::in, constraint_proof_map::out,
constraint_map::in, constraint_map::out,
hlds_constraints::in, hlds_constraints::out, bool::out) is det.
-apply_class_rules(SuperClassTable, TVarSet, KindMap, !Proofs, !ConstraintMap,
- !Constraints, Changed) :-
- !.Constraints = constraints(Unproven0, Assumed, _),
- apply_class_rules_2(Assumed, SuperClassTable, TVarSet, KindMap,
- !Proofs, !ConstraintMap, Unproven0, Unproven, Changed),
+apply_class_rules(!Proofs, !ConstraintMap, !Constraints, Changed) :-
+ !.Constraints = constraints(Unproven0, _, _, Ancestors),
+ apply_class_rules_2(Ancestors, !Proofs, !ConstraintMap,
+ Unproven0, Unproven, Changed),
!:Constraints = !.Constraints ^ unproven := Unproven.
-:- pred apply_class_rules_2(list(hlds_constraint)::in, superclass_table::in,
- tvarset::in, tvar_kind_map::in, constraint_proof_map::in,
- constraint_proof_map::out, constraint_map::in, constraint_map::out,
- list(hlds_constraint)::in, list(hlds_constraint)::out,
- bool::out) is det.
+:- pred apply_class_rules_2(ancestor_constraints::in,
+ constraint_proof_map::in, constraint_proof_map::out,
+ constraint_map::in, constraint_map::out,
+ list(hlds_constraint)::in, list(hlds_constraint)::out, bool::out) is det.
-apply_class_rules_2(_, _, _, _, !Proofs, !ConstraintMap, [], [], no).
-apply_class_rules_2(AssumedConstraints, SuperClassTable, TVarSet, KindMap,
- !Proofs, !ConstraintMap, [Constraint0 | Constraints0],
- Constraints, Changed) :-
- Parents = [],
+apply_class_rules_2(_, !Proofs, !ConstraintMap, [], [], no).
+apply_class_rules_2(Ancestors, !Proofs, !ConstraintMap,
+ [Constraint0 | Constraints0], Constraints, Changed) :-
retrieve_prog_constraint(Constraint0, ProgConstraint0),
-
- % The head_type_params argument contains all the variables from the
- % original constraint that we are trying to prove. (These are the type
- % variables that must not be bound as we search through the superclass
- % relation).
- constraint_get_tvars(ProgConstraint0, HeadTypeParams),
(
- eliminate_constraint_by_class_rules(ProgConstraint0, _, _,
- AssumedConstraints, SuperClassTable, HeadTypeParams,
- TVarSet, KindMap, Parents, !Proofs)
+ map.search(Ancestors, ProgConstraint0, Descendants)
->
update_constraint_map(Constraint0, !ConstraintMap),
- apply_class_rules_2(AssumedConstraints, SuperClassTable,
- TVarSet, KindMap, !Proofs, !ConstraintMap,
+ add_superclass_proofs(ProgConstraint0, Descendants, !Proofs),
+ apply_class_rules_2(Ancestors, !Proofs, !ConstraintMap,
Constraints0, Constraints, _),
Changed = yes
;
- apply_class_rules_2(AssumedConstraints, SuperClassTable,
- TVarSet, KindMap, !Proofs, !ConstraintMap,
+ apply_class_rules_2(Ancestors, !Proofs, !ConstraintMap,
Constraints0, TailConstraints, Changed),
Constraints = [Constraint0 | TailConstraints]
).
- % eliminate_constraint_by_class_rules eliminates a class constraint
- % by applying the superclass relation. A list of "parent" constraints
- % is also passed in --- these are the constraints that we are
- % (recursively) in the process of checking, and is used to ensure that
- % we don't get into a cycle in the relation.
- %
-:- pred eliminate_constraint_by_class_rules(prog_constraint::in,
- prog_constraint::out, tsubst::out, list(hlds_constraint)::in,
- superclass_table::in, head_type_params::in, tvarset::in,
- tvar_kind_map::in, list(prog_constraint)::in,
- constraint_proof_map::in, constraint_proof_map::out) is semidet.
-
-eliminate_constraint_by_class_rules(C, SubstC, SubClassSubst,
- AssumedConstraints, SuperClassTable, HeadTypeParams, TVarSet,
- KindMap, ParentConstraints, Proofs0, Proofs) :-
-
- % Make sure we aren't in a cycle in the superclass relation.
- \+ list.member(C, ParentConstraints),
-
- C = constraint(SuperClassName, SuperClassTypes),
- list.length(SuperClassTypes, SuperClassArity),
- SuperClassId = class_id(SuperClassName, SuperClassArity),
- multi_map.search(SuperClassTable, SuperClassId, SubClasses),
-
- % Convert all the subclass_details into prog_constraints by doing the
- % appropriate variable renaming and applying the type variable bindings.
- % If the unification of the type variables for a particular constraint
- % fails then that constraint is eliminated because it cannot contribute
- % to proving the constraint we are trying to prove.
- list.filter_map(
- subclass_details_to_constraint(TVarSet, KindMap, SuperClassTypes),
- SubClasses, SubClassConstraints),
- (
- % Do the first level of search. We search for an assumed constraint
- % which unifies with any of the subclass constraints.
- varset.vars(TVarSet, XXXHeadTypeParams),
- list.find_first_map(
- match_assumed_constraint(XXXHeadTypeParams, SubClassConstraints),
- AssumedConstraints, SubClass - SubClassSubst0)
- ->
- SubClassSubst = SubClassSubst0,
- apply_rec_subst_to_prog_constraint(SubClassSubst, C, SubstC),
- map.set(Proofs0, SubstC, superclass(SubClass), Proofs)
- ;
- NewParentConstraints = [C | ParentConstraints],
-
- % Recursively search the rest of the superclass relation.
- SubClassSearch = (pred(Constraint::in, CnstrtAndProof::out)
- is semidet :-
- eliminate_constraint_by_class_rules(Constraint,
- SubstConstraint, SubClassSubst0,
- AssumedConstraints, SuperClassTable,
- HeadTypeParams, TVarSet, KindMap,
- NewParentConstraints, Proofs0, SubProofs),
- CnstrtAndProof = {SubstConstraint, SubClassSubst0, SubProofs}
- ),
- % XXX this could (and should) be more efficient.
- % (i.e. by manually doing a "cut").
- find_first_map(SubClassSearch, SubClassConstraints,
- {NewSubClass, SubClassSubst, NewProofs}),
- apply_rec_subst_to_prog_constraint(SubClassSubst, C, SubstC),
- map.set(NewProofs, SubstC, superclass(NewSubClass), Proofs)
- ).
+:- pred add_superclass_proofs(prog_constraint::in, list(prog_constraint)::in,
+ constraint_proof_map::in, constraint_proof_map::out) is det.
-:- pred match_assumed_constraint(head_type_params::in,
- list(prog_constraint)::in, hlds_constraint::in,
- pair(prog_constraint, tsubst)::out) is semidet.
-
-match_assumed_constraint(HeadTypeParams, SubClassConstraints,
- AssumedConstraint, Match) :-
- find_first_map(
- match_assumed_constraint_2(HeadTypeParams, AssumedConstraint),
- SubClassConstraints, Match).
-
-:- pred match_assumed_constraint_2(head_type_params::in, hlds_constraint::in,
- prog_constraint::in, pair(prog_constraint, tsubst)::out) is semidet.
-
-match_assumed_constraint_2(HeadTypeParams, AssumedConstraint,
- SubClassConstraint, Match) :-
- AssumedConstraint = constraint(_, AssumedConstraintClass,
- AssumedConstraintTypes),
- SubClassConstraint = constraint(AssumedConstraintClass,
- SubClassConstraintTypes),
- map.init(EmptySub),
- type_unify_list(SubClassConstraintTypes, AssumedConstraintTypes,
- HeadTypeParams, EmptySub, AssumedConstraintSub),
- retrieve_prog_constraint(AssumedConstraint, MatchingProgConstraint),
- Match = MatchingProgConstraint - AssumedConstraintSub.
-
- % subclass_details_to_constraint will fail iff the call to
- % type_unify_list fails.
- %
-:- pred subclass_details_to_constraint(tvarset::in, tvar_kind_map::in,
- list(mer_type)::in, subclass_details::in, prog_constraint::out) is semidet.
-
-subclass_details_to_constraint(TVarSet, KindMap0, SuperClassTypes,
- SubClassDetails, SubC) :-
- SubClassDetails = subclass_details(SuperVars0, SubID, SubVars0,
- SuperVarSet),
-
- % Rename the variables from the typeclass declaration into those
- % of the current pred.
- tvarset_merge_renaming(TVarSet, SuperVarSet, _NewTVarSet, Renaming),
- apply_variable_renaming_to_tvar_kind_map(Renaming, KindMap0, KindMap),
- apply_variable_renaming_to_tvar_list(Renaming, SubVars0, SubVars),
- apply_variable_renaming_to_type_list(Renaming, SuperVars0, SuperVars),
-
- % Work out what the (renamed) vars from the typeclass declaration
- % are bound to here.
- type_unify_list(SuperVars, SuperClassTypes, [], map.init, Bindings),
- SubID = class_id(SubName, _SubArity),
- apply_rec_subst_to_tvar_list(KindMap, Bindings, SubVars,
- SubClassTypes),
- SubC = constraint(SubName, SubClassTypes).
+add_superclass_proofs(_, [], !Proofs).
+add_superclass_proofs(Constraint, [Descendant | Descendants], !Proofs) :-
+ svmap.set(Constraint, superclass(Descendant), !Proofs),
+ add_superclass_proofs(Descendant, Descendants, !Proofs).
% check_satisfiability(Constraints, HeadTypeParams):
%
Index: tests/valid/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/valid/Mmakefile,v
retrieving revision 1.180
diff -u -r1.180 Mmakefile
--- tests/valid/Mmakefile 9 Oct 2006 06:40:28 -0000 1.180
+++ tests/valid/Mmakefile 21 Oct 2006 18:40:01 -0000
@@ -36,6 +36,7 @@
mpj6 \
mpj7 \
repeated_class_constraint \
+ superclass_bug \
superclass_improvement \
typeclass_constraint_no_var \
typeclass_constraint_nonvar_bug \
Index: tests/valid/superclass_bug.m
===================================================================
RCS file: tests/valid/superclass_bug.m
diff -N tests/valid/superclass_bug.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ tests/valid/superclass_bug.m 21 Oct 2006 18:39:41 -0000
@@ -0,0 +1,38 @@
+:- module superclass_bug.
+:- interface.
+
+:- type s ---> s.
+:- type e ---> e.
+:- type c ---> c.
+
+:- typeclass my_stream(Stream, State) <= (Stream -> State) where
+[
+ pred name(Stream::in, string::out, State::di, State::uo) is det
+].
+
+:- typeclass my_god(Stream, State, Error)
+ <= ( my_stream(Stream, State), (Stream -> Error) ) where [].
+
+:- typeclass my_input(Stream, Unit, State, Error)
+ <= my_god(Stream, State, Error) where [].
+
+:- type tab_expander(S).
+
+:- instance my_stream(tab_expander(S), s)
+ <= my_input(S, c, s, e).
+
+:- implementation.
+
+:- type tab_expander(S)
+ ---> tab_expander(int, S).
+
+:- instance my_stream(tab_expander(S), s)
+ <= my_input(S, c, s, e) where
+[
+ pred(name/4) is foo
+].
+
+:- pred foo(tab_expander(S)::in, string::out, s::di, s::uo) is det
+ <= my_input(S, c, s, e).
+foo(tab_expander(_, Stream), Name, !S) :-
+ name(Stream, Name, !S).
--------------------------------------------------------------------------
mercury-reviews mailing list
Post messages to: mercury-reviews at csse.unimelb.edu.au
Administrative Queries: owner-mercury-reviews at csse.unimelb.edu.au
Subscriptions: mercury-reviews-request at csse.unimelb.edu.au
--------------------------------------------------------------------------
More information about the reviews
mailing list