X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicTypeChecker.ml;h=fbb384d5e66eb63909ae88aafaebb3a75f3c7c4e;hb=6beda5aa100b617b75d88a5a519b5022c99208a0;hp=0614eabfd61957ab8d66b55e42091d8ac3498a4e;hpb=5c8c7f0ae6fdbba432286c01feac114873a1cfe9;p=helm.git

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index 0614eabfd..fbb384d5e 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 if t <> optimized_t then 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