Improved support for CAT features

[ThomasHaas]

We need to improve our support for CAT features to handle the new ARM/ASL model. Having those features is generally useful even outside of ARM/ASL. I want to list the features and give some insight in how to implement them.

1. [DONE in Added support for includes and functions in cat #736]Support for function declarations and function calls. If we do not support recursive functions (though ARM/ASL does have those but I think they are unnecessary), it would be fine to have the parser directly inline all calls during parsing. So there is no need to update the backend in any way.
   herd7's support for function calls is quite extensive. For example (from herd7 enumerations.cat)

let add_pair p = map (fun r -> (p | r))

declares a function add_pair that takes a single parameter p and returns a partially applied map function (curried).
The result is a function that takes a set of relations R and maps this set to a new one by adding p to each r in R.
I don't believe we need such extensive support(*) but we should aim to support the basics at least.

2. [DONE in Added support for includes and functions in cat #736] Support for includes (include "other.cat"). The parser should just inline the included files directly at the location where it is included. Again, there is no need to update our backend. However, we could move common definitions like fr, fre, rfi, etc. into a basics.cat and then streamline our handling of those relations.

3. Support for ifs (needed for ARM/ASL). The syntax looks like this (if COND then r1 else r2). Here COND is like a compilation flag, meaning that during parsing time the parser will resolve the conditional choice. More concretely, the syntax is COND ::= "OPTION" | COND && COND | COND || COND | not COND, i.e., boolean expressions over atomic options flags "OPTION" (just any string). Again, this feature is parser-only and the backend doesn't need to change.

4. Support for special options that modify how the CAT file is interpreted. ARM/ASL has this line at the top "catdep (* This option says that the cat file computes dependencies *)", which likely means that local operations are visible so that internal data dependencies can be accessed (e.g. idd in our case). Such a feature would also allow for options like partialco to change how co is interpreted, or verification options like local-consistency to state helpful information that simplifies reasoning about the CAT file.

[DONE in #908] Apart from the support for new syntax, we should also add support for proper unary predicates as mentioned in #371.

(*) Herd7 uses a very convoluted way to take a set of unordered-pairs and ordering it so that it is compatible with some relation r. Herd7 uses recursion, complex pattern matching, and sets of relations to achieve this (enumerations.cat)
Using a free relation makes this rather trivial:

let result = new() // free relation
acyclic (result |  r) // relation must be acyclic and be compatible with r
empty (unordered-pairs \ (result | result^-1)) // Every unordered-pair must be related (and cannot be related in both directions due to acyclicity)

I would prefer this approach over trying to support the mess that herd7 does.