Flattening does not support all export use cases

[bugarela]

Examples of unsupported scenarios:

module A {
  const N: int
  var x: int

  action aInit = x' = 0
  action aStep = x' = x + N
}

module B {
  import A(N=2) as A2
  export A2.*

  action bInit = A2::aInit
  // x is visible in bStep
  action bStep = all { A2::x >= 0, A2::aStep }
}

// C can be the internal module constructed by REPL
module C {
  import B.*

  action cInit = bInit
  action cStep = bStep
  // aInit, aStep, and x are visible in C
  action cInit2 = aInit
  action cStep2 = all { x >= 0, aStep }
}

/**
 * A Fast Majority Vote Algorithm by J Strother Moore.
 *
 * See: https://www.cs.utexas.edu/users/boyer/ftp/ics-reports/cmp32.pdf
 */
module mjrty {
  const votes: List[str]
  var cand: str
  var i: int
  var k: int

  action init = all {
    cand' = "",
    i' = 0,
    k' = 0,
  }

  action step = all {
    i < length(votes),
    any {
      all {
        k == 0,
        cand' = votes[i],
        k' = 1,
      },
      all {
        cand == votes[i],
        cand' = cand,
        k' = k + 1,
      },
      all {
        cand != votes[i],
        cand' = cand,
        k' = k - 1,
      },
    },
    i' = i + 1,
  }

  val invariant = {
    (i == length(votes))
      implies
    {
      val candidates = indices(votes).map(j => votes[j])
      val winnerCount = indices(votes).filter(j => votes[j] == cand).size()
      candidates.forall(c =>
        val count = indices(votes).filter(j => votes[j] == c).size()
        count <= winnerCount
      )
    }
  }
}

module mjrtyTest {
  import mjrty(votes = ["A", "A", "A", "C", "C", "B", "B", "C", "C", "C", "A", "A", "A"]) as M
  export M.*
}

We should either support all use cases or report proper errors

[bugarela]

We had a meeting today to discuss the behavior in combinations of instances and exports. Here are the main outputs:

1. Definitions should only be exported with the same names as they appear on the exporting module.
2. We want to drop support of instances without a qualifier (import A(N=1).*)
3. We feel like we should change the syntax for instances, perhaps to instance A(N=1) as A1.
4. @Kukovec suggested that we might want a new type of import that imports only pure definitions from the module. We also think that having some sort of effect tracking for constant usage might be helpful - as pure in the sense should also mean that no constants are used.

More concretely, I suggested that we use this week's quint meeting to try to define the ideal scenario for imports, instances and exports, and from that, derive what we want to change right now.