Extend (and document) `require` clauses with functions

[alberdingk-thijm]

Currently the require clause accepts fairly simple statements. One possible extension that could be useful (particularly for my work) is to allow users to reference other NV functions from the require clause, e.g. writing something like the following:

symbolic x : int
require (f x) = (merge 0n (init 0n) (f x))
(* ... definitions of f, init and merge ... *)

This currently returns an "unbound variable f~0" on compilation. I would also find it handy to be able to refer to the solution at a node using a function, e.g. (lab n) would give me the solution at node n. My main use-case for this is in require clauses specifically, but it doesn't necessarily need to be a user-available feature; I can just add an SMT statement that does this internally.

Also, we don't document how to use require anywhere in the wiki. This would be useful for new users.

[DKLoehr]

To respond in order:

1. I'm not currently aware of any restrictions on the body of a requires clause, although there certainly might be some. But it's definitely possible to use functions inside them. This example does so. You're getting an unbound variable error because you're using f before you define it. That said, I expect it would fail regardless because I don't think you can reference trans/merge/init like normal variables. Not sure, though.
2. Referring to the solution of a node is something we've talked about in various ways. It's likely to appear when we add in ocaml-like module syntax. We haven't really figured out how they'll work, but they're what I'm hoping to work on next. We can probably talk directly to figure out exactly what your needs are for getting the label and how it relates to partitioning.
3. You're right that it's not on the wiki. I don't think symbolics are on there either. I'll try to add them tonight or tomorrow.

[alberdingk-thijm]

For point 1, I'm guessing this opens up into a more general question of using the definitions of trans, merge and init elsewhere in the program like they were regular functions. We can certainly emulate this behaviour by having a helper function, e.g.

let helper e x = match edge with
  | 0~1 -> x + 1
  | _ -> x

let trans e x = helper e x

let assert node x = match node with
  | 0n -> x = 0
  | 1n -> x = (helper 0~1 0)

But extending the language to allow the functions to be used elsewhere would be cleaner, and I think would also dovetail nicely with work on point 2.

[DKLoehr]

I did some digging through the code and concluded that it would be a big pain to change the semantics such that merge/trans/init exist as real variables. I can do a hacky fix, but I'd rather not if we can avoid it. Probably the best thing to do is use the above workaround until we get modules more fleshed out, since they should remove this problem (if we do them right). If the workaround turns out to be a pain, let me know and I'll give you that fix.

I've also edited the NV Syntax page on the wiki to include symbolic variables and require clauses.

[alberdingk-thijm]

All right, sounds good to me. I'll close this and we can come back to it in the future if need be.