feat: numerical comparison of literals in `where` clauses

[liangyiliang]

Is your feature request related to a problem? Please describe.

Now that we have substance literals (#1682) it would be nice to have some sort of built-in predicates for literal numbers, like <, <=, ==, >, and >=. It would also need to support numerical computations.

That way we can reason about literals like,

forall Number n1; Number n2
where Pred(n1); Pred(n2); n1 < n2 {
 ...
}

Notice that these "predicates" don't really appear in Substance, so we cannot directly perform matching against Substance. Instead we would need to first generate a list of matchings from all other declarations/predicates, and then filter them on which ones are not satisfied.

Implementation concerns

I feel that we may be able to reuse the "calculator" that I implemented for substance sequences (indexed sets) (#1572).

[liangyiliang]

Here is a concrete example. Suppose we want to visualize arrays like [obj1, obj2, obj3]. We want to visualize it left-to-right.

One way to specify such an array is to specify an order between the objects:

Object obj1, obj2, obj3
Succ(obj1, obj2)
Succ(obj2, obj3)

Then the array is easy to implement in Style:

forall Object obj {
  -- draw a circle with a text in it
  obj.y = 0
  obj.x = ?
  Circle {
    center: [obj.x, obj.y]
  }
  Text {
    string: nameof obj
    center: [obj.x, obj.y]
  }
}

forall Object o1, o2
where Succ(o1, o2) {
  -- o1 should be on the left of o2
  ensure o1.x < o2.x
}

But, another equally valid way to specify the array is as a mapping from index to object:

Object obj1, obj2, obj3
Index(0, obj1)
Index(1, obj2)
Index(2, obj3)

Then, we cannot write equivlalently-behaved selector blocks. The best thing we can do is,

forall Object obj1, obj2; Number n1; n2
where Index(n1, obj1); Index(n2, obj2) {
  -- reason about `n1` and `n2` within this block
  -- but this block is always going to get matched
}

There are probably smart ways we can make this functionally equivalent with the previous Style block by some intricate reasoning about n1 and n2, but it will definitely be harder.

On the other hand it would be much nicer to write,

forall Object obj1, obj2; Number n1, n2
where Index(n1, obj1); Index(n2, obj2); n1 < n2 {
  ensure obj1.x < obj2.x
}