"Performance bug" fixed: I removed a whd in the does_not_occur function.

[helm.git] / helm / software / components / cic_proof_checking / cicTypeChecker.ml

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) ->