From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 28 Apr 2008 17:43:33 +0000 (+0000)
Subject: In guarded by destructors, avoid computing the (whd ~delta:true) unless the
X-Git-Tag: make_still_working~5284
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ebb2f4bda5f7c5c7fc26d3aa1e17312f8900da4a;p=helm.git

In guarded by destructors, avoid computing the (whd ~delta:true) unless the
check fails. This is a major speed up, for instance for
cic:/Coq/ZArith/Zsqrt/sqrtrempos.con
---

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index a5e745af3..35015e541 100644
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -838,7 +838,9 @@ and guarded_by_destructors
 =
  let module C = Cic in
  let module U = UriManager in
-  match CicReduction.whd ~subst context t with
+  let t = CicReduction.whd ~delta:false ~subst context t in
+  let res =
+   match t with
      C.Rel m when m > n && m <= nn -> false
    | C.Rel m ->
       (match List.nth context (m-1) with
@@ -995,6 +997,14 @@ and guarded_by_destructors
       List.fold_right
        (fun t i -> i && guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes t)
        tl true
+  in
+   if res then res
+   else
+    let t' = CicReduction.whd ~subst context t in
+     if t = t' then
+      false
+     else
+      guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes t'
 
 (* the boolean h means already protected *)
 (* args is the list of arguments the type of the constructor that may be *)