нарезка списка, как если бы он имел поведение кольцевого буфера - PullRequest
Новая
       22

нарезка списка, как если бы он имел поведение кольцевого буфера

1 голос
/ 28 мая 2019

Чтобы создать функцию среза, которая имеет нижний и верхний индексы и размер списка в качестве параметров, чтобы при нарезке списка с учетом этих параметров она работала как функция сбора.

Я попытался определить его, используя концепцию фильтра, и снабдить его функцией тестирования.Пожалуйста, смотрите мой код ниже 

Require Import PeanoNat.
Require Import Coq.Init.Datatypes.
Require Import Notations.
Import Basics.

Fixpoint filter_index {X: Type} (currInd : nat) (test: nat -> bool) (l: list X ): list X :=
  match l with
  | [] => []
  | h::t =>  if test currInd then h :: filter_index (S currInd) test t else filter_index (S currInd) test t
  end.

Definition slicing_ring (tail head sz: nat) : nat -> bool :=
  fun n => if sz <=? head then orb ( n <=? head mod sz) ( tail <=? n) else andb ( tail <=? n) (n <=? head).

Example test1 : filter_index 0 (slicing_ring 3 5 4) [6;9;3;4] = [4;6;9].

Так что в приведенном выше примере я ожидаю получить список результатов.Однако, если я сделаю Compute filter_index 0 (slicing_ring 2 3 4) [6;9;3;4]., это даст мне [6;9;4].

1 Ответ

1 голос
/ 28 мая 2019

Ваша функция filter_index никогда не изменит порядок элементов списка. Элементы проверяются по порядку, а затем условно вставляются в выходные данные по порядку.

Лучший подход может быть основан на индексированном доступе. 

Fixpoint get_index {X: Type} (ls: list X) (index: nat): option X :=
  match ls, index with
  | [], _ => None
  | x :: _, 0 => Some x
  | x :: tl, S index' => get_index tl index'
  end.

(по сути это nth_error из стандартной библиотеки - есть варианты для других видов доступа).

Если вы можете перечислить индексы для вашего кольцевого буфера в нужном порядке, это должно работать нормально.

...