Séquences

TYPE sequence{t: type}
  INHERIT equality{sequence{t}}
  INHERIT total_order{sequence{t}}
  IMPORT Subtype FROM type
  EXPORT prefix suffix sorted distinct permutation frequency
    -- Generated by {empty, add}.

  MESSAGE empty
    -- Literal [ ] = empty.
    REPLY(s: sequence{t})

  MESSAGE add(x: t, s1: sequence{t})
    -- Literal [x] = add(x, empty).
    -- Literal [x, $s] = add(x, s).
    REPLY(s2: sequence{t})

  MESSAGE remove(x: t, s1: sequence{t})
    -- Remove all instances of x from s.
    REPLY(s2: sequence{t})
    WHERE ALL(x: t :: remove(x, empty) = empty),
      ALL(x: t, s: sequence{t} ::
          remove(x, add(x, s)) = remove(x, s) ),
      ALL(x y: t, s: sequence{t} SUCH THAT x ~= y
          :: remove(x, add(y, s)) = add(y, remove(x, s)) )

  MESSAGE "||"(s1 s2: sequence{t})  -- Concatenation.
    -- Literal [$s1, $s2] = s1 || s2.
    REPLY(s2: sequence{t})
    WHERE ALL(s: sequence{t} :: empty || s = s),
      ALL(x: t, s1 s2: sequence{t} ::
          add(x, s1) || s2 = add(x, s1 || s2) )

  MESSAGE "["(s: sequence{t}, n: nat)
    -- Indexing, "["(a, b) is written a[b].
    WHEN 1 <= n <= length(s)
      REPLY(x: t)
      WHERE ALL(x: t, s: sequence{t} :: add(x, s)[1] = x),
        ALL(n: nat, x: t, s: sequence{t} SUCH THAT n > 1
          :: add(x, s)[n] = s[n - 1] )
    OTHERWISE REPLY EXCEPTION bounds_error

  MESSAGE "["(s1: sequence{t}, s2: sequence{nat})
    -- Indirect indexing.
    -- Subrange is a special case:
    -- s[1 .. 3] is the same as s[[1, 2, 3]].
    WHEN ALL(n: nat SUCH THAT n IN s2 :: n IN domain(s1))
      REPLY(s3: sequence{t})
      WHERE length(s3) = length(s2),
        ALL(n: nat SUCH THAT n IN domain(s2) ::
            s3[n] = s1[s2[n]] )
    OTHERWISE REPLY EXCEPTION bounds_error

  MESSAGE length(s: sequence{t})
    REPLY(n: nat)
    WHERE length(empty) = 0,
      ALL(x: t, s: sequence{t} ::
          length(add(x, s)) = length(s) + 1 )

  MESSAGE domain(s: sequence{t})
    REPLY(d: set{nat})
    WHERE d = {1 .. length(s)}

  MESSAGE "IN"(x: t, s: sequence{t})
    -- "IN"(x, s) is written x IN s.
    REPLY(b: boolean)
    WHERE b <=> SOME(n: nat SUCH THAT n IN domain(s) :: s[n] = x)

  MESSAGE "IN"(s1 s2: sequence{t})
    REPLY(b: boolean)
    WHERE b <=> SOME(x y: sequence{t} :: x || s1 || y = s2)

  MESSAGE equal(s1 s2: sequence{t})
    REPLY(b: boolean)
    WHERE b <=> ALL(n: nat :: s1[n] = s2[n])

  MESSAGE "<"(s1 s2: sequence{t})
    -- Lexicographic ordering (dictionary ordering on strings).
    WHEN Has_operation{t, t, boolean}(t, "<") &
         Partial_ordering("<"@t)
      REPLY(b: boolean)
      WHERE ALL(s: sequence{t}, x: t :: [ ] < [x, $s]),
        ALL(s1 s2: sequence{t}, x1 x2: t
           :: [x1, $s1] < [x2, $s2] <=>
              x1 < x2 | x1 = x2 & s1 < s2 )
    OTHERWISE REPLY EXCEPTION operation_not_applicable

  MESSAGE subsequence(s1 s2: sequence{t})
    REPLY(b: boolean)
    -- True if the elements of s1 are embedded in s2,
    -- in the same order.
    WHERE ALL(s: sequence{t} :: subsequence([ ], s)),
      ALL(s1 s2: sequence{t}, x: t :: subsequence([x, $s1], s2)
              <=> SOME(s3 s4: sequence{t}
                       :: s2 = [$s3, x, $s4] &
                          subsequence(s1, s4) )),
      Partial_ordering(subsequence)

  MESSAGE ".."(x1 x2: t)  -- ".."(x1, x2)" is written [x1 .. x2].
    WHEN Subtype(t, total_order)
      REPLY(s: sequence{t})
      WHERE sorted{"<"@t}(s),
            ALL(x: t :: x IN s <=> x1 <= x <= x2)
    OTHERWISE REPLY EXCEPTION operation_not_applicable

  MESSAGE apply{rt: type}(f: function{t, rt}, s1: sequence{t})
    REPLY(s2: sequence{rt})
    WHERE length(s2) = length(s1),
      ALL(n: nat SUCH THAT n IN domain(s1) :: s2[n] = f(s1[n]))

  MESSAGE reduce{f: function{t, t, t}, identity: t SUCH THAT
                 ALL(y: t :: f(y, identity) = y) }
            (s: sequence{t})
      REPLY(x: t)
      WHERE IF s = [ ] THEN x = identity
            ELSE x = f(s[1], reduce{f}(s[2 .. length(s)])) FI

  MESSAGE reduce1{f: function{t, t, t}} (s: sequence{t})
      WHEN length(s) > 1 REPLY(x: t)
        WHERE x = f(s[1], reduce1{f}(s[2 .. length(s)]))
      WHEN length(s) = 1 REPLY(x: t) WHERE x = s[1]
      OTHERWISE REPLY EXCEPTION empty_reduction_undefined

  MESSAGE scan(s: sequence{t})
    GENERATE(s1: sequence{t}) WHERE s1 = s

  CONCEPT prefix(s1 s2: sequence{t})
    VALUE(b: boolean)
    -- True if s1 is a prefix of s2.
    WHERE b <=> SOME(s: sequence{t} :: s1 || s = s2)

  CONCEPT suffix(s1 s2: sequence{t})
    VALUE(b: boolean)
    -- True if s1 is a suffix of s2.
    WHERE b <=> SOME(s: sequence{t} :: s || s1 = s2)

  CONCEPT sorted{le: function{t, t, boolean} SUCH THAT
                 Total_ordering(le) }
            (s: sequence{t})
    VALUE(b: boolean)
    -- True if s is sorted in nondecreasing order
    -- with respect to le.
    WHERE b <=> ALL(n1 n2: nat SUCH THAT
                    1 <= n1 < n2 <= length(s) ::
                    le(s[n1], s[n2]) )

  CONCEPT distinct(s: sequence{t})
    VALUE(b: boolean)
    -- True if there are no repeated elements in s.
    WHERE b <=> ALL(n1 n2: nat SUCH THAT
                    1 <= n1 < n2 <= length(s) ::
                    s[n1] ~= s[n2] )

  CONCEPT permutation(s1 s2: sequence{t})
    VALUE(b: boolean)
    -- True is s1 is a permutation of s2.
    WHERE b <=> ALL(x: t :: frequency(x, s1) = frequency(x, s2))

  CONCEPT frequency(x: t, s: sequence{t})
    VALUE(n: nat)
    -- The number of times x appears as an element of s.
    WHERE n = NUMBER(k: nat SUCH THAT s[k] = x :: k)
END