From 8ef5515dd9adff2cd185123e371ee4bd84a890d0 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 9 Mar 2008 18:28:05 +0000 Subject: [PATCH] Added ad-hoc optimization for check_metasenv_consistency, case Rel to Let-in vs Def. Rationale: this is the case of an IRL when the metavariable is created in a context with definitions. Without this optimization, a (possibly expensive) reduction is always triggered. Note: this should be better handled using a reduction strategy based on heights. --- .../cic_proof_checking/cicTypeChecker.ml | 25 +++++++++++++++---- 1 file changed, 20 insertions(+), 5 deletions(-) diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml index 0614eabfd..ff56df73e 100644 --- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml +++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml @@ -1504,8 +1504,25 @@ and check_metasenv_consistency ~logger ~subst metasenv context match (t,ct) with | _,None -> ugraph | Some t,Some (_,C.Def (ct,_)) -> + (*CSC: the following optimization is to avoid a possibly expensive + reduction that can be easily avoided and that is quite + frequent. However, this is better handled using levels to + control reduction *) + let optimized_t = + match t with + Cic.Rel n -> + (try + match List.nth context (n - 1) with + Some (_,C.Def (te,_)) -> S.lift n te + | _ -> t + with + Failure _ -> t) + | _ -> t + in +if t <> optimized_t && optimized_t = ct then prerr_endline "!!!!!!!!!!!!!!!" +else prerr_endline ("@@ " ^ CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm optimized_t ^ " <==> " ^ CicPp.ppterm ct); let b,ugraph1 = - R.are_convertible ~subst ~metasenv context t ct ugraph + R.are_convertible ~subst ~metasenv context optimized_t ct ugraph in if not b then raise @@ -2042,10 +2059,8 @@ end; (match (CicReduction.whd ~subst context hetype) with Cic.Prod (n,s,t) -> let b,ugraph1 = -(* -if hety <> s then -prerr_endline ("AAA22: " ^ CicPp.ppterm hete ^ ": " ^ CicPp.ppterm hety ^ " <==> " ^ CicPp.ppterm s); -*) +(*if (match hety,s with Cic.Sort _,Cic.Sort _ -> false | _,_ -> true) && hety <> s then( +prerr_endline ("AAA22: " ^ CicPp.ppterm hete ^ ": " ^ CicPp.ppterm hety ^ " <==> " ^ CicPp.ppterm s); let res = CicReduction.are_convertible ~subst ~metasenv context hety s ugraph in prerr_endline "#"; res) else*) CicReduction.are_convertible ~subst ~metasenv context hety s ugraph in -- 2.39.2