[m-rev.] for review: check instance declarations

[Peter Ross]

Hi,

My last review was incorrect.
It didn't correctly identify which instance declartions were about
the same types.
Also there already existed some code which checked whether two
constraint lists were equivalent.  We call this code instead.



===================================================================


Estimated hours taken: 2
Branches: main

The following code causes code to be generated which seg-faults

 :- interface
 :- instance tc(list(T)).
 :- implementation.
 :- instance tc(list(T)) <= tc(T) where [...].

because the exported instance declaration doesn't contain the
typeclass constraint.

mercury/compiler/add_class.m:
       Check that for all the "same" instance declarations
       the instance constraints are exactly the same on each
       declaration.
	
tests/invalid/Mmakefile:
	Add tests for this code.


Index: mercury/compiler/add_class.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/add_class.m,v
retrieving revision 1.27
diff -u -r1.27 add_class.m
--- mercury/compiler/add_class.m	17 May 2007 03:52:38 -0000	1.27
+++ mercury/compiler/add_class.m	21 May 2007 00:38:25 -0000
@@ -108,7 +108,8 @@
             ClassInterface = Interface
         ),
         (
-            \+ superclass_constraints_are_identical(OldVars, OldVarSet,
+            % Check that the superclass constraints are identical
+            \+ constraints_are_identical(OldVars, OldVarSet,
                 OldConstraints, Vars, VarSet, Constraints)
         ->
             % Always report the error, even in `.opt' files.
@@ -218,11 +219,11 @@
         get_list_index(Es, N + 1, X)
     ).
 
-:- pred superclass_constraints_are_identical(list(tvar)::in, tvarset::in,
+:- pred constraints_are_identical(list(tvar)::in, tvarset::in,
     list(prog_constraint)::in, list(tvar)::in, tvarset::in,
     list(prog_constraint)::in) is semidet.
 
-superclass_constraints_are_identical(OldVars0, OldVarSet, OldConstraints0,
+constraints_are_identical(OldVars0, OldVarSet, OldConstraints0,
         Vars, VarSet, Constraints) :-
     tvarset_merge_renaming(VarSet, OldVarSet, _, Renaming),
     apply_variable_renaming_to_prog_constraint_list(Renaming, OldConstraints0,
@@ -461,8 +462,11 @@
         NewInstanceDefn = hlds_instance_defn(InstanceModuleName, Status,
             Context, Constraints, Types, Body, no, VarSet, Empty),
         map.lookup(Instances0, ClassId, InstanceDefns),
+
         check_for_overlapping_instances(NewInstanceDefn, InstanceDefns,
             ClassId, !Specs),
+        check_instance_compatibility(NewInstanceDefn, InstanceDefns, !Specs),
+
         map.det_update(Instances0, ClassId,
             [NewInstanceDefn | InstanceDefns], Instances),
         module_info_set_instance_table(Instances, !ModuleInfo)
@@ -509,6 +513,89 @@
     Spec = error_spec(severity_error, phase_parse_tree_to_hlds, [Msg1, Msg2]),
     !:Specs = [Spec | !.Specs].
 
+
+    %
+    % If two instance declarations are about the same type, then
+    % the declarations must be compatible.  This consists of checking
+    % that the constraints are identical.
+    % In other words, the abstract declaration must match the 
+    % concrete definition.
+    %
+:- pred check_instance_compatibility(hlds_instance_defn::in,
+    list(hlds_instance_defn)::in,
+    list(error_spec)::in, list(error_spec)::out) is det.
+
+check_instance_compatibility(InstanceDefn, InstanceDefns, !Specs) :-
+    list.filter(same_type_hlds_instance_defn(InstanceDefn),
+        InstanceDefns, EquivInstanceDefns),
+    list.foldl(check_instance_constraints(InstanceDefn),
+        EquivInstanceDefns, !Specs).
+
+:- pred check_instance_constraints(hlds_instance_defn::in,
+    hlds_instance_defn::in,
+    list(error_spec)::in, list(error_spec)::out) is det.
+
+check_instance_constraints(InstanceDefnA, InstanceDefnB, !Specs) :-
+    type_vars_list(InstanceDefnA ^ instance_types, TVarsA),
+    TVarsetA = InstanceDefnA ^ instance_tvarset,
+    ConstraintsA = InstanceDefnA ^ instance_constraints,
+
+    type_vars_list(InstanceDefnB ^ instance_types, TVarsB),
+    TVarsetB = InstanceDefnB ^ instance_tvarset,
+    ConstraintsB = InstanceDefnB ^ instance_constraints,
+
+    (
+        constraints_are_identical(TVarsA, TVarsetA, ConstraintsA,
+            TVarsB, TVarsetB, ConstraintsB)
+    ->
+        true
+    ;
+        ContextA = InstanceDefnA ^ instance_context, 
+        TxtA = [string_to_words_piece("instance constraints incompatible")],
+        MsgA = simple_msg(ContextA, [always(TxtA)]),
+
+        ContextB = InstanceDefnB ^ instance_context,
+        TxtB = [string_to_words_piece("with instance constraints here.")],
+        MsgB = simple_msg(ContextB, [always(TxtB)]),
+
+        Spec = error_spec(severity_error,
+            phase_parse_tree_to_hlds, [MsgA, MsgB]),
+        !:Specs = [Spec | !.Specs]
+    ).
+
+    %
+    % Do two hlds_instance_defn refer to the same type?
+    % eg "instance tc(f(T))" compares equal to "instance tc(f(U))"
+    % 
+    % Note we don't check that the constraints of the declarations are the
+    % same.
+    %
+:- pred same_type_hlds_instance_defn(hlds_instance_defn::in,
+    hlds_instance_defn::in) is semidet.
+
+same_type_hlds_instance_defn(InstanceDefnA, InstanceDefnB) :-
+    TypesA = InstanceDefnA ^ instance_types,
+    TypesB0 = InstanceDefnB ^ instance_types,
+
+    VarSetA = InstanceDefnA ^ instance_tvarset,
+    VarSetB = InstanceDefnB ^ instance_tvarset,
+
+        % Rename the two lists of types apart.
+    tvarset_merge_renaming(VarSetA, VarSetB, _NewVarSet, RenameApart),
+    apply_variable_renaming_to_type_list(RenameApart, TypesB0, TypesB1),
+
+    type_vars_list(TypesA, TVarsA),
+    type_vars_list(TypesB1, TVarsB),
+
+        % If the lengths are different they can't be the same type.
+    list.length(TVarsA, L),
+    list.length(TVarsB, L),
+
+    map.from_corresponding_lists(TVarsB, TVarsA, Renaming),
+    apply_variable_renaming_to_type_list(Renaming, TypesB1, TypesB),
+
+    TypesA = TypesB.
+    
 do_produce_instance_method_clauses(InstanceProcDefn, PredOrFunc, PredArity,
         ArgTypes, Markers, Context, Status, ClausesInfo, !ModuleInfo,
         !QualInfo, !Specs) :-
Index: tests/invalid/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/invalid/Mmakefile,v
retrieving revision 1.215
diff -u -r1.215 Mmakefile
--- tests/invalid/Mmakefile	17 May 2007 06:15:33 -0000	1.215
+++ tests/invalid/Mmakefile	21 May 2007 00:30:30 -0000
@@ -102,6 +102,7 @@
 	ho_unique_error \
 	illtyped_compare \
 	impure_method_impl \
+	incompatible_instance_constraints \
 	inconsistent_instances \
 	inline_conflict \
 	inst_list_dup \
Index: tests/invalid/incompatible_instance_constraints.m
===================================================================
:- module incompatible_instance_constraints.
:- interface.

:- type t1(T) ---> t1(T).
:- type t2(T) ---> t2(T).
:- type t3(T, U) ---> t3(T, U).
:- type t4(T, U) ---> t4(T, U).

:- typeclass tc1(T) where [].
:- typeclass tc2(T) where [].
:- typeclass tc3(T, U) where [].

    % Missing constraints
:- instance tc1(t1(T)).

    % Constraints in a different order
:- instance tc1(t3(A, B)) <= (tc2(B), tc1(A)).
:- instance tc1(t4(T, U)) <= (tc1(U), tc1(T)).

    % Valid - same order just different type variables
:- instance tc2(t4(A, B)) <= (tc1(A), tc1(B)).

:- implementation.

    % Incompatible abstract definitions
:- instance tc1(t1(T)) <= tc1(T) where [].
:- instance tc1(t3(T, U)) <= (tc1(T), tc2(U)) where [].
:- instance tc1(t4(T, U)) <= (tc1(T), tc1(U)) where [].

    % Compatible abstract definitions
:- instance tc2(t4(T, U)) <= (tc1(T), tc1(U)) where [].

Index: tests/invalid/incompatible_instance_constraints.err
===================================================================
incompatible_instance_constraints.m:025: instance constraints incompatible
incompatible_instance_constraints.m:014:   with instance constraints here.
incompatible_instance_constraints.m:026: instance constraints incompatible
incompatible_instance_constraints.m:017:   with instance constraints here.
incompatible_instance_constraints.m:027: instance constraints incompatible
incompatible_instance_constraints.m:018:   with instance constraints here.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------