From ebb2f4bda5f7c5c7fc26d3aa1e17312f8900da4a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 28 Apr 2008 17:43:33 +0000 Subject: [PATCH] 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 --- .../components/cic_proof_checking/cicTypeChecker.ml | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) 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 *) -- 2.39.2