[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