X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicUnification.ml;h=ff5f396054795b1fafc2a8567a9da8642143fbf9;hb=aeb225c2bb3291888ce3df279119a8bda4817087;hp=912ae1e8e0cbbee2d4deba85595418032c9ce04b;hpb=e5bcf92808b75387ef4d4ff0f827bf07ad9af2f7;p=helm.git

diff --git a/helm/software/components/cic_unification/cicUnification.ml b/helm/software/components/cic_unification/cicUnification.ml
index 912ae1e8e..ff5f39605 100644
--- a/helm/software/components/cic_unification/cicUnification.ml
+++ b/helm/software/components/cic_unification/cicUnification.ml
@@ -136,7 +136,7 @@ let eta_reduce after_beta_expansion after_beta_expansion_body
  with
   WrongShape -> after_beta_expansion
 
-let rec beta_expand test_equality_only metasenv subst context t arg ugraph =
+let rec beta_expand num test_equality_only metasenv subst context t arg ugraph =
  let module S = CicSubstitution in
  let module C = Cic in
 let foo () =
@@ -197,15 +197,17 @@ let foo () =
            in
            (* TASSI: sure this is in serial? *)
             subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
-        | C.LetIn (nn,s,t) ->
+        | C.LetIn (nn,s,ty,t) ->
            let subst,metasenv,s',ugraph1 = 
              aux metasenv subst n context s ugraph in
+           let subst,metasenv,ty',ugraph1 = 
+             aux metasenv subst n context ty ugraph in
            let subst,metasenv,t',ugraph2 =
-            aux metasenv subst (n+1) ((Some (nn, C.Def (s,None)))::context) t
+            aux metasenv subst (n+1) ((Some (nn, C.Def (s,ty)))::context) t
               ugraph1
            in
            (* TASSI: sure this is in serial? *)
-            subst,metasenv,(C.LetIn (nn, s', t')),ugraph2
+            subst,metasenv,(C.LetIn (nn, s', ty', t')),ugraph2
         | C.Appl l ->
            let subst,metasenv,revl',ugraph1 =
             List.fold_left
@@ -279,7 +281,7 @@ let foo () =
   let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
   let fresh_name =
    FreshNamesGenerator.mk_fresh_name ~subst
-    metasenv context (Cic.Name "Hbeta") ~typ:argty
+    metasenv context (Cic.Name ("Hbeta" ^ string_of_int num)) ~typ:argty
   in
    let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
    let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in
@@ -288,15 +290,15 @@ in profiler_beta_expand.HExtlib.profile foo ()
 
 
 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
-  let subst,metasenv,hd,ugraph =
+  let _,subst,metasenv,hd,ugraph =
     List.fold_right
-      (fun arg (subst,metasenv,t,ugraph) ->
+      (fun arg (num,subst,metasenv,t,ugraph) ->
          let subst,metasenv,t,ugraph1 =
-           beta_expand test_equality_only 
+           beta_expand num test_equality_only 
              metasenv subst context t arg ugraph 
          in
-           subst,metasenv,t,ugraph1 
-      ) args (subst,metasenv,t,ugraph) 
+           num+1,subst,metasenv,t,ugraph1 
+      ) args (1,subst,metasenv,t,ugraph) 
   in
     subst,metasenv,hd,ugraph
 
@@ -316,11 +318,18 @@ and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =
  let module S = CicSubstitution in
  let t1 = deref subst t1 in
  let t2 = deref subst t2 in
- let b,ugraph  = 
+ let (&&&) a b = (a && b) || ((not a) && (not b)) in
+(* let bef = Sys.time () in *)
+ let b,ugraph =
+  if not (CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t1) &&& CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t2)) then
+   false,ugraph
+  else
 let foo () =
    R.are_convertible ~subst ~metasenv context t1 t2 ugraph 
 in profiler_are_convertible.HExtlib.profile foo ()
  in
+(* let aft = Sys.time () in
+if (aft -. bef > 2.0) then prerr_endline ("LEEEENTO: " ^ CicMetaSubst.ppterm_in_context subst ~metasenv t1 context ^ " <===> " ^ CicMetaSubst.ppterm_in_context subst ~metasenv t2 context); *)
    if b then
      subst, metasenv, ugraph 
    else
@@ -508,8 +517,8 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
        in
          fo_unif_subst test_equality_only 
            subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
-   | (C.LetIn (_,s1,t1), t2)  
-   | (t2, C.LetIn (_,s1,t1)) -> 
+   | (C.LetIn (_,s1,ty1,t1), t2)  
+   | (t2, C.LetIn (_,s1,ty1,t1)) -> 
        fo_unif_subst 
         test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
    | (C.Appl l1, C.Appl l2) ->