Denotation

More functions on denotations. These functions are modelled after funtions on arrays. Denotations should be used for constant text which is not modified very often; otherwise the usage of tpe string is recommended.

Signature of Denotation

List of Import References :
See BOOL
See Char
See DENOTATION
See Nat

SIGNATURE Denotation

$Date: 2011-09-28 12:04:46 +0200 (Mi, 28. Sep 2011) $ ($Revision: 715 $)

Denotations are a special kind of strings of characters. The characters are counted from position 0 (at the left) to position n-1 at the right, where n is the length of the denotation. If not mentioned otherwise, functions which take an index as argument will abort if the index is not in the range 0 ... n-1.

IMPORT  Nat     ONLY nat
        Char ONLY char

Constructing New Denotations

init (n, c): generate denotation of size n and initial characters c

FUN init        : nat ** char -> denotation

init(n, f): generate denotation of size n and initial data ccode{f(i)}

FUN init        : nat ** (nat -> char) -> denotation

FUN empty       : denotation

Combining Denotations

Concatentation of two denotations.

FUN ++          : denotation ** denotation -> denotation

Concatenate: +/+(d)(d1, d2) concatenate both denotations, put d inbetween, if both are nonempty.

FUN +/+          : char -> denotation ** denotation -> denotation
FUN +/+          : denotation -> denotation ** denotation -> denotation

Concatenate: +%+(d)(d1, d2) concatenate both denotations, put d inbetween unconditionally.

FUN +%+         : char -> denotation ** denotation -> denotation
FUN +%+         : denotation -> denotation ** denotation -> denotation

Working On a Denotation

upd(i, c, d) = (d, i) := c: update ith character of denotation d with value c

FUN :=          : denotation ** nat ** char -> denotation
FUN upd         : nat ** char ** denotation -> denotation

slice (d, i, j): give the slice of denotation d from position i upto j (both inclusive). If i > j return the empty denotation. The function is total: values greater than n-1 are treated as equal to n-1.

FUN slice       : denotation ** nat ** nat -> denotation

delete(d, i, j): delete slice(d, i, j) from a denotation. This function is total.

FUN delete      : denotation ** nat ** nat  -> denotation

insert(d1, i, d2): insert denotation d2 in d1 at position i. If i >= n then insert is equal to concatenation.

FUN insert      : denotation ** nat ** denotation -> denotation

Accessing Chars in a Denotation

Select character at position i in d.

FUN !           : denotation ** nat -> char

Information About a Denotation

Length of denotation d

FUN #           : denotation -> nat

Test for emptyness

FUN empty?      : denotation -> bool

Comparing Denotations

Lexicographic orderings

FUN < <= >= >   : denotation ** denotation -> bool

Equality, Inequality

FUN = |=        : denotation ** denotation -> bool

Compatibility to Former String Type

Make denotation consisting of single character c

FUN %           : char -> denotation

Identity

FUN !           : denotation -> denotation

next node: PrintableChar,
prev node: Char,
up to node: Subsystem Text