Merge branch 'unstable' into enable-records-in-arrays-encoding

UNRELEASED.md

@@ -11,6 +11,10 @@
 
      DO NOT LEAVE A BLANK LINE BELOW THIS PREAMBLE -->
 ### Features
-
+ * Enable records in the arrays encoding, see #1288
  * Implement the sequence constructor `Apalache!MkSeq`, see #1439
- * Enable records in the arrays encoding, see #1288
+ * Add support for `Apalache!FunAsSeq`, see #1442
+ * Implement `EXCEPT` on sequences, see #1444
+
+### Bug fixes
+ * Fixed bug where TLA+ `LAMBDA`s wouldn't inline outside `Fold` and `MkSeq`, see #1446

docs/src/apalache/features.md

@@ -154,10 +154,11 @@ Operator  | Supported? | Milestone | Comment
 
 Operator  | Supported? | Milestone | Comment
 ------------------------|:------------------:|:---------------:|--------------
-``<<...>>``, ``Head``, ``Tail``, ``Len``, ``SubSeq``, `Append`, `\o`, `f[e]` | ✔ | - | The sequence constructor ``<<...>>`` needs a [type annotation](https://apalache.informal.systems/docs/tutorials/snowcat-tutorial.html).
-`EXCEPT` | ✖ |   | If you need it, let us know, issue #324
+`<<...>>` | ✔ |   | Often needs a [type annotation](https://apalache.informal.systems/docs/tutorials/snowcat-tutorial.html).
+`Head`, `Tail`, `Len``, `SubSeq`, `Append`, `\o`, `f[e]` | ✔ | - |
+`EXCEPT` | ✔ |   |
+`SelectSeq` | ✔ | - | Not as efficient, as it could be, see [#1350](https://github.com/informalsystems/apalache/issues/1350).
 `Seq(S)` | ✖ | - | Use `Gen` of Apalache to produce bounded sequences
-`SelectSeq` | ✖ | - | Planned in [#873](https://github.com/informalsystems/apalache/issues/873). Till then, use `FoldSeq`.
 
 ### FiniteSets
 

src/tla/Apalache.tla

@@ -74,8 +74,8 @@ MkSeq(N, F(_)) ==
  * @type: ((Int -> a), Int) => Seq(a);
  *)
 FunAsSeq(fn, maxSeqLen) ==
-    LET F(i) == fn[i] IN
-    MkSeq(maxSeqLen, F)
+    LET __FunAsSeq_elem_ctor(i) == fn[i] IN
+    MkSeq(maxSeqLen, __FunAsSeq_elem_ctor)
 
 (**
  * Annotating an expression \E x \in S: P as Skolemizable. That is, it can

test/tla/SimpleLambda.tla

@@ -0,0 +1,13 @@
+--------------------- MODULE SimpleLambda -----------------                      
+L(F(_), n) == F(n)
+
+Init ==
+    TRUE
+
+Next ==
+    TRUE
+
+Inv ==
+    L(LAMBDA i: i, 3) = 3
+
+===========================================================

test/tla/TestSequences.tla

@@ -176,6 +176,23 @@ TestSelectSeqEmpty ==
 TestFoldSeqOverSelectSeq ==
     FoldSeq(Add, 0, SelectSeq(seq345, IsOdd)) = 3 + 5
 
+TestFunAsSeq3 ==
+    LET f == [ i \in 1..3 |-> i + 1 ] IN
+    FunAsSeq(f, 3) = <<2, 3, 4>>
+
+TestFunAsSeqEmpty ==
+    LET
+        \* @type: Int -> Int;
+        f == [ i \in {} |-> i ]
+    IN
+    FunAsSeq(f, 0) = << >>
+
+TestExceptLen ==
+    Len([seq345 EXCEPT ![2] = 10]) = 3
+
+TestExceptDomain ==
+    DOMAIN [seq345 EXCEPT ![2] = 10] = DOMAIN seq345
+
 \* this test is a disjunction of all smaller tests
 AllTests ==
     /\ TestHeadEmpty
@@ -216,4 +233,8 @@ AllTests ==
     /\ TestMkSeqSubSeq
     /\ TestMkSeqLen
     /\ TestMkSeqFold
+    /\ TestFunAsSeq3
+    /\ TestFunAsSeqEmpty
+    /\ TestExceptLen
+    /\ TestExceptDomain
 ===============================================================================

test/tla/cli-integration-tests.md

@@ -1184,6 +1184,15 @@ The outcome is: NoError
 EXITCODE: OK
 ```
 
+### check SimpleLambda succeeds
+Regression test for https://github.com/informalsystems/apalache/issues/1446
+
+```sh
+$ apalache-mc check --inv=Inv SimpleLambda.tla | sed 's/I@.*//'
+...
+EXITCODE: OK
+```
+
 ### check Bug914 succeeds
 
 Regression test for https://github.com/informalsystems/apalache/issues/914 In

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunExceptRule.scala

@@ -1,13 +1,12 @@
 package at.forsyte.apalache.tla.bmcmt.rules
 
 import at.forsyte.apalache.tla.bmcmt._
+import at.forsyte.apalache.tla.bmcmt.rules.aux.ProtoSeqOps
 import at.forsyte.apalache.tla.lir.convenience._
 import at.forsyte.apalache.tla.lir.oper.TlaFunOper
 import at.forsyte.apalache.tla.lir.values.{TlaInt, TlaStr}
-import at.forsyte.apalache.tla.lir.{OperEx, TlaEx, ValEx}
+import at.forsyte.apalache.tla.lir.{BoolT1, FunT1, OperEx, RecT1, SeqT1, SetT1, TlaEx, TlaType1, TupT1, ValEx}
 import at.forsyte.apalache.tla.lir.TypedPredefs._
-import at.forsyte.apalache.tla.lir.TlaType1
-import at.forsyte.apalache.tla.lir.{BoolT1, FunT1, RecT1, SetT1, TupT1}
 
 /**
  * Rewriting EXCEPT for functions, tuples, and records.
@@ -16,6 +15,8 @@ import at.forsyte.apalache.tla.lir.{BoolT1, FunT1, RecT1, SetT1, TupT1}
  *   Igor Konnov
  */
 class FunExceptRule(rewriter: SymbStateRewriter) extends RewritingRule {
+  private val proto = new ProtoSeqOps(rewriter)
+
   private def cacheEq(s: SymbState, l: ArenaCell, r: ArenaCell) = rewriter.lazyEq.cacheOneEqConstraint(s, l, r)
 
   private def solverAssert = rewriter.solverContext.assertGroundExpr _
@@ -45,6 +46,7 @@ class FunExceptRule(rewriter: SymbStateRewriter) extends RewritingRule {
           case ft @ FunT1(_, _)  => rewriteFun(nextState, funCell, ft, indexCell, valueCell)
           case rt @ RecT1(_)     => rewriteRec(nextState, funCell, rt, indexEx, valueCell)
           case tt @ TupT1(_ @_*) => rewriteTuple(nextState, funCell, tt, indexEx, valueCell)
+          case SeqT1(et)         => rewriteSeq(nextState, funCell, et, indexCell, valueCell)
           case _ =>
             throw new NotImplementedError(s"EXCEPT is not implemented for $funT. Write a feature request.")
         }
@@ -189,4 +191,29 @@ class FunExceptRule(rewriter: SymbStateRewriter) extends RewritingRule {
 
     rewriter.rewriteUntilDone(nextState.setRex(newTuple.toNameEx))
   }
+
+  // rewrite a sequence with EXCEPT semantics
+  def rewriteSeq(
+      state: SymbState,
+      oldSeq: ArenaCell,
+      elemT: TlaType1,
+      indexCell: ArenaCell,
+      newValue: ArenaCell): SymbState = {
+    val (oldProtoSeq, len, capacity) = proto.unpackSeq(state.arena, oldSeq)
+
+    // make an element for the new proto sequence
+    def mkElem(state: SymbState, index: Int): (SymbState, ArenaCell) = {
+      val oldValue = proto.at(state.arena, oldProtoSeq, index)
+      val cond = tla.eql(indexCell.toNameEx, tla.int(index)).as(BoolT1())
+      // IF indexCell = index THEN newValue ELSE oldValue
+      val iteEx = tla.ite(cond, newValue.toNameEx, oldValue.toNameEx).as(elemT)
+      val newState = rewriter.rewriteUntilDone(state.setRex(iteEx))
+      (newState, newState.asCell)
+    }
+
+    // make a new proto sequence of the same capacity and the same length
+    val nextState = proto.make(state, capacity, mkElem)
+    val newProtoSeq = nextState.asCell
+    proto.mkSeq(nextState, SeqT1(elemT), newProtoSeq, len)
+  }
 }

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterSequence.scala

@@ -328,5 +328,35 @@ trait TestSymbStateRewriterSequence extends RewriterBase {
     assert(solverContext.sat())
   }
 
+  test("""(<<3, 4, 5, 6>> EXCEPT ![2] = 7) = <<3, 7, 5, 6>>""") { rewriterType: SMTEncoding =>
+    val tup3to6 = tuple(3.to(6).map(int): _*).as(intSeqT)
+    val tup3756 = tuple(Seq(3, 7, 5, 6).map(int): _*).as(intSeqT)
+    val exceptEx = except(tup3to6, tuple(int(2)).as(TupT1(IntT1())), int(7)).as(intSeqT)
+    val eq = eql(exceptEx, tup3756).as(boolT)
+
+    val state = new SymbState(eq, arena, Binding())
+    assertTlaExAndRestore(create(rewriterType), state)
+  }
+
+  test("""(<<3, 4, 5, 6>> EXCEPT ![10] = 7) = <<3, 4, 5, 6>>""") { rewriterType: SMTEncoding =>
+    val tup3to6 = tuple(3.to(6).map(int): _*).as(intSeqT)
+    val exceptEx = except(tup3to6, tuple(int(10)).as(TupT1(IntT1())), int(7)).as(intSeqT)
+    // since 10 does not belong to the domain, the sequence does not change
+    val eq = eql(exceptEx, tup3to6).as(boolT)
+
+    val state = new SymbState(eq, arena, Binding())
+    assertTlaExAndRestore(create(rewriterType), state)
+  }
+
+  test("""(<< >> EXCEPT ![10] = 7) = << >>""") { rewriterType: SMTEncoding =>
+    val emptyTuple = tuple().as(intSeqT)
+    val exceptEx = except(emptyTuple, tuple(int(10)).as(TupT1(IntT1())), int(7)).as(intSeqT)
+    // since 10 does not belong to the domain, the sequence does not change
+    val eq = eql(exceptEx, emptyTuple).as(boolT)
+
+    val state = new SymbState(eq, arena, Binding())
+    assertTlaExAndRestore(create(rewriterType), state)
+  }
+
   // for PICK see TestCherryPick
 }

tla-io/src/main/scala/at/forsyte/apalache/tla/imp/StandardLibrary.scala

@@ -59,7 +59,6 @@ object StandardLibrary {
         ("Apalache", "Skolem") -> ApalacheOper.skolem,
         ("Apalache", "Expand") -> ApalacheOper.expand,
         ("Apalache", "ConstCardinality") -> ApalacheOper.constCard,
-        ("Apalache", "FunAsSeq") -> ApalacheOper.funAsSeq,
         ("Apalache", "MkSeq") -> ApalacheOper.mkSeq,
         ("Apalache", "SetAsFun") -> ApalacheOper.setAsFun,
         ("Apalache", "FoldSet") -> ApalacheOper.foldSet,

tla-io/src/test/scala/at/forsyte/apalache/tla/imp/TestSanyImporterStandardModules.scala

@@ -516,7 +516,7 @@ class TestSanyImporterStandardModules extends SanyImporterTestBase {
 
     val root = modules("root")
     expectSourceInfoInDefs(root)
-    assert(8 == root.declarations.size)
+    assert(9 == root.declarations.size)
 
     def expectDecl(name: String, body: TlaEx) = {
       findAndExpectOperDecl(root, name, List(), body)

tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/InlinerOfUserOper.scala

@@ -58,6 +58,11 @@ class InlinerOfUserOper(defBodyMap: BodyMap, tracker: TransformationTracker) ext
         case _ => ex
       }
 
+    // Lambda and call-by name passed as LET-IN
+    case ex @ OperEx(TlaOper.apply, LetInEx(NameEx(name), decl @ TlaOperDecl(declName, params, _)), args @ _*)
+        if name == declName && params.size == args.size =>
+      instantiateWithArgs(stepLimitOpt)(decl, args).withTag(ex.typeTag)
+
     // recursive processing of composite operators and let-in definitions
     case ex @ LetInEx(body, defs @ _*) =>
       // transform bodies of all op.defs

tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/SetMembershipSimplifier.scala

@@ -7,9 +7,19 @@ import at.forsyte.apalache.tla.lir.transformations.{LanguageWatchdog, Transforma
 import at.forsyte.apalache.tla.lir.values._
 
 /**
- * A simplifier that rewrites vacuously true membership tests based on type information.
+ * A simplifier that rewrites expressions commonly found in `TypeOK`. Assumes expressions to be well-typed.
  *
- * For example, `x \in BOOLEAN` is rewritten to `TRUE` if x is typed BoolT1.
+ * After Apalache's type-checking, we can rewrite some expressions to simpler forms. For example, the (after
+ * type-checking) vacuously true `x \in BOOLEAN` is rewritten to `TRUE` (as `x` must be a `BoolT1`).
+ *
+ * We currently perform the following simplifications (for type-defining sets TDS, see [[isTypeDefining]]):
+ *   - `n \in Nat` ~> `x >= 0`
+ *   - `b \in BOOLEAN`, `i \in Int`, `r \in Real` ~> `TRUE`
+ *   - `seq \in Seq(TDS)` ~> `TRUE`
+ *   - `set \in SUBSET TDS` ~> `TRUE`
+ *   - `fun \in [TDS1 -> TDS2]` ~> `TRUE`
+ *   - `fun \in [Dom -> TDS]` ~> `DOMAIN fun = Dom`
+ *   - `tup \in TDS1 \X ... \X TDSn` ~> `TRUE`
  *
  * @author
  *   Thomas Pani
@@ -27,46 +37,60 @@ class SetMembershipSimplifier(tracker: TransformationTracker) extends AbstractTr
   }
 
   /**
-   * Returns the type of a TLA+ predefined set, if rewriting set membership to TRUE is applicable. In particular, it is
-   * *not* applicable to `Nat`, since `i \in Nat` does not hold for all `IntT1`-typed `i`.
+   * Returns true iff the passed TLA+ expression is a type-defining set. Type-defining sets contain all of the values of
+   * their respective element type.
+   *
+   * The type-defining sets are inductively defined as
+   *   - the predefined sets BOOLEAN, Int, Real, STRING,
+   *   - sets of sequences over type-defining sets, e.g., Seq(BOOLEAN), Seq(Int), Seq(Seq(Int)), Seq(SUBSET Int), ...
+   *   - power sets of type-defining sets, e.g., SUBSET BOOLEAN, SUBSET Int, SUBSET Seq(Int), ...
+   *   - sets of functions over type-defining sets, e.g., [Int -> BOOLEAN], ...
+   *   - the cartesian product TDS1 \X ...\X TDSn of type-defining sets
+   *
+   * In particular, `Nat` is not type-defining, nor are sequence sets / power sets thereof, since `i \in Nat` does not
+   * hold for all `IntT1`-typed `i`.
    */
-  private def typeOfSupportedPredefSet: PartialFunction[TlaPredefSet, TlaType1] = {
-    case TlaBoolSet => BoolT1()
-    case TlaIntSet  => IntT1()
-    case TlaRealSet => RealT1()
-    case TlaStrSet  => StrT1()
-    // intentionally omits TlaNatSet, see above.
-  }
+  private def isTypeDefining: Function[TlaEx, Boolean] = {
+    // base case: BOOLEAN, Int, Real, STRING
+    case ValEx(TlaBoolSet) | ValEx(TlaIntSet) | ValEx(TlaRealSet) | ValEx(TlaStrSet) => true
 
-  /**
-   * Checks if this transformation is applicable (see [[typeOfSupportedPredefSet]]) to a TLA+ predefined set `ps` of
-   * primitives, and if the types of `name` and `ps` match.
-   */
-  private def isApplicable(name: TlaEx, ps: TlaPredefSet): Boolean =
-    typeOfSupportedPredefSet.isDefinedAt(ps) && name.typeTag == Typed(typeOfSupportedPredefSet(ps))
+    // inductive cases:
+    // 1. Seq(s) for a type-defining set `s`
+    case OperEx(TlaSetOper.seqSet, set) => isTypeDefining(set)
+    // 2. SUBSET s for a type-defining set `s`
+    case OperEx(TlaSetOper.powerset, set) => isTypeDefining(set)
+    // 3. [s1 -> s2] for type-defining sets `s1` and `s2`
+    case OperEx(TlaSetOper.funSet, set1, set2) => isTypeDefining(set1) && isTypeDefining(set2)
+    // 4. s1 \X ... \X sn for type-defining sets `s1` to `sn`
+    case OperEx(TlaSetOper.times, args @ _*) => args.forall(set => isTypeDefining(set))
 
-  /**
-   * Checks if this transformation is applicable (see [[typeOfSupportedPredefSet]]) to a TLA+ predefined set of
-   * sequences (`Seq(_)`) `ps`, and if the types of `name` and `ps` match.
-   */
-  private def isApplicableSeq(name: TlaEx, ps: TlaPredefSet): Boolean =
-    typeOfSupportedPredefSet.isDefinedAt(ps) && name.typeTag == Typed(SeqT1(typeOfSupportedPredefSet(ps)))
+    // otherwise
+    case _ => false
+  }
 
   /**
-   * Rewrites vacuously true membership tests based on type information, and rewrites `i \in Nat` to `i \ge 0`.
+   * Simplifies expressions commonly found in `TypeOK`, assuming they are well-typed.
    *
-   * For example, `x \in BOOLEAN` is rewritten to `TRUE` if `x` is typed `BoolT1`.
+   * @see
+   *   [[SetMembershipSimplifier]] for a full list of supported rewritings.
    */
   private def transformMembership: PartialFunction[TlaEx, TlaEx] = {
-    // n \in Nat  ->  x >= 0
-    case OperEx(TlaSetOper.in, name, ValEx(TlaNatSet)) if name.typeTag == Typed(IntT1()) =>
-      OperEx(TlaArithOper.ge, name, ValEx(TlaInt(0))(intTag))(boolTag)
-    // b \in BOOLEAN, i \in Int, r \in Real  ->  TRUE
-    case OperEx(TlaSetOper.in, name, ValEx(ps: TlaPredefSet)) if isApplicable(name, ps) => trueVal
-    // seq \in Seq(_)  ->  TRUE
-    case OperEx(TlaSetOper.in, name, OperEx(TlaSetOper.seqSet, ValEx(ps: TlaPredefSet))) if isApplicableSeq(name, ps) =>
-      trueVal
-    // return `ex` unchanged
+    case ex @ OperEx(TlaSetOper.in, name, set) =>
+      set match {
+        // x \in TDS  ~>  TRUE
+        case set if isTypeDefining(set) => trueVal
+
+        // n \in Nat  ~>  x >= 0
+        case ValEx(TlaNatSet) => OperEx(TlaArithOper.ge, name, ValEx(TlaInt(0))(intTag))(boolTag)
+
+        // fun \in [Dom -> TDS]  ~>  DOMAIN fun = Dom    (fun \in [TDS1 -> TDS2] is handled above)
+        case OperEx(TlaSetOper.funSet, domain, set2) if isTypeDefining(set2) =>
+          OperEx(TlaOper.eq, OperEx(TlaFunOper.domain, name)(domain.typeTag), domain)(boolTag)
+
+        // otherwise, return `ex` unchanged
+        case _ => ex
+      }
+    // return non-set membership expressions unchanged
     case ex => ex
   }
 }