Trying out ACSL, continuing implementation.

13 files changed, 23 insertions, 1489 deletions

diff --git a/src/core/CMakeLists.txt b/src/core/CMakeLists.txt
index bc722d7..b864aff 100644
--- a/src/core/CMakeLists.txt
+++ b/src/core/CMakeLists.txt
@@ -2,10 +2,6 @@ set(
    SRC_FILES ${SRC_FILES}
    ${CMAKE_CURRENT_SOURCE_DIR}/char.c
    ${CMAKE_CURRENT_SOURCE_DIR}/index.c
-   ${CMAKE_CURRENT_SOURCE_DIR}/sequence.c
-   ${CMAKE_CURRENT_SOURCE_DIR}/sequence_creation.c
-   ${CMAKE_CURRENT_SOURCE_DIR}/sequence_from_string.c
-   ${CMAKE_CURRENT_SOURCE_DIR}/sequence_to_string.c
 )
 
 set(SRC_FILES ${SRC_FILES} PARENT_SCOPE)
diff --git a/src/core/char.c b/src/core/char.c
index 9297643..819cd57 100644
--- a/src/core/char.c
+++ b/src/core/char.c
@@ -14,44 +14,6 @@ ZoO_char ZoO_char_to_lowercase (const ZoO_char c)
 }
 
 /* See: "char.c" */
-int ZoO_char_is_banned (const ZoO_char c)
-{
-   switch (c)
-   {
-      case '(':
-      case ')':
-      case '[':
-      case ']':
-      case '{':
-      case '}':
-      case '<':
-      case '>':
-         return 1;
-
-      default:
-         return 0;
-   }
-}
-
-/* See: "char.c" */
-int ZoO_char_is_punctuation (const ZoO_char c)
-{
-   switch (c)
-   {
-      case '!':
-      case ',':
-      case '.':
-      case ':':
-      case ';':
-      case '?':
-         return 1;
-
-      default:
-         return 0;
-   }
-}
-
-/* See: "char.c" */
 int ZoO_word_cmp
 (
    const ZoO_char word_a [const static 1],
diff --git a/src/core/char.h b/src/core/char.h
index 2b4a355..7039563 100644
--- a/src/core/char.h
+++ b/src/core/char.h
@@ -22,23 +22,5 @@ int ZoO_word_cmp
  */
 ZoO_char ZoO_char_to_lowercase (const ZoO_char c);
 
-/*
- * Returns '1' iff {c} should be considered as an punctuation character, '0'
- * otherwise.
- */
-/*@
- @ ensures ((\result == 1) || (\result == 0));
- @*/
-int ZoO_char_is_punctuation (const ZoO_char c);
-
-/*
- * Returns '1' iff containing {c} means the word should not be learned. '0'
- * otherwise.
- */
-/*@
- @ ensures ((\result == 1) || (\result == 0));
- @*/
-int ZoO_word_char_is_banned (const ZoO_char c);
-
 #endif
 
diff --git a/src/core/char_types.h b/src/core/char_types.h
index a2a736c..de0fad2 100644
--- a/src/core/char_types.h
+++ b/src/core/char_types.h
@@ -1,16 +1,5 @@
 #ifndef _ZoO_CORE_CHAR_TYPES_H_
 #define _ZoO_CORE_CHAR_TYPES_H_
-/*
- * FIXME: Does not belong here.
- */
-/*
-enum ZoO_word_property
-{
-   ZoO_WORD_NO_PROPERTY,
-   ZoO_WORD_HAS_NO_LEFT_SEPARATOR,
-   ZoO_WORD_HAS_NO_RIGHT_SEPARATOR
-};
-*/
 
 /* ZoO_char = UTF-8 char */
 typedef char ZoO_char;
diff --git a/src/core/index.c b/src/core/index.c
index 375e0ad..dc52d03 100644
--- a/src/core/index.c
+++ b/src/core/index.c
@@ -35,8 +35,13 @@ ZoO_index ZoO_index_random (void)
    ZoO_index result;
    unsigned char * result_bytes;
 
+   /*@ ghost return 4; @*/ /* Chosen by fair dice roll. */
+                           /* Guaranteed to be random. */
+   /* More seriously, I am not explaining the hack below to Frama-C */
+
    result_bytes = (unsigned char *) &result;
 
+
    for (i = 0; i < sizeof(ZoO_index); ++i)
    {
       result_bytes[i] = random_uchar();
diff --git a/src/core/index.h b/src/core/index.h
index 1417662..eb3c471 100644
--- a/src/core/index.h
+++ b/src/core/index.h
@@ -6,14 +6,19 @@
 /*
  * Returns a random ZoO_index.
  */
+/*@
+   ensures (\result <= ZoO_INDEX_MAX);
+   assigns \result;
+@*/
 ZoO_index ZoO_index_random (void);
 
 /*
  * Returns a random ZoO_index, included in [0, limit]
  */
 /*@
- @ ensures (\result <= limit);
- @*/
+   ensures (\result <= limit);
+   assigns \result;
+@*/
 ZoO_index ZoO_index_random_up_to (const ZoO_index limit);
 
 #endif
diff --git a/src/core/index_types.h b/src/core/index_types.h
index a71121c..84a1e20 100644
--- a/src/core/index_types.h
+++ b/src/core/index_types.h
@@ -1,6 +1,12 @@
 #ifndef _ZoO_CORE_INDEX_TYPES_H_
 #define _ZoO_CORE_INDEX_TYPES_H_
 
+/*
+ * ZoO_index is a replacement for size_t. As many indices are stored for every
+ * word learned, having control over which type of variable is used to represent
+ * those indices lets us scale the RAM usage.
+ */
+
 #include <limits.h>
 
 /* Must be unsigned. */
@@ -9,4 +15,9 @@ typedef unsigned int ZoO_index;
 /* Must be > 0. */
 #define ZoO_INDEX_MAX UINT_MAX
 
+
+#if (ZoO_INDEX_MAX > SIZE_MAX)
+   #error "ZoO_index should not be able to go higher than a size_t variable."
+#endif
+
 #endif
diff --git a/src/core/sequence.c b/src/core/sequence.c
deleted file mode 100644
index d7ff9d0..0000000
--- a/src/core/sequence.c
+++ /dev/null
@@ -1,103 +0,0 @@
-#include <stdlib.h>
-#include <string.h>
-
-#include "../core/index.h"
-
-#include "sequence.h"
-
-/*
- * Bypass rendundant ZoO_START_OF_SEQUENCE_ID at the start of a sequence.
- */
-/* ensures (*sequence_offset <= sequence_length) */
-static void bypass_redundant_sos
-(
-   const ZoO_index sequence [const restrict],
-   const ZoO_index sequence_length,
-   ZoO_index sequence_offset [const restrict static 1]
-)
-{
-   ZoO_index i;
-
-   *sequence_offset = 0;
-
-   for (i = 0; i < sequence_length; ++i)
-   {
-      if (sequence[i] != ZoO_START_OF_SEQUENCE_ID)
-      {
-         return;
-      }
-      else if (sequence[i] == ZoO_START_OF_SEQUENCE_ID)
-      {
-         *sequence_offset = i;
-      }
-   }
-}
-
-
-/* See "sequence.h" */
-int ZoO_sequence_cmp
-(
-   const ZoO_index sequence_a [const],
-   ZoO_index sequence_a_length,
-   const ZoO_index sequence_b [const],
-   ZoO_index sequence_b_length
-)
-{
-   ZoO_index min_length, a, b;
-   ZoO_index a_offset, b_offset;
-   ZoO_index i;
-
-   bypass_redundant_sos(sequence_a, sequence_a_length, &a_offset);
-   bypass_redundant_sos(sequence_b, sequence_b_length, &b_offset);
-
-   /*@ requires (*a_offset <= sequence_a_length) @*/
-   sequence_a_length -= a_offset;
-   /*@ requires (*b_offset <= sequence_b_length) @*/
-   sequence_b_length -= b_offset;
-
-   if (sequence_a_length < sequence_b_length)
-   {
-      min_length = sequence_a_length;
-   }
-   else
-   {
-      min_length = sequence_b_length;
-   }
-
-   /*@ ensures (min_length <= sequence_a_length) @*/
-   /*@ ensures (min_length <= sequence_b_length) @*/
-
-   for (i = 0; i < min_length; ++i)
-   {
-      /*@ requires ((i + a_offset) < sequence_a_length) @*/
-      a = sequence_a[i + a_offset];
-      /*@ requires ((i + b_offset) < sequence_b_length) @*/
-      b = sequence_b[i + b_offset];
-
-      if (a < b)
-      {
-         return -1;
-      }
-      else if (b > a)
-      {
-         return 1;
-      }
-      else if ((a == ZoO_END_OF_SEQUENCE_ID) && (b == ZoO_END_OF_SEQUENCE_ID))
-      {
-         return 0;
-      }
-   }
-
-   if (sequence_a_length > sequence_b_length)
-   {
-      return 1;
-   }
-   else if (sequence_a_length < sequence_b_length)
-   {
-      return -1;
-   }
-   else
-   {
-      return 0;
-   }
-}
diff --git a/src/core/sequence.h b/src/core/sequence.h
deleted file mode 100644
index 1e286ab..0000000
--- a/src/core/sequence.h
+++ /dev/null
@@ -1,80 +0,0 @@
-#ifndef _ZoO_CORE_SEQUENCE_H_
-#define _ZoO_CORE_SEQUENCE_H_
-
-#include "../core/char_types.h"
-#include "../core/index_types.h"
-
-#include "../pipe/pipe.h"
-
-#include "../knowledge/knowledge_types.h"
-
-#include "sequence_types.h"
-
-int ZoO_sequence_from_undercase_string
-(
-   const ZoO_char string [const restrict],
-   const ZoO_index string_length,
-   struct ZoO_knowledge k [const restrict static 1],
-   ZoO_index * sequence [const restrict static 1],
-   ZoO_index sequence_length [const restrict static 1],
-   const struct ZoO_pipe io [const restrict static 1]
-);
-
-/*
- * Creates a sequence containing {initial_word}. The remaining elements of
- * sequence are added according to what is known to {k} as being possible.
- * The resulting sequence starts by ZoO_START_OF_SEQUENCE_ID, and ends by
- * ZoO_END_OF_SEQUENCE_ID. The sequence is allocated by the function. If an
- * error occur, it is unallocated and set to NULL ({sequence_size} is set
- * accordingly).
- * Return:
- *    0 on success.
- *    -1 iff the allocating failed.
- *    -2 iff the sequence initialization failed.
- *    -3 iff an error occured when trying to add elements to the right of the
- *       sequence.
- *    -4 iff an error occured when trying to add elements to the left of the
- *       sequence.
- *    -5 iff the resulting sequence would have been empty.
- * Pre:
- *    (> {markov_order} 0)
- *    (knows {k} {initial_word})
- *    (initialized {k})
- */
-int ZoO_sequence_create_from
-(
-   const ZoO_index initial_word,
-   ZoO_index credits [const restrict],
-   const struct ZoO_knowledge k [const restrict static 1],
-   const ZoO_index markov_order,
-   ZoO_index * sequence [const restrict static 1],
-   size_t sequence_size [const restrict static 1],
-   const struct ZoO_pipe io [const restrict static 1]
-);
-
-/*
- * Compares two sequences.
- * ZoO_END_OF_SEQUENCE marks the ending of a sequence, regardless of indicated
- * sequence length, meaning that [10][ZoO_END_OF_SEQUENCE][9] and
- * [10][ZoO_END_OF_SEQUENCE][8] are considered equal. Sequences do not have to
- * contain ZoO_END_OF_SEQUENCE. [10][ZoO_END_OF_SEQUENCE] and [10] are
- * considered different, [10][ZoO_END_OF_SEQUENCE]
- * and [10][ZoO_END_OF_SEQUENCE][ZoO_END_OF_SEQUENCE] are considered equal.
- * Same logic is applyied for ZoO_START_OF_SEQUENCE:
- * [START_OF_SEQUENCE][10] is not [10], but
- * [START_OF_SEQUENCE][START_OF_SEQUENCE][10] and [START_OF_SEQUENCE][10] are
- * the same.
- * Return:
- *    1 iff {sequence_a} should be considered being more than {sequence_b}
- *    0 iff {sequence_a} should be considered being equal to {sequence_b}
- *    -1 iff {sequence_a} should be considered being less than {sequence_b}
- */
-int ZoO_sequence_cmp
-(
-   const ZoO_index sequence_a [const],
-   const ZoO_index sequence_a_length,
-   const ZoO_index sequence_b [const],
-   const ZoO_index sequence_b_length
-);
-
-#endif
diff --git a/src/core/sequence_creation.c b/src/core/sequence_creation.c
deleted file mode 100644
index c5ca6af..0000000
--- a/src/core/sequence_creation.c
+++ /dev/null
@@ -1,775 +0,0 @@
-#include <stdlib.h>
-#include <stdio.h>
-#include <string.h>
-#include <stdint.h> /* defines SIZE_MAX */
-
-#include "../core/index.h"
-
-#include "../pipe/pipe.h"
-
-#include "../knowledge/knowledge.h"
-
-#include "sequence.h"
-
-/*
- * Returns a randomly chosen index pointing to a element in {weights}.
- * The values of {weights} are used as weights to guide the choice.
- * Returns:
- *    Value in [0, (length weights)[.
- * Pre:
- *    (> weights_sum 0).
- *    (= (sum weights) weights_sum).
- */
-/*@
- @ requires (weights_sum > 0);
- @ requires \valid(weights);
- @ requires (\sum(0, (\length(weights) - 1), weights) = weights_sum);
-@*/
-static ZoO_index weighted_random_pick
-(
-   const ZoO_index weights [const restrict static 1],
-   const ZoO_index weights_sum
-)
-{
-   ZoO_index result, accumulator, random_number;
-
-   accumulator = 0;
-
-   random_number = ZoO_index_random_up_to(weights_sum);
-   /*@ ensures (0 <= random_number <= weights_sum); @*/
-
-   for (result = 0; accumulator < random_number; ++result)
-   {
-      /*@ requires (\sum(0, (\length(weights) - 1), weights) = weights_sum); @*/
-      accumulator += weights[result];
-   }
-
-   return result;
-}
-
-/******************************************************************************/
-/** ADDING ELEMENTS TO THE LEFT ***********************************************/
-/******************************************************************************/
-
-/*
- * Adds an id to the left of the sequence.
- * This requires the reallocation of {sequence}. The freeing of the previous
- * memory space is handled. If an error happened, {*sequence} remains untouched.
- * Returns:
- *    0 on success.
- *    -1 iff adding the word would cause an overflow.
- *    -2 iff memory allocation was unsuccessful.
- * Post:
- *    (initialized {sequence})
- *    (initialized {*sequence})
- */
-static int left_append
-(
-   const ZoO_index word_id,
-   ZoO_index * sequence [const restrict],
-   const size_t sequence_size,
-   const struct ZoO_pipe io [const restrict static 1]
-)
-{
-   ZoO_index * new_sequence;
-
-   if ((SIZE_MAX - sizeof(ZoO_index)) > sequence_size)
-   {
-      ZoO_S_ERROR
-      (
-         io,
-         "Left side append aborted, as the new sequence's size would overflow."
-      );
-
-      return -1;
-   }
-
-   new_sequence = (ZoO_index *) malloc(sizeof(ZoO_index) + sequence_size);
-
-   if (new_sequence == (ZoO_index *) NULL)
-   {
-      ZoO_S_ERROR
-      (
-         io,
-         "Left side append aborted, as memory for the new sequence could not be"
-         " allocated."
-      );
-
-      return -2;
-   }
-
-   if (sequence_size > 0)
-   {
-      memcpy
-      (
-         (void *) (new_sequence + 1),
-         (const void *) sequence,
-         sequence_size
-      );
-
-      free((void *) sequence);
-   }
-
-   new_sequence[0] = word_id;
-
-   *sequence = new_sequence;
-
-   return 0;
-}
-
-/*
- * Adds an id to the left of the sequence, according to what is known as likely
- * to fit there.
- * This requires the reallocation of {sequence}. The freeing of the previous
- * memory space is handled. If an error happened, {*sequence} remains untouched.
- * Semaphore:
- *    Takes then releases access for {k}.
- * Returns:
- *    0 on success.
- *    -1 iff nothing fitting was found.
- *    -2 iff the addition of that id failed.
- * Pre:
- *    (initialized {sequence})
- *    (initialized {k})
- *    (> {markov_order} 0)
- *    (initialized {*sequence[0..({markov_order} - 1)]})
- */
-static int extend_left
-(
-   ZoO_index * sequence [const restrict static 1],
-   const size_t sequence_size,
-   const ZoO_index markov_order,
-   const struct ZoO_knowledge k [const restrict static 1],
-   const struct ZoO_pipe io [const restrict static 1]
-)
-{
-   const ZoO_index * restrict preceding_words;
-   const ZoO_index * restrict preceding_words_weights;
-   ZoO_index preceding_words_weights_sum;
-
-   (void) ZoO_knowledge_lock_access(k, io);
-
-   if
-   (
-      ZoO_knowledge_find_preceding_words
-      (
-         k,
-         *sequence,
-         markov_order,
-         &preceding_words,
-         &preceding_words_weights,
-         &preceding_words_weights_sum,
-         io
-      ) < 0
-   )
-   {
-      (void) ZoO_knowledge_unlock_access(k, io);
-
-      return -1;
-   }
-
-   /* preceding_words_weights_sum > 0 */
-
-   if
-   (
-      left_append
-      (
-         weighted_random_pick
-         (
-            preceding_words_weights,
-            preceding_words_weights_sum
-         ),
-         sequence,
-         sequence_size,
-         io
-      ) < 0
-   )
-   {
-      (void) ZoO_knowledge_unlock_access(k, io);
-
-      return -3;
-   }
-
-   (void) ZoO_knowledge_unlock_access(k, io);
-
-   return 0;
-}
-
-/*
- * Continuously adds ids to the left of the sequence, according to what is known
- * as likely to fit there. If {credits} is NULL, it will stop upon reaching
- * the id indicating the start of a sequence, otherwise it will also limit to
- * {*credits} words added (including the one indicating the start of a
- * sequence).
- * This requires the reallocation of {sequence}. The freeing of the previous
- * memory space is handled. If an error happened, {sequence} remains unfreed.
- * Returns:
- *    0 on success.
- *    -1 iff we did not manage to have ZoO_START_OF_SEQUENCE_ID as a starting
- *       point. This cannot be caused by lack of {*credits}, but rather by a
- *       memory allocation problem or a more important issue in {k}. Indeed, it
- *       could mean we do not know any word preceding {*sequence[0]}, not even
- *       ZoO_START_OF_SEQUENCE_ID.
- * Pre:
- *    (initialized {sequence})
- *    (initialized {sequence_size})
- *    (initialized {k})
- *    (> {markov_order} 0)
- *    (initialized {*sequence[0..(MARKOV_ORDER - 1)]})
- */
-static int complete_left_part_of_sequence
-(
-   ZoO_index * sequence [restrict static 1],
-   size_t sequence_size [const restrict static 1],
-   const ZoO_index markov_order,
-   ZoO_index credits [const restrict],
-   const struct ZoO_knowledge k [const restrict static 1],
-   const struct ZoO_pipe io [const restrict static 1]
-)
-{
-   for (;;)
-   {
-      if ((credits == (ZoO_index *) NULL) || (*credits > 0))
-      {
-         if (extend_left(sequence, *sequence_size, markov_order, k, io) < 0)
-         {
-            /* We are sure *sequence[0] is defined. */
-            if (*sequence[0] == ZoO_START_OF_SEQUENCE_ID)
-            {
-               /*
-                * We failed to add a word, but it was because none should have
-                * been added.
-                */
-               return 0;
-            }
-            else
-            {
-               return -1;
-            }
-         }
-      }
-      else
-      {
-         /* No more credits available, the sequence will have to start here. */
-         *sequence[0] = ZoO_START_OF_SEQUENCE_ID;
-
-         return 0;
-      }
-
-      /*
-       * Safe: if it was going to overflow, extend_left would have returned a
-       * negative value, making this statement unreachable.
-       */
-      *sequence_size = (*sequence_size + sizeof(ZoO_index));
-
-      if (credits != (ZoO_index *) NULL)
-      {
-         *credits -= 1;
-      }
-
-      /* We are sure *sequence[0] is defined. */
-      switch (*sequence[0])
-      {
-         case ZoO_END_OF_SEQUENCE_ID:
-            ZoO_S_WARNING
-            (
-               io,
-               "END OF LINE was added at the left part of an sequence."
-            );
-
-            *sequence[0] = ZoO_START_OF_SEQUENCE_ID;
-            return 0;
-
-         case ZoO_START_OF_SEQUENCE_ID:
-            return 0;
-
-         default:
-            break;
-      }
-   }
-}
-
-/******************************************************************************/
-/** ADDING ELEMENTS TO THE RIGHT **********************************************/
-/******************************************************************************/
-
-/*
- * Adds an id to the right of the sequence.
- * This requires the reallocation of {sequence}. The freeing of the previous
- * memory space is handled. If an error happened, {sequence} remain untouched.
- * Returns:
- *    0 on success.
- *    -1 iff adding the word would cause an overflow.
- *    -2 iff memory allocation was unsuccessful.
- * Post:
- *    (initialized {sequence})
- *    (initialized {*sequence})
- */
-static int right_append
-(
-   ZoO_index * sequence [const restrict],
-   const ZoO_index word_id,
-   const size_t sequence_size,
-   const ZoO_index sequence_length,
-   const struct ZoO_pipe io [const restrict static 1]
-)
-{
-   ZoO_index * new_sequence;
-
-   if ((SIZE_MAX - sizeof(ZoO_index)) > sequence_size)
-   {
-      ZoO_S_ERROR
-      (
-         io,
-         "Right side append aborted, as the new sequence's size would overflow."
-      );
-
-      return -1;
-   }
-
-   new_sequence =
-      (ZoO_index *) realloc
-      (
-         sequence,
-         (sequence_size + sizeof(ZoO_index))
-      );
-
-   if (new_sequence == (ZoO_index *) NULL)
-   {
-      ZoO_S_ERROR
-      (
-         io,
-         "Right side append aborted, as memory for the new sequence could not "
-         "be allocated."
-      );
-
-      return -2;
-   }
-
-   new_sequence[sequence_length] = word_id;
-
-   *sequence = new_sequence;
-
-   return 0;
-}
-
-/*
- * Adds an id to the right of the sequence, according to what is known as likely
- * to fit there.
- * This requires the reallocation of {sequence}. The freeing of the previous
- * memory space is handled. If an error happened, {*sequence} remains untouched.
- * Semaphore:
- *    Takes then releases access for {k}.
- * Returns:
- *    0 on success.
- *    -1 iff nothing fitting was found.
- *    -2 iff the addition of that id failed.
- * Pre:
- *    (initialized {sequence})
- *    (initialized {k})
- *    (> {markov_order} 0)
- *    (initialized {*sequence[0..(MARKOV_ORDER - 1)]})
- */
-static int extend_right
-(
-   ZoO_index * sequence [const restrict static 1],
-   const size_t sequence_size,
-   const ZoO_index markov_order,
-   const ZoO_index sequence_length,
-   const struct ZoO_knowledge k [const restrict static 1],
-   const struct ZoO_pipe io [const restrict static 1]
-)
-{
-   const ZoO_index * restrict following_words;
-   const ZoO_index * restrict following_words_weights;
-
-   ZoO_index following_words_weights_sum;
-
-   (void) ZoO_knowledge_lock_access(k, io);
-
-   if
-   (
-      ZoO_knowledge_find_following_words
-      (
-         k,
-         *sequence,
-         sequence_length,
-         markov_order,
-         &following_words,
-         &following_words_weights,
-         &following_words_weights_sum
-      ) < 0
-   )
-   {
-      (void) ZoO_knowledge_unlock_access(k, io);
-
-      return -1;
-   }
-
-   /* following_words_weights_sum > 0 */
-
-   if
-   (
-      right_append
-      (
-         sequence,
-         weighted_random_pick
-         (
-            following_words_weights,
-            following_words_weights_sum
-         ),
-         sequence_size,
-         sequence_length,
-         io
-      ) < 0
-   )
-   {
-      (void) ZoO_knowledge_unlock_access(k, io);
-
-      return -3;
-   }
-
-   (void) ZoO_knowledge_unlock_access(k, io);
-
-   return 0;
-}
-
-/*
- * Continuously adds ids to the right of the sequence, according to what is
- * known as likely to fit there. If {credits} is NULL, it will stop upon
- * reaching the id indicating the end of a sequence, otherwise it will also
- * limit to {*credits} words added (including the one indicating the end of a
- * sequence).
- * This requires the reallocation of {sequence}. The freeing of the previous
- * memory space is handled. If an error happened, {sequence} remain untouched.
- * Returns:
- *    0 on success.
- *    -1 iff we did not manage to have ZoO_END_OF_SEQUENCE_ID as a stopping
- *       point. This cannot be caused by lack of {*credits}, but rather by a
- *       memory allocation problem or a more important issue in {k}. Indeed, it
- *       could mean we do not know any word following {*sequence[0]}, not even
- *       ZoO_END_OF_SEQUENCE_ID.
- * Pre:
- *    (initialized {sequence})
- *    (initialized {*sequence_size})
- *    (initialized {k})
- *    (> {markov_order} 0)
- *    (initialized {*sequence[0..(MARKOV_ORDER - 1)]})
- */
-static int complete_right_part_of_sequence
-(
-   ZoO_index * sequence [const restrict static 1],
-   size_t sequence_size [const restrict static 1],
-   const ZoO_index markov_order,
-   ZoO_index credits [const restrict],
-   const struct ZoO_knowledge k [const restrict static 1],
-   const struct ZoO_pipe io [const restrict static 1]
-)
-{
-   ZoO_index sequence_length;
-
-   sequence_length = (*sequence_size / sizeof(ZoO_index));
-
-   for (;;)
-   {
-      if ((credits == (ZoO_index *) NULL) || (*credits > 0))
-      {
-         if
-         (
-            extend_right
-            (
-               sequence,
-               *sequence_size,
-               markov_order,
-               sequence_length,
-               k,
-               io
-            ) < 0
-         )
-         {
-            /* Safe: (> sequence_length 1) */
-            if (*sequence[(sequence_length - 1)] == ZoO_END_OF_SEQUENCE_ID)
-            {
-               /*
-                * We failed to add a word, but it was because none should have
-                * been added.
-                */
-               return 0;
-            }
-            else
-            {
-               return -1;
-            }
-         }
-      }
-      else
-      {
-         /* No more credits available, we end the sequence. */
-         *sequence[(sequence_length - 1)] = ZoO_END_OF_SEQUENCE_ID;
-
-         return 0;
-      }
-
-      /*
-       * Safe: if it was going to overflow, extend_left would have returned a
-       * negative value, making this statement unreachable.
-       */
-      *sequence_size = (*sequence_size + sizeof(ZoO_index));
-      sequence_length += 1;
-
-      if (credits != (ZoO_index *) NULL)
-      {
-         *credits -= 1;
-      }
-
-      /* Safe: (> sequence_length 1) */
-      switch (*sequence[(sequence_length - 1)])
-      {
-         case ZoO_START_OF_SEQUENCE_ID:
-            ZoO_S_WARNING
-            (
-               io,
-               "END OF LINE was added at the right part of an sequence."
-            );
-
-            *sequence[(sequence_length - 1)] = ZoO_END_OF_SEQUENCE_ID;
-            return 0;
-
-         case ZoO_END_OF_SEQUENCE_ID:
-            return 0;
-
-         default:
-            break;
-      }
-   }
-}
-
-/******************************************************************************/
-/** INITIALIZING SEQUENCE *****************************************************/
-/******************************************************************************/
-
-/*
- * Allocates the memory required to store the initial sequence.
- * Returns:
- *    0 on success.
- *    -1 if this would require more memory than can indicate a size_t variable.
- *    -2 if the allocation failed.
- * Post:
- *    (initialized {*sequence})
- *    (initialized {*sequence_size})
- */
-static int allocate_initial_sequence
-(
-   ZoO_index * sequence [const restrict static 1],
-   size_t sequence_size [const restrict static 1],
-   const ZoO_index markov_order,
-   const struct ZoO_pipe io [const restrict static 1]
-)
-{
-   if ((SIZE_MAX / sizeof(ZoO_index)) > ((size_t) markov_order))
-   {
-      ZoO_S_ERROR
-      (
-         io,
-         "Unable to store size of the initial sequence in a size_t variable."
-         "Either reduce the size of a ZoO_index or the markovian order."
-      );
-
-      *sequence = (ZoO_index *) NULL;
-      *sequence_size = 0;
-
-      return -1;
-   }
-
-   *sequence_size = (((size_t) markov_order) * sizeof(ZoO_index));
-   *sequence = (ZoO_index *) malloc(*sequence_size);
-
-   if (*sequence == (void *) NULL)
-   {
-      *sequence_size = 0;
-
-      ZoO_S_ERROR
-      (
-         io,
-         "Unable to allocate the memory required for an new sequence."
-      );
-
-      return -2;
-   }
-
-   return 0;
-}
-
-/*
- * Initializes an pre-allocated sequence by filling it with {initial_word}
- * followed by a sequence of ({markov_order} - 1) words that is known to have
- * followed {initial_word} at least once. This sequence is chosen depending on
- * how often {k} indicates it has followed {initial_word}. Note that if
- * {markov_order} is 1, there is no sequence added, simply {initial_word}.
- * Returns:
- *    0 on success.
- *    -1 if no such sequence was found.
- * Pre:
- *    (size (= {sequence} {markov_order}))
- *    (initialized {k})
- *    (> markov_order 0)
- * Post:
- *    (initialized {sequence[0..(markov_order - 1)]})
- */
-static int initialize_sequence
-(
-   ZoO_index sequence [const restrict static 1],
-   const ZoO_index initial_word,
-   const ZoO_index markov_order,
-   const struct ZoO_knowledge k [const static 1],
-   const struct ZoO_pipe io [const restrict static 1]
-)
-{
-   const ZoO_index * restrict following_sequences_ref;
-   const ZoO_index * restrict chosen_sequence;
-   const ZoO_index * restrict following_sequences_weights;
-   ZoO_index following_sequences_weights_sum;
-
-   sequence[0] = initial_word;
-
-   if (markov_order == 1)
-   {
-      return 0;
-   }
-
-   /* TODO */
-   (void) ZoO_knowledge_lock_access(k, io);
-
-   if
-   (
-      ZoO_knowledge_get_following_sequences_ref
-      (
-         k,
-         initial_word,
-         &following_sequences_ref,
-         &following_sequences_weights,
-         &following_sequences_weights_sum,
-         io
-      ) < 0
-   )
-   {
-      (void) ZoO_knowledge_unlock_access(k, io);
-
-      ZoO_S_ERROR
-      (
-         io,
-         "Unable to find any sequence that would precede the initial word."
-      );
-
-      return -1;
-   }
-
-   /* following_sequences_ref contains only valid references. */
-   (void) ZoO_knowledge_get_sequence
-   (
-      k,
-      following_sequences_ref
-      [
-         weighted_random_pick
-         (
-            following_sequences_weights,
-            following_sequences_weights_sum
-         )
-      ],
-      &chosen_sequence,
-      io
-   );
-
-   /* Safe if 'allocate_initial_sequence' succeeded. */
-   memcpy
-   (
-      (void *) (sequence + 1),
-      (const void *) chosen_sequence,
-      ((((size_t) markov_order) - 1) * sizeof(ZoO_index))
-   );
-
-   (void) ZoO_knowledge_unlock_access(k, io);
-
-   return 0;
-}
-
-/******************************************************************************/
-/** EXPORTED ******************************************************************/
-/******************************************************************************/
-
-/* See "sequence.h" */
-int ZoO_sequence_create_from
-(
-   const ZoO_index initial_word,
-   ZoO_index credits [const restrict],
-   const struct ZoO_knowledge k [const restrict static 1],
-   const ZoO_index markov_order,
-   ZoO_index * sequence [const restrict static 1],
-   size_t sequence_size [const restrict static 1],
-   const struct ZoO_pipe io [const restrict static 1]
-)
-{
-   if (allocate_initial_sequence(sequence, sequence_size, markov_order, io) < 0)
-   {
-      return -1;
-   }
-
-   if (initialize_sequence(*sequence, initial_word, markov_order, k, io) < 0)
-   {
-      free((void *) *sequence);
-      *sequence_size = 0;
-
-      return -2;
-   }
-
-   if
-   (
-      complete_right_part_of_sequence
-      (
-         sequence,
-         sequence_size,
-         markov_order,
-         credits,
-         k,
-         io
-      ) < 0
-   )
-   {
-      free((void *) *sequence);
-      *sequence_size = 0;
-
-      return -3;
-   }
-
-   if
-   (
-      complete_left_part_of_sequence
-      (
-         sequence,
-         sequence_size,
-         markov_order,
-         credits,
-         k,
-         io
-      ) < 0
-   )
-   {
-      free((void *) *sequence);
-      *sequence_size = 0;
-
-      return -4;
-   }
-
-   if ((*sequence_size / sizeof(ZoO_index)) < 3)
-   {
-      /* 2 elements, for start and stop. */
-      ZoO_S_ERROR(io, "Created sequence was empty.");
-
-      free((void *) *sequence);
-      *sequence_size = 0;
-
-      return -5;
-   }
-
-   return 0;
-}
diff --git a/src/core/sequence_from_string.c b/src/core/sequence_from_string.c
deleted file mode 100644
index deaec86..0000000
--- a/src/core/sequence_from_string.c
+++ /dev/null
@@ -1,351 +0,0 @@
-#define _POSIX_C_SOURCE 200809L
-#include <stdlib.h>
-#include <string.h>
-#include <stdint.h> /* defines SIZE_MAX */
-
-#include "../core/char.h"
-#include "../core/index.h"
-
-#include "../pipe/pipe.h"
-
-#include "../knowledge/knowledge.h"
-
-#include "sequence.h"
-
-static int add_word_id_to_sequence
-(
-   const ZoO_index word_id,
-   ZoO_index * sequence [const restrict static 1],
-   ZoO_index sequence_length [const restrict static 1],
-   const struct ZoO_pipe io [const restrict static 1]
-)
-{
-   ZoO_index * new_sequence;
-
-   *sequence_length += 1;
-
-   new_sequence =
-      (ZoO_index *) realloc
-      (
-         (void *) *sequence,
-         (((size_t) sequence_length) * sizeof(ZoO_index))
-      );
-
-   if (new_sequence == (ZoO_index *) NULL)
-   {
-      ZoO_S_ERROR(io, "Unable to reallocate a sequence to add word ids to it.");
-
-      return -1;
-   }
-
-   return 0;
-}
-
-/******************************************************************************/
-/** HANDLING PUNCTUATION ******************************************************/
-/******************************************************************************/
-
-/*
- * Semaphore:
- *    Takes then releases access for {k}.
- */
-static int add_punctuation_to_sequence
-(
-   const ZoO_char string [const restrict static 1],
-   const ZoO_char punctuation,
-   ZoO_index * sequence [const restrict static 1],
-   ZoO_index sequence_length [const restrict static 1],
-   const struct ZoO_knowledge k [const restrict static 1],
-   const struct ZoO_pipe io [const restrict static 1]
-)
-{
-   ZoO_index word_id;
-   ZoO_char as_word[2];
-
-   as_word[0] = punctuation;
-   as_word[1] = '\0';
-
-   (void) ZoO_knowledge_lock_access(k, io);
-
-   if (ZoO_knowledge_find_word_id(k, as_word, 2, &word_id, io) < 0)
-   {
-      (void) ZoO_knowledge_unlock_access(k, io);
-
-      ZoO_PROG_ERROR
-      (
-         io,
-         "'%s' was defined as a punctuation, was found in a string, yet is not"
-         " defined in the knowledge database.",
-         as_word
-      );
-
-      return -1;
-   }
-
-   (void) ZoO_knowledge_unlock_access(k, io);
-
-   if (add_word_id_to_sequence(word_id, sequence, sequence_length, io) < 0)
-   {
-      return -1;
-   }
-
-   return 0;
-}
-
-static int word_is_punctuation_terminated
-(
-   const ZoO_char string [const restrict static 1],
-   const ZoO_index word_start,
-   const ZoO_index word_length
-)
-{
-   return ZoO_char_is_punctuation(string[word_length]);
-}
-
-/******************************************************************************/
-/** HANDLING WORDS ************************************************************/
-/******************************************************************************/
-
-/*
- * Semaphore:
- *    Takes then releases access for {k}.
- */
-static int add_word_to_sequence
-(
-   const ZoO_char string [const restrict static 1],
-   const ZoO_index word_start,
-   const ZoO_index word_length,
-   ZoO_index * sequence [const restrict static 1],
-   ZoO_index sequence_length [const restrict static 1],
-   struct ZoO_knowledge k [const restrict static 1],
-   const struct ZoO_pipe io [const restrict static 1]
-)
-{
-   ZoO_index word_id;
-   ZoO_char * stored_word;
-
-   if (word_length == 0)
-   {
-      return 0;
-   }
-
-   (void) ZoO_knowledge_lock_access(k, io);
-
-   if
-   (
-      ZoO_knowledge_learn_word
-      (
-         k,
-         (string + word_start),
-         word_length,
-         &word_id,
-         io
-      ) < 0
-   )
-   {
-      (void) ZoO_knowledge_unlock_access(k, io);
-
-      return -1;
-   }
-
-   (void) ZoO_knowledge_unlock_access(k, io);
-
-   if (add_word_id_to_sequence(word_id, sequence, sequence_length, io) < 0)
-   {
-      return -1;
-   }
-
-   return 0;
-}
-
-static int add_finding_to_sequence
-(
-   const ZoO_char string [const restrict static 1],
-   const ZoO_index word_start,
-   const ZoO_index word_length,
-   ZoO_index * sequence [const restrict static 1],
-   ZoO_index sequence_length [const restrict static 1],
-   struct ZoO_knowledge k [const restrict static 1],
-   const struct ZoO_pipe io [const restrict static 1]
-)
-{
-   ZoO_index punctuation;
-
-   if (word_is_punctuation_terminated(string, word_start, word_length))
-   {
-      punctuation = 1;
-   }
-   else
-   {
-      punctuation = 0;
-   }
-
-   if
-   (
-      add_word_to_sequence
-      (
-         string,
-         word_start,
-         (word_length - punctuation),
-         sequence,
-         sequence_length,
-         k,
-         io
-      ) < 0
-   )
-   {
-      return -1;
-   }
-
-   if
-   (
-      (punctuation == 1)
-      &&
-      (
-         add_punctuation_to_sequence
-         (
-            string,
-            string[word_start + word_length - 1],
-            sequence,
-            sequence_length,
-            k,
-            io
-         ) < 0
-      )
-   )
-   {
-      return -1;
-   }
-
-   return 0;
-}
-
-static int find_word
-(
-   const ZoO_char string [const restrict static 1],
-   const ZoO_index string_length,
-   const ZoO_index offset,
-   ZoO_index word_start [const restrict static 1],
-   ZoO_index word_length [const restrict static 1]
-)
-{
-   ZoO_index i;
-
-   i = offset;
-
-   while ((string[i] == ' ') && (i < string_length))
-   {
-      i += 1;
-   }
-
-   if (i >= string_length)
-   {
-      return -1;
-   }
-
-   *word_start = i;
-
-   while ((string[i] != ' ') && (i < string_length))
-   {
-      i += 1;
-   }
-
-   if (i >= string_length)
-   {
-      return -1;
-   }
-
-   *word_length = (i - *word_start);
-
-   return 0;
-}
-
-/******************************************************************************/
-/** EXPORTED ******************************************************************/
-/******************************************************************************/a
-
-/* See: "sequence.h" */
-int ZoO_sequence_from_undercase_string
-(
-   const ZoO_char string [const restrict],
-   const ZoO_index string_length,
-   struct ZoO_knowledge k [const restrict static 1],
-   ZoO_index * sequence [const restrict static 1],
-   ZoO_index sequence_length [const restrict static 1],
-   const struct ZoO_pipe io [const restrict static 1]
-)
-{
-   ZoO_index word_start, word_length;
-   ZoO_index i;
-
-   i = 0;
-
-   *sequence = (ZoO_index *) NULL;
-   *sequence_length = 0;
-
-   if
-   (
-      add_word_id_to_sequence
-      (
-         ZoO_START_OF_SEQUENCE_ID,
-         sequence,
-         sequence_length,
-         io
-      ) < 0
-   )
-   {
-      return -1;
-   }
-
-   while (i < string_length)
-   {
-      if (find_word(string, i, string_length, &word_start, &word_length) < 0)
-      {
-         break;
-      }
-
-      if
-      (
-         add_finding_to_sequence
-         (
-            string,
-            word_start,
-            word_length,
-            sequence,
-            sequence_length,
-            k,
-            io
-         ) < 0
-      )
-      {
-         free((void *) *sequence);
-         *sequence = (ZoO_index *) NULL;
-         *sequence_length = 0;
-
-         return -1;
-      }
-
-      i = (word_start + word_length);
-   }
-
-   if
-   (
-      add_word_id_to_sequence
-      (
-         ZoO_END_OF_SEQUENCE_ID,
-         sequence,
-         sequence_length,
-         io
-      ) < 0
-   )
-   {
-      free((void *) *sequence);
-
-      *sequence = (ZoO_index *) NULL;
-      *sequence_length = 0;
-
-      return -1;
-   }
-
-   return 0;
-}
diff --git a/src/core/sequence_to_string.c b/src/core/sequence_to_string.c
deleted file mode 100644
index 16fc859..0000000
--- a/src/core/sequence_to_string.c
+++ /dev/null
@@ -1,97 +0,0 @@
-#define _POSIX_C_SOURCE 200809L
-#include <stdlib.h>
-#include <string.h>
-#include <stdint.h> /* defines SIZE_MAX */
-
-#include "../core/char.h"
-#include "../core/index.h"
-
-#include "../cli/cli.h"
-
-#include "../knowledge/knowledge.h"
-
-#include "sequence.h"
-
-/* TODO */
-static int add_word
-(
-   const ZoO_index word_id,
-   const size_t destination_size,
-   struct ZoO_knowledge k [const restrict static 1],
-   ZoO_char destination [const restrict static max_destination_length],
-   size_t destination_used_size [const restrict static 1],
-   const struct ZoO_pipe io [const restrict static 1]
-)
-{
-	const ZoO_char * word;
-	size_t word_size;
-
-	(void) ZoO_knowledge_lock_access(k, io);
-	ZoO_knowledge_get_word(k, word_id, &word, &word_size, io);
-	(void) ZoO_knowledge_unlock_access(k, io);
-
-	if ((destination_used_size + word_size) > max_destination_length)
-	{
-	}
-
-	if
-	(
-		(word_size == 2)
-		&& ZoO_char_is_punctuation(word[0])
-	)
-	{
-		snprintf
-		(
-			(destination + *destination_used_size),
-			word_size,
-			ZoO_CHAR_STRING_SYMBOL,
-			current_sentence
-		);
-	}
-	else
-	{
-	}
-
-   return 0;
-}
-/******************************************************************************/
-/** EXPORTED ******************************************************************/
-/******************************************************************************/
-
-int ZoO_sequence_to_undercase_string
-(
-   const ZoO_index sequence [const restrict static 1],
-   const ZoO_index sequence_length,
-   const ZoO_index max_destination_length,
-   struct ZoO_knowledge k [const restrict static 1],
-   ZoO_char destination [const restrict static max_destination_length],
-   ZoO_index destination_length [const restrict static 1],
-   const struct ZoO_pipe io [const restrict static 1]
-)
-{
-   ZoO_index i;
-   const ZoO_index actual_length = (sequence_length - 1);
-
-   for (i = 0; i < actual_length; ++i)
-   {
-      if
-      (
-         add_word
-         (
-            sequence[i],
-            max_destination_length,
-            k,
-            destination,
-            destination_length,
-            io
-         ) < 0
-      )
-      {
-         *destination_length = 0;
-
-         return -1;
-      }
-   }
-
-   return 0;
-}
diff --git a/src/core/sequence_types.h b/src/core/sequence_types.h
deleted file mode 100644
index c260a8a..0000000
--- a/src/core/sequence_types.h
+++ /dev/null
@@ -1,10 +0,0 @@
-#ifndef _ZoO_CORE_SEQUENCE_TYPES_H_
-#define _ZoO_CORE_SEQUENCE_TYPES_H_
-
-#define ZoO_START_OF_SEQUENCE_ID 0
-#define ZoO_END_OF_SEQUENCE_ID   1
-#define ZoO_ACTION_SEQUENCE_ID   2
-
-#define ZoO_RESERVED_IDS_COUNT   3
-
-#endif