subst_vars optimized for the explicit_named_subst=[] case (the most common

[helm.git] / helm / ocaml / cic_acic / doubleTypeInference.ml

diff --git a/helm/ocaml/cic_acic/doubleTypeInference.ml b/helm/ocaml/cic_acic/doubleTypeInference.ml
index 69287243918419218848f810371f5c0c1843fa83..30a8f5c290fdaac79a3ecc28f10269f2d2db611f 100644 (file)
--- a/helm/ocaml/cic_acic/doubleTypeInference.ml
+++ b/helm/ocaml/cic_acic/doubleTypeInference.ml
@@ -23,6 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
+(* $Id$ *)
+
 exception Impossible of int;;
 exception NotWellTyped of string;;
 exception WrongUriToConstant of string;;
@@ -84,9 +86,6 @@ let rec does_not_occur n =
    | C.Fix (_,fl) ->
       let len = List.length fl in
        let n_plus_len = n + len in
-       let tys =
-        List.map (fun (n,_,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
-       in
         List.fold_right
          (fun (_,_,ty,bo) i ->
            i && does_not_occur n ty &&
@@ -95,9 +94,6 @@ let rec does_not_occur n =
    | C.CoFix (_,fl) ->
       let len = List.length fl in
        let n_plus_len = n + len in
-       let tys =
-        List.map (fun (n,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
-       in
         List.fold_right
          (fun (_,ty,bo) i ->
            i && does_not_occur n ty &&
@@ -114,7 +110,7 @@ let rec beta_reduce =
        let exp_named_subst' =
         List.map (function (i,t) -> i, beta_reduce t) exp_named_subst
        in
-        C.Var (uri,exp_named_subst)
+        C.Var (uri,exp_named_subst')
     | C.Meta (n,l) ->
        C.Meta (n,
         List.map
@@ -323,20 +319,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 +622,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 +728,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
 ;;