Материал из eSyr's wiki.

Списки

Спискм в RSL нз. упорядч. типизир. набор эл-тов, эл-иы могут пвторяться. Списк в угловых скбкх, прядок вжен, все элементы дного типа

<1, 3, 1, 5, 4>
<false, true>

Для спискв, кк и для всех типов в rsl пр. две перации: =, ≠

Для список опр. дв типа: T-list(для конечных), T-inflist(для бесконечных) (по ANSI); T×, T^ω

Определён пустой список: <>

пр. синтаксис <v1..vn>

Опр. синтксис: <expr|limit>

Пример:

<2×n|n in <0..3>>

<3..7> ≡ < 3,4,5,6,7>
<7..3 > ≡ <>

Список может быть опр. для лдюбго ип, не олько бзового: мнжества, списка...

Индексация

Для того, чтобы добрться д эл-та, исп. перация index, "()", в которой ук. номер эл-та:

<1,4,5,6>(2) = 4
<2,5,3>,<3,1>>(2) = <3,1>
<2,5,3>,<3,1>>(2)(2) = 1

Если по не существующему номеру, то возвращает chaos.

Операции со списками:

Конктенация

Конк. мжно применять только к кнеч. спискм, второй эл-т мжет быть и конеч, и беск. Рез-т соотв. типа

l1^l2
^:T-list x T-inflist -> T-inflist

Head: Первый элемент

hd: T^ω стрелочк с влной T
hd<> = chaos

Tail: Хвст

tl: T^ω стрпелчк с волной T^ω
tl<> = chaos

Len: длина списка

len:T^ω стрелочк с влной Nat
len<n|n • is_prime> ≡ chaos

elems: Элементы

elems: T^ω стрелочк с волнлй T-infset
Возвращает множество элементов списка

inds: Индексы

inds: T^ω стрелочк с волнлй Nat-infset 
inds FL={1..len FL}

Задача

Задача: пр. функцию length, которя выч. длину списка

value
  length: T× → Nat
    length(l) ≡ if l ≠ <> then 1 + length(tl l) else 0 end

  length2: T× → Nat 
    length2(l) ≡ card inds l

Case

Конструкция case:

case cond of
  pattern1 → expr1
  pattern2 → expr2
  ...
  _ → def_expr
end

Список чисел фибоначи

type Nat1= {n:Nat &circle; n > 0 }
value Fib:Nat1->Nat1
      Fib(n) ≡  
case n of  
      1->1
      2->2
      _->Fib(n-2)+Fib(n-1)
end

value rev:int-list× → T×
    rev(l) ≡ 
case L of 
<> -> <> 
^L2 -> rev(L2)^<i>
end

value
  length: T× → Nat
    length(l) ≡
      case l of
        <> → 0
        <i>^lr → length(lr) + 1
      end

<<1>,
 <1,1>,
 <1,2,1>,
 <1,3,3,1>,
 <1,4,6,4,1>>

type
  T1={i | i:Nat • i ≥ 1}

value
  pascal:T1 → (T1×)×
    pascal(i) ≡ if i=1 then <<1>> else pascal(i-1)^<<1>^<pascal(i-1)(i-1)(j)+pascal(i-1)(i-1)(j-)|j:T1 • j in <2..i-1>>^<1>>

value
  rev:T× → T×
    rev(l) ≡ if l = <> then <> else rev(tl l)^ hd l end

value
  rev:T× → T×
    rev(l) ≡ <l(len(l)+1-n)|n in <1..len(n)>>

type
  Page=Line×,
  Line=Word×,
  Word

value
  is_on: Word × Page → Bool
    is_on(w,p) ≡ if p=<> then False else w ∈ elems hd p ∨ is_on(w, tl p) end

  is_on: Word × Page → Bool
    is_on(w,p) ≡ ∃ i : Nat • (i ∈ {1..len(p)}) ∧ (w ∈ elems p(i))

value
  number_of: Word × Page → Nat
    number_of(w,p) → if p=<> then 0 else number_of_line(w,l) + number_of(w, tl p)

  number_of_line: Word × Line → Nat
    number_o_line(w,l) → if l=<> then 0 else (if w=hd l then 1 else 0) + number_of_line(w, tl l)


  number_of: Word × Page → Nat
    number_of(w,p) → {(i,j)|(i:Nat•j:Nat; • p(i)(j)=w ∧ i∈ p ∧ ∈p(i)}