mathlib3 documentation

core / init.data.string.basic

structure string_imp :

data : list char

In the VM, strings are implemented using a dynamic array and UTF-8 encoding.

TODO: we currently cannot mark string_imp as private because we need to bind string_imp.mk and string_imp.cases_on in the VM.

Instances for string_imp

string_imp.has_sizeof_inst
string_imp.inhabited

def string :

Equations

string = string_imp

Instances for string

def list.as_string (s : list char) :

Equations

s.as_string = {data := s}

@[protected, instance]

def string.has_lt :

Equations

string.has_lt = {lt := λ (s₁ s₂ : string), s₁.data < s₂.data}

@[protected, instance]

def string.has_decidable_lt (s₁ s₂ : string) :

decidable (s₁ < s₂)

Remark: this function has a VM builtin efficient implementation.

Equations

s₁.has_decidable_lt s₂ = s₁.data.has_decidable_lt s₂.data

@[protected, instance]

def string.has_decidable_eq :

decidable_eq string

Equations

string.has_decidable_eq = λ (_x : string), string.has_decidable_eq._match_3 _x
string.has_decidable_eq._match_3 {data := x} = λ (_x : string), string.has_decidable_eq._match_2 x _x
string.has_decidable_eq._match_2 x {data := y} = string.has_decidable_eq._match_1 x y (list.has_dec_eq x y)
string.has_decidable_eq._match_1 x y (decidable.is_true p) = decidable.is_true _
string.has_decidable_eq._match_1 x y (decidable.is_false p) = decidable.is_false _

def string.empty :

Equations

"" = {data := list.nil char}

def string.length :

Equations

string.length {data := s} = s.length

def string.push :

string → char → string

The internal implementation uses dynamic arrays and will perform destructive updates if the string is not shared.

Equations

string.push {data := s} c = {data := s ++ [c]}

def string.append :

string → string → string

The internal implementation uses dynamic arrays and will perform destructive updates if the string is not shared.

Equations

string.append {data := a} {data := b} = {data := a ++ b}

def string.to_list :

string → list char

O(n) in the VM, where n is the length of the string

Equations

string.to_list {data := s} = s

def string.fold {α : Type u_1} (a : α) (f : α → char → α) (s : string) :

α

Equations

string.fold a f s = list.foldl f a s.to_list

structure string.iterator_imp :

fst : list char
snd : list char

In the VM, the string iterator is implemented as a pointer to the string being iterated + index.

TODO: we currently cannot mark interator_imp as private because we need to bind string_imp.mk and string_imp.cases_on in the VM.

Instances for string.iterator_imp

string.iterator_imp.has_sizeof_inst
string.iterator_imp.inhabited

def string.iterator :

Equations

string.iterator = string.iterator_imp

Instances for string.iterator

string.iterator.inhabited

def string.mk_iterator :

string → string.iterator

Equations

string.mk_iterator {data := s} = {fst := list.nil char, snd := s}

def string.iterator.curr :

string.iterator → char

Equations

string.iterator.curr {fst := p, snd := c :: n} = c
string.iterator.curr {fst := fst, snd := list.nil char} = inhabited.default

def string.iterator.set_curr :

string.iterator → char → string.iterator

In the VM, set_curr is constant time if the string being iterated is not shared and linear time if it is.

Equations

string.iterator.set_curr {fst := p, snd := c :: n} c' = {fst := p, snd := c' :: n}
string.iterator.set_curr {fst := fst, snd := list.nil char} c' = {fst := fst, snd := list.nil char}

def string.iterator.next :

string.iterator → string.iterator

Equations

string.iterator.next {fst := p, snd := c :: n} = {fst := c :: p, snd := n}
string.iterator.next {fst := p, snd := list.nil char} = {fst := p, snd := list.nil char}

def string.iterator.prev :

string.iterator → string.iterator

Equations

string.iterator.prev {fst := c :: p, snd := n} = {fst := p, snd := c :: n}
string.iterator.prev {fst := list.nil char, snd := n} = {fst := list.nil char, snd := n}

def string.iterator.has_next :

string.iterator → bool

Equations

string.iterator.has_next {fst := fst, snd := hd :: tl} = bool.tt
string.iterator.has_next {fst := p, snd := list.nil char} = bool.ff

def string.iterator.has_prev :

string.iterator → bool

Equations

string.iterator.has_prev {fst := hd :: tl, snd := snd} = bool.tt
string.iterator.has_prev {fst := list.nil char, snd := n} = bool.ff

def string.iterator.insert :

string.iterator → string → string.iterator

Equations

string.iterator.insert {fst := p, snd := n} {data := s} = {fst := p, snd := s ++ n}

def string.iterator.remove :

string.iterator → ℕ → string.iterator

Equations

string.iterator.remove {fst := p, snd := n} m = {fst := p, snd := list.drop m n}

def string.iterator.to_string :

string.iterator → string

In the VM, to_string is a constant time operation.

Equations

string.iterator.to_string {fst := p, snd := n} = {data := p.reverse ++ n}

def string.iterator.to_end :

string.iterator → string.iterator

Equations

string.iterator.to_end {fst := p, snd := n} = {fst := n.reverse ++ p, snd := list.nil char}

def string.iterator.next_to_string :

string.iterator → string

Equations

string.iterator.next_to_string {fst := p, snd := n} = {data := n}

def string.iterator.prev_to_string :

string.iterator → string

Equations

string.iterator.prev_to_string {fst := p, snd := n} = {data := p.reverse}

@[protected]

def string.iterator.extract_core :

list char → list char → option (list char)

Equations

string.iterator.extract_core (c :: cs₁) cs₂ = ite (cs₁ = cs₂) (option.some [c]) (string.iterator.extract_core._match_1 c (string.iterator.extract_core cs₁ cs₂))
string.iterator.extract_core list.nil cs = option.none
string.iterator.extract_core._match_1 c (option.some r) = option.some (c :: r)
string.iterator.extract_core._match_1 c option.none = option.none

def string.iterator.extract :

string.iterator → string.iterator → option string

Equations

string.iterator.extract {fst := p₁, snd := n₁} {fst := p₂, snd := n₂} = ite (p₁.reverse ++ n₁ ≠ p₂.reverse ++ n₂) option.none (ite (n₁ = n₂) (option.some "") (string.iterator.extract._match_1 (string.iterator.extract_core n₁ n₂)))
string.iterator.extract._match_1 (option.some r) = option.some {data := r}
string.iterator.extract._match_1 option.none = option.none

The following definitions do not have builtin support in the VM

@[protected, instance]

def string.inhabited :

inhabited string

Equations

string.inhabited = {default := ""}

@[protected, instance]

def string.has_sizeof :

has_sizeof string

Equations

string.has_sizeof = {sizeof := string.length}

@[protected, instance]

def string.has_append :

has_append string

Equations

string.has_append = {append := string.append}

def string.str :

string → char → string

Equations

string.str = string.push

def string.is_empty (s : string) :

Equations

s.is_empty = decidable.to_bool (s.length = 0)

def string.front (s : string) :

Equations

s.front = s.mk_iterator.curr

def string.back (s : string) :

Equations

s.back = s.mk_iterator.to_end.prev.curr

def string.join (l : list string) :

Equations

string.join l = list.foldl (λ (r s : string), r ++ s) "" l

def string.singleton (c : char) :

Equations

string.singleton c = "".push c

def string.intercalate (s : string) (ss : list string) :

Equations

s.intercalate ss = (s.to_list.intercalate (list.map string.to_list ss)).as_string

def string.iterator.nextn :

string.iterator → ℕ → string.iterator

Equations

it.nextn (i + 1) = it.next.nextn i
it.nextn 0 = it

def string.iterator.prevn :

string.iterator → ℕ → string.iterator

Equations

it.prevn (i + 1) = it.prev.prevn i
it.prevn 0 = it

def string.pop_back (s : string) :

Equations

s.pop_back = s.mk_iterator.to_end.prev.prev_to_string

def string.popn_back (s : string) (n : ℕ) :

Equations

s.popn_back n = (s.mk_iterator.to_end.prevn n).prev_to_string

def string.backn (s : string) (n : ℕ) :

Equations

s.backn n = (s.mk_iterator.to_end.prevn n).next_to_string

@[protected]

def char.to_string (c : char) :

Equations

c.to_string = string.singleton c

def string.to_nat (s : string) :

Equations

s.to_nat = to_nat_core s.mk_iterator s.length 0

theorem string.empty_ne_str (c : char) (s : string) :

"" ≠ s.str c

theorem string.str_ne_empty (c : char) (s : string) :

s.str c ≠ ""

theorem string.str_ne_str_left {c₁ c₂ : char} (s₁ s₂ : string) :

c₁ ≠ c₂ → s₁.str c₁ ≠ s₂.str c₂

theorem string.str_ne_str_right (c₁ c₂ : char) {s₁ s₂ : string} :

s₁ ≠ s₂ → s₁.str c₁ ≠ s₂.str c₂