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 954c4835bcd05b3d7a126ed7483656f0bcdc08bc..318d1e742be3aa5e4daf0436574e04a9d8d87b5c 100644 (file)
--- 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) ->