From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 12 Mar 2008 18:52:54 +0000 (+0000)
Subject: Almost always correct optimization: during unification, a meta-closed term and
X-Git-Tag: make_still_working~5534
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f45e7c2b52e83e4461056d386dcb768d7b25df05;p=helm.git

Almost always correct optimization: during unification, a meta-closed term and
a term that is not meta closed are not tried for convertibility. This greatly
speeds up, for instance, some examples in Bertrand.
---

diff --git a/helm/software/components/cic_unification/cicUnification.ml b/helm/software/components/cic_unification/cicUnification.ml
index 8044878b2..ff5f39605 100644
--- a/helm/software/components/cic_unification/cicUnification.ml
+++ b/helm/software/components/cic_unification/cicUnification.ml
@@ -318,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