mirror of
https://github.com/Mercury-Language/mercury.git
synced 2026-04-20 11:54:02 +00:00
d551dd1dc9
Estimated hours taken: 10
Handle quantification analysis of bi-implication (`<=>') goals correctly.
Previously we used to expand bi-implications before doing quantification
analysis, which stuffed up the results of quantification analysis for
those goals. We need to do quantification analysis first, and only
then can we expand bi-implications. In addition, elimination of double
negation needs to come after expansion of bi-implication, so I moved
that from make_hlds.m to purity.m.
compiler/hlds_goal.m:
Add a new alternative to the HLDS goal type for bi-implications.
Also add a new predicate negate_goal, for use by purity.m.
compiler/make_hlds.m:
Don't expand bi-implication here, instead just use the new
bi_implication/2 HLDS goal type.
Don't eliminated double negation here.
compiler/quantification.m:
Handle quantification for bi-implications.
Expand bi-implications.
compiler/purity.m:
Eliminate double negation.
compiler/hlds_out.m:
Add code to print out bi-implication goals.
compiler/*.m:
Trivial changes to handle the new bi_implication/2
alternative in the HLDS goal type.
compiler/notes/compiler_design.html:
Document the above changes.
tests/hard_coded/Mmakefile:
tests/hard_coded/quantifier2.m:
tests/hard_coded/quantifier2.exp:
A regression test for the above change.
38 lines
604 B
Mathematica
38 lines
604 B
Mathematica
:- module quantifier2.
|
|
|
|
:- interface.
|
|
|
|
:- import_module io.
|
|
|
|
:- pred main(io__state::di,io__state::uo) is det.
|
|
|
|
:- implementation.
|
|
|
|
:- import_module list, int.
|
|
|
|
:- pred testsum(list(int),int,int).
|
|
:- mode testsum(in,in,out) is semidet.
|
|
|
|
testsum([],I,0) :- I > 0.
|
|
testsum([X|L],I,X + N1) :- testsum(L,I,N1).
|
|
|
|
|
|
:- pred foo(pred(int, int)).
|
|
:- mode foo(free->pred(in, out) is semidet) is det.
|
|
|
|
foo(testsum([1,2,3])).
|
|
|
|
|
|
main -->
|
|
(
|
|
{ P = lambda([I :: in, X :: out] is semidet, (I > 0, X = 6)),
|
|
foo(Q),
|
|
J = 1,
|
|
(call(P,J,_X) <=> call(Q,J,_Y)) }
|
|
->
|
|
print("yes"), nl
|
|
;
|
|
print("no"), nl
|
|
).
|
|
|