loop guards don't allow quantifiers

[erniecohen]

Guards of while statements should take the full expression language, just like guards of conditionals, including "some". (The workaround is predictably gross.)

[kenmcmil]

True enough. What I am seeing though is that quantifiers are allowed in while conditions but don't compile correctly, but "while some" is rejected as bad syntax. If you have an example where a quantifier in a while condition is giving an error messages, please let me know.

[kenmcmil]

Fixed checker and compiler so that 'while some' is supported. For example, this program now checks and compiles:

#lang ivy1.7

include order

instance t : unbounded_sequence 

var v : t
relation p(X:t)


action a(bound:t) = {
    while some x:t. (x < bound & ~p(x)) {
	assert ~p(x);
	p(x) := true
    };
    assert X < bound -> p(X)
}

export a

Also, fixed problem of incorrect compilation of quantifiers in while conditions. Added regressions. These fixes are not well tested, so please reopen this issue with a test case if there is still a problem.