Support for mutually-recursive operators in the type checker

[konnov]

This is probably a very rare feature request: freespek/ssf-mc#14

Here is the test to reproduce:

---- MODULE RecMutual1 ----
(*
 * An example of mutual recursion. Even though the model checker of Apalache does not support recursion
 * any longer, asking the users to use FoldSeq or FoldSet instead, the type checker should still accept it.
 *
 * We simply use the example of mutual recursion from Wikipedia:
 * https://en.wikipedia.org/wiki/Mutual_recursion
 *
 * Obviously, it is an extremely suboptimal way to check if a number is even or odd.
 * We can simply use (i % 2) == 0 in TLA+.
 *
 * Igor Konnov, September 2024
 *)
EXTENDS Integers

VARIABLES
    \* @type: Int;
    n,
    \* @type: Str;
    oddity

RECURSIVE is_even(_)
RECURSIVE is_odd(_)

is_even(i) ==
  IF i = 0
  THEN TRUE
  ELSE is_odd(i - 1)

is_odd(i) ==
  IF i = 0
  THEN FALSE
  ELSE is_even(i - 1)

get_oddity(i) ==
  IF is_even(i) = 0
  THEN "even"
  ELSE "odd"

Init ==
    /\ n = 0
    /\ oddity = get_oddity(n)

Next ==
    /\ n' = n + 1
    /\ oddity' = get_oddity(n')

====

When we call apalache-mc typecheck, it fails in the parser:

$ apalache-mc typecheck test/tla/RecMutual1.tla
Type checking test/tla/RecMutual1.tla                             I@18:44:32.916
PASS #0: SanyParser                                               I@18:44:32.986
Parsing file /Users/igor/devl/apalache/test/tla/RecMutual1.tla
Parsing file /private/var/folders/93/s11lf4f16c77bpq91r90njbm0000gn/T/Integers.tla
Parsing file /private/var/folders/93/s11lf4f16c77bpq91r90njbm0000gn/T/Naturals.tla
Check the dependency graph in dependencies.dot. You can view it with graphviz. E@18:44:33.097
Parsing error: Found a cyclic dependency among operators: get_oddity, Init, is_even, is_odd, Next

To fix this, we would have to properly identify mutually recursive operators, or extract this from SANY.