SIGNATURE String

-- strings of characters 

-- positions of characters in strings are counted beginning from 0!
-- in informal explanations, string "abcd" is represented as <a,b,c,d>

IMPORT  Nat             ONLY nat
        Char            ONLY char
        Seq[char]       ONLY seq
        Option[char]    ONLY option
        
-- the type itself
TYPE string == <>                               -- empty
            ::(ft:char, rt:string)              -- prepend

 
FUN empty: string
FUN cons:  char ** string -> string
FUN empty? 
    cons?   : string -> bool

-- constructing a string from chars
FUN %   : char ->string                         
    %   : char ** char -> string                        
    %   : char ** char ** char -> string                
    %   : char ** char ** char ** char -> string                
    %   : char ** char ** char ** char ** char -> string
    %   : char ** char ** char ** char ** char ** char -> string
    %   : char ** char ** char ** char ** char ** char ** char -> string
    %   : char ** char ** char ** char ** char ** char ** char ** char -> string

        

FUN ::  : char ** string -> string -- prepend
FUN +%  : string ** char -> string -- append at end

-- constructing a string from a function
FUN ..         : nat ** nat -> (nat -> char) -> string
               -- (n_1 .. n_2)(f) = <f(n1), f(n1 +1), ..., f(n2)>

FUN iter : char ** (char -> char) ** (char -> bool) -> string
                -- iter(start, it, P) == 
                --    <start,  it(start), ... it^n(start)>
                -- where P(it^i(start)) for 0 <= i <= n
                -- and ~(P(it^(n+1)(start)))

-- combining strings
FUN ++  : string ** string -> string    -- concat

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

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

-- working on a string

FUN take        : nat ** string -> string                       
                -- take (k, s)
                -- take first k components of s
                -- informally:
                -- take (k, <e_0, ..., e_k-1, ..., e_n>) = <e_0, ..., e_k-1>
                -- take (k, <e_0, ..., e_k-c>)           = <e_0, ..., e_k-c>
                --	(with c >= 1)

FUN drop        : nat ** string -> string                       
                -- drop (k, s)
                -- drop first k components of s
                -- informally:
                -- drop (k, <e_0, ..., e_k-1, e_k, ..., e_n>) 
                --				= <e_k, ..., e_n>
                -- drop (k, <e_0, ..., e_k-c>)  = <> 
                --	(with c >= 1)

FUN split       : nat ** string -> string ** string             
                -- split (n, s) = (take (n,s), drop (n,s))
                -- split s after n elements

FUN front       : string -> string
                -- front(<e_0, ..., e_n>) = <e_0, ..., e_n-1>

FUN rt          : string -> string
                -- rt(<e_0, ..., e_n>) = <e_1, ..., e_n>

FUN revert      : string -> string
                -- revert(<e_0, ..., e_n>) = <e_n, ... , e_0>

-- accessing chars in a string
FUN ft last     : string -> char   
    
-- information about a string
FUN #   : string -> nat                         -- length

FUN exist?      : (char -> bool) ** string -> bool      
                -- exist? (p, s)
                -- is there any component of s fulfilling p?

FUN find?       : (char -> bool) ** string -> option[char]
                -- find? (p, s)
                -- return some component of s fulfilling p

FUN forall?     : (char -> bool) ** string -> bool
                -- forall? (p, s)
                -- do all components of s fulfill p? 

-- comparing strings
FUN < <= >= >   : string ** string -> bool      
                -- lexicographic orderings

FUN = |=        : string ** string -> bool              
                -- equal, not equal

FUN !           : denotation -> string                  
                -- transforms denotation into string, just as
                -- it is expected

-- old fashioned

FUN init        : nat ** char -> string                 
                -- init (n, c)
                -- generate string of size n and initial characters c
                -- informally:
                -- init (n, c) = 'c...c'
                --		  ^0  ^n-1
                -- init (0, c) = empty

FUN init        : nat ** (nat -> char) -> string        
                -- init (n, f)
                -- generate string of size n and initial char f (i)
                -- where i is a position ranging between 0 and n-1
                -- informally:
                -- init (n, f) = 'f(0)...f(n-1)'

FUN :=          : string ** nat ** char -> string       
                -- := (s, i, c)
                -- update i-th character of string s with value c
                -- where i ranges from 0 upto size of s-1

-- not for user purposes ----------------------------------------------

FUN chunk: nat ** denotation ** string -> string
FUN start: string -> nat
FUN data: string -> denotation
FUN rest: string -> string
FUN asString: denotation -> string