Merge pull request #1450 from informalsystems/ik/funAsSeq2

adding length to FunAsSeq

docs/src/lang/apalache-operators.md

@@ -175,49 +175,59 @@ MkSeq(3, Double) = <<2, 4, 6>>   \* TRUE
 
 ## Interpret a function as a sequence
 
-**Notation:** `FunAsSeq(fn, maxLen)`
+**Notation:** `FunAsSeq(fn, len, maxLen)`
 
-**LaTeX notation:** `FunAsSeq(fn, maxLen)`
+**LaTeX notation:** `FunAsSeq(fn, len, maxLen)`
 
-**Arguments:** Two arguments. The first is a function, the second is an integer.
+**Arguments:** Three arguments:
 
-**Apalache type:** `(Int -> a, Int) => Seq(a)`, for some type `a`
+* A function `fn` that should be interpreted as a sequence.
+* An integer `len`, denoting the length of the sequence, with the property
+  `1..len \subseteq DOMAIN fn`. Apalache does not check this requirement. It is up to the user to ensure that it holds. This expression is not necessarily constant.
+* An integer constant `maxLen`, which is an upper bound on `len`, that is, `len <= maxLen`.
 
-**Effect:** The expression `FunAsSeq(fn, maxLen)` evaluates to the sequence `<< fn[1], ..., fn[maxLen] >>`.
-At the level of Apalache static analysis, `FunAsSeq` indicates type-casting a function type `Int -> a` to a sequence type `Seq(a)`, since one cannot use function constructors to define a sequence in Apalache otherwise.
+**Apalache type:** `(Int -> a, Int, Int) => Seq(a)`, for some type `a`
+
+**Effect:** The expression `FunAsSeq(fn, len, maxLen)` evaluates to the
+sequence `<< fn[1], ..., fn[Min(len, maxLen)] >>`.
 
 **Determinism:** Deterministic.
 
-**Errors:** 
-If `fn` is not a function of the type `Int -> a` or if `maxLen` is not an integer, Apalache statically reports a type error. Additionally, if it is not the case that `1..maxLen \subseteq DOMAIN fn`, the result is undefined.
+**Errors:** If the types of `fn`, `len` or `maxLen` do not match the expected types, Apalache statically reports a
+type error. Additionally, if it is not the case that `1..len \subseteq DOMAIN fn`, the result is undefined.
 
 **Example in TLA+:**
 
 ```tla
-Head( [ x \in 1..5 |-> x * x ] )                \* 1 in TLC, type error in Apalache
-FunAsSeq( [ x \in 1..5 |-> x * x ], 3 )         \* <<1,4,9>>
-Head( FunAsSeq( [ x \in 1..5 |-> x * x ], 3 ) ) \* 1
-FunAsSeq( <<1,2,3>>, 3 )                        \* <<1,2,3>> in TLC, type error in Apalache
-FunAsSeq( [ x \in {0,42} |-> x * x ], 3 )       \* UNDEFINED
+Head([ x \in 1..5 |-> x * x ])                \* 1 in TLC, type error in Apalache
+FunAsSeq([ x \in 1..5 |-> x * x ], 3, 3)      \* <<1,4,9>>
+Head(FunAsSeq([ x \in 1..5 |-> x * x ], 3, 3)) \* 1
+FunAsSeq(<<1,2,3>>, 3, 3)                     \* <<1,2,3>> in TLC, type error in Apalache
+FunAsSeq([ x \in {0,42} |-> x * x ], 3, 3)    \* UNDEFINED
 ```
 
 **Example in Python:**
 
 ```python
-def funAsSeq(f,imax):
-  # f === { x:f(x) | x \in Dom(f) }
-  return[f.get(i) for i in range(1,imax+1)]
+# define a TLA+-like dictionary via a python function
 def boundedFn(f, dom):
-  return { x:f(x) for x in dom } 
-f = boundedFn( lambda x: x*x, range(1,6) ) # [ x \in 1..5 |-> x * x ]
-g = boundedFn( lambda x: x*x, {0,42} )     # [ x \in {0,42} |-> x * x ]
->>> f[1]                                   # Head( [ x \in 1..5 |-> x * x ] )  
+  return { x: f(x) for x in dom }
+
+# this is how we could define funAsSeq in python
+def funAsSeq(f, length, maxLen):
+  return [ f.get(i) for i in range(1, min(length, maxLen) + 1) ]
+
+# TLA+: [ x \in 1..5 |-> x * x ]
+f = boundedFn(lambda x: x * x, range(1,6))
+# TLA+: [ x \in {0, 42} |-> x * x ]
+g = boundedFn(lambda x: x * x, {0, 42})
+>>> f[1]
 1
->>> funAsSeq(f, 3)                         # FunAsSeq( [ x \in 1..5 |-> x * x ], 3 ) 
-[1,4,9]
->>> funAsSeq(f, 3)[1]                      # Head( FunAsSeq( [ x \in 1..5 |-> x * x ], 3 ) )
+>>> funAsSeq(f, 3, 3)
+[1, 4, 9]
+>>> funAsSeq(f, 3, 3)[1]
 1
->>> funAsSeq( g, 3 )                       # FunAsSeq( [ x \in {0,42} |-> x * x ], 3 )
+>>> funAsSeq(g, 3, 3)
 [None, None, None]
 ```
 

src/tla/Apalache.tla

@@ -66,16 +66,26 @@ MkSeq(N, F(_)) ==
     \* This is the TLC implementation. Apalache does it differently.
     [ i \in (1..N) |-> F(i) ]
 
+\* required by our default definition of FoldSeq and FunAsSeq
+LOCAL INSTANCE Sequences
+
 (**
  * As TLA+ is untyped, one can use function- and sequence-specific operators
  * interchangeably. However, to maintain correctness w.r.t. our type-system,
  * an explicit cast is needed when using functions as sequences.
  *
- * @type: ((Int -> a), Int) => Seq(a);
+ * The parameters have the following meaning:
+ *
+ *  - fn is the function from 1..len that should be interpreted as a sequence.
+ *  - len is the length of the sequence, len = Cardinality(DOMAIN fn),
+ *    len may be a variable, a computable expression, etc.
+ *  - capacity is a static upper bound on the length, that is, len <= capacity.
+ *
+ * @type: ((Int -> a), Int, Int) => Seq(a);
  *)
-FunAsSeq(fn, maxSeqLen) ==
+FunAsSeq(fn, len, capacity) ==
     LET __FunAsSeq_elem_ctor(i) == fn[i] IN
-    MkSeq(maxSeqLen, __FunAsSeq_elem_ctor)
+    SubSeq(MkSeq(capacity, __FunAsSeq_elem_ctor), 1, len)
 
 (**
  * Annotating an expression \E x \in S: P as Skolemizable. That is, it can
@@ -112,9 +122,6 @@ FoldSet( Op(_,_), v, S ) == IF S = {}
                                   IN LET T == S \ {w}
                                       IN FoldSet( Op, Op(v,w), T )
 
-\* required by our default definition of FoldSeq
-LOCAL INSTANCE Sequences
-
 (**
  * The folding operator, used to implement computation over a sequence.
  * Apalache implements a more efficient encoding than the one below.

test/tla/MC_QueensTyped.tla

@@ -0,0 +1,12 @@
+---------------------------- MODULE MC_QueensTyped ----------------------------
+\* an instance of QueensTyped for model checking.
+N == 4
+
+VARIABLES
+    \* @type: Set(Seq(Int));
+    todo,
+    \* @type: Set(Seq(Int));
+    sols
+
+INSTANCE QueensTyped
+===============================================================================

test/tla/MegaSpec1.tla

@@ -147,5 +147,5 @@ RealDiv(x, y) == x / y
 
 \* Apalache
 \* @type: (Int -> Str) => Seq(Str);
-Fas(f) == FunAsSeq(f, 3)
-===============================================================================
+Fas(f) == FunAsSeq(f, 3, 3)
+===============================================================================

test/tla/QueensTyped.tla

@@ -44,10 +44,10 @@ IsSolution(queens) ==
 \* We apply Apalache!FunAsSeq to convert a function to a sequence.
 Solutions ==
     LET Queens == { queens \in [1..N -> 1..N] :
-                    IsSolution(FunAsSeq(queens, N)) } IN
+                    IsSolution(FunAsSeq(queens, N, N)) } IN
     \* We have to apply FunAsSeq twice, as queens is used as a sequence twice.
     \* A better approach would be to refactor the spec, to call FunAsSeq once.
-    { FunAsSeq(queens, N): queens \in Queens }
+    { FunAsSeq(queens, N, N): queens \in Queens }
 
 (***************************************************************************)
 (* We now describe an algorithm that iteratively computes the set of       *)

test/tla/TestSequences.tla

@@ -178,14 +178,19 @@ TestFoldSeqOverSelectSeq ==
 
 TestFunAsSeq3 ==
     LET f == [ i \in 1..3 |-> i + 1 ] IN
-    FunAsSeq(f, 3) = <<2, 3, 4>>
+    FunAsSeq(f, 3, 3) = <<2, 3, 4>>
 
 TestFunAsSeqEmpty ==
     LET
         \* @type: Int -> Int;
         f == [ i \in {} |-> i ]
     IN
-    FunAsSeq(f, 0) = << >>
+    FunAsSeq(f, 0, 0) = << >>
+
+TestFunAsSeqLargerCapacity ==
+    LET f == [ i \in 1..3 |-> i + 1 ] IN
+    \* provide a larger upper bound
+    FunAsSeq(f, 3, 10) = <<2, 3, 4>>
 
 TestExceptLen ==
     Len([seq345 EXCEPT ![2] = 10]) = 3
@@ -235,6 +240,7 @@ AllTests ==
     /\ TestMkSeqFold
     /\ TestFunAsSeq3
     /\ TestFunAsSeqEmpty
+    /\ TestFunAsSeqLargerCapacity
     /\ TestExceptLen
     /\ TestExceptDomain
 ===============================================================================

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

@@ -10,7 +10,7 @@ import at.forsyte.apalache.tla.lir.oper.ApalacheOper
 import at.forsyte.apalache.tla.lir.storage.BodyMapFactory
 import at.forsyte.apalache.tla.lir.transformations.impl.IdleTracker
 import at.forsyte.apalache.tla.lir.values.TlaInt
-import at.forsyte.apalache.tla.pp.{ConstSimplifier, InlinerOfUserOper, TlaInputError}
+import at.forsyte.apalache.tla.pp.{InlinerOfUserOper, TlaInputError}
 
 /**
  * Rewriting rule for MkSeq. This rule is similar to [[FoldSeqRule]].
@@ -20,7 +20,6 @@ import at.forsyte.apalache.tla.pp.{ConstSimplifier, InlinerOfUserOper, TlaInputE
  */
 class MkSeqRule(rewriter: SymbStateRewriter) extends RewritingRule {
   private val proto = new ProtoSeqOps(rewriter)
-  private val simplifier = new ConstSimplifier(new IdleTracker())
 
   override def isApplicable(symbState: SymbState): Boolean = symbState.ex match {
     // match the internal representation of lambda expressions or embedded calls
@@ -71,7 +70,7 @@ class MkSeqRule(rewriter: SymbStateRewriter) extends RewritingRule {
 
   // extract capacity from the length expression
   private def extractCapacity(lenEx: TlaEx): Int = {
-    simplifier(lenEx) match {
+    lenEx match {
       case ValEx(TlaInt(n)) if n.isValidInt && n >= 0 =>
         n.toInt
 

tla-types/src/test/resources/MegaSpec1.tla

@@ -162,5 +162,5 @@ RealDiv(x, y) == x / y
 
 \* Apalache
 \* @type: (Int -> Str) => Seq(Str);
-Fas(f) == FunAsSeq(f, 3)
+Fas(f) == FunAsSeq(f, 3, 3)
 ===============================================================================