From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 10 Mar 2008 10:39:45 +0000 (+0000)
Subject: check_metasenv_consistency:
X-Git-Tag: make_still_working~5546
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c4f53600c65b71ae9e213a54bade36c0c2e2ae37;p=helm.git

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

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