Allow type annotations

[KenSakayori]

This PR allows users to annotate formulas with refinement types.
The refinement types should be written in a separate *.annot file.

TODOs:

• Contact the original authors and check if they are fine with this PR
• Run a regression test
• Polish the README
• Remove embedded examples
• (Further squash?)
• Add examples to this repository
• Bump up the version number

[KenSakayori]

This is now ready to be merged.
After all, the changes aren't that big.
The essential additions are

• the new parser and lexer for the type annotations
• check_annotation and infer_based_on_annotation functions in rinfer.ml. Plus some code for the "dependency tracking" in rinfer.ml, which is used to decide which predicates to keep when checking the type annotation.
• new options --annot <input.annot> and --target <CHECK_TARGET> defined in rethfl_options.ml. The main function of rethfl_typing.ml now changes its behavior according to these options.

@moratorium08 Do you want to review this or can I just merge it?

Let me also write down some areas for improvements (which I'm not going to address in this PR).

• Only one predicate can be annotated right now. To generalize this both the parser and rinfer.ml needs to be modified accordingly. But this doesn't seem that hard.
• We need to invoke ReTHFL twice to check whether a given formula is valid. This is because we need to run ReTHFL to (1) check if the annotation is correct and (2) check if the main formula is valid assuming that the annotation is correct. I think it's better if ReTHFL automatically does both when an annotation file is given. (I think the reason for separating the two was solely for the ease of experiment.)
• The disprove mode doesn't work well with the semi-automated method. I mean we don't report a useful information when the constraints are unsatisfiable because the only thing it says is "invalid". This might be confusing since it may just be the case that the annotation is wrong while the input formula is actually valid.

[moratorium08]

There are some concerns as follows, but overall, this change looks fine:

1. What happens if invalid refinement types, such as not well-formed ones, are provided?
2. --remove-disjunctions breaks the structure of fixpoints (e.g., by introducing another variable or continuations). But it’s fine to leave this for future work.
3. Why does input/annot/ only include ML files? If you expect ocaml2hfl functionality in MoCHi, it would be better to provide generated HFL(Z) files since the annotation targets HFL(Z).

[moratorium08]

I'm not sure what happens if we assume well-formedness for refinement types.
It might be better that when users write a non-well-formed type, the program fails with some error.

[moratorium08]

Since this change does not break the current functionality, you can merge it whenever you’re ready.

[KenSakayori]

As for 3, I just forgot to add it. I'll added them (and force pushed) now.

Actually, I was planning to add only the .hfl (or .in, whatever the suffix is) and the .annot file, but I accidentally pushed the .ml instead of .hfl.
My new change didn't delete the .ml files since I think those are useful as well.

[KenSakayori]

I won't address 1 and 2 for now, but those are good catches.
The first point is easy to fix. I think it's more natural to check it during the type checking phase than to check it during parsing.
For 2, do you know if --remove-disjunctions is the only optimization that introduces/removes new predicate variables?
Maybe inlining could be an issue as well?
If remove-disjunctions is the only one, for the current use case, it won't be a big problem.
This is because we are currently only interested in safety properties, and those only generate "tractable formulas".