0000191: indirect instance implementations ignore special insts

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Tags

No tags attached.

Attached Files

instbug.m (507 bytes) 2011-03-22 13:52

inst_match.patch (526 bytes) 2011-04-05 12:21

--- compiler/inst_match.m~	2011-04-04 22:03:49.489592747 -0400
+++ compiler/inst_match.m	2011-04-04 22:03:49.489592747 -0400
@@ -1048,7 +1048,7 @@
         % We can only do this check if the type is known.
         bound_inst_list_is_complete_for_type(set.init, ModuleInfo, ListB, Type)
     ;
-        true
+        MaybeType = no
         % XXX enabling the check for bound_inst_list_is_complete
         % for type makes the mode checker too conservative in
         % the absence of alias tracking, so we currently always

inst_match.patch (526 bytes) 2011-04-05 12:21

inst_match2.patch (14,424 bytes) 2011-04-07 13:37

--- compiler/inst_match.m~	2011-04-04 22:03:49.489592747 -0400
+++ compiler/inst_match.m	2011-04-04 22:03:49.489592747 -0400
@@ -1048,7 +1048,7 @@
         % We can only do this check if the type is known.
         bound_inst_list_is_complete_for_type(set.init, ModuleInfo, ListB, Type)
     ;
-        true
+        MaybeType = no
         % XXX enabling the check for bound_inst_list_is_complete
         % for type makes the mode checker too conservative in
         % the absence of alias tracking, so we currently always
--- library/builtin.m~	2011-04-06 21:55:19.844856577 -0400
+++ library/builtin.m	2011-04-06 22:16:34.098488142 -0400
@@ -388,7 +388,7 @@
     %
 :- pred cc_multi_equal(T, T).
 :- mode cc_multi_equal(di, uo) is cc_multi.
-:- mode cc_multi_equal(in, out) is cc_multi.
+:- mode cc_multi_equal(in(I =< ground), out(I =< ground)) is cc_multi.
 
     % `impure_true' is like `true' except that it is impure.
     %
@@ -1184,7 +1184,7 @@
 % Any changes here may need to be reflected there.
 
 :- pragma foreign_proc("C",
-    cc_multi_equal(X::in, Y::out),
+    cc_multi_equal(X::in(I =< ground), Y::out(I =< ground)),
     [will_not_call_mercury, thread_safe, promise_pure,
         does_not_affect_liveness],
 "
@@ -1199,7 +1199,7 @@
 ").
 
 :- pragma foreign_proc("C#",
-    cc_multi_equal(X::in, Y::out),
+    cc_multi_equal(X::in(I =< ground), Y::out(I =< ground)),
     [will_not_call_mercury, thread_safe, promise_pure],
 "
     Y = X;
@@ -1212,7 +1212,7 @@
 ").
 
 :- pragma foreign_proc("Java",
-    cc_multi_equal(X::in, Y::out),
+    cc_multi_equal(X::in(I =< ground), Y::out(I =< ground)),
     [will_not_call_mercury, thread_safe, promise_pure],
 "
     Y = X;
@@ -1225,7 +1225,7 @@
 ").
 
 :- pragma foreign_proc("Erlang",
-    cc_multi_equal(X::in, Y::out),
+    cc_multi_equal(X::in(I =< ground), Y::out(I =< ground)),
     [will_not_call_mercury, thread_safe, promise_pure],
 "
     Y = X
--- library/exception.m~	2011-04-06 22:07:33.804376595 -0400
+++ library/exception.m	2011-04-06 23:16:13.911887652 -0400
@@ -350,34 +350,39 @@
 :- pragma no_inline(get_determinism/2).
 :- pragma promise_equivalent_clauses(get_determinism/2).
 
+% Trick Mercury into using the correct mode.
+% The real fix is to make check_hlds.modecheck_call.choose_best_match nondet.
+:- pred ccme(A::in(I =< ground), A::out(I =< ground)) is cc_multi.
+ccme(A, B) :- cc_multi_equal(A, B).
+
 get_determinism(_Pred::(pred(out) is det),
         Det::out(bound(exp_detism_det))) :-
-    ( cc_multi_equal(exp_detism_det, Det)
+    ( ccme(exp_detism_det, Det)
     ; throw(software_error("get_determinism"))
     ).
 get_determinism(_Pred::(pred(out) is semidet),
         Det::out(bound(exp_detism_semidet))) :-
-    ( cc_multi_equal(exp_detism_semidet, Det)
+    ( ccme(exp_detism_semidet, Det)
     ; throw(software_error("get_determinism"))
     ).
 get_determinism(_Pred::(pred(out) is cc_multi),
         Det::out(bound(exp_detism_cc_multi))) :-
-    ( cc_multi_equal(exp_detism_cc_multi, Det)
+    ( ccme(exp_detism_cc_multi, Det)
     ; throw(software_error("get_determinism"))
     ).
 get_determinism(_Pred::(pred(out) is cc_nondet),
         Det::out(bound(exp_detism_cc_nondet))) :-
-    ( cc_multi_equal(exp_detism_cc_nondet, Det)
+    ( ccme(exp_detism_cc_nondet, Det)
     ; throw(software_error("get_determinism"))
     ).
 get_determinism(_Pred::(pred(out) is multi),
         Det::out(bound(exp_detism_multi))) :-
-    ( cc_multi_equal(exp_detism_multi, Det)
+    ( ccme(exp_detism_multi, Det)
     ; throw(software_error("get_determinism"))
     ).
 get_determinism(_Pred::(pred(out) is nondet),
         Det::out(bound(exp_detism_nondet))) :-
-    ( cc_multi_equal(exp_detism_nondet, Det)
+    ( ccme(exp_detism_nondet, Det)
     ; throw(software_error("get_determinism"))
     ).
 
@@ -386,12 +391,12 @@
 
 get_determinism_2(_Pred::pred(out, di, uo) is det,
         Det::out(bound(exp_detism_det))) :-
-    ( cc_multi_equal(exp_detism_det, Det)
+    ( ccme(exp_detism_det, Det)
     ; throw(software_error("get_determinism_2"))
     ).
 get_determinism_2(_Pred::pred(out, di, uo) is cc_multi,
         Det::out(bound(exp_detism_cc_multi))) :-
-    ( cc_multi_equal(exp_detism_cc_multi, Det)
+    ( ccme(exp_detism_cc_multi, Det)
     ; throw(software_error("get_determinism_2"))
     ).
 
@@ -492,14 +497,23 @@
 wrap_success(Goal, succeeded(R)) :- Goal(R).
 
 :- pred wrap_success_or_failure(pred(T), exception_result(T)) is det.
-:- mode wrap_success_or_failure(pred(out) is det, out) is det.
+:- mode wrap_success_or_failure(pred(out) is det, out(cannot_fail)) is det.
 :- mode wrap_success_or_failure(pred(out) is semidet, out) is det.
 %:- mode wrap_success_or_failure(pred(out) is multi, out) is multi. (unused)
 %:- mode wrap_success_or_failure(pred(out) is nondet, out) is multi. (unused)
-:- mode wrap_success_or_failure(pred(out) is cc_multi, out) is cc_multi.
+:- mode wrap_success_or_failure(pred(out) is cc_multi, out(cannot_fail)) is cc_multi.
 :- mode wrap_success_or_failure(pred(out) is cc_nondet, out) is cc_multi.
+:- pragma promise_equivalent_clauses(wrap_success_or_failure/2).
 
-wrap_success_or_failure(Goal, Result) :-
+% We need multiple clauses because Mercury seems to decide the
+% inst of Result before pruning the else branch.
+wrap_success_or_failure(Goal::pred(out) is det, Result::out(cannot_fail)) :-
+    Goal(R), Result = succeeded(R).
+wrap_success_or_failure(Goal::pred(out) is semidet, Result::out) :-
+    (if Goal(R) then Result = succeeded(R) else Result = failed).
+wrap_success_or_failure(Goal::pred(out) is cc_multi, Result::out(cannot_fail)) :-
+    Goal(R), Result = succeeded(R).
+wrap_success_or_failure(Goal::pred(out) is cc_nondet, Result::out) :-
     (if Goal(R) then Result = succeeded(R) else Result = failed).
 
 /*********************
@@ -518,19 +532,19 @@
     try_det(Detism, Goal, Result).
 
 try_det(exp_detism_det, Goal, Result) :-
-    WrappedGoal = (pred(R::out) is det :-
+    WrappedGoal = (pred(R::out(cannot_fail)) is det :-
         wrap_success_or_failure(Goal, R)
     ),
     catch_impl(WrappedGoal, wrap_exception, Result0),
-    cc_multi_equal(Result0, Result).
+    ccme(Result0, Result).
 try_det(exp_detism_semidet, Goal, Result) :-
     WrappedGoal = (pred(R::out) is det :-
         wrap_success_or_failure(Goal, R)
     ),
     catch_impl(WrappedGoal, wrap_exception, Result0),
-    cc_multi_equal(Result0, Result).
+    ccme(Result0, Result).
 try_det(exp_detism_cc_multi, Goal, Result) :-
-    WrappedGoal = (pred(R::out) is cc_multi :-
+    WrappedGoal = (pred(R::out(cannot_fail)) is cc_multi :-
         wrap_success_or_failure(Goal, R)
     ),
     catch_impl(WrappedGoal, wrap_exception, Result).
@@ -832,12 +846,18 @@
 :- pragma promise_pure(catch_impl/3).
 :- /* impure */
    pred catch_impl(pred(T), handler(T), T).
-:- mode catch_impl(pred(out) is det,       in(handler), out) is det.
-:- mode catch_impl(pred(out) is semidet,   in(handler), out) is semidet.
-:- mode catch_impl(pred(out) is cc_multi,  in(handler), out) is cc_multi.
-:- mode catch_impl(pred(out) is cc_nondet, in(handler), out) is cc_nondet.
-:- mode catch_impl(pred(out) is multi,     in(handler), out) is multi.
-:- mode catch_impl(pred(out) is nondet,    in(handler), out) is nondet.
+:- mode catch_impl(pred(out(I =< ground)) is det,       in(handler),
+    out(I =< ground)) is det.
+:- mode catch_impl(pred(out(I =< ground)) is semidet,   in(handler),
+    out(I =< ground)) is semidet.
+:- mode catch_impl(pred(out(I =< ground)) is cc_multi,  in(handler),
+    out(I =< ground)) is cc_multi.
+:- mode catch_impl(pred(out(I =< ground)) is cc_nondet, in(handler),
+    out(I =< ground)) is cc_nondet.
+:- mode catch_impl(pred(out(I =< ground)) is multi,     in(handler),
+    out(I =< ground)) is multi.
+:- mode catch_impl(pred(out(I =< ground)) is nondet,    in(handler),
+    out(I =< ground)) is nondet.
 
 %
 % By default we call the external implementation, but specific backends
@@ -852,17 +872,23 @@
 throw_impl(Univ::in) :-
     builtin_throw(Univ).
 
-catch_impl(Pred::(pred(out) is det), Handler::in(handler), T::out) :-
+catch_impl(Pred::(pred(out(I =< ground)) is det), Handler::in(handler),
+           T::out(I =< ground)) :-
     builtin_catch(Pred, Handler, T).
-catch_impl(Pred::(pred(out) is semidet), Handler::in(handler), T::out) :-
+catch_impl(Pred::(pred(out(I =< ground)) is semidet), Handler::in(handler),
+           T::out(I =< ground)) :-
     builtin_catch(Pred, Handler, T).
-catch_impl(Pred::(pred(out) is cc_multi), Handler::in(handler), T::out) :-
+catch_impl(Pred::(pred(out(I =< ground)) is cc_multi), Handler::in(handler),
+           T::out(I =< ground)) :-
     builtin_catch(Pred, Handler, T).
-catch_impl(Pred::(pred(out) is cc_nondet), Handler::in(handler), T::out) :-
+catch_impl(Pred::(pred(out(I =< ground)) is cc_nondet), Handler::in(handler),
+           T::out(I =< ground)) :-
     builtin_catch(Pred, Handler, T).
-catch_impl(Pred::(pred(out) is multi), Handler::in(handler), T::out) :-
+catch_impl(Pred::(pred(out(I =< ground)) is multi), Handler::in(handler),
+           T::out(I =< ground)) :-
     builtin_catch(Pred, Handler, T).
-catch_impl(Pred::(pred(out) is nondet), Handler::in(handler), T::out) :-
+catch_impl(Pred::(pred(out(I =< ground)) is nondet), Handler::in(handler),
+           T::out(I =< ground)) :-
     builtin_catch(Pred, Handler, T).
 
 % builtin_throw and builtin_catch are implemented below using
@@ -873,12 +899,18 @@
 
 :- /* impure */
    pred builtin_catch(pred(T), handler(T), T).
-:- mode builtin_catch(pred(out) is det, in(handler), out) is det.
-:- mode builtin_catch(pred(out) is semidet, in(handler), out) is semidet.
-:- mode builtin_catch(pred(out) is cc_multi, in(handler), out) is cc_multi.
-:- mode builtin_catch(pred(out) is cc_nondet, in(handler), out) is cc_nondet.
-:- mode builtin_catch(pred(out) is multi, in(handler), out) is multi.
-:- mode builtin_catch(pred(out) is nondet, in(handler), out) is nondet.
+:- mode builtin_catch(pred(out(I =< ground)) is det, in(handler),
+    out(I =< ground)) is det.
+:- mode builtin_catch(pred(out(I =< ground)) is semidet, in(handler),
+    out(I =< ground)) is semidet.
+:- mode builtin_catch(pred(out(I =< ground)) is cc_multi, in(handler),
+    out(I =< ground)) is cc_multi.
+:- mode builtin_catch(pred(out(I =< ground)) is cc_nondet, in(handler),
+    out(I =< ground)) is cc_nondet.
+:- mode builtin_catch(pred(out(I =< ground)) is multi, in(handler),
+    out(I =< ground)) is multi.
+:- mode builtin_catch(pred(out(I =< ground)) is nondet, in(handler),
+    out(I =< ground)) is nondet.
 
 %
 % IMPORTANT: any changes or additions to external predicates should be
--- library/list.m~	2011-04-06 22:38:34.127522212 -0400
+++ library/list.m	2011-04-06 22:40:37.672093399 -0400
@@ -126,8 +126,10 @@
     % and eliminating any duplicates. L1 and L2 must be sorted and must each
     % not contain any duplicates.
     %
-:- pred list.merge_and_remove_dups(list(T)::in, list(T)::in, list(T)::out)
-    is det.
+:- pred list.merge_and_remove_dups(list(T), list(T), list(T)) is det.
+:- mode list.merge_and_remove_dups(in, in, out) is det.
+:- mode list.merge_and_remove_dups(in(non_empty_list), in, out(non_empty_list)) is det.
+:- mode list.merge_and_remove_dups(in, in(non_empty_list), out(non_empty_list)) is det.
 :- func list.merge_and_remove_dups(list(T), list(T)) = list(T).
 
     % list.remove_adjacent_dups(L0, L):
@@ -343,7 +345,10 @@
     % List is List0 sorted with the second and subsequent occurrence of
     % any duplicates removed.
     %
-:- pred list.sort_and_remove_dups(list(T)::in, list(T)::out) is det.
+:- pred list.sort_and_remove_dups(list(T), list(T)) is det.
+:- mode list.sort_and_remove_dups(in, out) is det.
+:- mode list.sort_and_remove_dups(in(non_empty_list), out(non_empty_list))
+    is det.
 :- func list.sort_and_remove_dups(list(T)) = list(T).
 
     % list.sort(List0, List):
@@ -1891,17 +1896,18 @@
 
 %-----------------------------------------------------------------------------%
 
-:- pred list.merge_sort_and_remove_dups_2(int::in, list(T)::in, list(T)::out)
-    is det.
+:- pred list.merge_sort_and_remove_dups_2(int, list(T), list(T)).
+:- mode list.merge_sort_and_remove_dups_2(in, in, out) is det.
+:- mode list.merge_sort_and_remove_dups_2(in, in(non_empty_list), out(non_empty_list)) is det.
 :- pragma type_spec(list.merge_sort_and_remove_dups_2(in, in, out),
     T = var(_)).
 
 list.merge_sort_and_remove_dups_2(Length, List, SortedList) :-
-    ( Length > 1 ->
+    ( List = [A, B | Rest] ->
         HalfLength = Length // 2,
-        ( list.split_list(HalfLength, List, Front, Back) ->
+        ( list.split_list(HalfLength - 2, Rest, Front, Back) ->
             list.merge_sort_and_remove_dups_2(HalfLength,
-                Front, SortedFront),
+                [A, B | Front], SortedFront),
             list.merge_sort_and_remove_dups_2(Length - HalfLength,
                 Back, SortedBack),
             list.merge_and_remove_dups(SortedFront, SortedBack, SortedList)
--- library/solutions.m~	2011-04-06 22:26:52.724677229 -0400
+++ library/solutions.m	2011-04-06 22:27:35.684254515 -0400
@@ -196,7 +196,7 @@
 
 :- implementation.
 
-:- import_module mutvar.
+:- import_module exception, mutvar.
 
 %-----------------------------------------------------------------------------%
 
@@ -248,10 +248,19 @@
 %-----------------------------------------------------------------------------%
 
 :- pred builtin_solutions(pred(T), list(T)).
-:- mode builtin_solutions(pred(out) is multi, out) is det.  % really cc_multi
+:- mode builtin_solutions(pred(out) is multi, out(non_empty_list)) is det.  % really cc_multi
 :- mode builtin_solutions(pred(out) is nondet, out) is det. % really cc_multi
+:- pragma promise_equivalent_clauses(builtin_solutions/2).
 
-builtin_solutions(Generator, UnsortedList) :-
+builtin_solutions(Generator::pred(out) is multi, UnsortedList::out(non_empty_list)) :-
+    builtin_aggregate(Generator, list.cons, [], UnsortedList0),
+    (
+        UnsortedList0 = [_|_], UnsortedList = UnsortedList0
+    ;
+        UnsortedList0 = [], throw(software_error("builtin_solutions"))
+    ).
+
+builtin_solutions(Generator::pred(out) is nondet, UnsortedList::out) :-
     builtin_aggregate(Generator, list.cons, [], UnsortedList).
 
 %-----------------------------------------------------------------------------%

inst_match2.patch (14,424 bytes) 2011-04-07 13:37

Relationships

Relationships

Notes
~0000321 colanderman (reporter) 2011-03-22 14:18 Last edited: 2011-03-22 14:25	This seems to be part of a more general problem of complex insts not being propagated through predicate calls. Am I misunderstanding the semantics of the language? Edit: seems to be related to bugs # 86 and 117.

~0000322 colanderman (reporter) 2011-04-05 12:22	Squashed it, was a one-line fix in compiler/inst_match.m. Also fixes bugs 86 and 117. See attached patch.

~0000323 juliensf (administrator) 2011-04-07 03:22	The above patch breaks compilation of the stage 2 standard library. (That doesn't necessarily mean it is incorrect, since at least some the library code that breaks looks suspicious -- we will need to look into this further before applying the above patch.)

~0000326 colanderman (reporter) 2011-04-07 13:41	That's what I get for being sneaky and skipping the install phase :) Attached is a (much larger) patch that fixes most of the library issues. It involved some mode additions to the list module (there really should be lots more), generalizing the mode of cc_multi_equal, and specializing cc_multi_equal in exception.m (this is due to the fact that the compiler chooses the di/uo mode of cc_multi_equal as "best" and doesn't try the other mode when it fails). term_to_xml.m still doesn't compile, and I believe it is due to a possible bug I mentioned on the users mailing list, concerning predicates which refine nested insts. The error I'm getting is: term_to_xml.m:1348: In clause for `'__Unify__'(in, (unique(list.'[\|]'(free, term_to_xml.m:1348: unique((list.[])))) >> bound(list.'[\|]'(ground, term_to_xml.m:1348: bound((list.[]))))), (ground >> bound(list.'[\|]'(ground, term_to_xml.m:1348: bound((list.[]))))))': term_to_xml.m:1348: mode error: argument 3 did not get sufficiently term_to_xml.m:1348: instantiated. term_to_xml.m:1348: Final instantiatedness of `HeadVar__2' was term_to_xml.m:1348: `bound(list.'[\|]'(ground, ground))', term_to_xml.m:1348: expected final instantiatedness was term_to_xml.m:1348: `bound(list.'[\|]'(ground, bound((list.[]))))'. which looks suspiciously similar to the issue I mentioned. I will focus my efforts on trying to track down that bug, and will hope that it's as simple as this one was to fix.

~0000859 juliensf (administrator) 2015-11-02 11:10	This was fixed in commit 491bb0a.

Notes

Date Modified	Username	Field	Change
Issue History
2011-03-22 13:52	colanderman	New Issue
2011-03-22 13:52	colanderman	File Added: instbug.m
2011-03-22 14:18	colanderman	Note Added: 0000321
2011-03-22 14:25	colanderman	Note Edited: 0000321
2011-04-05 12:21	colanderman	File Added: inst_match.patch
2011-04-05 12:22	colanderman	Note Added: 0000322
2011-04-07 03:22	juliensf	Note Added: 0000323
2011-04-07 13:37	colanderman	File Added: inst_match2.patch
2011-04-07 13:41	colanderman	Note Added: 0000326
2015-11-02 11:10	juliensf	Note Added: 0000859
2015-11-02 11:10	juliensf	Status	new => resolved
2015-11-02 11:10	juliensf	Resolution	open => fixed
2015-11-02 11:10	juliensf	Assigned To	=> juliensf

Issue History