Change the syntax of predicates to be pred(ins ; outs)

[giltho]

Depends on #379

Change the syntax predicates to avoid having the clunky + to indicate in-parameters and have ins first, and then outs after a semi-colon.

This is better reviewed commit-by-commit.

• The first commit re-orders arguments in every predicate so that in-parameters come before out-parameters.
• The second commit changes the syntax of predicate declaration so that ins and outs must be separated with a semicolon
• The third commit changes the syntax of predicate calls with the same thing

[giltho]

Banger.
The next PR will be as massive, so let's get this one merged first

[giltho]

I do note that this incurs an additional overhead on the user part when writing predicates (as it requires writing explicitly ins and outs). This is a pre-existing choice for core predicates, but users would usually not write core predicates by hand unless they'd write GIL. Now they have to do it for predicates.

Eventually, it could be desirable for the GIL programs to define the number of parameters for each core predicate using e.g.

@ language_def
#core_pred "pred_name" 1 3
...

or something...

This would be optional but would enable checking programs...

[giltho]

Note that we could also have the compiler mark arguments as in and outs in predicate calls, but that means modifying all compilers to resolve all files with all definitions (including runtime .gil and .jsil files) before compilation happens.

[giltho]

Another note: this is also what CN and VeriFast require.
Cn requires user to write something like let v = PointsTo(x) instead x -> v, or let alpha = SLL(x), while VeriFast requires to write SLL(x, ?alpha).

[NatKarmios]

Okie doke, reviewing commit-by-commit

• 1c5bb46
• eeb7cba
• 15d85f6

[NatKarmios]

I'm not a big fan of always, always requiring a semicolon in predicate defs/calls, like
pred(;) feels pretty gross hahah
Shouldn't we have no semicolon implying all ins?
I can try tweaking the compilers tomorrow

[PetarMax]

Yes to pred(;) looking odd, but what kind of predicate would have zero parameters to begin with? This is a corner case that shouldn't appear much, surely.

[PetarMax]

No semicolon should be all ins, agreed.

[giltho]

Yes. And for predicate calls, ideally, they should be inserted by the compilers, inferred from predicate definitions

The issue is that the compilers currently don't assume we have the full program I think...

[NatKarmios]

Would it be more sane to change the types of preds / pred calls to have an ins list and an outs list, rather than a full params list and an ints count?

[giltho]

I considered both options, felt like this was the minimal change