<commit_before>\literate[list-index]
\begin{code}
module list-index
imports list-cons simple-traversal
strategies

// Index: Get the n-th element of a list 

  index = repeat(Ind2) ; Ind1

  Ind1   : (1, [x | xs]) -> x
  Ind2   : (n, [x | xs]) -> (<subt> (n, 1), xs) where <geq> (n, 2)

// Get-index: get index of element in list 

  get_index = Gind0 ; rec x(Gind1 <+ Gind2 ; x)
  get-index = Gind0 ; rec x(Gind1 <+ Gind2 ; x)

  get-index0(s) = at-suffix([s | id]; ![]); length

  Gind0  : (x, ys) -> (1, x, ys)
  Gind1  : (n, x, [x | xs]) -> n
  Gind2  : (n, y, [x | xs]) -> (<add> (n, 1), y, xs)

// Set-index: change element in list

  Sind0    : (i, x, ys) -> (0, i, x, ys)
  Sind1    : (i, i, x, [y | ys]) -> [x | ys]
  Sind2(r) : (n, i, x, [y | ys]) -> [y | <r>(<add> (n, 1), i, x, ys)]

  set-index = Sind0; rec x(Sind1 <+ Sind2(x))

// Insert: insert element in list

  insert = Ins0; rec x(Ins1 <+ Ins2(x))

  Ins0:    (i, x, ys) -> (0, i, x, ys)
  Ins1:    (i, i, x, xs) -> [x | xs]
  Ins2(r): (n, i, x, [y | ys]) -> [y | <r>(<add> (n, 1), i, x, ys)]
\end{code}

% Copyright (C) 1998-2002 <NAME> <<EMAIL>>
% 
% This program is free software; you can redistribute it and/or modify
% it under the terms of the GNU General Public License as published by
% the Free Software Foundation; either version 2, or (at your option)
% any later version.
% 
% This program is distributed in the hope that it will be useful,
% but WITHOUT ANY WARRANTY; without even the implied warranty of
% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
% GNU General Public License for more details.
% 
% You should have received a copy of the GNU General Public License
% along with this program; if not, write to the Free Software
% Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
% 02111-1307, USA.<commit_msg>documented existing strategies and added map-with-index and add-indices<commit_after>\literate[list-index]

	\begin{abstract}

  Every element of a list is associated with in an integer index.
  The first element of a list has index 1.

	\end{abstract}

\begin{code}
module list-index
imports list-cons simple-traversal

\end{code}

  Index: Get the n-th element of a list 

\begin{code}
strategies

  // :: Int * List(a) -> a
  index =
    repeat(Ind2) ; Ind1

      Ind1   : (1, [x | xs]) -> x
      Ind2   : (n, [x | xs]) -> (<subt> (n, 1), xs) where <geq> (n, 2)

\end{code}

  Get-index: get index of element in list 

\begin{code}
strategies

  // :: a * List(a) -> Int
  get-index =
    Gind0 ; rec x(Gind1 <+ Gind2 ; x)

      Gind0  : (x, ys) -> (1, x, ys)
      Gind1  : (n, x, [x | xs]) -> n
      Gind2  : (n, y, [x | xs]) -> (<add> (n, 1), y, xs)

  get_index = 
    obsolete(!"get_index/0; use get-index/0");
    get-index

  get-index0(s) = at-suffix([s | id]; ![]); length

\end{code}

	Set-index: change element in list

\begin{code}
strategies

  // :: Int * a * List(a) -> List(a)
  set-index =
    Sind0; rec x(Sind1 <+ Sind2(x))

      Sind0    : (i, x, ys) -> (0, i, x, ys)
      Sind1    : (i, i, x, [y | ys]) -> [x | ys]
      Sind2(r) : (n, i, x, [y | ys]) -> [y | <r>(<add> (n, 1), i, x, ys)]

\end{code}

	Insert: insert element in list

\begin{code}
strategies

  // :: Int * a * List(a) -> List(a)
  insert =
    Ins0; rec x(Ins1 <+ Ins2(x))

        Ins0:    (i, x, ys) -> (0, i, x, ys)
        Ins1:    (i, i, x, xs) -> [x | xs]
        Ins2(r): (n, i, x, [y | ys]) -> [y | <r>(<add> (n, 1), i, x, ys)]

\end{code}

	Map with index: apply strategies that require some knowledge
  of the index of an element to the elements of the list.

\begin{code}

  // Int * a -> b :: List(a) -> List(b)
  map-with-index(s) = 
      !(1, <id>)
    ; rec x(
        \ (_, [])       -> [] \
      + \ (i, [e | es]) -> [<s> (i, e) | <x> (<inc> i, es)] \
      )

  // :: List(a) -> List(Int * a)
  add-indices = 
    map-with-index(id)

\end{code}

% Copyright (C) 1998-2002 Eelco Visser <<EMAIL>>
% 
% This program is free software; you can redistribute it and/or modify
% it under the terms of the GNU General Public License as published by
% the Free Software Foundation; either version 2, or (at your option)
% any later version.
% 
% This program is distributed in the hope that it will be useful,
% but WITHOUT ANY WARRANTY; without even the implied warranty of
% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
% GNU General Public License for more details.
% 
% You should have received a copy of the GNU General Public License
% along with this program; if not, write to the Free Software
% Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
% 02111-1307, USA.
{'fraction_non_alphanumeric': 0.16619840069159283, 'fraction_numerical': 0.025286362653987465, 'mean_word_length': 2.6642913697545527, 'pattern_counts': {'":': 0, '<': 33, '<?xml version=': 0, '>': 57, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '315992', 'n_tokens_mistral': 1889, 'n_tokens_neox': 1777, 'n_words': 650}