From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 27 Mar 2006 14:01:26 +0000 (+0000)
Subject: "Performance bug" fixed: I removed a whd in the does_not_occur function.
X-Git-Tag: 0.4.95@7852~1555
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9af2c02b054a92804da88cb06d6699ce21b943c0;p=helm.git

"Performance bug" fixed: I removed a whd in the does_not_occur function.
Consequences:
  1. incredible speed-up in the type-checking of certain inductive types
  2. "dummy" occurrences (i.e. occurrences that are doomed to disappear because
     of reduction) are now rejected (they used to be accepted). Coq has the
     same behaviour.
---

diff --git a/components/cic_proof_checking/cicTypeChecker.ml b/components/cic_proof_checking/cicTypeChecker.ml
index c4b7f8cbf..3df3dc354 100644
--- a/components/cic_proof_checking/cicTypeChecker.ml
+++ b/components/cic_proof_checking/cicTypeChecker.ml
@@ -240,12 +240,16 @@ and type_of_variable ~logger uri ugraph =
 
 and does_not_occur ?(subst=[]) context n nn te =
  let module C = Cic in
-   (*CSC: whd sembra essere superflua perche' un caso in cui l'occorrenza *)
-   (*CSC: venga mangiata durante la whd sembra presentare problemi di *)
-   (*CSC: universi                                                    *)
-   match CicReduction.whd ~subst context te with
+   match te with
       C.Rel m when m > n && m <= nn -> false
-    | C.Rel _
+    | C.Rel m ->
+       (try
+         (match List.nth context (m-1) with
+             Some (_,C.Def (bo,_)) ->
+              does_not_occur ~subst context n nn (CicSubstitution.lift m bo)
+           | _ -> true)
+        with
+         Failure _ -> assert false)
     | C.Sort _
     | C.Implicit _ -> true
     | C.Meta (_,l) ->
@@ -253,7 +257,12 @@ and does_not_occur ?(subst=[]) context n nn te =
         (fun x i ->
           match x with
              None -> i
-           | Some x -> i && does_not_occur ~subst context n nn x) l true
+           | Some x -> i && does_not_occur ~subst context n nn x) l true &&
+       (try
+         let (canonical_context,term,ty) = CicUtil.lookup_subst n subst in
+          does_not_occur ~subst context n nn (CicSubstitution.subst_meta l term)
+        with
+         CicUtil.Subst_not_found _ -> true)
     | C.Cast (te,ty) ->
        does_not_occur ~subst context n nn te && does_not_occur ~subst context n nn ty
     | C.Prod (name,so,dest) ->