Add smart constructors for terms, and other improvements to fly/src/syntax.rs

[odedp]

Add smart constructors for Sort, Binder, and all Term cases. The smart constructors can take either something owned, and then they don't clone, or a reference, and then they clone. This is meant to make code for programmatically constructing Terms nicer, without a bunch of .clone everywhere. In a few (documented) cases, the smart constructors do a bit more normalization (e.g., Term::and([]) returns true and not an actual Term::And).

For now, these smart constructors are only used in code I still haven't pushed (in the liveness to safety), but I think they should be used everywhere. Basically, there's no reason to directly construct a Term.

To convert existing code, change the constructor to a smart constructor, and try to replace arg.clone() by &arg to make calling code look nicer.

Other small changes:

• Rename Sort::Id to Sort::Uninterpreted
• Rename UOp::Previously to UOp::Previous, which I think is more standard ("previously" is sometimes used for the past version of eventually)
• Documentation improvements

Minor issues and future TODOs:

• Binders passed to forall and exist still need to be owned. We can change this by having impl From<&Binder> for <Binder> similarly to what we do for Sort and Term.
• Term::and and Term::or take an IntoIterator which forces uniformity. So you cannot do Term::and([&t1, t2]) (where you can do Term::iff(&t1, t2), and must instead do Term::and([&t1, &t2]) which introduces an unnecessary clone. I don't think this clone gets optimized away. If we think this is a concern, we can implement variadic and and or, either with specialized functions (say for 2-9 arguments) or perhaps with a macro.

[tchajed]

I don't like this change to the documentation. I'd like to have some basic explanation of LTL here, and I don't think it's important to list the operators here (leave that for the language reference).

[odedp]

I didn't like the previous explanation, and I'm not sure the basic semantics of LTL should be explained in the documentation of Term. At some point, I think the language manual or other documentation should explain the semantics of FO-LTL. And I did find it helpful (even for myself) to list all the temporal operators here.

What do you think about the following compromise:

/// A Term is an FO-LTL (first-order linear temporal logic) term or formula. The
/// temporal operators supported are: Prime, Next, Prev, Until, Since, Always,
/// Eventually (see [`UOp`] and [`BinOp`]).
///
/// FO-LTL is an extension of first-order logic where the semantics is given in
/// terms of infinite sequences of models (over a shared universe). A term is
/// interpreted at a particular point (time) in the sequence, and using
/// temporal operators it can also query the past or future. For example
/// exists x. p(x) & (previous !p(x)) & always r(x) means that there exists
/// some element x for which p now holds, but it didn't hold a moment ago,
/// and from this point onwards r keeps holding for x.

[tchajed]

Sure, that looks good to me.

[odedp]

Great. I pushed a slightly edited version of this.

[vmwclabot]

@odedp, you must sign every commit in this pull request acknowledging our Developer Certificate of Origin before your changes are merged. This can be done by adding Signed-off-by: John Doe <john.doe@email.org> to the last line of each Git commit message. The e-mail address used to sign must match the e-mail address of the Git author. Click here to view the Developer Certificate of Origin agreement.

• Commit f1be1eb has a no-reply/unreachable author email address: odedp@users.noreply.github.com