menu fised

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

diff --git a/components/cic_acic/doubleTypeInference.ml b/components/cic_acic/doubleTypeInference.ml
index fd96270467aa746901de0ff2ba7e9d175f186197..905d1e6bc0be63568a8998ac6936f48cb59d2a78 100644 (file)
--- a/components/cic_acic/doubleTypeInference.ml
+++ b/components/cic_acic/doubleTypeInference.ml
@@ -33,6 +33,8 @@ exception WrongUriToMutualInductiveDefinitions of string;;
 exception ListTooShort;;
 exception RelToHiddenHypothesis;;
 
+(*CSC: must alfa-conversion be considered or not? *)
+
 let xxx_type_of_aux' m c t =
  try 
    Some (fst (CicTypeChecker.type_of_aux' m c t CicUniv.empty_ugraph))
@@ -49,6 +51,8 @@ let rec does_not_occur n =
   function
      C.Rel m when m = n -> false
    | C.Rel _
+(* FG/CSC: maybe we assume the meta is guarded so we do not recur on its *)
+(*         explicit subsitutions (copied from the kernel) ???            *)
    | C.Meta _
    | C.Sort _
    | C.Implicit _ -> true 
@@ -163,75 +167,6 @@ let rec beta_reduce =
         C.CoFix (i,fl')
 ;;
 
-(* syntactic_equality up to the                 *)
-(* distinction between fake dependent products  *)
-(* and non-dependent products, alfa-conversion  *)
-(*CSC: must alfa-conversion be considered or not? *)
-let syntactic_equality t t' =
- let module C = Cic in
- let rec syntactic_equality t t' =
-  if t = t' then true
-  else
-   match t, t' with
-      C.Var (uri,exp_named_subst), C.Var (uri',exp_named_subst') ->
-       UriManager.eq uri uri' &&
-        syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
-    | C.Cast (te,ty), C.Cast (te',ty') ->
-       syntactic_equality te te' &&
-        syntactic_equality ty ty'
-    | C.Prod (_,s,t), C.Prod (_,s',t') ->
-       syntactic_equality s s' &&
-        syntactic_equality t t'
-    | C.Lambda (_,s,t), C.Lambda (_,s',t') ->
-       syntactic_equality s s' &&
-        syntactic_equality t t'
-    | C.LetIn (_,s,t), C.LetIn(_,s',t') ->
-       syntactic_equality s s' &&
-        syntactic_equality t t'
-    | C.Appl l, C.Appl l' ->
-       List.fold_left2 (fun b t1 t2 -> b && syntactic_equality t1 t2) true l l'
-    | C.Const (uri,exp_named_subst), C.Const (uri',exp_named_subst') ->
-       UriManager.eq uri uri' &&
-        syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
-    | C.MutInd (uri,i,exp_named_subst), C.MutInd (uri',i',exp_named_subst') ->
-       UriManager.eq uri uri' && i = i' &&
-        syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
-    | C.MutConstruct (uri,i,j,exp_named_subst),
-      C.MutConstruct (uri',i',j',exp_named_subst') ->
-       UriManager.eq uri uri' && i = i' && j = j' &&
-        syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
-    | C.MutCase (sp,i,outt,t,pl), C.MutCase (sp',i',outt',t',pl') ->
-       UriManager.eq sp sp' && i = i' &&
-        syntactic_equality outt outt' &&
-         syntactic_equality t t' &&
-          List.fold_left2
-           (fun b t1 t2 -> b && syntactic_equality t1 t2) true pl pl'
-    | C.Fix (i,fl), C.Fix (i',fl') ->
-       i = i' &&
-        List.fold_left2
-         (fun b (_,i,ty,bo) (_,i',ty',bo') ->
-           b && i = i' &&
-            syntactic_equality ty ty' &&
-             syntactic_equality bo bo') true fl fl'
-    | C.CoFix (i,fl), C.CoFix (i',fl') ->
-       i = i' &&
-        List.fold_left2
-         (fun b (_,ty,bo) (_,ty',bo') ->
-           b &&
-            syntactic_equality ty ty' &&
-             syntactic_equality bo bo') true fl fl'
-    | _, _ -> false (* we already know that t != t' *)
- and syntactic_equality_exp_named_subst exp_named_subst1 exp_named_subst2 =
-  List.fold_left2
-   (fun b (_,t1) (_,t2) -> b && syntactic_equality t1 t2) true
-   exp_named_subst1 exp_named_subst2
- in
-  try
-   syntactic_equality t t'
-  with
-   _ -> false
-;;
-
 let rec split l n =
  match (l,n) with
     (l,0) -> ([], l)
@@ -303,6 +238,18 @@ let type_of_mutual_inductive_constr uri i j =
 
 let pack_coercion = ref (fun _ _ _ -> assert false);;
 
+let profiler_for_find = HExtlib.profile "CicHash ADD" ;;
+
+let cic_CicHash_add a b c =  
+  profiler_for_find.HExtlib.profile (Cic.CicHash.add a b) c
+;;
+
+let profiler_for_find1 = HExtlib.profile "CicHash MEM" ;;
+
+let cic_CicHash_mem a b =  
+  profiler_for_find1.HExtlib.profile (Cic.CicHash.mem a) b
+;;
+
 (* 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             *)
@@ -609,7 +556,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
          None ->
           (* No expected type *)
           {synthesized = synthesized' ; expected = None}, synthesized
-       | Some ty when syntactic_equality synthesized' ty ->
+       | Some ty when CicUtil.alpha_equivalence synthesized' ty ->
           (* The expected type is synthactically equal to *)
           (* the synthesized type. Let's forget it.       *)
           {synthesized = synthesized' ; expected = None}, synthesized
@@ -617,8 +564,8 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
           {synthesized = synthesized' ; expected = Some expectedty'},
           expectedty'
      in
-      assert (not (Cic.CicHash.mem subterms_to_types t));
-      Cic.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 =