(*
 * After going around in circles about whether exists should have its own
 * scope, I've decided that it should.  The long-pondered problem at the root
 * of things here is how to use exists effectively as a choose operator.  The
 * impediment to using the classically defined exists as choose is that the
 * scope of the chosen value is only within the scope of the exists.  This
 * means that an expression of the form:
 *
 *     if (exists (x in l) (x = input))
 *     then output = x
 *     else output = nil
 *
 * does not work because the scope of x is confined to the exists in the if
 * clause, not extending out to the scope of the then clause.  The pure logical
 * solution to this is to use the logical equivalent of if-then-else, as
 * follows:
 *
 *     (exists (x in s) (x = input) and (output = x))
 *         or
 *     (not (exists (x in s) (x = input))) and (output = nil)
 *
 * For me, this looks ugly and non-intuitive compared to the preceding
 * if-then-else form.
 *
 * A direct solution to the scoping problem could be to say simply that
 * quantifiers don't define scopes, so that quantifier variables are bound in
 * the enclosing scope, whatever that might be.  This, however, really opens a
 * can of worms in the area of functional semantics, since we are in effect
 * making quantifiers global binding mechanisms.  On the whole, I now believe
 * it is best to leave this can closed.
 *
 * A bit of further analysis reveals that the problem could be attacked from
 * the perspective of changing the return value of exists from boolean to
 * Object.  In particular, exists would return the value of its variable,
 * instead of true/false. Then we could do the following:
 *
 *     let found = (exists (x in s) (x = input));
 *     if found
 *     then output = found
 *     else output = nil
 *
 * The problem with this is that it disturbs the otherwise normal semantics of
 * exists as a boolean operator.  So, we could invent a choose operator, with
 * the same semantics but a different name, as in
 *
 *     let found = (choose (x in s) (x = input));
 *     if found
 *     then output = found
 *     else output = nil
 *
 * But this doesn't quite work, given the vague semantics of "if found ...".
 * Even if we go with false === nil, this is still doesn't work, I think.
 *
 * So, all we really need (or want) here is this
 *     output = (choose (x in s) (x = input))
 *
 * The deal, seemingly obviously, is that we must be clear that choose returns
 * nil if nothing is found.
 *
 * Given this, the archetypal postcond for a find op can look like this:
 *
 *     op find(name:string, l:Record* ) -> r:Record
 *         post:
 *	       if (exists (r' in l) r'.name = name) then
 *	       r = choose (r' in l) r'.name = name else
 *	       r = nil
 *
 * But heck, isn't this just
 *
 *     op find(name:string, l:Record* ) -> r:Record
 *         post:
 *	       r = choose (r' in l) r'.name = name;
 *
 * Yes, I believe it is.  Now we need to do some more examples with more
 * complicated choose logic, such as finding the first element in a sorted
 * list.
 *
 * I believe there's precedent for this in HOL, which as I recall had such a
 * choose operator.  This choose is also close to exists! (there exists a
 * unique), which we might also choose as a name.  However, I lean against this
 * for a couple reasons: (1) exists! will only work as a choice operator when
 * we are in fact searching for a unique item in a list, which is probably too
 * restrictive for what we want a choose for.  (2) changing the return
 * semantics of exists! is pretty much as problematic as it is for the regular
 * exists, in that the exists! return type really ought to be boolean.
 *
 * So, here's an idea -- we could add both choose and exists!, so the feature
 * creep of choose at least has a bit of company.  In an odd way, this somehow
 * seems less creepy, in that we're not just adding one new operator for one
 * special case.
 *
 * 20nov05 Update: I don't know what planet I was on when I wrote the following
 * 15dec04 note, but it doesn't look like it was earth, and I fell the off
 * anyway.  So f me, very hard.
 *
 * 15dec04 Addition: Also, let's push completely on the normal find logic to
 * fully flesh out the it's and we want and not implication in the exists body.
 *
 *     Here's the "normal" form used to date for "find x in l by ":
 *)


(*
 * OLD CRAP FOLLOWS.
 *)
obj Whatever;
obj ID = integer;
obj X = id:ID and data:Whatever;
obj LX = X*;
op Find(id:ID, xl:XL) -> x':X
    post:
        exists (x in xl) (x.id = id) and (x' = x)
            or
        not (exists (x in xl) (x.id = id)) and (x' = nil)
end Find;

(*
 * But what about the following version using implication?
 *)

op FindV2(id:ID, xl:XL) -> x':X
    post:
        exists (x in xl) if (x.id = id) then (x' = x)
            or
        if not (exists (x in xl) (x.id = id)) then (x' = nil);
end Find;

(*
 * Well, the clause
 *
 *     exists (x in xl) if (x.id = id) then (x' = x)
 *
 * doesn't work because it expands to
 *
 *     exists (x in xl) if (x.id = id) then (x' = x) else true
 *
 * which is true way too much of the time.
 *
 * So what about the following form, which it would seem has eluded us all this
 * time?
 *
 *     exists (x in xl) if (x.id = id) then (x' = x) else x' = nil
 *
 * At least one problem with this is it fails if xl is empty.  So if we guard
 * aginst this, we get this:
 *
 *     if (xl = nil) 
 *     then x' = nil
 *     else exists (x in xl) if (x.id = id) then (x' = x) else x' = nil
 *
 * But what the heck is going on here?  It seems like we don't care what the
 * exists returns, but on the "side effects" on the values of x and x' within
 * the exists body.  Does this work?  Well, let's go back to what the heck a
 * post cond means fundamentally.  Consider this:
 *
 *    op IsPositive(x:integer)->b:boolean
 *        post:
 *            if x >= 0
 *            then b = true
 *            else b = false;
 *
 * In this case, we require the implementors to have produced a value of b that
 * renders the if-then-else always true.  So, we could say in a way that we
 * don't care about the value of the if-then-else itself, but rather the "side
 * effects" of what goes on in the then and else parts, which we can think of
 * in a way as the if-then-else "body".  So given this bit of reasoning, let's
 * go back to
 *
 *     else exists (x in xl) if (x.id = id) then (x' = x) else x' = nil
 *
 * What exactly are we requiring from the implementors here in terms of the
 * value of x'?
 *
 * But wait just one gosh darn minute here.  Haven't we said that a false
 * postcond means the output is nil?  If this is the case, we don't need the
 * conditional at all.  I.e., when
 *
 *     exists (x in xl) (x.id = id) and (x' = x)
 *
 * is false, the output of Find will be nil, which in this case means x' =
 * nil.  So, is this strong enough?  I need to go now, but I'll come back here
 * hopefully.  The deal is, we need to determine if it's OK for a postcond ever
 * to go false, which I'd like to say "no" to, which means the this is not in
 * fact enough.  I.e., a false postcond means the implementation HAS
 * FUNDAMENTALLY FAILED, which means we cannot rely on a false postcond as a
 * shortcut to get a legitmately nil result as an output.

exists (x in xl) (x.id = id) and (x' = x) <=>
not (forall (x in xl) not ((x.id = id) and (x' = x))) <=>
not (forall (x in xl) not ( (not ((x.id != id) or (x' != x))))) <=>
not (forall (x in xl) (x.id != id) or (x' != x))

exists (x in xl) p <=> not (forall (x in xl) not p)
forall (x in xl) if (x.id = id) then (x' = x) else (x' = nil)

 *)


(*
 *)

obj Record = name:Name and id:ID and data:Data;
obj Name = string;
obj ID = integer;
obj Data;
obj DB = Record*;

op Find(db:DB, id:ID, ilist:integer*)->(r:Record)
    post:
        (if exists (r' in db) (r'.id = id)
         then r = r'
         else r = nil)

            or

        (exists (r' in ilist) (r' = 10))

            or

        (exists (r' in db) (r = r'))

            or

        (exists (r' in db) (r'.id = id) and (r = r'))

            or

        (exists (r' in db) (r'.id = id) and (r = r') or
         not (exists (r' in db) (r'.id = id)) and (r = nil));

end;