[m-rev.] for review: fix bug #15

[Julien Fischer]

For review by anyone.

Address bug #15.  In the current implementation if you have

    ( if some [V] C then T else E )

then V will be quantified over both C and T.  This was not
documented anywhere.  The fix is to document it.

(There has been some discussion in the notes for bug #15 about
adding new syntax to explicitly support the situation where you
want to quantify over both the condition and then branch of
and if-then-else.  The situation occurs so rarely that it's
probably not worth it - also, the current proposals don't work
with the ( C -> T ; E ) syntax for if-then-elses.)

doc/reference_manual.texi:
 	Document that the scope of an existential quantification that
 	occurs as the top-level goal of the condition of an if-then-else
 	extends over the then branch.

 	Add a couple of illustrative examples involving existential
 	quantifications in if-then-else conditions.

doc/faq.texi:
 	Delete part of an answer that is causing confusion.
 	This doesn't have any impact on the rest of the answer and avoids
 	the potential confusion.

Julien.

Index: doc/faq.texi
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/doc/faq.texi,v
retrieving revision 1.38
diff -u -r1.38 faq.texi
--- doc/faq.texi	25 Aug 2009 23:54:02 -0000	1.38
+++ doc/faq.texi	9 Dec 2009 00:02:52 -0000
@@ -217,21 +217,6 @@

  @example
  lookup(Map, Key, Value) :-
-        (if some [Value1]
-                map.search(Map, Key, Value1)
-        then
-                Value = Value1
-        else 
-                Value = -1
-        ).
- at end example
-
- at noindent
-The explicit existential quantifier is optional; if you
-prefer a slightly more succinct style you can write this as
-
- at example
-lookup(Map, Key, Value) :-
          ( map.search(Map, Key, Value1) ->
                  Value = Value1
          ;
Index: doc/reference_manual.texi
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/doc/reference_manual.texi,v
retrieving revision 1.435
diff -u -r1.435 reference_manual.texi
--- doc/reference_manual.texi	3 Dec 2009 06:41:38 -0000	1.435
+++ doc/reference_manual.texi	9 Dec 2009 00:16:55 -0000
@@ -722,6 +722,28 @@
  nondeterministic --- unlike Prolog, Mercury's if-then-else does not commit
  to the first solution of the condition if the condition succeeds.

+If @var{CondGoal} is an explicit existential quantification, 
+ at code{some @var{Vars} @var{QuantifiedCondGoal}}, then the variables
+ at var{Vars} are existentially quantified over the conjunction of the goals
+ at var{QuantifiedCondGoal} and @var{ThenGoal}.
+Explicit existential quantifications that occur as subgoals of @var{CondGoal}
+do @emph{not} affect the scope of variables in the ``then'' part.
+For example, in
+ at example
+   ( if some [V] @var{C} then @var{T} else @var{E} )
+ at end example
+ at noindent
+the variable @var{V} is quantified over the conjunction of the goals
+ at var{C} and @var{T} because the top-level goal of the condition is
+an explicit existential quantification, but in 
+ at example
+   ( if true, some [V] @var{C} then @var{T} else @var{E} )
+ at end example
+ at noindent
+the variable @var{V} is only quantified over @var{C}
+because the top-level goal of the condition is not an explicit
+existential quantification.
+
  @item @code{@var{Term1} = @var{Term2}}
  A unification.
  @var{Term1} and @var{Term2} must be valid data-terms.

--------------------------------------------------------------------------
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
--------------------------------------------------------------------------