ensure/requires: needs to be fmlas:

[dijkstracula]

The chain replication program fails to parse because of the following invariant:

102         ensure forall P1:pid,P2:pid. msg_count = 0 ->
103             host(P1).contents.end = host(P2).contents.end &
104             forall I. (I < host(P1).contents.end -> host(P1).contents.value(I) = host(P2).contents.value(I));

➜  irving git:(nathan/cli) ✗ cargo run ~/school/phd/coursework/395T_mcmillan/homework/homework2.ivy p-print
    Finished dev [unoptimized + debuginfo] target(s) in 0.02s
     Running `target/debug/irving /Users/ntaylor/school/phd/coursework/395T_mcmillan/homework/homework2.ivy p-print`
Error:    --> 104:13
    |
104 |             forall I. (I < host(P1).contents.end -> host(P1).contents.value(I) = host(P2).contents.value(I));
    |             ^---
    |
    = expected NOT, number, boollit, symbol, or LOGICVAR
➜  irving git:(nathan/cli) ✗

Basically, the logic parser forces us to push quantifiers to the outside but clearly there are cases where we want this to work..

Looks like Ivy knows how to push quantifiers outside the & expression, but maybe we should automate doing the same.

  1958         for (int P1 = 0; P1 < max+1; P1++) {
  1959             int __tmp4;
  1960             __tmp4 = 1;
  1961             for (int P2 = 0; P2 < max+1; P2++) {
  1962                 int __tmp5;
  1963                 __tmp5 = 1;
  1964                 for (unsigned long long I = 0; I < file__end(host__contents[P1]); I++) {
  1965                     if (!(!(I < file__end(host__contents[P1])) || (file__value(host__contents[P1],I) == file__value(host__contents[P2],I)))) __tmp5 = 0       ;
  1966                 }
  1967                 if (!(!(msg_count == 0) || ((file__end(host__contents[P1]) == file__end(host__contents[P2])) && __tmp5))) __tmp4 = 0;
  1968             }
  1969             if (!__tmp4) __tmp3 = 0;
  1970         }
  1971         ivy_assert(__tmp3, "homework2.ivy: line 102");

[dijkstracula]

While I'm in there, the grammar for logicvar should make the sort an ident.

[dijkstracula]

Up to this point I had been handling this by requiring all formulas on my end to be in prenex normal form. Unfortunately, this puts us in a bit of a bind because Ivy's quantifier bounds heuristic fails us in the case where we move the inner quantifier to the outside:

 18                 ensure forall P1:pid,P2:pid, I. msg_count = 0 ->
 19                     host(P1).contents.end = host(P2).contents.end &
 20                     (I < host(P1).contents.end -> host(P1).contents.value(I) = host(P2).contents.val    ue(I));

(venv) ➜  /tmp ivyc target=test foo.ivy  
foo.ivy: line 18: error: cannot find an upper bound for I:index
(venv) ➜  /tmp

Essentially this is because Ivy never walks the conjunction when exists=False in ivy_to_cpp::get_bound_exprs.

So, we need to actually handle arbitrary quantifiers in formulas. This is a problem because I was lazy and tried to separate out "quantifier definitions" from "the expression that might make use of them".

This will require:

[ ] Changing the grammar to support nested quantifiers; [ ] Changing the AST to not just hold expressions; [ ] Changing the visitor module to walk formulas without ever falling back to expressions.

This has the side benefit that we can also trivially emit custom code for formulae that we might not want to with expressions, so it's objectively the right thing to do anyway. Still, though, irritating.

[dijkstracula]

b7c60a3f0cc1dc6e41a9c98a962d5abb1ed00aa8 .