Native compiler: hash-consing of generated code and values.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16363 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 13 insertions, 0 deletions

diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 2f317ca96..f03d4f799 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -8,6 +8,7 @@
 open Term
 open Names
 open Errors
+open Util
 
 (** This modules defines the representation of values internally used by
 the native compiler *)
@@ -30,10 +31,22 @@ type annot_sw = {
     asw_prefix : string
   }
 
+(* We compare only what is relevant for generation of ml code *)
+let eq_annot_sw asw1 asw2 =
+  eq_ind asw1.asw_ind asw2.asw_ind &&
+  String.equal asw1.asw_prefix asw2.asw_prefix
+
+open Hashset.Combine
+
+let hash_annot_sw asw =
+  combine (Hashtbl.hash asw.asw_ind) (Hashtbl.hash asw.asw_prefix)
+
 type sort_annot = string * int
 
 type rec_pos = int array
 
+let eq_rec_pos = Array.equal Int.equal
+
 type atom = 
   | Arel of int
   | Aconstant of constant