From c4f53600c65b71ae9e213a54bade36c0c2e2ae37 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 10 Mar 2008 10:39:45 +0000 Subject: [PATCH] check_metasenv_consistency: big ad-hoc performance improvement propagated from CicTypeChecker to CicRefine. This really cuts down the total refinement time in some situations (freescale). --- .../components/cic_unification/cicRefine.ml | 19 +++++++++++++++++-- 1 file changed, 17 insertions(+), 2 deletions(-) diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index 954c4835b..318d1e742 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -956,12 +956,27 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t _,None -> l @ [None],subst,metasenv,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 let subst',metasenv',ugraph' = (try (*prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' * il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");*) - fo_unif_subst subst context metasenv t ct ugraph - with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm ~metasenv subst t) (CicMetaSubst.ppterm ~metasenv subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e)))))) + fo_unif_subst subst context metasenv optimized_t ct ugraph + with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm ~metasenv subst optimized_t) (CicMetaSubst.ppterm ~metasenv subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e)))))) in l @ [Some t],subst',metasenv',ugraph' | Some t,Some (_,C.Decl ct) -> -- 2.39.2