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 aacaabda95490e4f9e1cfc9df946f6be70e08c8c..624a3021640ea23eb3b961a06578dbf72ed4d539 100644 (file)
--- 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 1cdabc09fe673dd8ca222b5e376772612318e255..1943616226aa19005b0031cf4f86a8c649b72b8f 100644 (file)
--- 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 69287243918419218848f810371f5c0c1843fa83..b28359bd7857a9ebf0b36e092ba7ca9991b4c47b 100644 (file)
--- 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 138aad83440bcb062b00e637ca8a93bbfdf3898e..892e09f8ac4d1172f96f4f1a8c42cbb265fca5f6 100644 (file)
--- 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 **)