From 86357b63200368c818bbade20f2d71a3ddbaacb5 Mon Sep 17 00:00:00 2001
From: mdenes
Date: Mon, 25 Mar 2013 14:41:06 +0000
Subject: 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
---
 kernel/nativevalues.ml | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'kernel/nativevalues.ml')

diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 2f317ca969..f03d4f7990 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
-- 
cgit v1.2.3