"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/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index c4b7f8cbf6f8a521c8f1d7fc3682b0a3aecfd39b..3df3dc3549ea5cda47b0a891627fb52a694f5f0e 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/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) ->