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

Содержание 1 Списки 1.1 Индексация 1.1.1 Конкатенация 1.1.2 elems: Элементы 1.1.3 inds: Индексы 1.2 Задача 1.3 Case 1.3.1 Список чисел Фибоначчи 1.3.2

Списки

Списки в 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 
<> -> <> 
<_i>^L2 -> rev(L2)^<_i>
end

Как это используется для работы со списками (на том же примере):

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

Задача. Определить функцию Pascal, генерирующую треугольник Паскаля до уровня n включительно. Результат --- список списков. Например:

<<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>>

Задача. Реализовать функцию rev, которая возвращает реверсивную версию списка.

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

(стандартный тип text в rsl на самом деле text=char×)

Для таких типов требуется определить функцию is_on, проверяющую, встречается ли данне слово на странице

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))

Определить number_of, подсчитывающую количество вхождений слов в страницу

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)}