new message reporting system improves performance significatively

[helm.git] / helm / software / helena / src / basic_rg / brgType.ml

diff --git a/helm/software/helena/src/basic_rg/brgType.ml b/helm/software/helena/src/basic_rg/brgType.ml
index 7c47ff12cd10df8dcd36b266f5a3df39153e20d7..29b73beeb587c85bc58f2918e7ec652132c3648c 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgType.ml
+++ b/helm/software/helena/src/basic_rg/brgType.ml
@@ -14,8 +14,10 @@ module C  = Cps
 module W  = Share
 module L  = Log
 module H  = Hierarchy
-module E  = Entity
 module N  = Level
+module E  = Entity
+module G  = Options
+module S  = Status
 module B  = Brg
 module BE = BrgEnvironment
 module BS = BrgSubstitution
@@ -23,7 +25,7 @@ module BR = BrgReduction
 
 (* Internal functions *******************************************************)
 
-let level = 4
+let level = 3
 
 let message1 st1 m t1 =
    L.et_items1 "In the environment" m st1 t1
@@ -64,7 +66,7 @@ let assert_applicability err f st m u w v =
       | _                                -> assert false (**)
 
 let rec b_type_of err f st m x =
-   log1 "Now checking" m x;
+   if !G.trace >= level then log1 "Now checking" m x;
    match x with
    | B.Sort (a, h)           ->
       let h = H.apply h in f x (B.Sort (a, h)) 
@@ -127,6 +129,4 @@ let rec b_type_of err f st m x =
 
 (* Interface functions ******************************************************)
 
-and type_of err f st m x =
-   let f t u = L.unbox level; f t u in
-   L.box level; b_type_of err f st m x
+and type_of err f st m x = b_type_of err f st m x