alpha equivalence test factorized and moved to CicUtil

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

diff --git a/components/cic_acic/doubleTypeInference.ml b/components/cic_acic/doubleTypeInference.ml
index 1ea800a6b9307ec13065fe6d5c853f01a1090ba8..ca5848369c8f735bf410d5308daa67dfe7c9c72a 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))
@@ -163,75 +165,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)
@@ -621,7 +554,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