Initial Commit

7 files changed, 226 insertions, 0 deletions

diff --git a/src/core/CMakeLists.txt b/src/core/CMakeLists.txt
new file mode 100644
index 0000000..b864aff
--- /dev/null
+++ b/src/core/CMakeLists.txt
@@ -0,0 +1,8 @@
+set(
+   SRC_FILES ${SRC_FILES}
+   ${CMAKE_CURRENT_SOURCE_DIR}/char.c
+   ${CMAKE_CURRENT_SOURCE_DIR}/index.c
+)
+
+set(SRC_FILES ${SRC_FILES} PARENT_SCOPE)
+
diff --git a/src/core/char.c b/src/core/char.c
new file mode 100644
index 0000000..249ef1c
--- /dev/null
+++ b/src/core/char.c
@@ -0,0 +1,46 @@
+#include <string.h>
+
+#include "char.h"
+
+/* See: "char.c" */
+JH_char JH_char_to_lowercase (const JH_char c)
+{
+   if ((c >= 'A') && (c <= 'Z'))
+   {
+      return 'z' - ('Z' - c);
+   }
+
+   return c;
+}
+
+/* See: "char.c" */
+int JH_word_cmp
+(
+   const JH_char word_a [const static 1],
+   const size_t word_a_size,
+   const JH_char word_b [const static 1],
+   const size_t word_b_size
+)
+{
+   int result;
+
+   if (word_a_size < word_b_size)
+   {
+      result =
+         strncmp((const char *) word_a, (const char *) word_b, word_a_size);
+
+      return (result == 0) ? -1 : result;
+   }
+   else if (word_b_size < word_a_size)
+   {
+      result =
+         strncmp((const char *) word_a, (const char *) word_b, word_b_size);
+
+      return (result == 0) ? 1 : result;
+   }
+   else
+   {
+      return strncmp((const char *) word_a, (const char *) word_b, word_a_size);
+   }
+}
+
diff --git a/src/core/char.h b/src/core/char.h
new file mode 100644
index 0000000..fb4998e
--- /dev/null
+++ b/src/core/char.h
@@ -0,0 +1,27 @@
+#ifndef _JH_CORE_CHAR_H_
+#define _JH_CORE_CHAR_H_
+
+#include "char_types.h"
+
+/* Compares two words. {word_a} does not have to be null terminated. */
+/*@
+ @ requires null_terminated_string(word_b);
+ @ requires ((length(word_a) * sizeof(JH_char)) == word_a_size);
+ @ ensures ((\result == 1) || (\result == 0) || (\result == -1));
+ @*/
+int JH_word_cmp
+(
+   const JH_char word_a [const static 1],
+   const size_t word_a_size,
+   const JH_char word_b [const static 1],
+   const size_t word_b_size
+);
+
+/*
+ * Returns the lowercase equivalent of JH_char that are included in ['A','Z'].
+ * Other JH_char are returned untouched.
+ */
+JH_char JH_char_to_lowercase (const JH_char c);
+
+#endif
+
diff --git a/src/core/char_types.h b/src/core/char_types.h
new file mode 100644
index 0000000..5383dfd
--- /dev/null
+++ b/src/core/char_types.h
@@ -0,0 +1,10 @@
+#ifndef _JH_CORE_CHAR_TYPES_H_
+#define _JH_CORE_CHAR_TYPES_H_
+
+/* JH_char = UTF-8 char */
+typedef char JH_char;
+
+/* Functions that can handle UTF-8 'char' will use this symbol. */
+#define JH_CHAR_STRING_SYMBOL "%s"
+
+#endif
diff --git a/src/core/index.c b/src/core/index.c
new file mode 100644
index 0000000..ffddb97
--- /dev/null
+++ b/src/core/index.c
@@ -0,0 +1,82 @@
+#include <limits.h>
+#include <stdlib.h>
+
+#include "index.h"
+
+#if (RAND_MAX < UCHAR_MAX)
+   #error "RAND_MAX < UCHAR_MAX, unable to generate random numbers."
+#endif
+
+#if (RAND_MAX == 0)
+   #error "RAND_MAX is included in [0, 0]. What are you even doing?"
+#endif
+
+/*
+ * Returns a random unsigned char.
+ */
+static unsigned char random_uchar (void)
+{
+   return
+   (unsigned char)
+   (
+      /* FIXME: Do floats allow enough precision for this? */
+      (
+         ((float) rand())
+         / ((float) RAND_MAX)
+      )
+      * ((float) UCHAR_MAX)
+   );
+}
+
+/* See: "index.h" */
+JH_index JH_index_random (void)
+{
+   JH_index i;
+   JH_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(JH_index); ++i)
+   {
+      result_bytes[i] = random_uchar();
+   }
+
+   return result;
+}
+
+/* See: "index.h" */
+JH_index JH_index_random_up_to (const JH_index max)
+{
+   return
+   (JH_index)
+   (
+      /* FIXME: Do floats allow enough precision for this? */
+      (
+         ((float) JH_index_random())
+         / ((float) JH_INDEX_MAX)
+      )
+      * ((float) max)
+   );
+}
+
+int JH_index_cmp (const JH_index a, const JH_index b)
+{
+   if (a < b)
+   {
+      return -1;
+   }
+   else if (a > b)
+   {
+      return 1;
+   }
+   else
+   {
+      return 0;
+   }
+}
diff --git a/src/core/index.h b/src/core/index.h
new file mode 100644
index 0000000..66b2540
--- /dev/null
+++ b/src/core/index.h
@@ -0,0 +1,26 @@
+#ifndef _JH_CORE_INDEX_H_
+#define _JH_CORE_INDEX_H_
+
+#include "index_types.h"
+
+/*
+ * Returns a random JH_index.
+ */
+/*@
+   ensures (\result <= JH_INDEX_MAX);
+   assigns \result;
+@*/
+JH_index JH_index_random (void);
+
+/*
+ * Returns a random JH_index, included in [0, limit]
+ */
+/*@
+   ensures (\result <= limit);
+   assigns \result;
+@*/
+JH_index JH_index_random_up_to (const JH_index limit);
+
+int JH_index_cmp (const JH_index a, const JH_index b);
+
+#endif
diff --git a/src/core/index_types.h b/src/core/index_types.h
new file mode 100644
index 0000000..9131569
--- /dev/null
+++ b/src/core/index_types.h
@@ -0,0 +1,27 @@
+#ifndef _JH_CORE_INDEX_TYPES_H_
+#define _JH_CORE_INDEX_TYPES_H_
+
+#include "../pervasive.h"
+
+/*
+ * JH_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>
+#include <stdint.h>
+
+/* Must be unsigned. */
+typedef unsigned int JH_index;
+
+/* Must be > 0. */
+#define JH_INDEX_MAX UINT_MAX
+
+#ifndef JH_RUNNING_FRAMA_C
+   #if (JH_INDEX_MAX > SIZE_MAX)
+      #error "JH_index should not be able to go higher than a size_t variable."
+   #endif
+#endif
+
+#endif