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 0614eabfd61957ab8d66b55e42091d8ac3498a4e..ff56df73ec7d11f29acab1ddd1e09c49bfab1866 100644 (file)
--- 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