X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_paramodulation%2Fhash.c;fp=matita%2Fcomponents%2Fng_paramodulation%2Fhash.c;h=262c36e0fd9816d0a331a56437d68be3a4a3aeaa;hb=6b76c5b3b82753966cabffd8536d8dd9f8cada20;hp=0000000000000000000000000000000000000000;hpb=aa5c8c99c9f7ae285883cff133fc02b3d064888c;p=helm.git

diff --git a/matita/components/ng_paramodulation/hash.c b/matita/components/ng_paramodulation/hash.c
new file mode 100644
index 000000000..262c36e0f
--- /dev/null
+++ b/matita/components/ng_paramodulation/hash.c
@@ -0,0 +1,152 @@
+/***********************************************************************/
+/*                                                                     */
+/*                                OCaml                                */
+/*                                                                     */
+/*            Xavier Leroy, projet Cristal, INRIA Rocquencourt         */
+/*                                                                     */
+/*  Copyright 1996 Institut National de Recherche en Informatique et   */
+/*  en Automatique.  All rights reserved.  This file is distributed    */
+/*  under the terms of the GNU Library General Public License, with    */
+/*  the special exception on linking described in file ../LICENSE.     */
+/*                                                                     */
+/***********************************************************************/
+
+/* $Id: hash.c 12149 2012-02-10 16:15:24Z doligez $ */
+
+/* The generic hashing primitive */
+
+/* The interface of this file is in "mlvalues.h" (for [caml_hash_variant])
+   and in "hash.h" (for the other exported functions). */
+
+#include "mlvalues.h"
+#include "custom.h"
+#include "memory.h"
+#include "hash.h"
+#include "address_class.h"
+
+/*#ifdef ARCH_INT64_TYPE
+#include "int64_native.h"
+#else
+#include "int64_emul.h"
+#endif*/
+
+/* The old implementation */
+
+static uintnat hash_accu;
+static intnat hash_univ_limit, hash_univ_count;
+
+static void hash_aux(value obj);
+
+CAMLprim value caml_hash_univ_param(value count, value limit, value obj)
+{
+  hash_univ_limit = Long_val(limit);
+  hash_univ_count = Long_val(count);
+  hash_accu = 0;
+  hash_aux(obj);
+  return Val_long(hash_accu & 0x3FFFFFFF);
+  /* The & has two purposes: ensure that the return value is positive
+     and give the same result on 32 bit and 64 bit architectures. */
+}
+
+#define Alpha 65599
+#define Beta 19
+#define Combine(new)  (hash_accu = hash_accu * Alpha + (new))
+#define Combine_small(new) (hash_accu = hash_accu * Beta + (new))
+
+static void hash_aux(value obj)
+{
+  unsigned char * p;
+  mlsize_t i, j;
+  tag_t tag;
+
+  hash_univ_limit--;
+  if (hash_univ_count < 0 || hash_univ_limit < 0) return;
+
+ again:
+  if (Is_long(obj)) {
+    hash_univ_count--;
+    Combine(Long_val(obj));
+    return;
+  }
+
+  /* Pointers into the heap are well-structured blocks. So are atoms.
+     We can inspect the block contents. */
+
+  CAMLassert (Is_block (obj));
+  if (Is_in_value_area(obj)) {
+    tag = Tag_val(obj);
+    switch (tag) {
+    case String_tag:
+      hash_univ_count--;
+      i = caml_string_length(obj);
+      for (p = &Byte_u(obj, 0); i > 0; i--, p++)
+        Combine_small(*p);
+      break;
+    case Double_tag:
+      /* For doubles, we inspect their binary representation, LSB first.
+         The results are consistent among all platforms with IEEE floats. */
+      hash_univ_count--;
+#ifdef ARCH_BIG_ENDIAN
+      for (p = &Byte_u(obj, sizeof(double) - 1), i = sizeof(double);
+           i > 0;
+           p--, i--)
+#else
+      for (p = &Byte_u(obj, 0), i = sizeof(double);
+           i > 0;
+           p++, i--)
+#endif
+        Combine_small(*p);
+      break;
+    case Double_array_tag:
+      hash_univ_count--;
+      for (j = 0; j < Bosize_val(obj); j += sizeof(double)) {
+#ifdef ARCH_BIG_ENDIAN
+      for (p = &Byte_u(obj, j + sizeof(double) - 1), i = sizeof(double);
+           i > 0;
+           p--, i--)
+#else
+      for (p = &Byte_u(obj, j), i = sizeof(double);
+           i > 0;
+           p++, i--)
+#endif
+        Combine_small(*p);
+      }
+      break;
+    case Abstract_tag:
+      /* We don't know anything about the contents of the block.
+         Better do nothing. */
+      break;
+    case Infix_tag:
+      hash_aux(obj - Infix_offset_val(obj));
+      break;
+    case Forward_tag:
+      obj = Forward_val (obj);
+      goto again;
+    case Object_tag:
+      hash_univ_count--;
+      Combine(Oid_val(obj));
+      break;
+    case Custom_tag:
+      /* If no hashing function provided, do nothing */
+      if (Custom_ops_val(obj)->hash != NULL) {
+        hash_univ_count--;
+        Combine(Custom_ops_val(obj)->hash(obj));
+      }
+      break;
+    default:
+      hash_univ_count--;
+      Combine_small(tag);
+      i = Wosize_val(obj);
+      while (i != 0) {
+        i--;
+        hash_aux(Field(obj, i));
+      }
+      break;
+    }
+    return;
+  }
+
+  /* Otherwise, obj is a pointer outside the heap, to an object with
+     a priori unknown structure. Use its physical address as hash key. */
+  Combine((intnat) obj);
+}