StringFilter

Functions for removing elements of a string by a predicate on char.

Signature of StringFilter

List of Import References :
See BOOL
See Char
See DENOTATION
See Nat
See Option
See Seq
See String

SIGNATURE StringFilter

$Date: 2010-09-30 18:24:17 +0200 (Do, 30. Sep 2010) $ ($Revision: 616 $)

IMPORT String ONLY string
       Char   ONLY char
       Seq[string] ONLY seq

                -- p | s

filter: p | s selects all elements of s fulfilling predicate p without changing the order.

FUN |           : (char -> bool) ** string -> string    

partition (p, s) = (p | s, (\\x. ~(p(x))) | s)

FUN partition   : (char -> bool) ** string -> string ** string

take: take (p, s) takes all components of s (from left to right) fulfilling predicate p just upto the first component, which does not fulfill p.

FUN take        : (char -> bool) ** string -> string    

drop: drop(p, s) drops all components of s (from left to right) fulfilling predicate p just upto the first component, which does not fulfill p.

FUN drop        : (char -> bool) ** string -> string    
                

split: split (p, s) = (take (p,s), drop (p, s)). Split s before the first component (operating from left to right) which does not fulfill predicate p.

FUN split       : (char -> bool) ** string -> string ** string  

split: split(p, s1 ++ P ++ s2 ++ ... ++ P ++ sn) = <s1, s2, ..., sn>, where P is some character fulfilling p. Split s at characters (separators) which fulfill p. These separators are not part of the strings si.

FUN split   : (char -> bool) ** string -> seq[string]

components(~)(s) = s0 :: s1 :: ... :: sn. s = s0 ++ s1 ++ ..., all elements of si are related by ~, and the last element of si is not related by ~ with si+1

FUN components: (char ** char -> bool) -> string -> seq[string]

next node: StringFold,
prev node: String,
up to node: Subsystem Strings