Debugging print removed.

[helm.git] / helm / software / components / cic_proof_checking / cicTypeChecker.ml

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index 87a0ca0546f9b77f78b02da7a8380fd78f6cdc0f..fbb384d5e66eb63909ae88aafaebb3a75f3c7c4e 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 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 
@@ -1654,7 +1671,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
         List.fold_right (
           fun x (l,ugraph) -> 
             let ty,ugraph1 = type_of_aux ~logger context x ugraph in
-            let _,ugraph1 = type_of_aux ~logger  context ty ugraph1 in
+            (*let _,ugraph1 = type_of_aux ~logger  context ty ugraph1 in*)
               ((x,ty)::l,ugraph1)) 
           tl ([],ugraph1) 
        in
@@ -2042,6 +2059,8 @@ end;
         (match (CicReduction.whd ~subst context hetype) with 
               Cic.Prod (n,s,t) ->
                let b,ugraph1 = 
+(*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