From 6bf13300313450e582b3c105cfaf7cbbb785fdd6 Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Mon, 7 Mar 2022 09:41:57 +0100 Subject: [PATCH 1/7] Simplify SetMembershipSimplifier, assuming its inputs are well-typed --- .../tla/pp/SetMembershipSimplifier.scala | 53 +++++++++---------- .../tla/pp/TestSetMembershipSimplifier.scala | 12 +---- 2 files changed, 25 insertions(+), 40 deletions(-) diff --git a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/SetMembershipSimplifier.scala b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/SetMembershipSimplifier.scala index e0faf5917c..a66410e327 100644 --- a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/SetMembershipSimplifier.scala +++ b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/SetMembershipSimplifier.scala @@ -7,9 +7,15 @@ 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: + * - `n \in Nat` ~> `x >= 0` + * - `b \in BOOLEAN`, `i \in Int`, `r \in Real` ~> `TRUE` + * - `seq \in Seq(_)` ~> `TRUE` * * @author * Thomas Pani @@ -27,45 +33,34 @@ 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 rewriting of a well-typed set-membership test `x \in arg` to `TRUE` is applicable for the + * function's argument. + * + * In particular, it is *not* applicable to `Nat`, 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 isApplicable: Function[TlaPredefSet, Boolean] = { + case TlaBoolSet | TlaIntSet | TlaRealSet | TlaStrSet => true + case _ => false } /** - * 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)) - - /** - * 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))) - - /** - * 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()) => + case OperEx(TlaSetOper.in, name, ValEx(TlaNatSet)) => 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 + case OperEx(TlaSetOper.in, name, ValEx(ps: TlaPredefSet)) if isApplicable(ps) => trueVal + // seq \in Seq(_) -> TRUE - case OperEx(TlaSetOper.in, name, OperEx(TlaSetOper.seqSet, ValEx(ps: TlaPredefSet))) if isApplicableSeq(name, ps) => + case OperEx(TlaSetOper.in, name, OperEx(TlaSetOper.seqSet, ValEx(ps: TlaPredefSet))) if isApplicable(ps) => trueVal + // return `ex` unchanged case ex => ex } diff --git a/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestSetMembershipSimplifier.scala b/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestSetMembershipSimplifier.scala index 2e1e3e730e..5d9fcaf779 100644 --- a/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestSetMembershipSimplifier.scala +++ b/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestSetMembershipSimplifier.scala @@ -80,17 +80,7 @@ class TestSetMembershipSimplifier } } - test("returns inappropriately-typed set membership unchanged") { - expressions.foreach { case (name, value, _) => - expressions.filter { case (name2, _, _) => name != name2 }.foreach { case (_, _, otherSet) => - val inputName = tla.in(name, otherSet).as(BoolT1()) - simplifier(inputName) shouldBe inputName - - val inputValue = tla.in(value, otherSet).as(BoolT1()) - simplifier(inputValue) shouldBe inputValue - } - } - + test("returns myInt \\in Nat unchanged") { val intSeqNameInSeqNat = tla.in(intSeqName, natSeqSet).as(BoolT1()) val intSeqValInSeqNat = tla.in(intSeqVal, natSeqSet).as(BoolT1()) simplifier(intSeqNameInSeqNat) shouldBe intSeqNameInSeqNat From d03be0e87853b02e586a0d65dfe0d916ac41a76e Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Mon, 7 Mar 2022 09:46:35 +0100 Subject: [PATCH 2/7] Inductively define applicable sets This adds support for sets like `Seq(Seq(Int))`. Also, preparation for supporting further expressions like `SUBSET`. --- .../tla/pp/SetMembershipSimplifier.scala | 31 ++++++++++++------- 1 file changed, 19 insertions(+), 12 deletions(-) diff --git a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/SetMembershipSimplifier.scala b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/SetMembershipSimplifier.scala index a66410e327..99802b023d 100644 --- a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/SetMembershipSimplifier.scala +++ b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/SetMembershipSimplifier.scala @@ -36,11 +36,22 @@ class SetMembershipSimplifier(tracker: TransformationTracker) extends AbstractTr * Returns true iff rewriting of a well-typed set-membership test `x \in arg` to `TRUE` is applicable for the * function's argument. * - * In particular, it is *not* applicable to `Nat`, since `i \in Nat` does not hold for all `IntT1`-typed `i`. + * The applicable sets are inductively defined as + * - the predefined sets BOOLEAN, Int, Real, STRING, + * - sets of sequences over applicable sets, e.g., Seq(BOOLEAN), Seq(Int), Seq(Seq(Int)), ... + * + * In particular, it is *not* applicable to `Nat` and sequence sets, since `i \in Nat` does not hold for all + * `IntT1`-typed `i`. */ - private def isApplicable: Function[TlaPredefSet, Boolean] = { - case TlaBoolSet | TlaIntSet | TlaRealSet | TlaStrSet => true - case _ => false + private def isApplicable: Function[TlaEx, Boolean] = { + // base case: BOOLEAN, Int, Real, STRING + case ValEx(TlaBoolSet) | ValEx(TlaIntSet) | ValEx(TlaRealSet) | ValEx(TlaStrSet) => true + + // inductive case: Seq(s) for applicable set `s` + case OperEx(TlaSetOper.seqSet, set) => isApplicable(set) + + // otherwise + case _ => false } /** @@ -50,18 +61,14 @@ class SetMembershipSimplifier(tracker: TransformationTracker) extends AbstractTr * [[SetMembershipSimplifier]] for a full list of supported rewritings. */ private def transformMembership: PartialFunction[TlaEx, TlaEx] = { - // n \in Nat -> x >= 0 + // n \in Nat ~> x >= 0 case OperEx(TlaSetOper.in, name, ValEx(TlaNatSet)) => 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(ps) => trueVal - - // seq \in Seq(_) -> TRUE - case OperEx(TlaSetOper.in, name, OperEx(TlaSetOper.seqSet, ValEx(ps: TlaPredefSet))) if isApplicable(ps) => - trueVal + // x \in AS ~> TRUE for applicable sets AS (see `isApplicable`): + case OperEx(TlaSetOper.in, _, set) if isApplicable(set) => trueVal - // return `ex` unchanged + // otherwise, return `ex` unchanged case ex => ex } } From 96326ce04473ec5c8581ccfafa23783c929c203b Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Mon, 7 Mar 2022 09:54:59 +0100 Subject: [PATCH 3/7] Move test outside of loop --- .../apalache/tla/pp/TestSetMembershipSimplifier.scala | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestSetMembershipSimplifier.scala b/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestSetMembershipSimplifier.scala index 5d9fcaf779..c17812fbb5 100644 --- a/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestSetMembershipSimplifier.scala +++ b/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestSetMembershipSimplifier.scala @@ -60,6 +60,11 @@ class TestSetMembershipSimplifier } test("simplifies appropriately-typed set membership") { + val intNameInNat = tla.in(intName, tla.natSet()).as(BoolT1()) + val intValInNat = tla.in(intVal, tla.natSet()).as(BoolT1()) + simplifier(intNameInNat) shouldBe tla.ge(intName, tla.int(0)).as(BoolT1()) + simplifier(intValInNat) shouldBe tla.ge(intVal, tla.int(0)).as(BoolT1()) + expressions.foreach { case (name, value, set) => val inputName = tla.in(name, set).as(BoolT1()) simplifier(inputName) shouldBe tlaTrue @@ -72,11 +77,6 @@ class TestSetMembershipSimplifier val nestedInputValue = tla.and(tla.in(name, set).as(BoolT1()), tlaTrue).as(BoolT1()) simplifier(nestedInputValue) shouldBe tla.and(tlaTrue, tlaTrue).as(BoolT1()) - - val intNameInNat = tla.in(intName, tla.natSet()).as(BoolT1()) - val intValInNat = tla.in(intVal, tla.natSet()).as(BoolT1()) - simplifier(intNameInNat) shouldBe tla.ge(intName, tla.int(0)).as(BoolT1()) - simplifier(intValInNat) shouldBe tla.ge(intVal, tla.int(0)).as(BoolT1()) } } From 0867f1ed056d87b8fb93138296b1e36e666eaa44 Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Mon, 7 Mar 2022 10:05:42 +0100 Subject: [PATCH 4/7] Support simplifying SUBSET --- .../tla/pp/SetMembershipSimplifier.scala | 13 +++-- .../tla/pp/TestSetMembershipSimplifier.scala | 51 +++++++++++++++++++ 2 files changed, 60 insertions(+), 4 deletions(-) diff --git a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/SetMembershipSimplifier.scala b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/SetMembershipSimplifier.scala index 99802b023d..35a08da83b 100644 --- a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/SetMembershipSimplifier.scala +++ b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/SetMembershipSimplifier.scala @@ -16,6 +16,7 @@ import at.forsyte.apalache.tla.lir.values._ * - `n \in Nat` ~> `x >= 0` * - `b \in BOOLEAN`, `i \in Int`, `r \in Real` ~> `TRUE` * - `seq \in Seq(_)` ~> `TRUE` + * - `set \in SUBSET S` ~> `TRUE` * * @author * Thomas Pani @@ -38,17 +39,21 @@ class SetMembershipSimplifier(tracker: TransformationTracker) extends AbstractTr * * The applicable sets are inductively defined as * - the predefined sets BOOLEAN, Int, Real, STRING, - * - sets of sequences over applicable sets, e.g., Seq(BOOLEAN), Seq(Int), Seq(Seq(Int)), ... + * - sets of sequences over applicable sets, e.g., Seq(BOOLEAN), Seq(Int), Seq(Seq(Int)), Seq(SUBSET Int), ... + * - power sets of applicable sets, e.g., SUBSET BOOLEAN, SUBSET Int, SUBSET Seq(Int), ... * - * In particular, it is *not* applicable to `Nat` and sequence sets, since `i \in Nat` does not hold for all - * `IntT1`-typed `i`. + * In particular, it is *not* applicable to `Nat` and sequence sets / power sets thereof, since `i \in Nat` does not + * hold for all `IntT1`-typed `i`. */ private def isApplicable: Function[TlaEx, Boolean] = { // base case: BOOLEAN, Int, Real, STRING case ValEx(TlaBoolSet) | ValEx(TlaIntSet) | ValEx(TlaRealSet) | ValEx(TlaStrSet) => true - // inductive case: Seq(s) for applicable set `s` + // inductive cases: + // 1. Seq(s) for applicable set `s` case OperEx(TlaSetOper.seqSet, set) => isApplicable(set) + // 2. SUBSET s for applicable set `s` + case OperEx(TlaSetOper.powerset, set) => isApplicable(set) // otherwise case _ => false diff --git a/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestSetMembershipSimplifier.scala b/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestSetMembershipSimplifier.scala index c17812fbb5..c6d240ccfb 100644 --- a/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestSetMembershipSimplifier.scala +++ b/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestSetMembershipSimplifier.scala @@ -46,6 +46,19 @@ class TestSetMembershipSimplifier private val intSeqSet = tla.seqSet(tla.intSet()).as(SetT1(SeqT1(IntT1()))) private val natSeqSet = tla.seqSet(tla.natSet()).as(SetT1(SeqT1(IntT1()))) + private val boolSetVal = tla.enumSet(boolVal, boolName).as(SetT1(BoolT1())) + private val strSetVal = tla.enumSet(strVal, strName).as(SetT1(StrT1())) + private val intSetVal = tla.enumSet(intVal, intName).as(SetT1(IntT1())) + + private val boolSetName = tla.name("boolSet").as(SetT1(BoolT1())) + private val strSetName = tla.name("strSet").as(SetT1(StrT1())) + private val intSetName = tla.name("intSet").as(SetT1(IntT1())) + + private val boolPowerset = tla.seqSet(tla.booleanSet()).as(SetT1(SeqT1(BoolT1()))) + private val strPowerset = tla.seqSet(tla.stringSet()).as(SetT1(SeqT1(StrT1()))) + private val intPowerset = tla.seqSet(tla.intSet()).as(SetT1(SeqT1(IntT1()))) + private val natPowerset = tla.seqSet(tla.natSet()).as(SetT1(SeqT1(IntT1()))) + val expressions = List( (boolName, boolVal, boolSet), (strName, strVal, strSet), @@ -53,6 +66,9 @@ class TestSetMembershipSimplifier (boolSeqName, boolSeqVal, boolSeqSet), (strSeqName, strSeqVal, strSeqSet), (intSeqName, intSeqVal, intSeqSet), + (boolSetName, boolSetVal, boolPowerset), + (strSetName, strSetVal, strPowerset), + (intSetName, intSetVal, intPowerset), ) override def beforeEach(): Unit = { @@ -60,24 +76,54 @@ class TestSetMembershipSimplifier } test("simplifies appropriately-typed set membership") { + // i \in Nat ~> i >= 0 val intNameInNat = tla.in(intName, tla.natSet()).as(BoolT1()) val intValInNat = tla.in(intVal, tla.natSet()).as(BoolT1()) simplifier(intNameInNat) shouldBe tla.ge(intName, tla.int(0)).as(BoolT1()) simplifier(intValInNat) shouldBe tla.ge(intVal, tla.int(0)).as(BoolT1()) + /* *** tests for all supported types of applicable sets *** */ + expressions.foreach { case (name, value, set) => + // name \in ApplicableSet ~> TRUE + // e.g., b \in BOOLEAN, i \in Int, ... ~> TRUE val inputName = tla.in(name, set).as(BoolT1()) simplifier(inputName) shouldBe tlaTrue + // literal \in ApplicableSet ~> TRUE + // e.g., TRUE \in BOOLEAN, 42 \in Int, ... ~> TRUE val inputValue = tla.in(value, set).as(BoolT1()) simplifier(inputValue) shouldBe tlaTrue + /* *** nested cases *** */ + + // name \in ApplicableSet /\ _ ~> TRUE + // e.g., i \in Int /\ _, ... ~> TRUE val nestedInputName = tla.and(tla.in(name, set).as(BoolT1()), tlaTrue).as(BoolT1()) simplifier(nestedInputName) shouldBe tla.and(tlaTrue, tlaTrue).as(BoolT1()) + // literal \in ApplicableSet /\ _ ~> TRUE + // e.g., 42 \in Int /\ _, ... ~> TRUE val nestedInputValue = tla.and(tla.in(name, set).as(BoolT1()), tlaTrue).as(BoolT1()) simplifier(nestedInputValue) shouldBe tla.and(tlaTrue, tlaTrue).as(BoolT1()) } + + /* *** tests of particular expressions *** */ + + // <<{{1}}>> \in Seq(SUBSET Int) ~> TRUE + val setOfSetOfInt = SetT1(SetT1(IntT1())) + val seqOfSetOfSetOfInt = SeqT1(setOfSetOfInt) + val nestedSeqSubsetVal = + tla.tuple(tla.enumSet(intSetVal).as(setOfSetOfInt)).as(SeqT1(setOfSetOfInt)).as(seqOfSetOfSetOfInt) + val nestedSeqSubsetTest = + tla.in(nestedSeqSubsetVal, tla.seqSet(tla.powSet(intSet).as(setOfSetOfInt)).as(seqOfSetOfSetOfInt)).as(BoolT1()) + simplifier(nestedSeqSubsetTest) shouldBe tlaTrue + + // {<<1>>} \in SUBSET (Seq(Int)) ~> TRUE + val setOfSeqOfInt = SetT1(SeqT1(IntT1())) + val nestedSubsetSeqVal = tla.enumSet(tla.tuple(intVal).as(SeqT1(IntT1()))).as(setOfSeqOfInt) + val nestedSubsetSeqTest = tla.in(nestedSubsetSeqVal, tla.powSet(intSeqSet).as(setOfSeqOfInt)).as(BoolT1()) + simplifier(nestedSubsetSeqTest) shouldBe tlaTrue } test("returns myInt \\in Nat unchanged") { @@ -85,5 +131,10 @@ class TestSetMembershipSimplifier val intSeqValInSeqNat = tla.in(intSeqVal, natSeqSet).as(BoolT1()) simplifier(intSeqNameInSeqNat) shouldBe intSeqNameInSeqNat simplifier(intSeqValInSeqNat) shouldBe intSeqValInSeqNat + + val intSetNameInNatPowerset = tla.in(intSetName, natPowerset).as(BoolT1()) + val intSetValInNatPowerset = tla.in(intSetVal, natPowerset).as(BoolT1()) + simplifier(intSetNameInNatPowerset) shouldBe intSetNameInNatPowerset + simplifier(intSetValInNatPowerset) shouldBe intSetValInNatPowerset } } From 673f6bc8dafd388dec8ae791645e41cb8afeebdf Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Mon, 7 Mar 2022 10:22:27 +0100 Subject: [PATCH 5/7] Support simplifying sets of functions [AS1 -> AS2] --- .../tla/pp/SetMembershipSimplifier.scala | 19 +++++++++++--- .../tla/pp/TestSetMembershipSimplifier.scala | 26 +++++++++++++++++++ 2 files changed, 41 insertions(+), 4 deletions(-) diff --git a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/SetMembershipSimplifier.scala b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/SetMembershipSimplifier.scala index 35a08da83b..7f25fb287d 100644 --- a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/SetMembershipSimplifier.scala +++ b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/SetMembershipSimplifier.scala @@ -12,11 +12,13 @@ import at.forsyte.apalache.tla.lir.values._ * 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: + * We currently perform the following simplifications (for applicable sets AS, see [[isApplicable]]): * - `n \in Nat` ~> `x >= 0` * - `b \in BOOLEAN`, `i \in Int`, `r \in Real` ~> `TRUE` - * - `seq \in Seq(_)` ~> `TRUE` - * - `set \in SUBSET S` ~> `TRUE` + * - `seq \in Seq(AS)` ~> `TRUE` + * - `set \in SUBSET AS` ~> `TRUE` + * - `fun \in [AS1 -> AS2]` ~> `TRUE` + * - `fun \in [Dom -> AS]` ~> `DOMAIN fun = Dom` * * @author * Thomas Pani @@ -41,6 +43,7 @@ class SetMembershipSimplifier(tracker: TransformationTracker) extends AbstractTr * - the predefined sets BOOLEAN, Int, Real, STRING, * - sets of sequences over applicable sets, e.g., Seq(BOOLEAN), Seq(Int), Seq(Seq(Int)), Seq(SUBSET Int), ... * - power sets of applicable sets, e.g., SUBSET BOOLEAN, SUBSET Int, SUBSET Seq(Int), ... + * - sets of functions over applicable sets, e.g., [Int -> BOOLEAN], ... * * In particular, it is *not* applicable to `Nat` and sequence sets / power sets thereof, since `i \in Nat` does not * hold for all `IntT1`-typed `i`. @@ -54,6 +57,8 @@ class SetMembershipSimplifier(tracker: TransformationTracker) extends AbstractTr case OperEx(TlaSetOper.seqSet, set) => isApplicable(set) // 2. SUBSET s for applicable set `s` case OperEx(TlaSetOper.powerset, set) => isApplicable(set) + // 3. [s1 -> s2] for applicable sets `s1` and `s2 + case OperEx(TlaSetOper.funSet, set1, set2) => isApplicable(set1) && isApplicable(set2) // otherwise case _ => false @@ -70,9 +75,15 @@ class SetMembershipSimplifier(tracker: TransformationTracker) extends AbstractTr case OperEx(TlaSetOper.in, name, ValEx(TlaNatSet)) => OperEx(TlaArithOper.ge, name, ValEx(TlaInt(0))(intTag))(boolTag) - // x \in AS ~> TRUE for applicable sets AS (see `isApplicable`): + /* For ApplicableSets AS (see `isApplicable`): */ + + // x \in AS ~> TRUE case OperEx(TlaSetOper.in, _, set) if isApplicable(set) => trueVal + // fun \in [Dom -> AS] ~> DOMAIN fun = Dom (fun \in [AS1 -> AS2] is handled above) + case OperEx(TlaSetOper.in, fun, OperEx(TlaSetOper.funSet, domain, set2)) if isApplicable(set2) => + OperEx(TlaOper.eq, OperEx(TlaFunOper.domain, fun)(domain.typeTag), domain)(boolTag) + // otherwise, return `ex` unchanged case ex => ex } diff --git a/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestSetMembershipSimplifier.scala b/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestSetMembershipSimplifier.scala index c6d240ccfb..299836f6e3 100644 --- a/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestSetMembershipSimplifier.scala +++ b/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestSetMembershipSimplifier.scala @@ -28,6 +28,7 @@ class TestSetMembershipSimplifier private val boolName = tla.name("b").as(BoolT1()) private val strName = tla.name("s").as(StrT1()) private val intName = tla.name("i").as(IntT1()) + private val funName = tla.name("fun").as(FunT1(IntT1(), BoolT1())) private val boolSet = tla.booleanSet().as(SetT1(BoolT1())) private val strSet = tla.stringSet().as(SetT1(StrT1())) @@ -106,6 +107,13 @@ class TestSetMembershipSimplifier // e.g., 42 \in Int /\ _, ... ~> TRUE val nestedInputValue = tla.and(tla.in(name, set).as(BoolT1()), tlaTrue).as(BoolT1()) simplifier(nestedInputValue) shouldBe tla.and(tlaTrue, tlaTrue).as(BoolT1()) + + // fun \in [ApplicableSet1 -> ApplicableSet2], ... ~> TRUE + expressions.foreach { case (name2, _, set2) => + val funSetType = SetT1(FunT1(name.typeTag.asTlaType1(), name2.typeTag.asTlaType1())) + val funInFunSet = tla.in(funName, tla.funSet(set, set2).as(funSetType)).as(BoolT1()) + simplifier(funInFunSet) shouldBe tlaTrue + } } /* *** tests of particular expressions *** */ @@ -124,6 +132,24 @@ class TestSetMembershipSimplifier val nestedSubsetSeqVal = tla.enumSet(tla.tuple(intVal).as(SeqT1(IntT1()))).as(setOfSeqOfInt) val nestedSubsetSeqTest = tla.in(nestedSubsetSeqVal, tla.powSet(intSeqSet).as(setOfSeqOfInt)).as(BoolT1()) simplifier(nestedSubsetSeqTest) shouldBe tlaTrue + + // fun \in [Seq(SUBSET Int) -> SUBSET Seq(BOOLEAN)], ... ~> TRUE + val intPowersetSeqType = SeqT1(SetT1(IntT1())) + val boolSeqPowersetType = SetT1(SeqT1(BoolT1())) + val nestedFunSetType = SetT1(FunT1(intPowersetSeqType, boolSeqPowersetType)) + val nestedInput = tla + .in(funName, + tla + .funSet(tla.seqSet(intSeqSet).as(intPowersetSeqType), tla.powSet(boolSeqSet).as(boolSeqPowersetType)) + .as(nestedFunSetType)) + .as(BoolT1()) + simplifier(nestedInput) shouldBe tlaTrue + + // fun \in [RM -> PredefSet], ... ~> DOMAIN fun = RM + val domain = tla.name("RM").as(SetT1(IntT1())) + val funSetType = SetT1(FunT1(BoolT1(), IntT1())) + val funConstToBoolean = tla.in(funName, tla.funSet(domain, boolSet).as(funSetType)).as(BoolT1()) + simplifier(funConstToBoolean) shouldBe tla.eql(tla.dom(funName).as(SetT1(IntT1())), domain).as(BoolT1()) } test("returns myInt \\in Nat unchanged") { From 372742d200afe0b2e4b406f82b93e26a597e6d21 Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Mon, 7 Mar 2022 12:31:00 +0100 Subject: [PATCH 6/7] Replace "applicable" with "type-defining" --- .../tla/pp/SetMembershipSimplifier.scala | 48 +++++++++---------- 1 file changed, 24 insertions(+), 24 deletions(-) diff --git a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/SetMembershipSimplifier.scala b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/SetMembershipSimplifier.scala index 7f25fb287d..47194ce486 100644 --- a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/SetMembershipSimplifier.scala +++ b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/SetMembershipSimplifier.scala @@ -12,13 +12,13 @@ import at.forsyte.apalache.tla.lir.values._ * 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 applicable sets AS, see [[isApplicable]]): + * 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(AS)` ~> `TRUE` - * - `set \in SUBSET AS` ~> `TRUE` - * - `fun \in [AS1 -> AS2]` ~> `TRUE` - * - `fun \in [Dom -> AS]` ~> `DOMAIN fun = Dom` + * - `seq \in Seq(TDS)` ~> `TRUE` + * - `set \in SUBSET TDS` ~> `TRUE` + * - `fun \in [TDS1 -> TDS2]` ~> `TRUE` + * - `fun \in [Dom -> TDS]` ~> `DOMAIN fun = Dom` * * @author * Thomas Pani @@ -36,29 +36,29 @@ class SetMembershipSimplifier(tracker: TransformationTracker) extends AbstractTr } /** - * Returns true iff rewriting of a well-typed set-membership test `x \in arg` to `TRUE` is applicable for the - * function's argument. + * 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 applicable sets are inductively defined as + * The type-defining sets are inductively defined as * - the predefined sets BOOLEAN, Int, Real, STRING, - * - sets of sequences over applicable sets, e.g., Seq(BOOLEAN), Seq(Int), Seq(Seq(Int)), Seq(SUBSET Int), ... - * - power sets of applicable sets, e.g., SUBSET BOOLEAN, SUBSET Int, SUBSET Seq(Int), ... - * - sets of functions over applicable sets, e.g., [Int -> BOOLEAN], ... + * - 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], ... * - * In particular, it is *not* applicable to `Nat` and sequence sets / power sets thereof, since `i \in Nat` does not + * 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 isApplicable: Function[TlaEx, Boolean] = { + private def isTypeDefining: Function[TlaEx, Boolean] = { // base case: BOOLEAN, Int, Real, STRING case ValEx(TlaBoolSet) | ValEx(TlaIntSet) | ValEx(TlaRealSet) | ValEx(TlaStrSet) => true // inductive cases: - // 1. Seq(s) for applicable set `s` - case OperEx(TlaSetOper.seqSet, set) => isApplicable(set) - // 2. SUBSET s for applicable set `s` - case OperEx(TlaSetOper.powerset, set) => isApplicable(set) - // 3. [s1 -> s2] for applicable sets `s1` and `s2 - case OperEx(TlaSetOper.funSet, set1, set2) => isApplicable(set1) && isApplicable(set2) + // 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) // otherwise case _ => false @@ -75,13 +75,13 @@ class SetMembershipSimplifier(tracker: TransformationTracker) extends AbstractTr case OperEx(TlaSetOper.in, name, ValEx(TlaNatSet)) => OperEx(TlaArithOper.ge, name, ValEx(TlaInt(0))(intTag))(boolTag) - /* For ApplicableSets AS (see `isApplicable`): */ + /* For type-defining sets TDS (see [[isTypeDefining]]): */ - // x \in AS ~> TRUE - case OperEx(TlaSetOper.in, _, set) if isApplicable(set) => trueVal + // x \in TDS ~> TRUE + case OperEx(TlaSetOper.in, _, set) if isTypeDefining(set) => trueVal - // fun \in [Dom -> AS] ~> DOMAIN fun = Dom (fun \in [AS1 -> AS2] is handled above) - case OperEx(TlaSetOper.in, fun, OperEx(TlaSetOper.funSet, domain, set2)) if isApplicable(set2) => + // fun \in [Dom -> TDS] ~> DOMAIN fun = Dom (fun \in [TDS1 -> TDS2] is handled above) + case OperEx(TlaSetOper.in, fun, OperEx(TlaSetOper.funSet, domain, set2)) if isTypeDefining(set2) => OperEx(TlaOper.eq, OperEx(TlaFunOper.domain, fun)(domain.typeTag), domain)(boolTag) // otherwise, return `ex` unchanged From 9387f0937111e7c2e63b83531c3aea090ed1dec2 Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Mon, 7 Mar 2022 12:47:59 +0100 Subject: [PATCH 7/7] Refactor matcher --- .../tla/pp/SetMembershipSimplifier.scala | 24 ++++++++++--------- 1 file changed, 13 insertions(+), 11 deletions(-) diff --git a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/SetMembershipSimplifier.scala b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/SetMembershipSimplifier.scala index 47194ce486..771b6a0570 100644 --- a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/SetMembershipSimplifier.scala +++ b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/SetMembershipSimplifier.scala @@ -71,20 +71,22 @@ class SetMembershipSimplifier(tracker: TransformationTracker) extends AbstractTr * [[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)) => - OperEx(TlaArithOper.ge, name, ValEx(TlaInt(0))(intTag))(boolTag) + case ex @ OperEx(TlaSetOper.in, name, set) => + set match { + // x \in TDS ~> TRUE + case set if isTypeDefining(set) => trueVal - /* For type-defining sets TDS (see [[isTypeDefining]]): */ + // n \in Nat ~> x >= 0 + case ValEx(TlaNatSet) => OperEx(TlaArithOper.ge, name, ValEx(TlaInt(0))(intTag))(boolTag) - // x \in TDS ~> TRUE - case OperEx(TlaSetOper.in, _, set) if isTypeDefining(set) => trueVal + // 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) - // fun \in [Dom -> TDS] ~> DOMAIN fun = Dom (fun \in [TDS1 -> TDS2] is handled above) - case OperEx(TlaSetOper.in, fun, OperEx(TlaSetOper.funSet, domain, set2)) if isTypeDefining(set2) => - OperEx(TlaOper.eq, OperEx(TlaFunOper.domain, fun)(domain.typeTag), domain)(boolTag) - - // otherwise, return `ex` unchanged + // otherwise, return `ex` unchanged + case _ => ex + } + // return non-set membership expressions unchanged case ex => ex } }