From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sat, 26 Nov 2005 11:56:07 +0000 (+0000)
Subject: Module CicHash (hash-tables over CIC terms based on physical equality) moved
X-Git-Tag: make_still_working~8091
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=86241d46558e3a4979fc786e47ce78f90eb9190c;p=helm.git

Module CicHash (hash-tables over CIC terms based on physical equality) moved
into Cic.
---

diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml
index aacaabda9..624a30216 100644
--- a/helm/ocaml/cic/cic.ml
+++ b/helm/ocaml/cic/cic.ml
@@ -222,3 +222,12 @@ type anntarget =
  | Conjecture of annconjecture
  | Hypothesis of annhypothesis
 
+module CicHash =
+ Hashtbl.Make
+  (struct
+    type t = term
+    let equal = (==)
+    let hash = Hashtbl.hash
+   end)
+;;
+
diff --git a/helm/ocaml/cic_acic/cic2acic.ml b/helm/ocaml/cic_acic/cic2acic.ml
index 1cdabc09f..194361622 100644
--- a/helm/ocaml/cic_acic/cic2acic.ml
+++ b/helm/ocaml/cic_acic/cic2acic.ml
@@ -118,7 +118,7 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes
     if global_computeinnertypes then
      D.double_type_of metasenv context t expectedty
     else
-     D.CicHash.empty ()
+     Cic.CicHash.create 1 (* empty table *)
    in
 (*
    let time2 = Sys.time () in
@@ -157,7 +157,7 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes
 (* *)
         let {D.synthesized = synthesized; D.expected = expected} =
          if computeinnertypes then
-          D.CicHash.find terms_to_types tt
+          Cic.CicHash.find terms_to_types tt
          else
           (* We are already in an inner-type and Coscoy's double *)
           (* type inference algorithm has not been applied.      *)
diff --git a/helm/ocaml/cic_acic/doubleTypeInference.ml b/helm/ocaml/cic_acic/doubleTypeInference.ml
index 692872439..b28359bd7 100644
--- a/helm/ocaml/cic_acic/doubleTypeInference.ml
+++ b/helm/ocaml/cic_acic/doubleTypeInference.ml
@@ -323,20 +323,6 @@ let type_of_mutual_inductive_constr uri i j =
     | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
 ;;
 
-module CicHash =
-  struct
-    module Tmp = 
-     Hashtbl.Make
-      (struct
-        type t = Cic.term
-        let equal = (==)
-        let hash = Hashtbl.hash
-       end)
-    include Tmp
-    let empty () = Tmp.create 1
-  end
-;;
-
 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
 let rec type_of_aux' subterms_to_types metasenv context t expectedty =
  (* Coscoy's double type-inference algorithm             *)
@@ -640,8 +626,8 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
           {synthesized = synthesized' ; expected = Some expectedty'},
           expectedty'
      in
-      assert (not (CicHash.mem subterms_to_types t));
-      CicHash.add subterms_to_types t types ;
+      assert (not (Cic.CicHash.mem subterms_to_types t));
+      Cic.CicHash.add subterms_to_types t types ;
       res
 
  and visit_exp_named_subst context uri exp_named_subst =
@@ -746,7 +732,7 @@ and type_of_branch context argsno need_dummy outtype term constype =
 ;;
 
 let double_type_of metasenv context t expectedty =
- let subterms_to_types = CicHash.create 503 in
+ let subterms_to_types = Cic.CicHash.create 503 in
   ignore (type_of_aux' subterms_to_types metasenv context t expectedty) ;
   subterms_to_types
 ;;
diff --git a/helm/ocaml/cic_acic/doubleTypeInference.mli b/helm/ocaml/cic_acic/doubleTypeInference.mli
index 138aad834..892e09f8a 100644
--- a/helm/ocaml/cic_acic/doubleTypeInference.mli
+++ b/helm/ocaml/cic_acic/doubleTypeInference.mli
@@ -14,16 +14,9 @@ val number_new_type_of_aux'_prop: int ref
 
 type types = {synthesized : Cic.term ; expected : Cic.term option};;
 
-module CicHash :
-  sig
-    type 'a t
-    val find : 'a t -> Cic.term -> 'a
-    val empty: unit -> 'a t
-  end
-;;
-
 val double_type_of :
- Cic.metasenv -> Cic.context -> Cic.term -> Cic.term option -> types CicHash.t
+ Cic.metasenv -> Cic.context -> Cic.term -> Cic.term option ->
+  types Cic.CicHash.t
 
 (** Auxiliary functions **)