From 3add6ac24088e2a1d91a41123f433e2c2b0b796a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 27 Mar 2006 14:01:26 +0000 Subject: [PATCH] "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. --- .../cic_proof_checking/cicTypeChecker.ml | 21 +++++++++++++------ 1 file changed, 15 insertions(+), 6 deletions(-) diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml index c4b7f8cbf..3df3dc354 100644 --- 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) -> -- 2.39.2