From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 9 Mar 2008 18:28:05 +0000 (+0000)
Subject: Added ad-hoc optimization for check_metasenv_consistency, case Rel to Let-in
X-Git-Tag: make_still_working~5549
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8ef5515dd9adff2cd185123e371ee4bd84a890d0;p=helm.git

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

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