% @(#)$Id: string_ops.lsl,v 1.4 1995/01/27 18:56:58 leavens Exp $

% Various useful operations on strings as in C/C++ <string.h>
% Larch/C++ users should use the trait lcpp_string_ops instead of this one.

string_ops(E): trait

  includes String(E, String[E]),
           Sequence(String[E], Seq[String[E]]),
           Set(E, Set[E])

  introduces
    toSet: String[E] -> Set[E]
    anyIn: Set[E], String[E] -> Bool
    firstIndexOf: String[E], E -> Int               % cf. C(++) strchr
    lastIndexOf: String[E], E -> Int                % cf. C(++) strrchr
    tokens: String[E], E -> Seq[String[E]]          % cf. C(++) strtok
    indexOfFirstIn: String[E], Set[E] -> Int        % cf. C(++) strpbrk
    lengthOfPrefixNotFrom: String[E], Set[E] -> Int % cf. C(++) strcspn

  asserts
    \forall s, s1: String[E], s2: Set[E], c: E, i: Int

      toSet(empty) == {};
      toSet(c \precat s) == insert(c, toSet(s));

      ~anyIn({}, s);
      ~anyIn(s2, empty);
      anyIn(insert(c, s2), s1) == (c \in s1) \/ anyIn(s2, s1);

      firstIndexOf(s, c)
         == if not(c \in s)
            then -1
            else if (head(s) = c)
                 then 0
                 else 1 + firstIndexOf(tail(s), c);

      lastIndexOf(s, c)
         == if not(c \in s)
            then -1
            else if (last(s) = c)
                 then len(s) - 1
                 else lastIndexOf(init(s), c);

      tokens(s, c)
         == if not(c \in s)
            then { s }
            else {prefix(s, firstIndexOf(s, c))}
                 || tokens(removePrefix(s, 1 + firstIndexOf(s, c)), c);

      ~anyIn(s2, s1)
         => (indexOfFirstIn(s1, s2) = -1);
      anyIn(s2, s1)
         => (indexOfFirstIn(s1, s2) =
                (if (head(s1) \in s2)
                then 0
                else 1 + indexOfFirstIn(tail(s1), s2)));

      lengthOfPrefixNotFrom(empty, s2) == 0;
      lengthOfPrefixNotFrom(c \precat s1, s2)
         == if (c \in s2)
            then 1
            else 1 + lengthOfPrefixNotFrom(s1, s2);

  implies
    converts toSet, anyIn, firstIndexOf, lastIndexOf, tokens,
             indexOfFirstIn, lengthOfPrefixNotFrom

[Index]

HTML generated using lcpp2html.